~/jendhub

def inv32.lift

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

import bend-osdev-gf@0.1.1.0/PROOF.bend as PROOF
import Base
import bend-osdev-gf@0.1.1.0/gfm.bend as M

7785def inv32.lift(+a: U32, +nz: {U32.is_eq(M.Gfm.elt(M.Gfm.gf32(), a), 0) == False{} : Bool}) -> {M.gfm.mul.raw(M.Gfm.gf32(), M.Gfm.elt(M.Gfm.gf32(), a), M.Gfm.elt(M.Gfm.gf32(), M.gfm.pow.start(M.Gfm.gf32(), M.Gfm.elt(M.Gfm.gf32(), a), U32.sub(M.Gfm.mask(M.Gfm.gf32()), 1)))) == 1 : U32}:
7786  %fixm_nz(M.Gfm.elt(M.Gfm.gf32(), a), nz) : {M.gfm.mul.raw(M.Gfm.gf32(), _, M.Gfm.elt(M.Gfm.gf32(), M.gfm.pow.start(M.Gfm.gf32(), M.Gfm.elt(M.Gfm.gf32(), a), U32.sub(M.Gfm.mask(M.Gfm.gf32()), 1)))) == 1 : U32}
7787  %fixm_nz(M.Gfm.elt(M.Gfm.gf32(), a), nz) : {M.gfm.mul.raw(M.Gfm.gf32(), fixm(M.Gfm.elt(M.Gfm.gf32(), a)), M.Gfm.elt(M.Gfm.gf32(), M.gfm.pow.start(M.Gfm.gf32(), _, U32.sub(M.Gfm.mask(M.Gfm.gf32()), 1)))) == 1 : U32}
7788  inv32.core(a)

Uses (12)

Used by (1)