def sp_layer_inv

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

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

1152# an S-box layer and its inverse undo each other on four m-bit words
1153def 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>}:
1154  match m:
1155    case 0n:
1156      {==}
1157    case 1n+(+p):
1158      match q:
1159        case P.LcSpQ{WCon{+x0, +t0}, WCon{+x1, +t1}, WCon{+x2, +t2}, WCon{+x3, +t3}}:
1160          %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>}
1161          %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>}
1162          {==}