def m_sel_r

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

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

480def m_sel_r(+t: Bool, +a: G.Gf8Bits, +b: G.Gf8Bits, +p: G.Gf8Bits) -> {G.Gf8Bits.mul(a, G.Gf8Bits.sel(t, b), p) == G.Gf8Bits.sel(t, G.Gf8Bits.mul(a, b, p)) : G.Gf8Bits}:
481  match t:
482    case True{}:
483      {==}
484    case False{}:
485      m_zero_r(a, p)