proofs/containers/bitlist/da.bend
bend-collections-laws-containers@1.0.0.0 · 322 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/array.bend as AR
5import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
6import bend-collections-laws-containers@1.0.0.0/src/containers/dynamic_array.bend as D
7import bend-collections-laws-containers@1.0.0.0/src/containers/types/dynamic_array.bend as DE
8import bend-collections-laws-containers@1.0.0.0/spec/containers/dynamic_array.bend as DS
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/layout.bend as LY
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/state.bend as DAS
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/steps.bend as DSP
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/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
23def items(m: DS.Model<U32>) -> List<&2, U32>:
24 match m:
25 case DS.M{l, d, xs}:
26 xs
27
28def 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.
34def ws(w: DAS.Shadow<U32>) -> List<&2, U32>:
35 items(DAS.model(U32, w))
36
37def lim(w: DAS.Shadow<U32>) -> Nat:
38 mlim(DAS.model(U32, w))
39
40def 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
51def 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
62def 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
73def 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
77def 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
81def unat(p: D.DynArray<&2, U32> & DE.Obs<U32>) -> D.DynArray<&2, U32> & Nat:
82 (a, o) = p
83 (a, unnat(o))
84
85def 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
90def 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
95def 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
102def 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
105def 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
108def 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
111def 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
114def 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
119def 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
123def 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
127def 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
134def 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
137def 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
142def 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
145def 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
150def 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
153def 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
156def 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
161def 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
164def 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
169def 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
172def 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
177def 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
180def 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
183def 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
186def 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
193def 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
197def 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
200def 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
205def 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
208def 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
214def 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
217def 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
220def 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)
227def 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
236def 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
246def 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
254def 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
259def 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
262def 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
267def 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
271def 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
277def 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
280def 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
283def 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
286def 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
293def 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
296def 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
299def 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
304def 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
307def 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
310def 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
313def 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
318def 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
321def 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))