From 06fcd6ab3f71c93c888ab33d30f0bb8a6ec4ff27 Mon Sep 17 00:00:00 2001 From: Virgil Date: Tue, 26 Sep 2023 16:34:27 +0300 Subject: [PATCH 01/16] Rule labels --- auxil.md | 3 ++- test.md | 3 ++- wasm.md | 3 ++- 3 files changed, 6 insertions(+), 3 deletions(-) diff --git a/auxil.md b/auxil.md index 873a9afcb..f84d19dcf 100644 --- a/auxil.md +++ b/auxil.md @@ -14,7 +14,8 @@ module WASM-AUXIL syntax Auxil ::= "#clearConfig" // ------------------------------- - rule #clearConfig => . ... + rule [clearConfig]: + #clearConfig => . ... _ => .Int _ => .ValStack _ => .Map diff --git a/test.md b/test.md index 6ea7bb4cf..9f7ac1cd3 100644 --- a/test.md +++ b/test.md @@ -494,7 +494,8 @@ These assertions act on the last module defined. ```k syntax Assertion ::= "#assertNamedModule" Identifier WasmString // --------------------------------------------------------------- - rule #assertNamedModule NAME _S => . ... + rule [assertNamedModule]: + #assertNamedModule NAME _S => . ... ... NAME |-> IDX ... diff --git a/wasm.md b/wasm.md index 914c06d68..4c7aa4485 100644 --- a/wasm.md +++ b/wasm.md @@ -1388,7 +1388,8 @@ A new module instance gets allocated. Then, the surrounding `module` tag is discarded, and the definitions are executed, putting them into the module currently being defined. ```k - rule #module(... types: TS, funcs: FS, tables: TABS, mems: MS, globals: GS, elem: EL, data: DAT, start: S, importDefns: IS, exports: ES, + rule [newModule]: + #module(... types: TS, funcs: FS, tables: TABS, mems: MS, globals: GS, elem: EL, data: DAT, start: S, importDefns: IS, exports: ES, metadata: #meta(... id: OID, funcIds: FIDS, filename: FILE)) => sequenceDefns(TS) ~> sequenceDefns(IS) From f56b93e55dc1e9cf7c1b111d5aa38fbb6c143b08 Mon Sep 17 00:00:00 2001 From: Virgil Date: Tue, 26 Sep 2023 17:07:14 +0300 Subject: [PATCH 02/16] Mark some functions as total --- wasm.md | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/wasm.md b/wasm.md index 4c7aa4485..6a7acc856 100644 --- a/wasm.md +++ b/wasm.md @@ -271,9 +271,9 @@ Instructions ### Sequencing ```k - syntax K ::= sequenceStmts ( Stmts ) [function] - | sequenceDefns ( Defns ) [function] - | sequenceInstrs ( Instrs ) [function] + syntax K ::= sequenceStmts ( Stmts ) [function, total] + | sequenceDefns ( Defns ) [function, total] + | sequenceInstrs ( Instrs ) [function, total] // ------------------------------------------------- rule sequenceStmts(.Stmts) => . rule sequenceStmts(S SS ) => S ~> sequenceStmts(SS) @@ -1109,7 +1109,7 @@ By setting the `` field in the configuration to `true requires notBool DET orBool notBool #growthAllowed(SIZE +Int N, MAX) - syntax Bool ::= #growthAllowed(Int, OptionalInt) [function] + syntax Bool ::= #growthAllowed(Int, OptionalInt) [function, total] // ----------------------------------------------------------- rule #growthAllowed(SIZE, .Int ) => SIZE <=Int #maxMemorySize() rule #growthAllowed(SIZE, I:Int) => #growthAllowed(SIZE, .Int) andBool SIZE <=Int I @@ -1120,9 +1120,9 @@ Incidentally, the page size is 2^16 bytes. The maximum of table size is 2^32 bytes. ```k - syntax Int ::= #pageSize() [function] - syntax Int ::= #maxMemorySize() [function] - syntax Int ::= #maxTableSize() [function] + syntax Int ::= #pageSize() [function, total] + syntax Int ::= #maxMemorySize() [function, total] + syntax Int ::= #maxTableSize() [function, total] // ------------------------------------------ rule #pageSize() => 65536 rule #maxMemorySize() => 65536 From 14237e75b3555176e53c93eddaeed6c71e52fe84 Mon Sep 17 00:00:00 2001 From: Virgil Date: Tue, 26 Sep 2023 17:23:40 +0300 Subject: [PATCH 03/16] Definedness for #signed --- data.md | 46 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 46 insertions(+) diff --git a/data.md b/data.md index e8ac3e1a1..e174724bf 100644 --- a/data.md +++ b/data.md @@ -378,6 +378,10 @@ Some operations extend integers from 1, 2, or 4 bytes, so a special function wit syntax Int ::= #signed ( IValType , Int ) [function] | #unsigned ( IValType , Int ) [function] | #signedWidth ( Int , Int ) [function] + + syntax Bool ::= definedSigned ( IValType, Int ) [function, total] + | definedUnsigned( IValType, Int ) [function, total] + // --------------------------------------------------------- rule #signed(ITYPE, N) => N requires 0 <=Int N andBool N N -Int #pow(ITYPE) requires #pow1(ITYPE) <=Int N andBool N N requires 0 <=Int N andBool N N -Int 65536 requires 32768 <=Int N andBool N #signed(i32, N) + + rule definedSigned(T:IValType, N:Int) => 0 <=Int N andBool N (({ definedSigned(@Arg0, @Arg1) #Equals true } + #And #Ceil(@Arg0)) + #And #Ceil(@Arg1)) + [simplification] + + // Should this use `N 0 -Int #pow1(T) <=Int N andBool N (({ definedUnsigned(@Arg0, @Arg1) #Equals true } + #And #Ceil(@Arg0)) + #And #Ceil(@Arg1)) + [simplification] + ``` #### Boolean Interpretation @@ -604,6 +627,11 @@ endmodule module WASM-DATA-CONCRETE [concrete] imports WASM-DATA-COMMON + syntax Int ::= #signedTotal ( IValType , Int) [function, total, klabel(#signedTotal), symbol, smtlib(signedTotal)] + + rule #signedTotal ( TYPE:IValType , VAL:Int) => #signed(TYPE, VAL) + requires definedSigned(TYPE, VAL) + rule [wrap-Positive] : #wrap(WIDTH, N) => N &Int ((1 < #signed(Arg0, Arg1) + requires definedSigned(Arg0, Arg1) + [concrete, simplification] + + rule #signed(Arg0:IValType, Arg1:Int) + => #signedTotal(Arg0, Arg1) + requires definedSigned(Arg0, Arg1) + [symbolic(Arg0), simplification] + + rule #signed(Arg0:IValType, Arg1:Int) + => #signedTotal(Arg0, Arg1) + requires definedSigned(Arg0, Arg1) + [symbolic(Arg1), simplification] + + rule [wrap-Positive] : #wrap(WIDTH, N) => N &Int ((1 < Date: Tue, 26 Sep 2023 19:32:23 +0300 Subject: [PATCH 04/16] Add an Int-to-Int map --- data/int-type.k | 11 + data/map-int-to-int.k | 463 ++++++++++++++++++++++++++++++++++++++++++ wasm.md | 3 + 3 files changed, 477 insertions(+) create mode 100644 data/int-type.k create mode 100644 data/map-int-to-int.k diff --git a/data/int-type.k b/data/int-type.k new file mode 100644 index 000000000..43bd31ab6 --- /dev/null +++ b/data/int-type.k @@ -0,0 +1,11 @@ + +module INT-TYPE + import INT + + syntax WrappedInt + syntax Int + + syntax WrappedInt ::= wrap(Int) [symbol, klabel(wrapInt)] + syntax Int ::= unwrap(WrappedInt) [function, total, injective, symbol, klabel(unwrapInt)] + rule unwrap(wrap(A:Int)) => A +endmodule diff --git a/data/map-int-to-int.k b/data/map-int-to-int.k new file mode 100644 index 000000000..d0e87a94d --- /dev/null +++ b/data/map-int-to-int.k @@ -0,0 +1,463 @@ + +require "int-type.k" +// require "int-type.k" + +module MAP-INT-TO-INT + imports private BOOL-SYNTAX + imports private INT-SYNTAX + // imports private LIST-INT + // imports private LIST-INT + imports private LIST + // imports private SET-INT + imports private SET + imports INT-TYPE + imports INT-TYPE + + syntax Int + syntax Int + + syntax MapIntToInt [hook(MAP.Map)] + syntax MapIntToInt ::= MapIntToInt MapIntToInt + [ left, function, hook(MAP.concat), klabel(_MapIntToInt_), + symbol, assoc, comm, unit(.MapIntToInt), element(_Int2Int|->_), + index(0), format(%1%n%2) + ] + syntax MapIntToInt ::= ".MapIntToInt" + [ function, total, hook(MAP.unit), + klabel(.MapIntToInt), symbol, latex(\dotCt{MapIntToInt}) + ] + syntax MapIntToInt ::= WrappedInt "Int2Int|->" WrappedInt + [ function, total, hook(MAP.element), + klabel(_Int2Int|->_), symbol, + latex({#1}\mapsto{#2}), injective + ] + + syntax priorities _Int2Int|->_ > _MapIntToInt_ .MapIntToInt + syntax non-assoc _Int2Int|->_ + syntax WrappedInt ::= MapIntToInt "[" WrappedInt "]" + [function, hook(MAP.lookup), klabel(MapIntToInt:lookup), symbol] + syntax WrappedInt ::= MapIntToInt "[" WrappedInt "]" "orDefault" WrappedInt + [ function, total, hook(MAP.lookupOrDefault), + klabel(MapIntToInt:lookupOrDefault), symbol + ] + syntax MapIntToInt ::= MapIntToInt "[" key: WrappedInt "<-" value: WrappedInt "]" + [ function, total, klabel(MapIntToInt:update), symbol, + hook(MAP.update), prefer + ] + syntax MapIntToInt ::= MapIntToInt "[" WrappedInt "<-" "undef" "]" + [ function, total, hook(MAP.remove), + klabel(_MapIntToInt[_<-undef]), symbol + ] + syntax MapIntToInt ::= MapIntToInt "-Map" MapIntToInt + [ function, total, hook(MAP.difference), + latex({#1}-_{\it MapIntToIntMap}{#2}) + ] + syntax MapIntToInt ::= updateMap(MapIntToInt, MapIntToInt) + [function, total, hook(MAP.updateAll)] + + syntax MapIntToInt ::= removeAll(MapIntToInt, Set) + [function, total, hook(MAP.removeAll)] + // syntax MapIntToInt ::= removeAll(MapIntToInt, SetInt) + // [function, total, hook(MAP.removeAll)] + + syntax Set ::= keys(MapIntToInt) + [function, total, hook(MAP.keys)] + // syntax SetInt ::= keys(MapIntToInt) + // [function, total, hook(MAP.keys)] + + syntax List ::= "keys_list" "(" MapIntToInt ")" + [function, hook(MAP.keys_list)] + // syntax ListInt ::= "keys_list" "(" MapIntToInt ")" + // [function, hook(MAP.keys_list)] + + syntax Bool ::= WrappedInt "in_keys" "(" MapIntToInt ")" + [function, total, hook(MAP.in_keys)] + + syntax List ::= values(MapIntToInt) + [function, hook(MAP.values)] + // syntax ListInt ::= values(MapIntToInt) + // [function, hook(MAP.values)] + + syntax Int ::= size(MapIntToInt) + [function, total, hook(MAP.size), klabel(MapIntToInt.sizeMap), symbol] + syntax Bool ::= MapIntToInt "<=Map" MapIntToInt + [function, total, hook(MAP.inclusion)] + syntax WrappedInt ::= choice(MapIntToInt) + [function, hook(MAP.choice), klabel(MapIntToInt:choice), symbol] +endmodule + +module MAP-INT-TO-INT-PRIMITIVE + imports MAP-INT-TO-INT-PRIMITIVE-CONCRETE + imports MAP-INT-TO-INT-PRIMITIVE-SYMBOLIC +endmodule + +module MAP-INT-TO-INT-PRIMITIVE-CONCRETE [concrete] + imports public BOOL + imports private K-EQUAL + imports public MAP-INT-TO-INT + + syntax Int ::= MapIntToInt "{{" Int "}}" + [function, klabel(MapIntToInt:primitiveLookup), symbol] + syntax Int ::= MapIntToInt "{{" Int "}}" "orDefault" Int + [ function, total, klabel(MapIntToInt:primitiveLookupOrDefault), symbol ] + syntax MapIntToInt ::= MapIntToInt "{{" key: Int "<-" value: Int "}}" + [ function, total, klabel(MapIntToInt:primitiveUpdate), symbol, + prefer + ] + syntax MapIntToInt ::= MapIntToInt "{{" Int "<-" "undef" "}}" + [ function, total, klabel(MapIntToInt:primitiveRemove), symbol ] + syntax Bool ::= Int "in_keys" "{{" MapIntToInt "}}" + [function, total, klabel(MapIntToInt:primitiveInKeys), symbol] + + rule (M:MapIntToInt {{ Key:Int }}) + => (unwrap( M[wrap(Key)] )) + rule M:MapIntToInt {{ Key:Int }} orDefault Value:Int + => unwrap( M[wrap(Key)] orDefault wrap(Value) ) + rule M:MapIntToInt {{ Key:Int <- Value:Int }} + => M[wrap(Key) <- wrap(Value)] + rule M:MapIntToInt {{ Key:Int <- undef }} + => M[wrap(Key) <- undef] + rule Key:Int in_keys {{ M:MapIntToInt }} => wrap(Key) in_keys(M) +endmodule + +module MAP-INT-TO-INT-PRIMITIVE-SYMBOLIC [symbolic] + imports public BOOL + imports private K-EQUAL + imports public MAP-INT-TO-INT + imports private MAP-INT-TO-INT-KORE-SYMBOLIC + + syntax Int ::= MapIntToInt "{{" Int "}}" + [function, symbol, klabel(MapIntToInt:primitiveLookup)] + syntax Int ::= MapIntToInt "{{" Int "}}" "orDefault" Int + [ function, total, symbol, klabel(MapIntToInt:primitiveLookupOrDefault) ] + syntax MapIntToInt ::= MapIntToInt "{{" key: Int "<-" value: Int "}}" + [ function, total, klabel(MapIntToInt:primitiveUpdate), symbol, + prefer + ] + syntax MapIntToInt ::= MapIntToInt "{{" Int "<-" "undef" "}}" + [ function, total, symbol, klabel(MapIntToInt:primitiveRemove) ] + syntax Bool ::= Int "in_keys" "{{" MapIntToInt "}}" + [function, total, symbol, klabel(MapIntToInt:primitiveInKeys)] + + // Definitions + // ----------- + + rule (wrap(Key) Int2Int|-> V:WrappedInt M:MapIntToInt) + {{ Key:Int }} + => unwrap( V ) + ensures notBool Key in_keys {{ M }} + + rule (wrap(Key) Int2Int|-> V:WrappedInt M:MapIntToInt) + {{ Key:Int }} orDefault _:Int + => unwrap( V ) + ensures notBool Key in_keys {{ M }} + rule M:MapIntToInt {{ Key:Int }} orDefault V:Int + => V + requires notBool Key in_keys {{ M }} + + rule (wrap(Key) Int2Int|-> _:WrappedInt M:MapIntToInt) + {{ Key:Int <- Value:Int }} + => (wrap(Key) Int2Int|-> wrap(Value)) M + rule M:MapIntToInt {{ Key:Int <- Value:Int }} + => (wrap(Key) Int2Int|-> wrap(Value)) M + requires notBool Key in_keys {{ M }} + + rule (wrap(Key) Int2Int|-> _:WrappedInt M:MapIntToInt) + {{ Key:Int <- undef }} + => M + ensures notBool Key in_keys {{ M }} + rule M:MapIntToInt {{ Key:Int <- undef }} + => M + requires notBool Key in_keys {{ M }} + + rule Key:Int in_keys + {{wrap(Key) Int2Int|-> _:WrappedInt M:MapIntToInt}} + => true + ensures notBool Key in_keys {{ M }} + rule _Key:Int in_keys {{ .MapIntToInt }} + => false + // TODO: This may create an exponential evaluation tree, depending on how + // caching works in the backend. It should be rewritten to finish in + // O(n^2) or something like that, where n is the number of explicit keys + // in the map. + rule Key:Int in_keys + {{Key2:WrappedInt Int2Int|-> _:WrappedInt M:MapIntToInt}} + => Key in_keys {{ M }} + requires Key =/=K unwrap( Key2 ) + ensures notBool Key2 in_keys (M) + [simplification] + + // Translation rules + rule M:MapIntToInt[Key:WrappedInt] + => wrap(M{{unwrap( Key )}}) + [simplification, symbolic(M)] + rule M:MapIntToInt[Key:WrappedInt] + => wrap(M{{unwrap( Key )}}) + [simplification, symbolic(Key)] + rule M:MapIntToInt{{Key}} + => unwrap( M[wrap(Key)] ) + [simplification, concrete] + + rule M:MapIntToInt [ Key:WrappedInt ] orDefault Value:WrappedInt + => wrap(M {{ unwrap( Key ) }} orDefault unwrap( Value )) + [simplification, symbolic(M)] + rule M:MapIntToInt [ Key:WrappedInt ] orDefault Value:WrappedInt + => wrap(M {{ unwrap( Key ) }} orDefault unwrap( Value )) + [simplification, symbolic(Key)] + rule M:MapIntToInt [ Key:WrappedInt ] orDefault Value:WrappedInt + => wrap(M {{ unwrap( Key ) }} orDefault unwrap( Value )) + [simplification, symbolic(Value)] + rule M:MapIntToInt{{Key}} orDefault Value + => unwrap( M[wrap(Key)] orDefault wrap(Value) ) + [simplification, concrete] + + rule M:MapIntToInt[Key:WrappedInt <- Value:WrappedInt] + => M {{ unwrap( Key ) <- unwrap( Value ) }} + [simplification, symbolic(M)] + rule M:MapIntToInt[Key:WrappedInt <- Value:WrappedInt] + => M {{ unwrap( Key ) <- unwrap( Value ) }} + [simplification, symbolic(Key)] + rule M:MapIntToInt[Key:WrappedInt <- Value:WrappedInt] + => M {{ unwrap( Key ) <- unwrap( Value ) }} + [simplification, symbolic(Value)] + rule M:MapIntToInt{{Key <- Value}} => M[wrap(Key) <- wrap(Value) ] + [simplification, concrete] + + rule M:MapIntToInt[Key:WrappedInt <- undef] + => M {{ unwrap( Key ) <- undef }} + [simplification, symbolic(M)] + rule M:MapIntToInt[Key:WrappedInt <- undef] + => M {{ unwrap( Key ) <- undef }} + [simplification, symbolic(Key)] + rule M:MapIntToInt{{Key <- undef}} => M[wrap(Key) <- undef] + [simplification, concrete] + + rule Key:WrappedInt in_keys (M:MapIntToInt) + => unwrap( Key ) in_keys {{M}} + [simplification, symbolic(M)] + rule Key:WrappedInt in_keys (M:MapIntToInt) + => unwrap( Key ) in_keys {{M}} + [simplification, symbolic(Key)] + rule Key in_keys {{M:MapIntToInt}} => wrap(Key) in_keys(M) + [simplification, concrete] + + // Symbolic execution rules + // ------------------------ + syntax Bool ::= definedPrimitiveLookup(MapIntToInt, Int) [function, total] + rule definedPrimitiveLookup(M:MapIntToInt, K:Int) => K in_keys{{M}} + + rule #Ceil(@M:MapIntToInt {{@K:Int}}) + => {definedPrimitiveLookup(@M, @K) #Equals true} + #And #Ceil(@M) #And #Ceil(@K) + [simplification] + + rule M:MapIntToInt {{ K <- _ }} {{ K <- V }} => M {{ K <- V }} [simplification] + rule (K1 Int2Int|-> V1 M:MapIntToInt) {{ K2 <- V2 }} + => (K1 Int2Int|-> V1 (M {{ K2 <- V2 }})) + requires unwrap( K1 ) =/=K K2 + [simplification] + + rule (K1 Int2Int|-> V1 M:MapIntToInt) {{ K2 <- undef }} + => (K1 Int2Int|-> V1 (M {{ K2 <- undef }})) + requires unwrap( K1 ) =/=K K2 + [simplification] + + rule (K1 Int2Int|-> _V M:MapIntToInt) {{ K2 }} => M {{K2}} + requires unwrap( K1 ) =/=K K2 + ensures notBool (K1 in_keys(M)) + [simplification] + rule (_MAP:MapIntToInt {{ K <- V1 }}) {{ K }} => V1 [simplification] + rule ( MAP:MapIntToInt {{ K1 <- _V1 }}) {{ K2 }} => MAP {{ K2 }} + requires K1 =/=K K2 + [simplification] + + rule (K1 Int2Int|-> _V M:MapIntToInt) {{ K2 }} orDefault D + => M {{K2}} orDefault D + requires unwrap( K1 ) =/=K K2 + ensures notBool (K1 in_keys(M)) + [simplification] + rule (_MAP:MapIntToInt {{ K <- V1 }}) {{ K }} orDefault _ => V1 [simplification] + rule ( MAP:MapIntToInt {{ K1 <- _V1 }}) {{ K2 }} orDefault D + => MAP {{ K2 }} orDefault D + requires K1 =/=K K2 + [simplification] + + rule K in_keys{{_M:MapIntToInt {{ K <- undef }} }} => false [simplification] + rule K in_keys{{_M:MapIntToInt {{ K <- _ }} }} => true [simplification] + rule K1 in_keys{{ M:MapIntToInt {{ K2 <- _ }} }} + => true requires K1 ==K K2 orBool K1 in_keys{{M}} + [simplification] + rule K1 in_keys{{ M:MapIntToInt {{ K2 <- _ }} }} + => K1 in_keys {{ M }} + requires K1 =/=K K2 + [simplification] + + rule K1 in_keys {{ (K2 Int2Int|-> V) M:MapIntToInt }} + => K1 ==K unwrap( K2 ) orBool K1 in_keys {{ M }} + requires definedMapElementConcat(K2, V, M) + [simplification(100)] + + + rule {false #Equals @Key in_keys{{ Key' Int2Int|-> Val @M:MapIntToInt }}} + => #Ceil(@Key) #And #Ceil(Key' Int2Int|-> Val @M) + #And #Not({ @Key #Equals unwrap( Key' ) }) + #And {false #Equals @Key in_keys{{@M}}} + [simplification] + rule {@Key in_keys{{Key' Int2Int|-> Val @M:MapIntToInt}} #Equals false} + => #Ceil(@Key) #And #Ceil(Key' Int2Int|-> Val @M) + #And #Not({@Key #Equals unwrap( Key' ) }) + #And {@Key in_keys{{@M}} #Equals false} + [simplification] + +endmodule + +module MAP-INT-TO-INT-KORE-SYMBOLIC + imports MAP-INT-TO-INT + imports private K-EQUAL + imports private BOOL + + syntax Bool ::= definedMapElementConcat(WrappedInt, WrappedInt, MapIntToInt) [function, total] + rule definedMapElementConcat(K, _V, M:MapIntToInt) => notBool K in_keys(M) + + rule #Ceil(@M:MapIntToInt [@K:WrappedInt]) + => {(@K in_keys(@M)) #Equals true} + #And #Ceil(@M) #And #Ceil(@K) + [simplification] + + rule (K Int2Int|-> _ M:MapIntToInt) [ K <- V ] => (K Int2Int|-> V M) [simplification] + rule M:MapIntToInt [ K <- V ] => (K Int2Int|-> V M) requires notBool (K in_keys(M)) + [simplification] + rule M:MapIntToInt [ K <- _ ] [ K <- V ] => M [ K <- V ] [simplification] + rule (K1 Int2Int|-> V1 M:MapIntToInt) [ K2 <- V2 ] => (K1 Int2Int|-> V1 (M [ K2 <- V2 ])) + requires K1 =/=K K2 + [simplification] + + rule (K Int2Int|-> _ M:MapIntToInt) [ K <- undef ] => M + ensures notBool (K in_keys(M)) + [simplification] + rule M:MapIntToInt [ K <- undef ] => M + requires notBool (K in_keys(M)) + [simplification] + rule (K1 Int2Int|-> V1 M:MapIntToInt) [ K2 <- undef ] + => (K1 Int2Int|-> V1 (M [ K2 <- undef ])) + requires K1 =/=K K2 + [simplification] + + rule (K Int2Int|-> V M:MapIntToInt) [ K ] => V + ensures notBool (K in_keys(M)) + [simplification] + rule (K1 Int2Int|-> _V M:MapIntToInt) [ K2 ] => M [K2] + requires K1 =/=K K2 + ensures notBool (K1 in_keys(M)) + [simplification] + rule (_MAP:MapIntToInt [ K <- V1 ]) [ K ] => V1 [simplification] + rule ( MAP:MapIntToInt [ K1 <- _V1 ]) [ K2 ] => MAP [ K2 ] + requires K1 =/=K K2 + [simplification] + + rule (K Int2Int|-> V M:MapIntToInt) [ K ] orDefault _ => V + ensures notBool (K in_keys(M)) + [simplification] + rule (K1 Int2Int|-> _V M:MapIntToInt) [ K2 ] orDefault D + => M [K2] orDefault D + requires K1 =/=K K2 + ensures notBool (K1 in_keys(M)) + [simplification] + rule (_MAP:MapIntToInt [ K <- V1 ]) [ K ] orDefault _ => V1 [simplification] + rule ( MAP:MapIntToInt [ K1 <- _V1 ]) [ K2 ] orDefault D + => MAP [ K2 ] orDefault D + requires K1 =/=K K2 + [simplification] + rule .MapIntToInt [ _ ] orDefault D => D [simplification] + + rule K in_keys(_M:MapIntToInt [ K <- undef ]) => false [simplification] + rule K in_keys(_M:MapIntToInt [ K <- _ ]) => true [simplification] + rule K1 in_keys(M:MapIntToInt [ K2 <- _ ]) + => true requires K1 ==K K2 orBool K1 in_keys(M) + [simplification] + rule K1 in_keys(M:MapIntToInt [ K2 <- _ ]) + => K1 in_keys(M) + requires K1 =/=K K2 + [simplification] + + rule K in_keys((K Int2Int|-> V) M:MapIntToInt) + => true + requires definedMapElementConcat(K, V, M) + [simplification(50)] + rule K1 in_keys((K2 Int2Int|-> V) M:MapIntToInt) + => K1 in_keys(M) + requires true + andBool definedMapElementConcat(K2, V, M) + andBool K1 =/=K K2 + [simplification(50)] + rule K1 in_keys((K2 Int2Int|-> V) M:MapIntToInt) + => K1 ==K K2 orBool K1 in_keys(M) + requires definedMapElementConcat(K2, V, M) + [simplification(100)] + + + rule {false #Equals @Key in_keys(.MapIntToInt)} => #Ceil(@Key) [simplification] + rule {@Key in_keys(.MapIntToInt) #Equals false} => #Ceil(@Key) [simplification] + rule {false #Equals @Key in_keys(Key' Int2Int|-> Val @M:MapIntToInt)} + => #Ceil(@Key) #And #Ceil(Key' Int2Int|-> Val @M) + #And #Not({@Key #Equals Key'}) + #And {false #Equals @Key in_keys(@M)} + [simplification] + rule {@Key in_keys(Key' Int2Int|-> Val @M:MapIntToInt) #Equals false} + => #Ceil(@Key) #And #Ceil(Key' Int2Int|-> Val @M) + #And #Not({@Key #Equals Key'}) + #And {@Key in_keys(@M) #Equals false} + [simplification] +endmodule + +module MAP-INT-TO-INT-CURLY-BRACE + imports private BOOL + imports private K-EQUAL-SYNTAX + imports MAP-INT-TO-INT + + syntax MapIntToInt ::= MapIntToInt "{" key:WrappedInt "<-" value:WrappedInt "}" + [function, total, symbol, klabel(MapIntToInt:curly_update)] + rule M:MapIntToInt{Key <- Value} => M (Key Int2Int|-> Value) + requires notBool Key in_keys(M) + rule (Key Int2Int|-> _ M:MapIntToInt){Key <- Value} + => M (Key Int2Int|-> Value) + rule (M:MapIntToInt{Key <- Value})(A Int2Int|-> B N:MapIntToInt) + => (M (A Int2Int|-> B)) {Key <- Value} N + requires notBool A ==K Key + [simplification] + + rule M:MapIntToInt{Key1 <- Value1}[Key2 <- Value2] + => ((M:MapIntToInt[Key2 <- Value2]{Key1 <- Value1}) #And #Not ({Key1 #Equals Key2})) + #Or ((M:MapIntToInt[Key2 <- Value2]) #And {Key1 #Equals Key2}) + [simplification(20)] + rule M:MapIntToInt[Key <- Value] + => M:MapIntToInt{Key <- Value} + [simplification(100)] + rule M:MapIntToInt{Key1 <- _Value1}[Key2] orDefault Value2 + => M[Key2] orDefault Value2 + requires Key1 =/=K Key2 + [simplification] + rule _M:MapIntToInt{Key <- Value1}[Key] orDefault _Value2 + => Value1 + [simplification] + // rule M:MapIntToInt{Key1 <- Value1}[Key2] orDefault Value2 + // => (M[Key2] orDefault Value2 #And #Not ({Key1 #Equals Key2})) + // #Or (Value1 #And {Key1 #Equals Key2}) + // [simplification] + rule M:MapIntToInt{Key1 <- Value1}[Key2] + => (M[Key2] #And #Not ({Key1 #Equals Key2})) + #Or (Value1 #And {Key1 #Equals Key2}) + [simplification] + + rule Key1 in_keys(_:MapIntToInt{Key1 <- _}) + => true + [simplification(50)] + rule Key1 in_keys(M:MapIntToInt{Key2 <- _}) + => Key1 in_keys(M) + requires notBool Key1 ==K Key2 + [simplification(50)] + rule K1 in_keys(M:MapIntToInt { K2 <- _ }) + => K1 ==K K2 orBool K1 in_keys(M) + [simplification(100)] + +endmodule diff --git a/wasm.md b/wasm.md index 6a7acc856..42a806521 100644 --- a/wasm.md +++ b/wasm.md @@ -3,6 +3,7 @@ WebAssembly State and Semantics ```k require "data.md" +require "data/map-int-to-int.k" require "numeric.md" module WASM-SYNTAX @@ -156,6 +157,8 @@ Semantics ```k module WASM + imports MAP-INT-TO-INT + imports MAP-INT-TO-INT-PRIMITIVE imports WASM-COMMON-SYNTAX imports WASM-DATA imports WASM-NUMERIC From ac2d70a1e09e3f114d2ad0f3b5710af5ad712da9 Mon Sep 17 00:00:00 2001 From: Virgil Date: Tue, 26 Sep 2023 19:33:12 +0300 Subject: [PATCH 05/16] Use an Int-to-Int map for --- media/201903-report-chalmers.md | 2 +- media/memory-demo/memory-spec.k | 6 ++-- media/memory-demo/wasm.k | 6 ++-- test.md | 4 +-- tests/proofs/memory-spec.k | 4 +-- tests/proofs/wrc20-spec.k | 2 +- wasm.md | 54 ++++++++++++++++----------------- 7 files changed, 39 insertions(+), 39 deletions(-) diff --git a/media/201903-report-chalmers.md b/media/201903-report-chalmers.md index 886c3402b..10ad7770e 100644 --- a/media/201903-report-chalmers.md +++ b/media/201903-report-chalmers.md @@ -800,7 +800,7 @@ This is the full definition of the `(memory.grow)` operation: #then SIZE #else -1 #fi ... - 0 |-> ADDR + wrap(0) Int2Int|-> wrap(ADDR) ADDR MAX diff --git a/media/memory-demo/memory-spec.k b/media/memory-demo/memory-spec.k index e8dc009c5..3c12d7cdd 100644 --- a/media/memory-demo/memory-spec.k +++ b/media/memory-demo/memory-spec.k @@ -2,14 +2,14 @@ module MEMORY-SPEC imports WASM rule ( memory.size ) => (i32.const SZ) ... - 0 |-> A + wrap(0) Int2Int|-> wrap(A) A SZ rule (memory.grow (i32.const X)) => (i32.const SZ) ... - 0 |-> A + wrap(0) Int2Int|-> wrap(A) A SZ => (SZ +Int X) @@ -21,7 +21,7 @@ module MEMORY-SPEC andBool SZ >=Int 0 rule (memory.grow (i32.const X)) => (i32.const -1) ... - 0 |-> A + wrap(0) Int2Int|-> wrap(A) A SZ diff --git a/media/memory-demo/wasm.k b/media/memory-demo/wasm.k index 4d3e548da..d17cd5707 100644 --- a/media/memory-demo/wasm.k +++ b/media/memory-demo/wasm.k @@ -104,7 +104,7 @@ endmodule false rule (( memory ) ~> ELSE) => ELSE - .Map => 0 |-> NEXT + .MapIntToInt => wrap(0) Int2Int|-> wrap(NEXT) NEXT => NEXT +Int 1 (.Bag => @@ -118,7 +118,7 @@ endmodule syntax Instr ::= "(" "memory.size" ")" // -------------------------------------- rule ( memory.size ) => ( i32.const SZ ) ... - 0 |-> A + wrap(0) Int2Int|-> wrap(A) A SZ @@ -131,7 +131,7 @@ endmodule rule (memory.grow I:Instr) => I ~> (memory.grow) ... rule (memory.grow) => (i32.const SZ) ... < i32 > V : S => S - 0 |-> A + wrap(0) Int2Int|-> wrap(A) A SZ => SZ +Int V diff --git a/test.md b/test.md index 9f7ac1cd3..5c6645889 100644 --- a/test.md +++ b/test.md @@ -450,7 +450,7 @@ This checks that the last allocated memory has the given size and max value. CUR IDS - #ContextLookup(IDS, TFIDX) |-> ADDR + wrap(#ContextLookup(IDS, TFIDX)) Int2Int|-> wrap(ADDR) ... @@ -472,7 +472,7 @@ This checks that the last allocated memory has the given size and max value. rule #assertMemoryData MODIDX (KEY , VAL) _MSG => . ... MODIDX - 0 |-> ADDR + wrap(0) Int2Int|-> wrap(ADDR) ... diff --git a/tests/proofs/memory-spec.k b/tests/proofs/memory-spec.k index 1c8d93beb..b5aa94446 100644 --- a/tests/proofs/memory-spec.k +++ b/tests/proofs/memory-spec.k @@ -7,7 +7,7 @@ module MEMORY-SPEC CUR CUR - 0 |-> MEMADDR + wrap(0) Int2Int|-> wrap(MEMADDR) ... @@ -24,7 +24,7 @@ module MEMORY-SPEC CUR CUR - 0 |-> MEMADDR + wrap(0) Int2Int|-> wrap(MEMADDR) ... diff --git a/tests/proofs/wrc20-spec.k b/tests/proofs/wrc20-spec.k index 9ee3f2e33..79915773a 100644 --- a/tests/proofs/wrc20-spec.k +++ b/tests/proofs/wrc20-spec.k @@ -20,7 +20,7 @@ module WRC20-SPEC CUR #wrc20ReverseBytesTypeIdx |-> #wrc20ReverseBytesType - 0 |-> MEMADDR + wrap(0) Int2Int|-> wrap(MEMADDR) _ => ?_ NEXTFUNCIDX => NEXTFUNCIDX +Int 1 ... diff --git a/wasm.md b/wasm.md index 42a806521..7fe44378d 100644 --- a/wasm.md +++ b/wasm.md @@ -179,24 +179,24 @@ module WASM .Map - 0 - .Map - .Map - 0 - .Map - 0 - .Map - .Map - .Map - .Map - .Map - .Map - 0 + 0 + .Map + .Map + 0 + .Map + 0 + .Map + .Map + .Map + .MapIntToInt + .Map + .Map + 0 .String - - .Map - .Map + + .Map + .Map @@ -930,7 +930,7 @@ The importing and exporting parts of specifications are dealt with in the respec CUR IDS => #saveId(IDS, ID, 0) - .Map => (0 |-> NEXTADDR) + .MapIntToInt => (wrap(0) Int2Int|-> wrap(NEXTADDR)) ... NEXTADDR => NEXTADDR +Int 1 @@ -964,7 +964,7 @@ The value is encoded as bytes and stored at the "effective address", which is th CUR CUR - 0 |-> ADDR + wrap(0) Int2Int|-> wrap(ADDR) ... @@ -979,7 +979,7 @@ The value is encoded as bytes and stored at the "effective address", which is th CUR CUR - 0 |-> ADDR + wrap(0) Int2Int|-> wrap(ADDR) ... @@ -1022,7 +1022,7 @@ Sort `Signedness` is defined in module `BYTES`. CUR CUR - 0 |-> ADDR + wrap(0) Int2Int|-> wrap(ADDR) ... @@ -1037,7 +1037,7 @@ Sort `Signedness` is defined in module `BYTES`. CUR CUR - 0 |-> ADDR + wrap(0) Int2Int|-> wrap(ADDR) ... @@ -1058,7 +1058,7 @@ The `size` operation returns the size of the memory, measured in pages. CUR CUR - 0 |-> ADDR + wrap(0) Int2Int|-> wrap(ADDR) ... @@ -1084,7 +1084,7 @@ By setting the `` field in the configuration to `true CUR CUR - 0 |-> ADDR + wrap(0) Int2Int|-> wrap(ADDR) ... @@ -1100,7 +1100,7 @@ By setting the `` field in the configuration to `true CUR CUR - 0 |-> ADDR + wrap(0) Int2Int|-> wrap(ADDR) ... @@ -1186,7 +1186,7 @@ The `data` initializer simply puts these bytes into the specified memory, starti CUR CUR - MEMIDX |-> ADDR + wrap(MEMIDX) Int2Int|-> wrap(ADDR) ... @@ -1302,14 +1302,14 @@ The value of a global gets copied when it is imported. CUR IDS => #saveId(IDS, OID, 0) - .Map => 0 |-> ADDR + .MapIntToInt => wrap(0) Int2Int|-> wrap(ADDR) ... ... MOD |-> MODIDX ... MODIDX IDS' - ... #ContextLookup(IDS' , TFIDX) |-> ADDR ... + ... wrap(#ContextLookup(IDS' , TFIDX)) Int2Int|-> wrap(ADDR) ... ... NAME |-> TFIDX ... ... From fc028a89a3d0e6ccb748568ea351cdd745a40142 Mon Sep 17 00:00:00 2001 From: Virgil Date: Tue, 26 Sep 2023 19:40:04 +0300 Subject: [PATCH 06/16] Int-to-Int map for --- test.md | 4 ++-- wasm.md | 16 ++++++++-------- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/test.md b/test.md index 5c6645889..382c59204 100644 --- a/test.md +++ b/test.md @@ -168,7 +168,7 @@ We allow 2 kinds of actions: MODIDX ... ENAME |-> IDX ... - ... IDX |-> FADDR ... + ... wrap(IDX) Int2Int|-> wrap(FADDR) ... ... @@ -380,7 +380,7 @@ This simply checks that the given function exists in the `` cell and has CUR CUR - ... IDX |-> FADDR ... + ... wrap(IDX) Int2Int|-> wrap(FADDR) ... ... diff --git a/wasm.md b/wasm.md index 7fe44378d..4cf6195bc 100644 --- a/wasm.md +++ b/wasm.md @@ -183,7 +183,7 @@ module WASM .Map .Map 0 - .Map + .MapIntToInt 0 .Map .Map @@ -698,7 +698,7 @@ The importing and exporting parts of specifications are dealt with in the respec CUR ... TYPIDX |-> TYPE ... NEXTIDX => NEXTIDX +Int 1 - ADDRS => ADDRS [ NEXTIDX <- NEXTADDR ] + ADDRS => ADDRS {{ NEXTIDX <- NEXTADDR }} ... NEXTADDR => NEXTADDR +Int 1 @@ -783,7 +783,7 @@ The `#take` function will return the parameter stack in the reversed order, then CUR CUR - ... IDX |-> FADDR ... + ... wrap(IDX) Int2Int|-> wrap(FADDR) ... ... ``` @@ -1145,7 +1145,7 @@ A table index is optional and will be default to zero. syntax ElemDefn ::= #elem(index : Int, offset : Instrs, elemSegment : Ints) [klabel(aElemDefn), symbol] | "elem" "{" Int Ints "}" - syntax Stmt ::= #initElements ( Int, Int, Map, Ints ) + syntax Stmt ::= #initElements ( Int, Int, MapIntToInt, Ints ) // ----------------------------------------------------- rule #elem(TABIDX, IS, ELEMSEGMENT ) => sequenceInstrs(IS) ~> elem { TABIDX ELEMSEGMENT } ... @@ -1163,7 +1163,7 @@ A table index is optional and will be default to zero. rule #initElements ( ADDR, OFFSET, FADDRS, E:Int ES ) => #initElements ( ADDR, OFFSET +Int 1, FADDRS, ES ) ... ADDR - DATA => DATA [ OFFSET <- FADDRS[E] ] + DATA => DATA [ OFFSET <- FADDRS{{E}} ] ... ``` @@ -1212,7 +1212,7 @@ The `start` component of a module declares the function index of a `start functi CUR CUR - ... IDX |-> FADDR ... + ... wrap(IDX) Int2Int|-> wrap(FADDR) ... ... ``` @@ -1255,14 +1255,14 @@ The value of a global gets copied when it is imported. CUR TYPES - FS => FS [NEXT <- ADDR] + FS => FS {{ NEXT <- ADDR }} NEXT => NEXT +Int 1 ... ... MOD |-> MODIDX ... MODIDX - ... IDX |-> ADDR ... + ... wrap(IDX) Int2Int|-> wrap(ADDR) ... ... NAME |-> IDX ... ... From 78f41ebe1188039b324bd4082a93e36b10e9aafb Mon Sep 17 00:00:00 2001 From: Virgil Date: Tue, 26 Sep 2023 20:03:47 +0300 Subject: [PATCH 07/16] Make intBinOp total --- numeric.md | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/numeric.md b/numeric.md index a502e00c1..847c07910 100644 --- a/numeric.md +++ b/numeric.md @@ -184,11 +184,19 @@ There are 7 unary operators for floats: `abs`, `neg`, `sqrt`, `floor`, `ceil`, ` A `*BinOp` operator always produces a result of the same type as its operands. ```k - syntax Val ::= IValType "." IBinOp Int Int [klabel(intBinOp) , function] - | FValType "." FBinOp Float Float [klabel(floatBinOp), function] + syntax Val ::= IValType "." IBinOp Int Int [klabel(intBinOp) , symbol, function, total] + | FValType "." FBinOp Float Float [klabel(floatBinOp), symbol, function] // ----------------------------------------------------------------------------- ``` +Make intBinOp total + +```k + +rule _:IValType . _:IBinOp _:Int _:Int => undefined [owise] + +``` + #### Binary Operators for Integers There are 12 binary operators for integers: `add`, `sub`, `mul`, `div_sx`, `rem_sx`, `and`, `or`, `xor`, `shl`, `shr_sx`, `rotl`, `rotr`. @@ -220,6 +228,7 @@ There are 12 binary operators for integers: `add`, `sub`, `mul`, `div_sx`, `rem_ rule ITYPE . div_s I1 I2 => < ITYPE > #unsigned(ITYPE, #signed(ITYPE, I1) /Int #signed(ITYPE, I2)) requires I2 =/=Int 0 + andBool definedSigned(ITYPE, I1) andBool definedSigned(ITYPE, I2) andBool #signed(ITYPE, I1) /Int #signed(ITYPE, I2) =/=Int #pow1(ITYPE) rule _ITYPE . div_s _I1 I2 => undefined @@ -231,6 +240,7 @@ There are 12 binary operators for integers: `add`, `sub`, `mul`, `div_sx`, `rem_ rule ITYPE . rem_s I1 I2 => < ITYPE > #unsigned(ITYPE, #signed(ITYPE, I1) %Int #signed(ITYPE, I2)) requires I2 =/=Int 0 + andBool definedSigned(ITYPE, I1) andBool definedSigned(ITYPE, I2) rule _ITYPE . rem_s _I1 I2 => undefined requires I2 ==Int 0 @@ -261,6 +271,7 @@ Careful attention is made for the signed version `shr_s`. rule ITYPE . shr_u I1 I2 => < ITYPE > I1 >>Int (I2 %Int #width(ITYPE)) rule ITYPE . shr_s I1 I2 => < ITYPE > #unsigned(ITYPE, #signed(ITYPE, I1) >>Int (I2 %Int #width(ITYPE))) + requires definedSigned(ITYPE, I1) ``` - `rotl` returns the result of rotating the first operand left by k bits, in which k is the second operand modulo N. From 34f84b3f82be72dc2c1ab0a14575a81da4cc8ccf Mon Sep 17 00:00:00 2001 From: Virgil Date: Tue, 26 Sep 2023 20:07:42 +0300 Subject: [PATCH 08/16] Make intRelOp total --- numeric.md | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) diff --git a/numeric.md b/numeric.md index 847c07910..74dbf10a7 100644 --- a/numeric.md +++ b/numeric.md @@ -332,11 +332,19 @@ There is no test operation for float numbers. Relationship Operators consume two operands and produce a bool, which is an `i32` value. ```k - syntax Val ::= IValType "." IRelOp Int Int [klabel(intRelOp) , function] - | FValType "." FRelOp Float Float [klabel(floatRelOp), function] + syntax Val ::= IValType "." IRelOp Int Int [klabel(intRelOp) , symbol, function, total] + | FValType "." FRelOp Float Float [klabel(floatRelOp), symbol, function] // ----------------------------------------------------------------------------- ``` +Make intRelOp total. + +```k + +rule _:IValType . _:IRelOp _:Int _:Int => undefined [owise] + +``` + ### Relationship Operators for Integers There are 6 relationship operators for integers: `eq`, `ne`, `lt_sx`, `gt_sx`, `le_sx` and `ge_sx`. @@ -357,7 +365,9 @@ There are 6 relationship operators for integers: `eq`, `ne`, `lt_sx`, `gt_sx`, ` rule _ . gt_u I1 I2 => < i32 > #bool(I1 >Int I2) rule ITYPE . lt_s I1 I2 => < i32 > #bool(#signed(ITYPE, I1) < i32 > #bool(#signed(ITYPE, I1) >Int #signed(ITYPE, I2)) + requires definedSigned(ITYPE, I1) andBool definedSigned(ITYPE, I2) ``` - `le_sx` returns 1 if the first oprand is less than or equal to the second opeand, 0 otherwise. @@ -368,7 +378,9 @@ There are 6 relationship operators for integers: `eq`, `ne`, `lt_sx`, `gt_sx`, ` rule _ . ge_u I1 I2 => < i32 > #bool(I1 >=Int I2) rule ITYPE . le_s I1 I2 => < i32 > #bool(#signed(ITYPE, I1) <=Int #signed(ITYPE, I2)) + requires definedSigned(ITYPE, I1) andBool definedSigned(ITYPE, I2) rule ITYPE . ge_s I1 I2 => < i32 > #bool(#signed(ITYPE, I1) >=Int #signed(ITYPE, I2)) + requires definedSigned(ITYPE, I1) andBool definedSigned(ITYPE, I2) ``` ### Relationship Operators for Floats From d4047f8c19d1d215763780351b45993dbcb21d30 Mon Sep 17 00:00:00 2001 From: Virgil Date: Tue, 26 Sep 2023 20:11:06 +0300 Subject: [PATCH 09/16] Update without map unification. --- kwasm-lemmas.md | 1 + wasm.md | 6 ++++-- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/kwasm-lemmas.md b/kwasm-lemmas.md index 7728729a0..492b2ae96 100644 --- a/kwasm-lemmas.md +++ b/kwasm-lemmas.md @@ -11,6 +11,7 @@ module KWASM-LEMMAS [symbolic] imports WASM-TEXT imports BYTES-KORE imports INT-SYMBOLIC + imports MAP-SYMBOLIC ``` Basic logic diff --git a/wasm.md b/wasm.md index 4cf6195bc..6e4a3de65 100644 --- a/wasm.md +++ b/wasm.md @@ -532,11 +532,13 @@ The `*_local` instructions are defined here. rule #local.set(I) => . ... VALUE : VALSTACK => VALSTACK - ... I |-> (_ => VALUE) ... + LOCALS => LOCALS[I <- VALUE] + requires I in_keys(LOCALS) rule #local.tee(I) => . ... VALUE : _VALSTACK - ... I |-> (_ => VALUE) ... + LOCALS => LOCALS[I <- VALUE] + requires I in_keys(LOCALS) ``` ### Globals From 038e66b9749caa8ab5d0fe5159a160956cfdbf41 Mon Sep 17 00:00:00 2001 From: Virgil Date: Tue, 26 Sep 2023 20:14:27 +0300 Subject: [PATCH 10/16] Use lookup for in #call instead of map unification. --- wasm.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/wasm.md b/wasm.md index 6e4a3de65..120e63e5e 100644 --- a/wasm.md +++ b/wasm.md @@ -781,13 +781,14 @@ The `#take` function will return the parameter stack in the reversed order, then ```k syntax Instr ::= #call(Int) [klabel(aCall), symbol] // --------------------------------------------------- - rule #call(IDX) => ( invoke FADDR ) ... + rule #call(IDX) => ( invoke FUNCADDRS {{ IDX }} orDefault 0 ) ... CUR CUR - ... wrap(IDX) Int2Int|-> wrap(FADDR) ... + FUNCADDRS ... + requires IDX in_keys {{ FUNCADDRS }} ``` ```k From 6d3ca0d7742dc34dc4042aec41626e8cea0ee396 Mon Sep 17 00:00:00 2001 From: Virgil Date: Tue, 26 Sep 2023 20:35:35 +0300 Subject: [PATCH 11/16] Split store evaluation to use one map unification per rewrite --- wasm.md | 16 +++++++--------- 1 file changed, 7 insertions(+), 9 deletions(-) diff --git a/wasm.md b/wasm.md index 120e63e5e..6ffa7b616 100644 --- a/wasm.md +++ b/wasm.md @@ -959,17 +959,21 @@ The value is encoded as bytes and stored at the "effective address", which is th | IValType "." StoreOp Int Int // | FValType "." StoreOp Int Float | "store" "{" Int Int Number "}" + | "store" "{" Int Int Number Int "}" // ----------------------------------------------- rule #store(ITYPE:IValType, SOP, OFFSET) => ITYPE . SOP (IDX +Int OFFSET) VAL ... < ITYPE > VAL : < i32 > IDX : VALSTACK => VALSTACK - rule store { WIDTH EA VAL } => . ... + rule store { WIDTH EA VAL } => store { WIDTH EA VAL (MEMADDRS{{0}} orDefault 0) } ... CUR CUR - wrap(0) Int2Int|-> wrap(ADDR) + MEMADDRS ... + requires 0 in_keys{{MEMADDRS}} andBool size(MEMADDRS) ==Int 1 + + rule store { WIDTH EA VAL ADDR } => . ... ADDR SIZE @@ -978,13 +982,7 @@ The value is encoded as bytes and stored at the "effective address", which is th requires (EA +Int WIDTH) <=Int (SIZE *Int #pageSize()) - rule store { WIDTH EA _ } => trap ... - CUR - - CUR - wrap(0) Int2Int|-> wrap(ADDR) - ... - + rule store { WIDTH EA _ ADDR } => trap ... ADDR SIZE From 515b11cd71168897dd251b602a936260207d4f1c Mon Sep 17 00:00:00 2001 From: Virgil Date: Tue, 26 Sep 2023 20:39:46 +0300 Subject: [PATCH 12/16] Split load evaluation to use one map unification per rewrite --- wasm.md | 21 +++++++++------------ 1 file changed, 9 insertions(+), 12 deletions(-) diff --git a/wasm.md b/wasm.md index 6ffa7b616..791548201 100644 --- a/wasm.md +++ b/wasm.md @@ -1004,8 +1004,8 @@ Sort `Signedness` is defined in module `BYTES`. ```k syntax Instr ::= #load(ValType, LoadOp, offset : Int) [klabel(aLoad), symbol] | "load" "{" IValType Int Int Signedness"}" + | "load" "{" IValType Int Int Signedness Int"}" | "load" "{" IValType Int Int Signedness Bytes"}" - | "load" "{" IValType Int Int Signedness"}" | IValType "." LoadOp Int // ---------------------------------------- rule #load(ITYPE:IValType, LOP, OFFSET) => ITYPE . LOP (IDX +Int OFFSET) ... @@ -1019,13 +1019,16 @@ Sort `Signedness` is defined in module `BYTES`. rule ITYPE . load16_s EA:Int => load { ITYPE 2 EA Signed } ... rule i64 . load32_s EA:Int => load { i64 4 EA Signed } ... - rule load { ITYPE WIDTH EA SIGN } => load { ITYPE WIDTH EA SIGN DATA } ... + rule load { ITYPE WIDTH EA SIGN } => load { ITYPE WIDTH EA SIGN (MEMADDRS{{0}} orDefault 0)} ... CUR CUR - wrap(0) Int2Int|-> wrap(ADDR) + MEMADDRS ... + requires 0 in_keys{{MEMADDRS}} andBool size(MEMADDRS) ==Int 1 + + rule load { ITYPE WIDTH EA SIGN ADDR:Int} => load { ITYPE WIDTH EA SIGN DATA } ... ADDR SIZE @@ -1034,13 +1037,7 @@ Sort `Signedness` is defined in module `BYTES`. requires (EA +Int WIDTH) <=Int (SIZE *Int #pageSize()) - rule load { _ WIDTH EA _ } => trap ... - CUR - - CUR - wrap(0) Int2Int|-> wrap(ADDR) - ... - + rule load { _ WIDTH EA _ ADDR:Int} => trap ... ADDR SIZE @@ -1048,8 +1045,8 @@ Sort `Signedness` is defined in module `BYTES`. requires (EA +Int WIDTH) >Int (SIZE *Int #pageSize()) - rule load { ITYPE WIDTH EA Signed DATA } => #chop(< ITYPE > #signedWidth(WIDTH, #getRange(DATA, EA, WIDTH))) ... - rule load { ITYPE WIDTH EA Unsigned DATA } => < ITYPE > #getRange(DATA, EA, WIDTH) ... + rule load { ITYPE WIDTH EA Signed DATA:Bytes } => #chop(< ITYPE > #signedWidth(WIDTH, #getRange(DATA, EA, WIDTH))) ... + rule load { ITYPE WIDTH EA Unsigned DATA:Bytes } => < ITYPE > #getRange(DATA, EA, WIDTH) ... ``` The `size` operation returns the size of the memory, measured in pages. From 5ea94621acf68369346e0ab3e0ecebf78e1a7abe Mon Sep 17 00:00:00 2001 From: Virgil Date: Wed, 27 Sep 2023 14:03:13 +0300 Subject: [PATCH 13/16] Fix KBuild file --- kbuild.toml | 1 + 1 file changed, 1 insertion(+) diff --git a/kbuild.toml b/kbuild.toml index dfce7681b..3a909ea98 100644 --- a/kbuild.toml +++ b/kbuild.toml @@ -5,6 +5,7 @@ source = "." [targets.llvm] main-file = 'test.md' +main-module = 'WASM-TEST' backend='llvm' [targets.haskell] From e11cfaf9919eddeafa644d8f6149d26119a53907 Mon Sep 17 00:00:00 2001 From: Virgil Date: Wed, 27 Sep 2023 20:52:04 +0300 Subject: [PATCH 14/16] Remove concrete signedTotal --- data.md | 5 ----- 1 file changed, 5 deletions(-) diff --git a/data.md b/data.md index e174724bf..706aec381 100644 --- a/data.md +++ b/data.md @@ -627,11 +627,6 @@ endmodule module WASM-DATA-CONCRETE [concrete] imports WASM-DATA-COMMON - syntax Int ::= #signedTotal ( IValType , Int) [function, total, klabel(#signedTotal), symbol, smtlib(signedTotal)] - - rule #signedTotal ( TYPE:IValType , VAL:Int) => #signed(TYPE, VAL) - requires definedSigned(TYPE, VAL) - rule [wrap-Positive] : #wrap(WIDTH, N) => N &Int ((1 < Date: Wed, 27 Sep 2023 13:44:11 +0300 Subject: [PATCH 15/16] Map int to val for --- auxil.md | 32 +- data/map-int-to-val.k | 463 ++++++++++++++++++ .../201906-presentation-wasm-on-blockchain.md | 6 +- media/202001-presentation-dlab.md | 6 +- media/berlin-demo/div1-spec.k | 4 +- media/berlin-demo/div2-spec.k | 4 +- media/berlin-demo/div3-spec.k | 4 +- media/berlin-demo/div4-spec.k | 4 +- test.md | 5 +- tests/proofs/locals-spec.k | 2 +- tests/proofs/loops-spec.k | 8 +- wasm.md | 23 +- 12 files changed, 513 insertions(+), 48 deletions(-) create mode 100644 data/map-int-to-val.k diff --git a/auxil.md b/auxil.md index f84d19dcf..3d30b53c2 100644 --- a/auxil.md +++ b/auxil.md @@ -15,23 +15,23 @@ module WASM-AUXIL syntax Auxil ::= "#clearConfig" // ------------------------------- rule [clearConfig]: - #clearConfig => . ... - _ => .Int - _ => .ValStack - _ => .Map - _ => .Bag - _ => .Map - _ => 0 - _ => .Map + #clearConfig => . ... + _ => .Int + _ => .ValStack + _ => .MapIntToVal + _ => .Bag + _ => .Map + _ => 0 + _ => .Map - _ => 0 - _ => .Bag - _ => 0 - _ => .Bag - _ => 0 - _ => .Bag - _ => 0 - _ => .Bag + _ => 0 + _ => .Bag + _ => 0 + _ => .Bag + _ => 0 + _ => .Bag + _ => 0 + _ => .Bag endmodule diff --git a/data/map-int-to-val.k b/data/map-int-to-val.k new file mode 100644 index 000000000..f0fc9924b --- /dev/null +++ b/data/map-int-to-val.k @@ -0,0 +1,463 @@ + +require "int-type.k" +// require "val-type.k" + +module MAP-INT-TO-VAL + imports private BOOL-SYNTAX + imports private INT-SYNTAX + // imports private LIST-INT + // imports private LIST-VAL + imports private LIST + // imports private SET-INT + imports private SET + imports INT-TYPE + // imports VAL-TYPE + + syntax Int + syntax Val + + syntax MapIntToVal [hook(MAP.Map)] + syntax MapIntToVal ::= MapIntToVal MapIntToVal + [ left, function, hook(MAP.concat), klabel(_MapIntToVal_), + symbol, assoc, comm, unit(.MapIntToVal), element(_Int2Val|->_), + index(0), format(%1%n%2) + ] + syntax MapIntToVal ::= ".MapIntToVal" + [ function, total, hook(MAP.unit), + klabel(.MapIntToVal), symbol, latex(\dotCt{MapIntToVal}) + ] + syntax MapIntToVal ::= WrappedInt "Int2Val|->" Val + [ function, total, hook(MAP.element), + klabel(_Int2Val|->_), symbol, + latex({#1}\mapsto{#2}), injective + ] + + syntax priorities _Int2Val|->_ > _MapIntToVal_ .MapIntToVal + syntax non-assoc _Int2Val|->_ + syntax Val ::= MapIntToVal "[" WrappedInt "]" + [function, hook(MAP.lookup), klabel(MapIntToVal:lookup), symbol] + syntax Val ::= MapIntToVal "[" WrappedInt "]" "orDefault" Val + [ function, total, hook(MAP.lookupOrDefault), + klabel(MapIntToVal:lookupOrDefault), symbol + ] + syntax MapIntToVal ::= MapIntToVal "[" key: WrappedInt "<-" value: Val "]" + [ function, total, klabel(MapIntToVal:update), symbol, + hook(MAP.update), prefer + ] + syntax MapIntToVal ::= MapIntToVal "[" WrappedInt "<-" "undef" "]" + [ function, total, hook(MAP.remove), + klabel(_MapIntToVal[_<-undef]), symbol + ] + syntax MapIntToVal ::= MapIntToVal "-Map" MapIntToVal + [ function, total, hook(MAP.difference), + latex({#1}-_{\it MapIntToValMap}{#2}) + ] + syntax MapIntToVal ::= updateMap(MapIntToVal, MapIntToVal) + [function, total, hook(MAP.updateAll)] + + syntax MapIntToVal ::= removeAll(MapIntToVal, Set) + [function, total, hook(MAP.removeAll)] + // syntax MapIntToVal ::= removeAll(MapIntToVal, SetInt) + // [function, total, hook(MAP.removeAll)] + + syntax Set ::= keys(MapIntToVal) + [function, total, hook(MAP.keys)] + // syntax SetInt ::= keys(MapIntToVal) + // [function, total, hook(MAP.keys)] + + syntax List ::= "keys_list" "(" MapIntToVal ")" + [function, hook(MAP.keys_list)] + // syntax ListInt ::= "keys_list" "(" MapIntToVal ")" + // [function, hook(MAP.keys_list)] + + syntax Bool ::= WrappedInt "in_keys" "(" MapIntToVal ")" + [function, total, hook(MAP.in_keys)] + + syntax List ::= values(MapIntToVal) + [function, hook(MAP.values)] + // syntax ListVal ::= values(MapIntToVal) + // [function, hook(MAP.values)] + + syntax Int ::= size(MapIntToVal) + [function, total, hook(MAP.size), klabel(MapIntToVal.sizeMap), symbol] + syntax Bool ::= MapIntToVal "<=Map" MapIntToVal + [function, total, hook(MAP.inclusion)] + syntax WrappedInt ::= choice(MapIntToVal) + [function, hook(MAP.choice), klabel(MapIntToVal:choice), symbol] +endmodule + +module MAP-INT-TO-VAL-PRIMITIVE + imports MAP-INT-TO-VAL-PRIMITIVE-CONCRETE + imports MAP-INT-TO-VAL-PRIMITIVE-SYMBOLIC +endmodule + +module MAP-INT-TO-VAL-PRIMITIVE-CONCRETE [concrete] + imports public BOOL + imports private K-EQUAL + imports public MAP-INT-TO-VAL + + syntax Val ::= MapIntToVal "{{" Int "}}" + [function, klabel(MapIntToVal:primitiveLookup), symbol] + syntax Val ::= MapIntToVal "{{" Int "}}" "orDefault" Val + [ function, total, klabel(MapIntToVal:primitiveLookupOrDefault), symbol ] + syntax MapIntToVal ::= MapIntToVal "{{" key: Int "<-" value: Val "}}" + [ function, total, klabel(MapIntToVal:primitiveUpdate), symbol, + prefer + ] + syntax MapIntToVal ::= MapIntToVal "{{" Int "<-" "undef" "}}" + [ function, total, klabel(MapIntToVal:primitiveRemove), symbol ] + syntax Bool ::= Int "in_keys" "{{" MapIntToVal "}}" + [function, total, klabel(MapIntToVal:primitiveInKeys), symbol] + + rule (M:MapIntToVal {{ Key:Int }}) + => (M[wrap(Key)]) + rule M:MapIntToVal {{ Key:Int }} orDefault Value:Val + => M[wrap(Key)] orDefault Value + rule M:MapIntToVal {{ Key:Int <- Value:Val }} + => M[wrap(Key) <- Value] + rule M:MapIntToVal {{ Key:Int <- undef }} + => M[wrap(Key) <- undef] + rule Key:Int in_keys {{ M:MapIntToVal }} => wrap(Key) in_keys(M) +endmodule + +module MAP-INT-TO-VAL-PRIMITIVE-SYMBOLIC [symbolic] + imports public BOOL + imports private K-EQUAL + imports public MAP-INT-TO-VAL + imports private MAP-INT-TO-VAL-KORE-SYMBOLIC + + syntax Val ::= MapIntToVal "{{" Int "}}" + [function, symbol, klabel(MapIntToVal:primitiveLookup)] + syntax Val ::= MapIntToVal "{{" Int "}}" "orDefault" Val + [ function, total, symbol, klabel(MapIntToVal:primitiveLookupOrDefault) ] + syntax MapIntToVal ::= MapIntToVal "{{" key: Int "<-" value: Val "}}" + [ function, total, klabel(MapIntToVal:primitiveUpdate), symbol, + prefer + ] + syntax MapIntToVal ::= MapIntToVal "{{" Int "<-" "undef" "}}" + [ function, total, symbol, klabel(MapIntToVal:primitiveRemove) ] + syntax Bool ::= Int "in_keys" "{{" MapIntToVal "}}" + [function, total, symbol, klabel(MapIntToVal:primitiveInKeys)] + + // Definitions + // ----------- + + rule (wrap(Key) Int2Val|-> V:Val M:MapIntToVal) + {{ Key:Int }} + => V + ensures notBool Key in_keys {{ M }} + + rule (wrap(Key) Int2Val|-> V:Val M:MapIntToVal) + {{ Key:Int }} orDefault _:Val + => V + ensures notBool Key in_keys {{ M }} + rule M:MapIntToVal {{ Key:Int }} orDefault V:Val + => V + requires notBool Key in_keys {{ M }} + + rule (wrap(Key) Int2Val|-> _:Val M:MapIntToVal) + {{ Key:Int <- Value:Val }} + => (wrap(Key) Int2Val|-> Value) M + rule M:MapIntToVal {{ Key:Int <- Value:Val }} + => (wrap(Key) Int2Val|-> Value) M + requires notBool Key in_keys {{ M }} + + rule (wrap(Key) Int2Val|-> _:Val M:MapIntToVal) + {{ Key:Int <- undef }} + => M + ensures notBool Key in_keys {{ M }} + rule M:MapIntToVal {{ Key:Int <- undef }} + => M + requires notBool Key in_keys {{ M }} + + rule Key:Int in_keys + {{wrap(Key) Int2Val|-> _:Val M:MapIntToVal}} + => true + ensures notBool Key in_keys {{ M }} + rule _Key:Int in_keys {{ .MapIntToVal }} + => false + // TODO: This may create an exponential evaluation tree, depending on how + // caching works in the backend. It should be rewritten to finish in + // O(n^2) or something like that, where n is the number of explicit keys + // in the map. + rule Key:Int in_keys + {{Key2:WrappedInt Int2Val|-> _:Val M:MapIntToVal}} + => Key in_keys {{ M }} + requires Key =/=K unwrap( Key2 ) + ensures notBool Key2 in_keys (M) + [simplification] + + // Translation rules + rule M:MapIntToVal[Key:WrappedInt] + => M{{unwrap( Key )}} + [simplification, symbolic(M)] + rule M:MapIntToVal[Key:WrappedInt] + => M{{unwrap( Key )}} + [simplification, symbolic(Key)] + rule M:MapIntToVal{{Key}} + => M[wrap(Key)] + [simplification, concrete] + + rule M:MapIntToVal [ Key:WrappedInt ] orDefault Value:Val + => M {{ unwrap( Key ) }} orDefault Value + [simplification, symbolic(M)] + rule M:MapIntToVal [ Key:WrappedInt ] orDefault Value:Val + => M {{ unwrap( Key ) }} orDefault Value + [simplification, symbolic(Key)] + rule M:MapIntToVal [ Key:WrappedInt ] orDefault Value:Val + => M {{ unwrap( Key ) }} orDefault Value + [simplification, symbolic(Value)] + rule M:MapIntToVal{{Key}} orDefault Value + => M[wrap(Key)] orDefault Value + [simplification, concrete] + + rule M:MapIntToVal[Key:WrappedInt <- Value:Val] + => M {{ unwrap( Key ) <- Value }} + [simplification, symbolic(M)] + rule M:MapIntToVal[Key:WrappedInt <- Value:Val] + => M {{ unwrap( Key ) <- Value }} + [simplification, symbolic(Key)] + rule M:MapIntToVal[Key:WrappedInt <- Value:Val] + => M {{ unwrap( Key ) <- Value }} + [simplification, symbolic(Value)] + rule M:MapIntToVal{{Key <- Value}} => M[wrap(Key) <- Value ] + [simplification, concrete] + + rule M:MapIntToVal[Key:WrappedInt <- undef] + => M {{ unwrap( Key ) <- undef }} + [simplification, symbolic(M)] + rule M:MapIntToVal[Key:WrappedInt <- undef] + => M {{ unwrap( Key ) <- undef }} + [simplification, symbolic(Key)] + rule M:MapIntToVal{{Key <- undef}} => M[wrap(Key) <- undef] + [simplification, concrete] + + rule Key:WrappedInt in_keys (M:MapIntToVal) + => unwrap( Key ) in_keys {{M}} + [simplification, symbolic(M)] + rule Key:WrappedInt in_keys (M:MapIntToVal) + => unwrap( Key ) in_keys {{M}} + [simplification, symbolic(Key)] + rule Key in_keys {{M:MapIntToVal}} => wrap(Key) in_keys(M) + [simplification, concrete] + + // Symbolic execution rules + // ------------------------ + syntax Bool ::= definedPrimitiveLookup(MapIntToVal, Int) [function, total] + rule definedPrimitiveLookup(M:MapIntToVal, K:Int) => K in_keys{{M}} + + rule #Ceil(@M:MapIntToVal {{@K:Int}}) + => {definedPrimitiveLookup(@M, @K) #Equals true} + #And #Ceil(@M) #And #Ceil(@K) + [simplification] + + rule M:MapIntToVal {{ K <- _ }} {{ K <- V }} => M {{ K <- V }} [simplification] + rule (K1 Int2Val|-> V1 M:MapIntToVal) {{ K2 <- V2 }} + => (K1 Int2Val|-> V1 (M {{ K2 <- V2 }})) + requires unwrap( K1 ) =/=K K2 + [simplification] + + rule (K1 Int2Val|-> V1 M:MapIntToVal) {{ K2 <- undef }} + => (K1 Int2Val|-> V1 (M {{ K2 <- undef }})) + requires unwrap( K1 ) =/=K K2 + [simplification] + + rule (K1 Int2Val|-> _V M:MapIntToVal) {{ K2 }} => M {{K2}} + requires unwrap( K1 ) =/=K K2 + ensures notBool (K1 in_keys(M)) + [simplification] + rule (_MAP:MapIntToVal {{ K <- V1 }}) {{ K }} => V1 [simplification] + rule ( MAP:MapIntToVal {{ K1 <- _V1 }}) {{ K2 }} => MAP {{ K2 }} + requires K1 =/=K K2 + [simplification] + + rule (K1 Int2Val|-> _V M:MapIntToVal) {{ K2 }} orDefault D + => M {{K2}} orDefault D + requires unwrap( K1 ) =/=K K2 + ensures notBool (K1 in_keys(M)) + [simplification] + rule (_MAP:MapIntToVal {{ K <- V1 }}) {{ K }} orDefault _ => V1 [simplification] + rule ( MAP:MapIntToVal {{ K1 <- _V1 }}) {{ K2 }} orDefault D + => MAP {{ K2 }} orDefault D + requires K1 =/=K K2 + [simplification] + + rule K in_keys{{_M:MapIntToVal {{ K <- undef }} }} => false [simplification] + rule K in_keys{{_M:MapIntToVal {{ K <- _ }} }} => true [simplification] + rule K1 in_keys{{ M:MapIntToVal {{ K2 <- _ }} }} + => true requires K1 ==K K2 orBool K1 in_keys{{M}} + [simplification] + rule K1 in_keys{{ M:MapIntToVal {{ K2 <- _ }} }} + => K1 in_keys {{ M }} + requires K1 =/=K K2 + [simplification] + + rule K1 in_keys {{ (K2 Int2Val|-> V) M:MapIntToVal }} + => K1 ==K unwrap( K2 ) orBool K1 in_keys {{ M }} + requires definedMapElementConcat(K2, V, M) + [simplification(100)] + + + rule {false #Equals @Key in_keys{{ Key' Int2Val|-> Val @M:MapIntToVal }}} + => #Ceil(@Key) #And #Ceil(Key' Int2Val|-> Val @M) + #And #Not({ @Key #Equals unwrap( Key' ) }) + #And {false #Equals @Key in_keys{{@M}}} + [simplification] + rule {@Key in_keys{{Key' Int2Val|-> Val @M:MapIntToVal}} #Equals false} + => #Ceil(@Key) #And #Ceil(Key' Int2Val|-> Val @M) + #And #Not({@Key #Equals unwrap( Key' ) }) + #And {@Key in_keys{{@M}} #Equals false} + [simplification] + +endmodule + +module MAP-INT-TO-VAL-KORE-SYMBOLIC + imports MAP-INT-TO-VAL + imports private K-EQUAL + imports private BOOL + + syntax Bool ::= definedMapElementConcat(WrappedInt, Val, MapIntToVal) [function, total] + rule definedMapElementConcat(K, _V, M:MapIntToVal) => notBool K in_keys(M) + + rule #Ceil(@M:MapIntToVal [@K:WrappedInt]) + => {(@K in_keys(@M)) #Equals true} + #And #Ceil(@M) #And #Ceil(@K) + [simplification] + + rule (K Int2Val|-> _ M:MapIntToVal) [ K <- V ] => (K Int2Val|-> V M) [simplification] + rule M:MapIntToVal [ K <- V ] => (K Int2Val|-> V M) requires notBool (K in_keys(M)) + [simplification] + rule M:MapIntToVal [ K <- _ ] [ K <- V ] => M [ K <- V ] [simplification] + rule (K1 Int2Val|-> V1 M:MapIntToVal) [ K2 <- V2 ] => (K1 Int2Val|-> V1 (M [ K2 <- V2 ])) + requires K1 =/=K K2 + [simplification] + + rule (K Int2Val|-> _ M:MapIntToVal) [ K <- undef ] => M + ensures notBool (K in_keys(M)) + [simplification] + rule M:MapIntToVal [ K <- undef ] => M + requires notBool (K in_keys(M)) + [simplification] + rule (K1 Int2Val|-> V1 M:MapIntToVal) [ K2 <- undef ] + => (K1 Int2Val|-> V1 (M [ K2 <- undef ])) + requires K1 =/=K K2 + [simplification] + + rule (K Int2Val|-> V M:MapIntToVal) [ K ] => V + ensures notBool (K in_keys(M)) + [simplification] + rule (K1 Int2Val|-> _V M:MapIntToVal) [ K2 ] => M [K2] + requires K1 =/=K K2 + ensures notBool (K1 in_keys(M)) + [simplification] + rule (_MAP:MapIntToVal [ K <- V1 ]) [ K ] => V1 [simplification] + rule ( MAP:MapIntToVal [ K1 <- _V1 ]) [ K2 ] => MAP [ K2 ] + requires K1 =/=K K2 + [simplification] + + rule (K Int2Val|-> V M:MapIntToVal) [ K ] orDefault _ => V + ensures notBool (K in_keys(M)) + [simplification] + rule (K1 Int2Val|-> _V M:MapIntToVal) [ K2 ] orDefault D + => M [K2] orDefault D + requires K1 =/=K K2 + ensures notBool (K1 in_keys(M)) + [simplification] + rule (_MAP:MapIntToVal [ K <- V1 ]) [ K ] orDefault _ => V1 [simplification] + rule ( MAP:MapIntToVal [ K1 <- _V1 ]) [ K2 ] orDefault D + => MAP [ K2 ] orDefault D + requires K1 =/=K K2 + [simplification] + rule .MapIntToVal [ _ ] orDefault D => D [simplification] + + rule K in_keys(_M:MapIntToVal [ K <- undef ]) => false [simplification] + rule K in_keys(_M:MapIntToVal [ K <- _ ]) => true [simplification] + rule K1 in_keys(M:MapIntToVal [ K2 <- _ ]) + => true requires K1 ==K K2 orBool K1 in_keys(M) + [simplification] + rule K1 in_keys(M:MapIntToVal [ K2 <- _ ]) + => K1 in_keys(M) + requires K1 =/=K K2 + [simplification] + + rule K in_keys((K Int2Val|-> V) M:MapIntToVal) + => true + requires definedMapElementConcat(K, V, M) + [simplification(50)] + rule K1 in_keys((K2 Int2Val|-> V) M:MapIntToVal) + => K1 in_keys(M) + requires true + andBool definedMapElementConcat(K2, V, M) + andBool K1 =/=K K2 + [simplification(50)] + rule K1 in_keys((K2 Int2Val|-> V) M:MapIntToVal) + => K1 ==K K2 orBool K1 in_keys(M) + requires definedMapElementConcat(K2, V, M) + [simplification(100)] + + + rule {false #Equals @Key in_keys(.MapIntToVal)} => #Ceil(@Key) [simplification] + rule {@Key in_keys(.MapIntToVal) #Equals false} => #Ceil(@Key) [simplification] + rule {false #Equals @Key in_keys(Key' Int2Val|-> Val @M:MapIntToVal)} + => #Ceil(@Key) #And #Ceil(Key' Int2Val|-> Val @M) + #And #Not({@Key #Equals Key'}) + #And {false #Equals @Key in_keys(@M)} + [simplification] + rule {@Key in_keys(Key' Int2Val|-> Val @M:MapIntToVal) #Equals false} + => #Ceil(@Key) #And #Ceil(Key' Int2Val|-> Val @M) + #And #Not({@Key #Equals Key'}) + #And {@Key in_keys(@M) #Equals false} + [simplification] +endmodule + +module MAP-INT-TO-VAL-CURLY-BRACE + imports private BOOL + imports private K-EQUAL-SYNTAX + imports MAP-INT-TO-VAL + + syntax MapIntToVal ::= MapIntToVal "{" key:WrappedInt "<-" value:Val "}" + [function, total, symbol, klabel(MapIntToVal:curly_update)] + rule M:MapIntToVal{Key <- Value} => M (Key Int2Val|-> Value) + requires notBool Key in_keys(M) + rule (Key Int2Val|-> _ M:MapIntToVal){Key <- Value} + => M (Key Int2Val|-> Value) + rule (M:MapIntToVal{Key <- Value})(A Int2Val|-> B N:MapIntToVal) + => (M (A Int2Val|-> B)) {Key <- Value} N + requires notBool A ==K Key + [simplification] + + rule M:MapIntToVal{Key1 <- Value1}[Key2 <- Value2] + => ((M:MapIntToVal[Key2 <- Value2]{Key1 <- Value1}) #And #Not ({Key1 #Equals Key2})) + #Or ((M:MapIntToVal[Key2 <- Value2]) #And {Key1 #Equals Key2}) + [simplification(20)] + rule M:MapIntToVal[Key <- Value] + => M:MapIntToVal{Key <- Value} + [simplification(100)] + rule M:MapIntToVal{Key1 <- _Value1}[Key2] orDefault Value2 + => M[Key2] orDefault Value2 + requires Key1 =/=K Key2 + [simplification] + rule _M:MapIntToVal{Key <- Value1}[Key] orDefault _Value2 + => Value1 + [simplification] + // rule M:MapIntToVal{Key1 <- Value1}[Key2] orDefault Value2 + // => (M[Key2] orDefault Value2 #And #Not ({Key1 #Equals Key2})) + // #Or (Value1 #And {Key1 #Equals Key2}) + // [simplification] + rule M:MapIntToVal{Key1 <- Value1}[Key2] + => (M[Key2] #And #Not ({Key1 #Equals Key2})) + #Or (Value1 #And {Key1 #Equals Key2}) + [simplification] + + rule Key1 in_keys(_:MapIntToVal{Key1 <- _}) + => true + [simplification(50)] + rule Key1 in_keys(M:MapIntToVal{Key2 <- _}) + => Key1 in_keys(M) + requires notBool Key1 ==K Key2 + [simplification(50)] + rule K1 in_keys(M:MapIntToVal { K2 <- _ }) + => K1 ==K K2 orBool K1 in_keys(M) + [simplification(100)] + +endmodule diff --git a/media/201906-presentation-wasm-on-blockchain.md b/media/201906-presentation-wasm-on-blockchain.md index c09d4c3a7..68f145813 100644 --- a/media/201906-presentation-wasm-on-blockchain.md +++ b/media/201906-presentation-wasm-on-blockchain.md @@ -175,9 +175,9 @@ K Specifications: Configuration Tell K about the structure of your execution state. ```k - configuration $PGM:Instrs - .ValStack - .Map + configuration $PGM:Instrs + .ValStack + .MapIntToVal ``` . . . diff --git a/media/202001-presentation-dlab.md b/media/202001-presentation-dlab.md index ac464cc30..0a342287c 100644 --- a/media/202001-presentation-dlab.md +++ b/media/202001-presentation-dlab.md @@ -156,9 +156,9 @@ This would allow parsing a program like this: Tell \K about the structure of your execution state. ```k - configuration $PGM:Instrs - .ValStack - .Map + configuration $PGM:Instrs + .ValStack + .MapIntToVal ``` . . . diff --git a/media/berlin-demo/div1-spec.k b/media/berlin-demo/div1-spec.k index 015011518..3c2c89434 100644 --- a/media/berlin-demo/div1-spec.k +++ b/media/berlin-demo/div1-spec.k @@ -14,8 +14,8 @@ module DIV1-SPEC => . - 0 |-> < i32 > (X => X') - 1 |-> < i32 > Y + wrap(0) |-> < i32 > (X => X') + wrap(1) |-> < i32 > Y // We must specify that X and Y fulfill the invariant for locals to // be in the unsigned range. Otherwise, X and Y can be *any* integers. diff --git a/media/berlin-demo/div2-spec.k b/media/berlin-demo/div2-spec.k index f0c98bf68..1b2925bb6 100644 --- a/media/berlin-demo/div2-spec.k +++ b/media/berlin-demo/div2-spec.k @@ -19,8 +19,8 @@ module DIV2-SPEC => . - 0 |-> < i32 > (X => X') - 1 |-> < i32 > Y + wrap(0) |-> < i32 > (X => X') + wrap(1) |-> < i32 > Y requires #inUnsignedRange(i32, X) andBool #inUnsignedRange(i32, Y) diff --git a/media/berlin-demo/div3-spec.k b/media/berlin-demo/div3-spec.k index 7331ce99c..7a98b5fab 100644 --- a/media/berlin-demo/div3-spec.k +++ b/media/berlin-demo/div3-spec.k @@ -19,8 +19,8 @@ module DIV3-SPEC => . - 0 |-> < i32 > (X => X') - 1 |-> < i32 > Y + wrap(0) |-> < i32 > (X => X') + wrap(1) |-> < i32 > Y requires #inUnsignedRange(i32, X) andBool #inUnsignedRange(i32, Y) diff --git a/media/berlin-demo/div4-spec.k b/media/berlin-demo/div4-spec.k index 71b5bea4f..9af883970 100644 --- a/media/berlin-demo/div4-spec.k +++ b/media/berlin-demo/div4-spec.k @@ -23,8 +23,8 @@ module DIV4-SPEC => . - 0 |-> < i32 > (X => X') - 1 |-> < i32 > Y + wrap(0) |-> < i32 > (X => X') + wrap(1) |-> < i32 > Y requires #inUnsignedRange(i32, X) andBool #inUnsignedRange(i32, Y) diff --git a/test.md b/test.md index 382c59204..27da163fd 100644 --- a/test.md +++ b/test.md @@ -322,8 +322,9 @@ The operator `#assertLocal`/`#assertGlobal` operators perform a check for a loca syntax Assertion ::= "#assertLocal" Int Val WasmString | "#assertGlobal" Index Val WasmString // --------------------------------------------------------- - rule #assertLocal INDEX VALUE _ => . ... - ... INDEX |-> VALUE ... + rule #assertLocal INDEX (LOCALS{{INDEX}} orDefault undefined) _ => . ... + LOCALS + requires INDEX in_keys{{LOCALS}} rule #assertGlobal TFIDX VALUE _ => . ... CUR diff --git a/tests/proofs/locals-spec.k b/tests/proofs/locals-spec.k index b4afe22eb..536dd4fc4 100644 --- a/tests/proofs/locals-spec.k +++ b/tests/proofs/locals-spec.k @@ -5,6 +5,6 @@ module LOCALS-SPEC claim #local.get(X) ~> #local.set(X) => . ... - X |-> < _ITYPE > (VAL => VAL) + wrap(X) |-> < _ITYPE > (VAL => VAL) endmodule diff --git a/tests/proofs/loops-spec.k b/tests/proofs/loops-spec.k index 6f62a7a05..943c5ee77 100644 --- a/tests/proofs/loops-spec.k +++ b/tests/proofs/loops-spec.k @@ -29,8 +29,8 @@ module LOOPS-SPEC _ => STACK - 0 |-> < ITYPE > (I => 0) - 1 |-> < ITYPE > (X => X +Int ((I *Int (I +Int 1)) /Int 2)) + wrap(0) |-> < ITYPE > (I => 0) + wrap(1) |-> < ITYPE > (X => X +Int ((I *Int (I +Int 1)) /Int 2)) requires #inUnsignedRange(ITYPE, I) andBool I >Int 0 @@ -60,8 +60,8 @@ module LOOPS-SPEC ... - 0 |-> < ITYPE > (N => 0) - 1 |-> < ITYPE > (0 => (N *Int (N +Int 1)) /Int 2) + wrap(0) |-> < ITYPE > (N => 0) + wrap(1) |-> < ITYPE > (0 => (N *Int (N +Int 1)) /Int 2) requires #inUnsignedRange(ITYPE, N) andBool N >Int 0 diff --git a/wasm.md b/wasm.md index 791548201..305bcd08e 100644 --- a/wasm.md +++ b/wasm.md @@ -172,8 +172,8 @@ module WASM .K .ValStack - .Map - .Int + .MapIntToVal + .Int .Map .Map @@ -507,7 +507,7 @@ The various `init_local` variants assist in setting up the `locals` cell. | "#init_locals" Int ValStack // -------------------------------------------- rule init_local INDEX VALUE => . ... - LOCALS => LOCALS [ INDEX <- VALUE ] + LOCALS => LOCALS {{ INDEX <- VALUE }} rule init_locals VALUES => #init_locals 0 VALUES ... @@ -527,18 +527,19 @@ The `*_local` instructions are defined here. | "#local.tee" "(" Int ")" [klabel(aLocal.tee), symbol] // ---------------------------------------------------------------------- rule #local.get(I) => . ... - VALSTACK => VALUE : VALSTACK - ... I |-> VALUE ... + VALSTACK => LOCALS{{I}} orDefault undefined : VALSTACK + LOCALS + requires I in_keys{{LOCALS}} rule #local.set(I) => . ... VALUE : VALSTACK => VALSTACK - LOCALS => LOCALS[I <- VALUE] - requires I in_keys(LOCALS) + LOCALS => LOCALS{{I <- VALUE}} + requires I in_keys{{LOCALS}} rule #local.tee(I) => . ... VALUE : _VALSTACK - LOCALS => LOCALS[I <- VALUE] - requires I in_keys(LOCALS) + LOCALS => LOCALS{{I <- VALUE}} + requires I in_keys{{LOCALS}} ``` ### Globals @@ -735,7 +736,7 @@ Similar to labels, they sit on the instruction stack (the `` cell), and Unlike labels, only one frame can be "broken" through at a time. ```k - syntax Frame ::= "frame" Int ValTypes ValStack Map + syntax Frame ::= "frame" Int ValTypes ValStack MapIntToVal // -------------------------------------------------- rule frame MODIDX' TRANGE VALSTACK' LOCAL' => . ... VALSTACK => #take(lengthValTypes(TRANGE), VALSTACK) ++ VALSTACK' @@ -758,7 +759,7 @@ The `#take` function will return the parameter stack in the reversed order, then ... VALSTACK => .ValStack - LOCAL => .Map + LOCAL => .MapIntToVal MODIDX => MODIDX' FADDR From b1fa1e6c4854f2d4ef653be4f3d97c40da64ee95 Mon Sep 17 00:00:00 2001 From: Virgil Date: Wed, 27 Sep 2023 23:22:30 +0300 Subject: [PATCH 16/16] tmp --- data.md | 56 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ test.md | 4 ++-- wasm.md | 1 + 3 files changed, 59 insertions(+), 2 deletions(-) diff --git a/data.md b/data.md index 706aec381..6f13ee2f3 100644 --- a/data.md +++ b/data.md @@ -152,6 +152,8 @@ module WASM-DATA-COMMON imports STRING imports LIST imports MAP + imports MAP-INT-TO-VAL + imports MAP-INT-TO-VAL-PRIMITIVE imports FLOAT imports BYTES imports K-EQUAL @@ -415,6 +417,60 @@ Some operations extend integers from 1, 2, or 4 bytes, so a special function wit ``` +#### Val getters + +```k + + syntax Int ::= getI32ValOr0(Val) [function, total] + | getI64ValOr0(Val) [function, total] + + rule getI32ValOr0( V:Int) => V + rule getI32ValOr0(_:Val) => 0 [owise] + + rule getI64ValOr0( V:Int) => V + rule getI64ValOr0(_:Val) => 0 [owise] + + syntax Bool ::= isIntWithType(Val, ValType) [function, total] + rule isIntWithType( _:Int, T:ValType) => true + rule isIntWithType(_:Val, _:ValType) => false [owise] + +``` + +#### Int -> Val map operations + +mapInt2ValHasValues checks that the map has entries with the provided types, +numbered consecutively from 0, and only those entries. +This means that the keys are exactly 0, 1, ..., N - 1. + +```k + + syntax Bool ::= mapInt2ValHasValues(MapIntToVal, ValTypes) [function, total] + | #mapInt2ValHasValues(MapIntToVal, Int, ValTypes) [function, total] + rule mapInt2ValHasValues(M:MapIntToVal, VTs:ValTypes) + => size(M) ==Int lengthValTypes(VTs) andBool #mapInt2ValHasValues(M, 0, VTs) + rule #mapInt2ValHasValues(M:MapIntToVal, N:Int, VT VTs) + => N in_keys{{M}} + andBool isIntWithType(M{{N}} orDefault undefined, VT) + andBool #mapInt2ValHasValues(M, N +Int 1, VTs) + requires 0 <=Int N + rule #mapInt2ValHasValues(_:MapIntToVal, _:Int, _:ValTypes) => true [owise] + +``` + +getFromMapOr0 extract the int form the provided key if the value has +ValType. Returns 0 otherwise. + +```k + + syntax Int ::= getI32FromMapOr0(MapIntToVal, Int) [function, total] + | getI64FromMapOr0(MapIntToVal, Int) [function, total] + rule getI32FromMapOr0(M:MapIntToVal, N:Int) + => getI32ValOr0(M{{N}} orDefault undefined) + rule getI64FromMapOr0(M:MapIntToVal, N:Int) + => getI64ValOr0(M{{N}} orDefault undefined) + +``` + #### Boolean Interpretation Function `#bool` converts a `Bool` into an `Int`. diff --git a/test.md b/test.md index 27da163fd..63e821bc4 100644 --- a/test.md +++ b/test.md @@ -322,9 +322,9 @@ The operator `#assertLocal`/`#assertGlobal` operators perform a check for a loca syntax Assertion ::= "#assertLocal" Int Val WasmString | "#assertGlobal" Index Val WasmString // --------------------------------------------------------- - rule #assertLocal INDEX (LOCALS{{INDEX}} orDefault undefined) _ => . ... + rule #assertLocal INDEX VALUE _ => . ... LOCALS - requires INDEX in_keys{{LOCALS}} + requires INDEX in_keys{{LOCALS}} andBool VALUE ==K LOCALS{{INDEX}} orDefault undefined rule #assertGlobal TFIDX VALUE _ => . ... CUR diff --git a/wasm.md b/wasm.md index 305bcd08e..697c3a5a1 100644 --- a/wasm.md +++ b/wasm.md @@ -4,6 +4,7 @@ WebAssembly State and Semantics ```k require "data.md" require "data/map-int-to-int.k" +require "data/map-int-to-val.k" require "numeric.md" module WASM-SYNTAX