Usability fixes for Foundry integration (#1429)

* foundry.md: add LEMMAS module to FOUNDRY

* word.md: add notMaxUInt160

* kevm-pyk/kevm: add parens for |Int, &Int, modInt

* tests/lemmas-spec: add address reprojection tests

* include/lemmas: add lemmas for projection specs

* kevm-pyk/kevm: add parens for typedArgs too

* kevm-pyk/kevm: only update typedArgs if its present

* kevm-pyk/__main__: no need for lemmas or int-simplification requires anymore

* kevm-pyk/kevm: add more unparsing overrides

* kevm-pyk/kevm: add more parens to unparsing

* kevm-pyk/kevm: more parens

* tests/foundry: update expected output

* tests/foundry: update expected output

* include/lemmas.k: promote bool2Word lemmas to common module

* word: add notMaxUInt224 as well

Author: ehildenb

foundry.md

@@ -75,12 +75,14 @@ requires "evm.md"
 requires "hashed-locations.md"
 requires "abi.md"
 requires "edsl.md"
+requires "lemmas/lemmas.k"
 
 module FOUNDRY
     imports FOUNDRY-SUCCESS
     imports FOUNDRY-CHEAT-CODES
     imports FOUNDRY-ACCOUNTS
     imports EDSL
+    imports LEMMAS
 
     configuration
       <foundry>

kevm-pyk/src/kevm_pyk/__main__.py

@@ -130,8 +130,8 @@ def exec_foundry_kompile(
     foundry_definition_dir = foundry_out / 'kompiled'
     foundry_main_file = foundry_definition_dir / 'foundry.k'
     kompiled_timestamp = foundry_definition_dir / 'timestamp'
-    requires = ['foundry.md', 'lemmas/lemmas.k', 'lemmas/int-simplification.k'] + list(requires)
-    imports = ['FOUNDRY', 'LEMMAS', 'INT-SIMPLIFICATION'] + list(imports)
+    requires = ['foundry.md'] + list(requires)
+    imports = ['FOUNDRY'] + list(imports)
 
     if not foundry_definition_dir.exists():
         foundry_definition_dir.mkdir()

kevm-pyk/src/kevm_pyk/kevm.py

@@ -70,6 +70,7 @@ def kompile(
     @staticmethod
     def _patch_symbol_table(symbol_table: Dict[str, Any]) -> None:
         # fmt: off
+        symbol_table['#Bottom']                                       = lambda: '#Bottom'
         symbol_table['_orBool_']                                      = paren(symbol_table['_orBool_'])
         symbol_table['_andBool_']                                     = paren(symbol_table['_andBool_'])
         symbol_table['_impliesBool_']                                 = paren(symbol_table['_impliesBool_'])
@@ -78,6 +79,9 @@ def _patch_symbol_table(symbol_table: Dict[str, Any]) -> None:
         symbol_table['_*Int_']                                        = paren(symbol_table['_*Int_'])
         symbol_table['_-Int_']                                        = paren(symbol_table['_-Int_'])
         symbol_table['_+Int_']                                        = paren(symbol_table['_+Int_'])
+        symbol_table['_&Int_']                                        = paren(symbol_table['_&Int_'])
+        symbol_table['_|Int_']                                        = paren(symbol_table['_|Int_'])
+        symbol_table['_modInt_']                                      = paren(symbol_table['_modInt_'])
         symbol_table['#Or']                                           = paren(symbol_table['#Or'])
         symbol_table['#And']                                          = paren(symbol_table['#And'])
         symbol_table['#Implies']                                      = paren(symbol_table['#Implies'])
@@ -87,14 +91,20 @@ def _patch_symbol_table(symbol_table: Dict[str, Any]) -> None:
         symbol_table['_AccountCellMap_']                              = paren(lambda a1, a2: a1 + '\n' + a2)
         symbol_table['.AccountCellMap']                               = lambda: '.Bag'
         symbol_table['AccountCellMapItem']                            = lambda k, v: v
-        symbol_table['_[_:=_]_EVM-TYPES_Memory_Memory_Int_ByteArray'] = lambda m, k, v: m + ' [ '  + k + ' := (' + v + '):ByteArray ]'
+        symbol_table['_[_:=_]_EVM-TYPES_Memory_Memory_Int_ByteArray'] = paren(lambda m, k, v: m + ' [ '  + k + ' := (' + v + '):ByteArray ]')
         symbol_table['_[_.._]_EVM-TYPES_ByteArray_ByteArray_Int_Int'] = lambda m, s, w: '(' + m + ' [ ' + s + ' .. ' + w + ' ]):ByteArray'
+        symbol_table['_:__EVM-TYPES_WordStack_Int_WordStack']         = paren(symbol_table['_:__EVM-TYPES_WordStack_Int_WordStack'])
         symbol_table['_<Word__EVM-TYPES_Int_Int_Int']                 = paren(lambda a1, a2: '(' + a1 + ') <Word ('  + a2 + ')')
         symbol_table['_>Word__EVM-TYPES_Int_Int_Int']                 = paren(lambda a1, a2: '(' + a1 + ') >Word ('  + a2 + ')')
         symbol_table['_<=Word__EVM-TYPES_Int_Int_Int']                = paren(lambda a1, a2: '(' + a1 + ') <=Word (' + a2 + ')')
         symbol_table['_>=Word__EVM-TYPES_Int_Int_Int']                = paren(lambda a1, a2: '(' + a1 + ') >=Word (' + a2 + ')')
         symbol_table['_==Word__EVM-TYPES_Int_Int_Int']                = paren(lambda a1, a2: '(' + a1 + ') ==Word (' + a2 + ')')
         symbol_table['_s<Word__EVM-TYPES_Int_Int_Int']                = paren(lambda a1, a2: '(' + a1 + ') s<Word (' + a2 + ')')
+        symbol_table['_[_]_EVM-TYPES_Int_WordStack_Int']              = paren(symbol_table['_[_]_EVM-TYPES_Int_WordStack_Int'])
+        symbol_table['_++__EVM-TYPES_ByteArray_ByteArray_ByteArray']  = paren(symbol_table['_++__EVM-TYPES_ByteArray_ByteArray_ByteArray'])
+        symbol_table['_[_.._]_EVM-TYPES_ByteArray_ByteArray_Int_Int'] = paren(symbol_table['_[_.._]_EVM-TYPES_ByteArray_ByteArray_Int_Int'])
+        if 'typedArgs' in symbol_table:
+            symbol_table['typedArgs'] = paren(symbol_table['typedArgs'])
         # fmt: on
 
     class Sorts: