Skip to content

Commit

Permalink
Update data structures; split the config for #writeToStorage (#129)
Browse files Browse the repository at this point in the history
  • Loading branch information
@virgil-serbanuta
virgil-serbanuta authored Aug 23, 2023
1 parent 304113e commit 9d4f88b
Show file tree
Hide file tree
Showing 7 changed files with 116 additions and 112 deletions.
19 changes: 9 additions & 10 deletions data/list-bytes.k
View file
Original file line number Diff line number Diff line change
@@ -1,11 +1,10 @@
requires "bytes-type.k"
require "bytes-type.k"

module LIST-BYTES
imports private INT-SYNTAX
imports private BASIC-K

imports BYTES-TYPE

syntax Bytes

syntax ListBytes [hook(LIST.List)]
Expand All @@ -26,7 +25,7 @@ module LIST-BYTES
syntax WrappedBytes ::= ListBytes "[" Int "]"
[ function, hook(LIST.get), klabel(ListBytes:get), symbol ]
syntax ListBytes ::= ListBytes "[" index: Int "<-" value: WrappedBytes "]"
[function, hook(LIST.update), klabel(ListBytes:set)]
[function, hook(LIST.update), symbol, klabel(ListBytes:set)]
syntax ListBytes ::= makeListBytes(length: Int, value: WrappedBytes)
[function, hook(LIST.make)]
syntax ListBytes ::= updateList(dest: ListBytes, index: Int, src: ListBytes)
Expand All @@ -36,27 +35,26 @@ module LIST-BYTES
syntax ListBytes ::= range(ListBytes, fromFront: Int, fromBack: Int)
[function, hook(LIST.range), klabel(ListBytes:range), symbol]
syntax Bool ::= WrappedBytes "in" ListBytes
[function, total, hook(LIST.in), klabel(_inListBytes_)]
[function, total, hook(LIST.in), symbol, klabel(_inListBytes_)]
syntax Int ::= size(ListBytes)
[function, total, hook(LIST.size), klabel (sizeListBytes), smtlib(smt_seq_len)]
[function, total, hook(LIST.size), symbol, klabel (sizeListBytes), smtlib(smt_seq_len)]
endmodule

module LIST-BYTES-EXTENSIONS
imports BOOL
imports INT
imports LIST-BYTES
imports BYTES-TYPE

syntax WrappedBytes ::= ListBytes "[" Int "]" "orDefault" WrappedBytes
[ function, total, klabel(ListBytes:getOrDefault), symbol ]

syntax Bytes ::= ListBytes "{{" Int "}}"
[function, klabel(ListBytes:primitiveLookup)]
[function, symbol, klabel(ListBytes:primitiveLookup)]
// -----------------------------------------------------------
rule L:ListBytes {{ I:Int }} => unwrap( L[ I ] )

syntax Bytes ::= ListBytes "{{" Int "}}" "orDefault" Bytes
[ function, total, klabel(ListBytes:primitiveLookupOrDefault) ]
[ function, total, symbol, klabel(ListBytes:primitiveLookupOrDefault) ]
// -----------------------------------------------------------------------------
rule L:ListBytes {{ I:Int }} orDefault Value:Bytes
=> unwrap( L [I] orDefault wrap(Value) )
Expand All @@ -78,7 +76,8 @@ module LIST-BYTES-EXTENSIONS
requires notBool (0 -Int size(L) <=Int I andBool I <Int size(L))
[simplification]

syntax ListBytes ::= ListItemWrap( Bytes ) [function, total, klabel(ListBytesItemWrap)]
syntax ListBytes ::= ListItemWrap( Bytes )
[function, total, symbol, klabel(ListBytesItemWrap)]
rule ListItemWrap( B:Bytes ) => ListItem(wrap(B))

endmodule
109 changes: 55 additions & 54 deletions data/map-bytes-to-bytes.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,11 +6,12 @@ module MAP-BYTES-TO-BYTES
imports private BOOL-SYNTAX
imports private INT-SYNTAX
imports private LIST-BYTES
imports private LIST-BYTES
// imports private LIST
// imports private SET-BYTES
imports private SET
imports BYTES-TYPE
// imports BYTES-TYPE
imports BYTES-TYPE

syntax Bytes
syntax Bytes
Expand Down Expand Up @@ -109,7 +110,7 @@ module MAP-BYTES-TO-BYTES-PRIMITIVE-CONCRETE [concrete]
[function, total, klabel(MapBytesToBytes:primitiveInKeys), symbol]

