PROOF.sp_layer_inv: def of bend-osdev-legacy-ciphers@0.1.0.0
Import: import bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend as PROOF
Lines 1152-1162 of bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&start_line=1152&end_line=1162

import Base
import bend-osdev-legacy-ciphers@0.1.0.0/serpent.bend as P

# an S-box layer and its inverse undo each other on four m-bit words
def sp_layer_inv(+bx: P.LcSpBox, +inv: Bool, m: Nat, +q: P.LcSpQ<m>) -> {q == P.sp.layer(bx, Bool.not(inv), m, P.sp.layer(bx, inv, m, q)) : P.LcSpQ<m>}:
  match m:
    case 0n:
      {==}
    case 1n+(+p):
      match q:
        case P.LcSpQ{WCon{+x0, +t0}, WCon{+x1, +t1}, WCon{+x2, +t2}, WCon{+x3, +t3}}:
          %sp_nib_inv(bx, inv, P.LcSpNib{x0, x1, x2, x3}) : {P.LcSpQ{WCon{x0, t0}, WCon{x1, t1}, WCon{x2, t2}, WCon{x3, t3}} == P.LcSpQ{WCon{P.sp.na(_), P.sp.qa(p, P.sp.layer(bx, Bool.not(inv), p, P.LcSpQ{P.sp.qa(p, P.sp.layer(bx, inv, p, P.LcSpQ{t0, t1, t2, t3})), P.sp.qb(p, P.sp.layer(bx, inv, p, P.LcSpQ{t0, t1, t2, t3})), P.sp.qc(p, P.sp.layer(bx, inv, p, P.LcSpQ{t0, t1, t2, t3})), P.sp.qd(p, P.sp.layer(bx, inv, p, P.LcSpQ{t0, t1, t2, t3}))}))}, WCon{P.sp.nb(_), P.sp.qb(p, P.sp.layer(bx, Bool.not(inv), p, P.LcSpQ{P.sp.qa(p, P.sp.layer(bx, inv, p, P.LcSpQ{t0, t1, t2, t3})), P.sp.qb(p, P.sp.layer(bx, inv, p, P.LcSpQ{t0, t1, t2, t3})), P.sp.qc(p, P.sp.layer(bx, inv, p, P.LcSpQ{t0, t1, t2, t3})), P.sp.qd(p, P.sp.layer(bx, inv, p, P.LcSpQ{t0, t1, t2, t3}))}))}, WCon{P.sp.nc(_), P.sp.qc(p, P.sp.layer(bx, Bool.not(inv), p, P.LcSpQ{P.sp.qa(p, P.sp.layer(bx, inv, p, P.LcSpQ{t0, t1, t2, t3})), P.sp.qb(p, P.sp.layer(bx, inv, p, P.LcSpQ{t0, t1, t2, t3})), P.sp.qc(p, P.sp.layer(bx, inv, p, P.LcSpQ{t0, t1, t2, t3})), P.sp.qd(p, P.sp.layer(bx, inv, p, P.LcSpQ{t0, t1, t2, t3}))}))}, WCon{P.sp.nd(_), P.sp.qd(p, P.sp.layer(bx, Bool.not(inv), p, P.LcSpQ{P.sp.qa(p, P.sp.layer(bx, inv, p, P.LcSpQ{t0, t1, t2, t3})), P.sp.qb(p, P.sp.layer(bx, inv, p, P.LcSpQ{t0, t1, t2, t3})), P.sp.qc(p, P.sp.layer(bx, inv, p, P.LcSpQ{t0, t1, t2, t3})), P.sp.qd(p, P.sp.layer(bx, inv, p, P.LcSpQ{t0, t1, t2, t3}))}))}} : P.LcSpQ<1n+p>}
          %Equal.trans(P.LcSpQ<p>, P.LcSpQ{t0, t1, t2, t3}, P.sp.layer(bx, Bool.not(inv), p, P.sp.layer(bx, inv, p, P.LcSpQ{t0, t1, t2, t3})), P.sp.layer(bx, Bool.not(inv), p, P.LcSpQ{P.sp.qa(p, P.sp.layer(bx, inv, p, P.LcSpQ{t0, t1, t2, t3})), P.sp.qb(p, P.sp.layer(bx, inv, p, P.LcSpQ{t0, t1, t2, t3})), P.sp.qc(p, P.sp.layer(bx, inv, p, P.LcSpQ{t0, t1, t2, t3})), P.sp.qd(p, P.sp.layer(bx, inv, p, P.LcSpQ{t0, t1, t2, t3}))}), sp_layer_inv(bx, inv, p, P.LcSpQ{t0, t1, t2, t3}), sp_eta(bx, Bool.not(inv), p, P.sp.layer(bx, inv, p, P.LcSpQ{t0, t1, t2, t3}))) : {P.LcSpQ{WCon{x0, t0}, WCon{x1, t1}, WCon{x2, t2}, WCon{x3, t3}} == P.LcSpQ{WCon{x0, P.sp.qa(p, _)}, WCon{x1, P.sp.qb(p, _)}, WCon{x2, P.sp.qc(p, _)}, WCon{x3, P.sp.qd(p, _)}} : P.LcSpQ<1n+p>}
          {==}

Uses (19):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.not
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Con
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=sp_eta
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=sp_nib_inv
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/serpent.bend&name=LcSpBox
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/serpent.bend&name=LcSpNib
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/serpent.bend&name=LcSpQ
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/serpent.bend&name=sp.layer
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/serpent.bend&name=sp.na
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/serpent.bend&name=sp.nb
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/serpent.bend&name=sp.nc
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/serpent.bend&name=sp.nd
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/serpent.bend&name=sp.qa
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/serpent.bend&name=sp.qb
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/serpent.bend&name=sp.qc
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/serpent.bend&name=sp.qd