proofs/containers/hash_table/state.bend
bend-collections-laws-containers@1.0.0.0 · 345 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/spec/containers/hash_table.bend as S
7import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32div.bend as UD
8import bend-collections-laws-containers@1.0.0.0/src/containers/hash_table.bend as H
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/table.bend as TB
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/buckets.bend as B
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/cyc.bend as CY
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/inv.bend as IV
13import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat_list.bend as NL
14import bend-collections-laws-containers@1.0.0.0/proofs/lib/words32.bend as W32
15
16# The hash map as a Data shadow: its U32 fields, the table and arena
17# exponents k (2^k buckets) and sd (2^sd slots), and a mirror tree for each
18# array. real(sh) is the HashMap<&2, V> the implementation holds.
19
20type Sh<-V: Data> is Data:
21 HS{n: U32, k: Nat, td: U32, fresh: U32, sz: U32, sd: Nat, sdU: U32, free: U32, tabT: AR.Tree<U32>, ksT: AR.Tree<String>, vsT: AR.Tree<Maybe<&2, V>>, nxT: AR.Tree<U32>}
22
23def real(~V: Data, sh: Sh<V>) -> H.HashMap<&2, V>:
24 match sh:
25 case HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}:
26 H.HM{n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT)}
27
28# ---- the abstraction ----
29
30def some_b(~V: Data, m: Maybe<&2, V>) -> Bool:
31 match m:
32 case None{}:
33 False{}
34 case Some{v}:
35 True{}
36
37def lvs(~V: Data, vsl: List<&2, Maybe<&2, V>>) -> List<&2, Bool>:
38 match vsl:
39 case Nil{}:
40 Nil{}
41 case Con{m, t}:
42 Con{some_b(~V, m), lvs(~V, t)}
43
44def nthm(~V: Data, vsl: List<&2, Maybe<&2, V>>, +i: Nat) -> Maybe<&2, V>:
45 match vsl i:
46 case Nil{} _:
47 None{}
48 case Con{m, t} 0n:
49 m
50 case Con{m, t} 1n+p:
51 nthm(~V, t, p)
52
53def ent_m(~V: Data, +k: String, m: Maybe<&2, V>) -> List<&2, S.Entry<V>>:
54 match m:
55 case None{}:
56 Nil{}
57 case Some{v}:
58 Con{S.E{k, v}, Nil{}}
59
60# the entry of a bucket
61def ent(~V: Data, b: B.Bk, +vsl: List<&2, Maybe<&2, V>>) -> List<&2, S.Entry<V>>:
62 match b:
63 case B.BE{}:
64 Nil{}
65 case B.BF{w, +l, +k}:
66 ent_m(~V, k, nthm(~V, vsl, UD.v(H.slot(l))))
67
68# the entries of buckets j .. j + m - 1, in bucket order
69def absm(~V: Data, +bs: List<&2, B.Bk>, +vsl: List<&2, Maybe<&2, V>>, +m: Nat, +j: Nat) -> List<&2, S.Entry<V>>:
70 match m:
71 case 0n:
72 Nil{}
73 case 1n+p:
74 SC.append(S.Entry<V>, ent(~V, B.at(bs, j), vsl), absm(~V, bs, vsl, p, 1n+j))
75
76def bsof(~V: Data, sh: Sh<V>) -> List<&2, B.Bk>:
77 match sh:
78 case HS{n, +k, td, fresh, sz, sd, sdU, free, +tabT, +ksT, vsT, nxT}:
79 TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k))
80
81def model(~V: Data, sh: Sh<V>) -> List<&2, S.Entry<V>>:
82 match sh:
83 case HS{n, +k, td, fresh, sz, sd, sdU, free, +tabT, +ksT, +vsT, nxT}:
84 absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n)
85
86# ---- the invariant ----
87# stated over the stored keys' slot list kl and their tree's perfectness pk,
88# so that a read that swaps a key out and back keeps it
89
90
91# no full bucket among the first m uses slot s
92def noslot(+bs: List<&2, B.Bk>, +s: Nat, +m: Nat) -> Bool:
93 match m:
94 case 0n:
95 True{}
96 case 1n+j:
97 Bool.and(Bool.not(Bool.and(B.occ(B.at(bs, j)), Nat.is_eq(UD.v(H.slot(B.lnk(B.at(bs, j)))), s))), noslot(bs, s, j))
98
99# the free list from link f has exactly cnt links: each slot on it is below
100# fresh, used by no bucket and not repeated, and the list ends after them
101def fl_ok(+bs: List<&2, B.Bk>, +nb: Nat, +nxl: List<&2, U32>, +cnt: Nat, +f: U32, +fr: Nat, +seen: List<&2, Nat>) -> Bool:
102 match cnt:
103 case 0n:
104 U32.is_eq(f, 0)
105 case 1n+p:
106 Bool.and(Bool.not(U32.is_eq(f, 0)), Bool.and(Bool.and(Nat.is_lt(UD.v(H.slot(f)), fr), Bool.and(noslot(bs, UD.v(H.slot(f)), nb), Bool.not(NL.memn(UD.v(H.slot(f)), seen)))), fl_ok(bs, nb, nxl, p, W32.nth0(nxl, UD.v(H.slot(f))), fr, Con{UD.v(H.slot(f)), seen})))
107
108def ck(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
109 Bool.and(Nat.is_lt(k, 31n), Nat.is_lt(0n, k))
110
111def csd(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
112 Nat.is_lt(sd, 32n)
113
114def cpt(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
115 AR.perfect(U32, 1n+k, tabT)
116
117def cpk(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
118 pk
119
120def cpv(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
121 AR.perfect(Maybe<&2, V>, sd, vsT)
122
123def cpn(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
124 AR.perfect(U32, sd, nxT)
125
126def ctd(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
127 Nat.is_eq(UD.v(td), 1n+k)
128
129def csz(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
130 Nat.is_eq(UD.v(sz), SC.pow2(sd))
131
132def csdu(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
133 Nat.is_eq(UD.v(sdU), sd)
134
135def cwell(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
136 B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), sd}, SC.pow2(k))
137
138def cclus(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
139 B.cluster(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), SC.pow2(k), CY.msk(k))
140
141def cuniq(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
142 B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k))}, SC.pow2(k))
143
144def cn(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
145 Nat.is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), SC.pow2(k)))
146
147def cload(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
148 Nat.is_le(Nat.double(UD.v(n)), SC.pow2(k))
149
150def clive(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
151 B.all_lt(B.PLive{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(fresh)}, SC.pow2(k))
152
153def cfresh(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
154 Nat.is_le(UD.v(fresh), UD.v(sz))
155
156def cfree(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
157 Bool.and(Nat.is_le(UD.v(n), UD.v(fresh)), fl_ok(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fresh), UD.v(n)), free, UD.v(fresh), Nil{}))
158
159def csdk(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
160 Nat.is_lt(sd, k)
161
162def gr16(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
163 Bool.and(cfree(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), csdk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))
164
165def gr15(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
166 Bool.and(cfresh(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr16(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))
167
168def gr14(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
169 Bool.and(clive(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr15(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))
170
171def gr13(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
172 Bool.and(cload(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr14(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))
173
174def gr12(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
175 Bool.and(cn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr13(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))
176
177def gr11(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
178 Bool.and(cuniq(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr12(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))
179
180def gr10(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
181 Bool.and(cclus(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr11(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))
182
183def gr9(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
184 Bool.and(cwell(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr10(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))
185
186def gr8(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
187 Bool.and(csdu(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr9(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))
188
189def gr7(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
190 Bool.and(csz(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr8(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))
191
192def gr6(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
193 Bool.and(ctd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr7(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))
194
195def gr5(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
196 Bool.and(cpn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr6(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))
197
198def gr4(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
199 Bool.and(cpv(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr5(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))
200
201def gr3(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
202 Bool.and(cpk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr4(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))
203
204def gr2(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
205 Bool.and(cpt(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr3(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))
206
207def gr1(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
208 Bool.and(csd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr2(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))
209
210def goodF(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
211 Bool.and(ck(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr1(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))
212
213def good(~V: Data, sh: Sh<V>) -> Bool:
214 match sh:
215 case HS{+n, +k, +td, +fresh, +sz, +sd, +sdU, +free, +tabT, +ksT, +vsT, +nxT}:
216 goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT)
217
218def gp1(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr1(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
219 L.and_right(ck(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr1(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), g)
220
221def gp2(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr2(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
222 L.and_right(csd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr2(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp1(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
223
224def gp3(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr3(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
225 L.and_right(cpt(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr3(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp2(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
226
227def gp4(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr4(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
228 L.and_right(cpk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr4(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp3(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
229
230def gp5(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr5(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
231 L.and_right(cpv(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr5(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp4(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
232
233def gp6(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr6(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
234 L.and_right(cpn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr6(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp5(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
235
236def gp7(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr7(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
237 L.and_right(ctd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr7(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp6(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
238
239def gp8(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr8(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
240 L.and_right(csz(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr8(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp7(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
241
242def gp9(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr9(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
243 L.and_right(csdu(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr9(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp8(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
244
245def gp10(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr10(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
246 L.and_right(cwell(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr10(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp9(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
247
248def gp11(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr11(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
249 L.and_right(cclus(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr11(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp10(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
250
251def gp12(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr12(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
252 L.and_right(cuniq(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr12(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp11(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
253
254def gp13(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr13(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
255 L.and_right(cn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr13(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp12(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
256
257def gp14(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr14(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
258 L.and_right(cload(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr14(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp13(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
259
260def gp15(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr15(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
261 L.and_right(clive(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr15(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp14(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
262
263def gp16(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr16(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
264 L.and_right(cfresh(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr16(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp15(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
265
266def gp17(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {csdk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
267 L.and_right(cfree(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), csdk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp16(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
268
269def g_ck(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {ck(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
270 L.and_left(ck(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr1(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), g)
271
272def g_csd(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {csd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
273 L.and_left(csd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr2(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp1(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
274
275def g_cpt(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {cpt(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
276 L.and_left(cpt(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr3(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp2(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
277
278def g_cpk(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {cpk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
279 L.and_left(cpk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr4(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp3(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
280
281def g_cpv(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {cpv(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
282 L.and_left(cpv(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr5(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp4(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
283
284def g_cpn(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {cpn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
285 L.and_left(cpn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr6(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp5(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
286
287def g_ctd(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {ctd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
288 L.and_left(ctd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr7(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp6(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
289
290def g_csz(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {csz(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
291 L.and_left(csz(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr8(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp7(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
292
293def g_csdu(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {csdu(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
294 L.and_left(csdu(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr9(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp8(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
295
296def g_cwell(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {cwell(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
297 L.and_left(cwell(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr10(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp9(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
298
299def g_cclus(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {cclus(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
300 L.and_left(cclus(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr11(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp10(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
301
302def g_cuniq(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {cuniq(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
303 L.and_left(cuniq(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr12(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp11(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
304
305def g_cn(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {cn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
306 L.and_left(cn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr13(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp12(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
307
308def g_cload(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {cload(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
309 L.and_left(cload(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr14(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp13(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
310
311def g_clive(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {clive(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
312 L.and_left(clive(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr15(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp14(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
313
314def g_cfresh(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {cfresh(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
315 L.and_left(cfresh(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr16(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp15(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
316
317def g_cfree(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {cfree(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
318 L.and_left(cfree(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), csdk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp16(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
319
320def g_csdk(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {csdk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
321 gp17(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g)
322
323# the invariant from its components
324def good_intro(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +h_ck: {ck(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_csd: {csd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_cpt: {cpt(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_cpk: {cpk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_cpv: {cpv(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_cpn: {cpn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_ctd: {ctd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_csz: {csz(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_csdu: {csdu(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_cwell: {cwell(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_cclus: {cclus(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_cuniq: {cuniq(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_cn: {cn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_cload: {cload(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_clive: {clive(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_cfresh: {cfresh(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_cfree: {cfree(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_csdk: {csdk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
325 L.and_intro(ck(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr1(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), h_ck, L.and_intro(csd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr2(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), h_csd, L.and_intro(cpt(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr3(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), h_cpt, L.and_intro(cpk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr4(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), h_cpk, L.and_intro(cpv(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr5(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), h_cpv, L.and_intro(cpn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr6(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), h_cpn, L.and_intro(ctd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr7(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), h_ctd, L.and_intro(csz(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr8(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), h_csz, L.and_intro(csdu(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr9(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), h_csdu, L.and_intro(cwell(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr10(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), h_cwell, L.and_intro(cclus(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr11(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), h_cclus, L.and_intro(cuniq(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr12(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), h_cuniq, L.and_intro(cn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr13(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), h_cn, L.and_intro(cload(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr14(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), h_cload, L.and_intro(clive(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr15(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), h_clive, L.and_intro(cfresh(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr16(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), h_cfresh, L.and_intro(cfree(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), csdk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), h_cfree, h_csdk)))))))))))))))))
326
327# ---- slot values ----
328
329def lvs_nth(~V: Data, +vsl: List<&2, Maybe<&2, V>>, +i: Nat) -> {B.nthb(lvs(~V, vsl), i) == some_b(~V, nthm(~V, vsl, i)) : Bool}:
330 match vsl i:
331 case Nil{} _:
332 {==}
333 case Con{m, t} 0n:
334 {==}
335 case Con{m, t} 1n+p:
336 lvs_nth(~V, t, p)
337
338def nthm_some(~V: Data, +vsl: List<&2, Maybe<&2, V>>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Maybe<&2, V>, vsl)) == True{} : Bool}) -> {SC.nth(Maybe<&2, V>, vsl, i) == Some{nthm(~V, vsl, i)} : Maybe<&2, Maybe<&2, V>>}:
339 match vsl i:
340 case Nil{} _:
341 Empty.absurd({SC.nth(Maybe<&2, V>, Nil{}, i) == Some{nthm(~V, Nil{}, i)} : Maybe<&2, Maybe<&2, V>>}, N.lt_zero_absurd(i, h))
342 case Con{m, t} 0n:
343 {==}
344 case Con{m, t} 1n+p:
345 nthm_some(~V, t, p, h)