def m_sel_l

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

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

473def m_sel_l(+t: Bool, +a: G.Gf8Bits, +b: G.Gf8Bits, +p: G.Gf8Bits) -> {G.Gf8Bits.mul(G.Gf8Bits.sel(t, a), b, p) == G.Gf8Bits.sel(t, G.Gf8Bits.mul(a, b, p)) : G.Gf8Bits}:
474  match t:
475    case True{}:
476      {==}
477    case False{}:
478      m_zero_l(b, p)