solve the unhook problem during summarizing ADD.

runtimeverification · Jan 9, 2025 · a92e97e · a92e97e
1 parent c8104fa
commit a92e97e
Show file tree

Hide file tree

Showing 6 changed files with 2,806 additions and 7 deletions.
diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py
@@ -639,7 +639,7 @@ def exec_summarize(options: ProveOptions) -> None:
     proof_dir = Path(__file__).parent / 'proofs'
     save_directory = Path(__file__).parent / 'summaries'
     summarizer = KEVMSummarizer(proof_dir, save_directory)
-    proof = summarizer.build_spec('STOP')
+    proof = summarizer.build_spec('ADD')
     summarizer.explore(proof)
     summarizer.summarize(proof)
     # summarizer.analyze_proof(proof_dir / 'STOP_SPEC')

diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md
@@ -1886,9 +1886,9 @@ Precompiled Contracts
     syntax InternalOp ::= #ecadd(G1Point, G1Point) [symbol(#ecadd)]
  // ---------------------------------------------------------------
     rule <k> #ecadd(P1, P2) => #end EVMC_PRECOMPILE_FAILURE ... </k>
-      requires notBool isValidPoint(P1) orBool notBool isValidPoint(P2)
+      requires notBool isValidPointWrapper(P1) orBool notBool isValidPointWrapper(P2)
     rule <k> #ecadd(P1, P2) => #end EVMC_SUCCESS ... </k> <output> _ => #point(BN128Add(P1, P2)) </output>
-      requires isValidPoint(P1) andBool isValidPoint(P2)
+      requires isValidPointWrapper(P1) andBool isValidPointWrapper(P2)
 
     syntax PrecompiledOp ::= "ECMUL"
  // --------------------------------
@@ -1898,9 +1898,9 @@ Precompiled Contracts
     syntax InternalOp ::= #ecmul(G1Point, Int) [symbol(#ecmul)]
  // -----------------------------------------------------------
     rule <k> #ecmul(P, _S) => #end EVMC_PRECOMPILE_FAILURE ... </k>
-      requires notBool isValidPoint(P)
+      requires notBool isValidPointWrapper(P)
     rule <k> #ecmul(P,  S) => #end EVMC_SUCCESS ... </k> <output> _ => #point(BN128Mul(P, S)) </output>
-      requires isValidPoint(P)
+      requires isValidPointWrapper(P)
 
     syntax Bytes ::= #point ( G1Point ) [symbol(#point), function]
  // --------------------------------------------------------------
@@ -1925,9 +1925,9 @@ Precompiled Contracts
     syntax InternalOp ::= "#checkPoint"
  // -----------------------------------
     rule <k> (#checkPoint => .K) ~> #ecpairing(ListItem(AK::G1Point) _, ListItem(BK::G2Point) _, _, _, _) ... </k>
-      requires isValidPoint(AK) andBool isValidPoint(BK)
+      requires isValidPointWrapper(AK) andBool isValidPointWrapper(BK)
     rule <k> #checkPoint ~> #ecpairing(ListItem(AK::G1Point) _, ListItem(BK::G2Point) _, _, _, _) => #end EVMC_PRECOMPILE_FAILURE ... </k>
-      requires notBool isValidPoint(AK) orBool notBool isValidPoint(BK)
+      requires notBool isValidPointWrapper(AK) orBool notBool isValidPointWrapper(BK)
 
     syntax PrecompiledOp ::= "BLAKE2F"
  // ----------------------------------

diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md
@@ -18,6 +18,16 @@ module SERIALIZATION
 Address/Hash Helpers
 --------------------
 
+- `isValidPointWrapper` serves as a wrapper around the `isValidPoint` in `KRYPTO`.
+
+```k
+    syntax Bool ::= isValidPointWrapper ( G1Point ) [symbol(isValidPointWrapper), function, total, smtlib(smt_krypto_bn128valid)]
+                  | isValidPointWrapper ( G2Point ) [symbol(isValidG2PointWrapper), function, total, smtlib(smt_krypto_bn128g2valid)]
+ // -----------------------------------------------------------------------------------------------------------------------------
+    rule [isValidPointWrapper]: isValidPointWrapper(P:G1Point) => isValidPoint(P) [concrete]
+    rule [isValidG2PointWrapper]: isValidPointWrapper(P:G2Point) => isValidPoint(P) [concrete]
+```
+
 -   `keccak` serves as a wrapper around the `Keccak256` in `KRYPTO`.
 
 ```k