def lin_l

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

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

547def lin_l(ts: List<&2, Bool>, vs: List<&2, G.Gf8Bits>, +b: G.Gf8Bits, +p: G.Gf8Bits) -> {G.Gf8Bits.mul(ss(ts, vs), b, p) == ss(ts, ml(vs, b, p)) : G.Gf8Bits}:
548  match ts:
549    case Nil{}:
550      m_zero_l(b, p)
551    case Con{+t, +tr}:
552      match vs:
553        case Nil{}:
554          m_zero_l(b, p)
555        case Con{+v, +vr}:
556          %lin_l(tr, vr, b, p) : {G.Gf8Bits.mul(G.Gf8Bits.xor(G.Gf8Bits.sel(t, v), ss(tr, vr)), b, p) == G.Gf8Bits.xor(G.Gf8Bits.sel(t, G.Gf8Bits.mul(v, b, p)), _) : G.Gf8Bits}
557          %m_sel_l(t, v, b, p) : {G.Gf8Bits.mul(G.Gf8Bits.xor(G.Gf8Bits.sel(t, v), ss(tr, vr)), b, p) == G.Gf8Bits.xor(_, G.Gf8Bits.mul(ss(tr, vr), b, p)) : G.Gf8Bits}
558          m_lin_l(G.Gf8Bits.sel(t, v), ss(tr, vr), b, p)