Introducing first sumary for ERC20TransferValid.json contract

Pi-Squared-Inc · Oct 15, 2024 · fb3c445 · fb3c445
1 parent 1e44493
commit fb3c445
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 0 deletions.
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md
@@ -9,12 +9,14 @@ requires "evm.md"
 requires "optimizations.md"
 requires "asm.md"
 requires "state-utils.md"
+requires "lemmas/summaries.k"
 
 module ETHEREUM-SIMULATION
     imports EVM
     imports EVM-OPTIMIZATIONS
     imports EVM-ASSEMBLY
     imports STATE-UTILS
+    imports SUMMARIES
 ```
 
 An Ethereum simulation is a list of Ethereum commands.

diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/summaries.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/summaries.k
@@ -0,0 +1,15 @@
+requires "domains.md"
+requires "evm.md"
+
+module ERC20TRANSFERVALID-SUMMARY
+	imports EVM
+
+	rule [program.load]:
+		<k> #loadProgram BYTES => .K ...</k>
+		<program> _ => BYTES </program>
+		<jumpDests> _ => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00" </jumpDests> [priority(40)]
+endmodule
+
+module SUMMARIES
+    imports ERC20TRANSFERVALID-SUMMARY
+endmodule