From 7e908d3ada11caa1b44fc370a7b9f7c3083faa8e Mon Sep 17 00:00:00 2001 From: Virgil Date: Wed, 26 Jun 2024 19:11:09 +0300 Subject: [PATCH 01/10] Disable replaceAtB for symbolic inputs --- .../kdist/wasm-semantics/data/sparse-bytes.k | 57 +++++++++++++------ 1 file changed, 41 insertions(+), 16 deletions(-) diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/data/sparse-bytes.k b/pykwasm/src/pykwasm/kdist/wasm-semantics/data/sparse-bytes.k index 595cd85f7..ad68a38ab 100644 --- a/pykwasm/src/pykwasm/kdist/wasm-semantics/data/sparse-bytes.k +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/data/sparse-bytes.k @@ -1,6 +1,5 @@ -module SPARSE-BYTES - imports BOOL +module SPARSE-BYTES-SYNTAX imports BYTES imports INT @@ -9,9 +8,18 @@ module SPARSE-BYTES syntax SBItemChunk ::= SBChunk(SBItem) - + syntax SparseBytes ::= List{SBItemChunk, ""} +endmodule + +module SPARSE-BYTES + imports BOOL + imports REPLACE-AT-CONCRETE + imports REPLACE-AT-SYNTAX + imports REPLACE-AT-SYMBOLIC + imports SPARSE-BYTES-SYNTAX + syntax Bytes ::= unwrap(SparseBytes) [function, total, symbol, klabel(SparseBytes:unwrap)] // ----------------------------------------------------------------- @@ -88,10 +96,6 @@ module SPARSE-BYTES requires 0 <=Int S andBool S <=Int E andBool S .SparseBytes requires S SBChunk(SBI) replaceAt(REST, S -Int size(SBI), Bs) requires size(SBI) <=Int S - - rule replaceAt(SBChunk(#empty(N)) REST, S, Bs) => replaceAtZ(N, REST, S, Bs) - requires S replaceAtB(B, REST, S, Bs) - requires S .SparseBytes @@ -155,8 +152,6 @@ module SPARSE-BYTES andBool lengthBytes(Bs) >Int N - syntax SparseBytes ::= replaceAtB(Bytes, SparseBytes, Int, Bytes) - [function, total, symbol, klabel(SparseBytes:replaceAtB)] // --------------------------------------------------------------- ////////// S + len(Bs) <= len(MB) rule replaceAtB(MB, REST, S, Bs) @@ -190,5 +185,35 @@ module SPARSE-BYTES rule joinUntil(Bs, .SparseBytes, I) => SBChunk(#bytes( padRightBytes(Bs, I, 0) )) requires I >Int lengthBytes(Bs) +endmodule + +module REPLACE-AT-SYNTAX + imports SPARSE-BYTES-SYNTAX + + syntax SparseBytes ::= replaceAt(SparseBytes, Int, Bytes) + [function, total, symbol, klabel(SparseBytes:replaceAt)] + syntax SparseBytes ::= replaceAtZ(Int, SparseBytes, Int, Bytes) + [function, total, symbol, klabel(SparseBytes:replaceAtZ)] + syntax SparseBytes ::= replaceAtB(Bytes, SparseBytes, Int, Bytes) + [function, total, symbol, klabel(SparseBytes:replaceAtB)] +endmodule + +module REPLACE-AT-CONCRETE [concrete] + imports REPLACE-AT-SYNTAX + rule replaceAt(SBChunk(#empty(N)) REST, S, Bs) => replaceAtZ(N, REST, S, Bs) + requires S replaceAtB(B, REST, S, Bs) + requires S replaceAtZ(N, REST, S, Bs) + requires S replaceAtB(B, REST, S, Bs) + requires S Date: Wed, 26 Jun 2024 20:24:45 +0300 Subject: [PATCH 02/10] Add SparseBytes lemmas --- .../kdist/wasm-semantics/kwasm-lemmas.md | 8 +- .../wasm-semantics/symbolic/ceils-syntax.k | 64 + .../kdist/wasm-semantics/symbolic/ceils.k | 476 ++++++++ .../common-sparse-bytes-lemmas.md | 1083 +++++++++++++++++ .../sparse-bytes/get-bytes-range-lemmas.md | 23 + .../symbolic/sparse-bytes/get-range-lemmas.md | 23 + .../sparse-bytes/replace-at-lemmas.md | 79 ++ .../symbolic/sparse-bytes/set-range-lemmas.md | 93 ++ .../sparse-bytes/sparse-bytes-lemmas-basic.md | 210 ++++ .../sparse-bytes/sparse-bytes-lemmas.md | 26 + .../substr-sparse-bytes-lemmas.md | 94 ++ .../kdist/wasm-semantics/symbolic/symbolic.md | 10 + .../wasm-semantics/symbolic/wasm-lemmas.md | 78 ++ 13 files changed, 2266 insertions(+), 1 deletion(-) create mode 100644 pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/ceils-syntax.k create mode 100644 pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/ceils.k create mode 100644 pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/sparse-bytes/common-sparse-bytes-lemmas.md create mode 100644 pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/sparse-bytes/get-bytes-range-lemmas.md create mode 100644 pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/sparse-bytes/get-range-lemmas.md create mode 100644 pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/sparse-bytes/replace-at-lemmas.md create mode 100644 pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/sparse-bytes/set-range-lemmas.md create mode 100644 pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/sparse-bytes/sparse-bytes-lemmas-basic.md create mode 100644 pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/sparse-bytes/sparse-bytes-lemmas.md create mode 100644 pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/sparse-bytes/substr-sparse-bytes-lemmas.md create mode 100644 pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/symbolic.md create mode 100644 pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/wasm-lemmas.md diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/kwasm-lemmas.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/kwasm-lemmas.md index cfb43da1f..7257ff806 100644 --- a/pykwasm/src/pykwasm/kdist/wasm-semantics/kwasm-lemmas.md +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/kwasm-lemmas.md @@ -6,8 +6,14 @@ They are part of the *trusted* base, and so should be scrutinized carefully. ```k requires "wasm-text.md" +requires "symbolic/symbolic.md" -module KWASM-LEMMAS [symbolic] +module KWASM-LEMMAS + imports WASM-SYMBOLIC + imports KWASM-LEMMAS-SYMBOLIC +endmodule + +module KWASM-LEMMAS-SYMBOLIC [symbolic] imports WASM-TEXT imports BYTES-KORE imports INT-SYMBOLIC diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/ceils-syntax.k b/pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/ceils-syntax.k new file mode 100644 index 000000000..720e3a90f --- /dev/null +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/ceils-syntax.k @@ -0,0 +1,64 @@ +module CEILS-SYNTAX + imports BOOL + imports BYTES + imports INT + imports WASM-DATA + + syntax Bool ::= definedSubstrBytes(Bytes, startIndex: Int, endIndex: Int) [function, total] + syntax Bool ::= definedReplaceAtBytes(dest: Bytes, index: Int, src: Bytes) [function, total] + syntax Bool ::= definedPadRightBytes(Bytes, length: Int, value: Int) [function, total] + syntax Bool ::= definedPadLeftBytes(Bytes, length: Int, value: Int) [function, total] + syntax Bool ::= definedModInt(Int, Int) [function, total] + syntax Bool ::= definedDivInt(Int, Int) [function, total] + syntax Bool ::= definedShlInt(Int, Int) [function, total] + syntax Bool ::= definedShrInt(Int, Int) [function, total] + syntax Bool ::= definedPowInt(Int, Int) [function, total] + syntax Bool ::= definedTModInt(Int, Int) [function, total] + syntax Bool ::= definedTDivInt(Int, Int) [function, total] + syntax Bool ::= definedLog2Int(Int) [function, total] + syntax Bool ::= definedProjectBytes(KItem) [function, total] + syntax Bool ::= definedProjectInt(KItem) [function, total] + syntax Bool ::= definedMapLookup(Map, KItem) [function, total] + + syntax Bool ::= definedGetInts(Ints, Int) [function, total] + syntax Bool ::= definedGetElemSegment(ElemSegment, Int) [function, total] + + // --------------------------------------- + + syntax Bytes ::= substrBytesTotal(Bytes, startIndex: Int, endIndex: Int) + [function, total, symbol(substrBytesTotal), no-evaluators] + syntax Bytes ::= replaceAtBytesTotal(dest: Bytes, index: Int, src: Bytes) + [function, total, symbol(replaceAtBytesTotal), no-evaluators] + syntax Bytes ::= padRightBytesTotal(Bytes, length: Int, value: Int) + [function, total, symbol(padRightBytesTotal), no-evaluators] + syntax Bytes ::= padLeftBytesTotal(Bytes, length: Int, value: Int) + [function, total, symbol(padLeftBytesTotal), no-evaluators] + syntax Int ::= Int "modIntTotal" Int + [function, total, symbol(modIntTotal), no-evaluators, smtlib(modIntTotal)] + syntax Int ::= Int "divIntTotal" Int + [function, total, symbol(divIntTotal), no-evaluators, smt-hook(div)] + syntax Int ::= Int "<>IntTotal" Int + [function, total, symbol(shrIntTotal), no-evaluators] + syntax Int ::= Int "^IntTotal" Int + [function, total, symbol(powIntTotal), no-evaluators] + syntax Int ::= Int "%IntTotal" Int + [function, total, symbol(tModIntTotal), no-evaluators, smtlib(tModInt)] + syntax Int ::= Int "/IntTotal" Int + [function, total, symbol(tDivIntTotal), no-evaluators, smtlib(tDivInt)] + syntax Int ::= log2IntTotal(Int) + [ function, total, symbol(log2IntTotal), no-evaluators, + smtlib(log2IntTotal) + ] + syntax Bytes ::= projectBytesTotal(KItem) + [function, total, symbol(projectBytesTotal), no-evaluators] + syntax Int ::= projectIntTotal(KItem) + [function, total, symbol(projectIntTotal), no-evaluators] + + + syntax Int ::= #getIntsTotal(Ints, Int) + [function, total, symbol(#getIntsTotal), no-evaluators/*, smtlib(poundGetInts)*/] + syntax Index ::= #getElemSegmentTotal(ElemSegment, Int) + [function, total, symbol(#getElemSegmentTotal), no-evaluators] +endmodule \ No newline at end of file diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/ceils.k b/pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/ceils.k new file mode 100644 index 000000000..2caf7889a --- /dev/null +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/ceils.k @@ -0,0 +1,476 @@ +requires "ceils-syntax.k" + +module CEILS + imports BOOL + imports BYTES + imports CEILS-SYNTAX + imports INT + + rule definedSubstrBytes(B:Bytes, StartIndex:Int, EndIndex:Int) + => (0 <=Int StartIndex) andBool (0 <=Int EndIndex) + andBool (EndIndex <=Int lengthBytes(B)) + andBool (StartIndex <=Int EndIndex) + + + rule definedReplaceAtBytes(Dest:Bytes, Index:Int, Src:Bytes) + => (0 <=Int Index) + andBool (Index +Int lengthBytes(Src) <=Int lengthBytes(Dest)) + + + rule definedPadRightBytes(_B:Bytes, Length:Int, Value:Int) + => (0 <=Int Length) + andBool (0 <=Int Value) + andBool (Value <=Int 255) + + + rule definedPadLeftBytes(_B:Bytes, Length:Int, Value:Int) + => (0 <=Int Length) + andBool (0 <=Int Value) + andBool (Value <=Int 255) + + + // --------------------------------------- + + + rule #Ceil(substrBytes(@Arg0:Bytes, @StartIndex:Int, @EndIndex:Int)) + => ((({ definedSubstrBytes(@Arg0, @StartIndex, @EndIndex) #Equals true } + #And #Ceil(@Arg0)) + #And #Ceil(@StartIndex)) + #And #Ceil(@EndIndex)) + [simplification] + + + rule substrBytesTotal(Arg0:Bytes, StartIndex:Int, EndIndex:Int) + => substrBytes(Arg0, StartIndex, EndIndex) + requires definedSubstrBytes(Arg0, StartIndex, EndIndex) + [concrete, simplification(10), preserves-definedness] + + rule substrBytes(Arg0:Bytes, StartIndex:Int, EndIndex:Int) + => substrBytesTotal(Arg0, StartIndex, EndIndex) + requires definedSubstrBytes(Arg0, StartIndex, EndIndex) + [symbolic(Arg0), simplification, preserves-definedness] + + rule substrBytes(Arg0:Bytes, StartIndex:Int, EndIndex:Int) + => substrBytesTotal(Arg0, StartIndex, EndIndex) + requires definedSubstrBytes(Arg0, StartIndex, EndIndex) + [symbolic(StartIndex), simplification, preserves-definedness] + + rule substrBytes(Arg0:Bytes, StartIndex:Int, EndIndex:Int) + => substrBytesTotal(Arg0, StartIndex, EndIndex) + requires definedSubstrBytes(Arg0, StartIndex, EndIndex) + [symbolic(EndIndex), simplification, preserves-definedness] + + + + rule #Ceil(replaceAtBytes(@Dest:Bytes, @Index:Int, @Src:Bytes)) + => ((({ definedReplaceAtBytes(@Dest, @Index, @Src) #Equals true } + #And #Ceil(@Dest)) + #And #Ceil(@Index)) + #And #Ceil(@Src)) + [simplification] + + rule replaceAtBytesTotal(Dest:Bytes, Index:Int, Src:Bytes) + => replaceAtBytes(Dest, Index, Src) + requires definedReplaceAtBytes(Dest, Index, Src) + [concrete, simplification(10), preserves-definedness] + + rule replaceAtBytes(Dest:Bytes, Index:Int, Src:Bytes) + => replaceAtBytesTotal(Dest, Index, Src) + requires definedReplaceAtBytes(Dest, Index, Src) + [symbolic(Dest), simplification, preserves-definedness] + + rule replaceAtBytes(Dest:Bytes, Index:Int, Src:Bytes) + => replaceAtBytesTotal(Dest, Index, Src) + requires definedReplaceAtBytes(Dest, Index, Src) + [symbolic(Index), simplification, preserves-definedness] + + rule replaceAtBytes(Dest:Bytes, Index:Int, Src:Bytes) + => replaceAtBytesTotal(Dest, Index, Src) + requires definedReplaceAtBytes(Dest, Index, Src) + [symbolic(Src), simplification, preserves-definedness] + + + rule #Ceil(padRightBytes(@Arg0:Bytes, @Length:Int, @Value:Int)) + => ((({ definedPadRightBytes(@Arg0, @Length, @Value) #Equals true } + #And #Ceil(@Arg0)) + #And #Ceil(@Length)) + #And #Ceil(@Value)) + [simplification] + + rule padRightBytesTotal(Arg0:Bytes, Length:Int, Value:Int) + => padRightBytes(Arg0, Length, Value) + requires definedPadRightBytes(Arg0, Length, Value) + [concrete, simplification(10), preserves-definedness] + + rule padRightBytes(Arg0:Bytes, Length:Int, Value:Int) + => padRightBytesTotal(Arg0, Length, Value) + requires definedPadRightBytes(Arg0, Length, Value) + [symbolic(Arg0), simplification, preserves-definedness] + + rule padRightBytes(Arg0:Bytes, Length:Int, Value:Int) + => padRightBytesTotal(Arg0, Length, Value) + requires definedPadRightBytes(Arg0, Length, Value) + [symbolic(Length), simplification, preserves-definedness] + + rule padRightBytes(Arg0:Bytes, Length:Int, Value:Int) + => padRightBytesTotal(Arg0, Length, Value) + requires definedPadRightBytes(Arg0, Length, Value) + [symbolic(Value), simplification, preserves-definedness] + + + rule #Ceil(padLeftBytes(@Arg0:Bytes, @Length:Int, @Value:Int)) + => ((({ definedPadLeftBytes(@Arg0, @Length, @Value) #Equals true } + #And #Ceil(@Arg0)) + #And #Ceil(@Length)) + #And #Ceil(@Value)) + [simplification] + + rule padLeftBytesTotal(Arg0:Bytes, Length:Int, Value:Int) + => padLeftBytes(Arg0, Length, Value) + requires definedPadLeftBytes(Arg0, Length, Value) + [concrete, simplification(10), preserves-definedness] + + rule padLeftBytes(Arg0:Bytes, Length:Int, Value:Int) + => padLeftBytesTotal(Arg0, Length, Value) + requires definedPadLeftBytes(Arg0, Length, Value) + [symbolic(Arg0), simplification, preserves-definedness] + + rule padLeftBytes(Arg0:Bytes, Length:Int, Value:Int) + => padLeftBytesTotal(Arg0, Length, Value) + requires definedPadLeftBytes(Arg0, Length, Value) + [symbolic(Length), simplification, preserves-definedness] + + rule padLeftBytes(Arg0:Bytes, Length:Int, Value:Int) + => padLeftBytesTotal(Arg0, Length, Value) + requires definedPadLeftBytes(Arg0, Length, Value) + [symbolic(Value), simplification, preserves-definedness] + + + //---------------------------------- + + + rule definedModInt (_:Int, X:Int) => X =/=Int 0 + + rule #Ceil(@Arg0:Int modInt @Arg1:Int) + => (({ definedModInt(@Arg0, @Arg1) #Equals true } + #And #Ceil(@Arg0)) + #And #Ceil(@Arg1)) + [simplification] + + rule _ modIntTotal 0 => 0 + + rule Arg0:Int modIntTotal Arg1:Int + => Arg0 modInt Arg1 + requires definedModInt(Arg0, Arg1) + [concrete, simplification(10), preserves-definedness] + + rule Arg0:Int modInt Arg1:Int + => Arg0 modIntTotal Arg1 // Arg0 modIntTotal Arg1 + requires definedModInt(Arg0, Arg1) + [symbolic(Arg0), simplification, preserves-definedness] + + rule Arg0:Int modInt Arg1:Int + => Arg0 modIntTotal Arg1 // Arg0 modIntTotal Arg1 + requires definedModInt(Arg0, Arg1) + [symbolic(Arg1), simplification, preserves-definedness] + + //---------------------------------- + + + rule definedDivInt (_:Int, X:Int) => X =/=Int 0 + + rule #Ceil(@Arg0:Int divInt @Arg1:Int) + => (({ definedDivInt(@Arg0, @Arg1) #Equals true } + #And #Ceil(@Arg0)) + #And #Ceil(@Arg1)) + [simplification, preserves-definedness] + + rule _ divIntTotal 0 => 0 + + rule Arg0:Int divIntTotal Arg1:Int + => Arg0 divInt Arg1 + requires definedDivInt(Arg0, Arg1) + [concrete, simplification(10), preserves-definedness] + + rule Arg0:Int divInt Arg1:Int + => Arg0 divIntTotal Arg1 + requires definedDivInt(Arg0, Arg1) + [symbolic(Arg0), simplification, preserves-definedness] + + rule Arg0:Int divInt Arg1:Int + => Arg0 divIntTotal Arg1 + requires definedDivInt(Arg0, Arg1) + [symbolic(Arg1), simplification, preserves-definedness] + + //---------------------------------- + + rule definedShlInt(_:Int, I:Int) => I >=Int 0 + + rule Arg0:Int < Arg0 < Arg0 < Arg0 < I >=Int 0 + + rule Arg0:Int >>IntTotal Arg1:Int + => Arg0 >>Int Arg1 + requires definedShrInt(Arg0, Arg1) + [concrete, simplification(10), preserves-definedness] + + rule Arg0:Int >>Int Arg1:Int + => Arg0 >>IntTotal Arg1 + requires definedShrInt(Arg0, Arg1) + [symbolic(Arg0), simplification, preserves-definedness] + + rule Arg0:Int >>Int Arg1:Int + => Arg0 >>IntTotal Arg1 + requires definedShrInt(Arg0, Arg1) + [symbolic(Arg1), simplification, preserves-definedness] + + + //------------------------------------- + + + rule definedPowInt(A:Int, B:Int) => A =/=Int 0 orBool B =/=Int 0 + + rule #Ceil(Arg0:Int ^Int Arg1:Int) + => { definedPowInt(Arg0, Arg1) #Equals true } + [simplification] + + rule Arg0:Int ^IntTotal Arg1:Int + => Arg0 ^Int Arg1 + requires definedPowInt(Arg0, Arg1) + [concrete, simplification(10), preserves-definedness] + + rule Arg0:Int ^Int Arg1:Int + => Arg0 ^IntTotal Arg1 + requires definedPowInt(Arg0, Arg1) + [symbolic(Arg0), simplification, preserves-definedness] + + rule Arg0:Int ^Int Arg1:Int + => Arg0 ^IntTotal Arg1 + requires definedPowInt(Arg0, Arg1) + [symbolic(Arg1), simplification, preserves-definedness] + + + //------------------------------------- + + + rule definedTModInt(_:Int, Y:Int) => Y =/=Int 0 + + rule #Ceil(@Arg0:Int %Int @Arg1:Int) + => (({ definedTModInt(@Arg0, @Arg1) #Equals true } + #And #Ceil(@Arg0)) + #And #Ceil(@Arg1)) + [simplification] + + rule Arg0:Int %IntTotal Arg1:Int + => Arg0 %Int Arg1 + requires definedTModInt(Arg0, Arg1) + [concrete, simplification(10), preserves-definedness] + + rule Arg0:Int %Int Arg1:Int + => Arg0 %IntTotal Arg1 + requires definedTModInt(Arg0, Arg1) + [symbolic(Arg0), simplification, preserves-definedness] + + rule Arg0:Int %Int Arg1:Int + => Arg0 %IntTotal Arg1 + requires definedTModInt(Arg0, Arg1) + [symbolic(Arg1), simplification, preserves-definedness] + + + //------------------------------------- + + + rule definedTDivInt(_:Int, Y:Int) => Y =/=Int 0 + + rule #Ceil(@Arg0:Int /Int @Arg1:Int) + => (({ definedTDivInt(@Arg0, @Arg1) #Equals true } + #And #Ceil(@Arg0)) + #And #Ceil(@Arg1)) + [simplification] + + rule Arg0:Int /IntTotal Arg1:Int + => Arg0 /Int Arg1 + requires definedTDivInt(Arg0, Arg1) + [concrete, simplification(10), preserves-definedness] + + rule Arg0:Int /Int Arg1:Int + => Arg0 /IntTotal Arg1 + requires definedTDivInt(Arg0, Arg1) + [symbolic(Arg0), simplification, preserves-definedness] + + rule Arg0:Int /Int Arg1:Int + => Arg0 /IntTotal Arg1 + requires definedTDivInt(Arg0, Arg1) + [symbolic(Arg1), simplification, preserves-definedness] + + + //------------------------------------- + + + rule definedLog2Int (X:Int) => 0 {true #Equals definedLog2Int(X)} + [simplification] + + rule log2IntTotal(Arg0:Int) + => log2Int(Arg0) + requires definedLog2Int(Arg0) + [concrete, simplification(10), preserves-definedness] + + rule log2Int(Arg0:Int) + => log2IntTotal(Arg0) + requires definedLog2Int(Arg0) + [symbolic(Arg0), simplification, preserves-definedness] + + + //------------------------------------- + + rule definedGetElemSegment(Es:ElemSegment, I:Int) + => 0 <=Int I andBool I <=Int #lenElemSegment(Es) + + rule #Ceil(#getElemSegment(@Arg0:ElemSegment, @Arg1:Int)) + => (({ definedGetElemSegment(@Arg0, @Arg1) #Equals true } + #And #Ceil(@Arg0)) + #And #Ceil(@Arg1)) + [simplification] + + rule #getElemSegmentTotal(Arg0:ElemSegment, Arg1:Int) + => #getElemSegment(Arg0, Arg1) + requires definedGetElemSegment(Arg0, Arg1) + [concrete, simplification(10), preserves-definedness] + + rule #getElemSegment(Arg0:ElemSegment, Arg1:Int) + => #getElemSegmentTotal(Arg0, Arg1) + requires definedGetElemSegment(Arg0, Arg1) + [symbolic(Arg0), simplification, preserves-definedness] + + rule #getElemSegment(Arg0:ElemSegment, Arg1:Int) + => #getElemSegmentTotal(Arg0, Arg1) + requires definedGetElemSegment(Arg0, Arg1) + [symbolic(Arg1), simplification, preserves-definedness] + + //------------------------------------- + + rule definedGetInts(Is:Ints, I:Int) + => 0 <=Int I andBool I <=Int #lenInts(Is) + + rule #Ceil(#getInts(@Arg0:Ints, @Arg1:Int)) + => (({ definedGetInts(@Arg0, @Arg1) #Equals true } + #And #Ceil(@Arg0)) + #And #Ceil(@Arg1)) + [simplification] + + rule #getIntsTotal(Arg0:Ints, Arg1:Int) + => #getInts(Arg0, Arg1) + requires definedGetInts(Arg0, Arg1) + [concrete, simplification(10), preserves-definedness] + + rule #getInts(Arg0:Ints, Arg1:Int) + => #getIntsTotal(Arg0, Arg1) + requires definedGetInts(Arg0, Arg1) + [symbolic(Arg0), simplification, preserves-definedness] + + rule #getInts(Arg0:Ints, Arg1:Int) + => #getIntsTotal(Arg0, Arg1) + requires definedGetInts(Arg0, Arg1) + [symbolic(Arg1), simplification, preserves-definedness] + + + // ------------------------------------ + + rule #Ceil({@Arg0:KItem}:>Bytes) + => ({ definedProjectBytes(@Arg0) #Equals true } + #And #Ceil(@Arg0)) + [simplification] + + rule definedProjectBytes(K:KItem) => isBytes(K) + + + rule projectBytesTotal(Arg0:KItem) + => {Arg0}:>Bytes + requires definedProjectBytes(Arg0) + [concrete, simplification(10), preserves-definedness] + + rule {Arg0:KItem}:>Bytes + => projectBytesTotal(Arg0) + requires definedProjectBytes(Arg0) + [symbolic(Arg0), simplification, preserves-definedness] + + rule projectBytesTotal(Arg0:Bytes) + => Arg0 + [simplification] + + // ------------------------------------ + + rule #Ceil({@Arg0:KItem}:>Int) + => ({ definedProjectInt(@Arg0) #Equals true } + #And #Ceil(@Arg0)) + [simplification] + + rule definedProjectInt(K:KItem) => isInt(K) + + + rule projectIntTotal(Arg0:KItem) + => {Arg0}:>Int + requires definedProjectInt(Arg0) + [concrete, simplification(10), preserves-definedness] + + rule {Arg0:KItem}:>Int + => projectIntTotal(Arg0) + requires definedProjectInt(Arg0) + [symbolic(Arg0), simplification, preserves-definedness] + + + // ----------------------------------- + + rule definedMapLookup(M:Map, Key:KItem) => Key in_keys(M) + + rule M:Map[Key:KItem] orDefault _:KItem + => M[Key] + requires definedMapLookup(M, Key) + [concrete, simplification(10), preserves-definedness] + rule M:Map[Key:KItem] + => M[Key] orDefault 0 + requires definedMapLookup(M, Key) + [symbolic(M), simplification, preserves-definedness] + rule M:Map[Key:KItem] + => M[Key] orDefault 0 + requires definedMapLookup(M, Key) + [symbolic(Key), simplification, preserves-definedness] + + + // ----------------------------------- + + rule #Ceil(#signed(@T:IValType, @N:Int)) + => {0 <=Int @N andBool @N I divIntTotal J requires 0 I modIntTotal J requires 0 true + rule empty(SBChunk(#bytes(B)) _SB:SparseBytes) => false requires lengthBytes(B) >Int 0 + rule empty(SBChunk(#bytes(B)) SB:SparseBytes) => empty(SB) requires lengthBytes(B) ==Int 0 + rule empty(SBChunk(#empty(N)) _SB:SparseBytes) => false requires N >Int 0 + rule empty(SBChunk(#empty(N)) SB:SparseBytes) => empty(SB) requires N <=Int 0 +endmodule + +module COMMON-SPARSE-BYTES-LEMMAS-SYMBOLIC [symbolic] + imports COMMON-SPARSE-BYTES-LEMMAS-SYNTAX + + rule empty(concat(SB1, _SB2)) => false requires notBool empty(SB1) [simplification] + rule empty(concat(SB1, SB2)) => empty(SB2) requires empty(SB1) [simplification] + rule empty(merge(SB1, _SB2)) => false requires notBool empty(SB1) [simplification] + rule empty(merge(SB1, SB2)) => empty(SB2) requires empty(SB1) [simplification] + rule empty(updateSparseBytes(_Fn:SBSetFunction, SB:SparseBytes, Start:Int, Width:Int)) => false + requires (0 <=Int Start) + andBool (notBool empty(SB) orBool 0 true + requires 0 <=Int Start + andBool empty(SB) andBool 0 ==Int Width + [simplification] +endmodule + +module SPLIT-SPARSE-BYTES [symbolic] + imports COMMON-SPARSE-BYTES-LEMMAS-SYNTAX + +``` + +We have the following goals: +* All functions must be well defined, i.e. they must evaluate to values that + depend only on the values passed as arguments, and not on the unevaluated + functions present in the arguments. +* Evaluate `canSplitSparseBytes` to `true` only for arguments for which + `splitSparseBytesFunction` will fully evaluate + +The first goal can be achieved by having `canSplitSparseBytes` as a function +that is always true (but may stay unevaluated sometimes), and having +`splitSparseBytesFunction` always equal to the first argument (may also +stay unevaluated sometimes). + +We achieve the second goal by having an additional `splitSparseBytes` function +that takes three arguments: a suffix, a prefix, and an Addr. This function +is equal to the concatenation of the suffix and the prefix, but is never +actually evaluated. Instead, it changes its internal representation by moving +bytes from the suffix to the prefix, and removing the size of those bytes from +Addr, until the addr becomes 0 (if possible). + +Then we can evaluate `canSplitSparseBytes(..., Addr)` to +`#canSplitSparseBytes(... splitSparseBytes(..., Addr) ...)` and then evaluate +`#canSplitSparseBytes(... splitSparseBytes(..., Addr=0) ...)` to `true`, as +sown below, in order to see if we can split the given bytes in a prefix and a +suffix at the exact `Addr` point. + +In a similar way, we can evaluate `splitSparseBytesFunction(...)` to +`#splitSparseBytesFunction(... splitSparseBytes(...) ...)` and then evaluate +`#splitSparseBytesFunction(... splitSparseBytes(...) ...)` to an actual split. + +Using exactly the same `splitSparseBytes(...)` call for both +`canSplitSparseBytes` and `splitSparseBytesFunction`, together with a requires +clause that is more restrictive for `canSplitSparseBytes` ensures that +`splitSparseBytesFunction` will always fully evaluate. + +```k + + rule canSplitSparseBytes(_F:SBSetFunction, SB, Addr, InnerAddr:Int, InnerWidth:Int) + => #canSplitSparseBytes(SB, splitSparseBytes(SB, .SparseBytes, Addr)) + requires 0 true + requires 0 #splitSparseBytesFunction( + Function, ToSplit, splitSparseBytes(ToSplit, .SparseBytes, Addr), Addr + ) + requires InnerAddr +Int InnerWidth <=Int Addr + rule #splitSparseBytesFunction( + updateSparseBytes(Fn:SBSetFunction, _:SparseBytes, Addr:Int, Width:Int), + _:SparseBytes, + splitSparseBytes(Suffix:SparseBytes, Prefix:SparseBytes, 0), + _:Int + ) + => concat(updateSparseBytes(Fn, Prefix, Addr, Width), Suffix) + requires Addr +Int Width <=Int size(Prefix) + [simplification] + + + rule splitSparseBytes(SBI:SBItemChunk SB:SparseBytes, Prefix:SparseBytes, Addr:Int) + => splitSparseBytes(SB, concat(Prefix, SBI), Addr -Int size(SBI)) + requires size(SBI) <=Int Addr + [simplification] + rule splitSparseBytes(concat(SB1:SparseBytes, SB2:SparseBytes), Prefix:SparseBytes, Addr:Int) + => splitSparseBytes(SB2, concat(Prefix, SB1), Addr -Int size(SB1)) + requires size(SB1) <=Int Addr + [simplification] + rule splitSparseBytes(merge(SB1, SB2:SparseBytes), Prefix:SparseBytes, Addr:Int) + => splitSparseBytes(SB2, concat(Prefix, SB1), Addr -Int size(SB1)) + requires size(SB1) <=Int Addr + [simplification] + + rule splitSparseBytes(SBChunk(#bytes(A +Bytes B)) SB:SparseBytes, Prefix:SparseBytes, Addr:Int) + => splitSparseBytes(SBChunk(#bytes(B)) SB, concat(Prefix, SBChunk(#bytes(A))), Addr -Int lengthBytes(A)) + requires lengthBytes(A) <=Int Addr + [simplification] + + rule splitSparseBytes(SBChunk(#bytes(A +Bytes B)) SB:SparseBytes, Prefix:SparseBytes, Addr:Int) + => splitSparseBytes(SBChunk(#bytes(A)) SBChunk(#bytes(B)) SB, Prefix, Addr) + requires 0 splitSparseBytes + ( SBChunk(#bytes(substrBytes(A, Addr, lengthBytes(A)))) + SB + , concat(Prefix, SBChunk(#bytes(substrBytes(A, 0, Addr)))) + , 0 + ) + requires 0 splitSparseBytes + ( SBChunk(#empty(A -Int Addr)) + SB + , concat(Prefix, SBChunk(#empty(Addr))) + , 0 + ) + requires 0 splitSparseBytes + ( splitSparseBytesFunction + ( updateSparseBytes(F, SB, AddrF, WidthF) + , F, SB, Addr, AddrF, WidthF + ) + , Prefix, Addr + ) + requires canSplitSparseBytes(F, SB, Addr, AddrF, WidthF) + [simplification] + + + rule size(updateSparseBytes(Fn:SBSetFunction, SB:SparseBytes, Start:Int, Width:Int)) + => updateSparseBytesSize(Fn, size(SB), Start, Width) + [simplification] +endmodule + +module UPDATE-SPARSE-BYTES-LEMMAS [symbolic] + imports COMMON-SPARSE-BYTES-LEMMAS-SYNTAX + +``` + Evaluation schema for simplifying the basic SB representation + Arguments: F, SB, Start, Len + + *This is not fully implemented.* + + * SB = .SparseBytes + - replace SB with zeros + * SB = chunk SB' + * size(chunk) <= start + - move the chunk before the update (1) + * start < size(chunk) + * SB' = .SparseBytes + * size(chunk) < start + width + - add zeros at the end of the SB / + * start + width <= size(chunk) + * 0 < start + * chunk = #bytes(A) + * concrete(A, Start) + - high priority rule to remove the prefix + * A = B + C + * len(B) <= start + - remove + * start < len(B) + * start + width <= len(B) + - remove end + * len(B) < start + width + * concrete(B, Start) + - high priority rule to remove the start + * give up + * otherwise + - give up + * chunk = #empty(A) + - remove the prefix + * 0 == start + * chunk = #bytes(A) + * start + width = len(A) + - return result + * start + width < len(A) + * concrete(A, Width) + - high priority rule to split + * A = B + C + * Width <= len(B) + - split + * len(B) < width + - give up + * otherwise + - give up + * chunk = #empty(A) + * start + width = A + - return result + * start + width < A + - split + * SB' = chunk2 SB''' + * start + width <= size(chunk) + - remove SB' (2) + * size(chunk) < start + width + * chunk = #bytes(A) + * chunk2 = #bytes(B) + - concatenate A + B + - with high priority, if s+w concat( + SBI, + updateSparseBytes(F, SB, Start -Int size(SBI), Width)) + requires functionSparseBytesWellDefined(F, Start, Width) + andBool size(SBI) <=Int Start + [simplification] + rule updateSparseBytes( + F:SBSetFunction, + SBI:SBItemChunk SB:SparseBytes, + Start:Int, Width:Int) + => concat( + updateSparseBytes(F, SBI, Start, Width), + SB + ) + requires functionSparseBytesWellDefined(F, Start, Width) + andBool Start +Int Width <=Int size(SBI) + andBool notBool empty(SB) + [simplification] + + rule updateSparseBytes( + F:SBSetFunction, + SBChunk(#bytes(A)) SB:SparseBytes, + Start:Int, Width:Int) + => concat( + SBChunk(#bytes(substrBytes(A, 0, Start))), + updateSparseBytes + ( F + , SBChunk(#bytes(substrBytes(A, Start, lengthBytes(A)))) + SB + , 0, Width + ) + ) + requires functionSparseBytesWellDefined(F, Start, Width) + andBool Start concat( + SBChunk(#empty(Start)), + updateSparseBytes + ( F + , SBChunk(#empty(A -Int Start)) + SB + , 0, Width + ) + ) + requires functionSparseBytesWellDefined(F, Start, Width) + andBool Start updateSparseBytes(F, SBChunk(#bytes(A +Bytes B)) SB, 0, Width) + requires functionSparseBytesWellDefined(F, 0, Width) + andBool lengthBytes(A) updateSparseBytes(F, SBChunk(#bytes(A +Bytes B)) SB, Start, Width) + requires functionSparseBytesWellDefined(F, Start, Width) + andBool 0 updateSparseBytes + ( F + , SBChunk(#bytes(A +Bytes zeros(Start +Int Width -Int lengthBytes(A)))) + SBChunk(#empty(lengthBytes(A) +Int B -Int (Start +Int Width))) + SB + , Start, Width + ) + requires functionSparseBytesWellDefined(F, Start, Width) + andBool Start updateSparseBytes + ( F + , SBChunk(#bytes(A +Bytes zeros(B))) + SB + , Start, Width + ) + requires functionSparseBytesWellDefined(F, Start, Width) + andBool Start updateSparseBytes + ( F + , SBChunk(#bytes(zeros(A))) + SB + , 0, Width + ) + requires functionSparseBytesWellDefined(F, 0, Width) + andBool 0 concat( + updateSparseBytes(F, SBChunk(#bytes(A)), Start, Width), + SBChunk(#bytes(B)) + ) + requires functionSparseBytesWellDefined(F, Start, Width) + andBool Start +Int Width <=Int lengthBytes(A) + [simplification] + rule updateSparseBytes( + F:SBSetFunction, + SBChunk(#bytes(A +Bytes B)), + Start:Int, Width:Int) + => concat( + SBChunk(#bytes(A)), + updateSparseBytes(F, SBChunk(#bytes(B)), Start -Int lengthBytes(A), Width) + ) + requires functionSparseBytesWellDefined(F, Start, Width) + andBool lengthBytes(A) <=Int Start + [simplification] + rule updateSparseBytes( + F:SBSetFunction, + SBChunk(#bytes(A +Bytes B)), + Start:Int, Width:Int) + => concat( + SBChunk(#bytes(substrBytes(A, 0, Start))), + updateSparseBytes(F, SBChunk(#bytes(substrBytes(A, Start, lengthBytes(A)) +Bytes B)), 0, Width) + ) + requires functionSparseBytesWellDefined(F, Start, Width) + andBool 0 concat( + SBChunk(#bytes(substrBytes(A, 0, Start))), + updateSparseBytes(F, SBChunk(#bytes(substrBytes(A, Start, lengthBytes(A)))), 0, Width) + ) + requires functionSparseBytesWellDefined(F, Start, Width) + andBool 0 concat( + updateSparseBytes(F, SBChunk(#bytes(substrBytes(A, 0, Width))), 0, Width), + SBChunk(#bytes(substrBytes(A, Width, lengthBytes(A)))) + ) + requires functionSparseBytesWellDefined(F, 0, Width) + andBool Width updateSparseBytes( + // F, splitSparseBytesItemNoFunction(SB, Width)), + // 0, Width + // ) + // requires functionSparseBytesWellDefined(F, 0, Width) + // andBool Width concat( + SBChunk(#empty(Start)), + updateSparseBytes(F, SBChunk(#empty(A -Int Start)), 0, Width) + ) + requires functionSparseBytesWellDefined(F, Start, Width) + andBool 0 concat( + updateSparseBytes(F, SBChunk(#empty(Width)), 0, Width), + SBChunk(#empty(A -Int Width)) + ) + requires functionSparseBytesWellDefined(F, 0, Width) + andBool 0 concat( + SB1, + updateSparseBytes(F, SB2, Start -Int size(SB1), Width)) + requires functionSparseBytesWellDefined(F, Start, Width) + andBool size(SB1) <=Int Start + [simplification] + rule updateSparseBytes( + F:SBSetFunction, + concat(SB1:SparseBytes, SB2:SparseBytes), + Start:Int, Width:Int) + => concat( + updateSparseBytes(F, SB1, Start, Width), + SB2) + requires functionSparseBytesWellDefined(F, Start, Width) + andBool Start +Int Width <=Int size(SB1) + [simplification] + + rule updateSparseBytes( + F:SBSetFunction, + merge(SB1, SB2:SparseBytes), + Start:Int, Width:Int) + => merge( + SB1, + updateSparseBytes(F, SB2, Start -Int size(SB1), Width)) + requires functionSparseBytesWellDefined(F, Start, Width) + andBool size(SB1) <=Int Start + [simplification] + rule updateSparseBytes( + F:SBSetFunction, + merge(SB1, SB2:SparseBytes), + Start:Int, Width:Int) + => concat( + updateSparseBytes(F, SB1, Start, Width), + SB2) + requires functionSparseBytesWellDefined(F, Start, Width) + andBool Start +Int Width <=Int size(SB1) + [simplification] + + rule updateSparseBytes( + F:SBSetFunction, + merge(SBChunk(#empty(B)), SB2:SparseBytes), + Start:Int, Width:Int) + => concat( + SBChunk(#empty(Start)), + updateSparseBytes( + F:SBSetFunction, + merge( + SBChunk(#empty(B -Int Start)), + SB2:SparseBytes + ), + 0, Width) + ) + requires functionSparseBytesWellDefined(F, Start, Width) + andBool Start updateSparseBytes( + F:SBSetFunction, + merge( + SBChunk(#bytes(B +Bytes zeros(Start +Int Width -Int lengthBytes(B)))), + merge( + SBChunk(#empty(A +Int lengthBytes(B) -Int Start -Int Width)), + SB2:SparseBytes + ) + ), + Start:Int, Width:Int) + requires functionSparseBytesWellDefined(F, Start, Width) + andBool Start updateSparseBytes( + F:SBSetFunction, + merge(SBChunk(#bytes(B +Bytes zeros(A))), SB2:SparseBytes), + Start:Int, Width:Int) + requires functionSparseBytesWellDefined(F, Start, Width) + andBool Start merge( + SBChunk(#bytes(A)), + updateSparseBytes( + F:SBSetFunction, + merge(SBChunk(#bytes(B)), SB), + Start -Int lengthBytes(A), Width)) + requires functionSparseBytesWellDefined(F, Start, Width) + andBool lengthBytes(A) <=Int Start + andBool Start updateSparseBytes( + F1, + splitSparseBytesFunction( + updateSparseBytes(F2, SB, Start2, Width2), + F2, SB, Start1, Start2, Width2 + ), + Start1, Width1) + requires disjontRanges(Start1, Width1, Start2, Width2) + andBool canSplitSparseBytes(F2, SB, Start1, Start2, Width2) + [simplification] + + // ---------------------------- + // Included ranges cancelling + // ---------------------------- + + rule updateSparseBytes( + F1:SBSetFunction, + updateSparseBytes( + _F2:SBSetFunction, + SB:SparseBytes, + Start2:Int, Width2:Int), + Start1:Int, Width1:Int) + => updateSparseBytes(F1, SB, Start1, Width1) + requires Start1 <=Int Start2 andBool Start2 +Int Width2 <=Int Start1 +Int Width1 + // Assumes that an update over the larger range cancels the narrower range. + [simplification] + + // ---------------------------- + // Overlapping ranges + // ---------------------------- + + // Not implemented yet +endmodule + +module EXTRACT-SPARSE-BYTES-LEMMAS + imports COMMON-SPARSE-BYTES-LEMMAS-SYNTAX + + // Final extraction + // rule extractSparseBytes( + // F:SBGetFunction, SB:SparseBytes, 0, Len + // ) => SB + // requires Len ==Int size(SB) + // [simplification] + + + // ------------------------------------------ + // Simplify concatenation - ignore first + // ------------------------------------------ + rule extractSparseBytes( + F:SBGetFunction, + SBI:SBItemChunk SB:SparseBytes, + Start:Int, Width:Int) + => extractSparseBytes(F, SB, Start -Int size(SBI), Width) + requires size(SBI) <=Int Start + [simplification] + + rule extractSparseBytes( + F:SBGetFunction, + concat(SB1:SparseBytes, SB2:SparseBytes), + Start:Int, Width:Int) + => extractSparseBytes(F, SB2, Start -Int size(SB1), Width) + requires size(SB1) <=Int Start + [simplification] + + rule extractSparseBytes( + F:SBGetFunction, + merge(SB1, SB2:SparseBytes), + Start:Int, Width:Int) + => extractSparseBytes(F, SB2, Start -Int size(SB1), Width) + requires size(SB1) <=Int Start + [simplification] + + // ------------------------------------------ + // Simplify concatenation - included in first + // ------------------------------------------ + rule extractSparseBytes( + _F:SBGetFunction, + SBI:SBItemChunk SB:SparseBytes, + Start:Int, Width:Int) + => substrSparseBytes(SBI, Start, Start +Int Width) + requires Start +Int Width <=Int size(SBI) + andBool notBool empty(SB) + [simplification] + + rule extractSparseBytes( + F:SBGetFunction, + concat(SB1:SparseBytes, _SB2:SparseBytes), + Start:Int, Width:Int) + => extractSparseBytes(F, SB1, Start, Width) + requires 0 <=Int Start + andBool Start +Int Width <=Int size(SB1) + [simplification] + + rule extractSparseBytes( + F:SBGetFunction, + merge(SB1, _SB2:SparseBytes), + Start:Int, Width:Int) + => extractSparseBytes(F, SB1, Start, Width) + requires 0 <=Int Start + andBool Start +Int Width <=Int size(SB1) + [simplification] + + // ------------------------------------------ + // Simplify concatenation - only one chunk + // ------------------------------------------ + + rule extractSparseBytes( + _F:SBGetFunction, + SBChunk(#empty(A)), + Start:Int, Width:Int) + => SBChunk(#empty(Width)) + requires 0 <=Int Start + andBool Start +Int Width <=Int A + [simplification] + rule extractSparseBytes( + F:SBGetFunction, + SBChunk(#bytes(A +Bytes _B)), + Start:Int, Width:Int) + => extractSparseBytes( + F, + SBChunk(#bytes(A)), + Start, Width) + requires Start +Int Width <=Int lengthBytes(A) + [simplification] + rule extractSparseBytes( + F:SBGetFunction, + SBChunk(#bytes(A +Bytes B)), + Start:Int, Width:Int) + => extractSparseBytes( + F, + SBChunk(#bytes(B)), + Start -Int lengthBytes(A), Width) + requires lengthBytes(A) <=Int Start + [simplification] + rule extractSparseBytes( + F:SBGetFunction, + SBChunk(#bytes(A +Bytes B)), + Start:Int, Width:Int) + => extractSparseBytes( + F, + SBChunk(#bytes(substrBytes(A, Start, lengthBytes(A)) +Bytes B)), + 0, Width) + requires 0 substrSparseBytes(SBI, Start, Start +Int Width) + requires 0 substrSparseBytes(SBI, Start, Start +Int Width) + requires 0 substrSparseBytes(SBI, Start, Start +Int Width) + requires 0 <=Int Start + andBool Start +Int Width SBI + requires Width ==Int size(SBI) + [simplification] + + // ------------------------------------------ + // Simplify concatenation - overlaps first + // ------------------------------------------ + rule extractSparseBytes( + F:SBGetFunction, + SBI:SBItemChunk SB:SparseBytes, + Start:Int, Width:Int) + => concat( + substrSparseBytes(SBI, Start, size(SBI)), + extractSparseBytes(F, SB, 0, Width +Int Start -Int size(SBI)) + ) + requires Start concat( + substrSparseBytes(SB1, Start, size(SB1)), + extractSparseBytes(F, SB2, 0, Width +Int Start -Int size(SB1)) + ) + requires Start concat( + substrSparseBytes(SB1, Start, size(SB1)), + extractSparseBytes(F, SB2, 0, Width +Int Start -Int size(SB1)) + ) + requires Start extractSparseBytes(F1, SB, Start1, Width1) + requires disjontRanges(Start1, Width1, Start2, Width2) + andBool 0 <=Int Start1 + [simplification] + + // ------------------------------------------- + // With update - Included range - Skipping + // ------------------------------------------- + rule extractSparseBytes( + F1:SBGetFunction, + updateSparseBytes( + F2:SBSetFunction, + _SB:SparseBytes, + Start2:Int, Width2:Int), + Start1:Int, Width1:Int) + => extractSparseBytes( + F1, + getReplacementSparseBytes(F2, Start2, Width2), + Start1 -Int Start2, Width1 + ) + requires Start2 <=Int Start1 andBool Start1 +Int Width1 <=Int Start2 +Int Width2 + [simplification] + + // ------------------------------------------- + // With update - Overlapping ranges - Before + // ------------------------------------------- + rule extractSparseBytes( + F1:SBGetFunction, + updateSparseBytes( + F2:SBSetFunction, + SB:SparseBytes, + Start2:Int, Width2:Int), + Start1:Int, Width1:Int) + => concat( + extractSparseBytes(F1, SB, Start1, Start2 -Int Start1), + extractSparseBytes( + F1, updateSparseBytes(F2, SB, Start2, Width2), + Start2, Start1 +Int Width1 -Int Start2) + ) + requires Start1 concat( + extractSparseBytes( + F1, updateSparseBytes(F2, SB, Start2, Width2), + Start1, Start2 +Int Width2 -Int Start1), + extractSparseBytes( + F1, SB, + Start2 +Int Width2, + Start1 +Int Width1 -Int (Start2 +Int Width2)) + ) + requires Start2 <=Int Start1 + andBool Start1 unwrap(extractSparseBytes(getBytesRange, SB, Addr, Width)) + requires (0 fromBytes(#getBytesRange(SB, Addr, Width)) + requires (Addr ==Int 0 andBool Addr +Int Width ==Int size(SB)) + orBool size(SB) <=Int Addr + [simplification] +endmodule + +``` \ No newline at end of file diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/sparse-bytes/get-range-lemmas.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/sparse-bytes/get-range-lemmas.md new file mode 100644 index 000000000..e03d13e8f --- /dev/null +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/sparse-bytes/get-range-lemmas.md @@ -0,0 +1,23 @@ +```k + +module GET-RANGE-LEMMAS-BASIC + imports COMMON-SPARSE-BYTES-LEMMAS-SYNTAX + imports GET-BYTES-RANGE-LEMMAS-BASIC +endmodule + +module GET-RANGE-LEMMAS [symbolic] + imports GET-RANGE-LEMMAS-BASIC + + rule #getRange(SB, Addr:Int, Width:Int) + => Bytes2Int(unwrap(extractSparseBytes(getBytesRange, SB, Addr, Width)), LE, Unsigned) + requires Addr 0 + requires size(SB) <=Int Addr + andBool 0 0 <=Int Addr andBool 0 maxInt(SBSize, Addr +Int Width) + requires functionSparseBytesWellDefined( + replaceAt(Val:Bytes), Addr, Width + ) + rule getReplacementSparseBytes( + replaceAt(Value:Bytes), Addr:Int, Width:Int + ) + => SBChunk(#bytes(Value)) + requires functionSparseBytesWellDefined( + replaceAt(Value:Bytes), Addr, Width + ) + andBool Width ==Int lengthBytes(Value) + + rule replaceAt(SB:SparseBytes, Addr:Int, Value:Bytes) + => updateSparseBytes( + replaceAt(Value), SB, Addr, lengthBytes(Value) + ) + requires functionSparseBytesWellDefined( + replaceAt(Value), Addr, lengthBytes(Value) + ) + [simplification, symbolic(SB)] + rule replaceAt(SB:SparseBytes, Addr:Int, Value:Bytes) + => updateSparseBytes( + replaceAt(Value), SB, Addr, lengthBytes(Value) + ) + requires functionSparseBytesWellDefined( + replaceAt(Value), Addr, lengthBytes(Value) + ) + [simplification, symbolic(Addr)] + rule replaceAt(SB:SparseBytes, Addr:Int, Value:Bytes) + => updateSparseBytes( + replaceAt(Value), SB, Addr, lengthBytes(Value) + ) + requires functionSparseBytesWellDefined( + replaceAt(Value), Addr, lengthBytes(Value) + ) + [simplification, symbolic(Value)] + + rule updateSparseBytes( + replaceAt(Value), SB, Addr, Width + ) + => replaceAt(SB, Addr, Value) + requires functionSparseBytesWellDefined( + replaceAt(Value), Addr, Width + ) + andBool Width ==Int lengthBytes(Value) + [simplification, concrete] + + rule updateSparseBytes( + replaceAt(Value), SB, 0, Width + ) + => SBChunk(#bytes(Value)) + requires functionSparseBytesWellDefined( + replaceAt(Value), 0, Width + ) + andBool Width ==Int lengthBytes(Value) + andBool Width ==Int size(SB) + [simplification] + +endmodule + +``` \ No newline at end of file diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/sparse-bytes/set-range-lemmas.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/sparse-bytes/set-range-lemmas.md new file mode 100644 index 000000000..08cbd3ed0 --- /dev/null +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/sparse-bytes/set-range-lemmas.md @@ -0,0 +1,93 @@ +```k +module SET-RANGE-LEMMAS-BASIC + imports COMMON-SPARSE-BYTES-LEMMAS-SYNTAX + + syntax SBSetFunction ::= setRange(value:Int) +endmodule + +module SET-RANGE-LEMMAS [symbolic] + imports SET-RANGE-LEMMAS-BASIC + + rule functionSparseBytesWellDefined( + setRange(Val:Int), Addr:Int, Width:Int + ) + => #setRangeActuallySets(Addr, Val, Width) + rule updateSparseBytesSize( + setRange(Val:Int), SBSize:Int, Addr:Int, Width:Int + ) + => maxInt(SBSize, Addr +Int Width) + requires #setRangeActuallySets(Addr, Val, Width) + rule getReplacementSparseBytes( + setRange(Value:Int), Addr:Int, Width:Int + ) + => SBChunk(#bytes(Int2Bytes(Width, Value, LE))) + requires #setRangeActuallySets(Addr, Value, Width) + + rule #setRange(SB:SparseBytes, Addr:Int, Value:Int, Width:Int) + => updateSparseBytes( + setRange(Value), SB, Addr, Width + ) + requires functionSparseBytesWellDefined( + setRange(Value), Addr, Width + ) + [simplification] + + rule updateSparseBytes(setRange(Value:Int), SBChunk(#bytes(A)), Start:Int, Width:Int) + => SBChunk(#bytes(replaceAtBytes(A, Start, Int2Bytes(Width, Value, LE)))) + requires functionSparseBytesWellDefined(setRange(Value), Start, Width) + andBool Start +Int Width <=Int lengthBytes(A) + [simplification, concrete(A)] + + rule updateSparseBytes(setRange(Value:Int), SBChunk(#empty(A)), Start:Int, Width:Int) + => SBChunk(#empty(Start)) + updateSparseBytes(setRange(Value), SBChunk(#empty(A -Int Start)), 0, Width) + requires functionSparseBytesWellDefined(setRange(Value), Start, Width) + andBool Start +Int Width <=Int A + andBool 0 concat( + updateSparseBytes(setRange(Value), SBChunk(#empty(Width)), 0, Width), + SBChunk(#empty(A -Int Width)) + ) + requires functionSparseBytesWellDefined(setRange(Value), 0, Width) + andBool Width SBChunk(#bytes(Int2Bytes(A, Value, LE))) + requires functionSparseBytesWellDefined(setRange(Value), 0, A) + [simplification] + + rule updateSparseBytes(setRange(Value:Int), .SparseBytes, 0, Width:Int) + => SBChunk(#bytes(Int2Bytes(Width, Value, LE))) + requires functionSparseBytesWellDefined(setRange(Value), 0, Width) + [simplification] + rule updateSparseBytes(setRange(Value:Int), .SparseBytes, Addr:Int, Width:Int) + => SBChunk(#empty(Addr)) SBChunk(#bytes(Int2Bytes(Width, Value, LE))) + requires 0 SBChunk(#bytes(Int2Bytes(Width, Value, LE))) + substrSparseBytes(M, Width, size(M)) + requires Width SBChunk(#bytes(Int2Bytes(Width, Value, LE))) + requires size(M) <=Int Width + andBool functionSparseBytesWellDefined(setRange(Value), 0, Width) + [simplification] + + rule updateSparseBytes(setRange(Value:Int), M:SparseBytes, Addr, Width:Int) + => concat(M, updateSparseBytes(setRange(Value:Int), .SparseBytes, Addr -Int size(M), Width:Int)) + requires size(M) <=Int Addr + andBool 0 A + rule concat(A:SBItemChunk B:SparseBytes, C:SparseBytes) => merge(A, concat(B, C)) + + syntax SparseBytes ::= merge(SBItemChunk, SparseBytes) [function, total, symbol(mergeSparseBytes)] + rule merge(SBChunk(#bytes(A)), SBChunk(#bytes(B)) C:SparseBytes) => SBChunk(#bytes(A +Bytes B)) C + rule merge(SBChunk(#empty(A)), SBChunk(#empty(B)) C:SparseBytes) => SBChunk(#empty(A +Int B)) C + rule merge(SBChunk(#bytes(A)), SBChunk(#empty(B)) C:SparseBytes) => SBChunk(#bytes(A)) SBChunk(#empty(B)) C + rule merge(SBChunk(#empty(A)), SBChunk(#bytes(B)) C:SparseBytes) => SBChunk(#empty(A)) SBChunk(#bytes(B)) C + rule merge(SBChunk(#bytes(A)), .SparseBytes) => SBChunk(#bytes(A)) .SparseBytes + rule merge(SBChunk(#empty(A)), .SparseBytes) => SBChunk(#empty(A)) .SparseBytes + + syntax Bool ::= #setRangeActuallySets(addr:Int, val:Int, width:Int) [function, total] + rule #setRangeActuallySets(Addr:Int, Val:Int, Width:Int) + => 0 (Start1 +Int Len1 <=Int Start2) + orBool (Start2 +Int Len2 <=Int Start1) + + syntax Bool ::= disjontRanges(start1:Int, len1:Int, start2:Int, len2:Int) [function, total] + rule disjontRanges(Start1:Int, Len1:Int, Start2:Int, Len2:Int) + => true + requires disjontRangesSimple(Start1:Int, Len1:Int, Start2:Int, Len2:Int) + rule disjontRanges(Start1:Int, Len1:Int, Start2:Int, Len2:Int) + => false + requires notBool disjontRangesSimple(Start1:Int, Len1:Int, Start2:Int, Len2:Int) + +endmodule + +module SPARSE-BYTES-LEMMAS-BASIC-SYMBOLIC [symbolic] + imports private CEILS-SYNTAX + imports private SPARSE-BYTES-LEMMAS-BASIC + + rule concat(A, .SparseBytes) => A + [simplification] + rule concat(concat(A:SparseBytes, B:SparseBytes), C:SparseBytes) => concat(A, concat(B, C)) + [simplification] + + rule merge(SBChunk(#bytes(A)), merge(SBChunk(#bytes(B)), C)) => merge(SBChunk(#bytes(A +Bytes B)), C) + [simplification] + rule merge(SBChunk(#bytes(A)), merge(SBChunk(#empty(B)), C)) => SBChunk(#bytes(A)) merge(SBChunk(#empty(B)), C) + [simplification] + rule merge(SBChunk(#empty(A)), merge(SBChunk(#bytes(B)), C)) => SBChunk(#empty(A)) merge(SBChunk(#bytes(B)), C) + [simplification] + rule merge(SBChunk(#empty(A)), merge(SBChunk(#empty(B)), C)) => merge(SBChunk(#empty(A +Int B)), C) + [simplification] + + rule concat(merge(A, B), C) => merge(A, concat(B, C)) + [simplification] + + rule disjontRanges + ( (A1:Int modIntTotal M1:Int) +Int B1:Int, Len1:Int + , (A2:Int modIntTotal M2:Int) +Int B2:Int, Len2:Int + ) + => true + requires + ( ( (0 <=Int A1 andBool A1 =Int 0 andBool A2 =Int 0 andBool A2 true + requires + ( ( (0 <=Int A1 andBool A1 =Int 0 andBool A2 =Int 0 andBool A2 true + requires + ( ( (0 <=Int A1 andBool A1 =Int 0 andBool A2 =Int 0 andBool A2 true + requires + ( ( (0 <=Int A1 andBool A1 =Int 0 andBool A2 =Int 0 andBool A2 maxInt(Addr +Int Width, size(M)) + requires #setRangeActuallySets(Addr, Val, Width) + [simplification] + rule size(#setRange(M:SparseBytes, Addr:Int, Val:Int, Width:Int)) + => size(M) + requires notBool (#setRangeActuallySets(Addr, Val, Width)) + [simplification] + + rule size(replaceAt(Dest:SparseBytes, Index:Int, Src:Bytes)) + => maxInt(size(Dest), Index +Int lengthBytes(Src)) + requires 0 <=Int Index + [simplification] + rule size(substrSparseBytes(B:SparseBytes, Start:Int, End:Int)) + => End -Int Start + requires 0 <=Int Start andBool Start <=Int End andBool End <=Int size(B) + [simplification] + rule size(concat(A:SparseBytes, B:SparseBytes)) => size(A) +Int size(B) + [simplification] + rule size(merge(A:SBItemChunk, B:SparseBytes)) => size(A) +Int size(B) + [simplification] + rule 0 <=Int size(_:SparseBytes) => true + [simplification] +endmodule + +``` \ No newline at end of file diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/sparse-bytes/sparse-bytes-lemmas.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/sparse-bytes/sparse-bytes-lemmas.md new file mode 100644 index 000000000..2f5e87f7c --- /dev/null +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/sparse-bytes/sparse-bytes-lemmas.md @@ -0,0 +1,26 @@ +```k +requires "get-bytes-range-lemmas.md" +requires "get-range-lemmas.md" +requires "common-sparse-bytes-lemmas.md" +requires "replace-at-lemmas.md" +requires "set-range-lemmas.md" +requires "sparse-bytes-lemmas-basic.md" +requires "substr-sparse-bytes-lemmas.md" + +module SPARSE-BYTES-LEMMAS + imports private COMMON-SPARSE-BYTES-LEMMAS + imports private GET-BYTES-RANGE-LEMMAS + imports private GET-BYTES-RANGE-LEMMAS-BASIC + imports private GET-RANGE-LEMMAS + imports private GET-RANGE-LEMMAS-BASIC + imports private REPLACE-AT-LEMMAS + imports private REPLACE-AT-LEMMAS-BASIC + imports private SET-RANGE-LEMMAS + imports private SET-RANGE-LEMMAS-BASIC + imports private SPARSE-BYTES-LEMMAS-BASIC + imports private SPARSE-BYTES-LEMMAS-BASIC-SYMBOLIC + imports private SUBSTR-SPARSE-BYTES-LEMMAS + imports private SUBSTR-SPARSE-BYTES-LEMMAS-BASIC +endmodule + +``` \ No newline at end of file diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/sparse-bytes/substr-sparse-bytes-lemmas.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/sparse-bytes/substr-sparse-bytes-lemmas.md new file mode 100644 index 000000000..4a9ec191a --- /dev/null +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/sparse-bytes/substr-sparse-bytes-lemmas.md @@ -0,0 +1,94 @@ +```k +module SUBSTR-SPARSE-BYTES-LEMMAS-BASIC + imports COMMON-SPARSE-BYTES-LEMMAS-SYNTAX + imports GET-BYTES-RANGE-LEMMAS-BASIC +endmodule + +module SUBSTR-SPARSE-BYTES-LEMMAS [symbolic] + imports SPARSE-BYTES-LEMMAS-BASIC + imports SUBSTR-SPARSE-BYTES-LEMMAS-BASIC + + rule substrSparseBytes(SBI:SBItemChunk SB, Start:Int, End:Int) + => extractSparseBytes(substr, SBI SB, Start, End -Int Start) + requires 0 extractSparseBytes(substr, concat(SB1, SB2), Start, End -Int Start) + requires 0 <=Int Start andBool Start <=Int End + [simplification] + rule substrSparseBytes(merge(SB1, SB2), Start:Int, End:Int) + => extractSparseBytes(substr, merge(SB1, SB2), Start, End -Int Start) + requires 0 <=Int Start andBool Start <=Int End + [simplification] + rule substrSparseBytes(extractSparseBytes(F, SB, A, W), Start:Int, End:Int) + => extractSparseBytes(substr, extractSparseBytes(F, SB, A, W), Start, End -Int Start) + requires 0 <=Int Start andBool Start <=Int End + [simplification] + rule substrSparseBytes(substrSparseBytes(SB, A, W), Start:Int, End:Int) + => extractSparseBytes(substr, substrSparseBytes(SB, A, W), Start, End -Int Start) + requires 0 <=Int Start andBool Start <=Int End + [simplification] + + rule extractSparseBytes(substr, SB, Start, Width) + => substrSparseBytes(SB, Start, Start +Int Width) + // requires size(SB) <=Int Start +Int Width + [simplification, concrete] + + rule substrSparseBytes(.SparseBytes, _:Int, _:Int) => .SparseBytes + [simplification] + rule substrSparseBytes(updateSparseBytes(F, SB, Start, Width), SStart, SEnd) + => substrSparseBytes( + splitSparseBytesFunction( + updateSparseBytes(F, SB, Start, Width), + F, SB, SStart, Start, Width + ), + SStart, SEnd + ) + requires Start +Int Width <=Int SStart + andBool canSplitSparseBytes(F, SB, SStart, Start, Width) + [simplification] + rule substrSparseBytes(updateSparseBytes(F, _SB, Start, Width), SStart, SEnd) + => substrSparseBytes( + getReplacementSparseBytes(F, Start, Width), + SStart -Int Start, SEnd -Int Start + ) + requires Start <=Int SStart andBool SEnd <=Int Start +Int Width + [simplification] + rule substrSparseBytes(_, Start, End) => .SparseBytes + requires End <=Int Start + [simplification] + rule substrSparseBytes(updateSparseBytes(_F, _SB, _Start, _Width) #as Update, 0, SEnd) + => Update + requires SEnd ==Int size(Update) + [simplification] + + rule extractSparseBytes(substr, SB, 0, Width) + => SB + requires size(SB) <=Int Width + [simplification] + + rule extractSparseBytes( + substr, SBChunk(#bytes(Int2Bytes(Size:Int, Val:Int, LE))), + Start:Int, Width:Int + ) + => extractSparseBytes( + substr, SBChunk(#bytes(Int2Bytes(Size -Int Start, Val >>Int (8 *Int Start), LE))), + 0, Width + ) + requires 0 extractSparseBytes( + substr, SBChunk(#bytes(Int2Bytes(Width, Val &Int ((1 < true + requires 2 ^Int (8 *Int N) <=Int M + [simplification] + + rule { (< _:IValType > _:Int) #Equals undefined } => #Bottom [simplification] + rule { (< _:FValType > _:Float) #Equals undefined } => #Bottom [simplification] + rule { (< _:RefValType > _:Int) #Equals undefined } => #Bottom [simplification] + + rule { undefined #Equals (< _:IValType > _:Int) } => #Bottom [simplification] + rule { undefined #Equals (< _:FValType > _:Float) } => #Bottom [simplification] + rule { undefined #Equals (< _:RefValType > _:Int) } => #Bottom [simplification] + + rule undefined ==K (< _:IValType > _:Int) => false + [simplification] + rule undefined ==K (< _:FValType > _:Float) => false + [simplification] + rule undefined ==K (< _:RefValType > _:Int) => false + [simplification] + + rule (< _:IValType > _:Int) ==K undefined => false + [simplification] + rule (< _:FValType > _:Float) ==K undefined => false + [simplification] + rule (< _:RefValType > _:Int) ==K undefined => false + [simplification] + + rule 0 <=Int #signedTotal(T:IValType, N:Int) => 0 <=Int N andBool N A + requires M ==Int #pow(IType) + andBool 0 -Int #pow1(IType) <=Int A + andBool A true + requires #typeMatches(T, A) andBool #typeMatches(T, B) + [simplification] + rule #typeMatches(T, #if _ #then A #else B #fi:IVal) => true + requires #typeMatches(T, A) andBool #typeMatches(T, B) + [simplification] + rule #typeMatches(T, #if _ #then A #else B #fi:FVal) => true + requires #typeMatches(T, A) andBool #typeMatches(T, B) + [simplification] + rule #typeMatches(T, #if _ #then A #else B #fi:RefVal) => true + requires #typeMatches(T, A) andBool #typeMatches(T, B) + [simplification] + + // #if is parametric in the sort of the return value, and matching + // works on exact sort matches, so we need symplification rules + // for all possible combinations. + rule #typeMatches(T, #if _ #then A:Val #else B #fi) => false + requires notBool #typeMatches(T, A) andBool notBool #typeMatches(T, B) + [simplification] + rule #typeMatches(T, #if _ #then A #else B #fi:IVal) => false + requires notBool #typeMatches(T, A) andBool notBool #typeMatches(T, B) + [simplification] + rule #typeMatches(T, #if _ #then A #else B #fi:FVal) => false + requires notBool #typeMatches(T, A) andBool notBool #typeMatches(T, B) + [simplification] + rule #typeMatches(T, #if _ #then A #else B #fi:RefVal) => false + requires notBool #typeMatches(T, A) andBool notBool #typeMatches(T, B) + [simplification] +endmodule +``` \ No newline at end of file From ff07664bcba3416a73d7cba7c0cd3b289eb6b177 Mon Sep 17 00:00:00 2001 From: devops Date: Wed, 26 Jun 2024 17:54:21 +0000 Subject: [PATCH 03/10] Set Version: 0.1.71 --- package/version | 2 +- pykwasm/pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index f0768f091..7c3ae4e02 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.70 +0.1.71 diff --git a/pykwasm/pyproject.toml b/pykwasm/pyproject.toml index 0924280e6..372bce5d2 100644 --- a/pykwasm/pyproject.toml +++ b/pykwasm/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pykwasm" -version = "0.1.70" +version = "0.1.71" description = "" authors = [ "Runtime Verification, Inc. ", From 437e7f648b2ce572b4d25ff3cda6272fe8045b10 Mon Sep 17 00:00:00 2001 From: Virgil Date: Thu, 27 Jun 2024 18:21:28 +0300 Subject: [PATCH 04/10] Fix shift definedness --- .../kdist/wasm-semantics/kwasm-lemmas.md | 49 ++++++++++++++----- 1 file changed, 36 insertions(+), 13 deletions(-) diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/kwasm-lemmas.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/kwasm-lemmas.md index 7257ff806..88543e3a1 100644 --- a/pykwasm/src/pykwasm/kdist/wasm-semantics/kwasm-lemmas.md +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/kwasm-lemmas.md @@ -174,29 +174,48 @@ x mod m + y = r + y We want K to understand what a bit-shift is. ```k + // According to domains.md, shifting by negative amounts is #False, so + // all simplification rules must take that into account. + rule (_X < 0 - requires (2 ^Int N) modInt M ==Int 0 + requires 0 <=Int N andBool (2 ^Int N) modInt M ==Int 0 [simplification] rule #wrap(M, _X < 0 - requires (M *Int 8) <=Int N + requires 0 <=Int N andBool (M *Int 8) <=Int N [simplification] - rule (X >>Int N) => 0 requires X 0 requires M >Int N) => 0 + requires 0 <=Int N + andBool X 0 + requires 0 <=Int N + andBool M >Int N) >>Int M => X >>Int (N +Int M) [simplification] - rule (X < X <>Int N) >>Int M => X >>Int (N +Int M) + requires 0 <=Int N andBool 0 <=Int M + [simplification] + rule (X < X <>Int M => X <=Int M [simplification] - rule (X <>Int M => X >>Int (M -Int N) requires notBool (N >=Int M) [simplification] + rule (X <>Int M => X <>Int M => X >>Int (M -Int N) + requires 0 <=Int N andBool notBool (N >=Int M) + [simplification] ``` ```k - rule ((X <>Int N => (X <>Int N) requires M >=Int N [simplification] - rule (Y +Int (X <>Int N => (X <>Int N) requires M >=Int N [simplification] + rule ((X <>Int N => (X <>Int N) + requires M >=Int N andBool N >=Int 0 + [simplification] + rule (Y +Int (X <>Int N => (X <>Int N) + requires M >=Int N andBool N >=Int 0 + [simplification] ``` Proof: @@ -291,10 +310,13 @@ Bounds on `#getRange`: rule 0 <=Int VAL1 +Int VAL2 => true requires 0 <=Int VAL1 andBool 0 <=Int VAL2 [simplification] rule #getRange(_, _, WIDTH) true requires 2 ^Int (8 *Int WIDTH) <=Int MAX [simplification] - rule #getRange(_, _, WIDTH) < true requires 2 ^Int ((8 *Int WIDTH) +Int SHIFT) <=Int MAX [simplification] + rule #getRange(_, _, WIDTH) < true requires 2 ^Int ((8 *Int WIDTH) +Int SHIFT) <=Int MAX + requires 0 <=Int SHIFT + [simplification] rule (#getRange(_, _, WIDTH1) #as VAL1) +Int ((#getRange(_, _, WIDTH2) < true requires VAL1 #setRange(#setRange(BM, ADDR, VAL1, minInt(WIDTH1, WIDTH)), ADDR +Int WIDTH1, VAL2, WIDTH -Int WIDTH1) requires 0 <=Int ADDR + andBool 0 <=Int SHIFT andBool 0 Date: Thu, 27 Jun 2024 18:29:20 +0300 Subject: [PATCH 05/10] Fix right shifting of negative numbers: -1 >>Int 1 ==K -1 --- pykwasm/src/pykwasm/kdist/wasm-semantics/kwasm-lemmas.md | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/kwasm-lemmas.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/kwasm-lemmas.md index 88543e3a1..af013afce 100644 --- a/pykwasm/src/pykwasm/kdist/wasm-semantics/kwasm-lemmas.md +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/kwasm-lemmas.md @@ -187,6 +187,7 @@ We want K to understand what a bit-shift is. rule (X >>Int N) => 0 requires 0 <=Int N + andBool 0 <=Int X andBool X 0 @@ -212,9 +213,11 @@ We want K to understand what a bit-shift is. ```k rule ((X <>Int N => (X <>Int N) requires M >=Int N andBool N >=Int 0 + andBool 0 <=Int X andBool 0 <=Int Y [simplification] rule (Y +Int (X <>Int N => (X <>Int N) requires M >=Int N andBool N >=Int 0 + andBool 0 <=Int X andBool 0 <=Int Y [simplification] ``` @@ -241,6 +244,7 @@ The following rules decrease the modulus by rearranging it around a shift. requires N >=Int 0 andBool POW >Int 0 andBool POW modInt (2 ^Int N) ==Int 0 + andBool 0 <=Int X [simplification] rule (X < (X modInt (POW /Int (2 ^Int N))) < true requires 0 <=Int VAL1 andBool 0 <=Int VAL2 [simplification] rule #getRange(_, _, WIDTH) true requires 2 ^Int (8 *Int WIDTH) <=Int MAX [simplification] - rule #getRange(_, _, WIDTH) < true requires 2 ^Int ((8 *Int WIDTH) +Int SHIFT) <=Int MAX - requires 0 <=Int SHIFT + rule #getRange(_, _, WIDTH) < true + requires 2 ^Int ((8 *Int WIDTH) +Int SHIFT) <=Int MAX + andBool 0 <=Int SHIFT [simplification] rule (#getRange(_, _, WIDTH1) #as VAL1) +Int ((#getRange(_, _, WIDTH2) < true requires VAL1 Date: Thu, 27 Jun 2024 17:52:19 +0300 Subject: [PATCH 06/10] Fix lemmas --- .../wasm-semantics/symbolic/sparse-bytes/set-range-lemmas.md | 3 +++ .../src/pykwasm/kdist/wasm-semantics/symbolic/wasm-lemmas.md | 2 ++ 2 files changed, 5 insertions(+) diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/sparse-bytes/set-range-lemmas.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/sparse-bytes/set-range-lemmas.md index 08cbd3ed0..c781e571e 100644 --- a/pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/sparse-bytes/set-range-lemmas.md +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/sparse-bytes/set-range-lemmas.md @@ -88,6 +88,9 @@ module SET-RANGE-LEMMAS [symbolic] andBool functionSparseBytesWellDefined(setRange(Value), Addr, Width) [simplification] + rule updateSparseBytes(setRange(#getRange(M, Addr, Width)), M, Addr, Width) => M + [simplification] + endmodule ``` \ No newline at end of file diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/wasm-lemmas.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/wasm-lemmas.md index 2f187c6e6..d4b666618 100644 --- a/pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/wasm-lemmas.md +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/wasm-lemmas.md @@ -1,9 +1,11 @@ ```k +requires "int/symbolic.md" requires "sparse-bytes/sparse-bytes-lemmas.md" module WASM-LEMMAS imports private CEILS-SYNTAX imports private SPARSE-BYTES-LEMMAS + imports private WASM-INT-SYMBOLIC imports private WASM-TEXT rule Bytes2Int(#getBytesRange(_:SparseBytes, _:Int, N:Int), _:Endianness, _:Signedness) Date: Thu, 27 Jun 2024 18:48:37 +0300 Subject: [PATCH 07/10] Use total versions of operators. --- .../kdist/wasm-semantics/kwasm-lemmas.md | 67 ++++++++++--------- 1 file changed, 34 insertions(+), 33 deletions(-) diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/kwasm-lemmas.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/kwasm-lemmas.md index af013afce..0c0622069 100644 --- a/pykwasm/src/pykwasm/kdist/wasm-semantics/kwasm-lemmas.md +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/kwasm-lemmas.md @@ -18,6 +18,7 @@ module KWASM-LEMMAS-SYMBOLIC [symbolic] imports BYTES-KORE imports INT-SYMBOLIC imports MAP-SYMBOLIC + imports CEILS-SYNTAX ``` Basic logic @@ -54,14 +55,14 @@ These are given in pure modulus form, and in form with `#wrap`, which is modulus andBool X 0 + rule _X modIntTotal 1 => 0 [simplification] ``` `modInt` selects the least non-negative representative of a congruence class modulo `N`. ```k - rule (X modInt M) modInt N => X modInt M + rule (X modIntTotal M) modIntTotal N => X modInt M requires M >Int 0 andBool M <=Int N [simplification] @@ -78,7 +79,7 @@ Since 0 <= x mod m < m <= n, (x mod m) mod n = x mod m ``` ```k - rule (X modInt M) modInt N => X modInt N + rule (X modIntTotal M) modIntTotal N => X modInt N requires M >Int 0 andBool N >Int 0 andBool M modInt N ==Int 0 @@ -104,24 +105,24 @@ x = m * q + r, for a unique q and r s.t. 0 <= r < m #### Modulus Over Addition ```k - rule (_X *Int M +Int Y) modInt N => Y modInt N + rule (_X *Int M +Int Y) modIntTotal N => Y modInt N requires M >Int 0 andBool N >Int 0 andBool M modInt N ==Int 0 [simplification] - rule (Y +Int _X *Int M) modInt N => Y modInt N + rule (Y +Int _X *Int M) modIntTotal N => Y modInt N requires M >Int 0 andBool N >Int 0 andBool M modInt N ==Int 0 [simplification] - rule #wrap(N, (_X < #wrap(N, Y) + rule #wrap(N, (_X < #wrap(N, Y) requires 0 <=Int M andBool (N *Int 8) <=Int M [simplification] - rule #wrap(N, Y +Int (_X < #wrap(N, Y) + rule #wrap(N, Y +Int (_X < #wrap(N, Y) requires 0 <=Int M andBool (N *Int 8) <=Int M [simplification] @@ -135,13 +136,13 @@ x * m + y mod n = x * (k * n) + y mod n = y mod n ``` ```k - rule ((X modInt M) +Int Y) modInt N => (X +Int Y) modInt N + rule ((X modIntTotal M) +Int Y) modIntTotal N => (X +Int Y) modInt N requires M >Int 0 andBool N >Int 0 andBool M modInt N ==Int 0 [simplification] - rule (X +Int (Y modInt M)) modInt N => (X +Int Y) modInt N + rule (X +Int (Y modIntTotal M)) modIntTotal N => (X +Int Y) modInt N requires M >Int 0 andBool N >Int 0 andBool M modInt N ==Int 0 @@ -177,45 +178,45 @@ We want K to understand what a bit-shift is. // According to domains.md, shifting by negative amounts is #False, so // all simplification rules must take that into account. - rule (_X < 0 + rule (_X < 0 requires 0 <=Int N andBool (2 ^Int N) modInt M ==Int 0 [simplification] - rule #wrap(M, _X < 0 + rule #wrap(M, _X < 0 requires 0 <=Int N andBool (M *Int 8) <=Int N [simplification] - rule (X >>Int N) => 0 + rule (X >>IntTotal N) => 0 requires 0 <=Int N andBool 0 <=Int X andBool X 0 + rule (_X < 0 requires 0 <=Int N andBool M >Int N) >>Int M => X >>Int (N +Int M) + rule (X >>IntTotal N) >>IntTotal M => X >>Int (N +Int M) requires 0 <=Int N andBool 0 <=Int M [simplification] - rule (X < X < X <>Int M => X <>IntTotal M => X <>Int M => X >>Int (M -Int N) + rule (X <>IntTotal M => X >>Int (M -Int N) requires 0 <=Int N andBool notBool (N >=Int M) [simplification] ``` ```k - rule ((X <>Int N => (X <>Int N) + rule ((X <>IntTotal N => (X <>Int N) requires M >=Int N andBool N >=Int 0 andBool 0 <=Int X andBool 0 <=Int Y [simplification] - rule (Y +Int (X <>Int N => (X <>Int N) + rule (Y +Int (X <>IntTotal N => (X <>Int N) requires M >=Int N andBool N >=Int 0 andBool 0 <=Int X andBool 0 <=Int Y [simplification] @@ -240,14 +241,14 @@ Let x' = x << m The following rules decrease the modulus by rearranging it around a shift. ```k - rule (X modInt POW) >>Int N => (X >>Int N) modInt (POW /Int (2 ^Int N)) + rule (X modIntTotal POW) >>IntTotal N => (X >>Int N) modInt (POW /Int (2 ^Int N)) requires N >=Int 0 andBool POW >Int 0 andBool POW modInt (2 ^Int N) ==Int 0 andBool 0 <=Int X [simplification] - rule (X < (X modInt (POW /Int (2 ^Int N))) < (X modInt (POW /Int (2 ^Int N))) <=Int 0 andBool POW >Int 0 andBool POW modInt (2 ^Int N) ==Int 0 @@ -260,13 +261,13 @@ Therefore, we may as well shift first and then take the modulus, only we need to The argument for the left shift is similar. ```k - rule (X +Int (_Y < X modInt POW + rule (X +Int (_Y < X modInt POW requires N >=Int 0 andBool POW >Int 0 andBool (2 ^Int N) modInt POW ==Int 0 [simplification] - rule ((_Y < X modInt POW + rule ((_Y < X modInt POW requires N >=Int 0 andBool POW >Int 0 andBool (2 ^Int N) modInt POW ==Int 0 @@ -281,7 +282,7 @@ When reasoning about `#chop`, it's often the case that the precondition to the p In this case, it's simpler (and safe) to simply discard the `#chop`, instead of evaluating it. ```k - rule X modInt #pow(ITYPE) => #unsigned(ITYPE, X) + rule X modIntTotal #pow(ITYPE) => #unsigned(ITYPE, X) requires #inSignedRange (ITYPE, X) [simplification] @@ -309,16 +310,16 @@ Memory Bounds on `#getRange`: ```k - rule 0 <=Int #getRange(_, _, _) => true [simplification] - rule 0 <=Int VAL < true requires 0 <=Int VAL andBool 0 <=Int SHIFT [simplification] - rule 0 <=Int VAL1 +Int VAL2 => true requires 0 <=Int VAL1 andBool 0 <=Int VAL2 [simplification] + rule 0 <=Int #getRange(_, _, _) => true [simplification] + rule 0 <=Int VAL < true requires 0 <=Int VAL andBool 0 <=Int SHIFT [simplification] + rule 0 <=Int VAL1 +Int VAL2 => true requires 0 <=Int VAL1 andBool 0 <=Int VAL2 [simplification] - rule #getRange(_, _, WIDTH) true requires 2 ^Int (8 *Int WIDTH) <=Int MAX [simplification] - rule #getRange(_, _, WIDTH) < true + rule #getRange(_, _, WIDTH) true requires 2 ^Int (8 *Int WIDTH) <=Int MAX [simplification] + rule #getRange(_, _, WIDTH) < true requires 2 ^Int ((8 *Int WIDTH) +Int SHIFT) <=Int MAX andBool 0 <=Int SHIFT [simplification] - rule (#getRange(_, _, WIDTH1) #as VAL1) +Int ((#getRange(_, _, WIDTH2) < true + rule (#getRange(_, _, WIDTH1) #as VAL1) +Int ((#getRange(_, _, WIDTH2) < true requires VAL1 >Int SHIFT => #getRange(BM, ADDR +Int 1, WIDTH -Int 1) >>Int (SHIFT -Int 8) + rule #getRange(BM, ADDR, WIDTH) >>IntTotal SHIFT => #getRange(BM, ADDR +Int 1, WIDTH -Int 1) >>Int (SHIFT -Int 8) requires 0 <=Int ADDR andBool 0 #getRange(BM, ADDR, WIDTH -Int 1) modInt MAX + rule #getRange(BM, ADDR, WIDTH) modIntTotal MAX => #getRange(BM, ADDR, WIDTH -Int 1) modInt MAX requires 0 BM [simplification] - rule #setRange(BM, ADDR, (#getRange(_, _, WIDTH1) #as VAL1) +Int (VAL2 < #setRange(#setRange(BM, ADDR, VAL1, minInt(WIDTH1, WIDTH)), ADDR +Int WIDTH1, VAL2, WIDTH -Int WIDTH1) requires 0 <=Int ADDR andBool 0 <=Int SHIFT From 7d716315767efc872cd9bd363e54b0eea372be29 Mon Sep 17 00:00:00 2001 From: Virgil Date: Fri, 28 Jun 2024 21:56:59 +0300 Subject: [PATCH 08/10] Enable trivial evaluation for extractSparseBytes --- .../sparse-bytes/common-sparse-bytes-lemmas.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/sparse-bytes/common-sparse-bytes-lemmas.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/sparse-bytes/common-sparse-bytes-lemmas.md index 6968f5b0a..2d2d7738b 100644 --- a/pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/sparse-bytes/common-sparse-bytes-lemmas.md +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/sparse-bytes/common-sparse-bytes-lemmas.md @@ -821,11 +821,11 @@ module EXTRACT-SPARSE-BYTES-LEMMAS imports COMMON-SPARSE-BYTES-LEMMAS-SYNTAX // Final extraction - // rule extractSparseBytes( - // F:SBGetFunction, SB:SparseBytes, 0, Len - // ) => SB - // requires Len ==Int size(SB) - // [simplification] + rule extractSparseBytes( + _F:SBGetFunction, SB:SparseBytes, 0, Len + ) => SB + requires Len ==Int size(SB) + [simplification] // ------------------------------------------ From 8b17c665995b83816fb06bebbe34ab7811132c3b Mon Sep 17 00:00:00 2001 From: Virgil Date: Fri, 28 Jun 2024 21:57:39 +0300 Subject: [PATCH 09/10] Int simplification lemmas --- .../symbolic/int/arithmetic-normalization.md | 170 +++++++++++++++ .../symbolic/int/bit-normalization.md | 196 ++++++++++++++++++ .../wasm-semantics/symbolic/int/common.md | 24 +++ .../wasm-semantics/symbolic/int/symbolic.md | 12 ++ 4 files changed, 402 insertions(+) create mode 100644 pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/int/arithmetic-normalization.md create mode 100644 pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/int/bit-normalization.md create mode 100644 pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/int/common.md create mode 100644 pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/int/symbolic.md diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/int/arithmetic-normalization.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/int/arithmetic-normalization.md new file mode 100644 index 000000000..c438f2615 --- /dev/null +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/int/arithmetic-normalization.md @@ -0,0 +1,170 @@ +Arithmetic normalization +======================== + +The normal form of an arithmetic expression is less well defined. + +* there are no '-' operations, `A +Int -1 *Int B` is used instead of + `A -Int B +* Addition is grouped to the left, i.e., + `((..((A +Int B) +Int C) +Int ...) +Int Z)` +* Only the last element of an addition is concrete, i.e. `(A +Int B) +Int 7` + is normal, `(A +Int 7) +Int 8` and `(A +Int 7) +Int C` are not. +* Multiplication is grouped to the right, i.e., + `(Z *Int (... *Int (C *Int (A *Int B)) ...))` +* Only the fist element of multiplication is concrete, i.e., `7 *Int (A *Int B)` + is normal, `8 *Int (7 *Int A)` and `C *Int (7*Int B)` are not. +* Multiplication with constants is always distributed, i.e., + `7 *Int A +Int 7 *Int B` is normal, `7 *Int (A +Int B)` is not. +* (Not fully enforced): Constants multiplied with the same symbolic term, then + added, are merged, i.e., `(7 *Int A +Int B) +Int 8 *Int A` is not normal and + will be transformed to `15 *Int A +Int B` +```k +module WASM-INT-ARITHMETIC-NORMALIZATION + imports INT + + // The rules below complement the ones in INT-KORE + +``` +-Int elimination +---------------- +```k + + rule X -Int Y => X +Int (-1 *Int Y) [simplification] + +``` ++Int +---- + +* associativity +```k + rule X +Int (Y +Int Z) => (X +Int Y) +Int Z [simplification] + +``` +* constants +```k + rule I +Int X => X +Int I [simplification, symbolic(X), concrete(I)] + rule (X +Int I) +Int Y => (X +Int Y) +Int I [simplification, symbolic(X, Y), concrete(I)] +``` +*Int +---- + +* associativity +```k + rule (X *Int Y) *Int Z => X *Int (Y *Int Z) [simplification] + +``` +* constants +```k + rule X *Int I => I *Int X [simplification, symbolic(X), concrete(I)] + rule X *Int (I *Int Y) => I *Int (X *Int Y) [simplification, symbolic(X, Y), concrete(I)] + rule I1 *Int (I2 *Int X) => (I1 *Int I2) *Int X [simplification, symbolic(X), concrete(I1, I2)] + + rule 1 *Int X => X [simplification] + rule 0 *Int _ => 0 [simplification] + +``` +Distributivity for *Int and +Int +-------------------------------- + +* Multiplication with constants +```k + rule I *Int (X +Int Y) => I *Int X +Int I *Int Y + [simplification, symbolic(X), concrete(I)] + rule I *Int (X +Int Y) => I *Int X +Int I *Int Y + [simplification, symbolic(Y), concrete(I)] +``` +* Reverse distributivity for different-constants * same-term. +```k + // It would be really nice if the backend would check the equality for the + // two occurrences of X by matching. The next best option is to make these + // rules low-priority, so they are applied only after the formula has already + // stabilized (including normalization). + rule X +Int X => 2 *Int X [simplification(200)] + rule X +Int I *Int X => (1 +Int I) *Int X [simplification(200), concrete(I)] + rule I *Int X +Int X => (1 +Int I) *Int X [simplification(200), concrete(I)] + rule I1 *Int X +Int I2 *Int X => (I1 +Int I2) *Int X [simplification(200), concrete(I1, I2)] +``` +* Generalized reverse distributivity +```k + // The backends do not allow to do meta-manipulation of terms (e.g. to sort + // them by some criteria), so this is an attempt to catch the most common + // non-basic cases for reverse distributivity: + + // Distance 1: + rule (X +Int Y) +Int X => 2 *Int X +Int Y + [simplification(200)] + rule (X +Int Y) +Int I *Int X => (1 +Int I) *Int X +Int Y + [simplification(200), concrete(I)] + rule (I *Int X +Int Y) +Int X => (1 +Int I) *Int X +Int Y + [simplification(200), concrete(I)] + rule (I1 *Int X +Int Y) +Int I2 *Int X => (I1 +Int I2) *Int X +Int Y + [simplification(200), symbolic(X), concrete(I1, I2)] + + rule (Y +Int X) +Int X => Y +Int 2 *Int X + [simplification(200)] + rule (Y +Int X) +Int I *Int X => Y +Int (1 +Int I) *Int X + [simplification(200), concrete(I)] + rule (Y +Int I *Int X) +Int X => Y +Int (1 +Int I) *Int X + [simplification(200), concrete(I)] + rule (Y +Int I1 *Int X) +Int I2 *Int X => Y +Int (I1 +Int I2) *Int X + [simplification(200), concrete(I1, I2)] + + // Distance 2: + rule ((X +Int Y) +Int Z) +Int X => (2 *Int X +Int Y) +Int Z + [simplification(200)] + rule ((X +Int Y) +Int Z) +Int I *Int X => ((1 +Int I) *Int X +Int Y) +Int Z + [simplification(200), concrete(I)] + rule ((I *Int X +Int Y) +Int Z) +Int X => ((1 +Int I) *Int X +Int Y) +Int Z + [simplification(200), concrete(I)] + rule ((I1 *Int X +Int Y) +Int Z) +Int I2 *Int X => ((I1 +Int I2) *Int X +Int Y) +Int Z + [simplification(200), symbolic(X), concrete(I1, I2)] + + rule ((Y +Int X) +Int Z) +Int X => (Y +Int 2 *Int X) +Int Z + [simplification(200)] + rule ((Y +Int X) +Int Z) +Int I *Int X => (Y +Int (1 +Int I) *Int X) +Int Z + [simplification(200), concrete(I)] + rule ((Y +Int I *Int X) +Int Z) +Int X => (Y +Int (1 +Int I) *Int X) +Int Z + [simplification(200), concrete(I)] + rule ((Y +Int I1 *Int X) +Int Z) +Int I2 *Int X => (Y +Int (I1 +Int I2) *Int X) +Int Z + [simplification(200), concrete(I1, I2)] + + // Distance 3: + rule (((X +Int Y) +Int Z) +Int T) +Int X => ((2 *Int X +Int Y) +Int Z) +Int T + [simplification(200)] + rule (((X +Int Y) +Int Z) +Int T) +Int I *Int X => (((1 +Int I) *Int X +Int Y) +Int Z) +Int T + [simplification(200), concrete(I)] + rule (((I *Int X +Int Y) +Int Z) +Int T) +Int X => (((1 +Int I) *Int X +Int Y) +Int T) +Int Z + [simplification(200), concrete(I)] + rule (((I1 *Int X +Int Y) +Int Z) +Int T) +Int I2 *Int X => (((I1 +Int I2) *Int X +Int Y) +Int T) +Int Z + [simplification(200), symbolic(X), concrete(I1, I2)] + + rule (((Y +Int X) +Int Z) +Int T) +Int X => ((Y +Int 2 *Int X) +Int Z) +Int T + [simplification(200)] + rule (((Y +Int X) +Int Z) +Int T) +Int I *Int X => ((Y +Int (1 +Int I) *Int X) +Int Z) +Int T + [simplification(200), concrete(I)] + rule (((Y +Int I *Int X) +Int Z) +Int T) +Int X => ((Y +Int (1 +Int I) *Int X) +Int Z) +Int T + [simplification(200), concrete(I)] + rule (((Y +Int I1 *Int X) +Int Z) +Int T) +Int I2 *Int X => ((Y +Int (I1 +Int I2) *Int X) +Int Z) +Int T + [simplification(200), concrete(I1, I2)] + + // Distance 4: + rule ((((X +Int Y) +Int Z) +Int T) +Int S) +Int X => (((2 *Int X +Int Y) +Int Z) +Int T) +Int S + [simplification(200)] + rule ((((X +Int Y) +Int Z) +Int T) +Int S) +Int I *Int X => ((((1 +Int I) *Int X +Int Y) +Int Z) +Int T) +Int S + [simplification(200), concrete(I)] + rule ((((I *Int X +Int Y) +Int Z) +Int T) +Int S) +Int X => ((((1 +Int I) *Int X +Int Y) +Int T) +Int S) +Int Z + [simplification(200), concrete(I)] + rule ((((I1 *Int X +Int Y) +Int Z) +Int T) +Int S) +Int I2 *Int X => ((((I1 +Int I2) *Int X +Int Y) +Int T) +Int S) +Int Z + [simplification(200), symbolic(X), concrete(I1, I2)] + + rule ((((Y +Int X) +Int Z) +Int T) +Int S) +Int X => (((Y +Int 2 *Int X) +Int Z) +Int S) +Int T + [simplification(200)] + rule ((((Y +Int X) +Int Z) +Int T) +Int S) +Int I *Int X => (((Y +Int (1 +Int I) *Int X) +Int Z) +Int T) +Int S + [simplification(200), concrete(I)] + rule ((((Y +Int I *Int X) +Int Z) +Int T) +Int S) +Int X => (((Y +Int (1 +Int I) *Int X) +Int Z) +Int T) +Int S + [simplification(200), concrete(I)] + rule ((((Y +Int I1 *Int X) +Int Z) +Int T) +Int S) +Int I2 *Int X => (((Y +Int (I1 +Int I2) *Int X) +Int Z) +Int T) +Int S + [simplification(200), concrete(I1, I2)] +endmodule + +``` \ No newline at end of file diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/int/bit-normalization.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/int/bit-normalization.md new file mode 100644 index 000000000..05cf8f30a --- /dev/null +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/int/bit-normalization.md @@ -0,0 +1,196 @@ +Int bit normalization +===================== + +The normal form of an int expression based on bit operations is defined by: + +``` +or-operand = ((non-bit-int-expression &Int mask) >>Int shift) + | ((non-bit-int-expression &Int mask) <>Int B` and `A < 0 + rule A &Int B => A + requires 0 <=Int A + andBool A <=Int B + andBool isFullMask(B) + [simplification, concrete(B)] + rule (A &Int B) => 0 + requires 0 <=Int A + andBool ( + ( A <=Int fullMask(8) + andBool B &Int fullMask(8) ==Int 0 + ) + orBool ( A <=Int fullMask(16) + andBool B &Int fullMask(16) ==Int 0 + ) + orBool ( A <=Int fullMask(32) + andBool B &Int fullMask(32) ==Int 0 + ) + ) + [simplification] + rule A &Int B => B &Int A + [simplification, concrete(A), symbolic(B)] + rule (A &Int B) &Int C => A &Int (B &Int C) + [simplification, concrete(B, C)] + rule A &Int (B &Int C) => (A &Int B) &Int C + [simplification, symbolic(A, B)] + + rule (A < (A &Int (M >>Int B)) < 0 + requires 0 <=Int M + andBool 0 <=Int B + andBool M >IntTotal B) &Int M + => (A &Int (M <>IntTotal B + requires 0 <=Int B + [simplification, concrete(M, B)] + + rule (A < A + [simplification] + rule (A >>IntTotal 0) => A + [simplification] + rule (A >>IntTotal B) => 0 + requires 0 <=Int A andBool 0 >IntTotal B) >>IntTotal C => A >>IntTotal (B +Int C) + [simplification, concrete(B, C)] + rule (A < A <>IntTotal C => A <>IntTotal C => A >>IntTotal (C -Int B) + requires B >IntTotal B) < (A >>IntTotal (B -Int C)) + &Int (fullMask(64) -Int fullMask(C)) + requires 0 <=Int C + andBool C <=Int B + andBool B <=Int 64 + andBool 0 <=Int A + andBool A >IntTotal B) < (A < A + [simplification] + rule A |Int B => B |Int A + [simplification, concrete(A), symbolic(B)] + rule (A |Int B) |Int C => A |Int (B |Int C) + [simplification, concrete(B, C)] + rule A |Int (B |Int C) => (A |Int B) |Int C + [simplification, symbolic(A, B)] + + rule (A |Int B) &Int C => (A &Int C) |Int (B &Int C) + [simplification] + rule A &Int (B |Int C) => (A |Int C) &Int (B |Int C) + [simplification, symbolic(B)] + rule A &Int (B |Int C) => (A |Int C) &Int (B |Int C) + [simplification, symbolic(C)] + rule (A &Int B) |Int (A &Int C) + => A &Int (B |Int C) + [simplification, concrete(B, C)] + rule (A |Int B) >>IntTotal C => (A >>IntTotal C) |Int (B >>IntTotal C) + requires 0 <=Int C + [simplification] + rule (A |Int B) < (A < (A &Int B) &Int (M -Int 1) + requires (0 <=Int A orBool 0 <=Int B) + andBool isPowerOf2(M) + [simplification] + rule (A >>IntTotal B) modIntTotal M => (A >>IntTotal B) &Int (M -Int 1) + requires 0 <=Int A + andBool isPowerOf2(M) + [simplification] + rule (A < (A < (A |Int B) &Int (M -Int 1) + requires 0 <=Int A + andBool 0 <=Int B + andBool isPowerOf2(M) + [simplification] + + rule (A modIntTotal M) &Int B => (A &Int (M -Int 1)) &Int B + requires (0 <=Int A orBool 0 <=Int B) + andBool isPowerOf2(M) + [simplification] + rule (A modIntTotal M) >>IntTotal B => (A &Int (M -Int 1)) >>IntTotal B + requires 0 <=Int A + andBool isPowerOf2(M) + [simplification] + rule (A modIntTotal M) < (A &Int (M -Int 1)) < (A &Int (M -Int 1)) |Int B + requires 0 <=Int A + andBool 0 <=Int B + andBool isPowerOf2(M) + [simplification] + + // Rules for having saner masks. + rule A &Int B => A &Int (B &Int fullMask(8)) + requires fullMask(8) A &Int (B &Int fullMask(16)) + requires fullMask(16) A &Int (B &Int fullMask(24)) + requires fullMask(24) A &Int (B &Int fullMask(32)) + requires fullMask(32) A &Int (B &Int fullMask(40)) + requires fullMask(40) A &Int (B &Int fullMask(48)) + requires fullMask(48) A &Int (B &Int fullMask(56)) + requires fullMask(56) >IntTotal C } + => { 0 #Equals A &Int B } + requires B &Int fullMask(C) ==Int 0 + [simplification, concrete(B, C)] +endmodule +``` \ No newline at end of file diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/int/common.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/int/common.md new file mode 100644 index 000000000..95759546e --- /dev/null +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/int/common.md @@ -0,0 +1,24 @@ +```k +module WASM-INT-COMMON + imports BOOL + imports INT + + syntax Bool ::= isFullMask(Int) [function, total] + rule isFullMask(I:Int) => I ==Int fullMask(log2Int(I) +Int 1) + requires 0 false + requires I <=Int 0 + + syntax Bool ::= isPowerOf2(Int) [function, total] + rule isPowerOf2(I:Int) => I ==Int 1 < false + requires I <=Int 0 + + syntax Int ::= fullMask(Int) [function, total] + rule fullMask(I:Int) => (1 < 0 + requires I <=Int 0 +endmodule +``` \ No newline at end of file diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/int/symbolic.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/int/symbolic.md new file mode 100644 index 000000000..f48d57c3b --- /dev/null +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/int/symbolic.md @@ -0,0 +1,12 @@ +```k +requires "arithmetic-normalization.md" +requires "bit-normalization.md" +requires "common.md" + +module WASM-INT-SYMBOLIC + imports private WASM-INT-ARITHMETIC-NORMALIZATION + imports private WASM-INT-BIT-NORMALIZATION-LEMMAS + imports private WASM-INT-COMMON +endmodule + +``` \ No newline at end of file From 46d9252650c7024054b41eff4e0dc2ec5487e244 Mon Sep 17 00:00:00 2001 From: devops Date: Fri, 28 Jun 2024 20:07:00 +0000 Subject: [PATCH 10/10] Set Version: 0.1.74 --- package/version | 2 +- pykwasm/pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index 416eb55e2..21f074dfc 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.73 +0.1.74 diff --git a/pykwasm/pyproject.toml b/pykwasm/pyproject.toml index ab6a536fd..20b3d0a70 100644 --- a/pykwasm/pyproject.toml +++ b/pykwasm/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pykwasm" -version = "0.1.73" +version = "0.1.74" description = "" authors = [ "Runtime Verification, Inc. ",