proofs/containers/hash_table/new.bend

bend-collections-laws-containers@1.0.0.0 · 14 lines · 0 definitions

1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/array.bend as AR
3import bend-collections-laws-containers@1.0.0.0/spec/containers/hash_table.bend as S
4import bend-collections-laws-containers@1.0.0.0/src/containers/hash_table.bend as H
5import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/state.bend as ST
6
7# new: the empty map is a good shadow with the empty model.
8
9def empty(~V: Data) -> ST.Sh<V>:
10  ST.HS{0, 1n, 2, 0, 1, 0n, 0, 0, AR.trep(U32, 2n, 0), AR.trep(String, 0n, ""), AR.trep(Maybe<&2, V>, 0n, None{}), AR.trep(U32, 0n, 0)}
11
12# THEOREM: new is the shadow of the empty specification map
13def new_ok(~V: Data) -> {H.new(&2, V) == ST.real(~V, empty(~V)) : H.HashMap<&2, V>} & ({ST.good(~V, empty(~V)) == True{} : Bool} & {ST.model(~V, empty(~V)) == Nil{} : List<&2, S.Entry<V>>}):
14  ({==}, ({==}, {==}))