def gt.exp_table

bend-osdev-gf@0.1.1.0 · proof_tab.bend:262

import Base
import bend-osdev-array@0.1.0.1/array.bend as A
import bend-osdev-array@0.1.0.1/LAWS.bend as AL
import bend-osdev-gf@0.1.1.0/gf.bend as G
import bend-osdev-gf@0.1.1.0/tables.bend as T

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))