def sp_sop_inv

bend-osdev-legacy-ciphers@0.1.0.0 · PROOF.bend:1164

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

1164# an S-box step and its inverse undo each other on the state
1165def 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}:
1166  match s:
1167    case M.CmBlock{U32{+w0}, U32{+w1}, U32{+w2}, U32{+w3}}:
1168      %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}
1169      {==}