rule (M:MapBytesToBytes {{ Key:Bytes }})
=> unwrap( M[ wrap(Key) ] )
=> (unwrap( M[wrap(Key)] ))
rule M:MapBytesToBytes {{ Key:Bytes }} orDefault Value:Bytes
=> unwrap( M[wrap(Key)] orDefault wrap(Value) )
rule M:MapBytesToBytes {{ Key:Bytes <- Value:Bytes }}
Expand Down Expand Up @@ -141,27 +142,27 @@ module MAP-BYTES-TO-BYTES-PRIMITIVE-SYMBOLIC [symbolic]
// Definitions
// -----------

rule (Key Bytes2Bytes|-> V:Bytes M:MapBytesToBytes)
rule (wrap(Key) Bytes2Bytes|-> V:WrappedBytes M:MapBytesToBytes)
{{ Key:Bytes }}
=> V
=> unwrap( V )
ensures notBool Key in_keys {{ M }}

rule (Key Bytes2Bytes|-> V:Bytes M:MapBytesToBytes)
rule (wrap(Key) Bytes2Bytes|-> V:WrappedBytes M:MapBytesToBytes)
{{ Key:Bytes }} orDefault _:Bytes
=> V
=> unwrap( V )
ensures notBool Key in_keys {{ M }}
rule M:MapBytesToBytes {{ Key:Bytes }} orDefault V:Bytes
=> V
requires notBool Key in_keys {{ M }}

rule (Key Bytes2Bytes|-> _:Bytes M:MapBytesToBytes)
rule (wrap(Key) Bytes2Bytes|-> _:WrappedBytes M:MapBytesToBytes)
{{ Key:Bytes <- Value:Bytes }}
=> (Key Bytes2Bytes|-> Value) M
=> (wrap(Key) Bytes2Bytes|-> wrap(Value)) M
rule M:MapBytesToBytes {{ Key:Bytes <- Value:Bytes }}
=> (Key Bytes2Bytes|-> Value) M
=> (wrap(Key) Bytes2Bytes|-> wrap(Value)) M
requires notBool Key in_keys {{ M }}

rule (Key Bytes2Bytes|-> _:Bytes M:MapBytesToBytes)
rule (wrap(Key) Bytes2Bytes|-> _:WrappedBytes M:MapBytesToBytes)
{{ Key:Bytes <- undef }}
=> M
ensures notBool Key in_keys {{ M }}
Expand All @@ -170,7 +171,7 @@ module MAP-BYTES-TO-BYTES-PRIMITIVE-SYMBOLIC [symbolic]
requires notBool Key in_keys {{ M }}

rule Key:Bytes in_keys
{{Key Bytes2Bytes|-> _:Bytes M:MapBytesToBytes}}
{{wrap(Key) Bytes2Bytes|-> _:WrappedBytes M:MapBytesToBytes}}
=> true
ensures notBool Key in_keys {{ M }}
rule _Key:Bytes in_keys {{ .MapBytesToBytes }}
Expand All @@ -180,62 +181,62 @@ module MAP-BYTES-TO-BYTES-PRIMITIVE-SYMBOLIC [symbolic]
// O(n^2) or something like that, where n is the number of explicit keys
// in the map.
rule Key:Bytes in_keys
{{Key2:Bytes Bytes2Bytes|-> _:Bytes M:MapBytesToBytes}}
{{Key2:WrappedBytes Bytes2Bytes|-> _:WrappedBytes M:MapBytesToBytes}}
=> Key in_keys {{ M }}
requires Key =/=K Key2
requires Key =/=K unwrap( Key2 )
ensures notBool Key2 in_keys (M)
[simplification]

// Translation rules
rule M:MapBytesToBytes[ wrap(Key) ]
=> M{{Key}}
rule M:MapBytesToBytes[Key:WrappedBytes]
=> wrap(M{{unwrap( Key )}})
[simplification, symbolic(M)]
rule M:MapBytesToBytes[ wrap(Key) ]
=> M{{Key}}
rule M:MapBytesToBytes[Key:WrappedBytes]
=> wrap(M{{unwrap( Key )}})
[simplification, symbolic(Key)]
rule M:MapBytesToBytes{{Key}}
=> M[wrap(Key)]
=> unwrap( M[wrap(Key)] )
[simplification, concrete]

