def sp_nib_inv

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

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

1095def sp_nib_inv(bx: P.LcSpBox, inv: Bool, +n: P.LcSpNib) -> {n == P.sp.nib(bx, Bool.not(inv), P.LcSpNib{P.sp.na(P.sp.nib(bx, inv, n)), P.sp.nb(P.sp.nib(bx, inv, n)), P.sp.nc(P.sp.nib(bx, inv, n)), P.sp.nd(P.sp.nib(bx, inv, n))}) : P.LcSpNib}:
1096  match bx:
1097    case P.LcSp0{}:
1098      match inv:
1099        case True{}:
1100          sp_nib_0_t(n)
1101        case False{}:
1102          sp_nib_0_f(n)
1103    case P.LcSp1{}:
1104      match inv:
1105        case True{}:
1106          sp_nib_1_t(n)
1107        case False{}:
1108          sp_nib_1_f(n)
1109    case P.LcSp2{}:
1110      match inv:
1111        case True{}:
1112          sp_nib_2_t(n)
1113        case False{}:
1114          sp_nib_2_f(n)
1115    case P.LcSp3{}:
1116      match inv:
1117        case True{}:
1118          sp_nib_3_t(n)
1119        case False{}:
1120          sp_nib_3_f(n)
1121    case P.LcSp4{}:
1122      match inv:
1123        case True{}:
1124          sp_nib_4_t(n)
1125        case False{}:
1126          sp_nib_4_f(n)
1127    case P.LcSp5{}:
1128      match inv:
1129        case True{}:
1130          sp_nib_5_t(n)
1131        case False{}:
1132          sp_nib_5_f(n)
1133    case P.LcSp6{}:
1134      match inv:
1135        case True{}:
1136          sp_nib_6_t(n)
1137        case False{}:
1138          sp_nib_6_f(n)
1139    case P.LcSp7{}:
1140      match inv:
1141        case True{}:
1142          sp_nib_7_t(n)
1143        case False{}:
1144          sp_nib_7_f(n)