PROOF.sp_sop_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 1164-1169 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=1164&end_line=1169

import Base
import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M
import bend-osdev-legacy-ciphers@0.1.0.0/serpent.bend as P

# an S-box step and its inverse undo each other on the state
def sp_sop_inv(+bx: P.LcSpBox, +inv: Bool, s: M.CmBlock) -> {s == P.sp.sop(bx, Bool.not(inv), P.sp.sop(bx, inv, s)) : M.CmBlock}:
  match s:
    case M.CmBlock{U32{+w0}, U32{+w1}, U32{+w2}, U32{+w3}}:
      %Equal.trans(P.LcSpQ<32n>, P.LcSpQ{w0, w1, w2, w3}, P.sp.layer(bx, Bool.not(inv), 32n, P.sp.layer(bx, inv, 32n, P.LcSpQ{w0, w1, w2, w3})), P.sp.layer(bx, Bool.not(inv), 32n, P.LcSpQ{P.sp.qa(32n, P.sp.layer(bx, inv, 32n, P.LcSpQ{w0, w1, w2, w3})), P.sp.qb(32n, P.sp.layer(bx, inv, 32n, P.LcSpQ{w0, w1, w2, w3})), P.sp.qc(32n, P.sp.layer(bx, inv, 32n, P.LcSpQ{w0, w1, w2, w3})), P.sp.qd(32n, P.sp.layer(bx, inv, 32n, P.LcSpQ{w0, w1, w2, w3}))}), sp_layer_inv(bx, inv, 32n, P.LcSpQ{w0, w1, w2, w3}), sp_eta(bx, Bool.not(inv), 32n, P.sp.layer(bx, inv, 32n, P.LcSpQ{w0, w1, w2, w3}))) : {M.CmBlock{U32{w0}, U32{w1}, U32{w2}, U32{w3}} == M.CmBlock{U32{P.sp.qa(32n, _)}, U32{P.sp.qb(32n, _)}, U32{P.sp.qc(32n, _)}, U32{P.sp.qd(32n, _)}} : M.CmBlock}
      {==}

Uses (15):
  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=U32
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend&name=CmBlock
  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_layer_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=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.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
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/serpent.bend&name=sp.sop