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.
12	import Base
13	import bend-osdev-array@0.1.0.1/array.bend as A
14	import bend-osdev-array@0.1.0.1/LAWS.bend as AL
15	import bend-osdev-array@0.1.0.1/PROOF.bend as APF
16	import ./gf.bend as G
17	import ./tables.bend as T
18	import bend-osdev-u32@0.1.0.0/LAWS.bend as UL
19	import bend-osdev-u32@0.1.0.0/PROOF.bend as UP
20	
21	# Contradictions and congruence
22	
23	def gt.bt(b: Bool) -> Type:
24	  match b:
25	    case True{}:
26	      Unit
27	    case False{}:
28	      Empty
29	
30	def gt.ft(e: {False{} == True{} : Bool}) -> Empty:
31	  %Equal.sym(Bool, False{}, True{}, e) : gt.bt(_)
32	  Unit{}
33	
34	def gt.tf(e: {True{} == False{} : Bool}) -> Empty:
35	  %e : gt.bt(_)
36	  Unit{}
37	
38	def 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	
43	def 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	
49	def 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
63	def 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
81	def 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	
98	def 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	
103	def 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
109	def 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
114	def 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	
124	def 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	
133	def 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)
141	def 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
149	def 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
157	def 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
167	def 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	
172	def 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	
182	def 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	
187	def gt.hd9() -> {Nat.is_lt(9n, 32n) == True{} : Bool}:
188	  {==}
189	
190	def gt.hd8() -> {Nat.is_lt(8n, 32n) == True{} : Bool}:
191	  {==}
192	
193	def 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
197	def 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	
204	def 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
214	def 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	
221	def 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	
232	def 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	
239	def 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	
242	def 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	
250	def 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	
253	def gt.hl_elist(+f: G.Gf8Field) -> {List.length(&2, U32, gt.elist(510n, f, 0n)) == A.Arrays.slots(9n) : Nat}:
254	  {==}
255	
256	def gt.f0() -> {U32.from_nat(0n) == 0 : U32}:
257	  {==}
258	
259	def 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)
265	def 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
274	def 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	
288	def 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
297	def 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	
307	def 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	
310	def 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	  {==}