proofs/containers/dynamic_array/closed.bend
bend-collections-laws-containers@1.0.0.0 · 178 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/src/math/pow2.bend as P2
3import bend-collections-laws-containers@1.0.0.0/proofs/math/pow2/pow2.bend as PT
4import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/clear.bend as CLR
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LL
7import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
8import bend-collections-laws-containers@1.0.0.0/proofs/lib/array.bend as AR
9import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
10import bend-collections-laws-containers@1.0.0.0/spec/containers/dynamic_array.bend as S
11import bend-collections-laws-containers@1.0.0.0/src/containers/dynamic_array.bend as DA
12import bend-collections-laws-containers@1.0.0.0/src/containers/types/dynamic_array.bend as E
13import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/layout.bend as LY
14import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/state.bend as ST
15import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/steps.bend as SP
16import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/growth.bend as GR
17import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/trace.bend as TR
18
19# The executable specializations DA.*_at (template element type, so every
20# Base.Array call is compiled at a closed type) compute exactly what the
21# parametric definitions compute. Every universal law proved about DA.step
22# and DA.run therefore holds of DA.step_at and DA.run_at at each instance.
23
24# ---- the growth loop ----
25
26def gstep_at_case(~T: Data, +k: Nat, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +b: Bool, +eb: {Nat.is_le(k, SC.pow2(d)) == b : Bool}) -> {DA.grow_step_at(~T, k, ST.real(T, ST.Sh{l, d, n, t})) == ST.real(T, GR.sgstep(T, k, ST.Sh{l, d, n, t})) : DA.DynArray<&2, T>}:
27 match b:
28 case True{}:
29 %Equal.sym(Bool, Nat.is_le(k, SC.pow2(d)), True{}, eb) : {DA.grow_if_at(~T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), _) == ST.real(T, Bool.pick(ST.Shadow<T>, Nat.is_le(k, SC.pow2(d)), ST.Sh{l, d, n, t}, ST.Sh{l, 1n+d, n, AR.TNode{t, AR.trep(Maybe<&2, T>, d, None{})}})) : DA.DynArray<&2, T>}
30 %Equal.sym(Bool, Nat.is_le(k, SC.pow2(d)), True{}, eb) : {DA.DA{l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t)} == ST.real(T, Bool.pick(ST.Shadow<T>, _, ST.Sh{l, d, n, t}, ST.Sh{l, 1n+d, n, AR.TNode{t, AR.trep(Maybe<&2, T>, d, None{})}})) : DA.DynArray<&2, T>}
31 {==}
32 case False{}:
33 %Equal.sym(Bool, Nat.is_le(k, SC.pow2(d)), False{}, eb) : {DA.grow_if_at(~T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), _) == ST.real(T, Bool.pick(ST.Shadow<T>, Nat.is_le(k, SC.pow2(d)), ST.Sh{l, d, n, t}, ST.Sh{l, 1n+d, n, AR.TNode{t, AR.trep(Maybe<&2, T>, d, None{})}})) : DA.DynArray<&2, T>}
34 %Equal.sym(Bool, Nat.is_le(k, SC.pow2(d)), False{}, eb) : {DA.DA{l, 1n+d, Nat.double(SC.pow2(d)), n, DA.grown_at(~T, d, AR.thaw(Maybe<&2, T>, t))} == ST.real(T, Bool.pick(ST.Shadow<T>, _, ST.Sh{l, d, n, t}, ST.Sh{l, 1n+d, n, AR.TNode{t, AR.trep(Maybe<&2, T>, d, None{})}})) : DA.DynArray<&2, T>}
35 %Equal.sym(Array<Maybe<&2, T>>, DA.grown_at(~T, d, AR.thaw(Maybe<&2, T>, t)), AR.thaw(Maybe<&2, T>, AR.TNode{t, AR.trep(Maybe<&2, T>, d, None{})}), ST.grown_eq(T, d, t)) : {DA.DA{l, 1n+d, Nat.double(SC.pow2(d)), n, _} == ST.real(T, ST.Sh{l, 1n+d, n, AR.TNode{t, AR.trep(Maybe<&2, T>, d, None{})}}) : DA.DynArray<&2, T>}
36 {==}
37
38def grow_until_at_real(~T: Data, +f: Nat, +k: Nat, +sh: ST.Shadow<T>) -> {DA.grow_until_at(~T, f, k, ST.real(T, sh)) == ST.real(T, GR.sgrow(T, f, k, sh)) : DA.DynArray<&2, T>}:
39 match f sh:
40 case 0n _:
41 {==}
42 case 1n+g ST.Sh{+l, +d, +n, +t}:
43 %Equal.sym(DA.DynArray<&2, T>, DA.grow_step_at(~T, k, ST.real(T, ST.Sh{l, d, n, t})), ST.real(T, GR.sgstep(T, k, ST.Sh{l, d, n, t})), gstep_at_case(~T, k, l, d, n, t, Nat.is_le(k, SC.pow2(d)), {==})) : {DA.grow_until_at(~T, g, k, _) == ST.real(T, GR.sgrow(T, g, k, GR.sgstep(T, k, ST.Sh{l, d, n, t}))) : DA.DynArray<&2, T>}
44 grow_until_at_real(~T, g, k, GR.sgstep(T, k, ST.Sh{l, d, n, t}))
45
46def grow_until_eq(~T: Data, +f: Nat, +k: Nat, +sh: ST.Shadow<T>) -> {DA.grow_until_at(~T, f, k, ST.real(T, sh)) == DA.grow_until(T, f, k, ST.real(T, sh)) : DA.DynArray<&2, T>}:
47 %Equal.sym(DA.DynArray<&2, T>, DA.grow_until(T, f, k, ST.real(T, sh)), ST.real(T, GR.sgrow(T, f, k, sh)), GR.grow_until_real(T, f, k, sh)) : {DA.grow_until_at(~T, f, k, ST.real(T, sh)) == _ : DA.DynArray<&2, T>}
48 grow_until_at_real(~T, f, k, sh)
49
50# ---- the flattening walk ----
51
52def found_eq(~T: Data, +l: Nat, +d: Nat, +c: Nat, +n: Nat, r: Array<Maybe<&2, T>> & Maybe<&2, T>) -> {DA.get_found_at(~T, l, d, c, n, r) == DA.get_found(T, l, d, c, n, r) : DA.DynArray<&2, T> & Result<&2, &2, E.Error, T>}:
53 match r:
54 case Tuple{arr, None{}}:
55 {==}
56 case Tuple{arr, Some{x}}:
57 {==}
58
59def get_eq_case(~T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +i: Nat, +b: Bool, +eb: {Nat.is_lt(i, n) == b : Bool}) -> {DA.step_at(~T, ST.real(T, ST.Sh{l, d, n, t}), E.Get{i}) == DA.step(T, ST.real(T, ST.Sh{l, d, n, t}), E.Get{i}) : DA.DynArray<&2, T> & E.Obs<T>}:
60 match b:
61 case True{}:
62 %Equal.sym(Bool, Nat.is_lt(i, n), True{}, eb) : {DA.obs_item(T, DA.get_checked_at(~T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), i, _)) == DA.obs_item(T, DA.get_checked(T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), i, _)) : DA.DynArray<&2, T> & E.Obs<T>}
63 Equal.cong(DA.DynArray<&2, T> & Result<&2, &2, E.Error, T>, DA.DynArray<&2, T> & E.Obs<T>, r => DA.obs_item(T, r), DA.get_found_at(~T, l, d, SC.pow2(d), n, Array.get(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, t), U32.from_nat(i))), DA.get_found(T, l, d, SC.pow2(d), n, Array.get(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, t), U32.from_nat(i))), found_eq(~T, l, d, SC.pow2(d), n, Array.get(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, t), U32.from_nat(i))))
64 case False{}:
65 %Equal.sym(Bool, Nat.is_lt(i, n), False{}, eb) : {DA.obs_item(T, DA.get_checked_at(~T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), i, _)) == DA.obs_item(T, DA.get_checked(T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), i, _)) : DA.DynArray<&2, T> & E.Obs<T>}
66 {==}
67
68def set_eq_case(~T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +i: Nat, +v: T, +b: Bool, +eb: {Nat.is_lt(i, n) == b : Bool}) -> {DA.step_at(~T, ST.real(T, ST.Sh{l, d, n, t}), E.Set{i, v}) == DA.step(T, ST.real(T, ST.Sh{l, d, n, t}), E.Set{i, v}) : DA.DynArray<&2, T> & E.Obs<T>}:
69 match b:
70 case True{}:
71 %Equal.sym(Bool, Nat.is_lt(i, n), True{}, eb) : {DA.obs_unit(T, DA.set_checked_at(~T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), i, v, _)) == DA.obs_unit(T, DA.set_checked(T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), i, v, _)) : DA.DynArray<&2, T> & E.Obs<T>}
72 {==}
73 case False{}:
74 %Equal.sym(Bool, Nat.is_lt(i, n), False{}, eb) : {DA.obs_unit(T, DA.set_checked_at(~T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), i, v, _)) == DA.obs_unit(T, DA.set_checked(T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), i, v, _)) : DA.DynArray<&2, T> & E.Obs<T>}
75 {==}
76
77def push_eq_case(~T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +v: T, +room: Bool, +er: {Nat.is_lt(n, SC.pow2(d)) == room : Bool}, +grow: Bool, +eg: {Nat.is_lt(d, l) == grow : Bool}) -> {DA.step_at(~T, ST.real(T, ST.Sh{l, d, n, t}), E.Push{v}) == DA.step(T, ST.real(T, ST.Sh{l, d, n, t}), E.Push{v}) : DA.DynArray<&2, T> & E.Obs<T>}:
78 match room grow:
79 case True{} _:
80 %Equal.sym(Bool, Nat.is_lt(n, SC.pow2(d)), True{}, er) : {DA.obs_unit(T, DA.push_room_at(~T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), v, _, Nat.is_lt(d, l))) == 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))) : DA.DynArray<&2, T> & E.Obs<T>}
81 {==}
82 case False{} True{}:
83 %Equal.sym(Bool, Nat.is_lt(n, SC.pow2(d)), False{}, er) : {DA.obs_unit(T, DA.push_room_at(~T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), v, _, Nat.is_lt(d, l))) == 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))) : DA.DynArray<&2, T> & E.Obs<T>}
84 %Equal.sym(Bool, Nat.is_lt(d, l), True{}, eg) : {DA.obs_unit(T, DA.push_room_at(~T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), v, False{}, _)) == DA.obs_unit(T, DA.push_room(T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), v, False{}, _)) : DA.DynArray<&2, T> & E.Obs<T>}
85 %Equal.sym(Array<Maybe<&2, T>>, DA.grown_at(~T, d, AR.thaw(Maybe<&2, T>, t)), AR.thaw(Maybe<&2, T>, AR.TNode{t, AR.trep(Maybe<&2, T>, d, None{})}), 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{}}}) == (DA.DA{l, 1n+d, Nat.double(SC.pow2(d)), 1n+n, Array.set(Maybe<&2, T>, DA.grown(T, d, AR.thaw(Maybe<&2, T>, t)), U32.from_nat(n), Some{v})}, E.OUnit{Done{Unit{}}}) : DA.DynArray<&2, T> & E.Obs<T>}
86 %Equal.sym(Array<Maybe<&2, T>>, DA.grown(T, d, AR.thaw(Maybe<&2, T>, t)), AR.thaw(Maybe<&2, T>, AR.TNode{t, AR.trep(Maybe<&2, T>, d, None{})}), ST.grown_eq(T, d, t)) : {(DA.DA{l, 1n+d, Nat.double(SC.pow2(d)), 1n+n, Array.set(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, AR.TNode{t, AR.trep(Maybe<&2, T>, d, None{})}), U32.from_nat(n), Some{v})}, E.OUnit{Done{Unit{}}}) == (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{}}}) : DA.DynArray<&2, T> & E.Obs<T>}
87 {==}
88 case False{} False{}:
89 %Equal.sym(Bool, Nat.is_lt(n, SC.pow2(d)), False{}, er) : {DA.obs_unit(T, DA.push_room_at(~T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), v, _, Nat.is_lt(d, l))) == 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))) : DA.DynArray<&2, T> & E.Obs<T>}
90 %Equal.sym(Bool, Nat.is_lt(d, l), False{}, eg) : {DA.obs_unit(T, DA.push_room_at(~T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), v, False{}, _)) == DA.obs_unit(T, DA.push_room(T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), v, False{}, _)) : DA.DynArray<&2, T> & E.Obs<T>}
91 {==}
92
93def pop_eq_case(~T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>) -> {DA.step_at(~T, ST.real(T, ST.Sh{l, d, n, t}), E.Pop{}) == DA.step(T, ST.real(T, ST.Sh{l, d, n, t}), E.Pop{}) : DA.DynArray<&2, T> & E.Obs<T>}:
94 match n:
95 case 0n:
96 {==}
97 case 1n+ +m:
98 {==}
99
100def tl_go_eq(~T: Data, k: Nat, acc: List<&2, T>, r: Array<Maybe<&2, T>> & Maybe<&2, T>) -> {DA.tl_go_at(~T, k, acc, r) == DA.tl_go(k, T, acc, r) : Array<Maybe<&2, T>> & List<&2, T>}:
101 match k r:
102 case 0n Tuple{a, x}:
103 {==}
104 case 1n+ +m Tuple{a, x}:
105 tl_go_eq(~T, m, DA.cons_some(T, x, acc), Array.get(Maybe<&2, T>, a, U32.from_nat(DA.dec1(m))))
106
107def to_list_eq(~T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>) -> {DA.step_at(~T, ST.real(T, ST.Sh{l, d, n, t}), E.ToList{}) == DA.step(T, ST.real(T, ST.Sh{l, d, n, t}), E.ToList{}) : DA.DynArray<&2, T> & E.Obs<T>}:
108 match n:
109 case 0n:
110 {==}
111 case 1n+ +m:
112 Equal.cong(Array<Maybe<&2, T>> & List<&2, T>, DA.DynArray<&2, T> & E.Obs<T>, r => DA.obs_list(T, DA.tl_done(T, l, d, SC.pow2(d), 1n+m, r)),
113 DA.tl_go_at(~T, 1n+m, Nil{}, Array.get(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, t), U32.from_nat(m))),
114 DA.tl_go(1n+m, T, Nil{}, Array.get(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, t), U32.from_nat(m))),
115 tl_go_eq(~T, 1n+m, Nil{}, Array.get(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, t), U32.from_nat(m))))
116
117def reserve_eq_case(~T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +k: Nat, +fits: Bool, +ef: {Nat.is_le(k, SC.pow2(d)) == fits : Bool}, +feas: Bool, +ep: {Nat.is_le(k, DA.pow2(l)) == feas : Bool}) -> {DA.step_at(~T, ST.real(T, ST.Sh{l, d, n, t}), E.Reserve{k}) == DA.step(T, ST.real(T, ST.Sh{l, d, n, t}), E.Reserve{k}) : DA.DynArray<&2, T> & E.Obs<T>}:
118 match fits feas:
119 case True{} _:
120 %Equal.sym(Bool, Nat.is_le(k, SC.pow2(d)), True{}, ef) : {DA.obs_unit(T, DA.reserve_checked_at(~T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), k, _)) == DA.obs_unit(T, DA.reserve_checked(T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), k, _)) : DA.DynArray<&2, T> & E.Obs<T>}
121 {==}
122 case False{} True{}:
123 %Equal.sym(Bool, Nat.is_le(k, SC.pow2(d)), False{}, ef) : {DA.obs_unit(T, DA.reserve_checked_at(~T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), k, _)) == DA.obs_unit(T, DA.reserve_checked(T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), k, _)) : DA.DynArray<&2, T> & E.Obs<T>}
124 %Equal.trans(Nat, DA.pow2(l), SC.pow2(l), P2.pow2t(l), ST.pow2_src(l), Equal.sym(Nat, P2.pow2t(l), SC.pow2(l), PT.same(l))) : {DA.obs_unit(T, DA.reserve_room_at(~T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), k, Nat.is_le(k, _))) == DA.obs_unit(T, DA.reserve_room(T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), k, Nat.is_le(k, DA.pow2(l)))) : DA.DynArray<&2, T> & E.Obs<T>}
125 %Equal.sym(Bool, Nat.is_le(k, DA.pow2(l)), True{}, ep) : {DA.obs_unit(T, DA.reserve_room_at(~T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), k, _)) == DA.obs_unit(T, DA.reserve_room(T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), k, _)) : DA.DynArray<&2, T> & E.Obs<T>}
126 %Equal.sym(DA.DynArray<&2, T>, DA.grow_until_at(~T, Nat.sub(l, d), k, ST.real(T, ST.Sh{l, d, n, t})), DA.grow_until(T, Nat.sub(l, d), k, ST.real(T, ST.Sh{l, d, n, t})), grow_until_eq(~T, Nat.sub(l, d), k, ST.Sh{l, d, n, t})) : {(_, E.OUnit{Done{Unit{}}}) == (DA.grow_until(T, Nat.sub(l, d), k, DA.DA{l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t)}), E.OUnit{Done{Unit{}}}) : DA.DynArray<&2, T> & E.Obs<T>}
127 {==}
128 case False{} False{}:
129 %Equal.sym(Bool, Nat.is_le(k, SC.pow2(d)), False{}, ef) : {DA.obs_unit(T, DA.reserve_checked_at(~T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), k, _)) == DA.obs_unit(T, DA.reserve_checked(T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), k, _)) : DA.DynArray<&2, T> & E.Obs<T>}
130 %Equal.trans(Nat, DA.pow2(l), SC.pow2(l), P2.pow2t(l), ST.pow2_src(l), Equal.sym(Nat, P2.pow2t(l), SC.pow2(l), PT.same(l))) : {DA.obs_unit(T, DA.reserve_room_at(~T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), k, Nat.is_le(k, _))) == DA.obs_unit(T, DA.reserve_room(T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), k, Nat.is_le(k, DA.pow2(l)))) : DA.DynArray<&2, T> & E.Obs<T>}
131 %Equal.sym(Bool, Nat.is_le(k, DA.pow2(l)), False{}, ep) : {DA.obs_unit(T, DA.reserve_room_at(~T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), k, _)) == DA.obs_unit(T, DA.reserve_room(T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), k, _)) : DA.DynArray<&2, T> & E.Obs<T>}
132 {==}
133
134def step_eq(~T: Data, +sh: ST.Shadow<T>, +op: E.Op<T>, +g: {ST.good(T, sh) == True{} : Bool}) -> {DA.step_at(~T, ST.real(T, sh), op) == DA.step(T, ST.real(T, sh), op) : DA.DynArray<&2, T> & E.Obs<T>}:
135 match sh op:
136 case ST.Sh{+l, +d, +n, +t} E.Length{}:
137 {==}
138 case ST.Sh{+l, +d, +n, +t} E.Capacity{}:
139 {==}
140 case ST.Sh{+l, +d, +n, +t} E.Get{+i}:
141 get_eq_case(~T, l, d, n, t, i, Nat.is_lt(i, n), {==})
142 case ST.Sh{+l, +d, +n, +t} E.Set{+i, +v}:
143 set_eq_case(~T, l, d, n, t, i, v, Nat.is_lt(i, n), {==})
144 case ST.Sh{+l, +d, +n, +t} E.Push{+v}:
145 push_eq_case(~T, l, d, n, t, v, Nat.is_lt(n, SC.pow2(d)), {==}, Nat.is_lt(d, l), {==})
146 case ST.Sh{+l, +d, +n, +t} E.Pop{}:
147 pop_eq_case(~T, l, d, n, t)
148 case ST.Sh{+l, +d, +n, +t} E.Reserve{+k}:
149 reserve_eq_case(~T, l, d, n, t, k, Nat.is_le(k, SC.pow2(d)), {==}, Nat.is_le(k, DA.pow2(l)), {==})
150 case ST.Sh{+l, +d, +n, +t} E.Clear{}:
151 Equal.cong(DA.DynArray<&2, T>, DA.DynArray<&2, T> & E.Obs<T>, z => (z, E.OUnit{Done{Unit{}}}), 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})), CLR.clear_eq(~T, l, d, n, t, g))
152 case ST.Sh{+l, +d, +n, +t} E.ToList{}:
153 to_list_eq(~T, l, d, n, t)
154
155# ---- whole traces ----
156
157def run_acc_eq(~T: Data, +ops: List<&2, E.Op<T>>, +sh: ST.Shadow<T>, +acc: List<&2, E.Obs<T>>, +g: {ST.good(T, sh) == True{} : Bool}) -> {DA.run_acc_at(~T, ops, (ST.real(T, sh), acc)) == DA.run_acc(T, ops, (ST.real(T, sh), acc)) : DA.DynArray<&2, T> & List<&2, E.Obs<T>>}:
158 match ops:
159 case Nil{}:
160 {==}
161 case Con{+op, +rest}:
162 +sh1 = TR.so_sh(T, sh, op, SP.step_ok(T, sh, op, g))
163 +o = TR.so_obs(T, sh, op, SP.step_ok(T, sh, op, g))
164 +g1 = TR.so_good(T, sh, op, SP.step_ok(T, sh, op, g))
165 %Equal.sym(DA.DynArray<&2, T> & E.Obs<T>, DA.step_at(~T, ST.real(T, sh), op), DA.step(T, ST.real(T, sh), op), step_eq(~T, sh, op, g)) : {DA.run_acc_at(~T, rest, DA.record(T, acc, _)) == DA.run_acc(T, rest, DA.record(T, acc, DA.step(T, ST.real(T, sh), op))) : DA.DynArray<&2, T> & List<&2, E.Obs<T>>}
166 %Equal.sym(DA.DynArray<&2, T> & E.Obs<T>, DA.step(T, ST.real(T, sh), op), (ST.real(T, sh1), o), TR.so_step(T, sh, op, SP.step_ok(T, sh, op, g))) : {DA.run_acc_at(~T, rest, DA.record(T, acc, _)) == DA.run_acc(T, rest, DA.record(T, acc, _)) : DA.DynArray<&2, T> & List<&2, E.Obs<T>>}
167 run_acc_eq(~T, rest, sh1, Con{o, acc}, g1)
168
169def run_eq(~T: Data, +ops: List<&2, E.Op<T>>, +sh: ST.Shadow<T>, +g: {ST.good(T, sh) == True{} : Bool}) -> {DA.run_at(~T, ops, ST.real(T, sh)) == DA.run(T, ops, ST.real(T, sh)) : DA.DynArray<&2, T> & List<&2, E.Obs<T>>}:
170 Equal.cong(DA.DynArray<&2, T> & List<&2, E.Obs<T>>, DA.DynArray<&2, T> & List<&2, E.Obs<T>>, r => DA.finish(T, r), DA.run_acc_at(~T, ops, (ST.real(T, sh), Nil{})), DA.run_acc(T, ops, (ST.real(T, sh), Nil{})), run_acc_eq(~T, ops, sh, Nil{}, g))
171
172# ---- the constructors ----
173
174def new_eq(~T: Data) -> {DA.new_at(~T) == DA.new(T) : DA.DynArray<&2, T>}:
175 {==}
176
177def with_limit_eq(~T: Data, +k: Nat) -> {DA.with_limit_at(~T, k) == DA.with_limit(T, k) : DA.DynArray<&2, T>}:
178 {==}