rule M:MapBytesToBytes [ wrap(Key) ] orDefault wrap(Value)
=> M {{ Key }} orDefault Value
rule M:MapBytesToBytes [ Key:WrappedBytes ] orDefault Value:WrappedBytes
=> wrap(M {{ unwrap( Key ) }} orDefault unwrap( Value ))
[simplification, symbolic(M)]
rule M:MapBytesToBytes [ wrap(Key) ] orDefault wrap(Value)
=> M {{ Key }} orDefault Value
rule M:MapBytesToBytes [ Key:WrappedBytes ] orDefault Value:WrappedBytes
=> wrap(M {{ unwrap( Key ) }} orDefault unwrap( Value ))
[simplification, symbolic(Key)]
rule M:MapBytesToBytes [ wrap(Key) ] orDefault wrap(Value)
=> M {{ Key }} orDefault Value
rule M:MapBytesToBytes [ Key:WrappedBytes ] orDefault Value:WrappedBytes
=> wrap(M {{ unwrap( Key ) }} orDefault unwrap( Value ))
[simplification, symbolic(Value)]
rule M:MapBytesToBytes{{Key}} orDefault Value
=> M[wrap(Key)] orDefault Value
=> unwrap( M[wrap(Key)] orDefault wrap(Value) )
[simplification, concrete]

rule M:MapBytesToBytes[wrap(Key) <- wrap(Value)]
=> M {{ Key <- Value }}
rule M:MapBytesToBytes[Key:WrappedBytes <- Value:WrappedBytes]
=> M {{ unwrap( Key ) <- unwrap( Value ) }}
[simplification, symbolic(M)]
rule M:MapBytesToBytes[wrap(Key) <- wrap(Value)]
=> M {{ Key <- Value }}
rule M:MapBytesToBytes[Key:WrappedBytes <- Value:WrappedBytes]
=> M {{ unwrap( Key ) <- unwrap( Value ) }}
[simplification, symbolic(Key)]
rule M:MapBytesToBytes[wrap(Key) <- wrap(Value)]
=> M {{ Key <- Value }}
rule M:MapBytesToBytes[Key:WrappedBytes <- Value:WrappedBytes]
=> M {{ unwrap( Key ) <- unwrap( Value ) }}
[simplification, symbolic(Value)]
rule M:MapBytesToBytes{{Key <- Value}} => M[wrap(Key) <- wrap(Value) ]
[simplification, concrete]

rule M:MapBytesToBytes[wrap(Key) <- undef]
=> M {{ Key <- undef }}
rule M:MapBytesToBytes[Key:WrappedBytes <- undef]
=> M {{ unwrap( Key ) <- undef }}
[simplification, symbolic(M)]
rule M:MapBytesToBytes[wrap(Key) <- undef]
=> M {{ Key <- undef }}
rule M:MapBytesToBytes[Key:WrappedBytes <- undef]
=> M {{ unwrap( Key ) <- undef }}
[simplification, symbolic(Key)]
rule M:MapBytesToBytes{{Key <- undef}} => M[wrap(Key) <- undef]
[simplification, concrete]

rule wrap(Key) in_keys (M:MapBytesToBytes)
=> Key in_keys {{M}}
rule Key:WrappedBytes in_keys (M:MapBytesToBytes)
=> unwrap( Key ) in_keys {{M}}
[simplification, symbolic(M)]
rule wrap(Key) in_keys (M:MapBytesToBytes)
=> Key in_keys {{M}}
rule Key:WrappedBytes in_keys (M:MapBytesToBytes)
=> unwrap( Key ) in_keys {{M}}
[simplification, symbolic(Key)]
rule Key in_keys {{M:MapBytesToBytes}} => wrap(Key) in_keys(M)
[simplification, concrete]
Expand All @@ -253,16 +254,16 @@ module MAP-BYTES-TO-BYTES-PRIMITIVE-SYMBOLIC [symbolic]
rule M:MapBytesToBytes {{ K <- _ }} {{ K <- V }} => M {{ K <- V }} [simplification]
rule (K1 Bytes2Bytes|-> V1 M:MapBytesToBytes) {{ K2 <- V2 }}
=> (K1 Bytes2Bytes|-> V1 (M {{ K2 <- V2 }}))
requires K1 =/=K K2
requires unwrap( K1 ) =/=K K2
[simplification]

rule (K1 Bytes2Bytes|-> V1 M:MapBytesToBytes) {{ K2 <- undef }}
=> (K1 Bytes2Bytes|-> V1 (M {{ K2 <- undef }}))
requires K1 =/=K K2
requires unwrap( K1 ) =/=K K2
[simplification]

rule (K1 Bytes2Bytes|-> _V M:MapBytesToBytes) {{ K2 }} => M {{K2}}
requires K1 =/=K K2
requires unwrap( K1 ) =/=K K2
ensures notBool (K1 in_keys(M))
[simplification]
rule (_MAP:MapBytesToBytes {{ K <- V1 }}) {{ K }} => V1 [simplification]
Expand All @@ -272,7 +273,7 @@ module MAP-BYTES-TO-BYTES-PRIMITIVE-SYMBOLIC [symbolic]

