def lin_x

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

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

573def lin_x(ts: List<&2, Bool>, vs: List<&2, G.Gf8Bits>, +p: G.Gf8Bits) -> {G.Gf8Bits.x(ss(ts, vs), p) == ss(ts, xl(vs, p)) : G.Gf8Bits}:
574  match ts:
575    case Nil{}:
576      x_zero(p)
577    case Con{+t, +tr}:
578      match vs:
579        case Nil{}:
580          x_zero(p)
581        case Con{+v, +vr}:
582          %lin_x(tr, vr, p) : {G.Gf8Bits.x(G.Gf8Bits.xor(G.Gf8Bits.sel(t, v), ss(tr, vr)), p) == G.Gf8Bits.xor(G.Gf8Bits.sel(t, G.Gf8Bits.x(v, p)), _) : G.Gf8Bits}
583          %x_sel(t, v, p) : {G.Gf8Bits.x(G.Gf8Bits.xor(G.Gf8Bits.sel(t, v), ss(tr, vr)), p) == G.Gf8Bits.xor(_, G.Gf8Bits.x(ss(tr, vr), p)) : G.Gf8Bits}
584          x_lin(G.Gf8Bits.sel(t, v), ss(tr, vr), p)