def gt.fill_exp

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

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

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