def elt_pow

bend-osdev-gf@0.1.1.0 · PROOF.bend:1838

import Base
import bend-osdev-gf@0.1.1.0/gf.bend as G

1838def elt_pow(n: Nat, +f: G.Gf8Field, +a: U32) -> {G.Gf8.elt(G.Gf8.pow(f, a, n)) == G.Gf8.pow(f, a, n) : U32}:
1839  match n:
1840    case 0n:
1841      {==}
1842    case 1n+k:
1843      match f:
1844        case G.Gf8Field{+poly, +gen}:
1845          Equal.cong(G.Gf8Bits, U32, r => G.Gf8Bits.to(r), G.Gf8Bits.of(G.Gf8Bits.to(G.Gf8Bits.mul(G.Gf8Bits.of(a), G.Gf8Bits.of(G.Gf8.pow(G.Gf8Field{poly, gen}, a, k)), G.Gf8Bits.of(poly)))), G.Gf8Bits.mul(G.Gf8Bits.of(a), G.Gf8Bits.of(G.Gf8.pow(G.Gf8Field{poly, gen}, a, k)), G.Gf8Bits.of(poly)), ot(G.Gf8Bits.mul(G.Gf8Bits.of(a), G.Gf8Bits.of(G.Gf8.pow(G.Gf8Field{poly, gen}, a, k)), G.Gf8Bits.of(poly))))