Incremental exploration based kprove using rpc endpoints

.github/workflows/test-pr.yml

@@ -109,7 +109,7 @@ jobs:
       - name: 'Build Foundry'
         run: docker exec -u user kevm-ci-foundry-${GITHUB_SHA} /bin/bash -c 'make build-foundry -j2'
       - name: 'Test Foundry'
-        run: docker exec -u user kevm-ci-foundry-${GITHUB_SHA} /bin/bash -c 'make test-foundry -j2 FOUNDRY_PAR=4 KPROVE_OPTS=--retry'
+        run: docker exec -u user kevm-ci-foundry-${GITHUB_SHA} /bin/bash -c 'make test-foundry -j2 FOUNDRY_PAR=12 KPROVE_OPTS=--retry'
       - name: 'Tear down Docker'
         if: always()
         run: |

Makefile

@@ -512,7 +512,7 @@ tests/foundry/out/kompiled/foundry.k: tests/foundry/out/kompiled/timestamp
 
 tests/foundry/out/kompiled/foundry.k.prove: tests/foundry/out/kompiled/timestamp
 	$(KEVM) foundry-prove tests/foundry/out                              \
-	    -j$(FOUNDRY_PAR) --no-simplify-init                              \
+	    -j$(FOUNDRY_PAR) --max-depth 1000                                \
 	    $(KEVM_OPTS) $(KPROVE_OPTS)                                      \
 	    $(addprefix --exclude-test , $(shell cat tests/foundry/exclude))
 

bin/kevm

@@ -59,6 +59,7 @@ run_kevm_pyk() {
             ;;
     esac
     ! ${verbose} || pyk_args+=(--verbose)
+    ! ${debug} || pyk_args+=(--debug)
     execute python3 -m kevm_pyk "${pyk_command}" "$@" "${pyk_args[@]}"
 }
 

deps/pyk_release

@@ -1 +1 @@
-v0.1.89
+v0.1.91

flake.nix

@@ -18,7 +18,7 @@
       "github:ethereum/legacytests/d7abc42a7b352a7b44b1f66b58aca54e4af6a9d7";
     ethereum-legacytests.flake = false;
     haskell-backend.follows = "k-framework/haskell-backend";
-    pyk.url = "github:runtimeverification/pyk/v0.1.89";
+    pyk.url = "github:runtimeverification/pyk/custom-kcfg-view";
     pyk.inputs.flake-utils.follows = "k-framework/flake-utils";
     pyk.inputs.nixpkgs.follows = "k-framework/nixpkgs";
 

include/kframework/evm.md

@@ -1469,7 +1469,8 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state-
 ```k
     syntax CallOp ::= "CALL"
  // ------------------------
-    rule <k> CALL _GCAP ACCTTO VALUE ARGSTART ARGWIDTH RETSTART RETWIDTH
+    rule [call]:
+         <k> CALL _GCAP ACCTTO VALUE ARGSTART ARGWIDTH RETSTART RETWIDTH
           => #checkCall ACCTFROM VALUE
           ~> #call ACCTFROM ACCTTO ACCTTO VALUE VALUE #range(LM, ARGSTART, ARGWIDTH) false
           ~> #return RETSTART RETWIDTH
@@ -1480,7 +1481,8 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state-
 
     syntax CallOp ::= "CALLCODE"
  // ----------------------------
-    rule <k> CALLCODE _GCAP ACCTTO VALUE ARGSTART ARGWIDTH RETSTART RETWIDTH
+    rule [callcode]:
+         <k> CALLCODE _GCAP ACCTTO VALUE ARGSTART ARGWIDTH RETSTART RETWIDTH
           => #checkCall ACCTFROM VALUE
           ~> #call ACCTFROM ACCTFROM ACCTTO VALUE VALUE #range(LM, ARGSTART, ARGWIDTH) false
           ~> #return RETSTART RETWIDTH
@@ -1491,7 +1493,8 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state-
 
     syntax CallSixOp ::= "DELEGATECALL"
  // -----------------------------------
-    rule <k> DELEGATECALL _GCAP ACCTTO ARGSTART ARGWIDTH RETSTART RETWIDTH
+    rule [delegatecall]:
+         <k> DELEGATECALL _GCAP ACCTTO ARGSTART ARGWIDTH RETSTART RETWIDTH
           => #checkCall ACCTFROM 0
           ~> #call ACCTAPPFROM ACCTFROM ACCTTO 0 VALUE #range(LM, ARGSTART, ARGWIDTH) false
           ~> #return RETSTART RETWIDTH
@@ -1504,7 +1507,8 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state-
 
     syntax CallSixOp ::= "STATICCALL"
  // ---------------------------------
-    rule <k> STATICCALL _GCAP ACCTTO ARGSTART ARGWIDTH RETSTART RETWIDTH
+    rule [staticcall]:
+         <k> STATICCALL _GCAP ACCTTO ARGSTART ARGWIDTH RETSTART RETWIDTH
           => #checkCall ACCTFROM 0
           ~> #call ACCTFROM ACCTTO ACCTTO 0 0 #range(LM, ARGSTART, ARGWIDTH) true
           ~> #return RETSTART RETWIDTH
@@ -1623,7 +1627,8 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state-
 ```k
     syntax TernStackOp ::= "CREATE"
  // -------------------------------
-    rule <k> CREATE VALUE MEMSTART MEMWIDTH
+    rule [create]:
+         <k> CREATE VALUE MEMSTART MEMWIDTH
           => #accessAccounts #newAddr(ACCT, NONCE)
           ~> #checkCall ACCT VALUE
           ~> #create ACCT #newAddr(ACCT, NONCE) VALUE #range(LM, MEMSTART, MEMWIDTH)
@@ -1644,7 +1649,8 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state-
 ```k
     syntax QuadStackOp ::= "CREATE2"
  // --------------------------------
-    rule <k> CREATE2 VALUE MEMSTART MEMWIDTH SALT
+    rule [create2]:
+         <k> CREATE2 VALUE MEMSTART MEMWIDTH SALT
           => #accessAccounts #newAddr(ACCT, SALT, #range(LM, MEMSTART, MEMWIDTH))
           ~> #checkCall ACCT VALUE
           ~> #create ACCT #newAddr(ACCT, SALT, #range(LM, MEMSTART, MEMWIDTH)) VALUE #range(LM, MEMSTART, MEMWIDTH)
@@ -2336,8 +2342,7 @@ There are several helpers for calculating gas (most of them also specified in th
 
     syntax Int ::= #allBut64th ( Int ) [function, total, smtlib(gas_allBut64th)]
  // ----------------------------------------------------------------------------
-    rule [allBut64th.pos]: #allBut64th(N) => N -Int (N /Int 64) requires 0 <=Int N
-    rule [allBut64th.neg]: #allBut64th(N) => 0                  requires N  <Int 0
+    rule [allBut64th]: #allBut64th(N) => N -Int (N /Int 64)
 ```
 
 ```{.k .nobytes}

include/kframework/infinite-gas.md

@@ -74,11 +74,13 @@ module INFINITE-GAS-COMMON
 
     syntax Int ::= #gas ( Int ) [function, total, no-evaluators, klabel(infGas), symbol, smtlib(infGas)]
  // ----------------------------------------------------------------------------------------------------
-    rule #gas(G) +Int G' => #gas(G +Int G') requires 0 <=Int G' orBool 0 -Int G' <Int #gas(G)  [simplification]
-    rule G +Int #gas(G') => #gas(G +Int G') requires 0 <=Int G  orBool 0 -Int G  <Int #gas(G') [simplification]
-
-    rule #gas(G) -Int G'       => #gas(G -Int G') requires 0 <=Int G' andBool G' <Int #gas(G) [simplification]
-    rule #gas(G) -Int #gas(G') => #gas(G -Int G')                                             [simplification]
+    // N.B.: These lemmas amount to defining \inf - \inf as \inf.
+    // In most mathematics, it's undefined it seems, so we get the choice!
+    // We make them lower priority than other rules.
+    rule #gas(G) +Int G'       => #gas(G +Int G') [simplification(60)]
+    rule G +Int #gas(G')       => #gas(G +Int G') [simplification(60)]
+    rule #gas(G) -Int G'       => #gas(G -Int G') [simplification(60)]
+    rule #gas(G) -Int #gas(G') => #gas(G -Int G') [simplification(60)]
 
     rule #gas(G) *Int G' => #gas(G *Int G') requires 0 <=Int G' [simplification]
     rule G *Int #gas(G') => #gas(G *Int G') requires 0 <=Int G  [simplification]
@@ -87,14 +89,11 @@ module INFINITE-GAS-COMMON
     rule G /Int #gas(G') => 0               requires 0 <=Int G  andBool G  <Int #gas(G') [simplification]
 
     rule #gas(#gas(G)) => #gas(G) [simplification]
+    rule #gas(#gas(G) +Int G') => #gas(G +Int G') [simplification]
 
     rule minInt(#gas(G), #gas(G'))              => #gas(minInt(G, G'))              [simplification]
     rule #if B #then #gas(G) #else #gas(G') #fi => #gas(#if B #then G #else G' #fi) [simplification]
 
-    rule #allBut64th(#gas(G)) => #gas(#allBut64th(G)) [simplification]
-
-    rule Cgascap(SCHED, #gas(GCAP), #gas(GAVAIL), GEXTRA) => #gas(Cgascap(SCHED, GCAP, GAVAIL, GEXTRA)) requires #rangeUInt(256, GEXTRA) [simplification]
-
     rule _ <=Int #gas(_)        => true  [simplification]
     rule         #gas(_) <Int _ => false [simplification]
 
@@ -124,11 +123,6 @@ module INFINITE-GAS-COMMON
     rule #gas(_)  <Int Csload(_, _) => false [simplification]
     rule #gas(_) >=Int Csload(_, _) => true  [simplification]
 
-    rule 0 <=Int Cmem(_, _)       => true  [simplification]
-    rule Cmem(_, _) <Int #gas(_)  => true  [simplification]
-    rule #gas(_) <Int Cmem(_, _)  => false [simplification]
-    rule Cmem(_, _) <=Int #gas(_) => true  [simplification]
-
     rule 0 <=Int Caddraccess(_, _)       => true  [simplification]
     rule Caddraccess(_, _) <Int #gas(_)  => true  [simplification]
     rule #gas(_) <Int Caddraccess(_, _)  => false [simplification]
@@ -140,15 +134,26 @@ module INFINITE-GAS-COMMON
     rule 0 <=Int Cmem(_, N)              => true requires 0 <=Int N       [simplification]
     rule         Cmem(_, N) <Int #gas(G) => true requires N  <Int #gas(G) [simplification]
 
-    rule 0 <=Int Cgascap(_, _, _, _)                           => true                                                                                    [simplification]
-    rule         Cgascap(_, GCAP, GAVAIL, GEXTRA) <Int #gas(G) => true requires GCAP <Int #gas(G) andBool GAVAIL <Int #gas(G) andBool GEXTRA <Int #gas(G) [simplification]
+    rule Cgascap(SCHED, GAVAIL, GAVAIL, GEXTRA) => #allBut64th(GAVAIL -Int GEXTRA)
+      requires 0 <=Int GEXTRA andBool GEXTRA <=Int GAVAIL
+       andBool notBool Gstaticcalldepth << SCHED >>
+      [simplification]
+
+    rule 0 <=Int Cgascap(_, _, _, _)                     => true                                            [simplification]
+    rule G <=Int Cgascap(_, GCAP, #gas(_), _)            => true  requires 0 <=Int G andBool G <=Int GCAP   [simplification]
+    rule         Cgascap(_, GCAP, #gas(_), _)     <Int G => false requires 0 <=Int G andBool G <=Int GCAP   [simplification]
+    rule         Cgascap(_, GCAP, _, _)           <Int G => true  requires 0 <=Int GCAP andBool GCAP <Int G [simplification]
+    rule         Cgascap(_, #gas(_), #gas(_), _)  <Int _ => false                                           [simplification]
 
     rule 0 <=Int Cextra(_, _, _, _)              => true [simplification]
     rule         Cextra(_, _, _, _) <Int #gas(_) => true [simplification]
     rule         Cextra(_, _, _, _) <Int pow256  => true [simplification]
 
-    rule 0 <=Int #allBut64th(_)                => true                          [simplification]
-    rule         #allBut64th(G)  <Int #gas(G') => true requires G <Int #gas(G') [simplification]
+    rule #allBut64th(#gas(G))            => #gas(#allBut64th(G))         [simplification]
+    rule (G /Int 64) +Int #allBut64th(G) => G                            [simplification]
+
+    rule 0 <=Int #allBut64th(G)         => true requires 0 <=Int G  [simplification]
+    rule         #allBut64th(G) <Int G' => true requires G  <Int G' [simplification]
 
     rule 0 <=Int _:ScheduleConst < _:Schedule >               => true [simplification]
     rule         _:ScheduleConst < _:Schedule >  <Int #gas(_) => true [simplification]

include/kframework/lemmas/lemmas.k

@@ -27,6 +27,8 @@ module LEMMAS [symbolic]
     rule maxUInt48  &Int X <Int pow48  => true requires 0 <=Int X [simplification, smt-lemma]
     rule maxUInt160 &Int X <Int pow160 => true requires 0 <=Int X [simplification, smt-lemma]
 
+    rule (X /Int 64) +Int #allBut64th(X) => X [simplification]
+
   // ########################
   // Set Reasoning
   // ########################