def lin_r

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

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

560def lin_r(ts: List<&2, Bool>, vs: List<&2, G.Gf8Bits>, +b: G.Gf8Bits, +p: G.Gf8Bits) -> {G.Gf8Bits.mul(b, ss(ts, vs), p) == ss(ts, mr(vs, b, p)) : G.Gf8Bits}:
561  match ts:
562    case Nil{}:
563      m_zero_r(b, p)
564    case Con{+t, +tr}:
565      match vs:
566        case Nil{}:
567          m_zero_r(b, p)
568        case Con{+v, +vr}:
569          %lin_r(tr, vr, b, p) : {G.Gf8Bits.mul(b, G.Gf8Bits.xor(G.Gf8Bits.sel(t, v), ss(tr, vr)), p) == G.Gf8Bits.xor(G.Gf8Bits.sel(t, G.Gf8Bits.mul(b, v, p)), _) : G.Gf8Bits}
570          %m_sel_r(t, b, v, p) : {G.Gf8Bits.mul(b, G.Gf8Bits.xor(G.Gf8Bits.sel(t, v), ss(tr, vr)), p) == G.Gf8Bits.xor(_, G.Gf8Bits.mul(b, ss(tr, vr), p)) : G.Gf8Bits}
571          m_lin_r(b, G.Gf8Bits.sel(t, v), ss(tr, vr), p)