From 4cc162b05b608f8a0bb985c8989ea3547289f344 Mon Sep 17 00:00:00 2001 From: palinatolmach Date: Thu, 6 Feb 2025 16:49:36 +0400 Subject: [PATCH] Add bytes lookup lemmas --- .../evm-semantics/lemmas/bytes-simplification.k | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k index 00ad215864..909656aace 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k @@ -256,6 +256,23 @@ module BYTES-SIMPLIFICATION [symbolic] requires 0 <=Int S andBool lengthBytes(B1) <=Int S +Int lengthBytes(B2) [simplification(60)] + // Memory lookup + + rule [bytes-concat-lookup-left]: + ( B1:Bytes +Bytes B2:Bytes ) [ I:Int ] => B1 [ I ] + requires 0 <=Int I andBool I 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)] + // lengthBytes rule [lengthBytes-geq-zero]: 0 <=Int lengthBytes ( _ ) => true [simplification, smt-lemma]