proofs/containers/bitset/proof.bend
bend-collections-laws-containers@1.0.0.0 · 404 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/array.bend as A
3import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
4import bend-collections-laws-containers@1.0.0.0/spec/containers/bitset.bend as S
5import bend-collections-laws-containers@1.0.0.0/src/containers/bitset.bend as B
6import bend-collections-laws-containers@1.0.0.0/src/containers/types/bitset.bend as E
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/word.bend as W
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/index.bend as IX
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/depth.bend as DP
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/arr.bend as AR
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/state.bend as ST
13import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/steps.bend as BS
14import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/trace.bend as BT
15import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
16import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
17import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LL
18
19# Packed bitset: public proof entry point.
20# abstraction ST.abs(n, t) (first n bits of the stored U32 words)
21# invariant ST.rep(n, d, t) (the depth is the one `depth_for` picks, the
22# word array is a perfect tree of that depth, n <= stored bits,
23# every stored bit at a position >= n is zero)
24# shadow ST.Sh / ST.real / ST.good / ST.model (Base.Array is linear,
25# so every law is about the array built from a Data mirror
26# tree, exactly as in proofs/dynamic_array)
27# word facts W.* (U32 and/or/xor/not/shifts from Base's Word defs)
28# index facts IX.* (i / 32 and i % 32 peel 32 bits at a time)
29# array facts AR.* (Base.Array get/set against the slot list)
30# operations BS.step_ok (every op; IndexOutOfRange / LengthMismatch keep
31# the state)
32# traces trace_new (arbitrary op lists from B.new(n))
33#
34# `capacity(n)` is the documented capacity condition of the packed
35# representation: 2^31 words = 2^36 bits (see src/bitset.bend). It is a
36# premise only of the laws about `new`; every other law holds at every state
37# satisfying the invariant, and the invariant itself implies it
38# (ST.rep_fits).
39
40def capacity(+n: Nat) -> Type:
41 {Nat.is_le(n, Nat.mul(SC.pow2(B.depth_for(n)), 32n)) == True{} : Bool}
42
43def new_abs(+n: Nat, +h: {Nat.is_le(n, Nat.mul(SC.pow2(B.depth_for(n)), 32n)) == True{} : Bool}) -> {ST.model(BT.initial(n)) == S.new(n) : List<&2, Bool>}:
44 BT.new_model(n, h)
45
46def new_inv(+n: Nat, +h: {Nat.is_le(n, Nat.mul(SC.pow2(B.depth_for(n)), 32n)) == True{} : Bool}) -> {ST.good(BT.initial(n)) == True{} : Bool}:
47 BT.new_good(n, h)
48
49def new_real(+n: Nat) -> {B.new(n) == ST.real(BT.initial(n)) : B.Bitset}:
50 BT.new_real(n)
51
52def from_bools(+ys: List<&2, Bool>, +hf: {Nat.is_le(B.bool_count(ys), Nat.mul(SC.pow2(B.depth_for(B.bool_count(ys))), 32n)) == True{} : Bool}) -> BS.FromOK(ys):
53 BS.from_ok(ys, hf)
54
55def step_ok(sh: ST.Sh, op: E.Op, +g: {ST.good(sh) == True{} : Bool}) -> BS.StepOK(sh, op):
56 BS.step_ok(sh, op, g)
57
58# A runtime bitset determines its shadow, so "the operation lands on the array
59# of THIS shadow, whose model is the spec's" pins the abstract state: the laws
60# above cannot be satisfied by naming a different shadow.
61def shadow_unique(+a: ST.Sh, +b: ST.Sh, +e: {ST.real(a) == ST.real(b) : B.Bitset}) -> {a == b : ST.Sh}:
62 ST.real_inj(a, b, e)
63
64# Arbitrary finite operation traces from the real constructor.
65def trace_new(+n: Nat, +ops: List<&2, E.Op>, +h: {Nat.is_le(n, Nat.mul(SC.pow2(B.depth_for(n)), 32n)) == True{} : Bool}) -> BT.TraceOK(ops, BT.initial(n)):
66 BT.trace_from(ops, BT.initial(n), BT.new_good(n, h))
67
68# ==== the contract of bitset (stated in spec/containers/bitset.bend) ====================
69
70# ---- the implementation ----
71def Impl(sh: ST.Sh, op: E.Op, Post: (List<&2, Bool> & E.Obs) -> Type) -> Type:
72 Sigma<&1, &1, ST.Sh, sh2 => Sigma<&1, &1, E.Obs, o => {B.step(ST.real(sh), op) == (ST.real(sh2), o) : B.Bitset & E.Obs} & ({ST.good(sh2) == True{} : Bool} & Post((ST.model(sh2), o)))>>
73
74def impl_of(-sh: ST.Sh, -op: E.Op, -Post: (List<&2, Bool> & E.Obs) -> Type, k: BS.StepOK(sh, op), pf: Post(S.step(ST.model(sh), op))) -> Impl(sh, op, Post):
75 match k:
76 case Tuple{sh2, Tuple{o, Tuple{e1, Tuple{g2, e2}}}}:
77 (sh2, (o, (e1, (g2, L.subst(List<&2, Bool> & E.Obs, Post, S.step(ST.model(sh), op), (ST.model(sh2), o), Equal.sym(List<&2, Bool> & E.Obs, (ST.model(sh2), o), S.step(ST.model(sh), op), e2), pf)))))
78
79def impl(sh: ST.Sh, op: E.Op, +g: {ST.good(sh) == True{} : Bool}, -Post: (List<&2, Bool> & E.Obs) -> Type, pf: Post(S.step(ST.model(sh), op))) -> Impl(sh, op, Post):
80 impl_of(sh, op, Post, step_ok(sh, op, g), pf)
81
82# ---- arithmetic and Boolean facts ----
83def succ_ne_zero(+a: Nat, +e: {1n+a == 0n : Nat}) -> Empty:
84 L.false_true(Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), 1n+a, 0n, e))
85
86def zero_ne_succ(+a: Nat, +e: {0n == 1n+a : Nat}) -> Empty:
87 L.true_false(Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), 0n, 1n+a, e))
88
89def succ_pick(+b: Bool, +x: Nat, +y: Nat) -> {1n+Bool.pick(Nat, b, x, y) == Bool.pick(Nat, b, 1n+x, 1n+y) : Nat}:
90 match b:
91 case True{}:
92 {==}
93 case False{}:
94 {==}
95
96def zero_add(+n: Nat) -> {Nat.add(0n, n) == n : Nat}:
97 Equal.trans(Nat, Nat.add(0n, n), Nat.add(n, 0n), n, N.add_comm(0n, n), N.add_zero(n))
98
99def succ_add(+a: Nat, +b: Nat) -> {Nat.add(1n+a, b) == Nat.add(a, 1n+b) : Nat}:
100 Equal.trans(Nat, Nat.add(1n+a, b), Nat.add(b, 1n+a), Nat.add(a, 1n+b), N.add_comm(1n+a, b),
101 Equal.trans(Nat, Nat.add(b, 1n+a), 1n+Nat.add(b, a), Nat.add(a, 1n+b), N.add_succ(b, a),
102 Equal.trans(Nat, 1n+Nat.add(b, a), 1n+Nat.add(a, b), Nat.add(a, 1n+b), N.succ_cong(Nat.add(b, a), Nat.add(a, b), N.add_comm(b, a)), Equal.sym(Nat, Nat.add(a, 1n+b), 1n+Nat.add(a, b), N.add_succ(a, b)))))
103
104# ---- Contains ----
105def inset_nth(+xs: List<&2, Bool>, +k: Nat, +b: Bool, +h: {SC.nth(Bool, xs, k) == Some{b} : Maybe<&2, Bool>}) -> {S.inset(xs, k) == b : Bool}:
106 %Equal.sym(Maybe<&2, Bool>, SC.nth(Bool, xs, k), Some{b}, h) : {S.ins(_) == b : Bool}
107 {==}
108
109def gr_y(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}, +y: Maybe<&2, Bool>, +hy: {SC.nth(Bool, xs, i) == y : Maybe<&2, Bool>}) -> {S.ob(xs, E.Get{i}) == E.OBit{Done{S.inset(xs, i)}} : E.Obs}:
110 match y:
111 case None{}:
112 Empty.absurd({S.ob(xs, E.Get{i}) == E.OBit{Done{S.inset(xs, i)}} : E.Obs}, LL.sc_nth_some(Bool, xs, i, h, hy))
113 case Some{+b}:
114 %Equal.sym(Maybe<&2, Bool>, SC.nth(Bool, xs, i), Some{b}, hy) : {E.OBit{S.bit(_)} == E.OBit{Done{S.ins(_)}} : E.Obs}
115 {==}
116
117def get_result(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}) -> S.Contains.get_result(xs, i, h):
118 gr_y(xs, i, h, SC.nth(Bool, xs, i), {==})
119
120def get_frame(+xs: List<&2, Bool>, +i: Nat) -> S.Contains.get_frame(xs, i):
121 {==}
122
123def get_outside(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_le(SC.length(Bool, xs), i) == True{} : Bool}) -> S.Contains.get_outside(xs, i, h):
124 %Equal.sym(Maybe<&2, Bool>, SC.nth(Bool, xs, i), None{}, LL.nth_none(Bool, xs, i, h)) : {E.OBit{S.bit(_)} == E.OBit{Fail{E.IndexOutOfRange{}}} : E.Obs}
125 {==}
126
127# ---- Length (the member count), Capacity (the universe) ----
128def count_result(+xs: List<&2, Bool>) -> S.Length.count_result(xs):
129 {==}
130
131def count_frame(+xs: List<&2, Bool>) -> S.Length.count_frame(xs):
132 {==}
133
134def length_result(+xs: List<&2, Bool>) -> S.Capacity.length_result(xs):
135 {==}
136
137def length_frame(+xs: List<&2, Bool>) -> S.Capacity.length_frame(xs):
138 {==}
139
140# ---- Empty_Set: no member, Length 0, over the universe [0, n) ----
141def new_contains(+n: Nat, +k: Nat) -> S.Empty_Set.new_contains(n, k):
142 match n k:
143 case 0n _:
144 {==}
145 case 1n+m 0n:
146 {==}
147 case 1n+ +m 1n+ +j:
148 new_contains(m, j)
149
150def new_count(+n: Nat) -> S.Empty_Set.new_count(n):
151 match n:
152 case 0n:
153 {==}
154 case 1n+ +m:
155 new_count(m)
156
157def new_length(+n: Nat) -> S.Empty_Set.new_length(n):
158 LL.length_replicate(Bool, n, False{})
159
160# ---- the update of one bit ----
161def assign_is(+xs: List<&2, Bool>, +i: Nat, +v: Bool, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}, +y: Maybe<&2, Bool>, +hy: {SC.nth(Bool, xs, i) == y : Maybe<&2, Bool>}) -> {S.assign(xs, i, v) == (SC.update(Bool, xs, i, v), E.OUnit{Done{Unit{}}}) : List<&2, Bool> & E.Obs}:
162 match y:
163 case None{}:
164 Empty.absurd({S.assign(xs, i, v) == (SC.update(Bool, xs, i, v), E.OUnit{Done{Unit{}}}) : List<&2, Bool> & E.Obs}, LL.sc_nth_some(Bool, xs, i, h, hy))
165 case Some{b}:
166 %Equal.sym(Maybe<&2, Bool>, SC.nth(Bool, xs, i), Some{b}, hy) : {S.assign_at(_, xs, i, v) == (SC.update(Bool, xs, i, v), E.OUnit{Done{Unit{}}}) : List<&2, Bool> & E.Obs}
167 {==}
168
169def inset_update_same(+xs: List<&2, Bool>, +i: Nat, +v: Bool, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}) -> {S.inset(SC.update(Bool, xs, i, v), i) == v : Bool}:
170 inset_nth(SC.update(Bool, xs, i, v), i, v, LL.nth_update_same(Bool, xs, i, v, h))
171
172def inset_update_other(+xs: List<&2, Bool>, +i: Nat, +j: Nat, +v: Bool, +ne: {Nat.is_eq(i, j) == False{} : Bool}) -> {S.inset(SC.update(Bool, xs, i, v), j) == S.inset(xs, j) : Bool}:
173 Equal.cong(Maybe<&2, Bool>, Bool, z => S.ins(z), SC.nth(Bool, SC.update(Bool, xs, i, v), j), SC.nth(Bool, xs, j), LL.nth_update_other(Bool, xs, i, j, v, ne))
174
175# count after setting a bit: one more unless it was set
176def cu_set(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}) -> {S.count(SC.update(Bool, xs, i, True{})) == Bool.pick(Nat, S.inset(xs, i), S.count(xs), 1n+S.count(xs)) : Nat}:
177 match xs i:
178 case Nil{} _:
179 Empty.absurd({S.count(SC.update(Bool, Nil{}, i, True{})) == Bool.pick(Nat, S.inset(Nil{}, i), S.count(Nil{}), 1n+S.count(Nil{})) : Nat}, N.lt_zero_absurd(i, h))
180 case Con{True{}, t} 0n:
181 {==}
182 case Con{False{}, t} 0n:
183 {==}
184 case Con{True{}, +t} 1n+ +p:
185 %Equal.sym(Nat, S.count(SC.update(Bool, t, p, True{})), Bool.pick(Nat, S.inset(t, p), S.count(t), 1n+S.count(t)), cu_set(t, p, h)) : {1n+_ == Bool.pick(Nat, S.inset(t, p), 1n+S.count(t), 1n+(1n+S.count(t))) : Nat}
186 succ_pick(S.inset(t, p), S.count(t), 1n+S.count(t))
187 case Con{False{}, +t} 1n+ +p:
188 cu_set(t, p, h)
189
190# count after clearing a bit: one less if it was set
191def cu_clear(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}) -> {S.count(xs) == Bool.pick(Nat, S.inset(xs, i), 1n+S.count(SC.update(Bool, xs, i, False{})), S.count(SC.update(Bool, xs, i, False{}))) : Nat}:
192 match xs i:
193 case Nil{} _:
194 Empty.absurd({S.count(Nil{}) == Bool.pick(Nat, S.inset(Nil{}, i), 1n+S.count(SC.update(Bool, Nil{}, i, False{})), S.count(SC.update(Bool, Nil{}, i, False{}))) : Nat}, N.lt_zero_absurd(i, h))
195 case Con{True{}, t} 0n:
196 {==}
197 case Con{False{}, t} 0n:
198 {==}
199 case Con{True{}, +t} 1n+ +p:
200 %Equal.sym(Nat, S.count(t), Bool.pick(Nat, S.inset(t, p), 1n+S.count(SC.update(Bool, t, p, False{})), S.count(SC.update(Bool, t, p, False{}))), cu_clear(t, p, h)) : {1n+_ == Bool.pick(Nat, S.inset(t, p), 1n+(1n+S.count(SC.update(Bool, t, p, False{}))), 1n+S.count(SC.update(Bool, t, p, False{}))) : Nat}
201 succ_pick(S.inset(t, p), 1n+S.count(SC.update(Bool, t, p, False{})), S.count(SC.update(Bool, t, p, False{})))
202 case Con{False{}, +t} 1n+ +p:
203 cu_clear(t, p, h)
204
205# ---- Include / Insert (set) ----
206def set_model(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}) -> {S.nx(xs, E.Set{i}) == SC.update(Bool, xs, i, True{}) : List<&2, Bool>}:
207 %Equal.sym(List<&2, Bool> & E.Obs, S.assign(xs, i, True{}), (SC.update(Bool, xs, i, True{}), E.OUnit{Done{Unit{}}}), assign_is(xs, i, True{}, h, SC.nth(Bool, xs, i), {==})) : {Pair.fst(List<&2, Bool>, E.Obs, _) == SC.update(Bool, xs, i, True{}) : List<&2, Bool>}
208 {==}
209
210def set_contains(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}) -> S.Include.set_contains(xs, i, h):
211 %Equal.sym(List<&2, Bool>, S.nx(xs, E.Set{i}), SC.update(Bool, xs, i, True{}), set_model(xs, i, h)) : {S.inset(_, i) == True{} : Bool}
212 inset_update_same(xs, i, True{}, h)
213
214def set_others(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}, +j: Nat, +ne: {Nat.is_eq(i, j) == False{} : Bool}) -> S.Include.set_others(xs, i, h, j, ne):
215 %Equal.sym(List<&2, Bool>, S.nx(xs, E.Set{i}), SC.update(Bool, xs, i, True{}), set_model(xs, i, h)) : {S.inset(_, j) == S.inset(xs, j) : Bool}
216 inset_update_other(xs, i, j, True{}, ne)
217
218def set_universe(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}) -> S.Include.set_universe(xs, i, h):
219 %Equal.sym(List<&2, Bool>, S.nx(xs, E.Set{i}), SC.update(Bool, xs, i, True{}), set_model(xs, i, h)) : {SC.length(Bool, _) == SC.length(Bool, xs) : Nat}
220 LL.length_update(Bool, xs, i, True{})
221
222def set_outside(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_le(SC.length(Bool, xs), i) == True{} : Bool}) -> S.Include.set_outside(xs, i, h):
223 %Equal.sym(Maybe<&2, Bool>, SC.nth(Bool, xs, i), None{}, LL.nth_none(Bool, xs, i, h)) : {S.assign_at(_, xs, i, True{}) == (xs, E.OUnit{Fail{E.IndexOutOfRange{}}}) : List<&2, Bool> & E.Obs}
224 {==}
225
226# ---- Exclude / Delete (clear) ----
227def clear_model(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}) -> {S.nx(xs, E.Clear{i}) == SC.update(Bool, xs, i, False{}) : List<&2, Bool>}:
228 %Equal.sym(List<&2, Bool> & E.Obs, S.assign(xs, i, False{}), (SC.update(Bool, xs, i, False{}), E.OUnit{Done{Unit{}}}), assign_is(xs, i, False{}, h, SC.nth(Bool, xs, i), {==})) : {Pair.fst(List<&2, Bool>, E.Obs, _) == SC.update(Bool, xs, i, False{}) : List<&2, Bool>}
229 {==}
230
231def clear_contains(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}) -> S.Exclude.clear_contains(xs, i, h):
232 %Equal.sym(List<&2, Bool>, S.nx(xs, E.Clear{i}), SC.update(Bool, xs, i, False{}), clear_model(xs, i, h)) : {S.inset(_, i) == False{} : Bool}
233 inset_update_same(xs, i, False{}, h)
234
235def clear_others(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}, +j: Nat, +ne: {Nat.is_eq(i, j) == False{} : Bool}) -> S.Exclude.clear_others(xs, i, h, j, ne):
236 %Equal.sym(List<&2, Bool>, S.nx(xs, E.Clear{i}), SC.update(Bool, xs, i, False{}), clear_model(xs, i, h)) : {S.inset(_, j) == S.inset(xs, j) : Bool}
237 inset_update_other(xs, i, j, False{}, ne)
238
239def clear_universe(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}) -> S.Exclude.clear_universe(xs, i, h):
240 %Equal.sym(List<&2, Bool>, S.nx(xs, E.Clear{i}), SC.update(Bool, xs, i, False{}), clear_model(xs, i, h)) : {SC.length(Bool, _) == SC.length(Bool, xs) : Nat}
241 LL.length_update(Bool, xs, i, False{})
242
243def clear_outside(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_le(SC.length(Bool, xs), i) == True{} : Bool}) -> S.Exclude.clear_outside(xs, i, h):
244 %Equal.sym(Maybe<&2, Bool>, SC.nth(Bool, xs, i), None{}, LL.nth_none(Bool, xs, i, h)) : {S.assign_at(_, xs, i, False{}) == (xs, E.OUnit{Fail{E.IndexOutOfRange{}}}) : List<&2, Bool> & E.Obs}
245 {==}
246
247# Include: one more member unless it was one (Insert's Pre: it was not)
248def set_count(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}) -> S.Include.set_count(xs, i, h):
249 %Equal.sym(List<&2, Bool>, S.nx(xs, E.Set{i}), SC.update(Bool, xs, i, True{}), set_model(xs, i, h)) : {S.count(_) == Bool.pick(Nat, S.inset(xs, i), S.count(xs), 1n+S.count(xs)) : Nat}
250 cu_set(xs, i, h)
251
252# Exclude: one member less if it was one (Delete's Pre: it was)
253def clear_count(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}) -> S.Exclude.clear_count(xs, i, h):
254 %Equal.sym(List<&2, Bool>, S.nx(xs, E.Clear{i}), SC.update(Bool, xs, i, False{}), clear_model(xs, i, h)) : {S.count(xs) == Bool.pick(Nat, S.inset(xs, i), 1n+S.count(_), S.count(_)) : Nat}
255 cu_clear(xs, i, h)
256
257# ---- Union (1180) ----
258def union_pt(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +k: Nat, +h: {SC.length(Bool, xs) == SC.length(Bool, ys) : Nat}) -> {S.inset(S.zip_or(xs, ys), k) == Bool.or(S.inset(xs, k), S.inset(ys, k)) : Bool}:
259 match xs ys k:
260 case Nil{} Nil{} _:
261 {==}
262 case Nil{} Con{b, t} _:
263 Empty.absurd({S.inset(S.zip_or(Nil{}, Con{b, t}), k) == Bool.or(S.inset(Nil{}, k), S.inset(Con{b, t}, k)) : Bool}, zero_ne_succ(SC.length(Bool, t), h))
264 case Con{a, s} Nil{} _:
265 Empty.absurd({S.inset(S.zip_or(Con{a, s}, Nil{}), k) == Bool.or(S.inset(Con{a, s}, k), S.inset(Nil{}, k)) : Bool}, succ_ne_zero(SC.length(Bool, s), h))
266 case Con{a, s} Con{b, t} 0n:
267 {==}
268 case Con{a, +s} Con{b, +t} 1n+ +p:
269 union_pt(s, t, p, N.succ_inj(SC.length(Bool, s), SC.length(Bool, t), h))
270
271def union_contains(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +k: Nat, +h: {SC.length(Bool, xs) == SC.length(Bool, ys) : Nat}) -> S.Union.union_contains(xs, ys, k, h):
272 %h : {S.inset(Pair.fst(List<&2, Bool>, E.Obs, S.combine_if(Nat.is_eq(SC.length(Bool, xs), _), xs, S.zip_or(xs, ys))), k) == Bool.or(S.inset(xs, k), S.inset(ys, k)) : Bool}
273 %Equal.sym(Bool, Nat.is_eq(SC.length(Bool, xs), SC.length(Bool, xs)), True{}, N.is_eq_refl(SC.length(Bool, xs))) : {S.inset(Pair.fst(List<&2, Bool>, E.Obs, S.combine_if(_, xs, S.zip_or(xs, ys))), k) == Bool.or(S.inset(xs, k), S.inset(ys, k)) : Bool}
274 union_pt(xs, ys, k, h)
275
276def union_mismatch(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +h: {Nat.is_eq(SC.length(Bool, xs), SC.length(Bool, ys)) == False{} : Bool}) -> S.Union.union_mismatch(xs, ys, h):
277 %Equal.sym(Bool, Nat.is_eq(SC.length(Bool, xs), SC.length(Bool, ys)), False{}, h) : {S.combine_if(_, xs, S.zip_or(xs, ys)) == (xs, E.OUnit{Fail{E.LengthMismatch{}}}) : List<&2, Bool> & E.Obs}
278 {==}
279
280# ---- Intersection (1279) ----
281def intersection_pt(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +k: Nat, +h: {SC.length(Bool, xs) == SC.length(Bool, ys) : Nat}) -> {S.inset(S.zip_and(xs, ys), k) == Bool.and(S.inset(xs, k), S.inset(ys, k)) : Bool}:
282 match xs ys k:
283 case Nil{} Nil{} _:
284 {==}
285 case Nil{} Con{b, t} _:
286 Empty.absurd({S.inset(S.zip_and(Nil{}, Con{b, t}), k) == Bool.and(S.inset(Nil{}, k), S.inset(Con{b, t}, k)) : Bool}, zero_ne_succ(SC.length(Bool, t), h))
287 case Con{a, s} Nil{} _:
288 Empty.absurd({S.inset(S.zip_and(Con{a, s}, Nil{}), k) == Bool.and(S.inset(Con{a, s}, k), S.inset(Nil{}, k)) : Bool}, succ_ne_zero(SC.length(Bool, s), h))
289 case Con{a, s} Con{b, t} 0n:
290 {==}
291 case Con{a, +s} Con{b, +t} 1n+ +p:
292 intersection_pt(s, t, p, N.succ_inj(SC.length(Bool, s), SC.length(Bool, t), h))
293
294def intersection_contains(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +k: Nat, +h: {SC.length(Bool, xs) == SC.length(Bool, ys) : Nat}) -> S.Intersection.intersection_contains(xs, ys, k, h):
295 %h : {S.inset(Pair.fst(List<&2, Bool>, E.Obs, S.combine_if(Nat.is_eq(SC.length(Bool, xs), _), xs, S.zip_and(xs, ys))), k) == Bool.and(S.inset(xs, k), S.inset(ys, k)) : Bool}
296 %Equal.sym(Bool, Nat.is_eq(SC.length(Bool, xs), SC.length(Bool, xs)), True{}, N.is_eq_refl(SC.length(Bool, xs))) : {S.inset(Pair.fst(List<&2, Bool>, E.Obs, S.combine_if(_, xs, S.zip_and(xs, ys))), k) == Bool.and(S.inset(xs, k), S.inset(ys, k)) : Bool}
297 intersection_pt(xs, ys, k, h)
298
299def intersection_mismatch(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +h: {Nat.is_eq(SC.length(Bool, xs), SC.length(Bool, ys)) == False{} : Bool}) -> S.Intersection.intersection_mismatch(xs, ys, h):
300 %Equal.sym(Bool, Nat.is_eq(SC.length(Bool, xs), SC.length(Bool, ys)), False{}, h) : {S.combine_if(_, xs, S.zip_and(xs, ys)) == (xs, E.OUnit{Fail{E.LengthMismatch{}}}) : List<&2, Bool> & E.Obs}
301 {==}
302
303# ---- Difference (1340) ----
304def difference_pt(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +k: Nat, +h: {SC.length(Bool, xs) == SC.length(Bool, ys) : Nat}) -> {S.inset(S.zip_diff(xs, ys), k) == Bool.and(S.inset(xs, k), Bool.not(S.inset(ys, k))) : Bool}:
305 match xs ys k:
306 case Nil{} Nil{} _:
307 {==}
308 case Nil{} Con{b, t} _:
309 Empty.absurd({S.inset(S.zip_diff(Nil{}, Con{b, t}), k) == Bool.and(S.inset(Nil{}, k), Bool.not(S.inset(Con{b, t}, k))) : Bool}, zero_ne_succ(SC.length(Bool, t), h))
310 case Con{a, s} Nil{} _:
311 Empty.absurd({S.inset(S.zip_diff(Con{a, s}, Nil{}), k) == Bool.and(S.inset(Con{a, s}, k), Bool.not(S.inset(Nil{}, k))) : Bool}, succ_ne_zero(SC.length(Bool, s), h))
312 case Con{a, s} Con{b, t} 0n:
313 {==}
314 case Con{a, +s} Con{b, +t} 1n+ +p:
315 difference_pt(s, t, p, N.succ_inj(SC.length(Bool, s), SC.length(Bool, t), h))
316
317def difference_contains(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +k: Nat, +h: {SC.length(Bool, xs) == SC.length(Bool, ys) : Nat}) -> S.Difference.difference_contains(xs, ys, k, h):
318 %h : {S.inset(Pair.fst(List<&2, Bool>, E.Obs, S.combine_if(Nat.is_eq(SC.length(Bool, xs), _), xs, S.zip_diff(xs, ys))), k) == Bool.and(S.inset(xs, k), Bool.not(S.inset(ys, k))) : Bool}
319 %Equal.sym(Bool, Nat.is_eq(SC.length(Bool, xs), SC.length(Bool, xs)), True{}, N.is_eq_refl(SC.length(Bool, xs))) : {S.inset(Pair.fst(List<&2, Bool>, E.Obs, S.combine_if(_, xs, S.zip_diff(xs, ys))), k) == Bool.and(S.inset(xs, k), Bool.not(S.inset(ys, k))) : Bool}
320 difference_pt(xs, ys, k, h)
321
322def difference_mismatch(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +h: {Nat.is_eq(SC.length(Bool, xs), SC.length(Bool, ys)) == False{} : Bool}) -> S.Difference.difference_mismatch(xs, ys, h):
323 %Equal.sym(Bool, Nat.is_eq(SC.length(Bool, xs), SC.length(Bool, ys)), False{}, h) : {S.combine_if(_, xs, S.zip_diff(xs, ys)) == (xs, E.OUnit{Fail{E.LengthMismatch{}}}) : List<&2, Bool> & E.Obs}
324 {==}
325
326# ---- Symmetric_Difference (1404) ----
327def symmetric_difference_pt(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +k: Nat, +h: {SC.length(Bool, xs) == SC.length(Bool, ys) : Nat}) -> {S.inset(S.zip_xor(xs, ys), k) == Bool.xor(S.inset(xs, k), S.inset(ys, k)) : Bool}:
328 match xs ys k:
329 case Nil{} Nil{} _:
330 {==}
331 case Nil{} Con{b, t} _:
332 Empty.absurd({S.inset(S.zip_xor(Nil{}, Con{b, t}), k) == Bool.xor(S.inset(Nil{}, k), S.inset(Con{b, t}, k)) : Bool}, zero_ne_succ(SC.length(Bool, t), h))
333 case Con{a, s} Nil{} _:
334 Empty.absurd({S.inset(S.zip_xor(Con{a, s}, Nil{}), k) == Bool.xor(S.inset(Con{a, s}, k), S.inset(Nil{}, k)) : Bool}, succ_ne_zero(SC.length(Bool, s), h))
335 case Con{a, s} Con{b, t} 0n:
336 {==}
337 case Con{a, +s} Con{b, +t} 1n+ +p:
338 symmetric_difference_pt(s, t, p, N.succ_inj(SC.length(Bool, s), SC.length(Bool, t), h))
339
340def symmetric_difference_contains(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +k: Nat, +h: {SC.length(Bool, xs) == SC.length(Bool, ys) : Nat}) -> S.Symmetric_Difference.symmetric_difference_contains(xs, ys, k, h):
341 %h : {S.inset(Pair.fst(List<&2, Bool>, E.Obs, S.combine_if(Nat.is_eq(SC.length(Bool, xs), _), xs, S.zip_xor(xs, ys))), k) == Bool.xor(S.inset(xs, k), S.inset(ys, k)) : Bool}
342 %Equal.sym(Bool, Nat.is_eq(SC.length(Bool, xs), SC.length(Bool, xs)), True{}, N.is_eq_refl(SC.length(Bool, xs))) : {S.inset(Pair.fst(List<&2, Bool>, E.Obs, S.combine_if(_, xs, S.zip_xor(xs, ys))), k) == Bool.xor(S.inset(xs, k), S.inset(ys, k)) : Bool}
343 symmetric_difference_pt(xs, ys, k, h)
344
345def xor_mismatch(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +h: {Nat.is_eq(SC.length(Bool, xs), SC.length(Bool, ys)) == False{} : Bool}) -> S.Symmetric_Difference.xor_mismatch(xs, ys, h):
346 %Equal.sym(Bool, Nat.is_eq(SC.length(Bool, xs), SC.length(Bool, ys)), False{}, h) : {S.combine_if(_, xs, S.zip_xor(xs, ys)) == (xs, E.OUnit{Fail{E.LengthMismatch{}}}) : List<&2, Bool> & E.Obs}
347 {==}
348
349def to_list_result(+xs: List<&2, Bool>) -> S.Elements.to_list_result(xs):
350 {==}
351
352def to_list_frame(+xs: List<&2, Bool>) -> S.Elements.to_list_frame(xs):
353 {==}
354
355# no member below the offset
356def members_above(+xs: List<&2, Bool>, +off: Nat, +j: Nat, +h: {Nat.is_lt(j, off) == True{} : Bool}) -> {S.nmem(j, S.members(xs, off)) == False{} : Bool}:
357 match xs:
358 case Nil{}:
359 {==}
360 case Con{False{}, +t}:
361 members_above(t, 1n+off, j, N.lt_trans(j, off, 1n+off, h, N.lt_succ(off)))
362 case Con{True{}, +t}:
363 %Equal.sym(Bool, Nat.is_eq(off, j), False{}, N.is_eq_sym_false(j, off, N.is_eq_lt(j, off, h))) : {Bool.or(_, S.nmem(j, S.members(t, 1n+off))) == False{} : Bool}
364 members_above(t, 1n+off, j, N.lt_trans(j, off, 1n+off, h, N.lt_succ(off)))
365
366def rel_add(+off: Nat, +p: Nat) -> {Nat.add(1n+off, p) == Nat.add(1n+p, off) : Nat}:
367 Equal.trans(Nat, Nat.add(1n+off, p), Nat.add(off, 1n+p), Nat.add(1n+p, off), succ_add(off, p), N.add_comm(off, 1n+p))
368
369def ne_add_succ(+off: Nat, +p: Nat) -> {Nat.is_eq(off, Nat.add(1n+p, off)) == False{} : Bool}:
370 N.is_eq_lt(off, Nat.add(1n+p, off), N.lt_le_trans(off, 1n+off, Nat.add(1n+p, off), N.lt_succ(off), L.subst(Nat, z => {Nat.is_le(1n+off, z) == True{} : Bool}, Nat.add(1n+off, p), Nat.add(1n+p, off), rel_add(off, p), N.le_add_right(1n+off, p))))
371
372# the member at relative index k is there exactly when bit k is set
373def members_pt(+xs: List<&2, Bool>, +k: Nat, +off: Nat) -> {S.nmem(Nat.add(k, off), S.members(xs, off)) == S.inset(xs, k) : Bool}:
374 match xs k:
375 case Nil{} _:
376 {==}
377 case Con{False{}, +t} 0n:
378 %Equal.sym(Nat, Nat.add(0n, off), off, zero_add(off)) : {S.nmem(_, S.members(t, 1n+off)) == False{} : Bool}
379 members_above(t, 1n+off, off, N.lt_succ(off))
380 case Con{True{}, +t} 0n:
381 %Equal.sym(Nat, Nat.add(0n, off), off, zero_add(off)) : {Bool.or(Nat.is_eq(off, _), S.nmem(_, S.members(t, 1n+off))) == True{} : Bool}
382 %Equal.sym(Bool, Nat.is_eq(off, off), True{}, N.is_eq_refl(off)) : {Bool.or(_, S.nmem(off, S.members(t, 1n+off))) == True{} : Bool}
383 {==}
384 case Con{False{}, +t} 1n+ +p:
385 %Equal.sym(Nat, Nat.add(1n+p, off), Nat.add(p, 1n+off), succ_add(p, off)) : {S.nmem(_, S.members(t, 1n+off)) == S.inset(t, p) : Bool}
386 members_pt(t, p, 1n+off)
387 case Con{True{}, +t} 1n+ +p:
388 %Equal.sym(Bool, Nat.is_eq(off, Nat.add(1n+p, off)), False{}, ne_add_succ(off, p)) : {Bool.or(_, S.nmem(Nat.add(1n+p, off), S.members(t, 1n+off))) == S.inset(t, p) : Bool}
389 %Equal.sym(Nat, Nat.add(1n+p, off), Nat.add(p, 1n+off), succ_add(p, off)) : {Bool.or(False{}, S.nmem(_, S.members(t, 1n+off))) == S.inset(t, p) : Bool}
390 members_pt(t, p, 1n+off)
391
392def elements_contains(+xs: List<&2, Bool>, +k: Nat) -> S.Elements.elements_contains(xs, k):
393 %N.add_zero(k) : {S.nmem(_, S.members(xs, 0n)) == S.inset(xs, k) : Bool}
394 members_pt(xs, k, 0n)
395
396# as many elements as members (SPARK: Length (Elements) = Length (Container))
397def elements_length(+xs: List<&2, Bool>, +off: Nat) -> S.Elements.elements_length(xs, off):
398 match xs:
399 case Nil{}:
400 {==}
401 case Con{False{}, +t}:
402 elements_length(t, 1n+off)
403 case Con{True{}, +t}:
404 N.succ_cong(SC.length(Nat, S.members(t, 1n+off)), S.count(t), elements_length(t, 1n+off))