Disable code size checks, minor fixes (#897)

* Add `no-code-size-check` module, minor fixes in kompilation, help

* Formatting, expected output update

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.'
         ),
     )

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 <k> #mkCodeDeposit ACCT
+          => Gcodedeposit < SCHED > *Int lengthBytes(OUT) ~> #deductGas
+          ~> #finishCodeDeposit ACCT OUT
+         ...
+         </k>
+         <schedule> SCHED </schedule>
+         <output> OUT => .Bytes </output>
+      requires #isValidCode(OUT, SCHED)
+   [priority(30)]
+
+endmodule
+```

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')])
         ),
     )
 

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