proofs/containers/bitset/state.bend
bend-collections-laws-containers@1.0.0.0 · 372 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/proofs/lib/list.bend as LL
5import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
6import bend-collections-laws-containers@1.0.0.0/spec/containers/bitset.bend as S
7import bend-collections-laws-containers@1.0.0.0/src/containers/bitset.bend as B
8import bend-collections-laws-containers@1.0.0.0/proofs/lib/array.bend as A
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/model.bend as MD
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/arr.bend as AR
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/depth.bend as DP
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/lists.bend as BL
13import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/word.bend as W
14
15# Abstraction and invariant of the packed representation.
16# flat(ws) all stored bits, word by word, bit 0 first
17# abs the first `len` stored bits
18# inv len <= |flat| < len + 32 (exactly ceil(len/32) words) and
19# every stored bit at position >= len is zero (masked tail)
20
21def flat(ws: List<&2, U32>) -> List<&2, Bool>:
22 match ws:
23 case Nil{}:
24 Nil{}
25 case Con{w, t}:
26 SC.append(Bool, W.ubits(w), flat(t))
27
28def invf(+n: Nat, +xs: List<&2, Bool>) -> Bool:
29 Bool.and(Nat.is_le(n, SC.length(Bool, xs)), BL.allf(SC.drop(Bool, xs, n)))
30
31def inv_le(+n: Nat, +xs: List<&2, Bool>, +g: {invf(n, xs) == True{} : Bool}) -> {Nat.is_le(n, SC.length(Bool, xs)) == True{} : Bool}:
32 L.and_left(Nat.is_le(n, SC.length(Bool, xs)), BL.allf(SC.drop(Bool, xs, n)), g)
33
34def inv_tail(+n: Nat, +xs: List<&2, Bool>, +g: {invf(n, xs) == True{} : Bool}) -> {BL.allf(SC.drop(Bool, xs, n)) == True{} : Bool}:
35 L.and_right(Nat.is_le(n, SC.length(Bool, xs)), BL.allf(SC.drop(Bool, xs, n)), g)
36
37def inv_mk(+n: Nat, +xs: List<&2, Bool>, +a: {Nat.is_le(n, SC.length(Bool, xs)) == True{} : Bool}, +c: {BL.allf(SC.drop(Bool, xs, n)) == True{} : Bool}) -> {invf(n, xs) == True{} : Bool}:
38 L.and_intro(Nat.is_le(n, SC.length(Bool, xs)), BL.allf(SC.drop(Bool, xs, n)), a, c)
39
40# The logical length is len.
41def length_abs(+n: Nat, +xs: List<&2, Bool>, +g: {invf(n, xs) == True{} : Bool}) -> {SC.length(Bool, SC.take(Bool, xs, n)) == n : Nat}:
42 BL.length_take(xs, n, inv_le(n, xs, g))
43
44# The stored bits are the logical bits followed by the zero tail.
45def split(+n: Nat, +xs: List<&2, Bool>) -> {xs == SC.append(Bool, SC.take(Bool, xs, n), SC.drop(Bool, xs, n)) : List<&2, Bool>}:
46 Equal.sym(List<&2, Bool>, SC.append(Bool, SC.take(Bool, xs, n), SC.drop(Bool, xs, n)), xs, BL.take_drop(xs, n))
47
48def take32(+w: U32) -> {SC.take(Bool, W.ubits(w), 32n) == W.ubits(w) : List<&2, Bool>}:
49 L.subst(Nat, k => {SC.take(Bool, W.ubits(w), k) == W.ubits(w) : List<&2, Bool>}, SC.length(Bool, W.ubits(w)), 32n, W.ulen(w), BL.take_all(W.ubits(w)))
50
51def length_flat_cons(+w: U32, +t: List<&2, U32>) -> {SC.length(Bool, flat(Con{w, t})) == Nat.add(32n, SC.length(Bool, flat(t))) : Nat}:
52 %Equal.sym(Nat, SC.length(Bool, SC.append(Bool, W.ubits(w), flat(t))), Nat.add(SC.length(Bool, W.ubits(w)), SC.length(Bool, flat(t))), LL.length_append(Bool, W.ubits(w), flat(t))) : {_ == Nat.add(32n, SC.length(Bool, flat(t))) : Nat}
53 %Equal.sym(Nat, SC.length(Bool, W.ubits(w)), 32n, W.ulen(w)) : {Nat.add(_, SC.length(Bool, flat(t))) == Nat.add(32n, SC.length(Bool, flat(t))) : Nat}
54 {==}
55
56# ---- word-list walks ----
57
58def get_case(+w: U32, +t: List<&2, U32>, +i: Nat, b: Bool, +eb: {Nat.is_lt(i, 32n) == b : Bool}, +h: {Nat.is_lt(i, Nat.add(32n, SC.length(Bool, flat(t)))) == True{} : Bool}, ih: @+h2: {Nat.is_lt(Nat.sub(i, 32n), SC.length(Bool, flat(t))) == True{} : Bool} -> {Some{MD.get_walk(t, Nat.sub(i, 32n))} == SC.nth(Bool, flat(t), Nat.sub(i, 32n)) : Maybe<&2, Bool>}) -> {Some{MD.get_pick(b, w, i, MD.get_walk(t, Nat.sub(i, 32n)))} == SC.nth(Bool, SC.append(Bool, W.ubits(w), flat(t)), i) : Maybe<&2, Bool>}:
59 match b:
60 case True{}:
61 +hl = L.subst(Nat, k => {Nat.is_lt(i, k) == True{} : Bool}, 32n, SC.length(Bool, W.ubits(w)), Equal.sym(Nat, SC.length(Bool, W.ubits(w)), 32n, W.ulen(w)), eb)
62 Equal.trans(Maybe<&2, Bool>, Some{B.word_get(w, i)}, SC.nth(Bool, W.ubits(w), i), SC.nth(Bool, SC.append(Bool, W.ubits(w), flat(t)), i),
63 W.word_get(w, i, eb),
64 Equal.sym(Maybe<&2, Bool>, SC.nth(Bool, SC.append(Bool, W.ubits(w), flat(t)), i), SC.nth(Bool, W.ubits(w), i), LL.nth_append_left(Bool, W.ubits(w), flat(t), i, hl)))
65 case False{}:
66 +le = N.not_lt_le(i, 32n, eb)
67 +hr = L.subst(Nat, k => {Nat.is_le(k, i) == True{} : Bool}, 32n, SC.length(Bool, W.ubits(w)), Equal.sym(Nat, SC.length(Bool, W.ubits(w)), 32n, W.ulen(w)), le)
68 %Equal.sym(Maybe<&2, Bool>, SC.nth(Bool, SC.append(Bool, W.ubits(w), flat(t)), i), SC.nth(Bool, flat(t), Nat.sub(i, SC.length(Bool, W.ubits(w)))), LL.nth_append_right(Bool, W.ubits(w), flat(t), i, hr)) : {Some{MD.get_walk(t, Nat.sub(i, 32n))} == _ : Maybe<&2, Bool>}
69 %Equal.sym(Nat, SC.length(Bool, W.ubits(w)), 32n, W.ulen(w)) : {Some{MD.get_walk(t, Nat.sub(i, 32n))} == SC.nth(Bool, flat(t), Nat.sub(i, _)) : Maybe<&2, Bool>}
70 ih(N.sub_lt(i, 32n, SC.length(Bool, flat(t)), le, h))
71
72def get_walk(+ws: List<&2, U32>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Bool, flat(ws))) == True{} : Bool}) -> {Some{MD.get_walk(ws, i)} == SC.nth(Bool, flat(ws), i) : Maybe<&2, Bool>}:
73 match ws:
74 case Nil{}:
75 Empty.absurd({Some{MD.get_walk(Nil{}, i)} == SC.nth(Bool, flat(Nil{}), i) : Maybe<&2, Bool>}, N.lt_zero_absurd(i, h))
76 case Con{w, t}:
77 get_case(w, t, i, Nat.is_lt(i, 32n), {==}, L.subst(Nat, k => {Nat.is_lt(i, k) == True{} : Bool}, SC.length(Bool, flat(Con{w, t})), Nat.add(32n, SC.length(Bool, flat(t))), length_flat_cons(w, t), h), h2 => get_walk(t, Nat.sub(i, 32n), h2))
78
79def put_case(+v: Bool, +w: U32, +i: Nat, +t: List<&2, U32>, b: Bool, +eb: {Nat.is_lt(i, 32n) == b : Bool}, +ih: {flat(MD.put_walk(t, Nat.sub(i, 32n), v)) == SC.update(Bool, flat(t), Nat.sub(i, 32n), v) : List<&2, Bool>}) -> {flat(MD.put_pick(b, v, w, i, t, MD.put_walk(t, Nat.sub(i, 32n), v))) == SC.update(Bool, SC.append(Bool, W.ubits(w), flat(t)), i, v) : List<&2, Bool>}:
80 match b:
81 case True{}:
82 +hl = L.subst(Nat, k => {Nat.is_lt(i, k) == True{} : Bool}, 32n, SC.length(Bool, W.ubits(w)), Equal.sym(Nat, SC.length(Bool, W.ubits(w)), 32n, W.ulen(w)), eb)
83 %Equal.sym(List<&2, Bool>, SC.update(Bool, SC.append(Bool, W.ubits(w), flat(t)), i, v), SC.append(Bool, SC.update(Bool, W.ubits(w), i, v), flat(t)), LL.update_append_left(Bool, W.ubits(w), flat(t), i, v, hl)) : {SC.append(Bool, W.ubits(B.word_put(v, w, i)), flat(t)) == _ : List<&2, Bool>}
84 %Equal.sym(List<&2, Bool>, W.ubits(B.word_put(v, w, i)), SC.update(Bool, W.ubits(w), i, v), W.word_put(v, w, i, eb)) : {SC.append(Bool, _, flat(t)) == SC.append(Bool, SC.update(Bool, W.ubits(w), i, v), flat(t)) : List<&2, Bool>}
85 {==}
86 case False{}:
87 +le = N.not_lt_le(i, 32n, eb)
88 +hr = L.subst(Nat, k => {Nat.is_le(k, i) == True{} : Bool}, 32n, SC.length(Bool, W.ubits(w)), Equal.sym(Nat, SC.length(Bool, W.ubits(w)), 32n, W.ulen(w)), le)
89 %Equal.sym(List<&2, Bool>, SC.update(Bool, SC.append(Bool, W.ubits(w), flat(t)), i, v), SC.append(Bool, W.ubits(w), SC.update(Bool, flat(t), Nat.sub(i, SC.length(Bool, W.ubits(w))), v)), LL.update_append_right(Bool, W.ubits(w), flat(t), i, v, hr)) : {SC.append(Bool, W.ubits(w), flat(MD.put_walk(t, Nat.sub(i, 32n), v))) == _ : List<&2, Bool>}
90 %Equal.sym(Nat, SC.length(Bool, W.ubits(w)), 32n, W.ulen(w)) : {SC.append(Bool, W.ubits(w), flat(MD.put_walk(t, Nat.sub(i, 32n), v))) == SC.append(Bool, W.ubits(w), SC.update(Bool, flat(t), Nat.sub(i, _), v)) : List<&2, Bool>}
91 %Equal.sym(List<&2, Bool>, flat(MD.put_walk(t, Nat.sub(i, 32n), v)), SC.update(Bool, flat(t), Nat.sub(i, 32n), v), ih) : {SC.append(Bool, W.ubits(w), _) == SC.append(Bool, W.ubits(w), SC.update(Bool, flat(t), Nat.sub(i, 32n), v)) : List<&2, Bool>}
92 {==}
93
94def put_walk(+ws: List<&2, U32>, +i: Nat, +v: Bool) -> {flat(MD.put_walk(ws, i, v)) == SC.update(Bool, flat(ws), i, v) : List<&2, Bool>}:
95 match ws:
96 case Nil{}:
97 {==}
98 case Con{w, t}:
99 put_case(v, w, i, t, Nat.is_lt(i, 32n), {==}, put_walk(t, Nat.sub(i, 32n), v))
100
101def zip_words(+k: B.WordOp, +ws: List<&2, U32>, +vs: List<&2, U32>) -> {flat(MD.zip_words(k, ws, vs)) == BL.zipk(k, flat(ws), flat(vs)) : List<&2, Bool>}:
102 match ws vs:
103 case Nil{} _:
104 {==}
105 case Con{a, s} Nil{}:
106 Equal.sym(List<&2, Bool>, BL.zipk(k, SC.append(Bool, W.ubits(a), flat(s)), Nil{}), Nil{}, BL.zipk_nil_r(k, SC.append(Bool, W.ubits(a), flat(s))))
107 case Con{a, s} Con{b, t}:
108 %Equal.sym(List<&2, Bool>, W.ubits(B.word_op(k, a, b)), BL.zipk(k, W.ubits(a), W.ubits(b)), W.u_op(k, a, b)) : {SC.append(Bool, _, flat(MD.zip_words(k, s, t))) == BL.zipk(k, SC.append(Bool, W.ubits(a), flat(s)), SC.append(Bool, W.ubits(b), flat(t))) : List<&2, Bool>}
109 %Equal.sym(List<&2, Bool>, flat(MD.zip_words(k, s, t)), BL.zipk(k, flat(s), flat(t)), zip_words(k, s, t)) : {SC.append(Bool, BL.zipk(k, W.ubits(a), W.ubits(b)), _) == BL.zipk(k, SC.append(Bool, W.ubits(a), flat(s)), SC.append(Bool, W.ubits(b), flat(t))) : List<&2, Bool>}
110 Equal.sym(List<&2, Bool>, BL.zipk(k, SC.append(Bool, W.ubits(a), flat(s)), SC.append(Bool, W.ubits(b), flat(t))), SC.append(Bool, BL.zipk(k, W.ubits(a), W.ubits(b)), BL.zipk(k, flat(s), flat(t))),
111 BL.zipk_append(k, W.ubits(a), W.ubits(b), flat(s), flat(t), Equal.trans(Nat, SC.length(Bool, W.ubits(a)), 32n, SC.length(Bool, W.ubits(b)), W.ulen(a), Equal.sym(Nat, SC.length(Bool, W.ubits(b)), 32n, W.ulen(b)))))
112
113def count_words(+ws: List<&2, U32>) -> {MD.count_words(ws) == S.count(flat(ws)) : Nat}:
114 match ws:
115 case Nil{}:
116 {==}
117 case Con{w, t}:
118 %Equal.sym(Nat, B.word_count(32n, w), S.count(SC.take(Bool, W.ubits(w), 32n)), W.word_count(32n, w)) : {Nat.add(_, MD.count_words(t)) == S.count(SC.append(Bool, W.ubits(w), flat(t))) : Nat}
119 %Equal.sym(List<&2, Bool>, SC.take(Bool, W.ubits(w), 32n), W.ubits(w), take32(w)) : {Nat.add(S.count(_), MD.count_words(t)) == S.count(SC.append(Bool, W.ubits(w), flat(t))) : Nat}
120 %Equal.sym(Nat, MD.count_words(t), S.count(flat(t)), count_words(t)) : {Nat.add(S.count(W.ubits(w)), _) == S.count(SC.append(Bool, W.ubits(w), flat(t))) : Nat}
121 Equal.sym(Nat, S.count(SC.append(Bool, W.ubits(w), flat(t))), Nat.add(S.count(W.ubits(w)), S.count(flat(t))), BL.count_append(W.ubits(w), flat(t)))
122
123def members_words(+ws: List<&2, U32>, +off: Nat) -> {MD.members_words(ws, off) == S.members(flat(ws), off) : List<&2, Nat>}:
124 match ws:
125 case Nil{}:
126 {==}
127 case Con{w, t}:
128 %Equal.sym(List<&2, Nat>, B.word_members(32n, w, off, MD.members_words(t, Nat.add(32n, off))), SC.append(Nat, S.members(SC.take(Bool, W.ubits(w), 32n), off), MD.members_words(t, Nat.add(32n, off))), W.word_members(32n, w, off, MD.members_words(t, Nat.add(32n, off)))) : {_ == S.members(SC.append(Bool, W.ubits(w), flat(t)), off) : List<&2, Nat>}
129 %Equal.sym(List<&2, Bool>, SC.take(Bool, W.ubits(w), 32n), W.ubits(w), take32(w)) : {SC.append(Nat, S.members(_, off), MD.members_words(t, Nat.add(32n, off))) == S.members(SC.append(Bool, W.ubits(w), flat(t)), off) : List<&2, Nat>}
130 %Equal.sym(List<&2, Nat>, MD.members_words(t, Nat.add(32n, off)), S.members(flat(t), Nat.add(32n, off)), members_words(t, Nat.add(32n, off))) : {SC.append(Nat, S.members(W.ubits(w), off), _) == S.members(SC.append(Bool, W.ubits(w), flat(t)), off) : List<&2, Nat>}
131 %Equal.sym(List<&2, Nat>, S.members(SC.append(Bool, W.ubits(w), flat(t)), off), SC.append(Nat, S.members(W.ubits(w), off), S.members(flat(t), Nat.add(SC.length(Bool, W.ubits(w)), off))), BL.members_append(W.ubits(w), flat(t), off)) : {SC.append(Nat, S.members(W.ubits(w), off), S.members(flat(t), Nat.add(32n, off))) == _ : List<&2, Nat>}
132 %Equal.sym(Nat, SC.length(Bool, W.ubits(w)), 32n, W.ulen(w)) : {SC.append(Nat, S.members(W.ubits(w), off), S.members(flat(t), Nat.add(32n, off))) == SC.append(Nat, S.members(W.ubits(w), off), S.members(flat(t), Nat.add(_, off))) : List<&2, Nat>}
133 {==}
134
135# ---- invariant preservation facts ----
136
137def invf_update(+n: Nat, +xs: List<&2, Bool>, +i: Nat, +v: Bool, +h: {Nat.is_lt(i, n) == True{} : Bool}, +g: {invf(n, xs) == True{} : Bool}) -> {invf(n, SC.update(Bool, xs, i, v)) == True{} : Bool}:
138 +el = Equal.sym(Nat, SC.length(Bool, SC.update(Bool, xs, i, v)), SC.length(Bool, xs), LL.length_update(Bool, xs, i, v))
139 inv_mk(n, SC.update(Bool, xs, i, v),
140 L.subst(Nat, k => {Nat.is_le(n, k) == True{} : Bool}, SC.length(Bool, xs), SC.length(Bool, SC.update(Bool, xs, i, v)), el, inv_le(n, xs, g)),
141 L.subst(List<&2, Bool>, d => {BL.allf(d) == True{} : Bool}, SC.drop(Bool, xs, n), SC.drop(Bool, SC.update(Bool, xs, i, v), n), Equal.sym(List<&2, Bool>, SC.drop(Bool, SC.update(Bool, xs, i, v), n), SC.drop(Bool, xs, n), BL.drop_update(xs, i, v, n, h)), inv_tail(n, xs, g)))
142
143def invf_zipk(+k: B.WordOp, +n: Nat, +xs: List<&2, Bool>, +ys: List<&2, Bool>, +gx: {invf(n, xs) == True{} : Bool}, +gy: {invf(n, ys) == True{} : Bool}) -> {invf(n, BL.zipk(k, xs, ys)) == True{} : Bool}:
144 inv_mk(n, BL.zipk(k, xs, ys),
145 BL.le_length_zipk(k, n, xs, ys, inv_le(n, xs, gx), inv_le(n, ys, gy)),
146 %Equal.sym(List<&2, Bool>, SC.drop(Bool, BL.zipk(k, xs, ys), n), BL.zipk(k, SC.drop(Bool, xs, n), SC.drop(Bool, ys, n)), BL.drop_zipk(k, xs, ys, n)) : {BL.allf(_) == True{} : Bool}
147 BL.allf_zipk(k, SC.drop(Bool, xs, n), SC.drop(Bool, ys, n), inv_tail(n, xs, gx), inv_tail(n, ys, gy)))
148
149# put_walk as seen through the abstraction.
150def put_abs(+n: Nat, +ws: List<&2, U32>, +i: Nat, +v: Bool) -> {SC.take(Bool, flat(MD.put_walk(ws, i, v)), n) == SC.update(Bool, SC.take(Bool, flat(ws), n), i, v) : List<&2, Bool>}:
151 %Equal.sym(List<&2, Bool>, flat(MD.put_walk(ws, i, v)), SC.update(Bool, flat(ws), i, v), put_walk(ws, i, v)) : {SC.take(Bool, _, n) == SC.update(Bool, SC.take(Bool, flat(ws), n), i, v) : List<&2, Bool>}
152 BL.take_update(flat(ws), i, v, n)
153
154def put_inv(+n: Nat, +ws: List<&2, U32>, +i: Nat, +v: Bool, +h: {Nat.is_lt(i, n) == True{} : Bool}, +g: {invf(n, flat(ws)) == True{} : Bool}) -> {invf(n, flat(MD.put_walk(ws, i, v))) == True{} : Bool}:
155 L.subst(List<&2, Bool>, x => {invf(n, x) == True{} : Bool}, SC.update(Bool, flat(ws), i, v), flat(MD.put_walk(ws, i, v)), Equal.sym(List<&2, Bool>, flat(MD.put_walk(ws, i, v)), SC.update(Bool, flat(ws), i, v), put_walk(ws, i, v)), invf_update(n, flat(ws), i, v, h, g))
156
157# ---- the representation: a word array of depth d holding n logical bits ----
158#
159# Base.Array is linear, so (exactly as in proofs/dynamic_array) the statements
160# are about `A.thaw(t)`, the array built from the Data mirror tree t.
161
162def rep(+n: Nat, +d: Nat, +t: A.Tree<B.Wd>) -> Bool:
163 Bool.and(Nat.is_eq(d, B.depth_for(n)), Bool.and(A.perfect(B.Wd, d, t), invf(n, flat(AR.ws(t)))))
164
165def abs(+n: Nat, +t: A.Tree<B.Wd>) -> List<&2, Bool>:
166 SC.take(Bool, flat(AR.ws(t)), n)
167
168def rep_depth(+n: Nat, +d: Nat, +t: A.Tree<B.Wd>, +g: {rep(n, d, t) == True{} : Bool}) -> {Nat.is_eq(d, B.depth_for(n)) == True{} : Bool}:
169 L.and_left(Nat.is_eq(d, B.depth_for(n)), Bool.and(A.perfect(B.Wd, d, t), invf(n, flat(AR.ws(t)))), g)
170
171def rep_perfect(+n: Nat, +d: Nat, +t: A.Tree<B.Wd>, +g: {rep(n, d, t) == True{} : Bool}) -> {A.perfect(B.Wd, d, t) == True{} : Bool}:
172 L.and_left(A.perfect(B.Wd, d, t), invf(n, flat(AR.ws(t))),
173 L.and_right(Nat.is_eq(d, B.depth_for(n)), Bool.and(A.perfect(B.Wd, d, t), invf(n, flat(AR.ws(t)))), g))
174
175def rep_invf(+n: Nat, +d: Nat, +t: A.Tree<B.Wd>, +g: {rep(n, d, t) == True{} : Bool}) -> {invf(n, flat(AR.ws(t))) == True{} : Bool}:
176 L.and_right(A.perfect(B.Wd, d, t), invf(n, flat(AR.ws(t))),
177 L.and_right(Nat.is_eq(d, B.depth_for(n)), Bool.and(A.perfect(B.Wd, d, t), invf(n, flat(AR.ws(t)))), g))
178
179def rep_mk(+n: Nat, +d: Nat, +t: A.Tree<B.Wd>, +a: {Nat.is_eq(d, B.depth_for(n)) == True{} : Bool}, +b: {A.perfect(B.Wd, d, t) == True{} : Bool}, +c: {invf(n, flat(AR.ws(t))) == True{} : Bool}) -> {rep(n, d, t) == True{} : Bool}:
180 L.and_intro(Nat.is_eq(d, B.depth_for(n)), Bool.and(A.perfect(B.Wd, d, t), invf(n, flat(AR.ws(t)))), a,
181 L.and_intro(A.perfect(B.Wd, d, t), invf(n, flat(AR.ws(t))), b, c))
182
183def rep_lt(+n: Nat, +d: Nat, +t: A.Tree<B.Wd>, +g: {rep(n, d, t) == True{} : Bool}) -> {Nat.is_lt(d, 32n) == True{} : Bool}:
184 L.subst(Nat, z => {Nat.is_lt(z, 32n) == True{} : Bool}, B.depth_for(n), d,
185 Equal.sym(Nat, d, B.depth_for(n), N.eq_from_is_eq(d, B.depth_for(n), rep_depth(n, d, t, g))),
186 DP.depth_lt(n))
187
188# ---- the all-zero array ----
189
190def length_flat(ws: List<&2, U32>) -> {SC.length(Bool, flat(ws)) == Nat.mul(SC.length(U32, ws), 32n) : Nat}:
191 match ws:
192 case Nil{}:
193 {==}
194 case Con{+w, +t}:
195 %Equal.sym(Nat, SC.length(Bool, flat(Con{w, t})), Nat.add(32n, SC.length(Bool, flat(t))), length_flat_cons(w, t)) : {_ == Nat.mul(SC.length(U32, Con{w, t}), 32n) : Nat}
196 Equal.cong(Nat, Nat, z => Nat.add(32n, z), SC.length(Bool, flat(t)), Nat.mul(SC.length(U32, t), 32n), length_flat(t))
197
198def flat_zeros(+m: Nat) -> {BL.allf(flat(SC.replicate(U32, m, 0))) == True{} : Bool}:
199 match m:
200 case 0n:
201 {==}
202 case 1n+p:
203 BL.allf_append(W.ubits(0), flat(SC.replicate(U32, p, 0)), {==}, flat_zeros(p))
204
205def zero_length(+d: Nat) -> {SC.length(Bool, flat(AR.ws(A.trep(B.Wd, d, B.W{0})))) == Nat.mul(SC.pow2(d), 32n) : Nat}:
206 %Equal.sym(List<&2, U32>, AR.ws(A.trep(B.Wd, d, B.W{0})), SC.replicate(U32, SC.pow2(d), 0), AR.ws_trep(d, 0)) : {SC.length(Bool, flat(_)) == Nat.mul(SC.pow2(d), 32n) : Nat}
207 %LL.length_replicate(U32, SC.pow2(d), 0) : {SC.length(Bool, flat(SC.replicate(U32, SC.pow2(d), 0))) == Nat.mul(_, 32n) : Nat}
208 length_flat(SC.replicate(U32, SC.pow2(d), 0))
209
210def zero_allf(+d: Nat) -> {BL.allf(flat(AR.ws(A.trep(B.Wd, d, B.W{0})))) == True{} : Bool}:
211 %Equal.sym(List<&2, U32>, AR.ws(A.trep(B.Wd, d, B.W{0})), SC.replicate(U32, SC.pow2(d), 0), AR.ws_trep(d, 0)) : {BL.allf(flat(_)) == True{} : Bool}
212 flat_zeros(SC.pow2(d))
213
214# `fits` is the documented capacity condition: the depth the representation is
215# allowed to reach (2^31 words = 2^36 bits) must cover n.
216def new_le(+n: Nat, +h: {Nat.is_le(n, Nat.mul(SC.pow2(B.depth_for(n)), 32n)) == True{} : Bool}) -> {Nat.is_le(n, SC.length(Bool, flat(AR.ws(A.trep(B.Wd, B.depth_for(n), B.W{0}))))) == True{} : Bool}:
217 L.subst(Nat, z => {Nat.is_le(n, z) == True{} : Bool}, Nat.mul(SC.pow2(B.depth_for(n)), 32n), SC.length(Bool, flat(AR.ws(A.trep(B.Wd, B.depth_for(n), B.W{0})))),
218 Equal.sym(Nat, SC.length(Bool, flat(AR.ws(A.trep(B.Wd, B.depth_for(n), B.W{0})))), Nat.mul(SC.pow2(B.depth_for(n)), 32n), zero_length(B.depth_for(n))), h)
219
220def new_rep(+n: Nat, +h: {Nat.is_le(n, Nat.mul(SC.pow2(B.depth_for(n)), 32n)) == True{} : Bool}) -> {rep(n, B.depth_for(n), A.trep(B.Wd, B.depth_for(n), B.W{0})) == True{} : Bool}:
221 rep_mk(n, B.depth_for(n), A.trep(B.Wd, B.depth_for(n), B.W{0}),
222 N.is_eq_refl(B.depth_for(n)),
223 A.trep_perfect(B.Wd, B.depth_for(n), B.W{0}),
224 inv_mk(n, flat(AR.ws(A.trep(B.Wd, B.depth_for(n), B.W{0}))), new_le(n, h),
225 BL.drop_allf(flat(AR.ws(A.trep(B.Wd, B.depth_for(n), B.W{0}))), n, zero_allf(B.depth_for(n)))))
226
227def new_abs(+n: Nat, +h: {Nat.is_le(n, Nat.mul(SC.pow2(B.depth_for(n)), 32n)) == True{} : Bool}) -> {abs(n, A.trep(B.Wd, B.depth_for(n), B.W{0})) == S.new(n) : List<&2, Bool>}:
228 BL.take_allf(flat(AR.ws(A.trep(B.Wd, B.depth_for(n), B.W{0}))), n, zero_allf(B.depth_for(n)), new_le(n, h))
229
230# `new(n)` is that array, thawed.
231def new_form(+n: Nat) -> {B.new(n) == B.BS{n, B.depth_for(n), A.thaw(B.Wd, A.trep(B.Wd, B.depth_for(n), B.W{0}))} : B.Bitset}:
232 Equal.cong(Array<B.Wd>, B.Bitset, a => B.BS{n, B.depth_for(n), a},
233 Array.new(B.Wd, B.depth_for(n), B.W{0}), A.thaw(B.Wd, A.trep(B.Wd, B.depth_for(n), B.W{0})),
234 A.new(B.Wd, B.depth_for(n), B.W{0}))
235
236# ---- the shadow: the Data mirror of a live bitset ----
237
238type Sh is Data:
239 Sh{len: Nat, depth: Nat, tree: A.Tree<B.Wd>}
240
241def real(sh: Sh) -> B.Bitset:
242 match sh:
243 case Sh{n, d, t}:
244 B.BS{n, d, A.thaw(B.Wd, t)}
245
246def good(sh: Sh) -> Bool:
247 match sh:
248 case Sh{n, d, t}:
249 rep(n, d, t)
250
251def model(sh: Sh) -> List<&2, Bool>:
252 match sh:
253 case Sh{n, d, t}:
254 abs(n, t)
255
256# The stored bit count is 32 per word.
257def flat_len(+d: Nat, +t: A.Tree<B.Wd>, +pf: {A.perfect(B.Wd, d, t) == True{} : Bool}) -> {SC.length(Bool, flat(AR.ws(t))) == Nat.mul(SC.pow2(d), 32n) : Nat}:
258 %AR.ws_length(d, t, pf) : {SC.length(Bool, flat(AR.ws(t))) == Nat.mul(_, 32n) : Nat}
259 length_flat(AR.ws(t))
260
261# Any bitset satisfying the invariant is within the capacity.
262def rep_fits(+n: Nat, +d: Nat, +t: A.Tree<B.Wd>, +g: {rep(n, d, t) == True{} : Bool}) -> {Nat.is_le(n, Nat.mul(SC.pow2(B.depth_for(n)), 32n)) == True{} : Bool}:
263 L.subst(Nat, z => {Nat.is_le(n, Nat.mul(SC.pow2(z), 32n)) == True{} : Bool}, d, B.depth_for(n),
264 N.eq_from_is_eq(d, B.depth_for(n), rep_depth(n, d, t, g)),
265 L.subst(Nat, z => {Nat.is_le(n, z) == True{} : Bool}, SC.length(Bool, flat(AR.ws(t))), Nat.mul(SC.pow2(d), 32n),
266 flat_len(d, t, rep_perfect(n, d, t, g)), inv_le(n, flat(AR.ws(t)), rep_invf(n, d, t, g))))
267
268# A bit index below the logical size addresses a word inside the array.
269def wordix_go(m: Nat, +i: Nat, b: Bool, +eb: {Nat.is_lt(i, 32n) == b : Bool}, +h: {Nat.is_lt(i, Nat.mul(m, 32n)) == True{} : Bool}) -> {Nat.is_lt(B.wordix(i), m) == True{} : Bool}:
270 match m b:
271 case 0n _:
272 Empty.absurd({Nat.is_lt(B.wordix(i), 0n) == True{} : Bool}, N.lt_zero_absurd(i, h))
273 case 1n+ +p True{}:
274 %Equal.sym(Nat, B.wordix(i), 0n, DP.wordix_small_alias(i, eb)) : {Nat.is_lt(_, 1n+p) == True{} : Bool}
275 {==}
276 case 1n+ +p False{}:
277 %Equal.sym(Nat, B.wordix(i), 1n+B.wordix(Nat.sub(i, 32n)), DP.wordix_step_alias(i, eb)) : {Nat.is_lt(_, 1n+p) == True{} : Bool}
278 wordix_go(p, Nat.sub(i, 32n), Nat.is_lt(Nat.sub(i, 32n), 32n), {==},
279 N.sub_lt(i, 32n, Nat.mul(p, 32n), N.not_lt_le(i, 32n, eb), h))
280
281def wordix_lt(+i: Nat, +m: Nat, +h: {Nat.is_lt(i, Nat.mul(m, 32n)) == True{} : Bool}) -> {Nat.is_lt(B.wordix(i), m) == True{} : Bool}:
282 wordix_go(m, i, Nat.is_lt(i, 32n), {==}, h)
283
284# Releasing a bitset is the unit: `burn_list` consumes any finite list.
285def burn_any(xs: List<B.Wd>) -> {B.burn_list(xs) == Unit{} : Unit}:
286 match xs:
287 case Nil{}:
288 {==}
289 case Con{x, t}:
290 burn_any(t)
291
292def dispose_ok(+n: Nat, +d: Nat, t: A.Tree<B.Wd>) -> {B.dispose(B.BS{n, d, A.thaw(B.Wd, t)}) == Unit{} : Unit}:
293 {==}
294
295# ---- the shadow of a live bitset is unique ----
296#
297# Every law about an operation says "the real operation lands on the array of
298# THIS shadow", and then states the model and the invariant of that shadow.
299# That is only meaningful if a runtime bitset determines its shadow, i.e. if
300# `real` is injective - otherwise a proof could name a different shadow that
301# happens to have the same `real` and claim its model. It is.
302
303def blen_go(+n: Nat, u: Unit) -> Nat:
304 match u:
305 case Unit{}:
306 n
307
308def blen(s: B.Bitset) -> Nat:
309 match s:
310 case B.BS{+n, d, a}:
311 blen_go(n, B.burn(a))
312
313def bdepth(s: B.Bitset) -> Nat:
314 match s:
315 case B.BS{n, +d, a}:
316 blen_go(d, B.burn(a))
317
318def btree(s: B.Bitset) -> A.Tree<B.Wd>:
319 match s:
320 case B.BS{n, d, a}:
321 A.freeze(B.Wd, a)
322
323def sh_len(sh: Sh) -> Nat:
324 match sh:
325 case Sh{n, d, t}:
326 n
327
328def sh_depth(sh: Sh) -> Nat:
329 match sh:
330 case Sh{n, d, t}:
331 d
332
333def sh_tree(sh: Sh) -> A.Tree<B.Wd>:
334 match sh:
335 case Sh{n, d, t}:
336 t
337
338def real_len(+sh: Sh) -> {blen(real(sh)) == sh_len(sh) : Nat}:
339 match sh:
340 case Sh{+n, d, t}:
341 {==}
342
343def real_depth(+sh: Sh) -> {bdepth(real(sh)) == sh_depth(sh) : Nat}:
344 match sh:
345 case Sh{n, +d, t}:
346 {==}
347
348def real_tree(+sh: Sh) -> {btree(real(sh)) == sh_tree(sh) : A.Tree<B.Wd>}:
349 match sh:
350 case Sh{n, d, +t}:
351 A.freeze_thaw(B.Wd, t)
352
353def sh_eta(+sh: Sh) -> {sh == Sh{sh_len(sh), sh_depth(sh), sh_tree(sh)} : Sh}:
354 match sh:
355 case Sh{n, d, t}:
356 {==}
357
358def real_inj_parts(+a: Sh, +b: Sh, +e: {real(a) == real(b) : B.Bitset}) -> {Sh{sh_len(a), sh_depth(a), sh_tree(a)} == Sh{sh_len(b), sh_depth(b), sh_tree(b)} : Sh}:
359 %real_len(a) : {Sh{_, sh_depth(a), sh_tree(a)} == Sh{sh_len(b), sh_depth(b), sh_tree(b)} : Sh}
360 %real_depth(a) : {Sh{blen(real(a)), _, sh_tree(a)} == Sh{sh_len(b), sh_depth(b), sh_tree(b)} : Sh}
361 %real_tree(a) : {Sh{blen(real(a)), bdepth(real(a)), _} == Sh{sh_len(b), sh_depth(b), sh_tree(b)} : Sh}
362 %real_len(b) : {Sh{blen(real(a)), bdepth(real(a)), btree(real(a))} == Sh{_, sh_depth(b), sh_tree(b)} : Sh}
363 %real_depth(b) : {Sh{blen(real(a)), bdepth(real(a)), btree(real(a))} == Sh{blen(real(b)), _, sh_tree(b)} : Sh}
364 %real_tree(b) : {Sh{blen(real(a)), bdepth(real(a)), btree(real(a))} == Sh{blen(real(b)), bdepth(real(b)), _} : Sh}
365 Equal.cong(B.Bitset, Sh, s => Sh{blen(s), bdepth(s), btree(s)}, real(a), real(b), e)
366
367def real_inj(+a: Sh, +b: Sh, +e: {real(a) == real(b) : B.Bitset}) -> {a == b : Sh}:
368 Equal.trans(Sh, a, Sh{sh_len(a), sh_depth(a), sh_tree(a)}, b,
369 sh_eta(a),
370 Equal.trans(Sh, Sh{sh_len(a), sh_depth(a), sh_tree(a)}, Sh{sh_len(b), sh_depth(b), sh_tree(b)}, b,
371 real_inj_parts(a, b, e),
372 Equal.sym(Sh, b, Sh{sh_len(b), sh_depth(b), sh_tree(b)}, sh_eta(b))))