LAWS_gfm.bend

bend-osdev-gf@0.1.2.0 · 12 lines · 0 definitions

1# GF(2^m) (gfm.bend), for every field and every input: a product is the
2# product of its factors' elements (Gfm.elt), so a factor may be reduced
3# first. In a pair of its own, with no table proofs, so that a proof
4# elsewhere (rs) can use it without importing PROOF.bend.
5import Base
6import bend-osdev-gf@0.1.2.0/gfm.bend as M
7
8law gfm_mul_elt:
9  for +f: M.GfmField
10  for +a: U32
11  for +b: U32
12  {M.Gfm.mul(f, M.Gfm.elt(f, a), b) == M.Gfm.mul(f, a, b) : U32}