Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Update data structs; split for #writeToStorage #129

Merged
merged 1 commit into from
Aug 23, 2023
Merged

Update data structs; split for #writeToStorage #129

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
19 changes: 9 additions & 10 deletions data/list-bytes.k
View file
Open in desktop
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
Open in desktop
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