proofs/containers/dynamic_array/steps.bend
bend-collections-laws-containers@1.0.0.0 · 341 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/u32.bend as U
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/array.bend as AR
7import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
8import bend-collections-laws-containers@1.0.0.0/spec/containers/dynamic_array.bend as S
9import bend-collections-laws-containers@1.0.0.0/src/containers/dynamic_array.bend as DA
10import bend-collections-laws-containers@1.0.0.0/src/containers/types/dynamic_array.bend as E
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/layout.bend as LY
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/state.bend as ST
13import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/growth.bend as GR
14import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/walk.bend as W
15
16# One actual public operation on a good shadow's array yields the array of a
17# new good shadow, and (abstract state, observation) equals the spec step.
18def StepOK(-T: Data, sh: ST.Shadow<T>, op: E.Op<T>) -> Type:
19 Sigma<&1, &1, ST.Shadow<T>, sh2 => Sigma<&1, &1, E.Obs<T>, o => {DA.step(T, ST.real(T, sh), op) == (ST.real(T, sh2), o) : DA.DynArray<&2, T> & E.Obs<T>} & ({ST.good(T, sh2) == True{} : Bool} & {(ST.model(T, sh2), o) == S.step(T, ST.model(T, sh), op) : S.Model<T> & E.Obs<T>})>>
20
21def length_ok(-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}) -> StepOK(T, ST.Sh{l, d, n, t}, E.Length{}):
22 +xs = LY.somes(T, AR.slots(Maybe<&2, T>, t))
23 (ST.Sh{l, d, n, t}, (E.ONat{n}, ({==}, (g,
24 %Equal.sym(Nat, SC.length(T, xs), n, LY.lay_len(T, AR.slots(Maybe<&2, T>, t), n, ST.g_lay(T, l, d, n, t, g))) : {(S.M{l, d, xs}, E.ONat{n}) == (S.M{l, d, xs}, E.ONat{_}) : S.Model<T> & E.Obs<T>}
25 {==}))))
26
27def capacity_ok(-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}) -> StepOK(T, ST.Sh{l, d, n, t}, E.Capacity{}):
28 +xs = LY.somes(T, AR.slots(Maybe<&2, T>, t))
29 (ST.Sh{l, d, n, t}, (E.ONat{SC.pow2(d)}, ({==}, (g,
30 {==}))))
31
32# ---- facts shared by indexed operations ----
33
34def n_le_cap(-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}) -> {Nat.is_le(n, SC.pow2(d)) == True{} : Bool}:
35 L.subst(Nat, k => {Nat.is_le(n, k) == True{} : Bool}, SC.length(Maybe<&2, T>, AR.slots(Maybe<&2, T>, t)), SC.pow2(d), AR.slots_length(Maybe<&2, T>, d, t, ST.g_perfect(T, l, d, n, t, g)), LY.lay_le(T, AR.slots(Maybe<&2, T>, t), n, ST.g_lay(T, l, d, n, t, g)))
36
37def idx_lt(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +i: Nat, +g: {ST.good(T, ST.Sh{l, d, n, t}) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}) -> {Nat.is_lt(U32.to_nat(U32.from_nat(i)), SC.pow2(d)) == True{} : Bool}:
38 L.subst(Nat, k => {Nat.is_lt(k, SC.pow2(d)) == True{} : Bool}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, U.to_nat_from_nat(i, d, ST.le32(d, l, ST.g_depth(T, l, d, n, t, g), ST.g_limit(T, l, d, n, t, g)), hi)), hi)
39
40def idx_slot(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +i: Nat, +x: Maybe<&2, T>, +g: {ST.good(T, ST.Sh{l, d, n, t}) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +hx: {SC.nth(Maybe<&2, T>, AR.slots(Maybe<&2, T>, t), i) == Some{x} : Maybe<&2, Maybe<&2, T>>}) -> {SC.nth(Maybe<&2, T>, AR.slots(Maybe<&2, T>, t), U32.to_nat(U32.from_nat(i))) == Some{x} : Maybe<&2, Maybe<&2, T>>}:
41 L.subst(Nat, k => {SC.nth(Maybe<&2, T>, AR.slots(Maybe<&2, T>, t), k) == Some{x} : Maybe<&2, Maybe<&2, T>>}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, U.to_nat_from_nat(i, d, ST.le32(d, l, ST.g_depth(T, l, d, n, t, g), ST.g_limit(T, l, d, n, t, g)), hi)), hx)
42
43# ---- get ----
44
45def get_case(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +i: Nat, +g: {ST.good(T, ST.Sh{l, d, n, t}) == True{} : Bool}, +b: Bool, +eb: {Nat.is_lt(i, n) == b : Bool}) -> StepOK(T, ST.Sh{l, d, n, t}, E.Get{i}):
46 match b:
47 case True{}:
48 +ss = AR.slots(Maybe<&2, T>, t)
49 +xs = LY.somes(T, ss)
50 +x = SC.nth(T, xs, i)
51 +hi = N.lt_le_trans(i, n, SC.pow2(d), eb, n_le_cap(T, l, d, n, t, g))
52 (ST.Sh{l, d, n, t}, (E.OItem{S.item_result(T, x)}, (
53 %Equal.sym(Bool, Nat.is_lt(i, n), True{}, eb) : {DA.obs_item(T, DA.get_checked(T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), i, _)) == (ST.real(T, ST.Sh{l, d, n, t}), E.OItem{S.item_result(T, x)}) : DA.DynArray<&2, T> & E.Obs<T>}
54 %Equal.sym(Array<Maybe<&2, T>> & Maybe<&2, T>, Array.get(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, t), U32.from_nat(i)), (AR.thaw(Maybe<&2, T>, t), x), AR.get(Maybe<&2, T>, d, t, U32.from_nat(i), x, ST.lt32(d, l, ST.g_depth(T, l, d, n, t, g), ST.g_limit(T, l, d, n, t, g)), idx_lt(T, l, d, n, t, i, g, hi), idx_slot(T, l, d, n, t, i, x, g, hi, LY.lay_nth(T, ss, n, i, ST.g_lay(T, l, d, n, t, g), eb)), ST.g_perfect(T, l, d, n, t, g))) : {DA.obs_item(T, DA.get_found(T, l, d, SC.pow2(d), n, _)) == (ST.real(T, ST.Sh{l, d, n, t}), E.OItem{S.item_result(T, x)}) : DA.DynArray<&2, T> & E.Obs<T>}
55 %Equal.sym(Result<&2, &2, E.Error, T>, DA.slot_result(T, x), S.item_result(T, x), ST.slot_item(T, x)) : {(DA.DA{l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t)}, E.OItem{_}) == (ST.real(T, ST.Sh{l, d, n, t}), E.OItem{S.item_result(T, x)}) : DA.DynArray<&2, T> & E.Obs<T>}
56 {==}, (g, {==}))))
57 case False{}:
58 +ss = AR.slots(Maybe<&2, T>, t)
59 +xs = LY.somes(T, ss)
60 (ST.Sh{l, d, n, t}, (E.OItem{Fail{E.IndexOutOfRange{}}}, (
61 %Equal.sym(Bool, Nat.is_lt(i, n), False{}, eb) : {DA.obs_item(T, DA.get_checked(T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), i, _)) == (ST.real(T, ST.Sh{l, d, n, t}), E.OItem{Fail{E.IndexOutOfRange{}}}) : DA.DynArray<&2, T> & E.Obs<T>}
62 {==}, (g,
63 %Equal.sym(Maybe<&2, T>, SC.nth(T, xs, i), None{}, LL.nth_none(T, xs, i, L.subst(Nat, k => {Nat.is_le(k, i) == True{} : Bool}, n, SC.length(T, xs), Equal.sym(Nat, SC.length(T, xs), n, LY.lay_len(T, ss, n, ST.g_lay(T, l, d, n, t, g))), N.not_lt_le(i, n, eb)))) : {(S.M{l, d, xs}, E.OItem{Fail{E.IndexOutOfRange{}}}) == (S.M{l, d, xs}, E.OItem{S.item_result(T, _)}) : S.Model<T> & E.Obs<T>}
64 {==}))))
65
66def get_ok(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +i: Nat, +g: {ST.good(T, ST.Sh{l, d, n, t}) == True{} : Bool}) -> StepOK(T, ST.Sh{l, d, n, t}, E.Get{i}):
67 get_case(T, l, d, n, t, i, g, Nat.is_lt(i, n), {==})
68
69# ---- writes through Base.Array.set / swap at a checked Nat index ----
70
71def set_arr(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +i: Nat, +w: Maybe<&2, T>, +x: Maybe<&2, T>, +g: {ST.good(T, ST.Sh{l, d, n, t}) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +hx: {SC.nth(Maybe<&2, T>, AR.slots(Maybe<&2, T>, t), i) == Some{x} : Maybe<&2, Maybe<&2, T>>}) -> {Array.set(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, t), U32.from_nat(i), w) == AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, t, i, w)) : Array<Maybe<&2, T>>}:
72 L.subst(Nat, k => {Array.set(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, t), U32.from_nat(i), w) == AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, t, k, w)) : Array<Maybe<&2, T>>}, U32.to_nat(U32.from_nat(i)), i, U.to_nat_from_nat(i, d, ST.le32(d, l, ST.g_depth(T, l, d, n, t, g), ST.g_limit(T, l, d, n, t, g)), hi),
73 AR.set(Maybe<&2, T>, d, t, U32.from_nat(i), w, x, ST.lt32(d, l, ST.g_depth(T, l, d, n, t, g), ST.g_limit(T, l, d, n, t, g)), idx_lt(T, l, d, n, t, i, g, hi), idx_slot(T, l, d, n, t, i, x, g, hi, hx), ST.g_perfect(T, l, d, n, t, g)))
74
75def swap_arr(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +i: Nat, +w: Maybe<&2, T>, +x: Maybe<&2, T>, +g: {ST.good(T, ST.Sh{l, d, n, t}) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +hx: {SC.nth(Maybe<&2, T>, AR.slots(Maybe<&2, T>, t), i) == Some{x} : Maybe<&2, Maybe<&2, T>>}) -> {Array.swap(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, t), U32.from_nat(i), w) == (AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, t, i, w)), x) : Array<Maybe<&2, T>> & Maybe<&2, T>}:
76 L.subst(Nat, k => {Array.swap(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, t), U32.from_nat(i), w) == (AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, t, k, w)), x) : Array<Maybe<&2, T>> & Maybe<&2, T>}, U32.to_nat(U32.from_nat(i)), i, U.to_nat_from_nat(i, d, ST.le32(d, l, ST.g_depth(T, l, d, n, t, g), ST.g_limit(T, l, d, n, t, g)), hi),
77 AR.swap(Maybe<&2, T>, d, t, U32.from_nat(i), w, x, ST.lt32(d, l, ST.g_depth(T, l, d, n, t, g), ST.g_limit(T, l, d, n, t, g)), idx_lt(T, l, d, n, t, i, g, hi), idx_slot(T, l, d, n, t, i, x, g, hi, hx), ST.g_perfect(T, l, d, n, t, g)))
78
79# slots of an updated tree (index below the capacity).
80def upd_slots(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +i: Nat, +w: Maybe<&2, T>, +g: {ST.good(T, ST.Sh{l, d, n, t}) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}) -> {AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, t, i, w)) == SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, t), i, w) : List<&2, Maybe<&2, T>>}:
81 AR.upd_slots(Maybe<&2, T>, d, t, i, w, hi, ST.g_perfect(T, l, d, n, t, g))
82
83# ---- set ----
84
85def set_case(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +i: Nat, +v: T, +g: {ST.good(T, ST.Sh{l, d, n, t}) == True{} : Bool}, +b: Bool, +eb: {Nat.is_lt(i, n) == b : Bool}) -> StepOK(T, ST.Sh{l, d, n, t}, E.Set{i, v}):
86 match b:
87 case True{}:
88 +ss = AR.slots(Maybe<&2, T>, t)
89 +xs = LY.somes(T, ss)
90 +hi = N.lt_le_trans(i, n, SC.pow2(d), eb, n_le_cap(T, l, d, n, t, g))
91 +t2 = AR.upd(Maybe<&2, T>, d, t, i, Some{v})
92 +hs = upd_slots(T, l, d, n, t, i, Some{v}, g, hi)
93 +hlay = ST.g_lay(T, l, d, n, t, g)
94 +hlen = LY.lay_len(T, ss, n, hlay)
95 (ST.Sh{l, d, n, t2}, (E.OUnit{Done{Unit{}}}, (
96 %Equal.sym(Bool, Nat.is_lt(i, n), True{}, eb) : {DA.obs_unit(T, DA.set_checked(T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), i, v, _)) == (ST.real(T, ST.Sh{l, d, n, t2}), E.OUnit{Done{Unit{}}}) : DA.DynArray<&2, T> & E.Obs<T>}
97 %Equal.sym(Array<Maybe<&2, T>>, Array.set(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, t), U32.from_nat(i), Some{v}), AR.thaw(Maybe<&2, T>, t2), set_arr(T, l, d, n, t, i, Some{v}, SC.nth(T, xs, i), g, hi, LY.lay_nth(T, ss, n, i, hlay, eb))) : {(DA.DA{l, d, SC.pow2(d), n, _}, E.OUnit{Done{Unit{}}}) == (ST.real(T, ST.Sh{l, d, n, t2}), E.OUnit{Done{Unit{}}}) : DA.DynArray<&2, T> & E.Obs<T>}
98 {==},
99 (ST.good_intro(T, l, d, n, t2, ST.g_limit(T, l, d, n, t, g), ST.g_depth(T, l, d, n, t, g), AR.upd_perfect(Maybe<&2, T>, d, t, i, Some{v}, ST.g_perfect(T, l, d, n, t, g)),
100 L.subst(List<&2, Maybe<&2, T>>, ys => {LY.lay(T, ys, n) == True{} : Bool}, SC.update(Maybe<&2, T>, ss, i, Some{v}), 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, i, Some{v}), hs), LY.lay_set(T, ss, n, i, v, hlay, eb))),
101 %Equal.sym(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, t2), SC.update(Maybe<&2, T>, ss, i, Some{v}), hs) : {(S.M{l, d, LY.somes(T, _)}, E.OUnit{Done{Unit{}}}) == S.step(T, S.M{l, d, xs}, E.Set{i, v}) : S.Model<T> & E.Obs<T>}
102 %Equal.sym(List<&2, T>, LY.somes(T, SC.update(Maybe<&2, T>, ss, i, Some{v})), SC.update(T, xs, i, v), LY.somes_set(T, ss, n, i, v, hlay, eb)) : {(S.M{l, d, _}, E.OUnit{Done{Unit{}}}) == S.step(T, S.M{l, d, xs}, E.Set{i, v}) : S.Model<T> & E.Obs<T>}
103 %Equal.sym(Nat, SC.length(T, xs), n, hlen) : {(S.M{l, d, SC.update(T, xs, i, v)}, E.OUnit{Done{Unit{}}}) == Bool.pick(S.Model<T> & E.Obs<T>, Nat.is_lt(i, _), (S.M{l, d, SC.update(T, xs, i, v)}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.IndexOutOfRange{}}})) : S.Model<T> & E.Obs<T>}
104 %Equal.sym(Bool, Nat.is_lt(i, n), True{}, eb) : {(S.M{l, d, SC.update(T, xs, i, v)}, E.OUnit{Done{Unit{}}}) == Bool.pick(S.Model<T> & E.Obs<T>, _, (S.M{l, d, SC.update(T, xs, i, v)}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.IndexOutOfRange{}}})) : S.Model<T> & E.Obs<T>}
105 {==}))))
106 case False{}:
107 +ss = AR.slots(Maybe<&2, T>, t)
108 +xs = LY.somes(T, ss)
109 +hlen = LY.lay_len(T, ss, n, ST.g_lay(T, l, d, n, t, g))
110 (ST.Sh{l, d, n, t}, (E.OUnit{Fail{E.IndexOutOfRange{}}}, (
111 %Equal.sym(Bool, Nat.is_lt(i, n), False{}, eb) : {DA.obs_unit(T, DA.set_checked(T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), i, v, _)) == (ST.real(T, ST.Sh{l, d, n, t}), E.OUnit{Fail{E.IndexOutOfRange{}}}) : DA.DynArray<&2, T> & E.Obs<T>}
112 {==},
113 (g,
114 %Equal.sym(Nat, SC.length(T, xs), n, hlen) : {(S.M{l, d, xs}, E.OUnit{Fail{E.IndexOutOfRange{}}}) == Bool.pick(S.Model<T> & E.Obs<T>, Nat.is_lt(i, _), (S.M{l, d, SC.update(T, xs, i, v)}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.IndexOutOfRange{}}})) : S.Model<T> & E.Obs<T>}
115 %Equal.sym(Bool, Nat.is_lt(i, n), False{}, eb) : {(S.M{l, d, xs}, E.OUnit{Fail{E.IndexOutOfRange{}}}) == Bool.pick(S.Model<T> & E.Obs<T>, _, (S.M{l, d, SC.update(T, xs, i, v)}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.IndexOutOfRange{}}})) : S.Model<T> & E.Obs<T>}
116 {==}))))
117
118def set_ok(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +i: Nat, +v: T, +g: {ST.good(T, ST.Sh{l, d, n, t}) == True{} : Bool}) -> StepOK(T, ST.Sh{l, d, n, t}, E.Set{i, v}):
119 set_case(T, l, d, n, t, i, v, g, Nat.is_lt(i, n), {==})
120
121# ---- push ----
122
123def len_slots(-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}, +hn: {Nat.is_lt(n, SC.pow2(d)) == True{} : Bool}) -> {Nat.is_lt(n, SC.length(Maybe<&2, T>, AR.slots(Maybe<&2, T>, t))) == True{} : Bool}:
124 L.subst(Nat, k => {Nat.is_lt(n, k) == True{} : Bool}, SC.pow2(d), SC.length(Maybe<&2, T>, AR.slots(Maybe<&2, T>, t)), Equal.sym(Nat, SC.length(Maybe<&2, T>, AR.slots(Maybe<&2, T>, t)), SC.pow2(d), AR.slots_length(Maybe<&2, T>, d, t, ST.g_perfect(T, l, d, n, t, g))), hn)
125
126def pi_arr(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +v: T, +g: {ST.good(T, ST.Sh{l, d, n, t}) == True{} : Bool}, +hn: {Nat.is_lt(n, SC.pow2(d)) == True{} : Bool}) -> {Array.set(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, t), U32.from_nat(n), Some{v}) == AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, t, n, Some{v})) : Array<Maybe<&2, T>>}:
127 set_arr(T, l, d, n, t, n, Some{v}, None{}, g, hn, LY.push_free(T, AR.slots(Maybe<&2, T>, t), n, ST.g_lay(T, l, d, n, t, g), len_slots(T, l, d, n, t, g, hn)))
128
129def pi_good(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +v: T, +g: {ST.good(T, ST.Sh{l, d, n, t}) == True{} : Bool}, +hn: {Nat.is_lt(n, SC.pow2(d)) == True{} : Bool}) -> {ST.good(T, ST.Sh{l, d, 1n+n, AR.upd(Maybe<&2, T>, d, t, n, Some{v})}) == True{} : Bool}:
130 +ss = AR.slots(Maybe<&2, T>, t)
131 +t2 = AR.upd(Maybe<&2, T>, d, t, n, Some{v})
132 ST.good_intro(T, l, d, 1n+n, t2, ST.g_limit(T, l, d, n, t, g), ST.g_depth(T, l, d, n, t, g), AR.upd_perfect(Maybe<&2, T>, d, t, n, Some{v}, ST.g_perfect(T, l, d, n, t, g)),
133 L.subst(List<&2, Maybe<&2, T>>, ys => {LY.lay(T, ys, 1n+n) == True{} : Bool}, SC.update(Maybe<&2, T>, ss, n, Some{v}), 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, n, Some{v}), upd_slots(T, l, d, n, t, n, Some{v}, g, hn)), LY.lay_push(T, ss, n, v, ST.g_lay(T, l, d, n, t, g), len_slots(T, l, d, n, t, g, hn))))
134
135def pi_model(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +v: T, +g: {ST.good(T, ST.Sh{l, d, n, t}) == True{} : Bool}, +hn: {Nat.is_lt(n, SC.pow2(d)) == True{} : Bool}) -> {LY.somes(T, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, t, n, Some{v}))) == SC.snoc(T, LY.somes(T, AR.slots(Maybe<&2, T>, t)), v) : List<&2, T>}:
136 +ss = AR.slots(Maybe<&2, T>, t)
137 Equal.trans(List<&2, T>, LY.somes(T, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, t, n, Some{v}))), LY.somes(T, SC.update(Maybe<&2, T>, ss, n, Some{v})), SC.snoc(T, LY.somes(T, ss), v),
138 Equal.cong(List<&2, Maybe<&2, T>>, List<&2, T>, ys => LY.somes(T, ys), AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, t, n, Some{v})), SC.update(Maybe<&2, T>, ss, n, Some{v}), upd_slots(T, l, d, n, t, n, Some{v}, g, hn)),
139 LY.somes_push(T, ss, n, v, ST.g_lay(T, l, d, n, t, g), len_slots(T, l, d, n, t, g, hn)))
140
141def room_nat(+n: Nat, +d: Nat, +b: Bool, +e: {Nat.is_lt(n, SC.pow2(d)) == b : Bool}) -> {Nat.is_lt(n, SC.pow2(d)) == b : Bool}:
142 e
143
144def push_case(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +v: T, +g: {ST.good(T, ST.Sh{l, d, n, t}) == True{} : Bool}, +room: Bool, +er: {Nat.is_lt(n, SC.pow2(d)) == room : Bool}, +grow: Bool, +eg: {Nat.is_lt(d, l) == grow : Bool}) -> StepOK(T, ST.Sh{l, d, n, t}, E.Push{v}):
145 match room grow:
146 case True{} _:
147 +xs = LY.somes(T, AR.slots(Maybe<&2, T>, t))
148 +hn = room_nat(n, d, True{}, er)
149 +t2 = AR.upd(Maybe<&2, T>, d, t, n, Some{v})
150 (ST.Sh{l, d, 1n+n, t2}, (E.OUnit{Done{Unit{}}}, (
151 %Equal.sym(Bool, Nat.is_lt(n, SC.pow2(d)), True{}, er) : {DA.obs_unit(T, DA.push_room(T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), v, _, Nat.is_lt(d, l))) == (ST.real(T, ST.Sh{l, d, 1n+n, t2}), E.OUnit{Done{Unit{}}}) : DA.DynArray<&2, T> & E.Obs<T>}
152 %Equal.sym(Array<Maybe<&2, T>>, Array.set(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, t), U32.from_nat(n), Some{v}), AR.thaw(Maybe<&2, T>, t2), pi_arr(T, l, d, n, t, v, g, hn)) : {(DA.DA{l, d, SC.pow2(d), 1n+n, _}, E.OUnit{Done{Unit{}}}) == (ST.real(T, ST.Sh{l, d, 1n+n, t2}), E.OUnit{Done{Unit{}}}) : DA.DynArray<&2, T> & E.Obs<T>}
153 {==},
154 (pi_good(T, l, d, n, t, v, g, hn),
155 %Equal.sym(List<&2, T>, LY.somes(T, AR.slots(Maybe<&2, T>, t2)), SC.snoc(T, xs, v), pi_model(T, l, d, n, t, v, g, hn)) : {(S.M{l, d, _}, E.OUnit{Done{Unit{}}}) == S.step(T, S.M{l, d, xs}, E.Push{v}) : S.Model<T> & E.Obs<T>}
156 %Equal.sym(Nat, SC.length(T, xs), n, LY.lay_len(T, AR.slots(Maybe<&2, T>, t), n, ST.g_lay(T, l, d, n, t, g))) : {(S.M{l, d, SC.snoc(T, xs, v)}, E.OUnit{Done{Unit{}}}) == Bool.pick(S.Model<T> & E.Obs<T>, Nat.is_lt(_, SC.pow2(d)), (S.M{l, d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), Bool.pick(S.Model<T> & E.Obs<T>, Nat.is_lt(d, l), (S.M{l, 1n+d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}))) : S.Model<T> & E.Obs<T>}
157 %Equal.sym(Bool, Nat.is_lt(n, SC.pow2(d)), True{}, hn) : {(S.M{l, d, SC.snoc(T, xs, v)}, E.OUnit{Done{Unit{}}}) == Bool.pick(S.Model<T> & E.Obs<T>, _, (S.M{l, d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), Bool.pick(S.Model<T> & E.Obs<T>, Nat.is_lt(d, l), (S.M{l, 1n+d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}))) : S.Model<T> & E.Obs<T>}
158 {==}))))
159 case False{} True{}:
160 +xs = LY.somes(T, AR.slots(Maybe<&2, T>, t))
161 +nf = room_nat(n, d, False{}, er)
162 +t1 = {AR.TNode{t, AR.trep(Maybe<&2, T>, d, None{})} : AR.Tree<Maybe<&2, T>>}
163 +g1 = GR.grow_good(T, l, d, n, t, g, eg)
164 +hn = N.le_lt_trans(n, SC.pow2(d), SC.pow2(1n+d), n_le_cap(T, l, d, n, t, g), N.pow2_lt_succ(d))
165 +t2 = AR.upd(Maybe<&2, T>, 1n+d, t1, n, Some{v})
166 (ST.Sh{l, 1n+d, 1n+n, t2}, (E.OUnit{Done{Unit{}}}, (
167 %Equal.sym(Bool, Nat.is_lt(n, SC.pow2(d)), False{}, er) : {DA.obs_unit(T, DA.push_room(T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), v, _, Nat.is_lt(d, l))) == (ST.real(T, ST.Sh{l, 1n+d, 1n+n, t2}), E.OUnit{Done{Unit{}}}) : DA.DynArray<&2, T> & E.Obs<T>}
168 %Equal.sym(Bool, Nat.is_lt(d, l), True{}, eg) : {DA.obs_unit(T, DA.push_room(T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), v, False{}, _)) == (ST.real(T, ST.Sh{l, 1n+d, 1n+n, t2}), E.OUnit{Done{Unit{}}}) : DA.DynArray<&2, T> & E.Obs<T>}
169 %Equal.sym(Array<Maybe<&2, T>>, DA.grown(T, d, AR.thaw(Maybe<&2, T>, t)), AR.thaw(Maybe<&2, T>, t1), ST.grown_eq(T, d, t)) : {(DA.DA{l, 1n+d, Nat.double(SC.pow2(d)), 1n+n, Array.set(Maybe<&2, T>, _, U32.from_nat(n), Some{v})}, E.OUnit{Done{Unit{}}}) == (ST.real(T, ST.Sh{l, 1n+d, 1n+n, t2}), E.OUnit{Done{Unit{}}}) : DA.DynArray<&2, T> & E.Obs<T>}
170 %Equal.sym(Array<Maybe<&2, T>>, Array.set(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, t1), U32.from_nat(n), Some{v}), AR.thaw(Maybe<&2, T>, t2), pi_arr(T, l, 1n+d, n, t1, v, g1, hn)) : {(DA.DA{l, 1n+d, Nat.double(SC.pow2(d)), 1n+n, _}, E.OUnit{Done{Unit{}}}) == (ST.real(T, ST.Sh{l, 1n+d, 1n+n, t2}), E.OUnit{Done{Unit{}}}) : DA.DynArray<&2, T> & E.Obs<T>}
171 {==},
172 (pi_good(T, l, 1n+d, n, t1, v, g1, hn),
173 %Equal.sym(List<&2, T>, LY.somes(T, AR.slots(Maybe<&2, T>, t2)), SC.snoc(T, LY.somes(T, AR.slots(Maybe<&2, T>, t1)), v), pi_model(T, l, 1n+d, n, t1, v, g1, hn)) : {(S.M{l, 1n+d, _}, E.OUnit{Done{Unit{}}}) == S.step(T, S.M{l, d, xs}, E.Push{v}) : S.Model<T> & E.Obs<T>}
174 %Equal.sym(List<&2, T>, LY.somes(T, AR.slots(Maybe<&2, T>, t1)), xs, GR.grow_model(T, d, t)) : {(S.M{l, 1n+d, SC.snoc(T, _, v)}, E.OUnit{Done{Unit{}}}) == S.step(T, S.M{l, d, xs}, E.Push{v}) : S.Model<T> & E.Obs<T>}
175 %Equal.sym(Nat, SC.length(T, xs), n, LY.lay_len(T, AR.slots(Maybe<&2, T>, t), n, ST.g_lay(T, l, d, n, t, g))) : {(S.M{l, 1n+d, SC.snoc(T, xs, v)}, E.OUnit{Done{Unit{}}}) == Bool.pick(S.Model<T> & E.Obs<T>, Nat.is_lt(_, SC.pow2(d)), (S.M{l, d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), Bool.pick(S.Model<T> & E.Obs<T>, Nat.is_lt(d, l), (S.M{l, 1n+d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}))) : S.Model<T> & E.Obs<T>}
176 %Equal.sym(Bool, Nat.is_lt(n, SC.pow2(d)), False{}, nf) : {(S.M{l, 1n+d, SC.snoc(T, xs, v)}, E.OUnit{Done{Unit{}}}) == Bool.pick(S.Model<T> & E.Obs<T>, _, (S.M{l, d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), Bool.pick(S.Model<T> & E.Obs<T>, Nat.is_lt(d, l), (S.M{l, 1n+d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}))) : S.Model<T> & E.Obs<T>}
177 %Equal.sym(Bool, Nat.is_lt(d, l), True{}, eg) : {(S.M{l, 1n+d, SC.snoc(T, xs, v)}, E.OUnit{Done{Unit{}}}) == Bool.pick(S.Model<T> & E.Obs<T>, _, (S.M{l, 1n+d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}})) : S.Model<T> & E.Obs<T>}
178 {==}))))
179 case False{} False{}:
180 +xs = LY.somes(T, AR.slots(Maybe<&2, T>, t))
181 +nf = room_nat(n, d, False{}, er)
182 (ST.Sh{l, d, n, t}, (E.OUnit{Fail{E.CapacityExceeded{}}}, (
183 %Equal.sym(Bool, Nat.is_lt(n, SC.pow2(d)), False{}, er) : {DA.obs_unit(T, DA.push_room(T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), v, _, Nat.is_lt(d, l))) == (ST.real(T, ST.Sh{l, d, n, t}), E.OUnit{Fail{E.CapacityExceeded{}}}) : DA.DynArray<&2, T> & E.Obs<T>}
184 %Equal.sym(Bool, Nat.is_lt(d, l), False{}, eg) : {DA.obs_unit(T, DA.push_room(T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), v, False{}, _)) == (ST.real(T, ST.Sh{l, d, n, t}), E.OUnit{Fail{E.CapacityExceeded{}}}) : DA.DynArray<&2, T> & E.Obs<T>}
185 {==},
186 (g,
187 %Equal.sym(Nat, SC.length(T, xs), n, LY.lay_len(T, AR.slots(Maybe<&2, T>, t), n, ST.g_lay(T, l, d, n, t, g))) : {(S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}) == Bool.pick(S.Model<T> & E.Obs<T>, Nat.is_lt(_, SC.pow2(d)), (S.M{l, d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), Bool.pick(S.Model<T> & E.Obs<T>, Nat.is_lt(d, l), (S.M{l, 1n+d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}))) : S.Model<T> & E.Obs<T>}
188 %Equal.sym(Bool, Nat.is_lt(n, SC.pow2(d)), False{}, nf) : {(S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}) == Bool.pick(S.Model<T> & E.Obs<T>, _, (S.M{l, d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), Bool.pick(S.Model<T> & E.Obs<T>, Nat.is_lt(d, l), (S.M{l, 1n+d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}))) : S.Model<T> & E.Obs<T>}
189 %Equal.sym(Bool, Nat.is_lt(d, l), False{}, eg) : {(S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}) == Bool.pick(S.Model<T> & E.Obs<T>, _, (S.M{l, 1n+d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}})) : S.Model<T> & E.Obs<T>}
190 {==}))))
191
192def push_ok(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +v: T, +g: {ST.good(T, ST.Sh{l, d, n, t}) == True{} : Bool}) -> StepOK(T, ST.Sh{l, d, n, t}, E.Push{v}):
193 push_case(T, l, d, n, t, v, g, Nat.is_lt(n, SC.pow2(d)), {==}, Nat.is_lt(d, l), {==})
194
195# ---- pop ----
196
197def pop_spec(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +m: Nat, +h: {SC.length(T, xs) == 1n+m : Nat}) -> {S.pop(T, l, d, xs) == (S.M{l, d, SC.init(T, xs)}, E.OItem{S.item_result(T, SC.nth(T, xs, m))}) : S.Model<T> & E.Obs<T>}:
198 match xs:
199 case Nil{}:
200 Empty.absurd({S.pop(T, l, d, Nil{}) == (S.M{l, d, Nil{}}, E.OItem{S.item_result(T, None{})}) : S.Model<T> & E.Obs<T>}, N.zero_succ(m, h))
201 case Con{+x, +r}:
202 %Equal.sym(Maybe<&2, T>, SC.nth(T, Con{x, r}, m), SC.last(T, Con{x, r}), LY.nth_last(T, Con{x, r}, m, h)) : {(S.M{l, d, SC.init(T, Con{x, r})}, E.OItem{S.item_result(T, SC.last(T, Con{x, r}))}) == (S.M{l, d, SC.init(T, Con{x, r})}, E.OItem{S.item_result(T, _)}) : S.Model<T> & E.Obs<T>}
203 {==}
204
205def pop_ok(-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}) -> StepOK(T, ST.Sh{l, d, n, t}, E.Pop{}):
206 match n:
207 case 0n:
208 +xs = LY.somes(T, AR.slots(Maybe<&2, T>, t))
209 (ST.Sh{l, d, 0n, t}, (E.OItem{Fail{E.EmptyArray{}}}, ({==}, (g,
210 %Equal.sym(List<&2, T>, xs, Nil{}, LL.length_zero_nil(T, xs, LY.lay_len(T, AR.slots(Maybe<&2, T>, t), 0n, ST.g_lay(T, l, d, 0n, t, g)))) : {(S.M{l, d, _}, E.OItem{Fail{E.EmptyArray{}}}) == S.pop(T, l, d, _) : S.Model<T> & E.Obs<T>}
211 {==}))))
212 case 1n+ +m:
213 +ss = AR.slots(Maybe<&2, T>, t)
214 +xs = LY.somes(T, ss)
215 +x = SC.nth(T, xs, m)
216 +hlay = ST.g_lay(T, l, d, 1n+m, t, g)
217 +hm = N.lt_succ(m)
218 +hi = N.lt_le_trans(m, 1n+m, SC.pow2(d), hm, n_le_cap(T, l, d, 1n+m, t, g))
219 +t2 = AR.upd(Maybe<&2, T>, d, t, m, None{})
220 +hs = upd_slots(T, l, d, 1n+m, t, m, None{}, g, hi)
221 (ST.Sh{l, d, m, t2}, (E.OItem{S.item_result(T, x)}, (
222 %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), swap_arr(T, l, d, 1n+m, t, m, None{}, x, g, hi, LY.lay_nth(T, ss, 1n+m, m, hlay, hm))) : {DA.obs_item(T, DA.pop_found(T, l, d, SC.pow2(d), m, _)) == (ST.real(T, ST.Sh{l, d, m, t2}), E.OItem{S.item_result(T, x)}) : DA.DynArray<&2, T> & E.Obs<T>}
223 %Equal.sym(Result<&2, &2, E.Error, T>, DA.slot_result(T, x), S.item_result(T, x), ST.slot_item(T, x)) : {(DA.DA{l, d, SC.pow2(d), m, AR.thaw(Maybe<&2, T>, t2)}, E.OItem{_}) == (ST.real(T, ST.Sh{l, d, m, t2}), E.OItem{S.item_result(T, x)}) : DA.DynArray<&2, T> & E.Obs<T>}
224 {==},
225 (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)),
226 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))),
227 %Equal.sym(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, t2), SC.update(Maybe<&2, T>, ss, m, None{}), hs) : {(S.M{l, d, LY.somes(T, _)}, E.OItem{S.item_result(T, x)}) == S.pop(T, l, d, xs) : S.Model<T> & E.Obs<T>}
228 %Equal.sym(List<&2, T>, LY.somes(T, SC.update(Maybe<&2, T>, ss, m, None{})), SC.init(T, xs), LY.somes_pop(T, ss, m, hlay)) : {(S.M{l, d, _}, E.OItem{S.item_result(T, x)}) == S.pop(T, l, d, xs) : S.Model<T> & E.Obs<T>}
229 Equal.sym(S.Model<T> & E.Obs<T>, S.pop(T, l, d, xs), (S.M{l, d, SC.init(T, xs)}, E.OItem{S.item_result(T, x)}), pop_spec(T, l, d, xs, m, LY.lay_len(T, ss, 1n+m, hlay)))))))
230
231# ---- clear ----
232
233def clear_ok(-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}) -> StepOK(T, ST.Sh{l, d, n, t}, E.Clear{}):
234 +t2 = AR.trep(Maybe<&2, T>, d, None{})
235 (ST.Sh{l, d, 0n, t2}, (E.OUnit{Done{Unit{}}}, (
236 %Equal.sym(Array<Maybe<&2, T>>, DA.empty_slots(T, d), AR.thaw(Maybe<&2, T>, t2), ST.empty_eq(T, d)) : {(DA.DA{l, d, SC.pow2(d), 0n, _}, E.OUnit{Done{Unit{}}}) == (ST.real(T, ST.Sh{l, d, 0n, t2}), E.OUnit{Done{Unit{}}}) : DA.DynArray<&2, T> & E.Obs<T>}
237 {==},
238 (ST.good_intro(T, l, d, 0n, t2, ST.g_limit(T, l, d, n, t, g), ST.g_depth(T, l, d, n, t, g), AR.trep_perfect(Maybe<&2, T>, d, None{}),
239 L.subst(List<&2, Maybe<&2, T>>, ys => {LY.lay(T, ys, 0n) == True{} : Bool}, SC.replicate(Maybe<&2, T>, SC.pow2(d), None{}), AR.slots(Maybe<&2, T>, t2), Equal.sym(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, t2), SC.replicate(Maybe<&2, T>, SC.pow2(d), None{}), AR.trep_slots(Maybe<&2, T>, d, None{})), LY.lay_rep(T, SC.pow2(d)))),
240 %Equal.sym(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, t2), SC.replicate(Maybe<&2, T>, SC.pow2(d), None{}), AR.trep_slots(Maybe<&2, T>, d, None{})) : {(S.M{l, d, LY.somes(T, _)}, E.OUnit{Done{Unit{}}}) == (S.M{l, d, Nil{}}, E.OUnit{S.ok_unit()}) : S.Model<T> & E.Obs<T>}
241 %Equal.sym(List<&2, T>, LY.somes(T, SC.replicate(Maybe<&2, T>, SC.pow2(d), None{})), Nil{}, LY.somes_rep(T, SC.pow2(d))) : {(S.M{l, d, _}, E.OUnit{Done{Unit{}}}) == (S.M{l, d, Nil{}}, E.OUnit{S.ok_unit()}) : S.Model<T> & E.Obs<T>}
242 {==}))))
243
244# ---- to_list ----
245
246def to_list_ok(-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}) -> StepOK(T, ST.Sh{l, d, n, t}, E.ToList{}):
247 match n:
248 case 0n:
249 +ss = AR.slots(Maybe<&2, T>, t)
250 +xs = LY.somes(T, ss)
251 (ST.Sh{l, d, 0n, t}, (E.OList{xs}, (
252 %Equal.sym(List<&2, T>, xs, Nil{}, LL.length_zero_nil(T, xs, LY.lay_len(T, ss, 0n, ST.g_lay(T, l, d, 0n, t, g)))) : {(DA.DA{l, d, SC.pow2(d), 0n, AR.thaw(Maybe<&2, T>, t)}, E.OList{Nil{}}) == (ST.real(T, ST.Sh{l, d, 0n, t}), E.OList{_}) : DA.DynArray<&2, T> & E.Obs<T>}
253 {==}, (g, {==}))))
254 case 1n+ +m:
255 +ss = AR.slots(Maybe<&2, T>, t)
256 +xs = LY.somes(T, ss)
257 +hlay = ST.g_lay(T, l, d, 1n+m, t, g)
258 +hd = ST.g_depth(T, l, d, 1n+m, t, g)
259 +hl = ST.g_limit(T, l, d, 1n+m, t, g)
260 +pf = ST.g_perfect(T, l, d, 1n+m, t, g)
261 +hm = N.succ_le_lt(m, SC.pow2(d), n_le_cap(T, l, d, 1n+m, t, g))
262 (ST.Sh{l, d, 1n+m, t}, (E.OList{xs}, (
263 %Equal.sym(Array<Maybe<&2, T>> & Maybe<&2, T>, Array.get(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, t), U32.from_nat(m)), (AR.thaw(Maybe<&2, T>, t), W.slot(T, ss, m)), W.get_slot(T, l, d, t, m, hd, hl, hm, pf)) : {DA.obs_list(T, DA.tl_done(T, l, d, SC.pow2(d), 1n+m, DA.tl_go(1n+m, T, Nil{}, _))) == (ST.real(T, ST.Sh{l, d, 1n+m, t}), E.OList{xs}) : DA.DynArray<&2, T> & E.Obs<T>}
264 %Equal.sym(Array<Maybe<&2, T>> & List<&2, T>, DA.tl_go(1n+m, T, Nil{}, (AR.thaw(Maybe<&2, T>, t), W.slot(T, ss, m))), (AR.thaw(Maybe<&2, T>, t), W.tvals(1n+m, T, ss, Nil{})), W.tl_thaw(1n+m, T, l, d, t, Nil{}, hd, hl, hm, pf)) : {DA.obs_list(T, DA.tl_done(T, l, d, SC.pow2(d), 1n+m, _)) == (ST.real(T, ST.Sh{l, d, 1n+m, t}), E.OList{xs}) : DA.DynArray<&2, T> & E.Obs<T>}
265 %Equal.sym(List<&2, T>, W.tvals(1n+m, T, ss, Nil{}), xs, W.tvals_model(T, ss, 1n+m, hlay)) : {(DA.DA{l, d, SC.pow2(d), 1n+m, AR.thaw(Maybe<&2, T>, t)}, E.OList{_}) == (ST.real(T, ST.Sh{l, d, 1n+m, t}), E.OList{xs}) : DA.DynArray<&2, T> & E.Obs<T>}
266 {==}, (g, {==}))))
267
268# ---- reserve ----
269
270def feasible_fuel(+l: Nat, +d: Nat, +k: Nat, +hdl: {Nat.is_le(d, l) == True{} : Bool}, +hp: {Nat.is_le(k, SC.pow2(l)) == True{} : Bool}) -> {Nat.is_le(k, SC.pow2(Nat.add(d, Nat.sub(l, d)))) == True{} : Bool}:
271 L.subst(Nat, x => {Nat.is_le(k, SC.pow2(x)) == True{} : Bool}, l, Nat.add(d, Nat.sub(l, d)), Equal.sym(Nat, Nat.add(d, Nat.sub(l, d)), l, N.sub_add(l, d, hdl)), hp)
272
273def spec_fuel(+d: Nat, +k: Nat) -> {Nat.is_le(k, SC.pow2(Nat.add(d, k))) == True{} : Bool}:
274 N.lt_le(k, SC.pow2(Nat.add(d, k)), N.lt_le_trans(k, SC.pow2(k), SC.pow2(Nat.add(d, k)), GR.pow2_gt(k), N.pow2_mono(k, Nat.add(d, k), L.subst(Nat, x => {Nat.is_le(k, x) == True{} : Bool}, Nat.add(k, d), Nat.add(d, k), N.add_comm(k, d), N.le_add_right(k, d)))))
275
276def reserve_case(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +k: Nat, +g: {ST.good(T, ST.Sh{l, d, n, t}) == True{} : Bool}, +fits: Bool, +ef: {Nat.is_le(k, SC.pow2(d)) == fits : Bool}, +feas: Bool, +ep: {Nat.is_le(k, DA.pow2(l)) == feas : Bool}) -> StepOK(T, ST.Sh{l, d, n, t}, E.Reserve{k}):
277 match fits feas:
278 case True{} _:
279 +xs = LY.somes(T, AR.slots(Maybe<&2, T>, t))
280 (ST.Sh{l, d, n, t}, (E.OUnit{Done{Unit{}}}, (
281 %Equal.sym(Bool, Nat.is_le(k, SC.pow2(d)), True{}, ef) : {DA.obs_unit(T, DA.reserve_checked(T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), k, _)) == (ST.real(T, ST.Sh{l, d, n, t}), E.OUnit{Done{Unit{}}}) : DA.DynArray<&2, T> & E.Obs<T>}
282 {==},
283 (g,
284 %Equal.sym(Bool, Nat.is_le(k, SC.pow2(d)), True{}, ef) : {(S.M{l, d, xs}, E.OUnit{Done{Unit{}}}) == Bool.pick(S.Model<T> & E.Obs<T>, _, (S.M{l, d, xs}, E.OUnit{S.ok_unit()}), Bool.pick(S.Model<T> & E.Obs<T>, Nat.is_le(k, SC.pow2(l)), (S.M{l, S.fit(k, d, k), xs}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}))) : S.Model<T> & E.Obs<T>}
285 {==}))))
286 case False{} True{}:
287 +xs = LY.somes(T, AR.slots(Maybe<&2, T>, t))
288 +f = Nat.sub(l, d)
289 +sh2 = GR.sgrow(T, f, k, ST.Sh{l, d, n, t})
290 +hdl = ST.g_depth(T, l, d, n, t, g)
291 +hp = GR.fits_nat(k, l, True{}, ep)
292 -mP = {ST.model(T, sh2) == S.M{l, S.fit(f, d, k), xs} : S.Model<T>}
293 -gP = {ST.good(T, sh2) == True{} : Bool}
294 +hf = L.subst(Nat, x => {Nat.is_le(x, l) == True{} : Bool}, l, Nat.add(d, f), Equal.sym(Nat, Nat.add(d, f), l, N.sub_add(l, d, hdl)), N.le_refl(l))
295 (sh2, (E.OUnit{Done{Unit{}}}, (
296 %Equal.sym(Bool, Nat.is_le(k, SC.pow2(d)), False{}, ef) : {DA.obs_unit(T, DA.reserve_checked(T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), k, _)) == (ST.real(T, sh2), E.OUnit{Done{Unit{}}}) : DA.DynArray<&2, T> & E.Obs<T>}
297 %Equal.sym(Bool, Nat.is_le(k, DA.pow2(l)), True{}, ep) : {DA.obs_unit(T, DA.reserve_room(T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), k, _)) == (ST.real(T, sh2), E.OUnit{Done{Unit{}}}) : DA.DynArray<&2, T> & E.Obs<T>}
298 %Equal.sym(DA.DynArray<&2, T>, DA.grow_until(T, f, k, ST.real(T, ST.Sh{l, d, n, t})), ST.real(T, sh2), GR.grow_until_real(T, f, k, ST.Sh{l, d, n, t})) : {(_, E.OUnit{Done{Unit{}}}) == (ST.real(T, sh2), E.OUnit{Done{Unit{}}}) : DA.DynArray<&2, T> & E.Obs<T>}
299 {==},
300 (Pair.snd(mP, gP, GR.sgrow_props(T, f, k, l, d, n, t, g, hf, Nat.is_le(k, SC.pow2(d)), {==})),
301 %Equal.sym(S.Model<T>, ST.model(T, sh2), S.M{l, S.fit(f, d, k), xs}, Pair.fst(mP, gP, GR.sgrow_props(T, f, k, l, d, n, t, g, hf, Nat.is_le(k, SC.pow2(d)), {==}))) : {(_, E.OUnit{Done{Unit{}}}) == S.step(T, S.M{l, d, xs}, E.Reserve{k}) : S.Model<T> & E.Obs<T>}
302 %Equal.sym(Nat, S.fit(f, d, k), S.fit(k, d, k), GR.fe_case(f, k, d, k, feasible_fuel(l, d, k, hdl, hp), spec_fuel(d, k), Nat.is_le(k, SC.pow2(d)), {==})) : {(S.M{l, _, xs}, E.OUnit{Done{Unit{}}}) == Bool.pick(S.Model<T> & E.Obs<T>, Nat.is_le(k, SC.pow2(d)), (S.M{l, d, xs}, E.OUnit{S.ok_unit()}), Bool.pick(S.Model<T> & E.Obs<T>, Nat.is_le(k, SC.pow2(l)), (S.M{l, S.fit(k, d, k), xs}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}))) : S.Model<T> & E.Obs<T>}
303 %Equal.sym(Bool, Nat.is_le(k, SC.pow2(d)), False{}, ef) : {(S.M{l, S.fit(k, d, k), xs}, E.OUnit{Done{Unit{}}}) == Bool.pick(S.Model<T> & E.Obs<T>, _, (S.M{l, d, xs}, E.OUnit{S.ok_unit()}), Bool.pick(S.Model<T> & E.Obs<T>, Nat.is_le(k, SC.pow2(l)), (S.M{l, S.fit(k, d, k), xs}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}))) : S.Model<T> & E.Obs<T>}
304 %Equal.sym(Bool, Nat.is_le(k, SC.pow2(l)), True{}, hp) : {(S.M{l, S.fit(k, d, k), xs}, E.OUnit{Done{Unit{}}}) == Bool.pick(S.Model<T> & E.Obs<T>, _, (S.M{l, S.fit(k, d, k), xs}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}})) : S.Model<T> & E.Obs<T>}
305 {==}))))
306 case False{} False{}:
307 +xs = LY.somes(T, AR.slots(Maybe<&2, T>, t))
308 (ST.Sh{l, d, n, t}, (E.OUnit{Fail{E.CapacityExceeded{}}}, (
309 %Equal.sym(Bool, Nat.is_le(k, SC.pow2(d)), False{}, ef) : {DA.obs_unit(T, DA.reserve_checked(T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), k, _)) == (ST.real(T, ST.Sh{l, d, n, t}), E.OUnit{Fail{E.CapacityExceeded{}}}) : DA.DynArray<&2, T> & E.Obs<T>}
310 %Equal.sym(Bool, Nat.is_le(k, DA.pow2(l)), False{}, ep) : {DA.obs_unit(T, DA.reserve_room(T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), k, _)) == (ST.real(T, ST.Sh{l, d, n, t}), E.OUnit{Fail{E.CapacityExceeded{}}}) : DA.DynArray<&2, T> & E.Obs<T>}
311 {==},
312 (g,
313 %Equal.sym(Bool, Nat.is_le(k, SC.pow2(d)), False{}, ef) : {(S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}) == Bool.pick(S.Model<T> & E.Obs<T>, _, (S.M{l, d, xs}, E.OUnit{S.ok_unit()}), Bool.pick(S.Model<T> & E.Obs<T>, Nat.is_le(k, SC.pow2(l)), (S.M{l, S.fit(k, d, k), xs}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}))) : S.Model<T> & E.Obs<T>}
314 %Equal.sym(Bool, Nat.is_le(k, SC.pow2(l)), False{}, GR.fits_nat(k, l, False{}, ep)) : {(S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}) == Bool.pick(S.Model<T> & E.Obs<T>, _, (S.M{l, S.fit(k, d, k), xs}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}})) : S.Model<T> & E.Obs<T>}
315 {==}))))
316
317def reserve_ok(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +k: Nat, +g: {ST.good(T, ST.Sh{l, d, n, t}) == True{} : Bool}) -> StepOK(T, ST.Sh{l, d, n, t}, E.Reserve{k}):
318 reserve_case(T, l, d, n, t, k, g, Nat.is_le(k, SC.pow2(d)), {==}, Nat.is_le(k, DA.pow2(l)), {==})
319
320# ---- every operation ----
321
322def step_ok(-T: Data, +sh: ST.Shadow<T>, +op: E.Op<T>, +g: {ST.good(T, sh) == True{} : Bool}) -> StepOK(T, sh, op):
323 match sh op:
324 case ST.Sh{+l, +d, +n, +t} E.Length{}:
325 length_ok(T, l, d, n, t, g)
326 case ST.Sh{+l, +d, +n, +t} E.Capacity{}:
327 capacity_ok(T, l, d, n, t, g)
328 case ST.Sh{+l, +d, +n, +t} E.Get{+i}:
329 get_ok(T, l, d, n, t, i, g)
330 case ST.Sh{+l, +d, +n, +t} E.Set{+i, +v}:
331 set_ok(T, l, d, n, t, i, v, g)
332 case ST.Sh{+l, +d, +n, +t} E.Push{+v}:
333 push_ok(T, l, d, n, t, v, g)
334 case ST.Sh{+l, +d, +n, +t} E.Pop{}:
335 pop_ok(T, l, d, n, t, g)
336 case ST.Sh{+l, +d, +n, +t} E.Reserve{+k}:
337 reserve_ok(T, l, d, n, t, k, g)
338 case ST.Sh{+l, +d, +n, +t} E.Clear{}:
339 clear_ok(T, l, d, n, t, g)
340 case ST.Sh{+l, +d, +n, +t} E.ToList{}:
341 to_list_ok(T, l, d, n, t, g)