diff --git a/src/kontrol/cli.py b/src/kontrol/cli.py index 83a838621..6ea7abd2a 100644 --- a/src/kontrol/cli.py +++ b/src/kontrol/cli.py @@ -573,8 +573,8 @@ def parse(s: str) -> list[T]: default=None, dest='optimize_performance', help=( - 'Optimize performance for proof execution. Takes the number of parallel threads to be used.' - "Will overwrite other settings of 'assume-defined', 'log-success-rewrites', 'max-frontier-parallel'," + 'Optimize performance for proof execution. Takes the number of parallel threads to be used. ' + "Will overwrite other settings of 'assume-defined', 'log-success-rewrites', 'max-frontier-parallel', " "'maintenance-rate', 'smt-timeout', 'smt-retry-limit', 'max-depth', 'max-iterations', and 'no-stack-checks'." ), ) @@ -584,7 +584,7 @@ def parse(s: str) -> list[T]: default=None, action='store_false', help=( - 'Optimize KEVM execution by removing stack overflow/underflow checks.' + 'Optimize KEVM execution by removing stack overflow/underflow checks. ' 'Assumes running Solidity-compiled bytecode cannot result in a stack overflow/underflow.' ), ) diff --git a/src/kontrol/kdist/no_code_size_checks.md b/src/kontrol/kdist/no_code_size_checks.md new file mode 100644 index 000000000..9708dd953 --- /dev/null +++ b/src/kontrol/kdist/no_code_size_checks.md @@ -0,0 +1,26 @@ +Relaxed Bytecode Limits Rules +=================== + +The provided rule disables the enforcement of the code size limit introduced in EIP-170 during contract deployment. +That enables the deployment of larger test contracts containing auxiliary functions for verification and testing. +In addition, it enhances compatibility with Foundry, which also does not enforce the code size limit. + +```k +requires "foundry.md" + +module NO-CODE-SIZE-CHECKS + imports EVM + imports FOUNDRY + + rule #mkCodeDeposit ACCT + => Gcodedeposit < SCHED > *Int lengthBytes(OUT) ~> #deductGas + ~> #finishCodeDeposit ACCT OUT + ... + + SCHED + OUT => .Bytes + requires #isValidCode(OUT, SCHED) + [priority(30)] + +endmodule +``` \ No newline at end of file diff --git a/src/kontrol/kompile.py b/src/kontrol/kompile.py index 9e853df89..10864945c 100644 --- a/src/kontrol/kompile.py +++ b/src/kontrol/kompile.py @@ -59,11 +59,14 @@ def foundry_kompile( regen = True foundry_up_to_date = False + options.requires = [str(foundry._root / r) for r in options.requires] + requires = ( options.requires + ([KSRC_DIR / 'keccak.md'] if options.keccak_lemmas else []) + ([KSRC_DIR / 'kontrol_lemmas.md'] if options.auxiliary_lemmas else []) + ([KSRC_DIR / 'no_stack_checks.md']) + + ([KSRC_DIR / 'no_code_size_checks.md']) ) for r in tuple(requires): req = Path(r) @@ -229,6 +232,7 @@ def _foundry_to_main_def( + ([KImport('KECCAK-LEMMAS')] if keccak_lemmas else []) + ([KImport('KONTROL-AUX-LEMMAS')] if auxiliary_lemmas else []) + ([KImport('NO-STACK-CHECKS')]) + + ([KImport('NO-CODE-SIZE-CHECKS')]) ), ) diff --git a/src/tests/integration/test-data/show/foundry.k.expected b/src/tests/integration/test-data/show/foundry.k.expected index 3e917cda0..f98fb965a 100644 --- a/src/tests/integration/test-data/show/foundry.k.expected +++ b/src/tests/integration/test-data/show/foundry.k.expected @@ -5,6 +5,7 @@ requires "requires/pausability-lemmas.k" requires "requires/symbolic-bytes-lemmas.k" requires "requires/keccak.md" requires "requires/no_stack_checks.md" +requires "requires/no_code_size_checks.md" module FOUNDRY-MAIN imports public S2KsrcZModduplicatesZMod2ZModDuplicateName-VERIFICATION @@ -173,6 +174,7 @@ module FOUNDRY-MAIN imports public S2KlibZModforgeZSubstdZModlibZModdsZSubtestZModsrcZModDSTest-VERIFICATION imports public KECCAK-LEMMAS imports public NO-STACK-CHECKS + imports public NO-CODE-SIZE-CHECKS