From 4a52acf73e5cdebc6ec12c40bb1f4326f3074187 Mon Sep 17 00:00:00 2001 From: Juan C Date: Fri, 29 Jul 2022 19:56:51 +0200 Subject: [PATCH 1/8] Add dummy foundry.md file --- Makefile | 1 + foundry.md | 19 +++++++++++++++++++ kevm_pyk/src/kevm_pyk/__main__.py | 2 +- kevm_pyk/src/kevm_pyk/solc_to_k.py | 2 +- tests/foundry/foundry.k.check.expected | 6 +++--- 5 files changed, 25 insertions(+), 5 deletions(-) create mode 100644 foundry.md diff --git a/Makefile b/Makefile index 6960a6e108..9597533d8a 100644 --- a/Makefile +++ b/Makefile @@ -176,6 +176,7 @@ kevm_files := abi.md \ evm.md \ evm-types.md \ evm-node.md \ + foundry.md \ hashed-locations.md \ infinite-gas.md \ json-rpc.md \ diff --git a/foundry.md b/foundry.md new file mode 100644 index 0000000000..1bb452117c --- /dev/null +++ b/foundry.md @@ -0,0 +1,19 @@ +Foundry Specifications +======================== + +### Overview + +Foundry's testing framework provides a series of cheatcodes so that developers can specify what situation they want to test. +This file describes the KEVM specification of the Foundry testing framework, which includes the definition of said cheatcodes and what does it mean for a test to pass. + +```k +requires "edsl.md" + +module FOUNDRY + imports EDSL +endmodule +``` + +Foundry Success Predicate +------------- + diff --git a/kevm_pyk/src/kevm_pyk/__main__.py b/kevm_pyk/src/kevm_pyk/__main__.py index 07dea935c3..9cb4583e85 100644 --- a/kevm_pyk/src/kevm_pyk/__main__.py +++ b/kevm_pyk/src/kevm_pyk/__main__.py @@ -88,7 +88,7 @@ def main(): claims_modules.append(claims_module) main_module = KFlatModule(args.main_module, [], [KImport(mname) for mname in [_m.name for _m in modules] + args.imports]) modules.append(main_module) - bin_runtime_definition = KDefinition(main_module.name, modules + claims_modules, requires=[KRequire(req) for req in ['edsl.md'] + args.requires]) + bin_runtime_definition = KDefinition(main_module.name, modules + claims_modules, requires=[KRequire(req) for req in ['foundry.md'] + args.requires]) _kprint = KPrint_make_unparsing(kevm, extra_modules=modules) KEVM._patch_symbol_table(_kprint.symbol_table) print(_kprint.pretty_print(bin_runtime_definition) + '\n') diff --git a/kevm_pyk/src/kevm_pyk/solc_to_k.py b/kevm_pyk/src/kevm_pyk/solc_to_k.py index cf2b4d8ba7..74a282cd8c 100644 --- a/kevm_pyk/src/kevm_pyk/solc_to_k.py +++ b/kevm_pyk/src/kevm_pyk/solc_to_k.py @@ -129,7 +129,7 @@ def contract_to_k(contract_json: Dict, contract_name: str, empty_config: KInner, module_name = contract_name.upper() + '-BIN-RUNTIME' sentences = [contract_subsort, contract_production] + storage_sentences + function_sentences + [contract_macro] + function_selector_alias_sentences - module = KFlatModule(module_name, sentences, [KImport('EDSL')]) + module = KFlatModule(module_name, sentences, [KImport('EDSL')]) if not foundry else KFlatModule(module_name, sentences, [KImport('FOUNDRY')]) claims_module: Optional[KFlatModule] = None function_test_productions = [prod for prod in module.syntax_productions if prod.sort == KSort(f'{contract_name}Function')] diff --git a/tests/foundry/foundry.k.check.expected b/tests/foundry/foundry.k.check.expected index 9cf725f94a..664d664fbf 100644 --- a/tests/foundry/foundry.k.check.expected +++ b/tests/foundry/foundry.k.check.expected @@ -1,8 +1,8 @@ -requires "edsl.md" +requires "foundry.md" requires "lemmas/int-simplification.k" module TOKEN-BIN-RUNTIME - imports public EDSL + imports public FOUNDRY syntax Contract ::= TokenContract @@ -44,7 +44,7 @@ module TOKEN-BIN-RUNTIME endmodule module TOKENTEST-BIN-RUNTIME - imports public EDSL + imports public FOUNDRY syntax Contract ::= TokenTestContract From 3b04aa29541a89c6116352f9bbd7f2f42f4d083e Mon Sep 17 00:00:00 2001 From: Juan C Date: Mon, 1 Aug 2022 20:10:39 +0200 Subject: [PATCH 2/8] Update dummy foundry.md file and solc_to_k mod --- foundry.md | 23 +++++++++++++++++++---- kevm_pyk/src/kevm_pyk/solc_to_k.py | 4 +++- 2 files changed, 22 insertions(+), 5 deletions(-) diff --git a/foundry.md b/foundry.md index 1bb452117c..c7d1352650 100644 --- a/foundry.md +++ b/foundry.md @@ -1,5 +1,5 @@ Foundry Specifications -======================== +====================== ### Overview @@ -8,12 +8,27 @@ This file describes the KEVM specification of the Foundry testing framework, whi ```k requires "edsl.md" - module FOUNDRY imports EDSL + imports FOUNDRY-SUCCESS + imports FOUNDRY-CHEAT-CODES endmodule ``` - Foundry Success Predicate -------------- +------------------------- +```k +module FOUNDRY-SUCCESS + imports EVM + syntax Bool ::= "foundry_success" "(" ")" [function] + // -------------------------------------------- + rule foundry_success() => false +endmodule +``` +Foundry Cheat Codes +------------------- +```k +module FOUNDRY-CHEAT-CODES + imports EDSL +endmodule +``` diff --git a/kevm_pyk/src/kevm_pyk/solc_to_k.py b/kevm_pyk/src/kevm_pyk/solc_to_k.py index 74a282cd8c..ad4e2117e6 100644 --- a/kevm_pyk/src/kevm_pyk/solc_to_k.py +++ b/kevm_pyk/src/kevm_pyk/solc_to_k.py @@ -129,7 +129,9 @@ def contract_to_k(contract_json: Dict, contract_name: str, empty_config: KInner, module_name = contract_name.upper() + '-BIN-RUNTIME' sentences = [contract_subsort, contract_production] + storage_sentences + function_sentences + [contract_macro] + function_selector_alias_sentences - module = KFlatModule(module_name, sentences, [KImport('EDSL')]) if not foundry else KFlatModule(module_name, sentences, [KImport('FOUNDRY')]) + imported_modules = KImport('FOUNDRY') if foundry else KImport('EDSL') + module = KFlatModule(module_name, sentences, [imported_modules]) + claims_module: Optional[KFlatModule] = None function_test_productions = [prod for prod in module.syntax_productions if prod.sort == KSort(f'{contract_name}Function')] From 428d67547bf71674b79f10fe58614133816c2c4a Mon Sep 17 00:00:00 2001 From: Juan C Date: Mon, 1 Aug 2022 21:09:02 +0200 Subject: [PATCH 3/8] Add ensures clause generation --- Makefile | 4 ++-- edsl.md | 2 ++ foundry.md | 7 +++---- kevm_pyk/src/kevm_pyk/__main__.py | 2 +- kevm_pyk/src/kevm_pyk/kevm.py | 4 ++++ kevm_pyk/src/kevm_pyk/solc_to_k.py | 9 +++++---- tests/foundry/foundry.k.check.expected | 8 +++++--- 7 files changed, 22 insertions(+), 14 deletions(-) diff --git a/Makefile b/Makefile index 9597533d8a..c15817e262 100644 --- a/Makefile +++ b/Makefile @@ -445,7 +445,7 @@ tests/foundry/foundry.k.check: tests/foundry/foundry.k $(CHECK) $< $@.expected tests/foundry/foundry.k.prove: tests/foundry/kompiled/timestamp - $(KEVM) prove tests/foundry/foundry.k --pyk --backend haskell --definition tests/foundry/kompiled \ + $(KEVM) prove tests/foundry/foundry.k --backend haskell --definition tests/foundry/kompiled \ $(TEST_OPTIONS) --spec-module TOKENTEST-BIN-RUNTIME-SPEC tests/foundry/kompiled/timestamp: tests/foundry/foundry.k @@ -614,7 +614,7 @@ kevm_pyk_tests := \ tests/specs/examples/erc20-bin-runtime.k \ tests/specs/examples/erc721-bin-runtime.k -test-kevm-pyk: KPROVE_OPTS += --pyk --verbose +#test-kevm-pyk: KPROVE_OPTS += --pyk --verbose test-kevm-pyk: KOMPILE_OPTS += --pyk --verbose test-kevm-pyk: KEVM = . ./kevm_pyk/venv-prod/bin/activate && kevm test-kevm-pyk: KOMPILE = . ./kevm_pyk/venv-prod/bin/activate && kevm kompile diff --git a/edsl.md b/edsl.md index 125531a838..01d8e820d0 100644 --- a/edsl.md +++ b/edsl.md @@ -12,6 +12,7 @@ requires "hashed-locations.md" requires "abi.md" requires "infinite-gas.md" requires "optimizations.md" +requires "foundry.md" module EDSL imports BUF @@ -20,6 +21,7 @@ module EDSL imports EVM-OPTIMIZATIONS imports INFINITE-GAS imports BIN-RUNTIME + imports FOUNDRY endmodule module BIN-RUNTIME diff --git a/foundry.md b/foundry.md index c7d1352650..57b60a6c12 100644 --- a/foundry.md +++ b/foundry.md @@ -7,9 +7,8 @@ Foundry's testing framework provides a series of cheatcodes so that developers c This file describes the KEVM specification of the Foundry testing framework, which includes the definition of said cheatcodes and what does it mean for a test to pass. ```k -requires "edsl.md" +requires "evm.md" module FOUNDRY - imports EDSL imports FOUNDRY-SUCCESS imports FOUNDRY-CHEAT-CODES endmodule @@ -19,7 +18,7 @@ Foundry Success Predicate ```k module FOUNDRY-SUCCESS imports EVM - syntax Bool ::= "foundry_success" "(" ")" [function] + syntax Bool ::= "foundry_success" "(" ")" [function, klabel(foundry_success), symbol] // -------------------------------------------- rule foundry_success() => false endmodule @@ -28,7 +27,7 @@ Foundry Cheat Codes ------------------- ```k module FOUNDRY-CHEAT-CODES - imports EDSL + imports EVM endmodule ``` diff --git a/kevm_pyk/src/kevm_pyk/__main__.py b/kevm_pyk/src/kevm_pyk/__main__.py index 9cb4583e85..07dea935c3 100644 --- a/kevm_pyk/src/kevm_pyk/__main__.py +++ b/kevm_pyk/src/kevm_pyk/__main__.py @@ -88,7 +88,7 @@ def main(): claims_modules.append(claims_module) main_module = KFlatModule(args.main_module, [], [KImport(mname) for mname in [_m.name for _m in modules] + args.imports]) modules.append(main_module) - bin_runtime_definition = KDefinition(main_module.name, modules + claims_modules, requires=[KRequire(req) for req in ['foundry.md'] + args.requires]) + bin_runtime_definition = KDefinition(main_module.name, modules + claims_modules, requires=[KRequire(req) for req in ['edsl.md'] + args.requires]) _kprint = KPrint_make_unparsing(kevm, extra_modules=modules) KEVM._patch_symbol_table(_kprint.symbol_table) print(_kprint.pretty_print(bin_runtime_definition) + '\n') diff --git a/kevm_pyk/src/kevm_pyk/kevm.py b/kevm_pyk/src/kevm_pyk/kevm.py index c21be5a816..ebf9d770be 100644 --- a/kevm_pyk/src/kevm_pyk/kevm.py +++ b/kevm_pyk/src/kevm_pyk/kevm.py @@ -209,3 +209,7 @@ def wordstack_len(constrainedTerm: KInner) -> int: @staticmethod def parse_bytestack(s: KInner) -> KApply: return KApply('#parseByteStack(_)_SERIALIZATION_ByteArray_String', [s]) + + @staticmethod + def foundry_success() -> KApply: + return KApply('foundry_success') diff --git a/kevm_pyk/src/kevm_pyk/solc_to_k.py b/kevm_pyk/src/kevm_pyk/solc_to_k.py index ad4e2117e6..f858601b68 100644 --- a/kevm_pyk/src/kevm_pyk/solc_to_k.py +++ b/kevm_pyk/src/kevm_pyk/solc_to_k.py @@ -28,7 +28,7 @@ KVariable, ) from pyk.kastManip import abstract_term_safely, substitute -from pyk.prelude import intToken, stringToken +from pyk.prelude import intToken, mlEqualsTrue, stringToken from pyk.utils import intersperse from .kevm import KEVM @@ -101,10 +101,11 @@ def gen_claims_for_contract(empty_config: KInner, contract_name: str, calldata_c init_terms = [(f'{contract_name.lower()}-{i}', substitute(init_term, {'CALLDATA_CELL': cd})) for i, cd in enumerate(calldata_cells)] else: init_terms = [(contract_name.lower(), init_term)] - final_term = abstract_cell_vars(substitute(empty_config, final_subst)) + final_cterm = CTerm(abstract_cell_vars(substitute(empty_config, final_subst))) + final_cterm = final_cterm.add_constraint(mlEqualsTrue(KEVM.foundry_success())) claims: List[KClaim] = [] for claim_id, i_term in init_terms: - claim, _ = build_claim(claim_id, CTerm(i_term), CTerm(final_term)) + claim, _ = build_claim(claim_id, CTerm(i_term), final_cterm) claims.append(claim) return claims @@ -129,7 +130,7 @@ def contract_to_k(contract_json: Dict, contract_name: str, empty_config: KInner, module_name = contract_name.upper() + '-BIN-RUNTIME' sentences = [contract_subsort, contract_production] + storage_sentences + function_sentences + [contract_macro] + function_selector_alias_sentences - imported_modules = KImport('FOUNDRY') if foundry else KImport('EDSL') + imported_modules = KImport('EDSL') module = KFlatModule(module_name, sentences, [imported_modules]) diff --git a/tests/foundry/foundry.k.check.expected b/tests/foundry/foundry.k.check.expected index 664d664fbf..a1d642aa86 100644 --- a/tests/foundry/foundry.k.check.expected +++ b/tests/foundry/foundry.k.check.expected @@ -1,8 +1,8 @@ -requires "foundry.md" +requires "edsl.md" requires "lemmas/int-simplification.k" module TOKEN-BIN-RUNTIME - imports public FOUNDRY + imports public EDSL syntax Contract ::= TokenContract @@ -44,7 +44,7 @@ module TOKEN-BIN-RUNTIME endmodule module TOKENTEST-BIN-RUNTIME - imports public FOUNDRY + imports public EDSL syntax Contract ::= TokenTestContract @@ -282,6 +282,7 @@ module TOKENTEST-BIN-RUNTIME-SPEC + ensures foundry_success ( ) [label(tokentest-0)] claim [tokentest-1]: @@ -473,6 +474,7 @@ module TOKENTEST-BIN-RUNTIME-SPEC + ensures foundry_success ( ) [label(tokentest-1)] endmodule From 4d1eb83b4f04352585821deea23676ac005b4643 Mon Sep 17 00:00:00 2001 From: Juan C Date: Tue, 2 Aug 2022 13:15:24 +0200 Subject: [PATCH 4/8] Makefile: remove test foundry.k.prove, add kompiled/timestamp --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index c15817e262..a9fef5000c 100644 --- a/Makefile +++ b/Makefile @@ -607,7 +607,7 @@ test-failure: $(failure_tests:=.run-expected) # kevm_pyk Tests kevm_pyk_tests := \ - tests/foundry/foundry.k.prove \ + tests/foundry/kompiled/timestamp \ tests/foundry/foundry.k.check \ tests/specs/bihu/functional-spec.k.prove \ tests/specs/examples/empty-bin-runtime.k \ From 4a01486e3fbee0f3f64b48cc979119710caacfb0 Mon Sep 17 00:00:00 2001 From: Juan C Date: Tue, 2 Aug 2022 18:50:38 +0200 Subject: [PATCH 5/8] kevm.py/solc_to_k.py: Fix merging mistakes --- kevm_pyk/src/kevm_pyk/kevm.py | 1 - kevm_pyk/src/kevm_pyk/solc_to_k.py | 2 +- 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/kevm_pyk/src/kevm_pyk/kevm.py b/kevm_pyk/src/kevm_pyk/kevm.py index 1592df7a8d..a4f28cbbe5 100644 --- a/kevm_pyk/src/kevm_pyk/kevm.py +++ b/kevm_pyk/src/kevm_pyk/kevm.py @@ -229,4 +229,3 @@ def typed_args(args: List[KInner]) -> KApply: for i in reversed(args): res = KApply('_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs', [i, res]) return res - diff --git a/kevm_pyk/src/kevm_pyk/solc_to_k.py b/kevm_pyk/src/kevm_pyk/solc_to_k.py index 7297559cac..a93e2b4c0d 100644 --- a/kevm_pyk/src/kevm_pyk/solc_to_k.py +++ b/kevm_pyk/src/kevm_pyk/solc_to_k.py @@ -30,7 +30,7 @@ KVariable, ) from pyk.kastManip import abstract_term_safely, substitute -from pyk.prelude import intToken, mlEqualsTrue, Sorts, stringToken +from pyk.prelude import Sorts, intToken, mlEqualsTrue, stringToken from pyk.utils import FrozenDict, intersperse from .kevm import KEVM From e680243635e30ab6526dc34980da5a64733fbbb7 Mon Sep 17 00:00:00 2001 From: Juan C Date: Tue, 2 Aug 2022 19:17:24 +0200 Subject: [PATCH 6/8] Makefile: add pyk arguments --- Makefile | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Makefile b/Makefile index a9fef5000c..2c1677bf6b 100644 --- a/Makefile +++ b/Makefile @@ -445,7 +445,7 @@ tests/foundry/foundry.k.check: tests/foundry/foundry.k $(CHECK) $< $@.expected tests/foundry/foundry.k.prove: tests/foundry/kompiled/timestamp - $(KEVM) prove tests/foundry/foundry.k --backend haskell --definition tests/foundry/kompiled \ + $(KEVM) prove tests/foundry/foundry.k --pyk --backend haskell --definition tests/foundry/kompiled \ $(TEST_OPTIONS) --spec-module TOKENTEST-BIN-RUNTIME-SPEC tests/foundry/kompiled/timestamp: tests/foundry/foundry.k @@ -614,7 +614,7 @@ kevm_pyk_tests := \ tests/specs/examples/erc20-bin-runtime.k \ tests/specs/examples/erc721-bin-runtime.k -#test-kevm-pyk: KPROVE_OPTS += --pyk --verbose +test-kevm-pyk: KPROVE_OPTS += --pyk --verbose test-kevm-pyk: KOMPILE_OPTS += --pyk --verbose test-kevm-pyk: KEVM = . ./kevm_pyk/venv-prod/bin/activate && kevm test-kevm-pyk: KOMPILE = . ./kevm_pyk/venv-prod/bin/activate && kevm kompile From be06e7bb8db811ac1d3c2ac1adf4c4b3628a9b50 Mon Sep 17 00:00:00 2001 From: Juan C <38925412+JuanCoRo@users.noreply.github.com> Date: Tue, 2 Aug 2022 20:48:46 +0200 Subject: [PATCH 7/8] foundry.md: correct formatting Co-authored-by: Everett Hildenbrandt --- foundry.md | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/foundry.md b/foundry.md index 57b60a6c12..ca3ffb1d87 100644 --- a/foundry.md +++ b/foundry.md @@ -13,18 +13,23 @@ module FOUNDRY imports FOUNDRY-CHEAT-CODES endmodule ``` + Foundry Success Predicate ------------------------- + ```k module FOUNDRY-SUCCESS imports EVM + syntax Bool ::= "foundry_success" "(" ")" [function, klabel(foundry_success), symbol] - // -------------------------------------------- + // ------------------------------------------------------------------------------------- rule foundry_success() => false endmodule ``` + Foundry Cheat Codes ------------------- + ```k module FOUNDRY-CHEAT-CODES imports EVM From 19fd6885e9e5b0f0834f6751600166ac6d1d7b27 Mon Sep 17 00:00:00 2001 From: Juan C <38925412+JuanCoRo@users.noreply.github.com> Date: Tue, 2 Aug 2022 20:50:06 +0200 Subject: [PATCH 8/8] solc_to_k.py: remove imported_modules variable Co-authored-by: Everett Hildenbrandt --- kevm_pyk/src/kevm_pyk/solc_to_k.py | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/kevm_pyk/src/kevm_pyk/solc_to_k.py b/kevm_pyk/src/kevm_pyk/solc_to_k.py index a93e2b4c0d..a6eb251275 100644 --- a/kevm_pyk/src/kevm_pyk/solc_to_k.py +++ b/kevm_pyk/src/kevm_pyk/solc_to_k.py @@ -309,8 +309,7 @@ def contract_to_k(contract: Contract, empty_config: KInner, foundry: bool = Fals sentences = contract.sentences module_name = contract_name.upper() + '-BIN-RUNTIME' - imported_modules = KImport('EDSL') - module = KFlatModule(module_name, sentences, [imported_modules]) + module = KFlatModule(module_name, sentences, [KImport('EDSL')]) claims_module: Optional[KFlatModule] = None function_test_productions = [prod for prod in module.syntax_productions if prod.sort == KSort(f'{contract_name}Method')]