proofs/containers/dynamic_array/clear.bend
bend-collections-laws-containers@1.0.0.0 · 70 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/proofs/lib/array.bend as AR
6import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
7import bend-collections-laws-containers@1.0.0.0/src/containers/dynamic_array.bend as DA
8import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/layout.bend as LY
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/state.bend as ST
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/steps.bend as SP
11import bend-collections-laws-containers@1.0.0.0/proofs/lib/array_ext.bend as AX
12
13# The executable clear (src/dynamic_array.bend clear_at) resets the occupied
14# slots [0, n) to None, top down, in the block it already has; the parametric
15# clear allocates a fresh all-None block of the same depth. On a good state
16# the two agree: each reset is the in-place write pop makes (and keeps the
17# layout good with one fewer element), and a good layout of length 0 is the
18# all-None tree itself.
19
20# A list of Nones is the replication of None to its length.
21def nones_rep_eq(-T: Data, +xs: List<&2, Maybe<&2, T>>, +h: {LY.nones(T, xs) == True{} : Bool}) -> {xs == SC.replicate(Maybe<&2, T>, SC.length(Maybe<&2, T>, xs), None{}) : List<&2, Maybe<&2, T>>}:
22 match xs:
23 case Nil{}:
24 {==}
25 case Con{None{}, +r}:
26 LL.cons_cong(Maybe<&2, T>, None{}, r, SC.replicate(Maybe<&2, T>, SC.length(Maybe<&2, T>, r), None{}), nones_rep_eq(T, r, h))
27 case Con{Some{x}, r}:
28 Empty.absurd({Con{Some{x}, r} == SC.replicate(Maybe<&2, T>, SC.length(Maybe<&2, T>, Con{Some{x}, r}), None{}) : List<&2, Maybe<&2, T>>}, L.false_true(h))
29
30# A layout of length 0 holds only Nones.
31def lay0_nones(-T: Data, +xs: List<&2, Maybe<&2, T>>, +h: {LY.lay(T, xs, 0n) == True{} : Bool}) -> {LY.nones(T, xs) == True{} : Bool}:
32 match xs:
33 case Nil{}:
34 {==}
35 case Con{None{}, r}:
36 h
37 case Con{Some{x}, r}:
38 Empty.absurd({LY.nones(T, Con{Some{x}, r}) == True{} : Bool}, L.false_true(h))
39
40# The slots of a good empty shadow are those of the all-None tree.
41def empty_slots_eq(-T: Data, +d: Nat, +t: AR.Tree<Maybe<&2, T>>, +pf: {AR.perfect(Maybe<&2, T>, d, t) == True{} : Bool}, +h: {LY.lay(T, AR.slots(Maybe<&2, T>, t), 0n) == True{} : Bool}) -> {AR.slots(Maybe<&2, T>, t) == AR.slots(Maybe<&2, T>, AR.trep(Maybe<&2, T>, d, None{})) : List<&2, Maybe<&2, T>>}:
42 +ss = AR.slots(Maybe<&2, T>, t)
43 %Equal.sym(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, AR.trep(Maybe<&2, T>, d, None{})), SC.replicate(Maybe<&2, T>, SC.pow2(d), None{}), AR.trep_slots(Maybe<&2, T>, d, None{})) : {ss == _ : List<&2, Maybe<&2, T>>}
44 %AR.slots_length(Maybe<&2, T>, d, t, pf) : {ss == SC.replicate(Maybe<&2, T>, _, None{}) : List<&2, Maybe<&2, T>>}
45 nones_rep_eq(T, ss, lay0_nones(T, ss, h))
46
47# Resetting the k occupied slots of a good shadow gives the all-None block.
48def clear_go_eq(~T: Data, +l: Nat, +d: Nat, +k: Nat, +t: AR.Tree<Maybe<&2, T>>, +g: {ST.good(T, ST.Sh{l, d, k, t}) == True{} : Bool}) -> {DA.clear_go_at(~T, k, AR.thaw(Maybe<&2, T>, t)) == DA.empty_slots(T, d) : Array<Maybe<&2, T>>}:
49 match k:
50 case 0n:
51 +pf = ST.g_perfect(T, l, d, 0n, t, g)
52 +te = AX.tree_ext(Maybe<&2, T>, d, t, AR.trep(Maybe<&2, T>, d, None{}), pf, AR.trep_perfect(Maybe<&2, T>, d, None{}), empty_slots_eq(T, d, t, pf, ST.g_lay(T, l, d, 0n, t, g)))
53 %Equal.sym(Array<Maybe<&2, T>>, DA.empty_slots(T, d), AR.thaw(Maybe<&2, T>, AR.trep(Maybe<&2, T>, d, None{})), ST.empty_eq(T, d)) : {AR.thaw(Maybe<&2, T>, t) == _ : Array<Maybe<&2, T>>}
54 %te : {AR.thaw(Maybe<&2, T>, t) == AR.thaw(Maybe<&2, T>, _) : Array<Maybe<&2, T>>}
55 {==}
56 case 1n+ +m:
57 +ss = AR.slots(Maybe<&2, T>, t)
58 +x = SC.nth(T, LY.somes(T, ss), m)
59 +hlay = ST.g_lay(T, l, d, 1n+m, t, g)
60 +hm = N.lt_succ(m)
61 +hi = N.lt_le_trans(m, 1n+m, SC.pow2(d), hm, SP.n_le_cap(T, l, d, 1n+m, t, g))
62 +t2 = AR.upd(Maybe<&2, T>, d, t, m, None{})
63 +hs = SP.upd_slots(T, l, d, 1n+m, t, m, None{}, g, hi)
64 +g2 = ST.good_intro(T, l, d, m, t2, ST.g_limit(T, l, d, 1n+m, t, g), ST.g_depth(T, l, d, 1n+m, t, g), AR.upd_perfect(Maybe<&2, T>, d, t, m, None{}, ST.g_perfect(T, l, d, 1n+m, t, g)),
65 L.subst(List<&2, Maybe<&2, T>>, ys => {LY.lay(T, ys, m) == True{} : Bool}, SC.update(Maybe<&2, T>, ss, m, None{}), AR.slots(Maybe<&2, T>, t2), Equal.sym(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, t2), SC.update(Maybe<&2, T>, ss, m, None{}), hs), LY.lay_pop(T, ss, m, hlay)))
66 %Equal.sym(Array<Maybe<&2, T>> & Maybe<&2, T>, Array.swap(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, t), U32.from_nat(m), None{}), (AR.thaw(Maybe<&2, T>, t2), x), SP.swap_arr(T, l, d, 1n+m, t, m, None{}, x, g, hi, LY.lay_nth(T, ss, 1n+m, m, hlay, hm))) : {DA.clear_go_at(~T, m, Array.set.fin(Maybe<&2, T>, _)) == DA.empty_slots(T, d) : Array<Maybe<&2, T>>}
67 clear_go_eq(~T, l, d, m, t2, g2)
68
69def clear_eq(~T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +g: {ST.good(T, ST.Sh{l, d, n, t}) == True{} : Bool}) -> {DA.clear_at(~T, ST.real(T, ST.Sh{l, d, n, t})) == DA.clear(T, ST.real(T, ST.Sh{l, d, n, t})) : DA.DynArray<&2, T>}:
70 Equal.cong(Array<Maybe<&2, T>>, DA.DynArray<&2, T>, z => DA.DA{l, d, SC.pow2(d), 0n, z}, DA.clear_go_at(~T, n, AR.thaw(Maybe<&2, T>, t)), DA.empty_slots(T, d), clear_go_eq(~T, l, d, n, t, g))