1	import Base
2	import ../../../src/math/pow2.bend as P2
3	import ../../math/pow2/pow2.bend as PT
4	import ./clear.bend as CLR
5	import ../../lib/logic.bend as L
6	import ../../lib/list.bend as LL
7	import ../../lib/nat.bend as N
8	import ../../lib/array.bend as AR
9	import ../../../spec/lib/common.bend as SC
10	import ../../../spec/containers/dynamic_array.bend as S
11	import ../../../src/containers/dynamic_array.bend as DA
12	import ../../../src/containers/types/dynamic_array.bend as E
13	import ./layout.bend as LY
14	import ./state.bend as ST
15	import ./steps.bend as SP
16	import ./growth.bend as GR
17	import ./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	
26	def 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	
38	def 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	
46	def 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	
52	def 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	
59	def 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	
68	def 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	
77	def 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	
93	def 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	
100	def 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	
107	def 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	
117	def 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	
134	def 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	
157	def 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	
169	def 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	
174	def new_eq(~T: Data) -> {DA.new_at(~T) == DA.new(T) : DA.DynArray<&2, T>}:
175	  {==}
176	
177	def with_limit_eq(~T: Data, +k: Nat) -> {DA.with_limit_at(~T, k) == DA.with_limit(T, k) : DA.DynArray<&2, T>}:
178	  {==}