proof_tab.bend
bend-osdev-gf@0.1.2.0 · 313 lines · 0 definitions
1# Proof helpers for bend-osdev-gf: the exp/log tables (tables.bend) as lists.
2#
3# The method (as bend-osdev-blockdev's ImgDev and bend-osdev-crc's tables
4# follow their arrays): array's laws turn each table fill, write by write,
5# into Arrays.of_list(d, l, 0) for a Data list l (of_list_new, of_list_set;
6# the fill's counter i is U32.from_nat(i), and its running power is
7# Gf8.exp(f, i)). The exp table's list is gt.elist(510, f, 0): entry i is
8# Gf8.exp(f, i), for every field. The log table's list is computed for the
9# named fields (proof_tab_cases.bend). A read of a table is then
10# array's of_list_get: a literal pair of the same table and the list's
11# entry. Lemmas are prefixed gt.
12import Base
13import bend-osdev-array@0.1.0.1/array.bend as A
14import bend-osdev-array@0.1.0.1/LAWS.bend as AL
15import bend-osdev-array@0.1.0.1/PROOF.bend as APF
16import bend-osdev-gf@0.1.2.0/gf.bend as G
17import bend-osdev-gf@0.1.2.0/tables.bend as T
18import bend-osdev-u32@0.1.0.0/LAWS.bend as UL
19import bend-osdev-u32@0.1.0.0/PROOF.bend as UP
20
21# Contradictions and congruence
22
23def gt.bt(b: Bool) -> Type:
24 match b:
25 case True{}:
26 Unit
27 case False{}:
28 Empty
29
30def gt.ft(e: {False{} == True{} : Bool}) -> Empty:
31 %Equal.sym(Bool, False{}, True{}, e) : gt.bt(_)
32 Unit{}
33
34def gt.tf(e: {True{} == False{} : Bool}) -> Empty:
35 %e : gt.bt(_)
36 Unit{}
37
38def gt.wcon2(-p: Nat, -a: Bool, -b: Bool, -x: Word(p), -y: Word(p), ea: {a == b : Bool}, ex: {x == y : Word(p)}) -> {WCon{a, x} == WCon{b, y} : Word(1n+p)}:
39 %ea : {WCon{a, x} == WCon{_, y} : Word(1n+p)}
40 %ex : {WCon{a, x} == WCon{a, _} : Word(1n+p)}
41 {==}
42
43def gt.u32_cong(-x: Word(32n), -y: Word(32n), e: {x == y : Word(32n)}) -> {U32{x} == U32{y} : U32}:
44 %e : {U32{x} == U32{_} : U32}
45 {==}
46
47# U32 addition of small counts: adding zero, adding an increment
48
49def gt.adc_zero(n: Nat, w: Word(n)) -> {Word.adc(n, w, Word.zero(n), False{}, False{}) == w : Word(n)}:
50 match n:
51 case 0n:
52 match w:
53 case WNil{}:
54 {==}
55 case 1n+p:
56 match w:
57 case WCon{False{}, +t}:
58 gt.wcon2(p, False{}, False{}, Word.adc(p, t, Word.zero(p), False{}, False{}), t, {==}, gt.adc_zero(p, t))
59 case WCon{True{}, +t}:
60 gt.wcon2(p, True{}, True{}, Word.adc(p, t, Word.zero(p), False{}, False{}), t, {==}, gt.adc_zero(p, t))
61
62# a + (b + 1) = a + b with a carry in
63def gt.adc_inc(n: Nat, a: Word(n), b: Word(n)) -> {Word.adc(n, a, Word.inc(n, b), False{}, False{}) == Word.adc(n, a, b, False{}, True{}) : Word(n)}:
64 match n:
65 case 0n:
66 match a b:
67 case WNil{} WNil{}:
68 {==}
69 case 1n+p:
70 match a b:
71 case WCon{False{}, at} WCon{False{}, bt}:
72 {==}
73 case WCon{True{}, at} WCon{False{}, bt}:
74 {==}
75 case WCon{False{}, +at} WCon{True{}, +bt}:
76 gt.wcon2(p, False{}, False{}, Word.adc(p, at, Word.inc(p, bt), False{}, False{}), Word.adc(p, at, bt, False{}, True{}), {==}, gt.adc_inc(p, at, bt))
77 case WCon{True{}, +at} WCon{True{}, +bt}:
78 gt.wcon2(p, True{}, True{}, Word.adc(p, at, Word.inc(p, bt), False{}, False{}), Word.adc(p, at, bt, False{}, True{}), {==}, gt.adc_inc(p, at, bt))
79
80# a + b with a carry in is (a + b) + 1
81def gt.adc_carry(n: Nat, a: Word(n), b: Word(n)) -> {Word.adc(n, a, b, False{}, True{}) == Word.inc(n, Word.adc(n, a, b, False{}, False{})) : Word(n)}:
82 match n:
83 case 0n:
84 match a b:
85 case WNil{} WNil{}:
86 {==}
87 case 1n+p:
88 match a b:
89 case WCon{False{}, at} WCon{False{}, bt}:
90 {==}
91 case WCon{True{}, +at} WCon{False{}, +bt}:
92 gt.wcon2(p, False{}, False{}, Word.adc(p, at, bt, False{}, True{}), Word.inc(p, Word.adc(p, at, bt, False{}, False{})), {==}, gt.adc_carry(p, at, bt))
93 case WCon{False{}, +at} WCon{True{}, +bt}:
94 gt.wcon2(p, False{}, False{}, Word.adc(p, at, bt, False{}, True{}), Word.inc(p, Word.adc(p, at, bt, False{}, False{})), {==}, gt.adc_carry(p, at, bt))
95 case WCon{True{}, at} WCon{True{}, bt}:
96 {==}
97
98def gt.add_zero(x: U32) -> {U32.add(x, 0) == x : U32}:
99 match x:
100 case U32{+w}:
101 gt.u32_cong(Word.adc(32n, w, Word.zero(32n), False{}, False{}), w, gt.adc_zero(32n, w))
102
103def gt.add_inc(a: U32, b: U32) -> {U32.add(a, U32.inc(b)) == U32.inc(U32.add(a, b)) : U32}:
104 match a b:
105 case U32{+x} U32{+y}:
106 gt.u32_cong(Word.adc(32n, x, Word.inc(32n, y), False{}, False{}), Word.inc(32n, Word.adc(32n, x, y, False{}, False{})), Equal.trans(Word(32n), Word.adc(32n, x, Word.inc(32n, y), False{}, False{}), Word.adc(32n, x, y, False{}, True{}), Word.inc(32n, Word.adc(32n, x, y, False{}, False{})), gt.adc_inc(32n, x, y), gt.adc_carry(32n, x, y)))
107
108# the fills' counter: i + 1 is the increment
109def gt.add_one(+x: U32) -> {U32.add(x, 1) == U32.inc(x) : U32}:
110 %gt.add_zero(x) : {U32.add(x, 1) == U32.inc(_) : U32}
111 gt.add_inc(x, 0)
112
113# the sum of two counts, as U32, is the U32 of their sum
114def gt.add_nat(+p: Nat, +q: Nat) -> {U32.add(U32.from_nat(p), U32.from_nat(q)) == U32.from_nat(Nat.add(q, p)) : U32}:
115 match q:
116 case 0n:
117 gt.add_zero(U32.from_nat(p))
118 case 1n+r:
119 %gt.add_nat(p, r) : {U32.add(U32.from_nat(p), U32.inc(U32.from_nat(r))) == U32.inc(_) : U32}
120 gt.add_inc(U32.from_nat(p), U32.from_nat(r))
121
122# Nat facts
123
124def gt.lt_succ_r(+x: Nat, +y: Nat, h: {Nat.is_lt(x, y) == True{} : Bool}) -> {Nat.is_lt(x, 1n+y) == True{} : Bool}:
125 match x y:
126 case 0n _:
127 {==}
128 case 1n+p 0n:
129 Empty.absurd({Nat.is_lt(1n+p, 1n) == True{} : Bool}, gt.ft(h))
130 case 1n+p 1n+q:
131 gt.lt_succ_r(p, q, h)
132
133def gt.lt_self(+x: Nat) -> {Nat.is_lt(x, 1n+x) == True{} : Bool}:
134 match x:
135 case 0n:
136 {==}
137 case 1n+p:
138 gt.lt_self(p)
139
140# x < 1 + (n + x)
141def gt.lt_self_add(+n: Nat, +x: Nat) -> {Nat.is_lt(x, 1n+Nat.add(n, x)) == True{} : Bool}:
142 match n:
143 case 0n:
144 gt.lt_self(x)
145 case 1n+k:
146 gt.lt_succ_r(x, 1n+Nat.add(k, x), gt.lt_self_add(k, x))
147
148# b < n, so b < m + n
149def gt.lt_add_left(+m: Nat, +b: Nat, +n: Nat, +h: {Nat.is_lt(b, n) == True{} : Bool}) -> {Nat.is_lt(b, Nat.add(m, n)) == True{} : Bool}:
150 match m:
151 case 0n:
152 h
153 case 1n+k:
154 gt.lt_succ_r(b, Nat.add(k, n), gt.lt_add_left(k, b, n, h))
155
156# a < m and b < n, so a + b < m + n
157def gt.lt_sum(+a: Nat, +m: Nat, +b: Nat, +n: Nat, ha: {Nat.is_lt(a, m) == True{} : Bool}, +hb: {Nat.is_lt(b, n) == True{} : Bool}) -> {Nat.is_lt(Nat.add(a, b), Nat.add(m, n)) == True{} : Bool}:
158 match a m:
159 case 0n _:
160 gt.lt_add_left(m, b, n, hb)
161 case 1n+p 0n:
162 Empty.absurd({Nat.is_lt(Nat.add(1n+p, b), n) == True{} : Bool}, gt.ft(ha))
163 case 1n+p 1n+q:
164 gt.lt_sum(p, q, b, n, ha, hb)
165
166# two logarithms (each below 255) sum below the exp table's 2^9 slots
167def gt.sum_lt(+a: Nat, +b: Nat, +ha: {Nat.is_lt(a, 255n) == True{} : Bool}, +hb: {Nat.is_lt(b, 255n) == True{} : Bool}) -> {Nat.is_lt(Nat.add(a, b), A.Arrays.slots(9n)) == True{} : Bool}:
168 gt.lt_add_left(2n, Nat.add(a, b), 510n, gt.lt_sum(a, 255n, b, 255n, ha, hb))
169
170# Gf8.log is below 255
171
172def gt.log_go_lt(+n: Nat, hit: Bool, +f: G.Gf8Field, +a: U32, +cur: U32, +i: Nat) -> {Nat.is_lt(G.Gf8.log.go(n, hit, f, a, cur, i), 1n+Nat.add(n, i)) == True{} : Bool}:
173 match n hit:
174 case _ True{}:
175 gt.lt_self_add(n, i)
176 case 0n False{}:
177 {==}
178 case 1n+k False{}:
179 %UL.nat_add_succ(k, i) : {Nat.is_lt(G.Gf8.log.go(k, U32.is_eq(G.Gf8.mul(f, G.Gf8.gen(f), cur), a), f, a, G.Gf8.mul(f, G.Gf8.gen(f), cur), 1n+i), 1n+_) == True{} : Bool}
180 gt.log_go_lt(k, U32.is_eq(G.Gf8.mul(f, G.Gf8.gen(f), cur), a), f, a, G.Gf8.mul(f, G.Gf8.gen(f), cur), 1n+i)
181
182def gt.log_lt(+f: G.Gf8Field, +a: U32) -> {Nat.is_lt(G.Gf8.log(f, a), 255n) == True{} : Bool}:
183 gt.log_go_lt(254n, U32.is_eq(1, G.Gf8.elt(a)), f, G.Gf8.elt(a), 1, 0n)
184
185# The fills, write by write
186
187def gt.hd9() -> {Nat.is_lt(9n, 32n) == True{} : Bool}:
188 {==}
189
190def gt.hd8() -> {Nat.is_lt(8n, 32n) == True{} : Bool}:
191 {==}
192
193def gt.hl_set(+d: Nat, +xs: List<&2, U32>, +k: Nat, +v: U32, +hl: {List.length(&2, U32, xs) == A.Arrays.slots(d) : Nat}) -> {List.length(&2, U32, List.set(&2, U32, xs, k, v)) == A.Arrays.slots(d) : Nat}:
194 Equal.trans(Nat, List.length(&2, U32, List.set(&2, U32, xs, k, v)), List.length(&2, U32, xs), A.Arrays.slots(d), AL.set_length(U32, xs, k, v), hl)
195
196# the exp fill's model: slot i (from slot k) holds gen^i
197def gt.fe(n: Nat, xs: List<&2, U32>, +f: G.Gf8Field, +k: Nat) -> List<&2, U32>:
198 match n:
199 case 0n:
200 xs
201 case 1n+j:
202 gt.fe(j, List.set(&2, U32, xs, A.Arrays.index(9n, U32.from_nat(k)), G.Gf8.exp(f, k)), f, 1n+k)
203
204def gt.fill_exp(n: Nat, +xs: List<&2, U32>, +f: G.Gf8Field, +k: Nat, +hl: {List.length(&2, U32, xs) == A.Arrays.slots(9n) : Nat}) -> {T.gf8tab.fill.exp(n, A.Arrays.of_list(U32, 9n, xs, 0), f, G.Gf8.exp(f, k), U32.from_nat(k)) == A.Arrays.of_list(U32, 9n, gt.fe(n, xs, f, k), 0) : Array<U32>}:
205 match n:
206 case 0n:
207 {==}
208 case 1n+j:
209 %Equal.sym(U32, U32.add(U32.from_nat(k), 1), U32.inc(U32.from_nat(k)), gt.add_one(U32.from_nat(k))) : {T.gf8tab.fill.exp(j, Array.set(U32, A.Arrays.of_list(U32, 9n, xs, 0), U32.from_nat(k), G.Gf8.exp(f, k)), f, G.Gf8.mul(f, G.Gf8.gen(f), G.Gf8.exp(f, k)), _) == A.Arrays.of_list(U32, 9n, gt.fe(j, List.set(&2, U32, xs, A.Arrays.index(9n, U32.from_nat(k)), G.Gf8.exp(f, k)), f, 1n+k), 0) : Array<U32>}
210 %Equal.sym(Array<U32>, Array.set(U32, A.Arrays.of_list(U32, 9n, xs, 0), U32.from_nat(k), G.Gf8.exp(f, k)), A.Arrays.of_list(U32, 9n, List.set(&2, U32, xs, A.Arrays.index(9n, U32.from_nat(k)), G.Gf8.exp(f, k)), 0), AL.of_list_set(U32, 9n, xs, 0, hl, gt.hd9(), U32.from_nat(k), G.Gf8.exp(f, k))) : {T.gf8tab.fill.exp(j, _, f, G.Gf8.mul(f, G.Gf8.gen(f), G.Gf8.exp(f, k)), U32.inc(U32.from_nat(k))) == A.Arrays.of_list(U32, 9n, gt.fe(j, List.set(&2, U32, xs, A.Arrays.index(9n, U32.from_nat(k)), G.Gf8.exp(f, k)), f, 1n+k), 0) : Array<U32>}
211 gt.fill_exp(j, List.set(&2, U32, xs, A.Arrays.index(9n, U32.from_nat(k)), G.Gf8.exp(f, k)), f, 1n+k, gt.hl_set(9n, xs, A.Arrays.index(9n, U32.from_nat(k)), G.Gf8.exp(f, k), hl))
212
213# the log fill's model: slot gen^i holds i, from i = k
214def gt.fl(n: Nat, xs: List<&2, U32>, +f: G.Gf8Field, +k: Nat) -> List<&2, U32>:
215 match n:
216 case 0n:
217 xs
218 case 1n+j:
219 gt.fl(j, List.set(&2, U32, xs, A.Arrays.index(8n, G.Gf8.exp(f, k)), U32.from_nat(k)), f, 1n+k)
220
221def gt.fill_log(n: Nat, +xs: List<&2, U32>, +f: G.Gf8Field, +k: Nat, +hl: {List.length(&2, U32, xs) == A.Arrays.slots(8n) : Nat}) -> {T.gf8tab.fill.log(n, A.Arrays.of_list(U32, 8n, xs, 0), f, G.Gf8.exp(f, k), U32.from_nat(k)) == A.Arrays.of_list(U32, 8n, gt.fl(n, xs, f, k), 0) : Array<U32>}:
222 match n:
223 case 0n:
224 {==}
225 case 1n+j:
226 %Equal.sym(U32, U32.add(U32.from_nat(k), 1), U32.inc(U32.from_nat(k)), gt.add_one(U32.from_nat(k))) : {T.gf8tab.fill.log(j, Array.set(U32, A.Arrays.of_list(U32, 8n, xs, 0), G.Gf8.exp(f, k), U32.from_nat(k)), f, G.Gf8.mul(f, G.Gf8.gen(f), G.Gf8.exp(f, k)), _) == A.Arrays.of_list(U32, 8n, gt.fl(j, List.set(&2, U32, xs, A.Arrays.index(8n, G.Gf8.exp(f, k)), U32.from_nat(k)), f, 1n+k), 0) : Array<U32>}
227 %Equal.sym(Array<U32>, Array.set(U32, A.Arrays.of_list(U32, 8n, xs, 0), G.Gf8.exp(f, k), U32.from_nat(k)), A.Arrays.of_list(U32, 8n, List.set(&2, U32, xs, A.Arrays.index(8n, G.Gf8.exp(f, k)), U32.from_nat(k)), 0), AL.of_list_set(U32, 8n, xs, 0, hl, gt.hd8(), G.Gf8.exp(f, k), U32.from_nat(k))) : {T.gf8tab.fill.log(j, _, f, G.Gf8.mul(f, G.Gf8.gen(f), G.Gf8.exp(f, k)), U32.inc(U32.from_nat(k))) == A.Arrays.of_list(U32, 8n, gt.fl(j, List.set(&2, U32, xs, A.Arrays.index(8n, G.Gf8.exp(f, k)), U32.from_nat(k)), f, 1n+k), 0) : Array<U32>}
228 gt.fill_log(j, List.set(&2, U32, xs, A.Arrays.index(8n, G.Gf8.exp(f, k)), U32.from_nat(k)), f, 1n+k, gt.hl_set(8n, xs, A.Arrays.index(8n, G.Gf8.exp(f, k)), U32.from_nat(k), hl))
229
230# The exp table, for every field: entry i is gen^i (i < 510), then two 0s
231
232def gt.elist(n: Nat, +f: G.Gf8Field, +k: Nat) -> List<&2, U32>:
233 match n:
234 case 0n:
235 [0, 0]
236 case 1n+j:
237 Con{G.Gf8.exp(f, k), gt.elist(j, f, 1n+k)}
238
239def gt.elist_model(+f: G.Gf8Field) -> {gt.fe(510n, List.replicate(U32, A.Arrays.slots(9n), 0), f, 0n) == gt.elist(510n, f, 0n) : List<&2, U32>}:
240 {==}
241
242def gt.rep_len(+n: Nat) -> {List.length(&2, U32, List.replicate(U32, n, 0)) == n : Nat}:
243 match n:
244 case 0n:
245 {==}
246 case 1n+k:
247 %Equal.sym(Nat, List.length(&2, U32, List.replicate(U32, k, 0)), k, gt.rep_len(k)) : {1n+_ == 1n+k : Nat}
248 {==}
249
250def gt.hl_rep(+d: Nat) -> {List.length(&2, U32, List.replicate(U32, A.Arrays.slots(d), 0)) == A.Arrays.slots(d) : Nat}:
251 gt.rep_len(A.Arrays.slots(d))
252
253def gt.hl_elist(+f: G.Gf8Field) -> {List.length(&2, U32, gt.elist(510n, f, 0n)) == A.Arrays.slots(9n) : Nat}:
254 {==}
255
256def gt.f0() -> {U32.from_nat(0n) == 0 : U32}:
257 {==}
258
259def gt.e0(+f: G.Gf8Field) -> {G.Gf8.exp(f, 0n) == 1 : U32}:
260 {==}
261
262# the exp table of a field f, given that it is its fill (for a named field
263# that is computation, proof_tab_cases.bend; it is stated per field because
264# --verdict's kernel compares the two sides by running them)
265def gt.exp_table(+f: G.Gf8Field, +e0: {T.Gf8Tab.exp_table(f) == T.gf8tab.fill.exp(510n, Array.new(U32, 9n, 0), f, 1, 0) : Array<U32>}) -> {T.Gf8Tab.exp_table(f) == A.Arrays.of_list(U32, 9n, gt.elist(510n, f, 0n), 0) : Array<U32>}:
266 %Equal.sym(Array<U32>, T.Gf8Tab.exp_table(f), T.gf8tab.fill.exp(510n, Array.new(U32, 9n, 0), f, 1, 0), e0) : {_ == A.Arrays.of_list(U32, 9n, gt.elist(510n, f, 0n), 0) : Array<U32>}
267 %Equal.sym(Array<U32>, Array.new(U32, 9n, 0), A.Arrays.of_list(U32, 9n, List.replicate(U32, A.Arrays.slots(9n), 0), 0), AL.of_list_new(U32, 9n, 0)) : {T.gf8tab.fill.exp(510n, _, f, 1, 0) == A.Arrays.of_list(U32, 9n, gt.elist(510n, f, 0n), 0) : Array<U32>}
268 %gt.elist_model(f) : {T.gf8tab.fill.exp(510n, A.Arrays.of_list(U32, 9n, List.replicate(U32, A.Arrays.slots(9n), 0), 0), f, 1, 0) == A.Arrays.of_list(U32, 9n, _, 0) : Array<U32>}
269 %gt.e0(f) : {T.gf8tab.fill.exp(510n, A.Arrays.of_list(U32, 9n, List.replicate(U32, A.Arrays.slots(9n), 0), 0), f, _, 0) == A.Arrays.of_list(U32, 9n, gt.fe(510n, List.replicate(U32, A.Arrays.slots(9n), 0), f, 0n), 0) : Array<U32>}
270 %gt.f0() : {T.gf8tab.fill.exp(510n, A.Arrays.of_list(U32, 9n, List.replicate(U32, A.Arrays.slots(9n), 0), 0), f, G.Gf8.exp(f, 0n), _) == A.Arrays.of_list(U32, 9n, gt.fe(510n, List.replicate(U32, A.Arrays.slots(9n), 0), f, 0n), 0) : Array<U32>}
271 gt.fill_exp(510n, List.replicate(U32, A.Arrays.slots(9n), 0), f, 0n, gt.hl_rep(9n))
272
273# entry j of the exp table's list is gen^j, for j < 510
274def gt.elist_nth(+n: Nat, +f: G.Gf8Field, +k: Nat, +j: Nat, h: {Nat.is_lt(j, n) == True{} : Bool}) -> {A.Arrays.nth(U32, gt.elist(n, f, k), j, 0) == G.Gf8.exp(f, Nat.add(j, k)) : U32}:
275 match n j:
276 case 0n 0n:
277 Empty.absurd({A.Arrays.nth(U32, gt.elist(0n, f, k), 0n, 0) == G.Gf8.exp(f, Nat.add(0n, k)) : U32}, gt.ft(h))
278 case 0n 1n+i:
279 Empty.absurd({A.Arrays.nth(U32, gt.elist(0n, f, k), 1n+i, 0) == G.Gf8.exp(f, Nat.add(1n+i, k)) : U32}, gt.ft(h))
280 case 1n+m 0n:
281 {==}
282 case 1n+m 1n+i:
283 %UL.nat_add_succ(i, k) : {A.Arrays.nth(U32, gt.elist(m, f, 1n+k), i, 0) == G.Gf8.exp(f, _) : U32}
284 gt.elist_nth(m, f, 1n+k, i, h)
285
286# The log table, for a field whose log list is given
287
288def gt.log_table(+f: G.Gf8Field, +l: List<&2, U32>, +e0: {T.Gf8Tab.log_table(f) == T.gf8tab.fill.log(255n, Array.new(U32, 8n, 0), f, 1, 0) : Array<U32>}, +e: {gt.fl(255n, List.replicate(U32, A.Arrays.slots(8n), 0), f, 0n) == l : List<&2, U32>}) -> {T.Gf8Tab.log_table(f) == A.Arrays.of_list(U32, 8n, l, 0) : Array<U32>}:
289 %Equal.sym(Array<U32>, T.Gf8Tab.log_table(f), T.gf8tab.fill.log(255n, Array.new(U32, 8n, 0), f, 1, 0), e0) : {_ == A.Arrays.of_list(U32, 8n, l, 0) : Array<U32>}
290 %Equal.sym(Array<U32>, Array.new(U32, 8n, 0), A.Arrays.of_list(U32, 8n, List.replicate(U32, A.Arrays.slots(8n), 0), 0), AL.of_list_new(U32, 8n, 0)) : {T.gf8tab.fill.log(255n, _, f, 1, 0) == A.Arrays.of_list(U32, 8n, l, 0) : Array<U32>}
291 %e : {T.gf8tab.fill.log(255n, A.Arrays.of_list(U32, 8n, List.replicate(U32, A.Arrays.slots(8n), 0), 0), f, 1, 0) == A.Arrays.of_list(U32, 8n, _, 0) : Array<U32>}
292 %gt.e0(f) : {T.gf8tab.fill.log(255n, A.Arrays.of_list(U32, 8n, List.replicate(U32, A.Arrays.slots(8n), 0), 0), f, _, 0) == A.Arrays.of_list(U32, 8n, gt.fl(255n, List.replicate(U32, A.Arrays.slots(8n), 0), f, 0n), 0) : Array<U32>}
293 %gt.f0() : {T.gf8tab.fill.log(255n, A.Arrays.of_list(U32, 8n, List.replicate(U32, A.Arrays.slots(8n), 0), 0), f, G.Gf8.exp(f, 0n), _) == A.Arrays.of_list(U32, 8n, gt.fl(255n, List.replicate(U32, A.Arrays.slots(8n), 0), f, 0n), 0) : Array<U32>}
294 gt.fill_log(255n, List.replicate(U32, A.Arrays.slots(8n), 0), f, 0n, gt.hl_rep(8n))
295
296# the log fill splits: n + m writes are n writes, then m more
297def gt.fl_split(+n: Nat, +m: Nat, xs: List<&2, U32>, +f: G.Gf8Field, +k: Nat) -> {gt.fl(Nat.add(n, m), xs, f, k) == gt.fl(m, gt.fl(n, xs, f, k), f, Nat.add(n, k)) : List<&2, U32>}:
298 match n:
299 case 0n:
300 {==}
301 case 1n+j:
302 %UL.nat_add_succ(j, k) : {gt.fl(Nat.add(j, m), List.set(&2, U32, xs, A.Arrays.index(8n, G.Gf8.exp(f, k)), U32.from_nat(k)), f, 1n+k) == gt.fl(m, gt.fl(j, List.set(&2, U32, xs, A.Arrays.index(8n, G.Gf8.exp(f, k)), U32.from_nat(k)), f, 1n+k), f, _) : List<&2, U32>}
303 gt.fl_split(j, m, List.set(&2, U32, xs, A.Arrays.index(8n, G.Gf8.exp(f, k)), U32.from_nat(k)), f, 1n+k)
304
305# A table whose lists are known
306
307def gt.tab(+f: G.Gf8Field, +l: List<&2, U32>) -> T.Gf8Tab:
308 T.Gf8Tab{A.Arrays.of_list(U32, 9n, gt.elist(510n, f, 0n), 0), A.Arrays.of_list(U32, 8n, l, 0)}
309
310def gt.new(+f: G.Gf8Field, +l: List<&2, U32>, +ex0: {T.Gf8Tab.exp_table(f) == T.gf8tab.fill.exp(510n, Array.new(U32, 9n, 0), f, 1, 0) : Array<U32>}, +el0: {T.Gf8Tab.log_table(f) == T.gf8tab.fill.log(255n, Array.new(U32, 8n, 0), f, 1, 0) : Array<U32>}, +e: {gt.fl(255n, List.replicate(U32, A.Arrays.slots(8n), 0), f, 0n) == l : List<&2, U32>}) -> {gt.tab(f, l) == T.Gf8Tab.new(f) : T.Gf8Tab}:
311 %Equal.sym(Array<U32>, T.Gf8Tab.exp_table(f), A.Arrays.of_list(U32, 9n, gt.elist(510n, f, 0n), 0), gt.exp_table(f, ex0)) : {gt.tab(f, l) == T.Gf8Tab{_, T.Gf8Tab.log_table(f)} : T.Gf8Tab}
312 %Equal.sym(Array<U32>, T.Gf8Tab.log_table(f), A.Arrays.of_list(U32, 8n, l, 0), gt.log_table(f, l, el0, e)) : {gt.tab(f, l) == T.Gf8Tab{A.Arrays.of_list(U32, 9n, gt.elist(510n, f, 0n), 0), _} : T.Gf8Tab}
313 {==}