proofs/containers/bitlist/state.bend
bend-collections-laws-containers@1.0.0.0 · 64 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
5import bend-collections-laws-containers@1.0.0.0/src/containers/bitlist.bend as BLI
6import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/state.bend as DAS
7import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/lists.bend as BL
8import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/state.bend as ST
9import bend-collections-laws-containers@1.0.0.0/spec/containers/bitlist.bend as S
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitlist/da.bend as DI
11
12# Shadow, invariant and abstraction of a bitlist.
13# shadow BSh{limit, len, w}: w is a good dynamic-array shadow of the words
14# F ST.flat(DI.ws(w)): every stored bit, word by word, bit 0 first
15# good the word array is good and ST.invf(len, F): len <= |F| and every
16# stored bit at a position >= len is zero (the masked tail)
17# model S.M{limit, DI.lim(w), take(F, len)}: the storage capacity exponent
18# is the word array's depth limit (2^lim words of 32 bits)
19# (source: proofs/containers/bitlist/state.src)
20
21
22type Sh is Data:
23 BSh{limit: Maybe<&2, Nat>, len: Nat, w: DAS.Shadow<U32>}
24
25def fl(w: DAS.Shadow<U32>) -> List<&2, Bool>:
26 ST.flat(DI.ws(w))
27
28def real(sh: Sh) -> BLI.Bitlist:
29 match sh:
30 case BSh{l, n, w}:
31 BLI.BL{l, n, DAS.real(U32, w)}
32
33def good(sh: Sh) -> Bool:
34 match sh:
35 case BSh{l, +n, +w}:
36 Bool.and(DAS.good(U32, w), ST.invf(n, fl(w)))
37
38def model(sh: Sh) -> S.Model:
39 match sh:
40 case BSh{l, +n, +w}:
41 S.M{l, DI.lim(w), SC.take(Bool, fl(w), n)}
42
43
44def g_w(+l: Maybe<&2, Nat>, +n: Nat, +w: DAS.Shadow<U32>, +g: {good(BSh{l, n, w}) == True{} : Bool}) -> {DAS.good(U32, w) == True{} : Bool}:
45 L.and_left(DAS.good(U32, w), ST.invf(n, fl(w)), g)
46
47def g_inv(+l: Maybe<&2, Nat>, +n: Nat, +w: DAS.Shadow<U32>, +g: {good(BSh{l, n, w}) == True{} : Bool}) -> {ST.invf(n, fl(w)) == True{} : Bool}:
48 L.and_right(DAS.good(U32, w), ST.invf(n, fl(w)), g)
49
50def g_mk(+l: Maybe<&2, Nat>, +n: Nat, +w: DAS.Shadow<U32>, +gw: {DAS.good(U32, w) == True{} : Bool}, +gi: {ST.invf(n, fl(w)) == True{} : Bool}) -> {good(BSh{l, n, w}) == True{} : Bool}:
51 L.and_intro(DAS.good(U32, w), ST.invf(n, fl(w)), gw, gi)
52
53# A word array with the same words: the invariant and the model carry over.
54def same_good(+l: Maybe<&2, Nat>, +n: Nat, +w: DAS.Shadow<U32>, +w2: DAS.Shadow<U32>, +gw2: {DAS.good(U32, w2) == True{} : Bool}, +e: {DI.ws(w2) == DI.ws(w) : List<&2, U32>}, +g: {good(BSh{l, n, w}) == True{} : Bool}) -> {good(BSh{l, n, w2}) == True{} : Bool}:
55 g_mk(l, n, w2, gw2, L.subst(List<&2, U32>, z => {ST.invf(n, ST.flat(z)) == True{} : Bool}, DI.ws(w), DI.ws(w2), Equal.sym(List<&2, U32>, DI.ws(w2), DI.ws(w), e), g_inv(l, n, w, g)))
56
57# The model of a shadow with given words and depth limit.
58def model_of(+l: Maybe<&2, Nat>, +n: Nat, +w2: DAS.Shadow<U32>, +xs: List<&2, U32>, +c: Nat, +e: {DI.ws(w2) == xs : List<&2, U32>}, +ec: {DI.lim(w2) == c : Nat}) -> {model(BSh{l, n, w2}) == S.M{l, c, SC.take(Bool, ST.flat(xs), n)} : S.Model}:
59 %Equal.sym(List<&2, U32>, DI.ws(w2), xs, e) : {S.M{l, DI.lim(w2), SC.take(Bool, ST.flat(_), n)} == S.M{l, c, SC.take(Bool, ST.flat(xs), n)} : S.Model}
60 %Equal.sym(Nat, DI.lim(w2), c, ec) : {S.M{l, _, SC.take(Bool, ST.flat(xs), n)} == S.M{l, c, SC.take(Bool, ST.flat(xs), n)} : S.Model}
61 {==}
62
63def good_of(+l: Maybe<&2, Nat>, +n: Nat, +w2: DAS.Shadow<U32>, +xs: List<&2, U32>, +gw2: {DAS.good(U32, w2) == True{} : Bool}, +e: {DI.ws(w2) == xs : List<&2, U32>}, +gi: {ST.invf(n, ST.flat(xs)) == True{} : Bool}) -> {good(BSh{l, n, w2}) == True{} : Bool}:
64 g_mk(l, n, w2, gw2, L.subst(List<&2, U32>, z => {ST.invf(n, ST.flat(z)) == True{} : Bool}, xs, DI.ws(w2), Equal.sym(List<&2, U32>, DI.ws(w2), xs, e), gi))