diff --git a/.gitignore b/.gitignore index 0e45ef89..1fb92def 100644 --- a/.gitignore +++ b/.gitignore @@ -5,6 +5,10 @@ .build .kprove-* +.kore-repl-history +.sessionCommands +kore-*.tar.gz +tmp # User-specific files *.rsuser diff --git a/kmxwasm/k-src/ceils.k b/kmxwasm/k-src/ceils.k new file mode 100644 index 00000000..c1cc076c --- /dev/null +++ b/kmxwasm/k-src/ceils.k @@ -0,0 +1,152 @@ +module CEILS + imports BOOL + imports BYTES + imports INT + + syntax Bool ::= definedSubstrBytes(Bytes, startIndex: Int, endIndex: Int) [function, total] + rule definedSubstrBytes(B:Bytes, StartIndex:Int, EndIndex:Int) + => (0 <=Int StartIndex) andBool (0 <=Int EndIndex) + andBool (StartIndex (0 <=Int Index) + andBool (Index +Int lengthBytes(Src) <=Int lengthBytes(Dest)) + + + syntax Bool ::= definedPadRightBytes(Bytes, length: Int, value: Int) [function, total] + rule definedPadRightBytes(_B:Bytes, Length:Int, Value:Int) + => (0 <=Int Length) + andBool (0 <=Int Value) + andBool (Value <=Int 255) + + + syntax Bool ::= definedModInt(Int, Int) [function, total] + rule definedModInt (_:Int, X:Int) => X =/=Int 0 + + + // --------------------------------------- + + + 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] + + + syntax Bytes ::= substrBytesTotal(Bytes, startIndex: Int, endIndex: Int) + [function, total, klabel(substrBytesTotal), symbol, no-evaluators] + + rule substrBytesTotal(Arg0:Bytes, StartIndex:Int, EndIndex:Int) + => substrBytes(Arg0, StartIndex, EndIndex) + requires definedSubstrBytes(Arg0, StartIndex, EndIndex) + [concrete, simplification] + + rule substrBytes(Arg0:Bytes, StartIndex:Int, EndIndex:Int) + => substrBytesTotal(Arg0, StartIndex, EndIndex) + requires definedSubstrBytes(Arg0, StartIndex, EndIndex) + [symbolic(Arg0), simplification] + + rule substrBytes(Arg0:Bytes, StartIndex:Int, EndIndex:Int) + => substrBytesTotal(Arg0, StartIndex, EndIndex) + requires definedSubstrBytes(Arg0, StartIndex, EndIndex) + [symbolic(StartIndex), simplification] + + rule substrBytes(Arg0:Bytes, StartIndex:Int, EndIndex:Int) + => substrBytesTotal(Arg0, StartIndex, EndIndex) + requires definedSubstrBytes(Arg0, StartIndex, EndIndex) + [symbolic(EndIndex), simplification] + + 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] + + + syntax Bytes ::= replaceAtBytesTotal(dest: Bytes, index: Int, src: Bytes) + [function, total, klabel(replaceAtBytesTotal), symbol, no-evaluators] + + rule replaceAtBytesTotal(Dest:Bytes, Index:Int, Src:Bytes) + => replaceAtBytes(Dest, Index, Src) + requires definedReplaceAtBytes(Dest, Index, Src) + [concrete, simplification] + + rule replaceAtBytes(Dest:Bytes, Index:Int, Src:Bytes) + => replaceAtBytesTotal(Dest, Index, Src) + requires definedReplaceAtBytes(Dest, Index, Src) + [symbolic(Dest), simplification] + + rule replaceAtBytes(Dest:Bytes, Index:Int, Src:Bytes) + => replaceAtBytesTotal(Dest, Index, Src) + requires definedReplaceAtBytes(Dest, Index, Src) + [symbolic(Index), simplification] + + rule replaceAtBytes(Dest:Bytes, Index:Int, Src:Bytes) + => replaceAtBytesTotal(Dest, Index, Src) + requires definedReplaceAtBytes(Dest, Index, Src) + [symbolic(Src), simplification] + + 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] + + + syntax Bytes ::= padRightBytesTotal(Bytes, length: Int, value: Int) + [function, total, klabel(padRightBytesTotal), symbol, no-evaluators] + + rule padRightBytesTotal(Arg0:Bytes, Length:Int, Value:Int) + => padRightBytes(Arg0, Length, Value) + requires definedPadRightBytes(Arg0, Length, Value) + [concrete, simplification] + + rule padRightBytes(Arg0:Bytes, Length:Int, Value:Int) + => padRightBytesTotal(Arg0, Length, Value) + requires definedPadRightBytes(Arg0, Length, Value) + [symbolic(Arg0), simplification] + + rule padRightBytes(Arg0:Bytes, Length:Int, Value:Int) + => padRightBytesTotal(Arg0, Length, Value) + requires definedPadRightBytes(Arg0, Length, Value) + [symbolic(Length), simplification] + + rule padRightBytes(Arg0:Bytes, Length:Int, Value:Int) + => padRightBytesTotal(Arg0, Length, Value) + requires definedPadRightBytes(Arg0, Length, Value) + [symbolic(Value), simplification] + + rule #Ceil(@Arg0:Int modInt @Arg1:Int) + => (({ definedModInt(@Arg0, @Arg1) #Equals true } + #And #Ceil(@Arg0)) + #And #Ceil(@Arg1)) + [simplification] + + + syntax Int ::= Int "modIntTotal" Int + [function, total, klabel(modIntTotal), symbol, no-evaluators, smtlib(modIntTotal)] + + rule Arg0:Int modIntTotal Arg1:Int + => Arg0 modInt Arg1 + requires definedModInt(Arg0, Arg1) + [concrete, simplification] + + rule Arg0:Int modInt Arg1:Int + => Arg0 modIntTotal Arg1 + requires definedModInt(Arg0, Arg1) + [symbolic(Arg0), simplification] + + rule Arg0:Int modInt Arg1:Int + => Arg0 modIntTotal Arg1 + requires definedModInt(Arg0, Arg1) + [symbolic(Arg1), simplification] + +endmodule diff --git a/kmxwasm/k-src/elrond-impl.md b/kmxwasm/k-src/elrond-impl.md index 6c118fcf..5146b32d 100644 --- a/kmxwasm/k-src/elrond-impl.md +++ b/kmxwasm/k-src/elrond-impl.md @@ -1,8 +1,10 @@ ```k +require "ceils.k" require "elrond-configuration.md" require "wasm-text.md" module ELROND-IMPL + imports CEILS imports ELROND-CONFIGURATION imports WASM-TEXT imports LIST-BYTESW-EXTENSIONS @@ -236,6 +238,20 @@ module ELROND-IMPL ) ] ) + rule + + elrond_trap("\"mBufferCopyByteSlice\"") => i32.const 1 + ... + + + (0 |-> _SourceHandle:Int) + (1 |-> _StartingPosition:Int) + (2 |-> _SliceLength:Int) + (3 |-> _DestinationHandle:Int) + + ... + + [owise] rule @@ -449,7 +465,10 @@ module ELROND-IMPL ... - ensures notBool wrap(?NewHandle) in_keys(M) andBool ?NewHandle >Int 0 + ensures true + andBool notBool wrap(?NewHandle) in_keys(M) + andBool 0 @@ -472,7 +491,10 @@ module ELROND-IMPL requires true #And #Ceil(substrBytes(Mem, Ptr, Ptr +Int Len)) - ensures notBool wrap(?NewHandle) in_keys(M) andBool ?NewHandle >Int 0 + ensures true + andBool notBool wrap(?NewHandle) in_keys(M) + andBool ?NewHandle >Int 0 + andBool ?NewHandle @@ -571,7 +593,7 @@ module ELROND-IMPL rule // TODO: Should append to the returned result, or something like that. - elrond_trap("\"mBufferFinish\"") => i32.const ?_MBufferFinishResult:Int + elrond_trap("\"mBufferFinish\"") => i32.const ?MBufferFinishResult:Int ... @@ -579,6 +601,9 @@ module ELROND-IMPL ... + ensures true + andBool 0 @@ -902,11 +927,13 @@ module ELROND-IMPL - PreviousGasLeft:Int + PreviousGasLeft:Int => ?NewGasLeft ... - ensures ?NewGasLeft #import(MOD, Name, #funcDesc(... id: OID, type: TIDX)) diff --git a/kmxwasm/k-src/elrond-lemmas.md b/kmxwasm/k-src/elrond-lemmas.md index b5e474ed..e8bda1c9 100644 --- a/kmxwasm/k-src/elrond-lemmas.md +++ b/kmxwasm/k-src/elrond-lemmas.md @@ -1,26 +1,11 @@ ```k -module ELROND-LEMMAS - imports public ELROND-IMPL - - syntax Bool ::= definedSubstrBytes(Bytes, startIndex: Int, endIndex: Int) [function, total] - rule definedSubstrBytes(B:Bytes, StartIndex:Int, EndIndex:Int) - => (0 <=Int StartIndex) andBool (0 <=Int EndIndex) - andBool (StartIndex (0 <=Int Index) - andBool (Index +Int lengthBytes(Src) <=Int lengthBytes(Dest)) +require "ceils.k" - syntax Bool ::= definedPadRightBytes(Bytes, length: Int, value: Int) [function, total] - rule definedPadRightBytes(_B:Bytes, Length:Int, Value:Int) - => (0 <=Int Length) - andBool (0 <=Int Value) - andBool (Value <=Int 255) - syntax Bool ::= definedModInt(Int, Int) [function, total] - rule definedModInt (_:Int, X:Int) => X =/=Int 0 +module ELROND-LEMMAS + imports public CEILS + imports public ELROND-IMPL + // imports private INT-NORMALIZATION // // TODO: Should, perhaps, change domains.md to add a smtlib attribute to // // Bytes2Int instead of creating a new symbol that we control. @@ -33,6 +18,15 @@ module ELROND-LEMMAS // rule 0 <=Int #Bytes2Int(_:Bytes, _:Endianness, Unsigned) => true // [simplification, smt-lemma] + rule Bytes2Int(#getBytesRange(_:Bytes, _:Int, N:Int), _:Endianness, _:Signedness) true + requires 2 ^Int (8 *Int N) <=Int M + [simplification] + rule N <=Int Bytes2Int(_:Bytes, _:Endianness, Unsigned) + => true + requires N <=Int 0 + [simplification] + rule Bytes2Int(Int2Bytes(Length:Int, Value:Int, E), E:Endianness, Unsigned) => Value modInt (2 ^Int (Length *Int 8)) requires 0 <=Int Value @@ -41,98 +35,73 @@ module ELROND-LEMMAS => Value [simplification] + rule 0 <=Int A +Int B => true + requires 0 <=Int A andBool 0 <=Int B + [simplification] + rule { _:Int #Equals undefined } => #Top [simplification] rule { (< _:IValType > _:Int) #Equals undefined } => #Bottom [simplification] rule { (< _:ValType > _:Int) #Equals undefined } => #Bottom [simplification] - 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 #Ceil(substrBytes(@B:Bytes, @StartIndex:Int, @EndIndex:Int)) - => ( {definedSubstrBytes(@B, @StartIndex, @EndIndex) #Equals true} - #And #Ceil(@B) - ) - #And - ( #Ceil(@StartIndex) - #And #Ceil(@EndIndex) - ) - [simplification] - rule #Ceil(padRightBytes (@B:Bytes, @Length:Int, @Value:Int)) - => ( {definedPadRightBytes(@B, @Length, @Value) #Equals true} - #And #Ceil(@B) - ) - #And - ( #Ceil(@Length) - #And #Ceil(@Value) - ) - [simplification] - rule #Ceil(#signed(@T:IValType, @N:Int)) => {0 <=Int @N andBool @N substrBytes(Dest, Start, End) + rule substrBytesTotal(replaceAtBytesTotal(Dest:Bytes, Index:Int, Src:Bytes), Start:Int, End:Int) + => substrBytesTotal(Dest, Start, End) requires (End <=Int Index orBool Index +Int lengthBytes(Src) <=Int Start) andBool definedReplaceAtBytes(Dest, Index, Src) [simplification] - rule substrBytes(replaceAtBytes(Dest:Bytes, Index:Int, Src:Bytes), Start:Int, End:Int) - => substrBytes(Src, Start -Int Index, End -Int Index) + rule substrBytesTotal(replaceAtBytesTotal(Dest:Bytes, Index:Int, Src:Bytes), Start:Int, End:Int) + => substrBytesTotal(Src, Start -Int Index, End -Int Index) requires Index <=Int Start andBool End <=Int Index +Int lengthBytes(Src) andBool definedReplaceAtBytes(Dest, Index, Src) [simplification] - rule substrBytes(B:Bytes, 0:Int, L:Int) => B - requires lengthBytes(B) ==Int L + rule substrBytesTotal(B:Bytes, 0:Int, Len:Int) => B + requires true + andBool Len ==Int lengthBytes(B) [simplification] - rule padRightBytes (B:Bytes, Length:Int, _Value:Int) => B + rule padRightBytesTotal (B:Bytes, Length:Int, _Value:Int) => B requires Length <=Int lengthBytes(B) + rule padRightBytesTotal(replaceAtBytesTotal(Dest:Bytes, Pos:Int, Source:Bytes) #as _Ceil, Length:Int, Value:Int) + => replaceAtBytesTotal(padRightBytesTotal(Dest, Length, Value), Pos, Source) + [simplification] + rule padRightBytesTotal(padRightBytesTotal(B:Bytes, Length1:Int, Value:Int) #as _Ceil, Length2:Int, Value:Int) + => padRightBytesTotal(B, maxInt (Length1, Length2), Value:Int) + [simplification] - rule #getBytesRange(replaceAtBytes(Dest:Bytes, Index:Int, Source:Bytes), Start:Int, Len:Int) + rule #getBytesRange(replaceAtBytesTotal(Dest:Bytes, Index:Int, Source:Bytes), Start:Int, Len:Int) => #getBytesRange(Dest, Start, Len) requires (Start +Int Len <=Int Index) orBool (Index +Int lengthBytes (Source) <=Int Start) [simplification] - rule #getBytesRange(replaceAtBytes(_Dest:Bytes, Index:Int, Source:Bytes), Start:Int, Len:Int) + rule #getBytesRange(replaceAtBytesTotal(_Dest:Bytes, Index:Int, Source:Bytes), Start:Int, Len:Int) => #getBytesRange(Source, Start -Int Index, Len) requires (Index <=Int Start) andBool (Start +Int Len <=Int Index +Int lengthBytes (Source)) [simplification] - rule #getBytesRange(padRightBytes(B:Bytes, PadLen:Int, Val:Int), Start:Int, GetLen:Int) + rule #getBytesRange(padRightBytesTotal(B:Bytes, PadLen:Int, Val:Int), Start:Int, GetLen:Int) => #getBytesRange(B, Start, GetLen) requires true andBool definedPadRightBytes(B, PadLen, Val) andBool (PadLen Dest - // requires (End <=Int Index orBool Index +Int lengthBytes(Src) <=Int Start) - // andBool definedReplaceAtBytes(Dest, Index, Src) - // [simplification] - // rule #substrBytes(#replaceAtBytes(Dest:Bytes, Index:Int, Src:Bytes), Start:Int, End:Int) - // => #substrBytes(Src, Start -Int Index, End -Int Index) - // requires Index <=Int Start andBool End <=Int Index +Int lengthBytes(Src) - // andBool definedReplaceAtBytes(Dest, Index, Src) - // [simplification] rule lengthBytes(Int2Bytes(Len:Int, _:Int, _:Endianness)) => Len [simplification] - rule lengthBytes(padRightBytes(B:Bytes, Length:Int, _Value:Int)) + rule lengthBytes(padRightBytesTotal(B:Bytes, Length:Int, _Value:Int)) => maxInt(lengthBytes(B:Bytes), Length:Int) [simplification] - rule lengthBytes(replaceAtBytes(Dest:Bytes, _Index:Int, _Src:Bytes) #as _Ceil) + rule lengthBytes(replaceAtBytesTotal(Dest:Bytes, _Index:Int, _Src:Bytes) #as _Ceil) => lengthBytes(Dest) [simplification] - // rule lengthBytes(#replaceAtBytes(Dest:Bytes, _Index:Int, _Src:Bytes) #as _Ceil) - // => lengthBytes(Dest) - // [simplification] + rule lengthBytes(substrBytesTotal(_:Bytes, Start:Int, End:Int)) + => End -Int Start + [simplification] rule 0 <=Int lengthBytes(_:Bytes) => true [simplification] + rule X -Int X => 0 [simplification] + rule A:Int <=Int maxInt(B:Int, C:Int) => true requires A <=Int B orBool A <=Int C [simplification] @@ -161,18 +130,122 @@ module ELROND-LEMMAS [simplification] rule (_X modIntTotal Y) true requires Y >Int 0 - [simplification] + [simplification, smt-lemma] rule 0 <=Int (_X modIntTotal Y) => true requires Y >Int 0 + [simplification, smt-lemma] + + rule {(A modIntTotal C) #Equals (B modIntTotal C)} => #Top + requires A ==Int B [simplification] - syntax Int ::= Int "modIntTotal" Int [function, total, klabel(_modIntTotal_), symbol, left, smt-hook(mod)] - rule _ modIntTotal 0 => 0 - rule X modIntTotal Y => X modInt Y [concrete, simplification] +endmodule + + +module INT-NORMALIZATION + imports BOOL + imports private CEILS + imports INT + + syntax IntList ::= ".IntList" | Int ":" IntList + syntax Bool ::= differentIntStructure(IntList, IntList) [function, total, no-evaluators] + syntax Bool ::= unevaluableDifferentIntStructure() [function, total, no-evaluators] + + rule differentIntStructure(.IntList, .IntList) => unevaluableDifferentIntStructure() - rule X modInt Y => X modIntTotal Y - requires definedModInt(X, Y) - [simplification, symbolic(X)] + rule differentIntStructure(A1:Int : L1:IntList, A2:Int : L2:IntList) + => differentIntStructure(L1, L2) + requires A1 ==Int A2 + [simplification(200), concrete(A1), concrete(A2)] + + rule differentIntStructure(A1:Int +Int A2 : L1:IntList, B1:Int +Int B2 : L2:IntList) + => differentIntStructure(A1 : A2 : L1, B1 : B2 : L2) + [simplification] + rule differentIntStructure(_A1:Int +Int _A2 : _L1:IntList, _:Int : _L2:IntList) + => true + [simplification(100)] + + rule differentIntStructure(A1:Int -Int A2 : L1:IntList, B1:Int -Int B2 : L2:IntList) + => differentIntStructure(A1 : A2 : L1, B1 : B2 : L2) + [simplification] + rule differentIntStructure(_A1:Int -Int _A2 : _L1:IntList, _:Int : _L2:IntList) + => true + [simplification(100)] + + rule differentIntStructure(A1:Int *Int A2 : L1:IntList, B1:Int *Int B2 : L2:IntList) + => differentIntStructure(A1 : A2 : L1, B1 : B2 : L2) + [simplification] + rule differentIntStructure(_A1:Int *Int _A2 : _L1:IntList, _:Int : _L2:IntList) + => true + [simplification(100)] + + rule differentIntStructure(A1:Int /Int A2 : L1:IntList, B1:Int /Int B2 : L2:IntList) + => differentIntStructure(A1 : A2 : L1, B1 : B2 : L2) + [simplification] + rule differentIntStructure(_A1:Int /Int _A2 : _L1:IntList, _:Int : _L2:IntList) + => true + [simplification(100)] + + rule differentIntStructure( + A1:Int modIntTotal A2 : L1:IntList, + B1:Int modIntTotal B2 : L2:IntList + ) + => differentIntStructure(A1 : A2 : L1, B1 : B2 : L2) + [simplification] + rule differentIntStructure(_A1:Int modIntTotal _A2 : _L1:IntList, _:Int : _L2:IntList) + => true + [simplification(100)] + + syntax Int ::= normalizeModIntTotal(Int) [function, total, no-evaluators] + rule normalizeModIntTotal(I:Int) => I + [simplification(200)] + rule normalizeModIntTotal(A +Int B) + => normalizeModIntTotal(A) +Int normalizeModIntTotal(B) + [simplification] + rule normalizeModIntTotal(A -Int B) + => normalizeModIntTotal(A) -Int normalizeModIntTotal(B) + [simplification] + rule normalizeModIntTotal(A *Int B) + => normalizeModIntTotal(A) *Int normalizeModIntTotal(B) + [simplification] + rule normalizeModIntTotal(A /Int B) + => normalizeModIntTotal(A) /Int normalizeModIntTotal(B) + [simplification] + rule normalizeModIntTotal(A modIntTotal B) + => normalizeModIntTotalHelper(A, B) modIntTotal normalizeModIntTotal(B) + [simplification] + + syntax Int ::= normalizeModIntTotalHelper(Int, Int) [function, total, no-evaluators] + rule normalizeModIntTotalHelper(I:Int, _) => I + [simplification(200)] + rule normalizeModIntTotalHelper(A +Int B, M) + => normalizeModIntTotalHelper(A, M) +Int normalizeModIntTotalHelper(B, M) + [simplification] + rule normalizeModIntTotalHelper(A -Int B, M) + => normalizeModIntTotalHelper(A, M) -Int normalizeModIntTotalHelper(B, M) + [simplification] + rule normalizeModIntTotalHelper(A *Int B, M) + => normalizeModIntTotalHelper(A, M) *Int normalizeModIntTotalHelper(B, M) + [simplification] + rule normalizeModIntTotalHelper(A /Int B, _) + => normalizeModIntTotal(A) /Int normalizeModIntTotal(B) + [simplification] + rule normalizeModIntTotalHelper(A modIntTotal M, M) + => normalizeModIntTotalHelper(A, M) + [simplification] + rule normalizeModIntTotalHelper(A modIntTotal N, M) + => normalizeModIntTotalHelper(A, N) + requires M =/=Int N + [simplification] + + syntax Int ::= normalizeInt(Int) [function, total] + rule normalizeInt(I) => normalizeModIntTotal(I) + + rule A modIntTotal M => normalizeModIntTotalHelper(A, M) modIntTotal M + requires differentIntStructure( + A : .IntList, + normalizeModIntTotalHelper(A, M) : .IntList) + [simplification] endmodule ``` \ No newline at end of file diff --git a/kmxwasm/k-src/elrond-wasm.md b/kmxwasm/k-src/elrond-wasm.md index fc11ed67..76108c90 100644 --- a/kmxwasm/k-src/elrond-wasm.md +++ b/kmxwasm/k-src/elrond-wasm.md @@ -1,5 +1,6 @@ ```k require "summaries.k" +require "ceils.k" require "elrond-impl.md" require "elrond-lemmas.md" require "elrond-configuration.md" @@ -11,9 +12,11 @@ module ELROND-WASM-SYNTAX endmodule module ELROND-WASM + imports CEILS imports ELROND-IMPL imports ELROND-LEMMAS imports ELROND-WASM-CONFIGURATION + imports INT-SYMBOLIC-KORE imports SUMMARIES imports PROOF-EXTENSIONS diff --git a/kmxwasm/pyproject.toml b/kmxwasm/pyproject.toml index aad31db5..43ea1277 100644 --- a/kmxwasm/pyproject.toml +++ b/kmxwasm/pyproject.toml @@ -12,8 +12,8 @@ authors = [ [tool.poetry.dependencies] python = "^3.8" -pyk = { git = "https://github.com/runtimeverification/pyk.git", tag = "v0.1.209" } -# pyk = { path = "/mnt/data/runtime-verification/pyk", develop = true } +# pyk = { git = "https://github.com/runtimeverification/pyk.git", tag = "v0.1.209" } +pyk = { path = "/mnt/data/runtime-verification/pyk", develop = true } [tool.poetry.group.dev.dependencies] autoflake = "*" diff --git a/kmxwasm/src/kmxwasm/kast.py b/kmxwasm/src/kmxwasm/kast.py index ad31c9d5..b42a89d2 100644 --- a/kmxwasm/src/kmxwasm/kast.py +++ b/kmxwasm/src/kmxwasm/kast.py @@ -1,5 +1,5 @@ import operator -from typing import Callable, Dict, Iterable, List, Optional, Tuple, TypeVar +from typing import Callable, Dict, Iterable, List, Optional, Set, Tuple, TypeVar from pyk.kast.inner import ( KApply, @@ -254,6 +254,30 @@ def maybe_is_questionmark_variable(term: KInner) -> Optional[bool]: return kinner_top_down_fold(maybe_is_questionmark_variable, operator.or_, False, term) +def get_variables(term: KInner) -> Set[KVariable]: + def extract_variable(term_: KInner) -> Optional[Set[KVariable]]: + if not isinstance(term_, KVariable): + return None + return {term_} + + return kinner_top_down_fold(extract_variable, operator.add, set(), term) + + +def has_unused_questionmark_variables(term: KInner, *, used_in: KInner) -> bool: + all_variables = get_variables(used_in) + + def maybe_is_questionmark_variable(term_: KInner) -> Optional[bool]: + if not isinstance(term_, KVariable): + return None + if term_.name.startswith('?'): + if term_ not in all_variables: + return True + return False + + assert isinstance(term, KInner) + return kinner_top_down_fold(maybe_is_questionmark_variable, operator.or_, False, term) + + def bytes_to_string(b: str) -> str: assert b.startswith('b"') assert b.endswith('"') diff --git a/kmxwasm/src/kmxwasm/lazy_explorer.py b/kmxwasm/src/kmxwasm/lazy_explorer.py index 187f9cab..f3a9d39e 100644 --- a/kmxwasm/src/kmxwasm/lazy_explorer.py +++ b/kmxwasm/src/kmxwasm/lazy_explorer.py @@ -4,6 +4,7 @@ from socket import AF_INET, SO_REUSEADDR, SOCK_STREAM, SOL_SOCKET, socket from typing import Any, Optional +from pyk.cli_utils import BugReport from pyk.kast.outer import KAtt, KDefinition, KFlatModule, KImport, KProduction, KRequire, KTerminal from pyk.kcfg import KCFGExplore from pyk.ktool.kompile import KompileBackend, kompile @@ -124,7 +125,7 @@ def make_kprove(definition_dir: Path) -> KProve: return KProve( definition_dir, bug_report=None - # bug_report=BugReport(Path('bug_report')) + # bug_report=BugReport(Path('bug-report')) ) diff --git a/kmxwasm/src/kmxwasm/proofs.py b/kmxwasm/src/kmxwasm/proofs.py index daa2b370..98aa9c7f 100644 --- a/kmxwasm/src/kmxwasm/proofs.py +++ b/kmxwasm/src/kmxwasm/proofs.py @@ -30,7 +30,15 @@ remove_all_functions_but_one_and_builtins, ) from .identifiers import Identifiers, find_identifiers -from .kast import DOT_BYTES, SET_BYTES_RANGE, bytes_to_string, extract_rewrite_parents, make_rewrite, replace_child +from .kast import ( + DOT_BYTES, + SET_BYTES_RANGE, + bytes_to_string, + extract_rewrite_parents, + has_unused_questionmark_variables, + make_rewrite, + replace_child, +) from .lazy_explorer import LazyExplorer, kompile_semantics from .rules import RuleCreator, build_rewrite_requires_new from .specs import Specs, find_specs @@ -96,7 +104,7 @@ def _patch_symbol_table(cls, symbol_table: SymbolTable) -> None: symbol_table['~Int_'] = lambda c1: f'~Int ({c1})' symbol_table['_modInt_'] = lambda c1, c2: f'({c1}) modInt ({c2})' - symbol_table['_modIntTotal_'] = lambda c1, c2: f'({c1}) modIntTotal ({c2})' + symbol_table['modIntTotal'] = lambda c1, c2: f'({c1}) modIntTotal ({c2})' symbol_table['_*Int_'] = lambda c1, c2: f'({c1}) *Int ({c2})' symbol_table['_/Int_'] = lambda c1, c2: f'({c1}) /Int ({c2})' symbol_table['_%Int_'] = lambda c1, c2: f'({c1}) %Int ({c2})' @@ -204,9 +212,7 @@ def replace_bytes(term: KInner) -> KInner: def replace_bytes_c_term(term: CTerm) -> CTerm: - new_term = replace_bytes(term.config) - thing = mlAnd([new_term] + list(term.constraints), GENERATED_TOP_CELL) - return CTerm(thing) + return CTerm(replace_bytes(term.config), term.constraints) def make_apply(label: str, args: List[KInner]) -> KApply: @@ -326,7 +332,7 @@ def make_claim(term: KInner, constraint: KInner, address: str, functions: Functi return (lhs, KClaim(body=rewrite, requires=full_constraint)) -def build_rewrite_requires(lhs_id: str, rhs_id: str, kcfg: KCFG) -> Tuple[KInner, KInner]: +def build_rewrite_requires(lhs_id: str, rhs_id: str, kcfg: KCFG) -> Tuple[KInner, KInner, KInner]: lhs_node = kcfg.node(lhs_id) rhs_node = kcfg.node(rhs_id) return build_rewrite_requires_new( @@ -339,8 +345,8 @@ def build_rewrite_requires(lhs_id: str, rhs_id: str, kcfg: KCFG) -> Tuple[KInner # configuration when calling `minimize_rule`. The rule is not valid without # those. def make_final_claim(lhs_id: str, rhs_id: str, kcfg: KCFG) -> KClaim: - (rewrite, constraint) = build_rewrite_requires(lhs_id=lhs_id, rhs_id=rhs_id, kcfg=kcfg) - return KClaim(body=rewrite, requires=constraint) + (rewrite, requires_constraint, ensures_constraint) = build_rewrite_requires(lhs_id=lhs_id, rhs_id=rhs_id, kcfg=kcfg) + return KClaim(body=rewrite, requires=requires_constraint, ensures=ensures_constraint) # It would be tempting to use cterm.build_rule or cterm.build_claim, however, @@ -348,11 +354,11 @@ def make_final_claim(lhs_id: str, rhs_id: str, kcfg: KCFG) -> KClaim: # configuration when calling `minimize_rule`. The rule is not valid without # those. def make_final_rule(lhs_id: str, rhs_id: str, kcfg: KCFG) -> KRule: - (rewrite, constraint) = build_rewrite_requires(lhs_id=lhs_id, rhs_id=rhs_id, kcfg=kcfg) + (rewrite, requires_constraint, ensures_constraint) = build_rewrite_requires(lhs_id=lhs_id, rhs_id=rhs_id, kcfg=kcfg) att_dict = {'priority': str(GENERATED_RULE_PRIORITY)} rule_att = KAtt(atts=att_dict) - return KRule(body=rewrite, requires=constraint, att=rule_att) + return KRule(body=rewrite, requires=requires_constraint, ensures=ensures_constraint, att=rule_att) def write_json(term: KInner, output_file: Path) -> None: @@ -360,19 +366,62 @@ def write_json(term: KInner, output_file: Path) -> None: output_file.write_text(json.dumps(term.to_dict())) -def my_step(explorer: LazyExplorer, cfg: KCFG, node_id: str) -> List[str]: +def debug_rewrite(start: CTerm, end: CTerm, printer: KPrint) -> None: + diff = make_rewrite(start.config, end.config) + children = extract_rewrite_parents(diff) + for child in children: + pretty = printer.pretty_print(child) + # if not cached: + print(pretty) + print() + + for constraint in end.constraints: + if constraint in start.constraints: + prefix1 = '--' + prefix2 = '//' + else: + prefix1 = '++' + prefix2 = '**' + print(prefix1, printer.pretty_print(constraint), flush=True) + try: + print(prefix2, printer.pretty_print(ml_pred_to_bool(constraint)), flush=True) + except Exception: + print(prefix2, 'Cannot print bool constraint') + + +def debug_step(start_node: KCFG.Node, cterm: CTerm, next_cterms: Iterable[CTerm], printer: KPrint) -> None: + first = True + + print('cterm:') + debug_rewrite(start_node.cterm, cterm, printer) + first = False + + print('next_cterms:') + for s in next_cterms: + if not first: + print('-' * 80) + first = False + debug_rewrite(start_node.cterm, s, printer) + print('next_cterms end') + + +def my_step(explorer: LazyExplorer, cfg: KCFG, node_id: str) -> Tuple[List[str], bool]: node = cfg.node(node_id) out_edges: List[str] = [] for split in cfg.splits(source_id=node.id): - for n, _ in split.targets: + for n in split.targets: + out_edges.append(n.id) + for branch in cfg.ndbranches(source_id=node.id): + for n in branch.targets: out_edges.append(n.id) for e in cfg.edges(source_id=node.id): out_edges.append(e.target.id) if len(out_edges) > 0: - return out_edges + return (out_edges, True) assert len(list(cfg.edges(source_id=node.id))) == 0 assert len(list(cfg.covers(source_id=node.id))) == 0 assert len(list(cfg.splits(source_id=node.id))) == 0 + assert len(list(cfg.ndbranches(source_id=node.id))) == 0 assert len(list(cfg.successors(node.id))) == 0 print('Executing!', flush=True) @@ -381,19 +430,41 @@ def my_step(explorer: LazyExplorer, cfg: KCFG, node_id: str) -> List[str]: if len(next_cterms) < 2: print(node.id) print(explorer.printer().pretty_print(node.cterm.config), flush=True) - for constraint in node.cterm.constraints: - print('--', explorer.printer().pretty_print(constraint), flush=True) - for constraint in node.cterm.constraints: - print('**', explorer.printer().pretty_print(ml_pred_to_bool(constraint)), flush=True) + debug_step(node, cterm, next_cterms, explorer.printer()) raise ValueError( f'Unable to take {1} steps from node (next={len(next_cterms)}), got {actual_depth} steps: {node.id}' ) - branches = [mlAnd(c for c in s.constraints if c not in cterm.constraints) for s in next_cterms] - next_ids = cfg.split_on_constraints(node.id, branches) - for next_id in next_ids: - print(node.id, '-*>', next_id) - assert node.id not in next_ids - return next_ids + has_question = False + has_top = False + for ct in next_cterms: + has_constraint = False + for constraint in ct.constraints: + if not constraint in ct.constraints: + if has_unused_questionmark_variables(constraint, used_in=ct.config): + has_question = True + break + has_constraint = True + if not has_constraint: + has_top = True + break + if has_question or has_top: + next_ids = [] + for ct in next_cterms: + next_node = cfg.get_or_create_node(ct) + next_ids.append(next_node.id) + cfg.create_ndbranch(node.id, next_ids) + else: + split_cond = [mlAnd(c for c in s.constraints if c not in cterm.constraints) for s in next_cterms] + next_ids = cfg.split_on_constraints(node.id, split_cond) + + for next_id in next_ids: + print(node.id, '-*>', next_id) + if node.id in next_ids: + debug_step(node, cterm, next_cterms, explorer.printer()) + raise ValueError( + 'Link form node to self, most likely caused by not completely rewriting the configuration.' + ) + return (next_ids, False) if actual_depth != 1: write_json(node.cterm.config, DEBUG_DIR / 'stuck.json') print('cterm=', cterm) @@ -405,14 +476,14 @@ def my_step(explorer: LazyExplorer, cfg: KCFG, node_id: str) -> List[str]: new_node = cfg.get_or_create_node(cterm) # TODO: This may be other things than mlTop() cfg.create_edge(node.id, new_node.id, depth=1) - return [new_node.id] + return ([new_node.id], False) def my_step_logging(explorer: LazyExplorer, kcfg: KCFG, node_id: str, branches: int) -> List[str]: prev_cterm = kcfg.node(node_id).cterm prev_config = prev_cterm.config # prev_config = replace_bytes(prev_config) - new_node_ids = my_step(explorer=explorer, cfg=kcfg, node_id=node_id) + (new_node_ids, cached) = my_step(explorer=explorer, cfg=kcfg, node_id=node_id) first = True print([node_id], '->', new_node_ids, f'{branches - 1} branches left', flush=True) for new_node_id in new_node_ids: @@ -428,6 +499,7 @@ def my_step_logging(explorer: LazyExplorer, kcfg: KCFG, node_id: str, branches: children = extract_rewrite_parents(diff) for child in children: pretty = explorer.printer().pretty_print(child) + # if not cached: print(pretty) print() @@ -485,7 +557,7 @@ def execute_function( try: first_node_id = kcfg.get_unique_init().id - node_ids = my_step(explorer, kcfg, first_node_id) + (node_ids, _) = my_step(explorer, kcfg, first_node_id) assert len(node_ids) == 1 lhs_id = node_ids[0] rhs_ids = [] @@ -729,7 +801,7 @@ def main(args: List[str]) -> None: sample_path = ROOT / 'kmxwasm' / 'samples' / f'{sample_name}.wat' if not sample_path.exists(): print(f'Input file ({sample_path}) does not exit.') - blacklist = {'multisig-full': {'78'}} + blacklist = {'multisig-full': {'78', '113'}} loop_whitelist = {'sum-to-n': {'13'}} run_for_input(sample_path, sample_name, blacklist.get(sample_name, set()), loop_whitelist.get(sample_name, set())) # run_for_input(samples / 'multisig-full.wat', 'multisig-full', {'78'}) diff --git a/kmxwasm/src/kmxwasm/rules.py b/kmxwasm/src/kmxwasm/rules.py index 15c95433..9ebb09ee 100644 --- a/kmxwasm/src/kmxwasm/rules.py +++ b/kmxwasm/src/kmxwasm/rules.py @@ -7,6 +7,7 @@ from pyk.prelude.bytes import BYTES, bytesToken from pyk.prelude.kbool import TRUE, andBool from pyk.prelude.kint import INT +from pyk.prelude.ml import mlAnd from .kast import ( DOT_BYTES, @@ -99,25 +100,32 @@ def make_final_rule_new( rhs_constraints: Tuple[KInner, ...], priority: int, ) -> KRule: - (rewrite, constraint) = build_rewrite_requires_new(lhs, lhs_constraints, rhs, rhs_constraints) - rewrite = underscore_for_unused_vars(rewrite, constraint) + (rewrite, requires_constraint, ensures_constraint) = build_rewrite_requires_new( + lhs, lhs_constraints, rhs, rhs_constraints + ) + rewrite = underscore_for_unused_vars(rewrite, mlAnd([requires_constraint, ensures_constraint])) - return KRule(body=rewrite, requires=constraint, att=default_atts(priority)) + return KRule(body=rewrite, requires=requires_constraint, ensures=ensures_constraint, att=default_atts(priority)) def build_rewrite_requires_new( lhs: KInner, lhs_constraints: Tuple[KInner, ...], rhs: KInner, rhs_constraints: Tuple[KInner, ...] -) -> Tuple[KInner, KInner]: +) -> Tuple[KInner, KInner, KInner]: lhs_config = unpack_bytes(lhs) rhs_config = unpack_bytes(rhs) rewrite = make_rewrite(lhs_config, rhs_config) rewrite = get_inner(rewrite, 0, '') requires = [c for c in lhs_constraints if c != TRUE] + ensures = [] for c in rhs_constraints: - if c != TRUE and c not in lhs_constraints and not has_questionmark_variables(c): - requires.append(c) - constraint = andBool([ml_pred_to_bool(c) for c in requires]) - return (rewrite, constraint) + if c != TRUE and c not in lhs_constraints: + if not has_questionmark_variables(c): + requires.append(c) + else: + ensures.append(c) + requires_constraint = andBool([ml_pred_to_bool(c) for c in requires]) + ensures_constraint = andBool([ml_pred_to_bool(c) for c in ensures]) + return (rewrite, requires_constraint, ensures_constraint) # TODO: This is probably no longer needed and should be removed. diff --git a/kmxwasm/src/kmxwasm/specs.py b/kmxwasm/src/kmxwasm/specs.py index 02179b0f..4b2a7345 100644 --- a/kmxwasm/src/kmxwasm/specs.py +++ b/kmxwasm/src/kmxwasm/specs.py @@ -3,6 +3,7 @@ from pyk.kast.outer import KRule from pyk.ktool.kprove import KProve +from pyk.prelude.ml import is_top from .kast import get_inner from .lazy_explorer import LazyExplorer @@ -36,7 +37,9 @@ def __has_dependencies(spec_dependencies: List[str], processed_functions: List[s @staticmethod def __prove(spec_path: Path, kprove: KProve) -> None: print(f'Proving {spec_path}', flush=True) - kprove.prove(spec_path) + final_state = kprove.prove(spec_path) + if not is_top(final_state): + raise ValueError(f'Failed to prove {spec_path}.') print('Proving done', flush=True) @staticmethod