rule (K1 Bytes2Bytes|-> _V M:MapBytesToBytes) {{ K2 }} orDefault D
=> M {{K2}} orDefault D
requires K1 =/=K K2
requires unwrap( K1 ) =/=K K2
ensures notBool (K1 in_keys(M))
[simplification]
rule (_MAP:MapBytesToBytes {{ K <- V1 }}) {{ K }} orDefault _ => V1 [simplification]
Expand All @@ -292,19 +293,19 @@ module MAP-BYTES-TO-BYTES-PRIMITIVE-SYMBOLIC [symbolic]
[simplification]

rule K1 in_keys {{ (K2 Bytes2Bytes|-> V) M:MapBytesToBytes }}
=> K1 ==K K2 orBool K1 in_keys {{ M }}
=> K1 ==K unwrap( K2 ) orBool K1 in_keys {{ M }}
requires definedMapElementConcat(K2, V, M)
[simplification(100)]


rule {false #Equals @Key in_keys{{ Key' Bytes2Bytes|-> Val @M:MapBytesToBytes }}}
=> #Ceil(@Key) #And #Ceil(Key' Bytes2Bytes|-> Val @M)
#And #Not({ @Key #Equals Key' })
#And #Not({ @Key #Equals unwrap( Key' ) })
#And {false #Equals @Key in_keys{{@M}}}
[simplification]
rule {@Key in_keys{{Key' Bytes2Bytes|-> Val @M:MapBytesToBytes}} #Equals false}
=> #Ceil(@Key) #And #Ceil(Key' Bytes2Bytes|-> Val @M)
#And #Not({@Key #Equals Key' })
#And #Not({@Key #Equals unwrap( Key' ) })
#And {@Key in_keys{{@M}} #Equals false}
[simplification]

Expand All @@ -315,8 +316,8 @@ module MAP-BYTES-TO-BYTES-KORE-SYMBOLIC
imports private K-EQUAL
imports private BOOL

syntax Bool ::= definedMapElementConcat(Bytes, Bytes, MapBytesToBytes) [function, total]
rule definedMapElementConcat(K, _V, M:MapBytesToBytes) => notBool wrap(K) in_keys(M)
syntax Bool ::= definedMapElementConcat(WrappedBytes, WrappedBytes, MapBytesToBytes) [function, total]
rule definedMapElementConcat(K, _V, M:MapBytesToBytes) => notBool K in_keys(M)

rule #Ceil(@M:MapBytesToBytes [@K:WrappedBytes])
=> {(@K in_keys(@M)) #Equals true}
Expand Down Expand Up @@ -379,18 +380,18 @@ module MAP-BYTES-TO-BYTES-KORE-SYMBOLIC
requires K1 =/=K K2
[simplification]

rule wrap(K) in_keys((wrap(K) Bytes2Bytes|-> wrap(V)) M:MapBytesToBytes)
rule K in_keys((K Bytes2Bytes|-> V) M:MapBytesToBytes)
=> true
requires definedMapElementConcat(K, V, M)
[simplification(50)]
rule wrap(K1) in_keys((wrap(K2) Bytes2Bytes|-> wrap(V)) M:MapBytesToBytes)
=> wrap(K1) in_keys(M)
rule K1 in_keys((K2 Bytes2Bytes|-> V) M:MapBytesToBytes)
=> K1 in_keys(M)
requires true
andBool definedMapElementConcat(K2, V, M)
andBool K1 =/=K K2
[simplification(50)]
rule wrap(K1) in_keys((wrap(K2) Bytes2Bytes|-> wrap(V)) M:MapBytesToBytes)
=> wrap(K1) ==K wrap(K2) orBool wrap(K1) in_keys(M)
rule K1 in_keys((K2 Bytes2Bytes|-> V) M:MapBytesToBytes)
=> K1 ==K K2 orBool K1 in_keys(M)
requires definedMapElementConcat(K2, V, M)
[simplification(100)]

Expand All @@ -414,7 +415,7 @@ module MAP-BYTES-TO-BYTES-CURLY-BRACE
imports private K-EQUAL-SYNTAX
imports MAP-BYTES-TO-BYTES

syntax MapBytesToBytes ::= MapBytesToBytes "{" key:Bytes "<-" value:Bytes "}"
syntax MapBytesToBytes ::= MapBytesToBytes "{" key:WrappedBytes "<-" value:WrappedBytes "}"
[function, total, symbol, klabel(MapBytesToBytes:curly_update)]
rule M:MapBytesToBytes{Key <- Value} => M (Key Bytes2Bytes|-> Value)
requires notBool Key in_keys(M)
Expand Down
Loading

0 comments on commit 9d4f88b

Please sign in to comment.