Rules for substrBytes

k-distribution/include/builtin/domains.k

@@ -865,6 +865,38 @@ module BYTES-SYMBOLIC [symbolic, kast]
   imports BYTES-IN-K
 endmodule
 
+module BYTES-KORE-SYMBOLIC [kore, symbolic]
+  import BYTES-KORE
+
+  rule #Ceil(substrBytes(@B, @START, @END))
+    => { @START <=Int @END #Equals true }
+       #And
+       { lengthBytes(@B) <=Int @END #Equals true }
+       #And #Ceil(@B) #And #Ceil(@START) #And #Ceil(@END)
+    [anywhere]
+
+    rule substrBytes(B, START, END) => B
+      requires START ==Int 0
+       andBool lengthBytes(B) ==Int END
+      [simplification]
+
+    rule substrBytes(B1 +Bytes B2, START, END) => substrBytes(B1, START, END)
+      requires END <=Int lengthBytes(B1)
+      [simplification]
+
+    rule substrBytes(B1 +Bytes B2, START, END) => substrBytes(B2, START -Int lengthBytes(B1), END -Int lengthBytes(B1))
+      requires lengthBytes(B1) <=Int START
+      [simplification]
+
+    rule substrBytes(B1 +Bytes B2, START, END)
+      => substrBytes(B1, START,                               lengthBytes(B1))
+         +Bytes
+         substrBytes(B2, START -Int lengthBytes(B1), END -Int lengthBytes(B1))
+      requires notBool (lengthBytes(B1) >=Int END)
+       andBool notBool (lengthBytes(B1) <=Int START)
+      [simplification]
+endmodule
+
 module BYTES
   imports BYTES-CONCRETE
   imports BYTES-KORE