diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/slot-updates.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/slot-updates.k index 4167371782..4ba193b550 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/slot-updates.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/slot-updates.k @@ -25,10 +25,12 @@ module SLOT-UPDATES [symbolic] // SHIFT appropriate, and in the latter case, the slot will appear on the LHS of the |Int. // 1. Slot masking using &Int - rule [mask-b-and]: + rule [multimask-b-and]: MASK:Int &Int SLOT:Int => + ( MASK |Int ( 2 ^Int ( 8 *Int ( #getMaskShiftBytes(MASK) +Int #getMaskWidthBytes(MASK) ) ) -Int 1 ) ) + &Int #asWord ( #buf ( 32, SLOT ) [ 32 -Int ( #getMaskShiftBytes(MASK) +Int #getMaskWidthBytes(MASK) ) := #buf ( #getMaskWidthBytes(MASK), 0 ) ] ) - requires #isMask(MASK) andBool #rangeUInt(256, SLOT) + requires 0 <=Int #getMaskShiftBytes(MASK) andBool 0 <=Int #getMaskWidthBytes(MASK) andBool #rangeUInt(256, SLOT) [simplification, concrete(MASK), preserves-definedness] // 2a. |Int and +Bytes, update to be done in left diff --git a/tests/specs/functional/slot-updates-spec.k b/tests/specs/functional/slot-updates-spec.k index 5aa76302ef..6ea887822d 100644 --- a/tests/specs/functional/slot-updates-spec.k +++ b/tests/specs/functional/slot-updates-spec.k @@ -191,4 +191,17 @@ module SLOT-UPDATES-SPEC andBool notBool #asWord ( #range(BA, lengthBytes(BA) -Int (log2Int(X +Int 1) /Int 8), log2Int(X +Int 1) /Int 8) ) <=Int Y andBool X ==Int 2 ^Int ( 8 *Int 5 ) -Int 1 // 5 can be replaced by any number between 0 and 32 + claim [slot-update-14]: + runLemma ( + #asWord ( #range ( + #buf ( 32 , + 80750600743933639278906278912030932992000 |Int + ( 664984632478924800 |Int + ( 115792089237316195423570985008687885552524791327314281033844573408277819293695 &Int + #asWord ( #range ( #buf ( 32 , #lookup ( STORAGE1:Map , 0 ) ) , 0 , 14 ) +Bytes + b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" +Bytes + #range ( #buf ( 32 , #lookup ( STORAGE1:Map , 0 ) ) , 27 , 4 ) +Bytes b"\x02" ) ) ) ) , + 31 , 1 ) ) <=Int 2 ) + => doneLemma ( true ) ... + endmodule