Upstream symbolic bytes lookup, List membership lemmas (#2702)

* Add bytes lookup lemmas

* Add test for the symbolic bytes index lookup lemma

* Add List membership lemmas

* Fix sign in `lookup-as-asWord` lemma

Author: palinatolmach

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k

@@ -285,4 +285,20 @@ module BYTES-SIMPLIFICATION [symbolic]
     rule #asWord ( #ecrec ( _ , _ , _ , _ ) ) <Int pow160 => true
         [simplification, smt-lemma]
 
+    // Symbolic bytes lookup
+
+    rule [bytes-concat-lookup-left]:
+      ( B1:Bytes +Bytes B2:Bytes ) [ I:Int ] => B1 [ I ]
+      requires 0 <=Int I andBool I <Int lengthBytes(B1)
+      [simplification(40), preserves-definedness]
+
+    rule [bytes-concat-lookup-right]:
+      ( B1:Bytes +Bytes B2:Bytes ) [ I:Int ] => B2 [ I -Int lengthBytes(B1) ]
+      requires lengthBytes(B1) <=Int I
+      [simplification(40), preserves-definedness]
+
+    rule [lookup-as-asWord]:
+      B:Bytes [ I:Int ] => #asWord ( #range ( B, I, 1 ) )
+      requires 0 <=Int I andBool I <Int lengthBytes(B)
+      [simplification(60)]
 endmodule

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k

@@ -132,6 +132,19 @@ module LEMMAS-WITHOUT-SLOT-UPDATES [symbolic]
  // Hardcoded #addrFromPrivateKey simplifications, see: https://github.com/runtimeverification/haskell-backend/issues/3573
     rule #addrFromPrivateKey("0x0000000000000000000000000000000000000000000000000000000000000001") => 721457446580647751014191829380889690493307935711 [priority(40), concrete]
 
+  // ########################
+  // List Reasoning
+  // ########################
+
+    // List membership check simplification for lists with a single element
+    rule KI:KItem in ListItem(KI:KItem) => true [simplification]
+    rule KI:KItem in ListItem(KJ:KItem) => KI ==K KJ [simplification]
+
+    // Recursive list membership check for lists with multiple elements
+    rule KI:KItem in (ListItem(KI) _REST) => true [simplification]
+    rule KI:KItem in (ListItem(KJ) REST) => KI in REST requires KI =/=K KJ [simplification]
+    rule _KI:KItem in .List => false [simplification]
+
   // ########################
   // Memory
   // ########################

tests/specs/functional/lemmas-spec.k

@@ -148,6 +148,12 @@ module LEMMAS-SPEC
       </k>
       requires X =/=K Y
 
+// List simplifications
+// --------------------
+
+  claim [list-in-simplification]:
+    <k> runLemma ( b"\xd3V\x97\x17" in ListItem ( b"Y\xecK\x01" +Bytes #buf ( 32 , W:Int ) ) ) => doneLemma ( false ) ... </k>
+      requires #rangeUInt(256, W)
 
  // Memory update simplifications
  // ----------------------------
@@ -366,6 +372,13 @@ module LEMMAS-SPEC
             => doneLemma(true) ... </k>
       requires lengthBytes ( BYTES:Bytes ) <Int 32
 
+// Symbolic bytes lookup simplification
+// -------------------
+    claim [lookup-symbolic-bytes]: 
+      <k> runLemma ( b"`\xa0`@R4\x80\x15a\x00\x10W`\x00" +Bytes #buf ( 32 , W:Int )  [ 0 ] )
+        => doneLemma ( 96 ) ... </k>
+        requires #rangeUInt(256, W)
+
  // #buf simplification
  // -------------------
     claim [bufExtractPadding]: <k> runLemma ( #asWord ( ( #range( #buf ( 32 , X ), 0, 28 ) ):Bytes ) ) => doneLemma ( 0 ) ... </k> requires #rangeUInt(32, X)