From bf6f92ffc784fb7ae90d5ce2e386f55cf3adc464 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Fri, 12 Jul 2024 13:50:15 +1000 Subject: [PATCH 1/5] add lemmas without #Equals to int-normalisation --- .../lemmas/int-normalization-lemmas.md | 46 +++++++++++++++++++ 1 file changed, 46 insertions(+) diff --git a/kmxwasm/src/kmxwasm/kdist/mxwasm-semantics/lemmas/int-normalization-lemmas.md b/kmxwasm/src/kmxwasm/kdist/mxwasm-semantics/lemmas/int-normalization-lemmas.md index 87896e5c..287f6010 100644 --- a/kmxwasm/src/kmxwasm/kdist/mxwasm-semantics/lemmas/int-normalization-lemmas.md +++ b/kmxwasm/src/kmxwasm/kdist/mxwasm-semantics/lemmas/int-normalization-lemmas.md @@ -257,6 +257,24 @@ module INT-BIT-NORMALIZATION-LEMMAS [symbolic] => {true #Equals A <=Int fullMask(8) } requires 0 <=Int A andBool A <=Int fullMask(16) [simplification] + + // versions of the above rules that avoid #Equals: + rule 0 ==Int (A &Int B) >>IntTotal C + => 0 ==Int A &Int B + requires B &Int fullMask(C) ==Int 0 + [simplification, concrete(B, C)] + rule 0 ==Int A &Int 4278190080 + => A <=Int fullMask(24) + requires 0 <=Int A andBool A <=Int fullMask(32) + [simplification] + rule 0 ==Int A &Int 16711680 + => A <=Int fullMask(16) + requires 0 <=Int A andBool A <=Int fullMask(24) + [simplification] + rule 0 ==Int A &Int 65280 + => A <=Int fullMask(8) + requires 0 <=Int A andBool A <=Int fullMask(16) + [simplification] endmodule module INT-ARITHMETIC-NORMALIZATION-LEMMAS @@ -399,11 +417,18 @@ module INT-ARITHMETIC-NORMALIZATION-LEMMAS rule {((X +Int Y) modIntTotal M) #Equals ((X +Int Z) modIntTotal M)} => {(Y modIntTotal M) #Equals (Z modIntTotal M)} [simplification] + rule ((X +Int Y) modIntTotal M) ==Int ((X +Int Z) modIntTotal M) + => (Y modIntTotal M) ==Int (Z modIntTotal M) + [simplification] + rule X modIntTotal Y => X requires 0 <=Int X andBool X #Top requires A ==Int B [simplification] + rule (A modIntTotal C) ==Int (B modIntTotal C) => true + requires A ==Int B + [simplification] rule {0 #Equals A ^IntTotal _B} => #Bottom @@ -416,6 +441,22 @@ module INT-ARITHMETIC-NORMALIZATION-LEMMAS requires B =/=Int 0 [simplification(50)] + // ==Int versions of the above rules + rule 0 ==Int A ^IntTotal _B => false + requires A =/=Int 0 + [simplification(40)] + rule A ^IntTotal _B ==Int 0 => false + requires A =/=Int 0 + [simplification(40)] + rule 0 ==Int A ^IntTotal B => 0 ==Int A + requires B =/=Int 0 + [simplification(50)] + + // complementing the above, ^IntTotal is positive if its 1st argument is + rule 0 0 {true #Equals A A Date: Fri, 12 Jul 2024 16:20:09 +1000 Subject: [PATCH 2/5] add lemmas without #Equals to bytes-normalisation and proven-mx lemma files --- .../lemmas/bytes-normalization-lemmas.md | 13 +++++++++++++ .../mxwasm-semantics/lemmas/proven-mx-lemmas.md | 10 ++++++++++ 2 files changed, 23 insertions(+) diff --git a/kmxwasm/src/kmxwasm/kdist/mxwasm-semantics/lemmas/bytes-normalization-lemmas.md b/kmxwasm/src/kmxwasm/kdist/mxwasm-semantics/lemmas/bytes-normalization-lemmas.md index c4ef058f..5afc3bf7 100644 --- a/kmxwasm/src/kmxwasm/kdist/mxwasm-semantics/lemmas/bytes-normalization-lemmas.md +++ b/kmxwasm/src/kmxwasm/kdist/mxwasm-semantics/lemmas/bytes-normalization-lemmas.md @@ -135,6 +135,19 @@ module BYTES-NORMALIZATION-LEMMAS [symbolic] requires lengthBytes(A) >Int 0 [simplification(100)] + rule b"" ==K Int2Bytes(Len:Int, _Value:Int, _E:Endianness) + => 0 ==Int Len + [simplification] + rule b"" ==K Int2Bytes(Value:Int, _E:Endianness, _S:Signedness) + => 0 ==Int Value + [simplification] + rule b"" ==K substrBytesTotal(B:Bytes, Start:Int, End:Int) + => 0 ==Int End -Int Start + requires definedSubstrBytes(B, Start, End) + [simplification] + rule b"" ==K A => false + requires lengthBytes(A) >Int 0 + [simplification(100)] endmodule ``` diff --git a/kmxwasm/src/kmxwasm/kdist/mxwasm-semantics/lemmas/proven-mx-lemmas.md b/kmxwasm/src/kmxwasm/kdist/mxwasm-semantics/lemmas/proven-mx-lemmas.md index 3b774cea..2c50a2e1 100644 --- a/kmxwasm/src/kmxwasm/kdist/mxwasm-semantics/lemmas/proven-mx-lemmas.md +++ b/kmxwasm/src/kmxwasm/kdist/mxwasm-semantics/lemmas/proven-mx-lemmas.md @@ -21,6 +21,12 @@ module PROVEN-MX-LEMMAS rule ( { 1 #Equals #bool ( B:Bool ) }:Bool => { true #Equals B:Bool }:Bool ) [simplification()] + rule 0 ==Int #bool ( B:Bool ) => notBool B + [simplification()] + + rule 1 ==Int #bool ( B:Bool ) => B:Bool + [simplification()] + rule ( size ( _L:List ) >=Int 0 => true ) [smt-lemma, simplification()] @@ -179,6 +185,10 @@ module PROVEN-MX-LEMMAS rule ( { ((X:Int) +Int (Y:Int)) modIntTotal (M:Int) #Equals ((X:Int) +Int (Z:Int)) modIntTotal (M:Int) }:Bool => { (Y:Int) modIntTotal (M:Int) #Equals (Z:Int) modIntTotal (M:Int) }:Bool ) [simplification()] + rule (X +Int Y) modIntTotal M ==Int (X +Int Z) modIntTotal M + => Y modIntTotal M ==Int Z modIntTotal M + [simplification()] + rule ( (X:Int) modIntTotal (Y:Int) => X:Int ) requires ( 0 <=Int X:Int andBool ( X:Int Date: Mon, 15 Jul 2024 16:13:40 +1000 Subject: [PATCH 3/5] add a trivial lemma for int64encoding of boolToInt values --- .../kdist/mxwasm-semantics/lemmas/int-encoding-lemmas.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/kmxwasm/src/kmxwasm/kdist/mxwasm-semantics/lemmas/int-encoding-lemmas.md b/kmxwasm/src/kmxwasm/kdist/mxwasm-semantics/lemmas/int-encoding-lemmas.md index 9f86adee..9eed77ab 100644 --- a/kmxwasm/src/kmxwasm/kdist/mxwasm-semantics/lemmas/int-encoding-lemmas.md +++ b/kmxwasm/src/kmxwasm/kdist/mxwasm-semantics/lemmas/int-encoding-lemmas.md @@ -74,6 +74,9 @@ of the bytes corresponding to `B` values that are `>= 0`, placed on the requires 0 <=Int B1 andBool B1 <=Int 7 [simplification, concrete, preserves-definedness] // All <>Int arguments are >= 0 + rule int64encoding(boolToInt(_), -1, -1, -1, -1, -1, -1, -1, 0) ==Int A => false + requires 1 Date: Mon, 15 Jul 2024 17:50:20 +1000 Subject: [PATCH 4/5] Constrain simplifications for ^IntTotal to have positive exponent --- .../lemmas/int-normalization-lemmas.md | 20 +++++++++++-------- 1 file changed, 12 insertions(+), 8 deletions(-) diff --git a/kmxwasm/src/kmxwasm/kdist/mxwasm-semantics/lemmas/int-normalization-lemmas.md b/kmxwasm/src/kmxwasm/kdist/mxwasm-semantics/lemmas/int-normalization-lemmas.md index 287f6010..376fce3b 100644 --- a/kmxwasm/src/kmxwasm/kdist/mxwasm-semantics/lemmas/int-normalization-lemmas.md +++ b/kmxwasm/src/kmxwasm/kdist/mxwasm-semantics/lemmas/int-normalization-lemmas.md @@ -431,32 +431,36 @@ module INT-ARITHMETIC-NORMALIZATION-LEMMAS [simplification] - rule {0 #Equals A ^IntTotal _B} => #Bottom + rule {0 #Equals A ^IntTotal B} => #Bottom requires A =/=Int 0 + andBool B >=Int 0 [simplification(40)] - rule {A ^IntTotal _B #Equals 0} => #Bottom + rule {A ^IntTotal B #Equals 0} => #Bottom requires A =/=Int 0 + andBool B >=Int 0 [simplification(40)] rule {0 #Equals A ^IntTotal B} => {0 #Equals A} - requires B =/=Int 0 + requires B >Int 0 [simplification(50)] // ==Int versions of the above rules - rule 0 ==Int A ^IntTotal _B => false + rule 0 ==Int A ^IntTotal B => false requires A =/=Int 0 + andBool B >=Int 0 [simplification(40)] - rule A ^IntTotal _B ==Int 0 => false + rule A ^IntTotal B ==Int 0 => false requires A =/=Int 0 + andBool B >=Int 0 [simplification(40)] rule 0 ==Int A ^IntTotal B => 0 ==Int A - requires B =/=Int 0 + requires B >Int 0 [simplification(50)] // complementing the above, ^IntTotal is positive if its 1st argument is - rule 0 0 0 Int 0 [simplification] - rule {0 #Equals A divIntTotal B} => {true #Equals A Date: Tue, 16 Jul 2024 09:34:50 +0000 Subject: [PATCH 5/5] Set Version: 0.1.75 --- kmxwasm/pyproject.toml | 2 +- package/version | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/kmxwasm/pyproject.toml b/kmxwasm/pyproject.toml index 12bb8442..a65dfb96 100644 --- a/kmxwasm/pyproject.toml +++ b/kmxwasm/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kmxwasm" -version = "0.1.74" +version = "0.1.75" description = "Symbolic execution for the MultiversX blockchain with the Wasm semantics, using pyk." authors = [ "Runtime Verification, Inc. ", diff --git a/package/version b/package/version index 21f074df..d9ba7470 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.74 +0.1.75