From 06abe553558b9e77042cd8a5ec1133a3ef558abf Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Wed, 18 Sep 2024 23:46:26 +0200 Subject: [PATCH] correction --- .../kproj/evm-semantics/lemmas/evm-int-simplification.k | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/evm-int-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/evm-int-simplification.k index 6c633d290d..3a16df7834 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/evm-int-simplification.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/evm-int-simplification.k @@ -59,6 +59,7 @@ module EVM-INT-SIMPLIFICATION // Unification: two `#asWord`s rule [asWord-eq-asWord-ml]: { #asWord ( B1 ) #Equals #asWord ( B2 ) } => { true #Equals #asWord ( B1 ) ==Int #asWord ( B2 ) } + requires lengthBytes(B1) <=Int 32 andBool lengthBytes(B2) <=Int 32 [simplification, preserves-definedness] // Unification: `#asWord` and concrete number @@ -70,8 +71,8 @@ module EVM-INT-SIMPLIFICATION [simplification, concrete(X), comm, preserves-definedness] // Unification: `#asWord` and concrete number - rule [asWord-eq-num-ml-l]: { #asWord ( B:Bytes ) #Equals X:Int } => { true #Equals #asWord ( B:Bytes ) ==K X:Int } [simplification, concrete(X), preserves-definedness] - rule [asWord-eq-num-ml-r]: { X:Int #Equals #asWord ( B:Bytes ) } => { true #Equals #asWord ( B:Bytes ) ==K X:Int } [simplification, concrete(X), preserves-definedness] + rule [asWord-eq-num-ml-l]: { #asWord ( B:Bytes ) #Equals X:Int } => { true #Equals #asWord ( B:Bytes ) ==K X:Int } requires lengthBytes(B) <=Int 32 [simplification, concrete(X), preserves-definedness] + rule [asWord-eq-num-ml-r]: { X:Int #Equals #asWord ( B:Bytes ) } => { true #Equals #asWord ( B:Bytes ) ==K X:Int } requires lengthBytes(B) <=Int 32 [simplification, concrete(X), preserves-definedness] // Reduction: we can always remove leading zeros rule [asWord-trim-leading-zeros]: