1	import Base
2	import ../../lib/logic.bend as L
3	import ../../lib/nat.bend as N
4	import ../../lib/array.bend as AR
5	import ../../../spec/lib/common.bend as SC
6	import ../../../src/containers/dynamic_array.bend as D
7	import ../../../src/containers/types/dynamic_array.bend as DE
8	import ../../../spec/containers/dynamic_array.bend as DS
9	import ../dynamic_array/layout.bend as LY
10	import ../dynamic_array/state.bend as DAS
11	import ../dynamic_array/steps.bend as DSP
12	import ../dynamic_array/trace.bend as DTR
13	
14	# The word array of a bitlist, used only through the dynamic array's proved
15	# contract (proofs/containers/dynamic_array: DSP.step_ok / DTR.so_*): each
16	# operation on the array of a good shadow lands on the array of another good
17	# shadow, whose model and answer are the dynamic-array spec step. Nothing
18	# here looks inside the array; only the item list `ws` and the depth limit
19	# `lim` of the model are used.
20	# (source: proofs/containers/bitlist/da.src)
21	
22	
23	def items(m: DS.Model<U32>) -> List<&2, U32>:
24	  match m:
25	    case DS.M{l, d, xs}:
26	      xs
27	
28	def mlim(m: DS.Model<U32>) -> Nat:
29	  match m:
30	    case DS.M{l, d, xs}:
31	      l
32	
33	# The stored words and the depth limit of a shadow.
34	def ws(w: DAS.Shadow<U32>) -> List<&2, U32>:
35	  items(DAS.model(U32, w))
36	
37	def lim(w: DAS.Shadow<U32>) -> Nat:
38	  mlim(DAS.model(U32, w))
39	
40	def unitem(o: DE.Obs<U32>) -> Result<&2, &2, DE.Error, U32>:
41	  match o:
42	    case DE.OItem{x}:
43	      x
44	    case DE.ONat{k}:
45	      Fail{DE.IndexOutOfRange{}}
46	    case DE.OUnit{r}:
47	      Fail{DE.IndexOutOfRange{}}
48	    case DE.OList{xs}:
49	      Fail{DE.IndexOutOfRange{}}
50	
51	def ununit(o: DE.Obs<U32>) -> Result<&2, &2, DE.Error, Unit>:
52	  match o:
53	    case DE.OItem{x}:
54	      Fail{DE.IndexOutOfRange{}}
55	    case DE.ONat{k}:
56	      Fail{DE.IndexOutOfRange{}}
57	    case DE.OUnit{r}:
58	      r
59	    case DE.OList{xs}:
60	      Fail{DE.IndexOutOfRange{}}
61	
62	def unnat(o: DE.Obs<U32>) -> Nat:
63	  match o:
64	    case DE.OItem{x}:
65	      0n
66	    case DE.ONat{k}:
67	      k
68	    case DE.OUnit{r}:
69	      0n
70	    case DE.OList{xs}:
71	      0n
72	
73	def uitem(p: D.DynArray<&2, U32> & DE.Obs<U32>) -> D.DynArray<&2, U32> & Result<&2, &2, DE.Error, U32>:
74	  (a, o) = p
75	  (a, unitem(o))
76	
77	def uunit(p: D.DynArray<&2, U32> & DE.Obs<U32>) -> D.DynArray<&2, U32> & Result<&2, &2, DE.Error, Unit>:
78	  (a, o) = p
79	  (a, ununit(o))
80	
81	def unat(p: D.DynArray<&2, U32> & DE.Obs<U32>) -> D.DynArray<&2, U32> & Nat:
82	  (a, o) = p
83	  (a, unnat(o))
84	
85	def uitem_obs(r: D.DynArray<&2, U32> & Result<&2, &2, DE.Error, U32>) -> {uitem(D.obs_item(U32, r)) == r : D.DynArray<&2, U32> & Result<&2, &2, DE.Error, U32>}:
86	  match r:
87	    case Tuple{a, x}:
88	      {==}
89	
90	def uunit_obs(r: D.DynArray<&2, U32> & Result<&2, &2, DE.Error, Unit>) -> {uunit(D.obs_unit(U32, r)) == r : D.DynArray<&2, U32> & Result<&2, &2, DE.Error, Unit>}:
91	  match r:
92	    case Tuple{a, x}:
93	      {==}
94	
95	def unat_obs(r: D.DynArray<&2, U32> & Nat) -> {unat(D.obs_nat(U32, r)) == r : D.DynArray<&2, U32> & Nat}:
96	  match r:
97	    case Tuple{a, x}:
98	      {==}
99	
100	# ---- reading the pieces of a spec answer ----
101	
102	def p_items(+a: DS.Model<U32>, o: DE.Obs<U32>, +b: DS.Model<U32>, o2: DE.Obs<U32>, e: {(a, o) == (b, o2) : DS.Model<U32> & DE.Obs<U32>}) -> {items(a) == items(b) : List<&2, U32>}:
103	  Equal.cong(DS.Model<U32> & DE.Obs<U32>, List<&2, U32>, p => items(Pair.fst(DS.Model<U32>, DE.Obs<U32>, p)), (a, o), (b, o2), e)
104	
105	def p_lim(+a: DS.Model<U32>, o: DE.Obs<U32>, +b: DS.Model<U32>, o2: DE.Obs<U32>, e: {(a, o) == (b, o2) : DS.Model<U32> & DE.Obs<U32>}) -> {mlim(a) == mlim(b) : Nat}:
106	  Equal.cong(DS.Model<U32> & DE.Obs<U32>, Nat, p => mlim(Pair.fst(DS.Model<U32>, DE.Obs<U32>, p)), (a, o), (b, o2), e)
107	
108	def p_item(+a: DS.Model<U32>, o: DE.Obs<U32>, +b: DS.Model<U32>, o2: DE.Obs<U32>, e: {(a, o) == (b, o2) : DS.Model<U32> & DE.Obs<U32>}) -> {unitem(o) == unitem(o2) : Result<&2, &2, DE.Error, U32>}:
109	  Equal.cong(DS.Model<U32> & DE.Obs<U32>, Result<&2, &2, DE.Error, U32>, p => unitem(Pair.snd(DS.Model<U32>, DE.Obs<U32>, p)), (a, o), (b, o2), e)
110	
111	def p_unit(+a: DS.Model<U32>, o: DE.Obs<U32>, +b: DS.Model<U32>, o2: DE.Obs<U32>, e: {(a, o) == (b, o2) : DS.Model<U32> & DE.Obs<U32>}) -> {ununit(o) == ununit(o2) : Result<&2, &2, DE.Error, Unit>}:
112	  Equal.cong(DS.Model<U32> & DE.Obs<U32>, Result<&2, &2, DE.Error, Unit>, p => ununit(Pair.snd(DS.Model<U32>, DE.Obs<U32>, p)), (a, o), (b, o2), e)
113	
114	def p_nat(+a: DS.Model<U32>, o: DE.Obs<U32>, +b: DS.Model<U32>, o2: DE.Obs<U32>, e: {(a, o) == (b, o2) : DS.Model<U32> & DE.Obs<U32>}) -> {unnat(o) == unnat(o2) : Nat}:
115	  Equal.cong(DS.Model<U32> & DE.Obs<U32>, Nat, p => unnat(Pair.snd(DS.Model<U32>, DE.Obs<U32>, p)), (a, o), (b, o2), e)
116	
117	# ---- facts of a good shadow ----
118	
119	def ws_len(+l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, U32>>, +g: {DAS.good(U32, DAS.Sh{l, d, n, t}) == True{} : Bool}) -> {SC.length(U32, ws(DAS.Sh{l, d, n, t})) == n : Nat}:
120	  LY.lay_len(U32, AR.slots(Maybe<&2, U32>, t), n, DAS.g_lay(U32, l, d, n, t, g))
121	
122	# at most 2^lim words
123	def ws_cap(+l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, U32>>, +g: {DAS.good(U32, DAS.Sh{l, d, n, t}) == True{} : Bool}) -> {Nat.is_le(SC.length(U32, ws(DAS.Sh{l, d, n, t})), SC.pow2(lim(DAS.Sh{l, d, n, t}))) == True{} : Bool}:
124	  %Equal.sym(Nat, SC.length(U32, ws(DAS.Sh{l, d, n, t})), n, ws_len(l, d, n, t, g)) : {Nat.is_le(_, SC.pow2(l)) == True{} : Bool}
125	  N.le_trans(n, SC.pow2(d), SC.pow2(l), DSP.n_le_cap(U32, l, d, n, t, g), N.pow2_mono(d, l, DAS.g_depth(U32, l, d, n, t, g)))
126	
127	def wcap(+w: DAS.Shadow<U32>, +g: {DAS.good(U32, w) == True{} : Bool}) -> {Nat.is_le(SC.length(U32, ws(w)), SC.pow2(lim(w))) == True{} : Bool}:
128	  match w:
129	    case DAS.Sh{+l, +d, +n, +t}:
130	      ws_cap(l, d, n, t, g)
131	
132	# ---- get ----
133	
134	def gsh(+w: DAS.Shadow<U32>, +g: {DAS.good(U32, w) == True{} : Bool}, +q: Nat) -> DAS.Shadow<U32>:
135	  DTR.so_sh(U32, w, DE.Get{q}, DSP.step_ok(U32, w, DE.Get{q}, g))
136	
137	def get_eq(+w: DAS.Shadow<U32>, +g: {DAS.good(U32, w) == True{} : Bool}, +q: Nat) -> {D.get(U32, DAS.real(U32, w), q) == (DAS.real(U32, gsh(w, g, q)), unitem(DTR.so_obs(U32, w, DE.Get{q}, DSP.step_ok(U32, w, DE.Get{q}, g)))) : D.DynArray<&2, U32> & Result<&2, &2, DE.Error, U32>}:
138	  Equal.trans(D.DynArray<&2, U32> & Result<&2, &2, DE.Error, U32>, D.get(U32, DAS.real(U32, w), q), uitem(D.obs_item(U32, D.get(U32, DAS.real(U32, w), q))), (DAS.real(U32, gsh(w, g, q)), unitem(DTR.so_obs(U32, w, DE.Get{q}, DSP.step_ok(U32, w, DE.Get{q}, g)))),
139	    Equal.sym(D.DynArray<&2, U32> & Result<&2, &2, DE.Error, U32>, uitem(D.obs_item(U32, D.get(U32, DAS.real(U32, w), q))), D.get(U32, DAS.real(U32, w), q), uitem_obs(D.get(U32, DAS.real(U32, w), q))),
140	    Equal.cong(D.DynArray<&2, U32> & DE.Obs<U32>, D.DynArray<&2, U32> & Result<&2, &2, DE.Error, U32>, p => uitem(p), D.step(U32, DAS.real(U32, w), DE.Get{q}), (DAS.real(U32, DTR.so_sh(U32, w, DE.Get{q}, DSP.step_ok(U32, w, DE.Get{q}, g))), DTR.so_obs(U32, w, DE.Get{q}, DSP.step_ok(U32, w, DE.Get{q}, g))), DTR.so_step(U32, w, DE.Get{q}, DSP.step_ok(U32, w, DE.Get{q}, g))))
141	
142	def get_good(+w: DAS.Shadow<U32>, +g: {DAS.good(U32, w) == True{} : Bool}, +q: Nat) -> {DAS.good(U32, gsh(w, g, q)) == True{} : Bool}:
143	  DTR.so_good(U32, w, DE.Get{q}, DSP.step_ok(U32, w, DE.Get{q}, g))
144	
145	def get_all(+w: DAS.Shadow<U32>, +g: {DAS.good(U32, w) == True{} : Bool}, +q: Nat) -> {(DAS.model(U32, gsh(w, g, q)), DTR.so_obs(U32, w, DE.Get{q}, DSP.step_ok(U32, w, DE.Get{q}, g))) == (DAS.model(U32, w), DE.OItem{DS.item_result(U32, SC.nth(U32, ws(w), q))}) : DS.Model<U32> & DE.Obs<U32>}:
146	  match w:
147	    case DAS.Sh{+l, +d, +n, +t}:
148	      DTR.so_spec(U32, DAS.Sh{l, d, n, t}, DE.Get{q}, DSP.step_ok(U32, DAS.Sh{l, d, n, t}, DE.Get{q}, g))
149	
150	def get_val(+w: DAS.Shadow<U32>, +g: {DAS.good(U32, w) == True{} : Bool}, +q: Nat) -> {unitem(DTR.so_obs(U32, w, DE.Get{q}, DSP.step_ok(U32, w, DE.Get{q}, g))) == DS.item_result(U32, SC.nth(U32, ws(w), q)) : Result<&2, &2, DE.Error, U32>}:
151	  p_item(DAS.model(U32, gsh(w, g, q)), DTR.so_obs(U32, w, DE.Get{q}, DSP.step_ok(U32, w, DE.Get{q}, g)), DAS.model(U32, w), DE.OItem{DS.item_result(U32, SC.nth(U32, ws(w), q))}, get_all(w, g, q))
152	
153	def get_ws(+w: DAS.Shadow<U32>, +g: {DAS.good(U32, w) == True{} : Bool}, +q: Nat) -> {ws(gsh(w, g, q)) == ws(w) : List<&2, U32>}:
154	  p_items(DAS.model(U32, gsh(w, g, q)), DTR.so_obs(U32, w, DE.Get{q}, DSP.step_ok(U32, w, DE.Get{q}, g)), DAS.model(U32, w), DE.OItem{DS.item_result(U32, SC.nth(U32, ws(w), q))}, get_all(w, g, q))
155	
156	def get_lim(+w: DAS.Shadow<U32>, +g: {DAS.good(U32, w) == True{} : Bool}, +q: Nat) -> {lim(gsh(w, g, q)) == lim(w) : Nat}:
157	  p_lim(DAS.model(U32, gsh(w, g, q)), DTR.so_obs(U32, w, DE.Get{q}, DSP.step_ok(U32, w, DE.Get{q}, g)), DAS.model(U32, w), DE.OItem{DS.item_result(U32, SC.nth(U32, ws(w), q))}, get_all(w, g, q))
158	
159	# ---- length ----
160	
161	def lsh(+w: DAS.Shadow<U32>, +g: {DAS.good(U32, w) == True{} : Bool}) -> DAS.Shadow<U32>:
162	  DTR.so_sh(U32, w, DE.Length{}, DSP.step_ok(U32, w, DE.Length{}, g))
163	
164	def len_eq(+w: DAS.Shadow<U32>, +g: {DAS.good(U32, w) == True{} : Bool}) -> {D.length(U32, DAS.real(U32, w)) == (DAS.real(U32, lsh(w, g)), unnat(DTR.so_obs(U32, w, DE.Length{}, DSP.step_ok(U32, w, DE.Length{}, g)))) : D.DynArray<&2, U32> & Nat}:
165	  Equal.trans(D.DynArray<&2, U32> & Nat, D.length(U32, DAS.real(U32, w)), unat(D.obs_nat(U32, D.length(U32, DAS.real(U32, w)))), (DAS.real(U32, lsh(w, g)), unnat(DTR.so_obs(U32, w, DE.Length{}, DSP.step_ok(U32, w, DE.Length{}, g)))),
166	    Equal.sym(D.DynArray<&2, U32> & Nat, unat(D.obs_nat(U32, D.length(U32, DAS.real(U32, w)))), D.length(U32, DAS.real(U32, w)), unat_obs(D.length(U32, DAS.real(U32, w)))),
167	    Equal.cong(D.DynArray<&2, U32> & DE.Obs<U32>, D.DynArray<&2, U32> & Nat, p => unat(p), D.step(U32, DAS.real(U32, w), DE.Length{}), (DAS.real(U32, DTR.so_sh(U32, w, DE.Length{}, DSP.step_ok(U32, w, DE.Length{}, g))), DTR.so_obs(U32, w, DE.Length{}, DSP.step_ok(U32, w, DE.Length{}, g))), DTR.so_step(U32, w, DE.Length{}, DSP.step_ok(U32, w, DE.Length{}, g))))
168	
169	def len_good(+w: DAS.Shadow<U32>, +g: {DAS.good(U32, w) == True{} : Bool}) -> {DAS.good(U32, lsh(w, g)) == True{} : Bool}:
170	  DTR.so_good(U32, w, DE.Length{}, DSP.step_ok(U32, w, DE.Length{}, g))
171	
172	def len_all(+w: DAS.Shadow<U32>, +g: {DAS.good(U32, w) == True{} : Bool}) -> {(DAS.model(U32, lsh(w, g)), DTR.so_obs(U32, w, DE.Length{}, DSP.step_ok(U32, w, DE.Length{}, g))) == (DAS.model(U32, w), DE.ONat{SC.length(U32, ws(w))}) : DS.Model<U32> & DE.Obs<U32>}:
173	  match w:
174	    case DAS.Sh{+l, +d, +n, +t}:
175	      DTR.so_spec(U32, DAS.Sh{l, d, n, t}, DE.Length{}, DSP.step_ok(U32, DAS.Sh{l, d, n, t}, DE.Length{}, g))
176	
177	def len_val(+w: DAS.Shadow<U32>, +g: {DAS.good(U32, w) == True{} : Bool}) -> {unnat(DTR.so_obs(U32, w, DE.Length{}, DSP.step_ok(U32, w, DE.Length{}, g))) == SC.length(U32, ws(w)) : Nat}:
178	  p_nat(DAS.model(U32, lsh(w, g)), DTR.so_obs(U32, w, DE.Length{}, DSP.step_ok(U32, w, DE.Length{}, g)), DAS.model(U32, w), DE.ONat{SC.length(U32, ws(w))}, len_all(w, g))
179	
180	def len_ws(+w: DAS.Shadow<U32>, +g: {DAS.good(U32, w) == True{} : Bool}) -> {ws(lsh(w, g)) == ws(w) : List<&2, U32>}:
181	  p_items(DAS.model(U32, lsh(w, g)), DTR.so_obs(U32, w, DE.Length{}, DSP.step_ok(U32, w, DE.Length{}, g)), DAS.model(U32, w), DE.ONat{SC.length(U32, ws(w))}, len_all(w, g))
182	
183	def len_lim(+w: DAS.Shadow<U32>, +g: {DAS.good(U32, w) == True{} : Bool}) -> {lim(lsh(w, g)) == lim(w) : Nat}:
184	  p_lim(DAS.model(U32, lsh(w, g)), DTR.so_obs(U32, w, DE.Length{}, DSP.step_ok(U32, w, DE.Length{}, g)), DAS.model(U32, w), DE.ONat{SC.length(U32, ws(w))}, len_all(w, g))
185	
186	def dep(w: DAS.Shadow<U32>) -> Nat:
187	  match w:
188	    case DAS.Sh{l, d, n, t}:
189	      d
190	
191	# ---- set (an index below the length) ----
192	
193	def sp_set(+l: Nat, +d: Nat, +xs: List<&2, U32>, +q: Nat, +v: U32, +h: {Nat.is_lt(q, SC.length(U32, xs)) == True{} : Bool}) -> {DS.step_parts(U32, l, d, xs, DE.Set{q, v}) == (DS.M{l, d, SC.update(U32, xs, q, v)}, DE.OUnit{Done{Unit{}}}) : DS.Model<U32> & DE.Obs<U32>}:
194	  %Equal.sym(Bool, Nat.is_lt(q, SC.length(U32, xs)), True{}, h) : {Bool.pick(DS.Model<U32> & DE.Obs<U32>, _, (DS.M{l, d, SC.update(U32, xs, q, v)}, DE.OUnit{DS.ok_unit()}), (DS.M{l, d, xs}, DE.OUnit{Fail{DE.IndexOutOfRange{}}})) == (DS.M{l, d, SC.update(U32, xs, q, v)}, DE.OUnit{Done{Unit{}}}) : DS.Model<U32> & DE.Obs<U32>}
195	  {==}
196	
197	def ssh(+w: DAS.Shadow<U32>, +g: {DAS.good(U32, w) == True{} : Bool}, +q: Nat, +v: U32) -> DAS.Shadow<U32>:
198	  DTR.so_sh(U32, w, DE.Set{q, v}, DSP.step_ok(U32, w, DE.Set{q, v}, g))
199	
200	def set_eq(+w: DAS.Shadow<U32>, +g: {DAS.good(U32, w) == True{} : Bool}, +q: Nat, +v: U32) -> {D.set(U32, DAS.real(U32, w), q, v) == (DAS.real(U32, ssh(w, g, q, v)), ununit(DTR.so_obs(U32, w, DE.Set{q, v}, DSP.step_ok(U32, w, DE.Set{q, v}, g)))) : D.DynArray<&2, U32> & Result<&2, &2, DE.Error, Unit>}:
201	  Equal.trans(D.DynArray<&2, U32> & Result<&2, &2, DE.Error, Unit>, D.set(U32, DAS.real(U32, w), q, v), uunit(D.obs_unit(U32, D.set(U32, DAS.real(U32, w), q, v))), (DAS.real(U32, ssh(w, g, q, v)), ununit(DTR.so_obs(U32, w, DE.Set{q, v}, DSP.step_ok(U32, w, DE.Set{q, v}, g)))),
202	    Equal.sym(D.DynArray<&2, U32> & Result<&2, &2, DE.Error, Unit>, uunit(D.obs_unit(U32, D.set(U32, DAS.real(U32, w), q, v))), D.set(U32, DAS.real(U32, w), q, v), uunit_obs(D.set(U32, DAS.real(U32, w), q, v))),
203	    Equal.cong(D.DynArray<&2, U32> & DE.Obs<U32>, D.DynArray<&2, U32> & Result<&2, &2, DE.Error, Unit>, p => uunit(p), D.step(U32, DAS.real(U32, w), DE.Set{q, v}), (DAS.real(U32, DTR.so_sh(U32, w, DE.Set{q, v}, DSP.step_ok(U32, w, DE.Set{q, v}, g))), DTR.so_obs(U32, w, DE.Set{q, v}, DSP.step_ok(U32, w, DE.Set{q, v}, g))), DTR.so_step(U32, w, DE.Set{q, v}, DSP.step_ok(U32, w, DE.Set{q, v}, g))))
204	
205	def set_good(+w: DAS.Shadow<U32>, +g: {DAS.good(U32, w) == True{} : Bool}, +q: Nat, +v: U32) -> {DAS.good(U32, ssh(w, g, q, v)) == True{} : Bool}:
206	  DTR.so_good(U32, w, DE.Set{q, v}, DSP.step_ok(U32, w, DE.Set{q, v}, g))
207	
208	def set_all(+w: DAS.Shadow<U32>, +g: {DAS.good(U32, w) == True{} : Bool}, +q: Nat, +v: U32, +h: {Nat.is_lt(q, SC.length(U32, ws(w))) == True{} : Bool}) -> {(DAS.model(U32, ssh(w, g, q, v)), DTR.so_obs(U32, w, DE.Set{q, v}, DSP.step_ok(U32, w, DE.Set{q, v}, g))) == (DS.M{lim(w), dep(w), SC.update(U32, ws(w), q, v)}, DE.OUnit{Done{Unit{}}}) : DS.Model<U32> & DE.Obs<U32>}:
209	  match w:
210	    case DAS.Sh{+l, +d, +n, +t}:
211	      Equal.trans(DS.Model<U32> & DE.Obs<U32>, (DAS.model(U32, ssh(DAS.Sh{l, d, n, t}, g, q, v)), DTR.so_obs(U32, DAS.Sh{l, d, n, t}, DE.Set{q, v}, DSP.step_ok(U32, DAS.Sh{l, d, n, t}, DE.Set{q, v}, g))), DS.step_parts(U32, l, d, LY.somes(U32, AR.slots(Maybe<&2, U32>, t)), DE.Set{q, v}), (DS.M{l, d, SC.update(U32, LY.somes(U32, AR.slots(Maybe<&2, U32>, t)), q, v)}, DE.OUnit{Done{Unit{}}}),
212	        DTR.so_spec(U32, DAS.Sh{l, d, n, t}, DE.Set{q, v}, DSP.step_ok(U32, DAS.Sh{l, d, n, t}, DE.Set{q, v}, g)), sp_set(l, d, LY.somes(U32, AR.slots(Maybe<&2, U32>, t)), q, v, h))
213	
214	def set_val(+w: DAS.Shadow<U32>, +g: {DAS.good(U32, w) == True{} : Bool}, +q: Nat, +v: U32, +h: {Nat.is_lt(q, SC.length(U32, ws(w))) == True{} : Bool}) -> {ununit(DTR.so_obs(U32, w, DE.Set{q, v}, DSP.step_ok(U32, w, DE.Set{q, v}, g))) == Done{Unit{}} : Result<&2, &2, DE.Error, Unit>}:
215	  p_unit(DAS.model(U32, ssh(w, g, q, v)), DTR.so_obs(U32, w, DE.Set{q, v}, DSP.step_ok(U32, w, DE.Set{q, v}, g)), DS.M{lim(w), dep(w), SC.update(U32, ws(w), q, v)}, DE.OUnit{Done{Unit{}}}, set_all(w, g, q, v, h))
216	
217	def set_ws(+w: DAS.Shadow<U32>, +g: {DAS.good(U32, w) == True{} : Bool}, +q: Nat, +v: U32, +h: {Nat.is_lt(q, SC.length(U32, ws(w))) == True{} : Bool}) -> {ws(ssh(w, g, q, v)) == SC.update(U32, ws(w), q, v) : List<&2, U32>}:
218	  p_items(DAS.model(U32, ssh(w, g, q, v)), DTR.so_obs(U32, w, DE.Set{q, v}, DSP.step_ok(U32, w, DE.Set{q, v}, g)), DS.M{lim(w), dep(w), SC.update(U32, ws(w), q, v)}, DE.OUnit{Done{Unit{}}}, set_all(w, g, q, v, h))
219	
220	def set_lim(+w: DAS.Shadow<U32>, +g: {DAS.good(U32, w) == True{} : Bool}, +q: Nat, +v: U32, +h: {Nat.is_lt(q, SC.length(U32, ws(w))) == True{} : Bool}) -> {lim(ssh(w, g, q, v)) == lim(w) : Nat}:
221	  p_lim(DAS.model(U32, ssh(w, g, q, v)), DTR.so_obs(U32, w, DE.Set{q, v}, DSP.step_ok(U32, w, DE.Set{q, v}, g)), DS.M{lim(w), dep(w), SC.update(U32, ws(w), q, v)}, DE.OUnit{Done{Unit{}}}, set_all(w, g, q, v, h))
222	
223	# ---- push ----
224	
225	
226	# below the depth limit a push succeeds (in place, or after one doubling)
227	def sp_push_c(+l: Nat, +d: Nat, +xs: List<&2, U32>, +v: U32, c: Bool, +ec: {Nat.is_lt(d, l) == c : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +h: {Nat.is_lt(SC.length(U32, xs), SC.pow2(l)) == True{} : Bool}, +e1: {Nat.is_lt(SC.length(U32, xs), SC.pow2(d)) == False{} : Bool}) -> {Bool.pick(DS.Model<U32> & DE.Obs<U32>, Nat.is_lt(d, l), (DS.M{l, 1n+d, SC.snoc(U32, xs, v)}, DE.OUnit{DS.ok_unit()}), (DS.M{l, d, xs}, DE.OUnit{Fail{DE.CapacityExceeded{}}})) == (DS.M{l, 1n+d, SC.snoc(U32, xs, v)}, DE.OUnit{Done{Unit{}}}) : DS.Model<U32> & DE.Obs<U32>}:
228	  match c:
229	    case True{}:
230	      %Equal.sym(Bool, Nat.is_lt(d, l), True{}, ec) : {Bool.pick(DS.Model<U32> & DE.Obs<U32>, _, (DS.M{l, 1n+d, SC.snoc(U32, xs, v)}, DE.OUnit{DS.ok_unit()}), (DS.M{l, d, xs}, DE.OUnit{Fail{DE.CapacityExceeded{}}})) == (DS.M{l, 1n+d, SC.snoc(U32, xs, v)}, DE.OUnit{Done{Unit{}}}) : DS.Model<U32> & DE.Obs<U32>}
231	      {==}
232	    case False{}:
233	      +edl = N.le_antisym(d, l, hd, N.not_lt_le(d, l, ec))
234	      Empty.absurd({Bool.pick(DS.Model<U32> & DE.Obs<U32>, Nat.is_lt(d, l), (DS.M{l, 1n+d, SC.snoc(U32, xs, v)}, DE.OUnit{DS.ok_unit()}), (DS.M{l, d, xs}, DE.OUnit{Fail{DE.CapacityExceeded{}}})) == (DS.M{l, 1n+d, SC.snoc(U32, xs, v)}, DE.OUnit{Done{Unit{}}}) : DS.Model<U32> & DE.Obs<U32>}, L.true_not_false(Nat.is_lt(SC.length(U32, xs), SC.pow2(d)), L.subst(Nat, x => {Nat.is_lt(SC.length(U32, xs), SC.pow2(x)) == True{} : Bool}, l, d, Equal.sym(Nat, d, l, edl), h), e1))
235	
236	def sp_push_b(+l: Nat, +d: Nat, +xs: List<&2, U32>, +v: U32, b: Bool, +eb: {Nat.is_lt(SC.length(U32, xs), SC.pow2(d)) == b : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +h: {Nat.is_lt(SC.length(U32, xs), SC.pow2(l)) == True{} : Bool}) -> {DS.step_parts(U32, l, d, xs, DE.Push{v}) == (DS.M{l, Bool.pick(Nat, Nat.is_lt(SC.length(U32, xs), SC.pow2(d)), d, 1n+d), SC.snoc(U32, xs, v)}, DE.OUnit{Done{Unit{}}}) : DS.Model<U32> & DE.Obs<U32>}:
237	  match b:
238	    case True{}:
239	      %Equal.sym(Bool, Nat.is_lt(SC.length(U32, xs), SC.pow2(d)), True{}, eb) : {Bool.pick(DS.Model<U32> & DE.Obs<U32>, _, (DS.M{l, d, SC.snoc(U32, xs, v)}, DE.OUnit{DS.ok_unit()}), Bool.pick(DS.Model<U32> & DE.Obs<U32>, Nat.is_lt(d, l), (DS.M{l, 1n+d, SC.snoc(U32, xs, v)}, DE.OUnit{DS.ok_unit()}), (DS.M{l, d, xs}, DE.OUnit{Fail{DE.CapacityExceeded{}}}))) == (DS.M{l, Bool.pick(Nat, _, d, 1n+d), SC.snoc(U32, xs, v)}, DE.OUnit{Done{Unit{}}}) : DS.Model<U32> & DE.Obs<U32>}
240	      {==}
241	    case False{}:
242	      %Equal.sym(Bool, Nat.is_lt(SC.length(U32, xs), SC.pow2(d)), False{}, eb) : {Bool.pick(DS.Model<U32> & DE.Obs<U32>, _, (DS.M{l, d, SC.snoc(U32, xs, v)}, DE.OUnit{DS.ok_unit()}), Bool.pick(DS.Model<U32> & DE.Obs<U32>, Nat.is_lt(d, l), (DS.M{l, 1n+d, SC.snoc(U32, xs, v)}, DE.OUnit{DS.ok_unit()}), (DS.M{l, d, xs}, DE.OUnit{Fail{DE.CapacityExceeded{}}}))) == (DS.M{l, Bool.pick(Nat, _, d, 1n+d), SC.snoc(U32, xs, v)}, DE.OUnit{Done{Unit{}}}) : DS.Model<U32> & DE.Obs<U32>}
243	      sp_push_c(l, d, xs, v, Nat.is_lt(d, l), {==}, hd, h, eb)
244	
245	# at the depth limit with every slot used a push is rejected
246	def sp_full_c(+l: Nat, +d: Nat, +xs: List<&2, U32>, +v: U32, c: Bool, +ec: {Nat.is_lt(d, l) == c : Bool}, +hc: {Nat.is_le(SC.length(U32, xs), SC.pow2(d)) == True{} : Bool}, +h: {Nat.is_lt(SC.length(U32, xs), SC.pow2(l)) == False{} : Bool}) -> {Bool.pick(DS.Model<U32> & DE.Obs<U32>, Nat.is_lt(d, l), (DS.M{l, 1n+d, SC.snoc(U32, xs, v)}, DE.OUnit{DS.ok_unit()}), (DS.M{l, d, xs}, DE.OUnit{Fail{DE.CapacityExceeded{}}})) == (DS.M{l, d, xs}, DE.OUnit{Fail{DE.CapacityExceeded{}}}) : DS.Model<U32> & DE.Obs<U32>}:
247	  match c:
248	    case False{}:
249	      %Equal.sym(Bool, Nat.is_lt(d, l), False{}, ec) : {Bool.pick(DS.Model<U32> & DE.Obs<U32>, _, (DS.M{l, 1n+d, SC.snoc(U32, xs, v)}, DE.OUnit{DS.ok_unit()}), (DS.M{l, d, xs}, DE.OUnit{Fail{DE.CapacityExceeded{}}})) == (DS.M{l, d, xs}, DE.OUnit{Fail{DE.CapacityExceeded{}}}) : DS.Model<U32> & DE.Obs<U32>}
250	      {==}
251	    case True{}:
252	      Empty.absurd({Bool.pick(DS.Model<U32> & DE.Obs<U32>, Nat.is_lt(d, l), (DS.M{l, 1n+d, SC.snoc(U32, xs, v)}, DE.OUnit{DS.ok_unit()}), (DS.M{l, d, xs}, DE.OUnit{Fail{DE.CapacityExceeded{}}})) == (DS.M{l, d, xs}, DE.OUnit{Fail{DE.CapacityExceeded{}}}) : DS.Model<U32> & DE.Obs<U32>}, L.true_not_false(Nat.is_lt(SC.length(U32, xs), SC.pow2(l)), N.le_lt_trans(SC.length(U32, xs), SC.pow2(d), SC.pow2(l), hc, N.pow2_strict(d, l, ec)), h))
253	
254	def sp_full(+l: Nat, +d: Nat, +xs: List<&2, U32>, +v: U32, +hc: {Nat.is_le(SC.length(U32, xs), SC.pow2(d)) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +h: {Nat.is_lt(SC.length(U32, xs), SC.pow2(l)) == False{} : Bool}) -> {DS.step_parts(U32, l, d, xs, DE.Push{v}) == (DS.M{l, d, xs}, DE.OUnit{Fail{DE.CapacityExceeded{}}}) : DS.Model<U32> & DE.Obs<U32>}:
255	  +h1 = N.le_not_lt(SC.length(U32, xs), SC.pow2(d), N.le_trans(SC.pow2(d), SC.pow2(l), SC.length(U32, xs), N.pow2_mono(d, l, hd), N.not_lt_le(SC.length(U32, xs), SC.pow2(l), h)))
256	  %Equal.sym(Bool, Nat.is_lt(SC.length(U32, xs), SC.pow2(d)), False{}, h1) : {Bool.pick(DS.Model<U32> & DE.Obs<U32>, _, (DS.M{l, d, SC.snoc(U32, xs, v)}, DE.OUnit{DS.ok_unit()}), Bool.pick(DS.Model<U32> & DE.Obs<U32>, Nat.is_lt(d, l), (DS.M{l, 1n+d, SC.snoc(U32, xs, v)}, DE.OUnit{DS.ok_unit()}), (DS.M{l, d, xs}, DE.OUnit{Fail{DE.CapacityExceeded{}}}))) == (DS.M{l, d, xs}, DE.OUnit{Fail{DE.CapacityExceeded{}}}) : DS.Model<U32> & DE.Obs<U32>}
257	  sp_full_c(l, d, xs, v, Nat.is_lt(d, l), {==}, hc, h)
258	
259	def psh(+w: DAS.Shadow<U32>, +g: {DAS.good(U32, w) == True{} : Bool}, +v: U32) -> DAS.Shadow<U32>:
260	  DTR.so_sh(U32, w, DE.Push{v}, DSP.step_ok(U32, w, DE.Push{v}, g))
261	
262	def push_eq(+w: DAS.Shadow<U32>, +g: {DAS.good(U32, w) == True{} : Bool}, +v: U32) -> {D.push(U32, DAS.real(U32, w), v) == (DAS.real(U32, psh(w, g, v)), ununit(DTR.so_obs(U32, w, DE.Push{v}, DSP.step_ok(U32, w, DE.Push{v}, g)))) : D.DynArray<&2, U32> & Result<&2, &2, DE.Error, Unit>}:
263	  Equal.trans(D.DynArray<&2, U32> & Result<&2, &2, DE.Error, Unit>, D.push(U32, DAS.real(U32, w), v), uunit(D.obs_unit(U32, D.push(U32, DAS.real(U32, w), v))), (DAS.real(U32, psh(w, g, v)), ununit(DTR.so_obs(U32, w, DE.Push{v}, DSP.step_ok(U32, w, DE.Push{v}, g)))),
264	    Equal.sym(D.DynArray<&2, U32> & Result<&2, &2, DE.Error, Unit>, uunit(D.obs_unit(U32, D.push(U32, DAS.real(U32, w), v))), D.push(U32, DAS.real(U32, w), v), uunit_obs(D.push(U32, DAS.real(U32, w), v))),
265	    Equal.cong(D.DynArray<&2, U32> & DE.Obs<U32>, D.DynArray<&2, U32> & Result<&2, &2, DE.Error, Unit>, p => uunit(p), D.step(U32, DAS.real(U32, w), DE.Push{v}), (DAS.real(U32, DTR.so_sh(U32, w, DE.Push{v}, DSP.step_ok(U32, w, DE.Push{v}, g))), DTR.so_obs(U32, w, DE.Push{v}, DSP.step_ok(U32, w, DE.Push{v}, g))), DTR.so_step(U32, w, DE.Push{v}, DSP.step_ok(U32, w, DE.Push{v}, g))))
266	
267	def push_good(+w: DAS.Shadow<U32>, +g: {DAS.good(U32, w) == True{} : Bool}, +v: U32) -> {DAS.good(U32, psh(w, g, v)) == True{} : Bool}:
268	  DTR.so_good(U32, w, DE.Push{v}, DSP.step_ok(U32, w, DE.Push{v}, g))
269	
270	
271	def push_all(+w: DAS.Shadow<U32>, +g: {DAS.good(U32, w) == True{} : Bool}, +v: U32, +h: {Nat.is_lt(SC.length(U32, ws(w)), SC.pow2(lim(w))) == True{} : Bool}) -> {(DAS.model(U32, psh(w, g, v)), DTR.so_obs(U32, w, DE.Push{v}, DSP.step_ok(U32, w, DE.Push{v}, g))) == (DS.M{lim(w), Bool.pick(Nat, Nat.is_lt(SC.length(U32, ws(w)), SC.pow2(dep(w))), dep(w), 1n+dep(w)), SC.snoc(U32, ws(w), v)}, DE.OUnit{Done{Unit{}}}) : DS.Model<U32> & DE.Obs<U32>}:
272	  match w:
273	    case DAS.Sh{+l, +d, +n, +t}:
274	      Equal.trans(DS.Model<U32> & DE.Obs<U32>, (DAS.model(U32, psh(DAS.Sh{l, d, n, t}, g, v)), DTR.so_obs(U32, DAS.Sh{l, d, n, t}, DE.Push{v}, DSP.step_ok(U32, DAS.Sh{l, d, n, t}, DE.Push{v}, g))), DS.step_parts(U32, l, d, LY.somes(U32, AR.slots(Maybe<&2, U32>, t)), DE.Push{v}), (DS.M{l, Bool.pick(Nat, Nat.is_lt(SC.length(U32, LY.somes(U32, AR.slots(Maybe<&2, U32>, t))), SC.pow2(d)), d, 1n+d), SC.snoc(U32, LY.somes(U32, AR.slots(Maybe<&2, U32>, t)), v)}, DE.OUnit{Done{Unit{}}}),
275	        DTR.so_spec(U32, DAS.Sh{l, d, n, t}, DE.Push{v}, DSP.step_ok(U32, DAS.Sh{l, d, n, t}, DE.Push{v}, g)), sp_push_b(l, d, LY.somes(U32, AR.slots(Maybe<&2, U32>, t)), v, Nat.is_lt(SC.length(U32, LY.somes(U32, AR.slots(Maybe<&2, U32>, t))), SC.pow2(d)), {==}, DAS.g_depth(U32, l, d, n, t, g), h))
276	
277	def push_val(+w: DAS.Shadow<U32>, +g: {DAS.good(U32, w) == True{} : Bool}, +v: U32, +h: {Nat.is_lt(SC.length(U32, ws(w)), SC.pow2(lim(w))) == True{} : Bool}) -> {ununit(DTR.so_obs(U32, w, DE.Push{v}, DSP.step_ok(U32, w, DE.Push{v}, g))) == Done{Unit{}} : Result<&2, &2, DE.Error, Unit>}:
278	  p_unit(DAS.model(U32, psh(w, g, v)), DTR.so_obs(U32, w, DE.Push{v}, DSP.step_ok(U32, w, DE.Push{v}, g)), DS.M{lim(w), Bool.pick(Nat, Nat.is_lt(SC.length(U32, ws(w)), SC.pow2(dep(w))), dep(w), 1n+dep(w)), SC.snoc(U32, ws(w), v)}, DE.OUnit{Done{Unit{}}}, push_all(w, g, v, h))
279	
280	def push_ws(+w: DAS.Shadow<U32>, +g: {DAS.good(U32, w) == True{} : Bool}, +v: U32, +h: {Nat.is_lt(SC.length(U32, ws(w)), SC.pow2(lim(w))) == True{} : Bool}) -> {ws(psh(w, g, v)) == SC.snoc(U32, ws(w), v) : List<&2, U32>}:
281	  p_items(DAS.model(U32, psh(w, g, v)), DTR.so_obs(U32, w, DE.Push{v}, DSP.step_ok(U32, w, DE.Push{v}, g)), DS.M{lim(w), Bool.pick(Nat, Nat.is_lt(SC.length(U32, ws(w)), SC.pow2(dep(w))), dep(w), 1n+dep(w)), SC.snoc(U32, ws(w), v)}, DE.OUnit{Done{Unit{}}}, push_all(w, g, v, h))
282	
283	def push_lim(+w: DAS.Shadow<U32>, +g: {DAS.good(U32, w) == True{} : Bool}, +v: U32, +h: {Nat.is_lt(SC.length(U32, ws(w)), SC.pow2(lim(w))) == True{} : Bool}) -> {lim(psh(w, g, v)) == lim(w) : Nat}:
284	  p_lim(DAS.model(U32, psh(w, g, v)), DTR.so_obs(U32, w, DE.Push{v}, DSP.step_ok(U32, w, DE.Push{v}, g)), DS.M{lim(w), Bool.pick(Nat, Nat.is_lt(SC.length(U32, ws(w)), SC.pow2(dep(w))), dep(w), 1n+dep(w)), SC.snoc(U32, ws(w), v)}, DE.OUnit{Done{Unit{}}}, push_all(w, g, v, h))
285	
286	def full_all(+w: DAS.Shadow<U32>, +g: {DAS.good(U32, w) == True{} : Bool}, +v: U32, +h: {Nat.is_lt(SC.length(U32, ws(w)), SC.pow2(lim(w))) == False{} : Bool}) -> {(DAS.model(U32, psh(w, g, v)), DTR.so_obs(U32, w, DE.Push{v}, DSP.step_ok(U32, w, DE.Push{v}, g))) == (DS.M{lim(w), dep(w), ws(w)}, DE.OUnit{Fail{DE.CapacityExceeded{}}}) : DS.Model<U32> & DE.Obs<U32>}:
287	  match w:
288	    case DAS.Sh{+l, +d, +n, +t}:
289	      +hc = L.subst(Nat, x => {Nat.is_le(x, SC.pow2(d)) == True{} : Bool}, n, SC.length(U32, LY.somes(U32, AR.slots(Maybe<&2, U32>, t))), Equal.sym(Nat, SC.length(U32, LY.somes(U32, AR.slots(Maybe<&2, U32>, t))), n, ws_len(l, d, n, t, g)), DSP.n_le_cap(U32, l, d, n, t, g))
290	      Equal.trans(DS.Model<U32> & DE.Obs<U32>, (DAS.model(U32, psh(DAS.Sh{l, d, n, t}, g, v)), DTR.so_obs(U32, DAS.Sh{l, d, n, t}, DE.Push{v}, DSP.step_ok(U32, DAS.Sh{l, d, n, t}, DE.Push{v}, g))), DS.step_parts(U32, l, d, LY.somes(U32, AR.slots(Maybe<&2, U32>, t)), DE.Push{v}), (DS.M{l, d, LY.somes(U32, AR.slots(Maybe<&2, U32>, t))}, DE.OUnit{Fail{DE.CapacityExceeded{}}}),
291	        DTR.so_spec(U32, DAS.Sh{l, d, n, t}, DE.Push{v}, DSP.step_ok(U32, DAS.Sh{l, d, n, t}, DE.Push{v}, g)), sp_full(l, d, LY.somes(U32, AR.slots(Maybe<&2, U32>, t)), v, hc, DAS.g_depth(U32, l, d, n, t, g), h))
292	
293	def full_val(+w: DAS.Shadow<U32>, +g: {DAS.good(U32, w) == True{} : Bool}, +v: U32, +h: {Nat.is_lt(SC.length(U32, ws(w)), SC.pow2(lim(w))) == False{} : Bool}) -> {ununit(DTR.so_obs(U32, w, DE.Push{v}, DSP.step_ok(U32, w, DE.Push{v}, g))) == Fail{DE.CapacityExceeded{}} : Result<&2, &2, DE.Error, Unit>}:
294	  p_unit(DAS.model(U32, psh(w, g, v)), DTR.so_obs(U32, w, DE.Push{v}, DSP.step_ok(U32, w, DE.Push{v}, g)), DS.M{lim(w), dep(w), ws(w)}, DE.OUnit{Fail{DE.CapacityExceeded{}}}, full_all(w, g, v, h))
295	
296	def full_ws(+w: DAS.Shadow<U32>, +g: {DAS.good(U32, w) == True{} : Bool}, +v: U32, +h: {Nat.is_lt(SC.length(U32, ws(w)), SC.pow2(lim(w))) == False{} : Bool}) -> {ws(psh(w, g, v)) == ws(w) : List<&2, U32>}:
297	  p_items(DAS.model(U32, psh(w, g, v)), DTR.so_obs(U32, w, DE.Push{v}, DSP.step_ok(U32, w, DE.Push{v}, g)), DS.M{lim(w), dep(w), ws(w)}, DE.OUnit{Fail{DE.CapacityExceeded{}}}, full_all(w, g, v, h))
298	
299	def full_lim(+w: DAS.Shadow<U32>, +g: {DAS.good(U32, w) == True{} : Bool}, +v: U32, +h: {Nat.is_lt(SC.length(U32, ws(w)), SC.pow2(lim(w))) == False{} : Bool}) -> {lim(psh(w, g, v)) == lim(w) : Nat}:
300	  p_lim(DAS.model(U32, psh(w, g, v)), DTR.so_obs(U32, w, DE.Push{v}, DSP.step_ok(U32, w, DE.Push{v}, g)), DS.M{lim(w), dep(w), ws(w)}, DE.OUnit{Fail{DE.CapacityExceeded{}}}, full_all(w, g, v, h))
301	
302	# ---- clear ----
303	
304	def csh(+w: DAS.Shadow<U32>, +g: {DAS.good(U32, w) == True{} : Bool}) -> DAS.Shadow<U32>:
305	  DTR.so_sh(U32, w, DE.Clear{}, DSP.step_ok(U32, w, DE.Clear{}, g))
306	
307	def clear_eq(+w: DAS.Shadow<U32>, +g: {DAS.good(U32, w) == True{} : Bool}) -> {D.clear(U32, DAS.real(U32, w)) == DAS.real(U32, csh(w, g)) : D.DynArray<&2, U32>}:
308	  L.pair_fst(D.DynArray<&2, U32>, DE.Obs<U32>, D.clear(U32, DAS.real(U32, w)), DE.OUnit{Done{Unit{}}}, DAS.real(U32, csh(w, g)), DTR.so_obs(U32, w, DE.Clear{}, DSP.step_ok(U32, w, DE.Clear{}, g)), DTR.so_step(U32, w, DE.Clear{}, DSP.step_ok(U32, w, DE.Clear{}, g)))
309	
310	def clear_good(+w: DAS.Shadow<U32>, +g: {DAS.good(U32, w) == True{} : Bool}) -> {DAS.good(U32, csh(w, g)) == True{} : Bool}:
311	  DTR.so_good(U32, w, DE.Clear{}, DSP.step_ok(U32, w, DE.Clear{}, g))
312	
313	def clear_all(+w: DAS.Shadow<U32>, +g: {DAS.good(U32, w) == True{} : Bool}) -> {(DAS.model(U32, csh(w, g)), DTR.so_obs(U32, w, DE.Clear{}, DSP.step_ok(U32, w, DE.Clear{}, g))) == (DS.M{lim(w), dep(w), Nil{}}, DE.OUnit{Done{Unit{}}}) : DS.Model<U32> & DE.Obs<U32>}:
314	  match w:
315	    case DAS.Sh{+l, +d, +n, +t}:
316	      DTR.so_spec(U32, DAS.Sh{l, d, n, t}, DE.Clear{}, DSP.step_ok(U32, DAS.Sh{l, d, n, t}, DE.Clear{}, g))
317	
318	def clear_ws(+w: DAS.Shadow<U32>, +g: {DAS.good(U32, w) == True{} : Bool}) -> {ws(csh(w, g)) == Nil{} : List<&2, U32>}:
319	  p_items(DAS.model(U32, csh(w, g)), DTR.so_obs(U32, w, DE.Clear{}, DSP.step_ok(U32, w, DE.Clear{}, g)), DS.M{lim(w), dep(w), Nil{}}, DE.OUnit{Done{Unit{}}}, clear_all(w, g))
320	
321	def clear_lim(+w: DAS.Shadow<U32>, +g: {DAS.good(U32, w) == True{} : Bool}) -> {lim(csh(w, g)) == lim(w) : Nat}:
322	  p_lim(DAS.model(U32, csh(w, g)), DTR.so_obs(U32, w, DE.Clear{}, DSP.step_ok(U32, w, DE.Clear{}, g)), DS.M{lim(w), dep(w), Nil{}}, DE.OUnit{Done{Unit{}}}, clear_all(w, g))