From 9163e2100928f96bf48624190b6ee4051cd8e3af Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 28 Feb 2025 09:46:52 +0100 Subject: [PATCH 01/37] add sanity spec --- certora/specs/sanity.spec | 1 + 1 file changed, 1 insertion(+) create mode 100644 certora/specs/sanity.spec diff --git a/certora/specs/sanity.spec b/certora/specs/sanity.spec new file mode 100644 index 0000000..6b20af0 --- /dev/null +++ b/certora/specs/sanity.spec @@ -0,0 +1 @@ +use builtin rule sanity filtered { f -> f.contract == currentContract } From 21ae7b4220dd1c577396215d5ae54b6edc995eaa Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 28 Feb 2025 09:47:00 +0100 Subject: [PATCH 02/37] add configs --- certora/confs/sanity/sanity-KatToken.conf | 27 ++++++++++++++++ certora/confs/sanity/sanity-MerkleMinter.conf | 31 +++++++++++++++++++ 2 files changed, 58 insertions(+) create mode 100644 certora/confs/sanity/sanity-KatToken.conf create mode 100644 certora/confs/sanity/sanity-MerkleMinter.conf diff --git a/certora/confs/sanity/sanity-KatToken.conf b/certora/confs/sanity/sanity-KatToken.conf new file mode 100644 index 0000000..3ef5b4e --- /dev/null +++ b/certora/confs/sanity/sanity-KatToken.conf @@ -0,0 +1,27 @@ +{ + "assert_autofinder_success": true, + "files": [ + "src/KatToken.sol" + ], + "global_timeout": "7200", + "loop_iter": "2", + "optimistic_loop": true, + "msg": "sanity KatToken", + "packages": [ + "@openzeppelin/merkle-tree=node_modules/@openzeppelin/merkle-tree", + "@openzeppelin-contracts-5.1.0=dependencies/@openzeppelin-contracts-5.1.0", + "forge-std-1.9.4=dependencies/forge-std-1.9.4" + ], + "process": "emv", + "prover_args": [ + "-verifyCache", + "-verifyTACDumps", + "-testMode", + "-checkRuleDigest", + "-callTraceHardFail on" + ], + "server": "production", + "solc": "solc8.28", + "solc_via_ir": false, + "verify": "KatToken:certora/specs/sanity.spec" +} \ No newline at end of file diff --git a/certora/confs/sanity/sanity-MerkleMinter.conf b/certora/confs/sanity/sanity-MerkleMinter.conf new file mode 100644 index 0000000..cf5afdc --- /dev/null +++ b/certora/confs/sanity/sanity-MerkleMinter.conf @@ -0,0 +1,31 @@ +{ + "assert_autofinder_success": true, + "files": [ + "src/MerkleMinter.sol", + "src/KatToken.sol" + ], + "global_timeout": "7200", + "loop_iter": "2", + "optimistic_loop": true, + "link": [ + "MerkleMinter:katToken=KatToken" + ], + "msg": "sanity MerkleMinter", + "packages": [ + "@openzeppelin/merkle-tree=node_modules/@openzeppelin/merkle-tree", + "@openzeppelin-contracts-5.1.0=dependencies/@openzeppelin-contracts-5.1.0", + "forge-std-1.9.4=dependencies/forge-std-1.9.4" + ], + "process": "emv", + "prover_args": [ + "-verifyCache", + "-verifyTACDumps", + "-testMode", + "-checkRuleDigest", + "-callTraceHardFail on" + ], + "server": "production", + "solc": "solc8.28", + "solc_via_ir": false, + "verify": "MerkleMinter:certora/specs/sanity.spec" +} \ No newline at end of file From b50be99dcd3efcc9706a1a1b23173b9aed25556a Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 28 Feb 2025 09:47:17 +0100 Subject: [PATCH 03/37] add script to run everything --- certora/scripts/full-test.py | 201 +++++++++++++++++++++++++++++++++++ 1 file changed, 201 insertions(+) create mode 100644 certora/scripts/full-test.py diff --git a/certora/scripts/full-test.py b/certora/scripts/full-test.py new file mode 100644 index 0000000..59a9029 --- /dev/null +++ b/certora/scripts/full-test.py @@ -0,0 +1,201 @@ +#!/usr/bin/python3 + +import argparse +import glob +import json +import logging +import os +import pathlib +import re +import subprocess + +# matches a commit hash +re_commit = re.compile('[0-9a-f]{40}') +# matches run links +re_link = re.compile('https://.*\\.certora\\.com/output/[0-9a-zA-Z?=/]+') +# matches alerts that are irrelevant +re_alerts_irrelevant = list(map(re.compile, [ + 'will not be accessible in CVL code', + 'Summarization for internal calls .* is unused', + 'Summarization for external calls .* is unused', + 'Type .* has several conflicting declarations', + 'Conflicting types with name', + 'Syntax warning .* Passed `env` argument to an `envfree` method', +])) +# matches alerts to categories +re_alerts_categories = { + 'SLOWDOWN': list(map(re.compile, [ + 'Memory partitioning failed while analyzing contract .* longer running times', + ])), + 'MEMOUT': list(map(re.compile, [ + 'Extremely low available memory', + ])), + 'HARDTIMEOUT': list(map(re.compile, [ + 'Reached global timeout', + ])), + 'ERROR': list(map(re.compile, [ + 'An internal Prover error occurred', + ])), +} + +__cleanup_commands = [ + 'find ./ -iname "treeView" -exec rm -rf {} \\;', + 'find ./ -iname "*.tar.gz" -exec rm -rf {} \\;', + 'find ./ -iname "*.tac" -exec rm -rf {} \\;', +] + +ARGS: argparse.Namespace = None + +def __load_links(): + return json.load(open(ARGS.links)) + +def __execute(conf: pathlib.Path, msg: str, opts=[]): + cmd = ['certoraRun', str(conf), '--msg', f'{ARGS.msg} {msg}', *opts] + + if ARGS.server is not None: + cmd += ['--server', ARGS.server] + if ARGS.group_id is not None: + cmd += ['--group_id', ARGS.group_id] + if ARGS.version is not None: + if re_commit.match(ARGS.version) is None: + cmd += ['--prover_version', ARGS.version] + else: + cmd += ['--commit_sha1', ARGS.version] + + logging.debug(f'running {' '.join(cmd)}') + if ARGS.dry: + return '' + try: + out = subprocess.run(cmd, stdout=subprocess.PIPE, stderr=subprocess.STDOUT).stdout.decode() + logging.debug(out) + return out + except subprocess.CalledProcessError as e: + logging.error(e) + raise e + +def __links(out: str): + for m in re_link.finditer(out): + yield m.group(0) + +def __start_run_all(config: dict): + re_filter = re.compile(ARGS.filter) + for conf in ARGS.search.rglob('*.conf'): + if re_filter.search(str(conf)) is None: + continue + c = config.get(conf.name, None) + match c: + case None: + logging.info(f'combined for {conf.name}') + yield from __links(__execute(conf, conf.name)) + case 'skip': + logging.info(f'skipping {conf.name}') + case 'individual-rules': + logging.info(f'individually for {conf.name}') + yield from __links(__execute(conf, f'{conf.name} individually', ['--split_rules', '*'])) + case _: + logging.info(f'custom config for {conf.name}') + for name,opts in c.items(): + yield from __links(__execute(conf, f'{conf.name} {name}', opts)) + +def cmd_start(): + search = [ + ARGS.config, + pathlib.Path(__file__).parent / ARGS.config, + ] + found = False + for s in search: + if s.exists(): + logging.info(f'loading config from {s}') + config = json.load(open(s)) + found = True + break + if not found: + logging.warning(f'config file {ARGS.config} does not exist') + config = {} + + links = list(__start_run_all(config)) + if ARGS.keep_links: + links = __load_links() + links + if not ARGS.dry: + json.dump(links, open(ARGS.links, 'w'), indent=4) + +def cmd_download(): + links = __load_links() + logging.info(f'loaded {len(links)} from {ARGS.links}') + os.makedirs(ARGS.download_dir, exist_ok=True) + + for link in links: + logging.info(f'downloading from {link} to {ARGS.download_dir}') + if not ARGS.dry: + subprocess.run(['fetch-files', link], cwd=ARGS.download_dir) + for cmd in __cleanup_commands: + logging.info(f'doing cleanup: {cmd}') + if not ARGS.dry: + subprocess.run(cmd, shell=True, cwd=ARGS.download_dir) + +def __analyze_is_pattern(msg: str, patterns: list[re.Pattern]) -> bool: + return any(pat.search(msg) is not None for pat in patterns) + +def __analyze_categorize(msg: str): + for name,patterns in re_alerts_categories.items(): + if __analyze_is_pattern(msg, patterns): + return name + return 'UNKNOWN' + +def cmd_analyze(): + alerts = set() + for alert in glob.iglob(f'{ARGS.download_dir}/{ARGS.alert_glob}', recursive=True): + id = pathlib.Path(alert).parts[1] + data = json.load(open(alert)) + for d in data: + msg = d['message'] + if not __analyze_is_pattern(msg, re_alerts_irrelevant): + alerts.add((id, msg)) + + for id,msg in sorted(alerts): + cat = __analyze_categorize(msg) + if (not ARGS.verbose) and cat in ['SLOWDOWN']: + continue + logging.info(f'{cat} {id}: {msg}') + +def parse_args(): + common = { 'formatter_class': argparse.ArgumentDefaultsHelpFormatter } + parser = argparse.ArgumentParser(**common) + parser.add_argument('-v', '--verbose', action='store_true', help='be more verbose') + parser.add_argument('--dry', action='store_true', help='do not actually do anything') + + sub = parser.add_subparsers(required=True) + + sub_start = sub.add_parser('start', **common) + sub_start.add_argument('--filter', type=str, default='.*', help='regex filter for job config files') + sub_start.add_argument('--version', type=str, help='prover version of commit hash') + sub_start.add_argument('--server', type=str, help='certora server') + sub_start.add_argument('--msg', type=str, default='kat-token', help='job message') + sub_start.add_argument('--group-id', type=str, default=None, help='group id for jobs') + sub_start.add_argument('--config', type=pathlib.Path, default='.full_test.json', help='path to config file') + sub_start.add_argument('--search', type=pathlib.Path, default='certora/confs/', help='search path for job config files') + sub_start.add_argument('--links', type=pathlib.Path, default='.full_test_links.json', help='path for link file') + sub_start.add_argument('--keep-links', action='store_true', help='append links instead of replace links') + sub_start.set_defaults(func=cmd_start) + + sub_download = sub.add_parser('download', **common) + sub_download.add_argument('--links', type=pathlib.Path, default='.full_test_links.json', help='path to link file') + sub_download.add_argument('--download-dir', type=pathlib.Path, default='current-data', help='path for downloaded job info') + sub_download.set_defaults(func=cmd_download) + + sub_analyze = sub.add_parser('analyze', **common) + sub_analyze.add_argument('--download-dir', type=pathlib.Path, default='current-data', help='path to downloaded job info') + sub_analyze.add_argument('--alert-glob', type=str, default='**/alertReport.json', help='glob pattern for alert reports') + sub_analyze.set_defaults(func=cmd_analyze) + + global ARGS + ARGS = parser.parse_args() + + if ARGS.verbose: + logging.basicConfig(level = logging.DEBUG) + else: + logging.basicConfig(level = logging.INFO) + +if __name__ == '__main__': + parse_args() + ARGS.func() \ No newline at end of file From eb5154502557bdd2abc45588ca9e24da5ac53dae Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 28 Feb 2025 09:47:40 +0100 Subject: [PATCH 04/37] not needed, I guess --- certora/scripts/full-test.py | 201 ----------------------------------- 1 file changed, 201 deletions(-) delete mode 100644 certora/scripts/full-test.py diff --git a/certora/scripts/full-test.py b/certora/scripts/full-test.py deleted file mode 100644 index 59a9029..0000000 --- a/certora/scripts/full-test.py +++ /dev/null @@ -1,201 +0,0 @@ -#!/usr/bin/python3 - -import argparse -import glob -import json -import logging -import os -import pathlib -import re -import subprocess - -# matches a commit hash -re_commit = re.compile('[0-9a-f]{40}') -# matches run links -re_link = re.compile('https://.*\\.certora\\.com/output/[0-9a-zA-Z?=/]+') -# matches alerts that are irrelevant -re_alerts_irrelevant = list(map(re.compile, [ - 'will not be accessible in CVL code', - 'Summarization for internal calls .* is unused', - 'Summarization for external calls .* is unused', - 'Type .* has several conflicting declarations', - 'Conflicting types with name', - 'Syntax warning .* Passed `env` argument to an `envfree` method', -])) -# matches alerts to categories -re_alerts_categories = { - 'SLOWDOWN': list(map(re.compile, [ - 'Memory partitioning failed while analyzing contract .* longer running times', - ])), - 'MEMOUT': list(map(re.compile, [ - 'Extremely low available memory', - ])), - 'HARDTIMEOUT': list(map(re.compile, [ - 'Reached global timeout', - ])), - 'ERROR': list(map(re.compile, [ - 'An internal Prover error occurred', - ])), -} - -__cleanup_commands = [ - 'find ./ -iname "treeView" -exec rm -rf {} \\;', - 'find ./ -iname "*.tar.gz" -exec rm -rf {} \\;', - 'find ./ -iname "*.tac" -exec rm -rf {} \\;', -] - -ARGS: argparse.Namespace = None - -def __load_links(): - return json.load(open(ARGS.links)) - -def __execute(conf: pathlib.Path, msg: str, opts=[]): - cmd = ['certoraRun', str(conf), '--msg', f'{ARGS.msg} {msg}', *opts] - - if ARGS.server is not None: - cmd += ['--server', ARGS.server] - if ARGS.group_id is not None: - cmd += ['--group_id', ARGS.group_id] - if ARGS.version is not None: - if re_commit.match(ARGS.version) is None: - cmd += ['--prover_version', ARGS.version] - else: - cmd += ['--commit_sha1', ARGS.version] - - logging.debug(f'running {' '.join(cmd)}') - if ARGS.dry: - return '' - try: - out = subprocess.run(cmd, stdout=subprocess.PIPE, stderr=subprocess.STDOUT).stdout.decode() - logging.debug(out) - return out - except subprocess.CalledProcessError as e: - logging.error(e) - raise e - -def __links(out: str): - for m in re_link.finditer(out): - yield m.group(0) - -def __start_run_all(config: dict): - re_filter = re.compile(ARGS.filter) - for conf in ARGS.search.rglob('*.conf'): - if re_filter.search(str(conf)) is None: - continue - c = config.get(conf.name, None) - match c: - case None: - logging.info(f'combined for {conf.name}') - yield from __links(__execute(conf, conf.name)) - case 'skip': - logging.info(f'skipping {conf.name}') - case 'individual-rules': - logging.info(f'individually for {conf.name}') - yield from __links(__execute(conf, f'{conf.name} individually', ['--split_rules', '*'])) - case _: - logging.info(f'custom config for {conf.name}') - for name,opts in c.items(): - yield from __links(__execute(conf, f'{conf.name} {name}', opts)) - -def cmd_start(): - search = [ - ARGS.config, - pathlib.Path(__file__).parent / ARGS.config, - ] - found = False - for s in search: - if s.exists(): - logging.info(f'loading config from {s}') - config = json.load(open(s)) - found = True - break - if not found: - logging.warning(f'config file {ARGS.config} does not exist') - config = {} - - links = list(__start_run_all(config)) - if ARGS.keep_links: - links = __load_links() + links - if not ARGS.dry: - json.dump(links, open(ARGS.links, 'w'), indent=4) - -def cmd_download(): - links = __load_links() - logging.info(f'loaded {len(links)} from {ARGS.links}') - os.makedirs(ARGS.download_dir, exist_ok=True) - - for link in links: - logging.info(f'downloading from {link} to {ARGS.download_dir}') - if not ARGS.dry: - subprocess.run(['fetch-files', link], cwd=ARGS.download_dir) - for cmd in __cleanup_commands: - logging.info(f'doing cleanup: {cmd}') - if not ARGS.dry: - subprocess.run(cmd, shell=True, cwd=ARGS.download_dir) - -def __analyze_is_pattern(msg: str, patterns: list[re.Pattern]) -> bool: - return any(pat.search(msg) is not None for pat in patterns) - -def __analyze_categorize(msg: str): - for name,patterns in re_alerts_categories.items(): - if __analyze_is_pattern(msg, patterns): - return name - return 'UNKNOWN' - -def cmd_analyze(): - alerts = set() - for alert in glob.iglob(f'{ARGS.download_dir}/{ARGS.alert_glob}', recursive=True): - id = pathlib.Path(alert).parts[1] - data = json.load(open(alert)) - for d in data: - msg = d['message'] - if not __analyze_is_pattern(msg, re_alerts_irrelevant): - alerts.add((id, msg)) - - for id,msg in sorted(alerts): - cat = __analyze_categorize(msg) - if (not ARGS.verbose) and cat in ['SLOWDOWN']: - continue - logging.info(f'{cat} {id}: {msg}') - -def parse_args(): - common = { 'formatter_class': argparse.ArgumentDefaultsHelpFormatter } - parser = argparse.ArgumentParser(**common) - parser.add_argument('-v', '--verbose', action='store_true', help='be more verbose') - parser.add_argument('--dry', action='store_true', help='do not actually do anything') - - sub = parser.add_subparsers(required=True) - - sub_start = sub.add_parser('start', **common) - sub_start.add_argument('--filter', type=str, default='.*', help='regex filter for job config files') - sub_start.add_argument('--version', type=str, help='prover version of commit hash') - sub_start.add_argument('--server', type=str, help='certora server') - sub_start.add_argument('--msg', type=str, default='kat-token', help='job message') - sub_start.add_argument('--group-id', type=str, default=None, help='group id for jobs') - sub_start.add_argument('--config', type=pathlib.Path, default='.full_test.json', help='path to config file') - sub_start.add_argument('--search', type=pathlib.Path, default='certora/confs/', help='search path for job config files') - sub_start.add_argument('--links', type=pathlib.Path, default='.full_test_links.json', help='path for link file') - sub_start.add_argument('--keep-links', action='store_true', help='append links instead of replace links') - sub_start.set_defaults(func=cmd_start) - - sub_download = sub.add_parser('download', **common) - sub_download.add_argument('--links', type=pathlib.Path, default='.full_test_links.json', help='path to link file') - sub_download.add_argument('--download-dir', type=pathlib.Path, default='current-data', help='path for downloaded job info') - sub_download.set_defaults(func=cmd_download) - - sub_analyze = sub.add_parser('analyze', **common) - sub_analyze.add_argument('--download-dir', type=pathlib.Path, default='current-data', help='path to downloaded job info') - sub_analyze.add_argument('--alert-glob', type=str, default='**/alertReport.json', help='glob pattern for alert reports') - sub_analyze.set_defaults(func=cmd_analyze) - - global ARGS - ARGS = parser.parse_args() - - if ARGS.verbose: - logging.basicConfig(level = logging.DEBUG) - else: - logging.basicConfig(level = logging.INFO) - -if __name__ == '__main__': - parse_args() - ARGS.func() \ No newline at end of file From 99d983b5c8234e42dec7911da592663f1e82e412 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 28 Feb 2025 09:47:52 +0100 Subject: [PATCH 05/37] add ci --- .github/workflows/run-confs.yml | 37 +++++++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) create mode 100644 .github/workflows/run-confs.yml diff --git a/.github/workflows/run-confs.yml b/.github/workflows/run-confs.yml new file mode 100644 index 0000000..1edbf5d --- /dev/null +++ b/.github/workflows/run-confs.yml @@ -0,0 +1,37 @@ +name: test + +on: pull_request + +env: + FOUNDRY_PROFILE: ci + CONFIGS: | + certora/confs/sanity/sanity-KatToken.conf + certora/confs/sanity/sanity-MerkleMinter.conf + +jobs: + check: + runs-on: ubuntu-latest + permissions: + contents: read + statuses: write + pull-requests: write + steps: + - name: checkout repository + uses: actions/checkout@v4 + with: + submodules: recursive + + - name: install + run: | + forge soldeer install + npm i + + - name: run configs + uses: Certora/certora-run-action@v1 + with: + configurations: ${{ env.CONFIGS }} + solc-versions: 0.8.28 + solc-remove-version-prefix: "0." + certora-key: ${{ secrets.CERTORAKEY }} + env: + GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} From 6d2d59dbe004d443fab4380e82414b4894511583 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 28 Feb 2025 09:51:13 +0100 Subject: [PATCH 06/37] install foundry --- .github/workflows/run-confs.yml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/.github/workflows/run-confs.yml b/.github/workflows/run-confs.yml index 1edbf5d..055f0ae 100644 --- a/.github/workflows/run-confs.yml +++ b/.github/workflows/run-confs.yml @@ -21,7 +21,10 @@ jobs: with: submodules: recursive - - name: install + - name: install foundry + uses: foundry-rs/foundry-toolchain@v1 + + - name: install dependencies run: | forge soldeer install npm i From e49c806d8105f1fa2d9f4160f3b4d169986da487 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 28 Feb 2025 10:47:43 +0100 Subject: [PATCH 07/37] Add some simple rules, move files around --- .github/workflows/run-confs.yml | 6 ++-- certora/confs/KatToken-simple.conf | 27 ++++++++++++++++ certora/confs/MerkleMinter-simple.conf | 31 +++++++++++++++++++ .../confs/{sanity => }/sanity-KatToken.conf | 0 .../{sanity => }/sanity-MerkleMinter.conf | 0 certora/specs/KatToken-simple.spec | 28 +++++++++++++++++ certora/specs/MerkleMinter-simple.spec | 27 ++++++++++++++++ 7 files changed, 117 insertions(+), 2 deletions(-) create mode 100644 certora/confs/KatToken-simple.conf create mode 100644 certora/confs/MerkleMinter-simple.conf rename certora/confs/{sanity => }/sanity-KatToken.conf (100%) rename certora/confs/{sanity => }/sanity-MerkleMinter.conf (100%) create mode 100644 certora/specs/KatToken-simple.spec create mode 100644 certora/specs/MerkleMinter-simple.spec diff --git a/.github/workflows/run-confs.yml b/.github/workflows/run-confs.yml index 055f0ae..978a8bc 100644 --- a/.github/workflows/run-confs.yml +++ b/.github/workflows/run-confs.yml @@ -5,8 +5,10 @@ on: pull_request env: FOUNDRY_PROFILE: ci CONFIGS: | - certora/confs/sanity/sanity-KatToken.conf - certora/confs/sanity/sanity-MerkleMinter.conf + certora/confs/KatToken-simple.conf + certora/confs/MerkleMinter-simple.conf + certora/confs/sanity-KatToken.conf + certora/confs/sanity-MerkleMinter.conf jobs: check: diff --git a/certora/confs/KatToken-simple.conf b/certora/confs/KatToken-simple.conf new file mode 100644 index 0000000..f55af84 --- /dev/null +++ b/certora/confs/KatToken-simple.conf @@ -0,0 +1,27 @@ +{ + "assert_autofinder_success": true, + "files": [ + "src/KatToken.sol" + ], + "global_timeout": "7200", + "loop_iter": "2", + "optimistic_loop": true, + "msg": "KatToken simple", + "packages": [ + "@openzeppelin/merkle-tree=node_modules/@openzeppelin/merkle-tree", + "@openzeppelin-contracts-5.1.0=dependencies/@openzeppelin-contracts-5.1.0", + "forge-std-1.9.4=dependencies/forge-std-1.9.4" + ], + "process": "emv", + "prover_args": [ + "-verifyCache", + "-verifyTACDumps", + "-testMode", + "-checkRuleDigest", + "-callTraceHardFail on" + ], + "server": "production", + "solc": "solc8.28", + "solc_via_ir": false, + "verify": "KatToken:certora/specs/KatToken-simple.spec" +} \ No newline at end of file diff --git a/certora/confs/MerkleMinter-simple.conf b/certora/confs/MerkleMinter-simple.conf new file mode 100644 index 0000000..4be446b --- /dev/null +++ b/certora/confs/MerkleMinter-simple.conf @@ -0,0 +1,31 @@ +{ + "assert_autofinder_success": true, + "files": [ + "src/MerkleMinter.sol", + "src/KatToken.sol" + ], + "global_timeout": "7200", + "loop_iter": "2", + "optimistic_loop": true, + "link": [ + "MerkleMinter:katToken=KatToken" + ], + "msg": "MerkleMinter simple", + "packages": [ + "@openzeppelin/merkle-tree=node_modules/@openzeppelin/merkle-tree", + "@openzeppelin-contracts-5.1.0=dependencies/@openzeppelin-contracts-5.1.0", + "forge-std-1.9.4=dependencies/forge-std-1.9.4" + ], + "process": "emv", + "prover_args": [ + "-verifyCache", + "-verifyTACDumps", + "-testMode", + "-checkRuleDigest", + "-callTraceHardFail on" + ], + "server": "production", + "solc": "solc8.28", + "solc_via_ir": false, + "verify": "MerkleMinter:certora/specs/MerkleMinter-simple.spec" +} \ No newline at end of file diff --git a/certora/confs/sanity/sanity-KatToken.conf b/certora/confs/sanity-KatToken.conf similarity index 100% rename from certora/confs/sanity/sanity-KatToken.conf rename to certora/confs/sanity-KatToken.conf diff --git a/certora/confs/sanity/sanity-MerkleMinter.conf b/certora/confs/sanity-MerkleMinter.conf similarity index 100% rename from certora/confs/sanity/sanity-MerkleMinter.conf rename to certora/confs/sanity-MerkleMinter.conf diff --git a/certora/specs/KatToken-simple.spec b/certora/specs/KatToken-simple.spec new file mode 100644 index 0000000..6582288 --- /dev/null +++ b/certora/specs/KatToken-simple.spec @@ -0,0 +1,28 @@ +rule onlyAdminCanChangeAdmin() { + env e; + address oldOwner = inflationAdmin(e); + address newOwner; + + changeInflationAdmin(e, newOwner); + + assert(e.msg.sender == oldOwner); + assert(inflationAdmin(e) == newOwner); +} + +rule canOnlySendAvailableMintCapacity() { + env e; + address to; + uint256 amount; + + uint256 ownCapacityBefore = mintCapacity(e, e.msg.sender); + uint256 toCapacityBefore = mintCapacity(e, to); + + distributeMintCapacity(e, to, amount); + + + uint256 ownCapacityAfter = mintCapacity(e, e.msg.sender); + uint256 toCapacityAfter = mintCapacity(e, to); + + assert(ownCapacityBefore >= amount); + assert(ownCapacityBefore + toCapacityBefore == ownCapacityAfter + toCapacityAfter); +} diff --git a/certora/specs/MerkleMinter-simple.spec b/certora/specs/MerkleMinter-simple.spec new file mode 100644 index 0000000..2357e2d --- /dev/null +++ b/certora/specs/MerkleMinter-simple.spec @@ -0,0 +1,27 @@ +rule onlyRootCanInit() { + env e; + bytes32 _root; + address _katToken; + + address rootBefore = rootSetter(); + + init(e, _root, _katToken); + + assert(e.msg.sender == rootBefore); + assert(root() == _root); + assert(rootSetter() == 0); + assert(katToken() == _katToken); +} + +rule canOnlyClaimWhenNotLocked() { + env e; + + bytes32[] proof; + uint256 amount; + address receiver; + + claimKatToken(e, proof, amount, receiver); + + assert(e.block.timestamp >= unlockTime()); + assert(!locked()); +} \ No newline at end of file From 311b94c0f3f9964731d10c1bb83078e181e5c940 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 28 Feb 2025 10:59:19 +0100 Subject: [PATCH 08/37] remove debug arguments --- certora/confs/KatToken-simple.conf | 7 ------- certora/confs/MerkleMinter-simple.conf | 7 ------- 2 files changed, 14 deletions(-) diff --git a/certora/confs/KatToken-simple.conf b/certora/confs/KatToken-simple.conf index f55af84..b7cd399 100644 --- a/certora/confs/KatToken-simple.conf +++ b/certora/confs/KatToken-simple.conf @@ -13,13 +13,6 @@ "forge-std-1.9.4=dependencies/forge-std-1.9.4" ], "process": "emv", - "prover_args": [ - "-verifyCache", - "-verifyTACDumps", - "-testMode", - "-checkRuleDigest", - "-callTraceHardFail on" - ], "server": "production", "solc": "solc8.28", "solc_via_ir": false, diff --git a/certora/confs/MerkleMinter-simple.conf b/certora/confs/MerkleMinter-simple.conf index 4be446b..f6d8304 100644 --- a/certora/confs/MerkleMinter-simple.conf +++ b/certora/confs/MerkleMinter-simple.conf @@ -17,13 +17,6 @@ "forge-std-1.9.4=dependencies/forge-std-1.9.4" ], "process": "emv", - "prover_args": [ - "-verifyCache", - "-verifyTACDumps", - "-testMode", - "-checkRuleDigest", - "-callTraceHardFail on" - ], "server": "production", "solc": "solc8.28", "solc_via_ir": false, From 6ea113ae978942e92eb03b6f7a5b7eba3e2b60c3 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 28 Feb 2025 10:59:29 +0100 Subject: [PATCH 09/37] fix test specs --- certora/specs/MerkleMinter-simple.spec | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/certora/specs/MerkleMinter-simple.spec b/certora/specs/MerkleMinter-simple.spec index 2357e2d..9e58d6d 100644 --- a/certora/specs/MerkleMinter-simple.spec +++ b/certora/specs/MerkleMinter-simple.spec @@ -1,3 +1,11 @@ +methods { + function root() external returns (bytes32) envfree; + function rootSetter() external returns (address) envfree; + function katToken() external returns (address) envfree; + function unlockTime() external returns (uint256) envfree; + function locked() external returns (bool) envfree; +} + rule onlyRootCanInit() { env e; bytes32 _root; @@ -22,6 +30,5 @@ rule canOnlyClaimWhenNotLocked() { claimKatToken(e, proof, amount, receiver); - assert(e.block.timestamp >= unlockTime()); - assert(!locked()); + assert(e.block.timestamp > unlockTime() || !locked()); } \ No newline at end of file From e74854d199a861ebc50a9fef39df445a17a4adcf Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 28 Feb 2025 14:11:35 +0100 Subject: [PATCH 10/37] add a summary + sanity checks for exp2 --- certora/confs/exp2-summary.conf | 20 ++++++++++++++++++++ certora/harnesses/PowUtilHarness.sol | 10 ++++++++++ certora/specs/exp2-check.spec | 20 ++++++++++++++++++++ certora/specs/exp2-summary.spec | 22 ++++++++++++++++++++++ 4 files changed, 72 insertions(+) create mode 100644 certora/confs/exp2-summary.conf create mode 100644 certora/harnesses/PowUtilHarness.sol create mode 100644 certora/specs/exp2-check.spec create mode 100644 certora/specs/exp2-summary.spec diff --git a/certora/confs/exp2-summary.conf b/certora/confs/exp2-summary.conf new file mode 100644 index 0000000..2f6ee19 --- /dev/null +++ b/certora/confs/exp2-summary.conf @@ -0,0 +1,20 @@ +{ + "assert_autofinder_success": true, + "files": [ + "certora/harnesses/PowUtilHarness.sol" + ], + "global_timeout": "7200", + "loop_iter": "2", + "optimistic_loop": true, + "msg": "PowUtilHarness simple", + "packages": [ + "@openzeppelin/merkle-tree=node_modules/@openzeppelin/merkle-tree", + "@openzeppelin-contracts-5.1.0=dependencies/@openzeppelin-contracts-5.1.0", + "forge-std-1.9.4=dependencies/forge-std-1.9.4" + ], + "process": "emv", + //"server": "production", + "solc": "solc8.28", + "solc_via_ir": false, + "verify": "PowUtilHarness:certora/specs/exp2-check.spec" +} \ No newline at end of file diff --git a/certora/harnesses/PowUtilHarness.sol b/certora/harnesses/PowUtilHarness.sol new file mode 100644 index 0000000..2963f09 --- /dev/null +++ b/certora/harnesses/PowUtilHarness.sol @@ -0,0 +1,10 @@ +//SPDX-License-Identifier: MIT +pragma solidity 0.8.28; + +import {PowUtil} from "../../src/Powutil.sol"; + +contract PowUtilHarness { + function exp2(uint256 x) public pure returns (uint256 result) { + return PowUtil.exp2(x); + } +} \ No newline at end of file diff --git a/certora/specs/exp2-check.spec b/certora/specs/exp2-check.spec new file mode 100644 index 0000000..49dee41 --- /dev/null +++ b/certora/specs/exp2-check.spec @@ -0,0 +1,20 @@ +import "./exp2-summary.spec"; + +methods { + function exp2(uint256 x) external returns (uint256) envfree; +} + +function almost_equal(mathint x, mathint res) { + uint256 e = exp2(assert_uint256(x)); + satisfy(99 * e < 100 * res && 101 * e > 100 * res); +} + +rule exp2GhostMakesSense() { + almost_equal(0*ONE18(), ONE18()); + almost_equal(1*ONE18(), 2*ONE18()); + almost_equal(2*ONE18(), 4*ONE18()); + almost_equal(3*ONE18(), 8*ONE18()); + almost_equal(4*ONE18(), 16*ONE18()); + almost_equal(5*ONE18(), 32*ONE18()); + almost_equal(6*ONE18(), 64*ONE18()); +} diff --git a/certora/specs/exp2-summary.spec b/certora/specs/exp2-summary.spec new file mode 100644 index 0000000..c46e30c --- /dev/null +++ b/certora/specs/exp2-summary.spec @@ -0,0 +1,22 @@ +methods { + function PowUtil.exp2(uint256 x) internal returns (uint256) => cvlExp2(x); + +} + +definition ONE18() returns uint256 = 1000000000000000000; +definition TWO18() returns uint256 = 2000000000000000000; +ghost ghostExp2(uint256) returns uint256 { + axiom ghostExp2(0) == ONE18(); + axiom ghostExp2(ONE18()) == TWO18(); + + axiom forall uint256 y1. forall uint256 y2. + y1 > y2 => ghostExp2(y1) >= ghostExp2(y2); + axiom forall uint256 y. + y > ONE18() => ghostExp2(y) >= TWO18(); + axiom forall uint256 y. + y <= ONE18() => ghostExp2(y) <= TWO18(); +} + +function cvlExp2(uint256 x) returns uint256 { + return ghostExp2(x); +} From 1fe6685f816b107e92b192c7bcb671c67d348205 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 28 Feb 2025 14:21:15 +0100 Subject: [PATCH 11/37] more checks --- certora/specs/exp2-check.spec | 25 ++++++++++++++++--------- 1 file changed, 16 insertions(+), 9 deletions(-) diff --git a/certora/specs/exp2-check.spec b/certora/specs/exp2-check.spec index 49dee41..be1ff33 100644 --- a/certora/specs/exp2-check.spec +++ b/certora/specs/exp2-check.spec @@ -4,17 +4,24 @@ methods { function exp2(uint256 x) external returns (uint256) envfree; } -function almost_equal(mathint x, mathint res) { +function maybeEqual(mathint x, mathint res) { uint256 e = exp2(assert_uint256(x)); satisfy(99 * e < 100 * res && 101 * e > 100 * res); } -rule exp2GhostMakesSense() { - almost_equal(0*ONE18(), ONE18()); - almost_equal(1*ONE18(), 2*ONE18()); - almost_equal(2*ONE18(), 4*ONE18()); - almost_equal(3*ONE18(), 8*ONE18()); - almost_equal(4*ONE18(), 16*ONE18()); - almost_equal(5*ONE18(), 32*ONE18()); - almost_equal(6*ONE18(), 64*ONE18()); +rule exp2Consts() { + maybeEqual(0*ONE18(), ONE18()); + maybeEqual(1*ONE18(), 2*ONE18()); + maybeEqual(2*ONE18(), 4*ONE18()); + maybeEqual(3*ONE18(), 8*ONE18()); + maybeEqual(4*ONE18(), 16*ONE18()); + maybeEqual(5*ONE18(), 32*ONE18()); + maybeEqual(6*ONE18(), 64*ONE18()); +} + +rule exp2Monotonicity() { + uint256 x; + uint256 y; + // weak monotonicity + assert((x < y) => (exp2(x) <= exp2(y))); } From 0989b2d34bfa4bb5715409af5b60b3cc30b9faaf Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 28 Feb 2025 14:21:47 +0100 Subject: [PATCH 12/37] work on sample rules --- certora/specs/KatToken-simple.spec | 38 +++++++++++++++++++++++++----- 1 file changed, 32 insertions(+), 6 deletions(-) diff --git a/certora/specs/KatToken-simple.spec b/certora/specs/KatToken-simple.spec index 6582288..16f9ea9 100644 --- a/certora/specs/KatToken-simple.spec +++ b/certora/specs/KatToken-simple.spec @@ -1,12 +1,23 @@ +import "./exp2-summary.spec"; + +methods { + function inflationAdmin() external returns (address) envfree; + function inflationBeneficiary() external returns (address) envfree; + function inflationFactor() external returns (uint256) envfree; + function MAX_INFLATION() external returns (uint256) envfree; + function merkleMinter() external returns (address) envfree; + function mintCapacity(address) external returns (uint256) envfree; +} + rule onlyAdminCanChangeAdmin() { env e; - address oldOwner = inflationAdmin(e); + address oldOwner = inflationAdmin(); address newOwner; changeInflationAdmin(e, newOwner); assert(e.msg.sender == oldOwner); - assert(inflationAdmin(e) == newOwner); + assert(inflationAdmin() == newOwner); } rule canOnlySendAvailableMintCapacity() { @@ -14,15 +25,30 @@ rule canOnlySendAvailableMintCapacity() { address to; uint256 amount; - uint256 ownCapacityBefore = mintCapacity(e, e.msg.sender); - uint256 toCapacityBefore = mintCapacity(e, to); + uint256 ownCapacityBefore = mintCapacity(e.msg.sender); + uint256 toCapacityBefore = mintCapacity(to); distributeMintCapacity(e, to, amount); - uint256 ownCapacityAfter = mintCapacity(e, e.msg.sender); - uint256 toCapacityAfter = mintCapacity(e, to); + uint256 ownCapacityAfter = mintCapacity(e.msg.sender); + uint256 toCapacityAfter = mintCapacity(to); assert(ownCapacityBefore >= amount); assert(ownCapacityBefore + toCapacityBefore == ownCapacityAfter + toCapacityAfter); } + +rule nonTrivialDistributeInflation() { + env e; + + // enforce non-trivial inflation + require(inflationFactor() > MAX_INFLATION() / 2); + require(inflationFactor() < MAX_INFLATION()); + + uint256 capacityBefore = mintCapacity(inflationBeneficiary()); + + distributeInflation(e); + + uint256 capacityAfter = mintCapacity(inflationBeneficiary()); + satisfy(capacityAfter > capacityBefore); +} \ No newline at end of file From e53043af4385a66ecc12bfd7fe0bcec887d4437b Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 28 Feb 2025 14:44:22 +0100 Subject: [PATCH 13/37] some comments --- certora/confs/{exp2-summary.conf => exp2-check-summary.conf} | 4 ++-- certora/harnesses/PowUtilHarness.sol | 1 + certora/specs/exp2-check.spec | 2 ++ certora/specs/exp2-summary.spec | 3 ++- 4 files changed, 7 insertions(+), 3 deletions(-) rename certora/confs/{exp2-summary.conf => exp2-check-summary.conf} (89%) diff --git a/certora/confs/exp2-summary.conf b/certora/confs/exp2-check-summary.conf similarity index 89% rename from certora/confs/exp2-summary.conf rename to certora/confs/exp2-check-summary.conf index 2f6ee19..5df491c 100644 --- a/certora/confs/exp2-summary.conf +++ b/certora/confs/exp2-check-summary.conf @@ -6,14 +6,14 @@ "global_timeout": "7200", "loop_iter": "2", "optimistic_loop": true, - "msg": "PowUtilHarness simple", + "msg": "Check exp2 summary", "packages": [ "@openzeppelin/merkle-tree=node_modules/@openzeppelin/merkle-tree", "@openzeppelin-contracts-5.1.0=dependencies/@openzeppelin-contracts-5.1.0", "forge-std-1.9.4=dependencies/forge-std-1.9.4" ], "process": "emv", - //"server": "production", + "server": "production", "solc": "solc8.28", "solc_via_ir": false, "verify": "PowUtilHarness:certora/specs/exp2-check.spec" diff --git a/certora/harnesses/PowUtilHarness.sol b/certora/harnesses/PowUtilHarness.sol index 2963f09..c832943 100644 --- a/certora/harnesses/PowUtilHarness.sol +++ b/certora/harnesses/PowUtilHarness.sol @@ -3,6 +3,7 @@ pragma solidity 0.8.28; import {PowUtil} from "../../src/Powutil.sol"; +// Makes it easier to access `PowUtil.exp2`. contract PowUtilHarness { function exp2(uint256 x) public pure returns (uint256 result) { return PowUtil.exp2(x); diff --git a/certora/specs/exp2-check.spec b/certora/specs/exp2-check.spec index be1ff33..a2a6055 100644 --- a/certora/specs/exp2-check.spec +++ b/certora/specs/exp2-check.spec @@ -1,5 +1,7 @@ import "./exp2-summary.spec"; +// Does some sanity checks on the exp2 summarization. + methods { function exp2(uint256 x) external returns (uint256) envfree; } diff --git a/certora/specs/exp2-summary.spec b/certora/specs/exp2-summary.spec index c46e30c..8c38bd0 100644 --- a/certora/specs/exp2-summary.spec +++ b/certora/specs/exp2-summary.spec @@ -1,6 +1,7 @@ +// Provides a summary for PowUtil.exp2 based on a ghost with some axioms. + methods { function PowUtil.exp2(uint256 x) internal returns (uint256) => cvlExp2(x); - } definition ONE18() returns uint256 = 1000000000000000000; From 4ebf1d0d45f586acd36fa7d188050036fda76021 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 28 Feb 2025 14:44:44 +0100 Subject: [PATCH 14/37] run exp2 summary checks in ci --- .github/workflows/run-confs.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/run-confs.yml b/.github/workflows/run-confs.yml index 978a8bc..7ff2acd 100644 --- a/.github/workflows/run-confs.yml +++ b/.github/workflows/run-confs.yml @@ -5,6 +5,7 @@ on: pull_request env: FOUNDRY_PROFILE: ci CONFIGS: | + certora/confs/exp2-check-summary.conf certora/confs/KatToken-simple.conf certora/confs/MerkleMinter-simple.conf certora/confs/sanity-KatToken.conf From a98ef8d25880fe5f407b0c37e8c5a46b1cd16df4 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 28 Feb 2025 16:05:45 +0100 Subject: [PATCH 15/37] better axioms --- certora/specs/exp2-check.spec | 19 +++++++++++++ certora/specs/exp2-summary.spec | 48 +++++++++++++++++++++++++-------- 2 files changed, 56 insertions(+), 11 deletions(-) diff --git a/certora/specs/exp2-check.spec b/certora/specs/exp2-check.spec index a2a6055..75d9210 100644 --- a/certora/specs/exp2-check.spec +++ b/certora/specs/exp2-check.spec @@ -27,3 +27,22 @@ rule exp2Monotonicity() { // weak monotonicity assert((x < y) => (exp2(x) <= exp2(y))); } + +function lowerBound(mathint x, mathint res) { + mathint e = exp2(assert_uint256(x)); + assert(10 * e >= 9*res); +} + +rule exp2LowerBound() { + lowerBound(0*ONE18(), ONE18()); + lowerBound(1*ONE18(), 2*ONE18()); + lowerBound(2*ONE18(), 4*ONE18()); + lowerBound(3*ONE18(), 8*ONE18()); + lowerBound(4*ONE18(), 16*ONE18()); + lowerBound(5*ONE18(), 32*ONE18()); + lowerBound(6*ONE18(), 64*ONE18()); + lowerBound(7*ONE18(), 128*ONE18()); + lowerBound(8*ONE18(), 256*ONE18()); + lowerBound(9*ONE18(), 512*ONE18()); + lowerBound(10*ONE18(), 1024*ONE18()); +} diff --git a/certora/specs/exp2-summary.spec b/certora/specs/exp2-summary.spec index 8c38bd0..a661c5f 100644 --- a/certora/specs/exp2-summary.spec +++ b/certora/specs/exp2-summary.spec @@ -4,18 +4,44 @@ methods { function PowUtil.exp2(uint256 x) internal returns (uint256) => cvlExp2(x); } -definition ONE18() returns uint256 = 1000000000000000000; -definition TWO18() returns uint256 = 2000000000000000000; -ghost ghostExp2(uint256) returns uint256 { +definition ONE18() returns uint256 = 1000000000000000000; +definition Log2() returns uint256 = 693147180559945309; + +definition to18(uint256 x) returns mathint = x * ONE18(); +definition taylor2xAt(uint256 min, uint256 max, uint256 mult) returns bool = + forall uint256 x. (x >= min && x < max) => ( + ghostExp2(x) >= + to18(mult) + + mult*(x-to18(min)) * Log2() / ONE18() + + mult*(x-to18(min))*(x-to18(min)) * Log2()*Log2() / ONE18()/ONE18()/ONE18() / 2 + + mult*(x-to18(min))*(x-to18(min))*(x-to18(min)) * Log2()*Log2()*Log2() /ONE18()/ONE18()/ONE18()/ONE18()/ONE18() / 6 + ); + +ghost ghostExp2(mathint) returns uint256 { axiom ghostExp2(0) == ONE18(); - axiom ghostExp2(ONE18()) == TWO18(); - - axiom forall uint256 y1. forall uint256 y2. - y1 > y2 => ghostExp2(y1) >= ghostExp2(y2); - axiom forall uint256 y. - y > ONE18() => ghostExp2(y) >= TWO18(); - axiom forall uint256 y. - y <= ONE18() => ghostExp2(y) <= TWO18(); + axiom ghostExp2(ONE18()) == 2*ONE18(); + + axiom forall uint256 x1. forall uint256 x2. + x1 > x2 => ghostExp2(x1) >= ghostExp2(x2); + axiom forall uint256 x. + x > ONE18() => ghostExp2(x) >= 2*ONE18(); + axiom forall uint256 x. + x <= ONE18() => ghostExp2(x) <= 2*ONE18(); + + axiom forall uint256 x. + ((x >= 0 && x < 2*ONE18()) => ( + ghostExp2(x) >= + ONE18() + + x * Log2() / ONE18() + + x*x * Log2()*Log2() / ONE18()/ONE18()/ONE18() / 2 + + x*x*x * Log2()*Log2()*Log2() /ONE18()/ONE18()/ONE18()/ONE18()/ONE18() / 6 + )) && + ((x >= 2*ONE18() && x < 4*ONE18()) => (ghostExp2(x) >= ghostExp2(x - 2*ONE18()) * 4)) && + ((x >= 4*ONE18() && x < 6*ONE18()) => (ghostExp2(x) >= ghostExp2(x - 4*ONE18()) * 16)) && + ((x >= 6*ONE18() && x < 8*ONE18()) => (ghostExp2(x) >= ghostExp2(x - 6*ONE18()) * 64)) && + ((x >= 8*ONE18()) => (ghostExp2(x) >= ghostExp2(x - 8*ONE18()) * 256)) + ; + } function cvlExp2(uint256 x) returns uint256 { From f84da80f839434a16feedd1a0826865d1c35b31b Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 28 Feb 2025 16:17:15 +0100 Subject: [PATCH 16/37] also some non-integers --- certora/specs/exp2-check.spec | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/certora/specs/exp2-check.spec b/certora/specs/exp2-check.spec index 75d9210..ec3fcf1 100644 --- a/certora/specs/exp2-check.spec +++ b/certora/specs/exp2-check.spec @@ -45,4 +45,15 @@ rule exp2LowerBound() { lowerBound(8*ONE18(), 256*ONE18()); lowerBound(9*ONE18(), 512*ONE18()); lowerBound(10*ONE18(), 1024*ONE18()); + + lowerBound(1*ONE18()/2, ONE18()* 14142 / 10000); + lowerBound(3*ONE18()/2, ONE18()* 28284 / 10000); + lowerBound(5*ONE18()/2, ONE18()* 56569 / 10000); + lowerBound(7*ONE18()/2, ONE18()* 113137 / 10000); + lowerBound(9*ONE18()/2, ONE18()* 226274 / 10000); + lowerBound(11*ONE18()/2, ONE18()* 452548 / 10000); + lowerBound(13*ONE18()/2, ONE18()* 905097 / 10000); + lowerBound(15*ONE18()/2, ONE18()* 1810193 / 10000); + lowerBound(17*ONE18()/2, ONE18()* 3620387 / 10000); + lowerBound(19*ONE18()/2, ONE18()* 7240773 / 10000); } From e8ccaca66352f6cae7491992b7c3cdc821c0b554 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Tue, 4 Mar 2025 09:22:11 +0100 Subject: [PATCH 17/37] add upper bounds --- certora/specs/exp2-check.spec | 30 ++++++++++++++++++++++++++++++ certora/specs/exp2-summary.spec | 15 +++++++++++++++ 2 files changed, 45 insertions(+) diff --git a/certora/specs/exp2-check.spec b/certora/specs/exp2-check.spec index ec3fcf1..43ad219 100644 --- a/certora/specs/exp2-check.spec +++ b/certora/specs/exp2-check.spec @@ -57,3 +57,33 @@ rule exp2LowerBound() { lowerBound(17*ONE18()/2, ONE18()* 3620387 / 10000); lowerBound(19*ONE18()/2, ONE18()* 7240773 / 10000); } + +function upperBound(mathint x, mathint res) { + mathint e = exp2(assert_uint256(x)); + assert(4 * e <= 5*res); +} + +rule exp2UpperBound() { + upperBound(0*ONE18(), ONE18()); + upperBound(1*ONE18(), 2*ONE18()); + upperBound(2*ONE18(), 4*ONE18()); + upperBound(3*ONE18(), 8*ONE18()); + upperBound(4*ONE18(), 16*ONE18()); + upperBound(5*ONE18(), 32*ONE18()); + upperBound(6*ONE18(), 64*ONE18()); + upperBound(7*ONE18(), 128*ONE18()); + upperBound(8*ONE18(), 256*ONE18()); + upperBound(9*ONE18(), 512*ONE18()); + upperBound(10*ONE18(), 1024*ONE18()); + + upperBound(1*ONE18()/2, ONE18()* 14142 / 10000); + upperBound(3*ONE18()/2, ONE18()* 28284 / 10000); + upperBound(5*ONE18()/2, ONE18()* 56569 / 10000); + upperBound(7*ONE18()/2, ONE18()* 113137 / 10000); + upperBound(9*ONE18()/2, ONE18()* 226274 / 10000); + upperBound(11*ONE18()/2, ONE18()* 452548 / 10000); + upperBound(13*ONE18()/2, ONE18()* 905097 / 10000); + upperBound(15*ONE18()/2, ONE18()* 1810193 / 10000); + upperBound(17*ONE18()/2, ONE18()* 3620387 / 10000); + upperBound(19*ONE18()/2, ONE18()* 7240773 / 10000); +} diff --git a/certora/specs/exp2-summary.spec b/certora/specs/exp2-summary.spec index a661c5f..394c68e 100644 --- a/certora/specs/exp2-summary.spec +++ b/certora/specs/exp2-summary.spec @@ -28,6 +28,7 @@ ghost ghostExp2(mathint) returns uint256 { axiom forall uint256 x. x <= ONE18() => ghostExp2(x) <= 2*ONE18(); + // lower bound axiom forall uint256 x. ((x >= 0 && x < 2*ONE18()) => ( ghostExp2(x) >= @@ -42,6 +43,20 @@ ghost ghostExp2(mathint) returns uint256 { ((x >= 8*ONE18()) => (ghostExp2(x) >= ghostExp2(x - 8*ONE18()) * 256)) ; + // upper bound + axiom forall uint256 x. + ((x >= 0 && x < 2*ONE18()) => ( + ghostExp2(x) <= + 4*ONE18()/3 // rough estimate: this approximation at 2 is about 0.21 to low + + x * Log2() / ONE18() + + x*x * Log2()*Log2() / ONE18()/ONE18()/ONE18() / 2 + + x*x*x * Log2()*Log2()*Log2() /ONE18()/ONE18()/ONE18()/ONE18()/ONE18() / 6 + )) && + ((x >= 2*ONE18() && x < 4*ONE18()) => (ghostExp2(x) <= ghostExp2(x - 2*ONE18()) * 4)) && + ((x >= 4*ONE18() && x < 6*ONE18()) => (ghostExp2(x) <= ghostExp2(x - 4*ONE18()) * 16)) && + ((x >= 6*ONE18() && x < 8*ONE18()) => (ghostExp2(x) <= ghostExp2(x - 6*ONE18()) * 64)) && + ((x >= 8*ONE18()) => (ghostExp2(x) <= ghostExp2(x - 8*ONE18()) * 256)) + ; } function cvlExp2(uint256 x) returns uint256 { From d1e7c12ba70e322f130c36cc6a4180587c592de5 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 5 Mar 2025 10:36:47 +0100 Subject: [PATCH 18/37] Add some stuff to .gitignore --- .gitignore | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/.gitignore b/.gitignore index 2e06fbc..2acac2c 100644 --- a/.gitignore +++ b/.gitignore @@ -14,4 +14,9 @@ docs/ .env dependencies/ -node_modules/ \ No newline at end of file +node_modules/ + +# Certora files +.certora_internal/ +.venv/ +emv-*-certora-* \ No newline at end of file From a1b0d8357e53a6090c3991d23daae8dcdc54832c Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 5 Mar 2025 10:37:12 +0100 Subject: [PATCH 19/37] some cleanup --- certora/specs/exp2-summary.spec | 10 ---------- 1 file changed, 10 deletions(-) diff --git a/certora/specs/exp2-summary.spec b/certora/specs/exp2-summary.spec index 394c68e..b00e8b4 100644 --- a/certora/specs/exp2-summary.spec +++ b/certora/specs/exp2-summary.spec @@ -7,16 +7,6 @@ methods { definition ONE18() returns uint256 = 1000000000000000000; definition Log2() returns uint256 = 693147180559945309; -definition to18(uint256 x) returns mathint = x * ONE18(); -definition taylor2xAt(uint256 min, uint256 max, uint256 mult) returns bool = - forall uint256 x. (x >= min && x < max) => ( - ghostExp2(x) >= - to18(mult) - + mult*(x-to18(min)) * Log2() / ONE18() - + mult*(x-to18(min))*(x-to18(min)) * Log2()*Log2() / ONE18()/ONE18()/ONE18() / 2 - + mult*(x-to18(min))*(x-to18(min))*(x-to18(min)) * Log2()*Log2()*Log2() /ONE18()/ONE18()/ONE18()/ONE18()/ONE18() / 6 - ); - ghost ghostExp2(mathint) returns uint256 { axiom ghostExp2(0) == ONE18(); axiom ghostExp2(ONE18()) == 2*ONE18(); From dea363fb6531c71896b76ef975d42ed4c3762bf2 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 5 Mar 2025 10:43:58 +0100 Subject: [PATCH 20/37] add comment for taylor bounds --- certora/specs/exp2-summary.spec | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/certora/specs/exp2-summary.spec b/certora/specs/exp2-summary.spec index b00e8b4..56ff60e 100644 --- a/certora/specs/exp2-summary.spec +++ b/certora/specs/exp2-summary.spec @@ -1,4 +1,15 @@ -// Provides a summary for PowUtil.exp2 based on a ghost with some axioms. +// Provides a summary for PowUtil.exp2. +// The summary refers to a ghost `ghostExp2` that is restricted by a number of +// simple axioms: +// - exp2(0) == 1 +// - exp2(1) == 2 +// - exp2(x) is monotonically increasing +// - for x>=1, exp2(x) >= 2 +// - for x<=1, exp2(x) <= 2 +// Furthermore, we add axioms based on 3rd-order taylor expansions. We spell out +// the expansion around zero for 0<=x<2 and shift it for higher values of x. +// Similarly, we implement an upper bound by moving the expansion around zero +// to start at x=0, y=4/3. methods { function PowUtil.exp2(uint256 x) internal returns (uint256) => cvlExp2(x); @@ -14,7 +25,7 @@ ghost ghostExp2(mathint) returns uint256 { axiom forall uint256 x1. forall uint256 x2. x1 > x2 => ghostExp2(x1) >= ghostExp2(x2); axiom forall uint256 x. - x > ONE18() => ghostExp2(x) >= 2*ONE18(); + x >= ONE18() => ghostExp2(x) >= 2*ONE18(); axiom forall uint256 x. x <= ONE18() => ghostExp2(x) <= 2*ONE18(); From f724dd1740969081620c78b285d4732401771fe8 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 6 Mar 2025 15:24:30 +0100 Subject: [PATCH 21/37] split exp2 to separate spec --- .github/workflows/run-confs.yml | 1 + certora/confs/KatToken-exp2.conf | 20 ++++++++++++++++++++ certora/specs/KatToken-exp2.spec | 25 +++++++++++++++++++++++++ certora/specs/KatToken-simple.spec | 17 ----------------- 4 files changed, 46 insertions(+), 17 deletions(-) create mode 100644 certora/confs/KatToken-exp2.conf create mode 100644 certora/specs/KatToken-exp2.spec diff --git a/.github/workflows/run-confs.yml b/.github/workflows/run-confs.yml index 7ff2acd..c5fc7c9 100644 --- a/.github/workflows/run-confs.yml +++ b/.github/workflows/run-confs.yml @@ -6,6 +6,7 @@ env: FOUNDRY_PROFILE: ci CONFIGS: | certora/confs/exp2-check-summary.conf + certora/confs/KatToken-exp2.conf certora/confs/KatToken-simple.conf certora/confs/MerkleMinter-simple.conf certora/confs/sanity-KatToken.conf diff --git a/certora/confs/KatToken-exp2.conf b/certora/confs/KatToken-exp2.conf new file mode 100644 index 0000000..7500b6d --- /dev/null +++ b/certora/confs/KatToken-exp2.conf @@ -0,0 +1,20 @@ +{ + "assert_autofinder_success": true, + "files": [ + "src/KatToken.sol" + ], + "global_timeout": "7200", + "loop_iter": "2", + "optimistic_loop": true, + "msg": "KatToken simple", + "packages": [ + "@openzeppelin/merkle-tree=node_modules/@openzeppelin/merkle-tree", + "@openzeppelin-contracts-5.1.0=dependencies/@openzeppelin-contracts-5.1.0", + "forge-std-1.9.4=dependencies/forge-std-1.9.4" + ], + "process": "emv", + "server": "production", + "solc": "solc8.28", + "solc_via_ir": false, + "verify": "KatToken:certora/specs/KatToken-exp2.spec" +} \ No newline at end of file diff --git a/certora/specs/KatToken-exp2.spec b/certora/specs/KatToken-exp2.spec new file mode 100644 index 0000000..9b2ff7a --- /dev/null +++ b/certora/specs/KatToken-exp2.spec @@ -0,0 +1,25 @@ +import "./exp2-summary.spec"; + +methods { + function inflationAdmin() external returns (address) envfree; + function inflationBeneficiary() external returns (address) envfree; + function inflationFactor() external returns (uint256) envfree; + function MAX_INFLATION() external returns (uint256) envfree; + function merkleMinter() external returns (address) envfree; + function mintCapacity(address) external returns (uint256) envfree; +} + +rule nonTrivialDistributeInflation() { + env e; + + // enforce non-trivial inflation + require(inflationFactor() > MAX_INFLATION() / 2); + require(inflationFactor() < MAX_INFLATION()); + + uint256 capacityBefore = mintCapacity(inflationBeneficiary()); + + distributeInflation(e); + + uint256 capacityAfter = mintCapacity(inflationBeneficiary()); + satisfy(capacityAfter > capacityBefore); +} \ No newline at end of file diff --git a/certora/specs/KatToken-simple.spec b/certora/specs/KatToken-simple.spec index 16f9ea9..a177771 100644 --- a/certora/specs/KatToken-simple.spec +++ b/certora/specs/KatToken-simple.spec @@ -1,5 +1,3 @@ -import "./exp2-summary.spec"; - methods { function inflationAdmin() external returns (address) envfree; function inflationBeneficiary() external returns (address) envfree; @@ -37,18 +35,3 @@ rule canOnlySendAvailableMintCapacity() { assert(ownCapacityBefore >= amount); assert(ownCapacityBefore + toCapacityBefore == ownCapacityAfter + toCapacityAfter); } - -rule nonTrivialDistributeInflation() { - env e; - - // enforce non-trivial inflation - require(inflationFactor() > MAX_INFLATION() / 2); - require(inflationFactor() < MAX_INFLATION()); - - uint256 capacityBefore = mintCapacity(inflationBeneficiary()); - - distributeInflation(e); - - uint256 capacityAfter = mintCapacity(inflationBeneficiary()); - satisfy(capacityAfter > capacityBefore); -} \ No newline at end of file From 4a248ef2a80d92ab19d05c3847ea8c70808ede31 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 7 Mar 2025 11:08:08 +0100 Subject: [PATCH 22/37] add nontrivial version of claimKatToken where we actually have a proof --- certora/specs/MerkleMinter-simple.spec | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/certora/specs/MerkleMinter-simple.spec b/certora/specs/MerkleMinter-simple.spec index 9e58d6d..9db10bb 100644 --- a/certora/specs/MerkleMinter-simple.spec +++ b/certora/specs/MerkleMinter-simple.spec @@ -31,4 +31,18 @@ rule canOnlyClaimWhenNotLocked() { claimKatToken(e, proof, amount, receiver); assert(e.block.timestamp > unlockTime() || !locked()); -} \ No newline at end of file +} + +rule canOnlyClaimWhenNotLocked_nontrivial() { + env e; + + bytes32[] proof; + uint256 amount; + address receiver; + + require(proof.length > 0); + + claimKatToken(e, proof, amount, receiver); + + assert(e.block.timestamp > unlockTime() || !locked()); +} From c6326157bce6d3fc13974cc82c2f27a63a1d6878 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 7 Mar 2025 11:46:00 +0100 Subject: [PATCH 23/37] add some checks about the actual implementation of exp2 --- .github/workflows/run-confs.yml | 1 + certora/confs/exp2-implementation.conf | 21 +++++++++ certora/specs/exp2-implementation.spec | 59 ++++++++++++++++++++++++++ 3 files changed, 81 insertions(+) create mode 100644 certora/confs/exp2-implementation.conf create mode 100644 certora/specs/exp2-implementation.spec diff --git a/.github/workflows/run-confs.yml b/.github/workflows/run-confs.yml index c5fc7c9..d377b5a 100644 --- a/.github/workflows/run-confs.yml +++ b/.github/workflows/run-confs.yml @@ -6,6 +6,7 @@ env: FOUNDRY_PROFILE: ci CONFIGS: | certora/confs/exp2-check-summary.conf + certora/confs/exp2-implementation.conf certora/confs/KatToken-exp2.conf certora/confs/KatToken-simple.conf certora/confs/MerkleMinter-simple.conf diff --git a/certora/confs/exp2-implementation.conf b/certora/confs/exp2-implementation.conf new file mode 100644 index 0000000..8ff3a6a --- /dev/null +++ b/certora/confs/exp2-implementation.conf @@ -0,0 +1,21 @@ +{ + "assert_autofinder_success": true, + "files": [ + "certora/harnesses/PowUtilHarness.sol", + "src/KatToken.sol", + ], + "global_timeout": "7200", + "loop_iter": "2", + "optimistic_loop": true, + "msg": "Check exp2 summary", + "packages": [ + "@openzeppelin/merkle-tree=node_modules/@openzeppelin/merkle-tree", + "@openzeppelin-contracts-5.1.0=dependencies/@openzeppelin-contracts-5.1.0", + "forge-std-1.9.4=dependencies/forge-std-1.9.4" + ], + "process": "emv", + "server": "production", + "solc": "solc8.28", + "solc_via_ir": false, + "verify": "PowUtilHarness:certora/specs/exp2-implementation.spec" +} \ No newline at end of file diff --git a/certora/specs/exp2-implementation.spec b/certora/specs/exp2-implementation.spec new file mode 100644 index 0000000..45adc6f --- /dev/null +++ b/certora/specs/exp2-implementation.spec @@ -0,0 +1,59 @@ +/** + * Check properties on the actual implementation here. + */ + +using KatToken as KatToken; + +methods { + function exp2(uint256 x) external returns (uint256) envfree; + + function KatToken.inflationFactor() external returns (uint256) envfree; + function KatToken.MAX_INFLATION() external returns (uint256) envfree; +} + +definition ONE18() returns uint256 = 1000000000000000000; +definition days(uint256 d) returns uint256 = assert_uint256(d * 60 * 60 * 24); + +rule exp2_correctValues() { + assert(exp2(require_uint256(0 * ONE18())) == 1*ONE18()); + assert(exp2(require_uint256(1 * ONE18())) == 2*ONE18()); + assert(exp2(require_uint256(2 * ONE18())) == 4*ONE18()); + assert(exp2(require_uint256(3 * ONE18())) == 8*ONE18()); + assert(exp2(require_uint256(4 * ONE18())) == 16*ONE18()); +} + +rule exp2_additivity() { + uint256 x; + uint256 y; + + assert(exp2(require_uint256(x + y)) == exp2(x) * exp2(y)); +} + +/** + * Prove that the inflation factor is bounded by MAX_INFLATION. + */ +invariant inflationFactorIsBounded() + KatToken.inflationFactor() <= KatToken.MAX_INFLATION(); + +/** + * Show that exp2 can not overflow within 100 years. + * Technically, we show that exp2 stays below 0x100000000000000000, which is + * well below anything close to an overflow. + */ +rule exp2_noOverflow() { + // we know that the inflation factor is bounded by MAX_INFLATION + uint256 inflationFactor = KatToken.inflationFactor(); + requireInvariant(inflationFactorIsBounded); + // let's assume that we can't have more than 100 years of inflation + uint256 timeElapsed; + require(timeElapsed <= 100 * days(365)); + uint256 x = assert_uint256((inflationFactor * timeElapsed) / days(365)); + + // that means x can't be more than 5 + assert(x < 5 * ONE18()); + + // this is well below anything that might overflow ... + assert(exp2(x) < 32 * ONE18() && 32 * ONE18() < 0x100000000000000000); + // ... but the upper bound is reasonably tight + satisfy(exp2(x) > 16 * ONE18()); +} \ No newline at end of file From bbb254dcb61080f75686b7973293e03caf35649d Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 7 Mar 2025 11:46:35 +0100 Subject: [PATCH 24/37] a comment --- certora/specs/exp2-implementation.spec | 3 +++ 1 file changed, 3 insertions(+) diff --git a/certora/specs/exp2-implementation.spec b/certora/specs/exp2-implementation.spec index 45adc6f..2a47a07 100644 --- a/certora/specs/exp2-implementation.spec +++ b/certora/specs/exp2-implementation.spec @@ -14,6 +14,9 @@ methods { definition ONE18() returns uint256 = 1000000000000000000; definition days(uint256 d) returns uint256 = assert_uint256(d * 60 * 60 * 24); +/** + * Show that exp2 is actually exact for some easy values. + */ rule exp2_correctValues() { assert(exp2(require_uint256(0 * ONE18())) == 1*ONE18()); assert(exp2(require_uint256(1 * ONE18())) == 2*ONE18()); From 6c36e41908e4b36eeb034d2d5682aa6a3310ccf4 Mon Sep 17 00:00:00 2001 From: Otakar Date: Mon, 10 Mar 2025 07:41:44 +0100 Subject: [PATCH 25/37] Initial notes added --- certora/notes.txt | 46 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 46 insertions(+) create mode 100644 certora/notes.txt diff --git a/certora/notes.txt b/certora/notes.txt new file mode 100644 index 0000000..d714f48 --- /dev/null +++ b/certora/notes.txt @@ -0,0 +1,46 @@ + +// questions / observations: +MerkleMinter.claimKatToken can be called with amount = 0 +KatToken.distributeInflation: wouldn't it be better to add a check block.timestamp > lastMintCapacityIncrease at the beginning to save execution of the other commands? +KatToken.distributeInflation: is the check on line 133 needed? +KatToken.distributeMintCapacity are the checks on lines 144 and 145 needed? +KatToken.distributeMintCapacity can we use unchecked instead? +KatToken: line 115 can't we have >= instead of > +wrong comment in KatToken.distributeInflation line 132, it should be before line 129 +inflationBeneficiary and inflationAdmin: wouldn't it be better to use the existing Ownable module? + - the new owner cannot decline +there's no check that merkleMinter is actually a MerkleMinter contract + +// properties: +---------------- +Powutil: + +exp2(x) == 2^x (or differs by at most 1e18, etc.), only for x < 1.03 * 1000 years +exp2(x + y) == exp2(x) * exp2(y) + +---------------- +merkleminter: + +kattoken cannot be changed +locked can only change from true -> false +rootSetter can only change from x -> 0 +root can only change once +only rootSetter can call init +only unlocker can call unlock +claimKatToken cannot be called before unlockTime unless already unlocked +claimKatToken will increase receiver's balance when executed succesfully + +---------------- +kattoken: + +only certain methods may increase/decrease total mint capacity +total mint capacity + mintedTokens can only increase +lastMintCapacityIncrease can only increase +distributedSupplyCap == total mint capacity + mintedTokens +for all x: mintCapacity[x] <= distributedSupplyCap +inflation is less than MAX_INFLATION +inflationBeneficiary and inflationAdmin != 0 +only inflationBeneficiary and inflationAdmin can change inflationBeneficiary and inflationAdmin respectively + +summarise _mint, keep track of balances in CVL +summarise MerklerProof.verify to nondet From aac523e2d5d323ef216f94772aa8afedeb53c531 Mon Sep 17 00:00:00 2001 From: Otakar Date: Mon, 10 Mar 2025 08:31:18 +0100 Subject: [PATCH 26/37] harness added, runscript, new rules --- certora/confs/KatToken-simple.conf | 4 +-- certora/harnesses/KatTokenHarness.sol | 24 +++++++++++++++++ certora/notes.txt | 4 +-- certora/scripts/run.sh | 2 ++ certora/specs/KatToken-simple.spec | 37 +++++++++++++++++++++++++-- 5 files changed, 65 insertions(+), 6 deletions(-) create mode 100644 certora/harnesses/KatTokenHarness.sol create mode 100755 certora/scripts/run.sh diff --git a/certora/confs/KatToken-simple.conf b/certora/confs/KatToken-simple.conf index b7cd399..7de6ef9 100644 --- a/certora/confs/KatToken-simple.conf +++ b/certora/confs/KatToken-simple.conf @@ -1,7 +1,7 @@ { "assert_autofinder_success": true, "files": [ - "src/KatToken.sol" + "certora/harnesses/KatTokenHarness.sol" ], "global_timeout": "7200", "loop_iter": "2", @@ -16,5 +16,5 @@ "server": "production", "solc": "solc8.28", "solc_via_ir": false, - "verify": "KatToken:certora/specs/KatToken-simple.spec" + "verify": "KatTokenHarness:certora/specs/KatToken-simple.spec" } \ No newline at end of file diff --git a/certora/harnesses/KatTokenHarness.sol b/certora/harnesses/KatTokenHarness.sol new file mode 100644 index 0000000..b210947 --- /dev/null +++ b/certora/harnesses/KatTokenHarness.sol @@ -0,0 +1,24 @@ +// SPDX-License-Identifier: SEE LICENSE IN LICENSE +pragma solidity 0.8.28; +import {KatToken} from "src/KatToken.sol"; + +contract KatTokenHarness is KatToken { + constructor( + string memory _name, + string memory _symbol, + address _inflationAdmin, + address _inflationBeneficiary, + address _merkleMinter + ) KatToken(_name, _symbol, _inflationAdmin, _inflationBeneficiary, _merkleMinter) + { + } + + function get_lastMintCapacityIncrease() public view returns (uint256) { + return lastMintCapacityIncrease; + } + + function get_distributedSupplyCap() public view returns (uint256) { + return distributedSupplyCap; + } + +} diff --git a/certora/notes.txt b/certora/notes.txt index d714f48..50dfb4a 100644 --- a/certora/notes.txt +++ b/certora/notes.txt @@ -5,9 +5,9 @@ KatToken.distributeInflation: wouldn't it be better to add a check block.timesta KatToken.distributeInflation: is the check on line 133 needed? KatToken.distributeMintCapacity are the checks on lines 144 and 145 needed? KatToken.distributeMintCapacity can we use unchecked instead? -KatToken: line 115 can't we have >= instead of > +KatToken: line 115 can't we have >= instead of > ? wrong comment in KatToken.distributeInflation line 132, it should be before line 129 -inflationBeneficiary and inflationAdmin: wouldn't it be better to use the existing Ownable module? +inflationBeneficiary and inflationAdmin: wouldn't it be better to use the existing Ownable interface? - the new owner cannot decline there's no check that merkleMinter is actually a MerkleMinter contract diff --git a/certora/scripts/run.sh b/certora/scripts/run.sh new file mode 100755 index 0000000..746061c --- /dev/null +++ b/certora/scripts/run.sh @@ -0,0 +1,2 @@ +# run this from the root directory. i.e. via './certora/scripts/run.sh' +certoraRun certora/confs/KatToken-simple.conf \ No newline at end of file diff --git a/certora/specs/KatToken-simple.spec b/certora/specs/KatToken-simple.spec index a177771..73a814f 100644 --- a/certora/specs/KatToken-simple.spec +++ b/certora/specs/KatToken-simple.spec @@ -5,10 +5,17 @@ methods { function MAX_INFLATION() external returns (uint256) envfree; function merkleMinter() external returns (address) envfree; function mintCapacity(address) external returns (uint256) envfree; + + //harness methods declared envfree + function get_lastMintCapacityIncrease() external returns (uint256) envfree; + function get_distributedSupplyCap() external returns (uint256) envfree; + + + //MerkleProof + function _.verify(bytes32[] memory, bytes32, bytes32) internal => NONDET; } -rule onlyAdminCanChangeAdmin() { - env e; +rule integrityOfchangeInflationAdmin(env e) { address oldOwner = inflationAdmin(); address newOwner; @@ -18,6 +25,32 @@ rule onlyAdminCanChangeAdmin() { assert(inflationAdmin() == newOwner); } +rule integrityOfchangeInflationBeneficiary(env e) { + address oldOwner = inflationBeneficiary(); + address newOwner; + + changeInflationBeneficiary(e, newOwner); + + assert(e.msg.sender == oldOwner); + assert(inflationBeneficiary() == newOwner); +} + +rule lastMintCapacityIncreaseDeverDecreases(env e, method f) +{ + uint256 lastMintCapacityIncrease_pre = get_lastMintCapacityIncrease(); + + calldataarg args; + f(e, args); + uint256 lastMintCapacityIncrease_post = get_lastMintCapacityIncrease(); + assert lastMintCapacityIncrease_post >= lastMintCapacityIncrease_pre; +} + +//mintCapacity[x] <= distributedSupplyCap +// not an inductive property :( we need to use the equality +// lets get rid of this. it will be in implied by the quality property anyway +invariant mintCapacityLessThanDistributedSupplyCap(address a) + mintCapacity(a) <= get_distributedSupplyCap(); + rule canOnlySendAvailableMintCapacity() { env e; address to; From f3c4b3322ec1a61a7aeab9ecb0635f5c6d9fdac9 Mon Sep 17 00:00:00 2001 From: Otakar Date: Tue, 11 Mar 2025 13:24:39 +0100 Subject: [PATCH 27/37] More rules --- certora/notes.txt | 33 +++++++------ certora/scripts/run.sh | 7 ++- certora/specs/KatToken-simple.spec | 64 ++++++++++++++++++++++++-- certora/specs/MerkleMinter-simple.spec | 60 ++++++++++++++++++------ certora/specs/exp2-implementation.spec | 45 ++++++++++++++++-- 5 files changed, 171 insertions(+), 38 deletions(-) diff --git a/certora/notes.txt b/certora/notes.txt index 50dfb4a..f89f904 100644 --- a/certora/notes.txt +++ b/certora/notes.txt @@ -21,26 +21,29 @@ exp2(x + y) == exp2(x) * exp2(y) ---------------- merkleminter: -kattoken cannot be changed -locked can only change from true -> false -rootSetter can only change from x -> 0 +kattoken cannot be changed done +locked can only change from true -> false done +rootSetter can only change from x -> 0 done root can only change once -only rootSetter can call init -only unlocker can call unlock -claimKatToken cannot be called before unlockTime unless already unlocked -claimKatToken will increase receiver's balance when executed succesfully +only rootSetter can call init done +only unlocker can call unlock done +claimKatToken cannot be called before unlockTime unless already unlocked done +claimKatToken will increase receiver's balance when executed succesfully ---------------- kattoken: -only certain methods may increase/decrease total mint capacity -total mint capacity + mintedTokens can only increase -lastMintCapacityIncrease can only increase -distributedSupplyCap == total mint capacity + mintedTokens -for all x: mintCapacity[x] <= distributedSupplyCap -inflation is less than MAX_INFLATION -inflationBeneficiary and inflationAdmin != 0 -only inflationBeneficiary and inflationAdmin can change inflationBeneficiary and inflationAdmin respectively +only certain methods may increase/decrease total mint capacity done +total mint capacity + mintedTokens can only increase done +lastMintCapacityIncrease can only increase done +distributedSupplyCap can only increase done +distributedSupplyCap == total mint capacity + mintedTokens done +for all x: mintCapacity[x] <= distributedSupplyCap done +inflation is less than MAX_INFLATION done +inflationBeneficiary and inflationAdmin != 0 done violated +only inflationBeneficiary and inflationAdmin can change inflationBeneficiary and inflationAdmin respectively done summarise _mint, keep track of balances in CVL summarise MerklerProof.verify to nondet + +exp2 error max 10 tokens per year diff --git a/certora/scripts/run.sh b/certora/scripts/run.sh index 746061c..b052b9d 100755 --- a/certora/scripts/run.sh +++ b/certora/scripts/run.sh @@ -1,2 +1,7 @@ # run this from the root directory. i.e. via './certora/scripts/run.sh' -certoraRun certora/confs/KatToken-simple.conf \ No newline at end of file +# certoraRun certora/confs/KatToken-simple.conf + +certoraRun certora/confs/exp2-implementation.conf --rule exp2_monotone01 --rule exp2_monotone12 +# certoraRun certora/confs/exp2-implementation.conf + +# certoraRun certora/confs/MerkleMinter-simple.conf diff --git a/certora/specs/KatToken-simple.spec b/certora/specs/KatToken-simple.spec index 73a814f..fd0faf0 100644 --- a/certora/specs/KatToken-simple.spec +++ b/certora/specs/KatToken-simple.spec @@ -1,3 +1,5 @@ +import "./exp2-summary.spec"; + methods { function inflationAdmin() external returns (address) envfree; function inflationBeneficiary() external returns (address) envfree; @@ -10,6 +12,8 @@ methods { function get_lastMintCapacityIncrease() external returns (uint256) envfree; function get_distributedSupplyCap() external returns (uint256) envfree; + function ERC20._mint(address to, uint256 amount) internal + => _mintCVL(to, amount); //MerkleProof function _.verify(bytes32[] memory, bytes32, bytes32) internal => NONDET; @@ -45,11 +49,15 @@ rule lastMintCapacityIncreaseDeverDecreases(env e, method f) assert lastMintCapacityIncrease_post >= lastMintCapacityIncrease_pre; } -//mintCapacity[x] <= distributedSupplyCap -// not an inductive property :( we need to use the equality -// lets get rid of this. it will be in implied by the quality property anyway -invariant mintCapacityLessThanDistributedSupplyCap(address a) - mintCapacity(a) <= get_distributedSupplyCap(); +rule distributedSupplyCapDeverDecreases(env e, method f) +{ + uint256 distributedSupplyCap_pre = get_distributedSupplyCap(); + + calldataarg args; + f(e, args); + uint256 distributedSupplyCap_post = get_distributedSupplyCap(); + assert distributedSupplyCap_post >= distributedSupplyCap_pre; +} rule canOnlySendAvailableMintCapacity() { env e; @@ -68,3 +76,49 @@ rule canOnlySendAvailableMintCapacity() { assert(ownCapacityBefore >= amount); assert(ownCapacityBefore + toCapacityBefore == ownCapacityAfter + toCapacityAfter); } + +ghost mapping(address => mathint) mintedTo; +ghost mathint totalMintCapacityChange; +ghost mathint totalMintedChange; + +function _mintCVL(address to, uint256 amount) +{ + mintedTo[to] = mintedTo[to] + amount; + totalMintedChange = totalMintedChange + amount; +} + +hook Sstore KatTokenHarness.mintCapacity[KEY address user] uint256 newCap (uint256 oldCap) { + totalMintCapacityChange = totalMintCapacityChange + newCap - oldCap; +} + +function initGhosts() +{ + totalMintCapacityChange = 0; + totalMintedChange = 0; +} + +rule mintCapacityPlusMintedNeverDecrease(env e, method f) +{ + initGhosts(); + calldataarg args; + f(e, args); + assert totalMintedChange + totalMintCapacityChange >= 0; +} + +rule mintCapacityPlusMintedEqualsDistributedSupplyCap(env e, method f) +{ + initGhosts(); + uint256 distributedSupplyCap_pre = get_distributedSupplyCap(); + calldataarg args; + f(e, args); + uint256 distributedSupplyCap_post = get_distributedSupplyCap(); + assert distributedSupplyCap_post - distributedSupplyCap_pre == + totalMintedChange + totalMintCapacityChange; +} + +// probably wrong property +invariant inflationBeneficiaryNeverZero() + inflationBeneficiary() != 0; + +invariant inflationAdminNeverZero() + inflationAdmin() != 0; diff --git a/certora/specs/MerkleMinter-simple.spec b/certora/specs/MerkleMinter-simple.spec index 9db10bb..c1dc792 100644 --- a/certora/specs/MerkleMinter-simple.spec +++ b/certora/specs/MerkleMinter-simple.spec @@ -4,9 +4,10 @@ methods { function katToken() external returns (address) envfree; function unlockTime() external returns (uint256) envfree; function locked() external returns (bool) envfree; + function unlocker() external returns (address) envfree; } -rule onlyRootCanInit() { +rule integrityOfInit() { env e; bytes32 _root; address _katToken; @@ -21,28 +22,59 @@ rule onlyRootCanInit() { assert(katToken() == _katToken); } -rule canOnlyClaimWhenNotLocked() { - env e; +rule integrityOfUnlock(env e) { + address currentUnlocker = unlocker(); + unlock(e); - bytes32[] proof; - uint256 amount; - address receiver; + assert(e.msg.sender == currentUnlocker); + assert(locked() == false); + assert(unlocker() == 0); +} +rule canOnlyClaimWhenNotLocked(env e) +{ + bytes32[] proof; uint256 amount; address receiver; claimKatToken(e, proof, amount, receiver); assert(e.block.timestamp > unlockTime() || !locked()); } -rule canOnlyClaimWhenNotLocked_nontrivial() { - env e; - - bytes32[] proof; - uint256 amount; - address receiver; - +rule canOnlyClaimWhenNotLocked_nontrivial(env e) +{ + bytes32[] proof; uint256 amount; address receiver; require(proof.length > 0); claimKatToken(e, proof, amount, receiver); - assert(e.block.timestamp > unlockTime() || !locked()); } + +rule katTokenCannotBeChanged(env e, method f) + filtered { f -> f.selector != sig:init(bytes32, address).selector } + // init is the only method that can set the katToken +{ + address token_pre = katToken(); + calldataarg args; + f(e, args); + address token_post = katToken(); + assert token_pre == token_post; +} + +//ocked can only change from true -> false +rule lockedValueChange(env e, method f) +{ + bool locked_pre = locked(); + calldataarg args; + f(e, args); + bool locked_post = locked(); + assert locked_post => locked_pre; // if true after then if was already true before, i.e. it cannot go from false to true +} + +//rootSetter can only change from x -> 0 +rule rootSetterValueChange(env e, method f) +{ + address rootSetter_pre = rootSetter(); + calldataarg args; + f(e, args); + address rootSetter_post = rootSetter(); + assert rootSetter_post == rootSetter_pre || rootSetter_post == 0; +} diff --git a/certora/specs/exp2-implementation.spec b/certora/specs/exp2-implementation.spec index 2a47a07..2ca38c4 100644 --- a/certora/specs/exp2-implementation.spec +++ b/certora/specs/exp2-implementation.spec @@ -26,10 +26,49 @@ rule exp2_correctValues() { } rule exp2_additivity() { - uint256 x; - uint256 y; + uint256 x; uint256 y; uint256 total; + require total == x + y; + require total <= 5*ONE18(); - assert(exp2(require_uint256(x + y)) == exp2(x) * exp2(y)); + assert exp2(total)*ONE18() == exp2(x) * exp2(y); +} + +rule exp2_additivity2() { + uint256 x; uint256 total; + require total == x + x; + require total <= 5*ONE18(); + + assert exp2(total)*ONE18() == exp2(x) * exp2(x); +} + +rule exp2_correctnes(uint8 n) { + mathint BOUND = 100; + uint256 x = require_uint256(n*ONE18()); + require n <= BOUND; + + assert exp2(x) == (1 << n) * ONE18(); +} + +rule exp2_monotone01(env e) +{ + mathint lBOUND = 0 * ONE18(); + mathint uBOUND = 1 * ONE18(); + uint256 x; uint256 y; + require x >= lBOUND && y >= lBOUND; + require x < uBOUND && y < uBOUND; + + assert x < y => exp2(x) <= exp2(y); +} + +rule exp2_monotone12(env e) +{ + mathint lBOUND = 1 * ONE18(); + mathint uBOUND = 2 * ONE18(); + uint256 x; uint256 y; + require x >= lBOUND && y >= lBOUND; + require x < uBOUND && y < uBOUND; + + assert x < y => exp2(x) <= exp2(y); } /** From 67f6c7c7ffea440ccb6612317633cfc8f83d05b8 Mon Sep 17 00:00:00 2001 From: Otakar Date: Tue, 11 Mar 2025 14:32:02 +0100 Subject: [PATCH 28/37] gitignore updated --- .gitignore | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/.gitignore b/.gitignore index 2acac2c..76e8f8d 100644 --- a/.gitignore +++ b/.gitignore @@ -19,4 +19,7 @@ node_modules/ # Certora files .certora_internal/ .venv/ -emv-*-certora-* \ No newline at end of file +emv-*-certora-* +package-lock.json +remappings.txt +soldeer.lock From 226f21e14ea36de82f01f8b2415da6a26eaa603e Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Tue, 11 Mar 2025 14:54:23 +0100 Subject: [PATCH 29/37] minor fixes to setup specs --- certora/specs/KatToken-simple.spec | 1 + certora/specs/MerkleMinter-simple.spec | 7 ++++--- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/certora/specs/KatToken-simple.spec b/certora/specs/KatToken-simple.spec index a177771..cfe7ac4 100644 --- a/certora/specs/KatToken-simple.spec +++ b/certora/specs/KatToken-simple.spec @@ -13,6 +13,7 @@ rule onlyAdminCanChangeAdmin() { address newOwner; changeInflationAdmin(e, newOwner); + acceptInflationAdmin(e); assert(e.msg.sender == oldOwner); assert(inflationAdmin() == newOwner); diff --git a/certora/specs/MerkleMinter-simple.spec b/certora/specs/MerkleMinter-simple.spec index 9db10bb..ef5fb60 100644 --- a/certora/specs/MerkleMinter-simple.spec +++ b/certora/specs/MerkleMinter-simple.spec @@ -17,7 +17,6 @@ rule onlyRootCanInit() { assert(e.msg.sender == rootBefore); assert(root() == _root); - assert(rootSetter() == 0); assert(katToken() == _katToken); } @@ -25,10 +24,11 @@ rule canOnlyClaimWhenNotLocked() { env e; bytes32[] proof; + uint256 index; uint256 amount; address receiver; - claimKatToken(e, proof, amount, receiver); + claimKatToken(e, proof, index, amount, receiver); assert(e.block.timestamp > unlockTime() || !locked()); } @@ -37,12 +37,13 @@ rule canOnlyClaimWhenNotLocked_nontrivial() { env e; bytes32[] proof; + uint256 index; uint256 amount; address receiver; require(proof.length > 0); - claimKatToken(e, proof, amount, receiver); + claimKatToken(e, proof, index, amount, receiver); assert(e.block.timestamp > unlockTime() || !locked()); } From 54f799398cb1eb86de6a5063e3e0ef6f198ee9e0 Mon Sep 17 00:00:00 2001 From: Otakar Date: Sun, 16 Mar 2025 14:11:36 +0100 Subject: [PATCH 30/37] Rules adjusted --- certora/confs/exp2-implementation.conf | 8 +++++-- certora/scripts/run.sh | 4 ++-- certora/specs/KatToken-simple.spec | 11 +++------ certora/specs/MerkleMinter-simple.spec | 33 +++++++++++++++++++------- certora/specs/exp2-implementation.spec | 33 ++++++++++++++++++++------ 5 files changed, 61 insertions(+), 28 deletions(-) diff --git a/certora/confs/exp2-implementation.conf b/certora/confs/exp2-implementation.conf index 8ff3a6a..9bcba65 100644 --- a/certora/confs/exp2-implementation.conf +++ b/certora/confs/exp2-implementation.conf @@ -5,17 +5,21 @@ "src/KatToken.sol", ], "global_timeout": "7200", + "smt_timeout": "7200", "loop_iter": "2", "optimistic_loop": true, - "msg": "Check exp2 summary", "packages": [ "@openzeppelin/merkle-tree=node_modules/@openzeppelin/merkle-tree", "@openzeppelin-contracts-5.1.0=dependencies/@openzeppelin-contracts-5.1.0", "forge-std-1.9.4=dependencies/forge-std-1.9.4" ], + "prover_args": [ + # "-smt_bitVectorTheory true" + ], "process": "emv", "server": "production", "solc": "solc8.28", "solc_via_ir": false, - "verify": "PowUtilHarness:certora/specs/exp2-implementation.spec" + "verify": "PowUtilHarness:certora/specs/exp2-implementation.spec", + "msg": "Check exp2 BV", } \ No newline at end of file diff --git a/certora/scripts/run.sh b/certora/scripts/run.sh index b052b9d..a8f509d 100755 --- a/certora/scripts/run.sh +++ b/certora/scripts/run.sh @@ -1,7 +1,7 @@ # run this from the root directory. i.e. via './certora/scripts/run.sh' # certoraRun certora/confs/KatToken-simple.conf -certoraRun certora/confs/exp2-implementation.conf --rule exp2_monotone01 --rule exp2_monotone12 +# certoraRun certora/confs/exp2-implementation.conf --rule exp2_monotonePlus01 # certoraRun certora/confs/exp2-implementation.conf -# certoraRun certora/confs/MerkleMinter-simple.conf +certoraRun certora/confs/MerkleMinter-simple.conf diff --git a/certora/specs/KatToken-simple.spec b/certora/specs/KatToken-simple.spec index fd0faf0..06da4f8 100644 --- a/certora/specs/KatToken-simple.spec +++ b/certora/specs/KatToken-simple.spec @@ -16,7 +16,9 @@ methods { => _mintCVL(to, amount); //MerkleProof - function _.verify(bytes32[] memory, bytes32, bytes32) internal => NONDET; + function _.verify(bytes32[] memory, bytes32, bytes32) external => NONDET DELETE; + + function _.eip712Domain() external => NONDET DELETE; } rule integrityOfchangeInflationAdmin(env e) { @@ -115,10 +117,3 @@ rule mintCapacityPlusMintedEqualsDistributedSupplyCap(env e, method f) assert distributedSupplyCap_post - distributedSupplyCap_pre == totalMintedChange + totalMintCapacityChange; } - -// probably wrong property -invariant inflationBeneficiaryNeverZero() - inflationBeneficiary() != 0; - -invariant inflationAdminNeverZero() - inflationAdmin() != 0; diff --git a/certora/specs/MerkleMinter-simple.spec b/certora/specs/MerkleMinter-simple.spec index c1dc792..c45a41f 100644 --- a/certora/specs/MerkleMinter-simple.spec +++ b/certora/specs/MerkleMinter-simple.spec @@ -5,6 +5,11 @@ methods { function unlockTime() external returns (uint256) envfree; function locked() external returns (bool) envfree; function unlocker() external returns (address) envfree; + + //MerkleProof + function _.verify(bytes32[], bytes32, bytes32) external => NONDET DELETE; + + function _.eip712Domain() external => NONDET DELETE; } rule integrityOfInit() { @@ -12,19 +17,18 @@ rule integrityOfInit() { bytes32 _root; address _katToken; - address rootBefore = rootSetter(); + address rootSetterBefore = rootSetter(); init(e, _root, _katToken); - assert(e.msg.sender == rootBefore); + assert(e.msg.sender == rootSetterBefore); assert(root() == _root); - assert(rootSetter() == 0); assert(katToken() == _katToken); } -rule integrityOfUnlock(env e) { +rule integrityOfUnlockAndRenounceUnlocker(env e) { address currentUnlocker = unlocker(); - unlock(e); + unlockAndRenounceUnlocker(e); assert(e.msg.sender == currentUnlocker); assert(locked() == false); @@ -33,18 +37,18 @@ rule integrityOfUnlock(env e) { rule canOnlyClaimWhenNotLocked(env e) { - bytes32[] proof; uint256 amount; address receiver; - claimKatToken(e, proof, amount, receiver); + bytes32[] proof; uint256 index; uint256 amount; address receiver; + claimKatToken(e, proof, index, amount, receiver); assert(e.block.timestamp > unlockTime() || !locked()); } rule canOnlyClaimWhenNotLocked_nontrivial(env e) { - bytes32[] proof; uint256 amount; address receiver; + bytes32[] proof; uint256 index; uint256 amount; address receiver; require(proof.length > 0); - claimKatToken(e, proof, amount, receiver); + claimKatToken(e, proof, index, amount, receiver); assert(e.block.timestamp > unlockTime() || !locked()); } @@ -59,6 +63,17 @@ rule katTokenCannotBeChanged(env e, method f) assert token_pre == token_post; } +rule rootCannotBeChanged(env e, method f) + filtered { f -> f.selector != sig:init(bytes32, address).selector } + // init is the only method that can set the root +{ + bytes32 root_pre = root(); + calldataarg args; + f(e, args); + bytes32 root_post = root(); + assert root_pre == root_post; +} + //ocked can only change from true -> false rule lockedValueChange(env e, method f) { diff --git a/certora/specs/exp2-implementation.spec b/certora/specs/exp2-implementation.spec index 2ca38c4..93bf6e3 100644 --- a/certora/specs/exp2-implementation.spec +++ b/certora/specs/exp2-implementation.spec @@ -9,6 +9,7 @@ methods { function KatToken.inflationFactor() external returns (uint256) envfree; function KatToken.MAX_INFLATION() external returns (uint256) envfree; + function _.eip712Domain() external => NONDET DELETE; } definition ONE18() returns uint256 = 1000000000000000000; @@ -49,15 +50,15 @@ rule exp2_correctnes(uint8 n) { assert exp2(x) == (1 << n) * ONE18(); } -rule exp2_monotone01(env e) +rule exp2_monotonePlus01(env e) { mathint lBOUND = 0 * ONE18(); - mathint uBOUND = 1 * ONE18(); - uint256 x; uint256 y; - require x >= lBOUND && y >= lBOUND; - require x < uBOUND && y < uBOUND; + mathint uBOUND = 1 * 10^10; + uint256 x; + require x >= lBOUND; + require x < uBOUND; - assert x < y => exp2(x) <= exp2(y); + assert exp2(x) <= exp2(require_uint256(x+1)); } rule exp2_monotone12(env e) @@ -98,4 +99,22 @@ rule exp2_noOverflow() { assert(exp2(x) < 32 * ONE18() && 32 * ONE18() < 0x100000000000000000); // ... but the upper bound is reasonably tight satisfy(exp2(x) > 16 * ONE18()); -} \ No newline at end of file +} + +// monotonicity +// try x vs. x+1 +// x vs. 2*x + +// rules for interest +// interest for timespan x, vs. interest vs. 2*x + +// inject mutations, demontrate to the customers the bug founding to the customer + + +// "imperminent loss" - concept related to AMM +// liquidity provider provides L, takes fees +// + +// DEFI lama +// tells what kind of protocols, overview of all protocols +// From b7e76dc957d2b15b0265f3991f3ef714ee451551 Mon Sep 17 00:00:00 2001 From: Otakar Date: Tue, 18 Mar 2025 11:24:38 +0100 Subject: [PATCH 31/37] MerkleMinter rules + cleanup --- ...leMinter-simple.conf => MerkleMinter.conf} | 2 +- certora/notes.txt | 97 +++++++++++++------ certora/scripts/run.sh | 3 +- ...leMinter-simple.spec => MerkleMinter.spec} | 54 ++++++++--- certora/specs/exp2-implementation.spec | 11 +-- 5 files changed, 114 insertions(+), 53 deletions(-) rename certora/confs/{MerkleMinter-simple.conf => MerkleMinter.conf} (90%) rename certora/specs/{MerkleMinter-simple.spec => MerkleMinter.spec} (62%) diff --git a/certora/confs/MerkleMinter-simple.conf b/certora/confs/MerkleMinter.conf similarity index 90% rename from certora/confs/MerkleMinter-simple.conf rename to certora/confs/MerkleMinter.conf index f6d8304..119cbad 100644 --- a/certora/confs/MerkleMinter-simple.conf +++ b/certora/confs/MerkleMinter.conf @@ -20,5 +20,5 @@ "server": "production", "solc": "solc8.28", "solc_via_ir": false, - "verify": "MerkleMinter:certora/specs/MerkleMinter-simple.spec" + "verify": "MerkleMinter:certora/specs/MerkleMinter.spec" } \ No newline at end of file diff --git a/certora/notes.txt b/certora/notes.txt index f89f904..cb78388 100644 --- a/certora/notes.txt +++ b/certora/notes.txt @@ -2,48 +2,85 @@ // questions / observations: MerkleMinter.claimKatToken can be called with amount = 0 KatToken.distributeInflation: wouldn't it be better to add a check block.timestamp > lastMintCapacityIncrease at the beginning to save execution of the other commands? -KatToken.distributeInflation: is the check on line 133 needed? -KatToken.distributeMintCapacity are the checks on lines 144 and 145 needed? +KatToken.distributeMintCapacity are the checks on lines 200 and 201 needed? KatToken.distributeMintCapacity can we use unchecked instead? -KatToken: line 115 can't we have >= instead of > ? -wrong comment in KatToken.distributeInflation line 132, it should be before line 129 +KatToken: line 170 can't we have >= instead of > ? inflationBeneficiary and inflationAdmin: wouldn't it be better to use the existing Ownable interface? - the new owner cannot decline + - it can change to the same value there's no check that merkleMinter is actually a MerkleMinter contract +---------------------------------- + +more questions: + +L/info finding: +the MerkleMinter.init function is very dangerous because the operation can only work if the new tree respects the same indexes (i.e. append-only), which is a very strict requirement for off-chain components. +Otherwise, there’s risk of one claiming twice if their claim is available under different indexes before and after the root update + + +L/info finding (this was discussed during the call with the team) KatToken.renounceInflationBeneficiary can be called when inflationFactor is non-zero. This will grant mint capacity to address(0) which is certainly unwanted. Fix is to require (or overwrite) inflationFactor to be zero when the inflationBeneficiary is reset +WHY IS IT A PROBLEM? + + // properties: ---------------- Powutil: -exp2(x) == 2^x (or differs by at most 1e18, etc.), only for x < 1.03 * 1000 years -exp2(x + y) == exp2(x) * exp2(y) +exp2(x) == 2^x , formally: exp2(x *1e18) == 2^x *1e18 +exp2(x+y) == exp2(x)*exp2(y) , formally: exp2(x+y) *1e18 == exp2(x)*exp2(y) +exp2(x) <= exp2(x+1) +lower and upper bounds: LB(x) <= exp2(x) <= UB(x) currently we're using bounds based on 3rd-order Taylor expansions + + more variants of these. With error bounds, etc. ---------------- merkleminter: -kattoken cannot be changed done -locked can only change from true -> false done -rootSetter can only change from x -> 0 done -root can only change once -only rootSetter can call init done -only unlocker can call unlock done -claimKatToken cannot be called before unlockTime unless already unlocked done -claimKatToken will increase receiver's balance when executed succesfully +katToken and root can only change via init +locked can only change from true -> false +rootSetter can only change from x -> 0 +only rootSetter can call init +only unlocker can call unlock +all calls to claimKatToken must revert before unlockTime unless already unlocked +claimKatToken will increase receiver's balance when executed successfully not written +once active, the protocol will not go to an inactive state, i.e., (block.timestamp > unlockTime || !locked) can only change false -> true +indexIsClaimed(index) can only change false -> true +indexIsClaimed(index) == true => claimKatToken(..,index) will revert + +---------------- +katToken: + +only certain methods may increase/decrease total mint capacity +total mint capacity + mintedTokens can only increase +lastMintCapacityIncrease can only increase +distributedSupplyCap can only increase +distributedSupplyCap == total mint capacity + mintedTokens +for all x: mintCapacity[x] <= distributedSupplyCap +mintCapacity of address(0) is always 0 +inflation <= MAX_INFLATION +inflation can be set to any value <= MAX_INFLATION +once renounceInflationAdmin is performed, the inflationAdmin will always be zero + 1. show that renounceInflationAdmin sets inflationAdmin to 0 + 2. show that inflationAdmin can never change from 0 to non-zero +the same for inflationBeneficiary +only inflationBeneficiary can change inflationBeneficiary +only inflationAdmin can change inflationAdmin ---------------- -kattoken: - -only certain methods may increase/decrease total mint capacity done -total mint capacity + mintedTokens can only increase done -lastMintCapacityIncrease can only increase done -distributedSupplyCap can only increase done -distributedSupplyCap == total mint capacity + mintedTokens done -for all x: mintCapacity[x] <= distributedSupplyCap done -inflation is less than MAX_INFLATION done -inflationBeneficiary and inflationAdmin != 0 done violated -only inflationBeneficiary and inflationAdmin can change inflationBeneficiary and inflationAdmin respectively done - -summarise _mint, keep track of balances in CVL -summarise MerklerProof.verify to nondet - -exp2 error max 10 tokens per year +more properties: + +KatToken.sol +158: require(value < MAX_INFLATION, "Inflation too large."); +can we write a rule that shows that all values within range must succeed? + +given any of the privileged addresses (KatToken.inflationAdmin, KatToken.inflationBeneficiary, MerkleMinter.rootSetter), once the corresponding renounce function is called, the given privileged address must remain address(0) indefinitely + +mintCapacity of address(0) is always 0 ..? + +mutations..?? + +any more properties? + +1000 year inflation -> 5e18, maybe use 10e18 instead . use this: 43e18 + +minimum arg to exp2 is about 6M but not a multiplier of it diff --git a/certora/scripts/run.sh b/certora/scripts/run.sh index a8f509d..a50898a 100755 --- a/certora/scripts/run.sh +++ b/certora/scripts/run.sh @@ -1,7 +1,6 @@ -# run this from the root directory. i.e. via './certora/scripts/run.sh' # certoraRun certora/confs/KatToken-simple.conf # certoraRun certora/confs/exp2-implementation.conf --rule exp2_monotonePlus01 # certoraRun certora/confs/exp2-implementation.conf -certoraRun certora/confs/MerkleMinter-simple.conf +certoraRun certora/confs/MerkleMinter.conf diff --git a/certora/specs/MerkleMinter-simple.spec b/certora/specs/MerkleMinter.spec similarity index 62% rename from certora/specs/MerkleMinter-simple.spec rename to certora/specs/MerkleMinter.spec index c45a41f..4daa258 100644 --- a/certora/specs/MerkleMinter-simple.spec +++ b/certora/specs/MerkleMinter.spec @@ -5,6 +5,7 @@ methods { function unlockTime() external returns (uint256) envfree; function locked() external returns (bool) envfree; function unlocker() external returns (address) envfree; + function indexIsClaimed(uint256 index) external returns (bool) envfree; //MerkleProof function _.verify(bytes32[], bytes32, bytes32) external => NONDET DELETE; @@ -12,6 +13,18 @@ methods { function _.eip712Domain() external => NONDET DELETE; } +// Once the claiming becomes possible, the contract will never go to a locked state again +rule onceActivatedItStaysActive(env e1, env e2, method f) +{ + require e1.block.timestamp <= e2.block.timestamp; + bool active_pre = (e1.block.timestamp > unlockTime()) || !locked(); + + calldataarg args; + f(e1, args); + bool active_post = (e2.block.timestamp > unlockTime()) || !locked(); + assert active_pre => active_post; +} + rule integrityOfInit() { env e; bytes32 _root; @@ -43,16 +56,7 @@ rule canOnlyClaimWhenNotLocked(env e) assert(e.block.timestamp > unlockTime() || !locked()); } -rule canOnlyClaimWhenNotLocked_nontrivial(env e) -{ - bytes32[] proof; uint256 index; uint256 amount; address receiver; - require(proof.length > 0); - - claimKatToken(e, proof, index, amount, receiver); - assert(e.block.timestamp > unlockTime() || !locked()); -} - -rule katTokenCannotBeChanged(env e, method f) +rule katTokenCannotBeChangedOutsideInit(env e, method f) filtered { f -> f.selector != sig:init(bytes32, address).selector } // init is the only method that can set the katToken { @@ -63,7 +67,7 @@ rule katTokenCannotBeChanged(env e, method f) assert token_pre == token_post; } -rule rootCannotBeChanged(env e, method f) +rule rootCannotBeChangedOutsideInit(env e, method f) filtered { f -> f.selector != sig:init(bytes32, address).selector } // init is the only method that can set the root { @@ -74,7 +78,7 @@ rule rootCannotBeChanged(env e, method f) assert root_pre == root_post; } -//ocked can only change from true -> false +//locked can only change from true -> false or stay the same rule lockedValueChange(env e, method f) { bool locked_pre = locked(); @@ -84,7 +88,7 @@ rule lockedValueChange(env e, method f) assert locked_post => locked_pre; // if true after then if was already true before, i.e. it cannot go from false to true } -//rootSetter can only change from x -> 0 +//rootSetter can only change from x -> 0 or stay the same rule rootSetterValueChange(env e, method f) { address rootSetter_pre = rootSetter(); @@ -93,3 +97,27 @@ rule rootSetterValueChange(env e, method f) address rootSetter_post = rootSetter(); assert rootSetter_post == rootSetter_pre || rootSetter_post == 0; } + +// indexIsClaimed can only change false -> true or stay the same +rule indexIsClaimedValueChange(env e, method f) +{ + uint256 index; + bool claimed_pre = indexIsClaimed(index); + calldataarg args; + f(e, args); + bool claimed_post = indexIsClaimed(index); + assert claimed_pre => claimed_post; +} + +// indexIsClaimed == true => claimKatToken(..,index) will revert +rule cannotClaimTheIndexTwice(env e) +{ + uint256 index; + bool isClaimed = indexIsClaimed(index); + bytes32[] proof; uint256 amount; address receiver; + + claimKatToken@withrevert(e, proof, index, amount, receiver); + bool reverted = lastReverted; + + assert isClaimed => reverted; +} \ No newline at end of file diff --git a/certora/specs/exp2-implementation.spec b/certora/specs/exp2-implementation.spec index 93bf6e3..a9a9117 100644 --- a/certora/specs/exp2-implementation.spec +++ b/certora/specs/exp2-implementation.spec @@ -72,12 +72,6 @@ rule exp2_monotone12(env e) assert x < y => exp2(x) <= exp2(y); } -/** - * Prove that the inflation factor is bounded by MAX_INFLATION. - */ -invariant inflationFactorIsBounded() - KatToken.inflationFactor() <= KatToken.MAX_INFLATION(); - /** * Show that exp2 can not overflow within 100 years. * Technically, we show that exp2 stays below 0x100000000000000000, which is @@ -86,7 +80,8 @@ invariant inflationFactorIsBounded() rule exp2_noOverflow() { // we know that the inflation factor is bounded by MAX_INFLATION uint256 inflationFactor = KatToken.inflationFactor(); - requireInvariant(inflationFactorIsBounded); + require inflationFactor() <= MAX_INFLATION(); + // let's assume that we can't have more than 100 years of inflation uint256 timeElapsed; require(timeElapsed <= 100 * days(365)); @@ -118,3 +113,5 @@ rule exp2_noOverflow() { // DEFI lama // tells what kind of protocols, overview of all protocols // + +// 10 tokens per year is an acceptable error for the inflation From da1735244278c105c2bd572387b1a626dd005f4f Mon Sep 17 00:00:00 2001 From: Otakar Date: Tue, 18 Mar 2025 14:23:08 +0100 Subject: [PATCH 32/37] KatToken rules + cleanup --- .../{KatToken-simple.conf => KatToken.conf} | 4 +- certora/confs/MerkleMinter.conf | 3 +- ...{exp2-implementation.conf => powUtil.conf} | 6 +- certora/scripts/run.sh | 12 ++-- certora/specs/KatToken-exp2.spec | 25 ------- .../{KatToken-simple.spec => KatToken.spec} | 66 ++++++++++++++++--- ...{exp2-implementation.spec => powUtil.spec} | 6 +- certora/specs/sanity.spec | 1 - 8 files changed, 74 insertions(+), 49 deletions(-) rename certora/confs/{KatToken-simple.conf => KatToken.conf} (84%) rename certora/confs/{exp2-implementation.conf => powUtil.conf} (81%) delete mode 100644 certora/specs/KatToken-exp2.spec rename certora/specs/{KatToken-simple.spec => KatToken.spec} (61%) rename certora/specs/{exp2-implementation.spec => powUtil.spec} (94%) delete mode 100644 certora/specs/sanity.spec diff --git a/certora/confs/KatToken-simple.conf b/certora/confs/KatToken.conf similarity index 84% rename from certora/confs/KatToken-simple.conf rename to certora/confs/KatToken.conf index 7de6ef9..b46987a 100644 --- a/certora/confs/KatToken-simple.conf +++ b/certora/confs/KatToken.conf @@ -6,7 +6,7 @@ "global_timeout": "7200", "loop_iter": "2", "optimistic_loop": true, - "msg": "KatToken simple", + "msg": "KatToken", "packages": [ "@openzeppelin/merkle-tree=node_modules/@openzeppelin/merkle-tree", "@openzeppelin-contracts-5.1.0=dependencies/@openzeppelin-contracts-5.1.0", @@ -16,5 +16,5 @@ "server": "production", "solc": "solc8.28", "solc_via_ir": false, - "verify": "KatTokenHarness:certora/specs/KatToken-simple.spec" + "verify": "KatTokenHarness:certora/specs/KatToken.spec" } \ No newline at end of file diff --git a/certora/confs/MerkleMinter.conf b/certora/confs/MerkleMinter.conf index 119cbad..5797184 100644 --- a/certora/confs/MerkleMinter.conf +++ b/certora/confs/MerkleMinter.conf @@ -10,12 +10,13 @@ "link": [ "MerkleMinter:katToken=KatToken" ], - "msg": "MerkleMinter simple", + "msg": "MerkleMinter", "packages": [ "@openzeppelin/merkle-tree=node_modules/@openzeppelin/merkle-tree", "@openzeppelin-contracts-5.1.0=dependencies/@openzeppelin-contracts-5.1.0", "forge-std-1.9.4=dependencies/forge-std-1.9.4" ], + "process": "emv", "server": "production", "solc": "solc8.28", diff --git a/certora/confs/exp2-implementation.conf b/certora/confs/powUtil.conf similarity index 81% rename from certora/confs/exp2-implementation.conf rename to certora/confs/powUtil.conf index 9bcba65..c3703a5 100644 --- a/certora/confs/exp2-implementation.conf +++ b/certora/confs/powUtil.conf @@ -13,13 +13,11 @@ "@openzeppelin-contracts-5.1.0=dependencies/@openzeppelin-contracts-5.1.0", "forge-std-1.9.4=dependencies/forge-std-1.9.4" ], - "prover_args": [ - # "-smt_bitVectorTheory true" - ], + "process": "emv", "server": "production", "solc": "solc8.28", "solc_via_ir": false, - "verify": "PowUtilHarness:certora/specs/exp2-implementation.spec", + "verify": "PowUtilHarness:certora/specs/powUtil.spec", "msg": "Check exp2 BV", } \ No newline at end of file diff --git a/certora/scripts/run.sh b/certora/scripts/run.sh index a50898a..c763b8d 100755 --- a/certora/scripts/run.sh +++ b/certora/scripts/run.sh @@ -1,6 +1,10 @@ -# certoraRun certora/confs/KatToken-simple.conf +# certoraRun certora/confs/KatToken.conf -# certoraRun certora/confs/exp2-implementation.conf --rule exp2_monotonePlus01 -# certoraRun certora/confs/exp2-implementation.conf +# certoraRun certora/confs/powUtil.conf --rule exp2_monotonePlus01 +# certoraRun certora/confs/powUtil.conf -certoraRun certora/confs/MerkleMinter.conf + +# the rule indexIsClaimedValueChange requires using bitVector theory +certoraRun certora/confs/MerkleMinter.conf --rule indexIsClaimedValueChange --prover_args -smt_bitVectorTheory true --msg "MerkleMinter indexIsClaimedValueChange" +# all the other rules can be verified using the default integer theory +# certoraRun certora/confs/MerkleMinter.conf --exclude_rule indexIsClaimedValueChange diff --git a/certora/specs/KatToken-exp2.spec b/certora/specs/KatToken-exp2.spec deleted file mode 100644 index 9b2ff7a..0000000 --- a/certora/specs/KatToken-exp2.spec +++ /dev/null @@ -1,25 +0,0 @@ -import "./exp2-summary.spec"; - -methods { - function inflationAdmin() external returns (address) envfree; - function inflationBeneficiary() external returns (address) envfree; - function inflationFactor() external returns (uint256) envfree; - function MAX_INFLATION() external returns (uint256) envfree; - function merkleMinter() external returns (address) envfree; - function mintCapacity(address) external returns (uint256) envfree; -} - -rule nonTrivialDistributeInflation() { - env e; - - // enforce non-trivial inflation - require(inflationFactor() > MAX_INFLATION() / 2); - require(inflationFactor() < MAX_INFLATION()); - - uint256 capacityBefore = mintCapacity(inflationBeneficiary()); - - distributeInflation(e); - - uint256 capacityAfter = mintCapacity(inflationBeneficiary()); - satisfy(capacityAfter > capacityBefore); -} \ No newline at end of file diff --git a/certora/specs/KatToken-simple.spec b/certora/specs/KatToken.spec similarity index 61% rename from certora/specs/KatToken-simple.spec rename to certora/specs/KatToken.spec index b7a6490..dcf83e7 100644 --- a/certora/specs/KatToken-simple.spec +++ b/certora/specs/KatToken.spec @@ -2,7 +2,9 @@ import "./exp2-summary.spec"; methods { function inflationAdmin() external returns (address) envfree; + function pendingInflationAdmin() external returns (address) envfree; function inflationBeneficiary() external returns (address) envfree; + function pendingInflationBeneficiary() external returns (address) envfree; function inflationFactor() external returns (uint256) envfree; function MAX_INFLATION() external returns (uint256) envfree; function merkleMinter() external returns (address) envfree; @@ -16,7 +18,7 @@ methods { => _mintCVL(to, amount); //MerkleProof - function _.verify(bytes32[] memory, bytes32, bytes32) external => NONDET DELETE; + function _.verify(bytes32[], bytes32, bytes32) external => NONDET DELETE; function _.eip712Domain() external => NONDET DELETE; } @@ -26,10 +28,9 @@ rule integrityOfchangeInflationAdmin(env e) { address newOwner; changeInflationAdmin(e, newOwner); - acceptInflationAdmin(e); assert(e.msg.sender == oldOwner); - assert(inflationAdmin() == newOwner); + assert(pendingInflationAdmin() == newOwner); } rule integrityOfchangeInflationBeneficiary(env e) { @@ -39,10 +40,10 @@ rule integrityOfchangeInflationBeneficiary(env e) { changeInflationBeneficiary(e, newOwner); assert(e.msg.sender == oldOwner); - assert(inflationBeneficiary() == newOwner); + assert(pendingInflationBeneficiary() == newOwner); } -rule lastMintCapacityIncreaseDeverDecreases(env e, method f) +rule lastMintCapacityIncreaseNeverDecreases(env e, method f) { uint256 lastMintCapacityIncrease_pre = get_lastMintCapacityIncrease(); @@ -52,7 +53,7 @@ rule lastMintCapacityIncreaseDeverDecreases(env e, method f) assert lastMintCapacityIncrease_post >= lastMintCapacityIncrease_pre; } -rule distributedSupplyCapDeverDecreases(env e, method f) +rule distributedSupplyCapNeverDecreases(env e, method f) { uint256 distributedSupplyCap_pre = get_distributedSupplyCap(); @@ -62,8 +63,7 @@ rule distributedSupplyCapDeverDecreases(env e, method f) assert distributedSupplyCap_post >= distributedSupplyCap_pre; } -rule canOnlySendAvailableMintCapacity() { - env e; +rule integrityOfDistributeMintCapacity(env e) { address to; uint256 amount; @@ -72,7 +72,6 @@ rule canOnlySendAvailableMintCapacity() { distributeMintCapacity(e, to, amount); - uint256 ownCapacityAfter = mintCapacity(e.msg.sender); uint256 toCapacityAfter = mintCapacity(to); @@ -118,3 +117,52 @@ rule mintCapacityPlusMintedEqualsDistributedSupplyCap(env e, method f) assert distributedSupplyCap_post - distributedSupplyCap_pre == totalMintedChange + totalMintCapacityChange; } + +/** + * The inflation factor is bounded by MAX_INFLATION. + */ +invariant inflationFactorIsBounded() + inflationFactor() <= MAX_INFLATION(); + +rule changeInflation_revertConditions(env e) +{ + uint256 value; + changeInflation@withrevert(e, value); + bool reverted = lastReverted; + assert lastReverted => + e.msg.sender != inflationAdmin() || + e.msg.value != 0 || + value > MAX_INFLATION(); +} + +// once renounceInflationAdmin is performed, the inflationAdmin will always be zero +// we've proved that renounceInflationAdmin changes it to zero so here we just prove +// that it cannot change from 0 to non-zero +rule inflationAdminValueChange(env e, method f) +{ + address admin_pre = inflationAdmin(); + require e.msg.sender != 0; + calldataarg args; + f(e, args); + address admin_post = inflationAdmin(); + assert admin_pre == 0 => admin_post == 0; +} + +// once renounceInflationBeneficiary is performed, the inflationBeneficiary will always be zero +// we've proved that renounceInflationBeneficiary changes it to zero so here we just prove +// that it cannot change from 0 to non-zero +rule inflationBeneficiaryValueChange(env e, method f) +{ + address beneficiary_pre = inflationBeneficiary(); + require e.msg.sender != 0; + calldataarg args; + f(e, args); + address beneficiary_post = inflationBeneficiary(); + assert beneficiary_pre == 0 => beneficiary_post == 0; +} + +invariant mintCapacityOfZeroIsZero() + mintCapacity(0) == 0 + { preserved + with (env e) { require e.msg.sender != 0; } + } \ No newline at end of file diff --git a/certora/specs/exp2-implementation.spec b/certora/specs/powUtil.spec similarity index 94% rename from certora/specs/exp2-implementation.spec rename to certora/specs/powUtil.spec index a9a9117..eddde0d 100644 --- a/certora/specs/exp2-implementation.spec +++ b/certora/specs/powUtil.spec @@ -13,7 +13,7 @@ methods { } definition ONE18() returns uint256 = 1000000000000000000; -definition days(uint256 d) returns uint256 = assert_uint256(d * 60 * 60 * 24); +definition daysToSeconds(uint256 days) returns uint256 = assert_uint256(days * 60 * 60 * 24); /** * Show that exp2 is actually exact for some easy values. @@ -84,8 +84,8 @@ rule exp2_noOverflow() { // let's assume that we can't have more than 100 years of inflation uint256 timeElapsed; - require(timeElapsed <= 100 * days(365)); - uint256 x = assert_uint256((inflationFactor * timeElapsed) / days(365)); + require(timeElapsed <= 100 * daysToSeconds(365)); + uint256 x = assert_uint256((inflationFactor * timeElapsed) / daysToSeconds(365)); // that means x can't be more than 5 assert(x < 5 * ONE18()); diff --git a/certora/specs/sanity.spec b/certora/specs/sanity.spec deleted file mode 100644 index 6b20af0..0000000 --- a/certora/specs/sanity.spec +++ /dev/null @@ -1 +0,0 @@ -use builtin rule sanity filtered { f -> f.contract == currentContract } From 55d4d9c556d1914e52c6e65149838b1b2cd1a43b Mon Sep 17 00:00:00 2001 From: Otakar Date: Thu, 20 Mar 2025 08:46:37 +0100 Subject: [PATCH 33/37] MerkleMinter rules + conf --- certora/confs/MerkleMinter.conf | 1 + certora/notes.txt | 28 +++++++++++++++------------- certora/scripts/run.sh | 4 ++-- certora/specs/KatToken.spec | 20 ++++++++++++++++++++ certora/specs/MerkleMinter.spec | 23 ++++++++++++++++++++++- 5 files changed, 60 insertions(+), 16 deletions(-) diff --git a/certora/confs/MerkleMinter.conf b/certora/confs/MerkleMinter.conf index 5797184..8bb02a7 100644 --- a/certora/confs/MerkleMinter.conf +++ b/certora/confs/MerkleMinter.conf @@ -10,6 +10,7 @@ "link": [ "MerkleMinter:katToken=KatToken" ], + "parametric_contracts": [ "MerkleMinter" ], "msg": "MerkleMinter", "packages": [ "@openzeppelin/merkle-tree=node_modules/@openzeppelin/merkle-tree", diff --git a/certora/notes.txt b/certora/notes.txt index cb78388..f721c42 100644 --- a/certora/notes.txt +++ b/certora/notes.txt @@ -46,25 +46,29 @@ claimKatToken will increase receiver's balance when executed successfully once active, the protocol will not go to an inactive state, i.e., (block.timestamp > unlockTime || !locked) can only change false -> true indexIsClaimed(index) can only change false -> true indexIsClaimed(index) == true => claimKatToken(..,index) will revert +init cannot be called after the minter is unlocked i.e., after ((block.timestamp > unlockTime) || !locked) +It should not be possible to permanently renounce the rootSetter role without actually setting the root first ---------------- katToken: only certain methods may increase/decrease total mint capacity -total mint capacity + mintedTokens can only increase -lastMintCapacityIncrease can only increase -distributedSupplyCap can only increase -distributedSupplyCap == total mint capacity + mintedTokens -for all x: mintCapacity[x] <= distributedSupplyCap -mintCapacity of address(0) is always 0 -inflation <= MAX_INFLATION -inflation can be set to any value <= MAX_INFLATION +total mint capacity + mintedTokens can only increase w +lastMintCapacityIncrease can only increase w +distributedSupplyCap can only increase w +distributedSupplyCap == total mint capacity + mintedTokens w +for all x: mintCapacity[x] <= distributedSupplyCap xx +mintCapacity of address(0) is always 0 w +inflation <= MAX_INFLATION w +inflation can be set to any value <= MAX_INFLATION w once renounceInflationAdmin is performed, the inflationAdmin will always be zero 1. show that renounceInflationAdmin sets inflationAdmin to 0 - 2. show that inflationAdmin can never change from 0 to non-zero + 2. show that inflationAdmin can never change from 0 to non-zero w the same for inflationBeneficiary -only inflationBeneficiary can change inflationBeneficiary -only inflationAdmin can change inflationAdmin + 1. show that renounceInflationAdmin sets inflationBeneficiary to 0 + 2. show that inflationBeneficiary can never change from 0 to non-zero w +only inflationBeneficiary can change inflationBeneficiary w +only inflationAdmin can change inflationAdmin w ---------------- more properties: @@ -75,8 +79,6 @@ can we write a rule that shows that all values within range must succeed? given any of the privileged addresses (KatToken.inflationAdmin, KatToken.inflationBeneficiary, MerkleMinter.rootSetter), once the corresponding renounce function is called, the given privileged address must remain address(0) indefinitely -mintCapacity of address(0) is always 0 ..? - mutations..?? any more properties? diff --git a/certora/scripts/run.sh b/certora/scripts/run.sh index c763b8d..23f247d 100755 --- a/certora/scripts/run.sh +++ b/certora/scripts/run.sh @@ -5,6 +5,6 @@ # the rule indexIsClaimedValueChange requires using bitVector theory -certoraRun certora/confs/MerkleMinter.conf --rule indexIsClaimedValueChange --prover_args -smt_bitVectorTheory true --msg "MerkleMinter indexIsClaimedValueChange" +# certoraRun certora/confs/MerkleMinter.conf --rule indexIsClaimedValueChange --prover_args -smt_bitVectorTheory true --msg "MerkleMinter indexIsClaimedValueChange" # all the other rules can be verified using the default integer theory -# certoraRun certora/confs/MerkleMinter.conf --exclude_rule indexIsClaimedValueChange +certoraRun certora/confs/MerkleMinter.conf --exclude_rule indexIsClaimedValueChange diff --git a/certora/specs/KatToken.spec b/certora/specs/KatToken.spec index dcf83e7..f71e99f 100644 --- a/certora/specs/KatToken.spec +++ b/certora/specs/KatToken.spec @@ -135,6 +135,26 @@ rule changeInflation_revertConditions(env e) value > MAX_INFLATION(); } +rule integrityOfRenounceInflationAdmin(env e, method f) +{ + address admin_pre = inflationAdmin(); + renounceInflationAdmin(e); + address admin_post = inflationAdmin(); + + assert admin_pre == e.msg.sender; + assert admin_post == 0; +} + +rule integrityOfRenounceInflationBeneficiary(env e, method f) +{ + address beneficiary_pre = inflationBeneficiary(); + renounceInflationBeneficiary(e); + address beneficiary_post = inflationBeneficiary(); + + assert beneficiary_pre == e.msg.sender; + assert beneficiary_post == 0; +} + // once renounceInflationAdmin is performed, the inflationAdmin will always be zero // we've proved that renounceInflationAdmin changes it to zero so here we just prove // that it cannot change from 0 to non-zero diff --git a/certora/specs/MerkleMinter.spec b/certora/specs/MerkleMinter.spec index 4daa258..9ccfc5c 100644 --- a/certora/specs/MerkleMinter.spec +++ b/certora/specs/MerkleMinter.spec @@ -120,4 +120,25 @@ rule cannotClaimTheIndexTwice(env e) bool reverted = lastReverted; assert isClaimed => reverted; -} \ No newline at end of file +} + +// init cannot be called after the minter is unlocked i.e., after ((block.timestamp > unlockTime) || !locked) +// otherwise some claims could already have happened with a different root +rule cannotInitAfterUnlocked(env e) +{ + bool active = (e.block.timestamp > unlockTime()) || !locked(); + + bytes32 _root; + address _katToken; + init(e, _root, _katToken); + assert !active; // if active, we shouldn't get here as the method shoud revert +} + +// It should not be possible to permanently renounce the rootSetter role without actually setting the root first +// We showed that rootSetter cannot change from address(0) to non-zero, +// so here we just prove that it's not possible to have rootSetter == 0 && root == 0 +invariant rootCanAlwaysBeSet() + !(rootSetter() == 0 && root() == to_bytes32(0)) + { preserved + with (env e) { require e.msg.sender != 0; } + } \ No newline at end of file From 38b2fe6bdbf0e2f06ecf184594d9a98b1d5ea3b1 Mon Sep 17 00:00:00 2001 From: Otakar Date: Mon, 24 Mar 2025 08:40:26 +0100 Subject: [PATCH 34/37] More rules, cleanup --- certora/confs/KatToken-exp2.conf | 20 ------ certora/confs/MerkleMinter.conf | 2 +- certora/confs/exp2-check-summary.conf | 20 ------ certora/confs/powUtil.conf | 2 +- certora/confs/sanity-KatToken.conf | 27 -------- certora/confs/sanity-MerkleMinter.conf | 31 --------- certora/notes.txt | 11 +++- certora/scripts/run.sh | 6 +- certora/specs/KatToken.spec | 2 +- certora/specs/MerkleMinter.spec | 28 +++++++- certora/specs/exp2-check.spec | 89 -------------------------- certora/specs/exp2-summary.spec | 56 ++++++++-------- certora/specs/powUtil.spec | 60 +++++++---------- 13 files changed, 93 insertions(+), 261 deletions(-) delete mode 100644 certora/confs/KatToken-exp2.conf delete mode 100644 certora/confs/exp2-check-summary.conf delete mode 100644 certora/confs/sanity-KatToken.conf delete mode 100644 certora/confs/sanity-MerkleMinter.conf delete mode 100644 certora/specs/exp2-check.spec diff --git a/certora/confs/KatToken-exp2.conf b/certora/confs/KatToken-exp2.conf deleted file mode 100644 index 7500b6d..0000000 --- a/certora/confs/KatToken-exp2.conf +++ /dev/null @@ -1,20 +0,0 @@ -{ - "assert_autofinder_success": true, - "files": [ - "src/KatToken.sol" - ], - "global_timeout": "7200", - "loop_iter": "2", - "optimistic_loop": true, - "msg": "KatToken simple", - "packages": [ - "@openzeppelin/merkle-tree=node_modules/@openzeppelin/merkle-tree", - "@openzeppelin-contracts-5.1.0=dependencies/@openzeppelin-contracts-5.1.0", - "forge-std-1.9.4=dependencies/forge-std-1.9.4" - ], - "process": "emv", - "server": "production", - "solc": "solc8.28", - "solc_via_ir": false, - "verify": "KatToken:certora/specs/KatToken-exp2.spec" -} \ No newline at end of file diff --git a/certora/confs/MerkleMinter.conf b/certora/confs/MerkleMinter.conf index 8bb02a7..855f984 100644 --- a/certora/confs/MerkleMinter.conf +++ b/certora/confs/MerkleMinter.conf @@ -10,7 +10,7 @@ "link": [ "MerkleMinter:katToken=KatToken" ], - "parametric_contracts": [ "MerkleMinter" ], + //"parametric_contracts": [ "MerkleMinter" ], "msg": "MerkleMinter", "packages": [ "@openzeppelin/merkle-tree=node_modules/@openzeppelin/merkle-tree", diff --git a/certora/confs/exp2-check-summary.conf b/certora/confs/exp2-check-summary.conf deleted file mode 100644 index 5df491c..0000000 --- a/certora/confs/exp2-check-summary.conf +++ /dev/null @@ -1,20 +0,0 @@ -{ - "assert_autofinder_success": true, - "files": [ - "certora/harnesses/PowUtilHarness.sol" - ], - "global_timeout": "7200", - "loop_iter": "2", - "optimistic_loop": true, - "msg": "Check exp2 summary", - "packages": [ - "@openzeppelin/merkle-tree=node_modules/@openzeppelin/merkle-tree", - "@openzeppelin-contracts-5.1.0=dependencies/@openzeppelin-contracts-5.1.0", - "forge-std-1.9.4=dependencies/forge-std-1.9.4" - ], - "process": "emv", - "server": "production", - "solc": "solc8.28", - "solc_via_ir": false, - "verify": "PowUtilHarness:certora/specs/exp2-check.spec" -} \ No newline at end of file diff --git a/certora/confs/powUtil.conf b/certora/confs/powUtil.conf index c3703a5..b9cf13d 100644 --- a/certora/confs/powUtil.conf +++ b/certora/confs/powUtil.conf @@ -19,5 +19,5 @@ "solc": "solc8.28", "solc_via_ir": false, "verify": "PowUtilHarness:certora/specs/powUtil.spec", - "msg": "Check exp2 BV", + "msg": "Check exp2", } \ No newline at end of file diff --git a/certora/confs/sanity-KatToken.conf b/certora/confs/sanity-KatToken.conf deleted file mode 100644 index 3ef5b4e..0000000 --- a/certora/confs/sanity-KatToken.conf +++ /dev/null @@ -1,27 +0,0 @@ -{ - "assert_autofinder_success": true, - "files": [ - "src/KatToken.sol" - ], - "global_timeout": "7200", - "loop_iter": "2", - "optimistic_loop": true, - "msg": "sanity KatToken", - "packages": [ - "@openzeppelin/merkle-tree=node_modules/@openzeppelin/merkle-tree", - "@openzeppelin-contracts-5.1.0=dependencies/@openzeppelin-contracts-5.1.0", - "forge-std-1.9.4=dependencies/forge-std-1.9.4" - ], - "process": "emv", - "prover_args": [ - "-verifyCache", - "-verifyTACDumps", - "-testMode", - "-checkRuleDigest", - "-callTraceHardFail on" - ], - "server": "production", - "solc": "solc8.28", - "solc_via_ir": false, - "verify": "KatToken:certora/specs/sanity.spec" -} \ No newline at end of file diff --git a/certora/confs/sanity-MerkleMinter.conf b/certora/confs/sanity-MerkleMinter.conf deleted file mode 100644 index cf5afdc..0000000 --- a/certora/confs/sanity-MerkleMinter.conf +++ /dev/null @@ -1,31 +0,0 @@ -{ - "assert_autofinder_success": true, - "files": [ - "src/MerkleMinter.sol", - "src/KatToken.sol" - ], - "global_timeout": "7200", - "loop_iter": "2", - "optimistic_loop": true, - "link": [ - "MerkleMinter:katToken=KatToken" - ], - "msg": "sanity MerkleMinter", - "packages": [ - "@openzeppelin/merkle-tree=node_modules/@openzeppelin/merkle-tree", - "@openzeppelin-contracts-5.1.0=dependencies/@openzeppelin-contracts-5.1.0", - "forge-std-1.9.4=dependencies/forge-std-1.9.4" - ], - "process": "emv", - "prover_args": [ - "-verifyCache", - "-verifyTACDumps", - "-testMode", - "-checkRuleDigest", - "-callTraceHardFail on" - ], - "server": "production", - "solc": "solc8.28", - "solc_via_ir": false, - "verify": "MerkleMinter:certora/specs/sanity.spec" -} \ No newline at end of file diff --git a/certora/notes.txt b/certora/notes.txt index f721c42..7f00f9c 100644 --- a/certora/notes.txt +++ b/certora/notes.txt @@ -60,7 +60,11 @@ distributedSupplyCap == total mint capacity + mintedTokens for all x: mintCapacity[x] <= distributedSupplyCap xx mintCapacity of address(0) is always 0 w inflation <= MAX_INFLATION w -inflation can be set to any value <= MAX_INFLATION w +inflation can be set to any value <= MAX_INFLATION + if value <= MAX_INFLATION then "satisfy" inflation == value + forall v satisfy + + w once renounceInflationAdmin is performed, the inflationAdmin will always be zero 1. show that renounceInflationAdmin sets inflationAdmin to 0 2. show that inflationAdmin can never change from 0 to non-zero w @@ -86,3 +90,8 @@ any more properties? 1000 year inflation -> 5e18, maybe use 10e18 instead . use this: 43e18 minimum arg to exp2 is about 6M but not a multiplier of it + + +during the handover + +show a simple but powerful rule, show mutation diff --git a/certora/scripts/run.sh b/certora/scripts/run.sh index 23f247d..c61b083 100755 --- a/certora/scripts/run.sh +++ b/certora/scripts/run.sh @@ -1,10 +1,10 @@ -# certoraRun certora/confs/KatToken.conf +certoraRun certora/confs/KatToken.conf -# certoraRun certora/confs/powUtil.conf --rule exp2_monotonePlus01 +# certoraRun certora/confs/powUtil.conf --rule exp2_additivity2X --msg exp2_additivity2X # certoraRun certora/confs/powUtil.conf # the rule indexIsClaimedValueChange requires using bitVector theory -# certoraRun certora/confs/MerkleMinter.conf --rule indexIsClaimedValueChange --prover_args -smt_bitVectorTheory true --msg "MerkleMinter indexIsClaimedValueChange" +certoraRun certora/confs/MerkleMinter.conf --rule indexIsClaimedValueChange --prover_args -smt_bitVectorTheory true --msg "MerkleMinter indexIsClaimedValueChange" # all the other rules can be verified using the default integer theory certoraRun certora/confs/MerkleMinter.conf --exclude_rule indexIsClaimedValueChange diff --git a/certora/specs/KatToken.spec b/certora/specs/KatToken.spec index f71e99f..dafa0b2 100644 --- a/certora/specs/KatToken.spec +++ b/certora/specs/KatToken.spec @@ -129,7 +129,7 @@ rule changeInflation_revertConditions(env e) uint256 value; changeInflation@withrevert(e, value); bool reverted = lastReverted; - assert lastReverted => + assert reverted => e.msg.sender != inflationAdmin() || e.msg.value != 0 || value > MAX_INFLATION(); diff --git a/certora/specs/MerkleMinter.spec b/certora/specs/MerkleMinter.spec index 9ccfc5c..29ffe11 100644 --- a/certora/specs/MerkleMinter.spec +++ b/certora/specs/MerkleMinter.spec @@ -134,9 +134,35 @@ rule cannotInitAfterUnlocked(env e) assert !active; // if active, we shouldn't get here as the method shoud revert } +rule cannotChangeRootWhenRootSetterIsZero(env e, method f) +{ + bytes32 root_pre = root(); + address rootSetter_pre = rootSetter(); + require e.msg.sender != 0; + calldataarg args; + f(e, args); + bytes32 root_post = root(); + + assert rootSetter_pre == 0 => root_post == root_pre; +} + +rule rootCanBeChanged(env e) +{ + bytes32 root_pre = root(); + bytes32 _root; address _katToken; + init(e, _root, _katToken); + + bytes32 root_post = root(); + satisfy root_pre != root_post; +} + // It should not be possible to permanently renounce the rootSetter role without actually setting the root first -// We showed that rootSetter cannot change from address(0) to non-zero, +// We showed that +// 1. root can be changed +// 2. root root cannot change when rootSetter == address(0) +// 3. rootSetter cannot change from address(0) to non-zero, // so here we just prove that it's not possible to have rootSetter == 0 && root == 0 +// that would already indicate an unrecoverable state invariant rootCanAlwaysBeSet() !(rootSetter() == 0 && root() == to_bytes32(0)) { preserved diff --git a/certora/specs/exp2-check.spec b/certora/specs/exp2-check.spec deleted file mode 100644 index 43ad219..0000000 --- a/certora/specs/exp2-check.spec +++ /dev/null @@ -1,89 +0,0 @@ -import "./exp2-summary.spec"; - -// Does some sanity checks on the exp2 summarization. - -methods { - function exp2(uint256 x) external returns (uint256) envfree; -} - -function maybeEqual(mathint x, mathint res) { - uint256 e = exp2(assert_uint256(x)); - satisfy(99 * e < 100 * res && 101 * e > 100 * res); -} - -rule exp2Consts() { - maybeEqual(0*ONE18(), ONE18()); - maybeEqual(1*ONE18(), 2*ONE18()); - maybeEqual(2*ONE18(), 4*ONE18()); - maybeEqual(3*ONE18(), 8*ONE18()); - maybeEqual(4*ONE18(), 16*ONE18()); - maybeEqual(5*ONE18(), 32*ONE18()); - maybeEqual(6*ONE18(), 64*ONE18()); -} - -rule exp2Monotonicity() { - uint256 x; - uint256 y; - // weak monotonicity - assert((x < y) => (exp2(x) <= exp2(y))); -} - -function lowerBound(mathint x, mathint res) { - mathint e = exp2(assert_uint256(x)); - assert(10 * e >= 9*res); -} - -rule exp2LowerBound() { - lowerBound(0*ONE18(), ONE18()); - lowerBound(1*ONE18(), 2*ONE18()); - lowerBound(2*ONE18(), 4*ONE18()); - lowerBound(3*ONE18(), 8*ONE18()); - lowerBound(4*ONE18(), 16*ONE18()); - lowerBound(5*ONE18(), 32*ONE18()); - lowerBound(6*ONE18(), 64*ONE18()); - lowerBound(7*ONE18(), 128*ONE18()); - lowerBound(8*ONE18(), 256*ONE18()); - lowerBound(9*ONE18(), 512*ONE18()); - lowerBound(10*ONE18(), 1024*ONE18()); - - lowerBound(1*ONE18()/2, ONE18()* 14142 / 10000); - lowerBound(3*ONE18()/2, ONE18()* 28284 / 10000); - lowerBound(5*ONE18()/2, ONE18()* 56569 / 10000); - lowerBound(7*ONE18()/2, ONE18()* 113137 / 10000); - lowerBound(9*ONE18()/2, ONE18()* 226274 / 10000); - lowerBound(11*ONE18()/2, ONE18()* 452548 / 10000); - lowerBound(13*ONE18()/2, ONE18()* 905097 / 10000); - lowerBound(15*ONE18()/2, ONE18()* 1810193 / 10000); - lowerBound(17*ONE18()/2, ONE18()* 3620387 / 10000); - lowerBound(19*ONE18()/2, ONE18()* 7240773 / 10000); -} - -function upperBound(mathint x, mathint res) { - mathint e = exp2(assert_uint256(x)); - assert(4 * e <= 5*res); -} - -rule exp2UpperBound() { - upperBound(0*ONE18(), ONE18()); - upperBound(1*ONE18(), 2*ONE18()); - upperBound(2*ONE18(), 4*ONE18()); - upperBound(3*ONE18(), 8*ONE18()); - upperBound(4*ONE18(), 16*ONE18()); - upperBound(5*ONE18(), 32*ONE18()); - upperBound(6*ONE18(), 64*ONE18()); - upperBound(7*ONE18(), 128*ONE18()); - upperBound(8*ONE18(), 256*ONE18()); - upperBound(9*ONE18(), 512*ONE18()); - upperBound(10*ONE18(), 1024*ONE18()); - - upperBound(1*ONE18()/2, ONE18()* 14142 / 10000); - upperBound(3*ONE18()/2, ONE18()* 28284 / 10000); - upperBound(5*ONE18()/2, ONE18()* 56569 / 10000); - upperBound(7*ONE18()/2, ONE18()* 113137 / 10000); - upperBound(9*ONE18()/2, ONE18()* 226274 / 10000); - upperBound(11*ONE18()/2, ONE18()* 452548 / 10000); - upperBound(13*ONE18()/2, ONE18()* 905097 / 10000); - upperBound(15*ONE18()/2, ONE18()* 1810193 / 10000); - upperBound(17*ONE18()/2, ONE18()* 3620387 / 10000); - upperBound(19*ONE18()/2, ONE18()* 7240773 / 10000); -} diff --git a/certora/specs/exp2-summary.spec b/certora/specs/exp2-summary.spec index 56ff60e..5cc841f 100644 --- a/certora/specs/exp2-summary.spec +++ b/certora/specs/exp2-summary.spec @@ -29,35 +29,35 @@ ghost ghostExp2(mathint) returns uint256 { axiom forall uint256 x. x <= ONE18() => ghostExp2(x) <= 2*ONE18(); - // lower bound - axiom forall uint256 x. - ((x >= 0 && x < 2*ONE18()) => ( - ghostExp2(x) >= - ONE18() - + x * Log2() / ONE18() - + x*x * Log2()*Log2() / ONE18()/ONE18()/ONE18() / 2 - + x*x*x * Log2()*Log2()*Log2() /ONE18()/ONE18()/ONE18()/ONE18()/ONE18() / 6 - )) && - ((x >= 2*ONE18() && x < 4*ONE18()) => (ghostExp2(x) >= ghostExp2(x - 2*ONE18()) * 4)) && - ((x >= 4*ONE18() && x < 6*ONE18()) => (ghostExp2(x) >= ghostExp2(x - 4*ONE18()) * 16)) && - ((x >= 6*ONE18() && x < 8*ONE18()) => (ghostExp2(x) >= ghostExp2(x - 6*ONE18()) * 64)) && - ((x >= 8*ONE18()) => (ghostExp2(x) >= ghostExp2(x - 8*ONE18()) * 256)) - ; + // // lower bound + // axiom forall uint256 x. + // ((x >= 0 && x < 2*ONE18()) => ( + // ghostExp2(x) >= + // ONE18() + // + x * Log2() / ONE18() + // + x*x * Log2()*Log2() / ONE18()/ONE18()/ONE18() / 2 + // + x*x*x * Log2()*Log2()*Log2() /ONE18()/ONE18()/ONE18()/ONE18()/ONE18() / 6 + // )) && + // ((x >= 2*ONE18() && x < 4*ONE18()) => (ghostExp2(x) >= ghostExp2(x - 2*ONE18()) * 4)) && + // ((x >= 4*ONE18() && x < 6*ONE18()) => (ghostExp2(x) >= ghostExp2(x - 4*ONE18()) * 16)) && + // ((x >= 6*ONE18() && x < 8*ONE18()) => (ghostExp2(x) >= ghostExp2(x - 6*ONE18()) * 64)) && + // ((x >= 8*ONE18()) => (ghostExp2(x) >= ghostExp2(x - 8*ONE18()) * 256)) + // ; - // upper bound - axiom forall uint256 x. - ((x >= 0 && x < 2*ONE18()) => ( - ghostExp2(x) <= - 4*ONE18()/3 // rough estimate: this approximation at 2 is about 0.21 to low - + x * Log2() / ONE18() - + x*x * Log2()*Log2() / ONE18()/ONE18()/ONE18() / 2 - + x*x*x * Log2()*Log2()*Log2() /ONE18()/ONE18()/ONE18()/ONE18()/ONE18() / 6 - )) && - ((x >= 2*ONE18() && x < 4*ONE18()) => (ghostExp2(x) <= ghostExp2(x - 2*ONE18()) * 4)) && - ((x >= 4*ONE18() && x < 6*ONE18()) => (ghostExp2(x) <= ghostExp2(x - 4*ONE18()) * 16)) && - ((x >= 6*ONE18() && x < 8*ONE18()) => (ghostExp2(x) <= ghostExp2(x - 6*ONE18()) * 64)) && - ((x >= 8*ONE18()) => (ghostExp2(x) <= ghostExp2(x - 8*ONE18()) * 256)) - ; + // // upper bound + // axiom forall uint256 x. + // ((x >= 0 && x < 2*ONE18()) => ( + // ghostExp2(x) <= + // 4*ONE18()/3 // rough estimate: this approximation at 2 is about 0.21 to low + // + x * Log2() / ONE18() + // + x*x * Log2()*Log2() / ONE18()/ONE18()/ONE18() / 2 + // + x*x*x * Log2()*Log2()*Log2() /ONE18()/ONE18()/ONE18()/ONE18()/ONE18() / 6 + // )) && + // ((x >= 2*ONE18() && x < 4*ONE18()) => (ghostExp2(x) <= ghostExp2(x - 2*ONE18()) * 4)) && + // ((x >= 4*ONE18() && x < 6*ONE18()) => (ghostExp2(x) <= ghostExp2(x - 4*ONE18()) * 16)) && + // ((x >= 6*ONE18() && x < 8*ONE18()) => (ghostExp2(x) <= ghostExp2(x - 6*ONE18()) * 64)) && + // ((x >= 8*ONE18()) => (ghostExp2(x) <= ghostExp2(x - 8*ONE18()) * 256)) + // ; } function cvlExp2(uint256 x) returns uint256 { diff --git a/certora/specs/powUtil.spec b/certora/specs/powUtil.spec index eddde0d..28220b0 100644 --- a/certora/specs/powUtil.spec +++ b/certora/specs/powUtil.spec @@ -72,46 +72,30 @@ rule exp2_monotone12(env e) assert x < y => exp2(x) <= exp2(y); } -/** - * Show that exp2 can not overflow within 100 years. - * Technically, we show that exp2 stays below 0x100000000000000000, which is - * well below anything close to an overflow. - */ -rule exp2_noOverflow() { - // we know that the inflation factor is bounded by MAX_INFLATION - uint256 inflationFactor = KatToken.inflationFactor(); - require inflationFactor() <= MAX_INFLATION(); - - // let's assume that we can't have more than 100 years of inflation - uint256 timeElapsed; - require(timeElapsed <= 100 * daysToSeconds(365)); - uint256 x = assert_uint256((inflationFactor * timeElapsed) / daysToSeconds(365)); - - // that means x can't be more than 5 - assert(x < 5 * ONE18()); - - // this is well below anything that might overflow ... - assert(exp2(x) < 32 * ONE18() && 32 * ONE18() < 0x100000000000000000); - // ... but the upper bound is reasonably tight - satisfy(exp2(x) > 16 * ONE18()); -} - -// monotonicity -// try x vs. x+1 -// x vs. 2*x - -// rules for interest -// interest for timespan x, vs. interest vs. 2*x +rule exp2_monotonicityX(env e) +{ + uint256 MIN_INFLATION = 1441974173906322; // log2(1.001) + uint256 MAX_INFLATION = 42644337408493690; // log2(1.03) + uint secondsPerYear = (365 *24 *60 *60); + uint256 minDifference = require_uint256(MIN_INFLATION / secondsPerYear); -// inject mutations, demontrate to the customers the bug founding to the customer + uint256 inflFactor; uint256 timeElapsed; + require inflFactor >= MIN_INFLATION && inflFactor <= MAX_INFLATION; + require timeElapsed <= 7 *24 *60 *60; //one week + uint256 input = require_uint256(inflFactor * timeElapsed / secondsPerYear); + assert exp2(input) <= exp2(require_uint256(input + minDifference)); +} -// "imperminent loss" - concept related to AMM -// liquidity provider provides L, takes fees -// +function withinTenPercentTolerance(mathint a, mathint b) returns bool +{ + return 9*a <= 10*b && 9*b <= 10*a; +} -// DEFI lama -// tells what kind of protocols, overview of all protocols -// +rule exp2_additivity2X() { + uint256 x; uint256 total; + require total == x + x; + require total <= 5*ONE18(); -// 10 tokens per year is an acceptable error for the inflation + assert withinTenPercentTolerance(exp2(total)*ONE18(), exp2(x) * exp2(x)); +} From aab98584e6d8079ad9f333a3334890cb4bc4a4cd Mon Sep 17 00:00:00 2001 From: Otakar Date: Mon, 24 Mar 2025 11:21:27 +0100 Subject: [PATCH 35/37] gitattributes added --- certora/.gitattributes | 3 +++ certora/scripts/run.sh | 2 +- 2 files changed, 4 insertions(+), 1 deletion(-) create mode 100644 certora/.gitattributes diff --git a/certora/.gitattributes b/certora/.gitattributes new file mode 100644 index 0000000..4dccbf9 --- /dev/null +++ b/certora/.gitattributes @@ -0,0 +1,3 @@ +*.spec linguist-language=Solidity +*.conf linguist-detectable +*.conf linguist-language=JSON5 \ No newline at end of file diff --git a/certora/scripts/run.sh b/certora/scripts/run.sh index c61b083..f87b56b 100755 --- a/certora/scripts/run.sh +++ b/certora/scripts/run.sh @@ -7,4 +7,4 @@ certoraRun certora/confs/KatToken.conf # the rule indexIsClaimedValueChange requires using bitVector theory certoraRun certora/confs/MerkleMinter.conf --rule indexIsClaimedValueChange --prover_args -smt_bitVectorTheory true --msg "MerkleMinter indexIsClaimedValueChange" # all the other rules can be verified using the default integer theory -certoraRun certora/confs/MerkleMinter.conf --exclude_rule indexIsClaimedValueChange +certoraRun certora/confs/MerkleMinter.conf --exclude_rule indexIsClaimedValueChange \ No newline at end of file From a4da50edcc4908206d0bdede75f6650ec609163e Mon Sep 17 00:00:00 2001 From: Otakar Date: Tue, 25 Mar 2025 17:58:02 +0100 Subject: [PATCH 36/37] Rules adjusted + more rules --- certora/specs/KatToken.spec | 43 ++++++++++++++++++++++++++----------- 1 file changed, 31 insertions(+), 12 deletions(-) diff --git a/certora/specs/KatToken.spec b/certora/specs/KatToken.spec index dafa0b2..c749d2e 100644 --- a/certora/specs/KatToken.spec +++ b/certora/specs/KatToken.spec @@ -124,17 +124,6 @@ rule mintCapacityPlusMintedEqualsDistributedSupplyCap(env e, method f) invariant inflationFactorIsBounded() inflationFactor() <= MAX_INFLATION(); -rule changeInflation_revertConditions(env e) -{ - uint256 value; - changeInflation@withrevert(e, value); - bool reverted = lastReverted; - assert reverted => - e.msg.sender != inflationAdmin() || - e.msg.value != 0 || - value > MAX_INFLATION(); -} - rule integrityOfRenounceInflationAdmin(env e, method f) { address admin_pre = inflationAdmin(); @@ -160,6 +149,7 @@ rule integrityOfRenounceInflationBeneficiary(env e, method f) // that it cannot change from 0 to non-zero rule inflationAdminValueChange(env e, method f) { + requireInvariant zeroAdminThenZeroPendingAdmin(); address admin_pre = inflationAdmin(); require e.msg.sender != 0; calldataarg args; @@ -173,6 +163,7 @@ rule inflationAdminValueChange(env e, method f) // that it cannot change from 0 to non-zero rule inflationBeneficiaryValueChange(env e, method f) { + requireInvariant zeroBeneficiaryThenZeroPendingBeneficiary(); address beneficiary_pre = inflationBeneficiary(); require e.msg.sender != 0; calldataarg args; @@ -184,5 +175,33 @@ rule inflationBeneficiaryValueChange(env e, method f) invariant mintCapacityOfZeroIsZero() mintCapacity(0) == 0 { preserved - with (env e) { require e.msg.sender != 0; } + with (env e) + { + requireInvariant noBeneficiaryThenNoInflation(); + require e.msg.sender != 0; + } + } + +invariant noBeneficiaryThenNoInflation() + inflationBeneficiary() == 0 => inflationFactor() == 0 + { preserved with (env e) + { + require e.msg.sender != 0; + } + } + +invariant zeroAdminThenZeroPendingAdmin() + inflationAdmin() == 0 => pendingInflationAdmin() == 0 + { preserved with (env e) + { + require e.msg.sender != 0; + } + } + +invariant zeroBeneficiaryThenZeroPendingBeneficiary() + inflationBeneficiary() == 0 => pendingInflationBeneficiary() == 0 + { preserved with (env e) + { + require e.msg.sender != 0; + } } \ No newline at end of file From be768587b44f8b92f6091dc8faafb09fc31dea65 Mon Sep 17 00:00:00 2001 From: Otakar Date: Tue, 25 Mar 2025 17:59:05 +0100 Subject: [PATCH 37/37] ChangeInflation_revertConditions moved to a separate file using a stronger summary --- certora/notes.txt | 97 --------------------- certora/scripts/run.sh | 1 + certora/specs/KatToken_changeInflation.spec | 43 +++++++++ certora/specs/exp2-summary.spec | 30 ------- certora/specs/exp2-summary_stronger.spec | 62 +++++++++++++ 5 files changed, 106 insertions(+), 127 deletions(-) delete mode 100644 certora/notes.txt create mode 100644 certora/specs/KatToken_changeInflation.spec create mode 100644 certora/specs/exp2-summary_stronger.spec diff --git a/certora/notes.txt b/certora/notes.txt deleted file mode 100644 index 7f00f9c..0000000 --- a/certora/notes.txt +++ /dev/null @@ -1,97 +0,0 @@ - -// questions / observations: -MerkleMinter.claimKatToken can be called with amount = 0 -KatToken.distributeInflation: wouldn't it be better to add a check block.timestamp > lastMintCapacityIncrease at the beginning to save execution of the other commands? -KatToken.distributeMintCapacity are the checks on lines 200 and 201 needed? -KatToken.distributeMintCapacity can we use unchecked instead? -KatToken: line 170 can't we have >= instead of > ? -inflationBeneficiary and inflationAdmin: wouldn't it be better to use the existing Ownable interface? - - the new owner cannot decline - - it can change to the same value -there's no check that merkleMinter is actually a MerkleMinter contract - ----------------------------------- - -more questions: - -L/info finding: -the MerkleMinter.init function is very dangerous because the operation can only work if the new tree respects the same indexes (i.e. append-only), which is a very strict requirement for off-chain components. -Otherwise, there’s risk of one claiming twice if their claim is available under different indexes before and after the root update - - -L/info finding (this was discussed during the call with the team) KatToken.renounceInflationBeneficiary can be called when inflationFactor is non-zero. This will grant mint capacity to address(0) which is certainly unwanted. Fix is to require (or overwrite) inflationFactor to be zero when the inflationBeneficiary is reset -WHY IS IT A PROBLEM? - - -// properties: ----------------- -Powutil: - -exp2(x) == 2^x , formally: exp2(x *1e18) == 2^x *1e18 -exp2(x+y) == exp2(x)*exp2(y) , formally: exp2(x+y) *1e18 == exp2(x)*exp2(y) -exp2(x) <= exp2(x+1) -lower and upper bounds: LB(x) <= exp2(x) <= UB(x) currently we're using bounds based on 3rd-order Taylor expansions - + more variants of these. With error bounds, etc. - ----------------- -merkleminter: - -katToken and root can only change via init -locked can only change from true -> false -rootSetter can only change from x -> 0 -only rootSetter can call init -only unlocker can call unlock -all calls to claimKatToken must revert before unlockTime unless already unlocked -claimKatToken will increase receiver's balance when executed successfully not written -once active, the protocol will not go to an inactive state, i.e., (block.timestamp > unlockTime || !locked) can only change false -> true -indexIsClaimed(index) can only change false -> true -indexIsClaimed(index) == true => claimKatToken(..,index) will revert -init cannot be called after the minter is unlocked i.e., after ((block.timestamp > unlockTime) || !locked) -It should not be possible to permanently renounce the rootSetter role without actually setting the root first - ----------------- -katToken: - -only certain methods may increase/decrease total mint capacity -total mint capacity + mintedTokens can only increase w -lastMintCapacityIncrease can only increase w -distributedSupplyCap can only increase w -distributedSupplyCap == total mint capacity + mintedTokens w -for all x: mintCapacity[x] <= distributedSupplyCap xx -mintCapacity of address(0) is always 0 w -inflation <= MAX_INFLATION w -inflation can be set to any value <= MAX_INFLATION - if value <= MAX_INFLATION then "satisfy" inflation == value - forall v satisfy - - w -once renounceInflationAdmin is performed, the inflationAdmin will always be zero - 1. show that renounceInflationAdmin sets inflationAdmin to 0 - 2. show that inflationAdmin can never change from 0 to non-zero w -the same for inflationBeneficiary - 1. show that renounceInflationAdmin sets inflationBeneficiary to 0 - 2. show that inflationBeneficiary can never change from 0 to non-zero w -only inflationBeneficiary can change inflationBeneficiary w -only inflationAdmin can change inflationAdmin w - ----------------- -more properties: - -KatToken.sol -158: require(value < MAX_INFLATION, "Inflation too large."); -can we write a rule that shows that all values within range must succeed? - -given any of the privileged addresses (KatToken.inflationAdmin, KatToken.inflationBeneficiary, MerkleMinter.rootSetter), once the corresponding renounce function is called, the given privileged address must remain address(0) indefinitely - -mutations..?? - -any more properties? - -1000 year inflation -> 5e18, maybe use 10e18 instead . use this: 43e18 - -minimum arg to exp2 is about 6M but not a multiplier of it - - -during the handover - -show a simple but powerful rule, show mutation diff --git a/certora/scripts/run.sh b/certora/scripts/run.sh index a9026fe..167df78 100755 --- a/certora/scripts/run.sh +++ b/certora/scripts/run.sh @@ -1,4 +1,5 @@ certoraRun certora/confs/KatToken.conf +certoraRun certora/confs/KatToken.conf --verify KatTokenHarness:certora/specs/KatToken_changeInflation.spec --msg changeInflation_revertConditions # the rule indexIsClaimedValueChange requires using bitVector theory certoraRun certora/confs/MerkleMinter.conf --rule indexIsClaimedValueChange --prover_args -smt_bitVectorTheory true --msg "MerkleMinter indexIsClaimedValueChange" diff --git a/certora/specs/KatToken_changeInflation.spec b/certora/specs/KatToken_changeInflation.spec new file mode 100644 index 0000000..bf65302 --- /dev/null +++ b/certora/specs/KatToken_changeInflation.spec @@ -0,0 +1,43 @@ +import "./exp2-summary_stronger.spec"; + +methods { + function inflationAdmin() external returns (address) envfree; + function pendingInflationAdmin() external returns (address) envfree; + function inflationBeneficiary() external returns (address) envfree; + function pendingInflationBeneficiary() external returns (address) envfree; + function inflationFactor() external returns (uint256) envfree; + function MAX_INFLATION() external returns (uint256) envfree; + function merkleMinter() external returns (address) envfree; + function mintCapacity(address) external returns (uint256) envfree; + + //harness methods declared envfree + function get_lastMintCapacityIncrease() external returns (uint256) envfree; + function get_distributedSupplyCap() external returns (uint256) envfree; + + //MerkleProof + function _.verify(bytes32[], bytes32, bytes32) external => NONDET DELETE; + + function _.eip712Domain() external => NONDET DELETE; +} + +/** + * The inflation factor is bounded by MAX_INFLATION. + */ +invariant inflationFactorIsBounded() + inflationFactor() <= MAX_INFLATION(); + +rule changeInflation_revertConditions(env e) +{ + requireInvariant inflationFactorIsBounded(); + require mintCapacity(inflationBeneficiary()) <= get_distributedSupplyCap(); // implied by mintCapacityPlusMintedEqualsDistributedSupplyCap + uint256 value; + changeInflation@withrevert(e, value); + bool reverted = lastReverted; + assert reverted => + e.msg.sender != inflationAdmin() || + e.msg.value != 0 || + inflationBeneficiary() == 0 || + value > MAX_INFLATION() || + e.block.timestamp > get_lastMintCapacityIncrease() + 100 *365 *24 *60 *60 || // unreasonably high, more than 100 years between calls to distributeInflation + get_distributedSupplyCap() > 10^35; // unreasonably high, causing an overflow. With 3% p.y. the inflation factor can get up to 1.03^100 < 20 while the initial distribution is 1e28 +} diff --git a/certora/specs/exp2-summary.spec b/certora/specs/exp2-summary.spec index 5cc841f..b27d865 100644 --- a/certora/specs/exp2-summary.spec +++ b/certora/specs/exp2-summary.spec @@ -28,36 +28,6 @@ ghost ghostExp2(mathint) returns uint256 { x >= ONE18() => ghostExp2(x) >= 2*ONE18(); axiom forall uint256 x. x <= ONE18() => ghostExp2(x) <= 2*ONE18(); - - // // lower bound - // axiom forall uint256 x. - // ((x >= 0 && x < 2*ONE18()) => ( - // ghostExp2(x) >= - // ONE18() - // + x * Log2() / ONE18() - // + x*x * Log2()*Log2() / ONE18()/ONE18()/ONE18() / 2 - // + x*x*x * Log2()*Log2()*Log2() /ONE18()/ONE18()/ONE18()/ONE18()/ONE18() / 6 - // )) && - // ((x >= 2*ONE18() && x < 4*ONE18()) => (ghostExp2(x) >= ghostExp2(x - 2*ONE18()) * 4)) && - // ((x >= 4*ONE18() && x < 6*ONE18()) => (ghostExp2(x) >= ghostExp2(x - 4*ONE18()) * 16)) && - // ((x >= 6*ONE18() && x < 8*ONE18()) => (ghostExp2(x) >= ghostExp2(x - 6*ONE18()) * 64)) && - // ((x >= 8*ONE18()) => (ghostExp2(x) >= ghostExp2(x - 8*ONE18()) * 256)) - // ; - - // // upper bound - // axiom forall uint256 x. - // ((x >= 0 && x < 2*ONE18()) => ( - // ghostExp2(x) <= - // 4*ONE18()/3 // rough estimate: this approximation at 2 is about 0.21 to low - // + x * Log2() / ONE18() - // + x*x * Log2()*Log2() / ONE18()/ONE18()/ONE18() / 2 - // + x*x*x * Log2()*Log2()*Log2() /ONE18()/ONE18()/ONE18()/ONE18()/ONE18() / 6 - // )) && - // ((x >= 2*ONE18() && x < 4*ONE18()) => (ghostExp2(x) <= ghostExp2(x - 2*ONE18()) * 4)) && - // ((x >= 4*ONE18() && x < 6*ONE18()) => (ghostExp2(x) <= ghostExp2(x - 4*ONE18()) * 16)) && - // ((x >= 6*ONE18() && x < 8*ONE18()) => (ghostExp2(x) <= ghostExp2(x - 6*ONE18()) * 64)) && - // ((x >= 8*ONE18()) => (ghostExp2(x) <= ghostExp2(x - 8*ONE18()) * 256)) - // ; } function cvlExp2(uint256 x) returns uint256 { diff --git a/certora/specs/exp2-summary_stronger.spec b/certora/specs/exp2-summary_stronger.spec new file mode 100644 index 0000000..2ac15d6 --- /dev/null +++ b/certora/specs/exp2-summary_stronger.spec @@ -0,0 +1,62 @@ +// The same as exp2-summary.spec but it adds several additional axioms + +methods { + function PowUtil.exp2(uint256 x) internal returns (uint256) => cvlExp2(x); +} + +definition ONE18() returns uint256 = 1000000000000000000; +definition Log2() returns uint256 = 693147180559945309; + +ghost ghostExp2(mathint) returns uint256 { + axiom ghostExp2(0) == ONE18(); + axiom ghostExp2(ONE18()) == 2*ONE18(); + + axiom ghostExp2(2*ONE18()) == 4*ONE18(); + axiom ghostExp2(3*ONE18()) == 8*ONE18(); + axiom ghostExp2(4*ONE18()) == 16*ONE18(); + axiom ghostExp2(5*ONE18()) == 32*ONE18(); + axiom ghostExp2(6*ONE18()) == 64*ONE18(); + axiom ghostExp2(7*ONE18()) == 128*ONE18(); + axiom ghostExp2(8*ONE18()) == 256*ONE18(); + + axiom forall uint256 x1. forall uint256 x2. + x1 > x2 => ghostExp2(x1) >= ghostExp2(x2); + axiom forall uint256 x. + x >= ONE18() => ghostExp2(x) >= 2*ONE18(); + axiom forall uint256 x. + x <= ONE18() => ghostExp2(x) <= 2*ONE18(); + + // // lower bound + // axiom forall uint256 x. + // ((x >= 0 && x < 2*ONE18()) => ( + // ghostExp2(x) >= + // ONE18() + // + x * Log2() / ONE18() + // + x*x * Log2()*Log2() / ONE18()/ONE18()/ONE18() / 2 + // + x*x*x * Log2()*Log2()*Log2() /ONE18()/ONE18()/ONE18()/ONE18()/ONE18() / 6 + // )) && + // ((x >= 2*ONE18() && x < 4*ONE18()) => (ghostExp2(x) >= ghostExp2(x - 2*ONE18()) * 4)) && + // ((x >= 4*ONE18() && x < 6*ONE18()) => (ghostExp2(x) >= ghostExp2(x - 4*ONE18()) * 16)) && + // ((x >= 6*ONE18() && x < 8*ONE18()) => (ghostExp2(x) >= ghostExp2(x - 6*ONE18()) * 64)) && + // ((x >= 8*ONE18()) => (ghostExp2(x) >= ghostExp2(x - 8*ONE18()) * 256)) + // ; + + // upper bound + axiom forall uint256 x. + ((x >= 0 && x < 2*ONE18()) => ( + ghostExp2(x) <= + 4*ONE18()/3 // rough estimate: this approximation at 2 is about 0.21 to low + + x * Log2() / ONE18() + + x*x * Log2()*Log2() / ONE18()/ONE18()/ONE18() / 2 + + x*x*x * Log2()*Log2()*Log2() /ONE18()/ONE18()/ONE18()/ONE18()/ONE18() / 6 + )) && + ((x >= 2*ONE18() && x < 4*ONE18()) => (ghostExp2(x) <= ghostExp2(x - 2*ONE18()) * 4)) && + ((x >= 4*ONE18() && x < 6*ONE18()) => (ghostExp2(x) <= ghostExp2(x - 4*ONE18()) * 16)) && + ((x >= 6*ONE18() && x < 8*ONE18()) => (ghostExp2(x) <= ghostExp2(x - 6*ONE18()) * 64)) && + ((x >= 8*ONE18()) => (ghostExp2(x) <= ghostExp2(x - 8*ONE18()) * 256)) + ; +} + +function cvlExp2(uint256 x) returns uint256 { + return ghostExp2(x); +}