1 import Base 2 import bend-osdev-bytes@0.1.0.0/bytes.bend as B 3 import bend-osdev-bytes@0.1.0.0/LAWS.bend as BL 4 import bend-osdev-bytes@0.1.0.0/PROOF.bend as BP 5 import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M 6 import ./legacy_ciphers.bend as L 7 import ./des.bend as D 8 import ./tdes.bend as T 9 import ./sm4.bend as S 10 import ./camellia.bend as C 11 import ./serpent.bend as P 12 import ./twofish.bend as F 13 import ./rc4.bend as R 14 import ./modes64.bend as X 15 import ./aria.bend as A 16 import ./cast6.bend as C6 17 import ./blowfish.bend as BF 18 import ./cast5.bend as C5 19 import ./tea.bend as TE 20 import ./xtea.bend as XT 21 import ./fcrypt.bend as FC 22 import ./LAWS.bend as Laws 23 24 # XOR undone: a == (a xor b) xor b, for every bit, word and block. Each lemma 25 # is stated simple side first, the form a rewrite (%e : P) takes. 26 27 def bool_xx(a: Bool, b: Bool) -> {a == Bool.xor(Bool.xor(a, b), b) : Bool}: 28 match a b: 29 case True{} True{}: 30 {==} 31 case True{} False{}: 32 {==} 33 case False{} True{}: 34 {==} 35 case False{} False{}: 36 {==} 37 38 def word_xx(n: Nat, a: Word(n), b: Word(n)) -> {a == Word.xor(n, Word.xor(n, a, b), b) : Word(n)}: 39 match n: 40 case 0n: 41 match a b: 42 case WNil{} WNil{}: 43 {==} 44 case 1n+p: 45 match a b: 46 case WCon{ah, at} WCon{bh, bt}: 47 %bool_xx(ah, bh) : {WCon{ah, at} == WCon{_, Word.xor(p, Word.xor(p, at, bt), bt)} : Word(1n+p)} 48 %word_xx(p, at, bt) : {WCon{ah, at} == WCon{ah, _} : Word(1n+p)} 49 {==} 50 51 def u32_xx(a: U32, b: U32) -> {a == U32.xor(U32.xor(a, b), b) : U32}: 52 match a b: 53 case U32{x} U32{y}: 54 %word_xx(32n, x, y) : {U32{x} == U32{_} : U32} 55 {==} 56 57 def block_xx(s: M.CmBlock, k: M.CmBlock) -> {s == M.CmBlock.xor(M.CmBlock.xor(s, k), k) : M.CmBlock}: 58 match s k: 59 case M.CmBlock{+a0, +a1, +a2, +a3} M.CmBlock{+b0, +b1, +b2, +b3}: 60 %u32_xx(a0, b0) : {M.CmBlock{a0, a1, a2, a3} == M.CmBlock{_, U32.xor(U32.xor(a1, b1), b1), U32.xor(U32.xor(a2, b2), b2), U32.xor(U32.xor(a3, b3), b3)} : M.CmBlock} 61 %u32_xx(a1, b1) : {M.CmBlock{a0, a1, a2, a3} == M.CmBlock{a0, _, U32.xor(U32.xor(a2, b2), b2), U32.xor(U32.xor(a3, b3), b3)} : M.CmBlock} 62 %u32_xx(a2, b2) : {M.CmBlock{a0, a1, a2, a3} == M.CmBlock{a0, a1, _, U32.xor(U32.xor(a3, b3), b3)} : M.CmBlock} 63 %u32_xx(a3, b3) : {M.CmBlock{a0, a1, a2, a3} == M.CmBlock{a0, a1, a2, _} : M.CmBlock} 64 {==} 65 66 # BEGIN GENERATED by gen/proof.py: bits 67 # Rotations and byte swaps undone, for every word: computed on its 32 bits 68 69 def rot_1_31(x: U32) -> {x == L.lc.rotl1.bits(L.lc.rotl31.bits(x)) : U32}: 70 match x: 71 case U32{WCon{a0, WCon{a1, WCon{a2, WCon{a3, WCon{a4, WCon{a5, WCon{a6, WCon{a7, WCon{a8, WCon{a9, WCon{a10, WCon{a11, WCon{a12, WCon{a13, WCon{a14, WCon{a15, WCon{a16, WCon{a17, WCon{a18, WCon{a19, WCon{a20, WCon{a21, WCon{a22, WCon{a23, WCon{a24, WCon{a25, WCon{a26, WCon{a27, WCon{a28, WCon{a29, WCon{a30, WCon{a31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 72 {==} 73 74 def rot_31_1(x: U32) -> {x == L.lc.rotl31.bits(L.lc.rotl1.bits(x)) : U32}: 75 match x: 76 case U32{WCon{a0, WCon{a1, WCon{a2, WCon{a3, WCon{a4, WCon{a5, WCon{a6, WCon{a7, WCon{a8, WCon{a9, WCon{a10, WCon{a11, WCon{a12, WCon{a13, WCon{a14, WCon{a15, WCon{a16, WCon{a17, WCon{a18, WCon{a19, WCon{a20, WCon{a21, WCon{a22, WCon{a23, WCon{a24, WCon{a25, WCon{a26, WCon{a27, WCon{a28, WCon{a29, WCon{a30, WCon{a31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 77 {==} 78 79 def rot_19_13(x: U32) -> {x == L.lc.rotl19.bits(L.lc.rotl13.bits(x)) : U32}: 80 match x: 81 case U32{WCon{a0, WCon{a1, WCon{a2, WCon{a3, WCon{a4, WCon{a5, WCon{a6, WCon{a7, WCon{a8, WCon{a9, WCon{a10, WCon{a11, WCon{a12, WCon{a13, WCon{a14, WCon{a15, WCon{a16, WCon{a17, WCon{a18, WCon{a19, WCon{a20, WCon{a21, WCon{a22, WCon{a23, WCon{a24, WCon{a25, WCon{a26, WCon{a27, WCon{a28, WCon{a29, WCon{a30, WCon{a31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 82 {==} 83 84 def rot_13_19(x: U32) -> {x == L.lc.rotl13.bits(L.lc.rotl19.bits(x)) : U32}: 85 match x: 86 case U32{WCon{a0, WCon{a1, WCon{a2, WCon{a3, WCon{a4, WCon{a5, WCon{a6, WCon{a7, WCon{a8, WCon{a9, WCon{a10, WCon{a11, WCon{a12, WCon{a13, WCon{a14, WCon{a15, WCon{a16, WCon{a17, WCon{a18, WCon{a19, WCon{a20, WCon{a21, WCon{a22, WCon{a23, WCon{a24, WCon{a25, WCon{a26, WCon{a27, WCon{a28, WCon{a29, WCon{a30, WCon{a31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 87 {==} 88 89 def rot_29_3(x: U32) -> {x == L.lc.rotl29.bits(L.lc.rotl3.bits(x)) : U32}: 90 match x: 91 case U32{WCon{a0, WCon{a1, WCon{a2, WCon{a3, WCon{a4, WCon{a5, WCon{a6, WCon{a7, WCon{a8, WCon{a9, WCon{a10, WCon{a11, WCon{a12, WCon{a13, WCon{a14, WCon{a15, WCon{a16, WCon{a17, WCon{a18, WCon{a19, WCon{a20, WCon{a21, WCon{a22, WCon{a23, WCon{a24, WCon{a25, WCon{a26, WCon{a27, WCon{a28, WCon{a29, WCon{a30, WCon{a31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 92 {==} 93 94 def rot_3_29(x: U32) -> {x == L.lc.rotl3.bits(L.lc.rotl29.bits(x)) : U32}: 95 match x: 96 case U32{WCon{a0, WCon{a1, WCon{a2, WCon{a3, WCon{a4, WCon{a5, WCon{a6, WCon{a7, WCon{a8, WCon{a9, WCon{a10, WCon{a11, WCon{a12, WCon{a13, WCon{a14, WCon{a15, WCon{a16, WCon{a17, WCon{a18, WCon{a19, WCon{a20, WCon{a21, WCon{a22, WCon{a23, WCon{a24, WCon{a25, WCon{a26, WCon{a27, WCon{a28, WCon{a29, WCon{a30, WCon{a31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 97 {==} 98 99 def rot_25_7(x: U32) -> {x == L.lc.rotl25.bits(L.lc.rotl7.bits(x)) : U32}: 100 match x: 101 case U32{WCon{a0, WCon{a1, WCon{a2, WCon{a3, WCon{a4, WCon{a5, WCon{a6, WCon{a7, WCon{a8, WCon{a9, WCon{a10, WCon{a11, WCon{a12, WCon{a13, WCon{a14, WCon{a15, WCon{a16, WCon{a17, WCon{a18, WCon{a19, WCon{a20, WCon{a21, WCon{a22, WCon{a23, WCon{a24, WCon{a25, WCon{a26, WCon{a27, WCon{a28, WCon{a29, WCon{a30, WCon{a31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 102 {==} 103 104 def rot_7_25(x: U32) -> {x == L.lc.rotl7.bits(L.lc.rotl25.bits(x)) : U32}: 105 match x: 106 case U32{WCon{a0, WCon{a1, WCon{a2, WCon{a3, WCon{a4, WCon{a5, WCon{a6, WCon{a7, WCon{a8, WCon{a9, WCon{a10, WCon{a11, WCon{a12, WCon{a13, WCon{a14, WCon{a15, WCon{a16, WCon{a17, WCon{a18, WCon{a19, WCon{a20, WCon{a21, WCon{a22, WCon{a23, WCon{a24, WCon{a25, WCon{a26, WCon{a27, WCon{a28, WCon{a29, WCon{a30, WCon{a31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 107 {==} 108 109 def rot_27_5(x: U32) -> {x == L.lc.rotl27.bits(L.lc.rotl5.bits(x)) : U32}: 110 match x: 111 case U32{WCon{a0, WCon{a1, WCon{a2, WCon{a3, WCon{a4, WCon{a5, WCon{a6, WCon{a7, WCon{a8, WCon{a9, WCon{a10, WCon{a11, WCon{a12, WCon{a13, WCon{a14, WCon{a15, WCon{a16, WCon{a17, WCon{a18, WCon{a19, WCon{a20, WCon{a21, WCon{a22, WCon{a23, WCon{a24, WCon{a25, WCon{a26, WCon{a27, WCon{a28, WCon{a29, WCon{a30, WCon{a31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 112 {==} 113 114 def rot_5_27(x: U32) -> {x == L.lc.rotl5.bits(L.lc.rotl27.bits(x)) : U32}: 115 match x: 116 case U32{WCon{a0, WCon{a1, WCon{a2, WCon{a3, WCon{a4, WCon{a5, WCon{a6, WCon{a7, WCon{a8, WCon{a9, WCon{a10, WCon{a11, WCon{a12, WCon{a13, WCon{a14, WCon{a15, WCon{a16, WCon{a17, WCon{a18, WCon{a19, WCon{a20, WCon{a21, WCon{a22, WCon{a23, WCon{a24, WCon{a25, WCon{a26, WCon{a27, WCon{a28, WCon{a29, WCon{a30, WCon{a31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 117 {==} 118 119 def rot_10_22(x: U32) -> {x == L.lc.rotl10.bits(L.lc.rotl22.bits(x)) : U32}: 120 match x: 121 case U32{WCon{a0, WCon{a1, WCon{a2, WCon{a3, WCon{a4, WCon{a5, WCon{a6, WCon{a7, WCon{a8, WCon{a9, WCon{a10, WCon{a11, WCon{a12, WCon{a13, WCon{a14, WCon{a15, WCon{a16, WCon{a17, WCon{a18, WCon{a19, WCon{a20, WCon{a21, WCon{a22, WCon{a23, WCon{a24, WCon{a25, WCon{a26, WCon{a27, WCon{a28, WCon{a29, WCon{a30, WCon{a31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 122 {==} 123 124 def rot_22_10(x: U32) -> {x == L.lc.rotl22.bits(L.lc.rotl10.bits(x)) : U32}: 125 match x: 126 case U32{WCon{a0, WCon{a1, WCon{a2, WCon{a3, WCon{a4, WCon{a5, WCon{a6, WCon{a7, WCon{a8, WCon{a9, WCon{a10, WCon{a11, WCon{a12, WCon{a13, WCon{a14, WCon{a15, WCon{a16, WCon{a17, WCon{a18, WCon{a19, WCon{a20, WCon{a21, WCon{a22, WCon{a23, WCon{a24, WCon{a25, WCon{a26, WCon{a27, WCon{a28, WCon{a29, WCon{a30, WCon{a31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 127 {==} 128 129 def bswap2(x: U32) -> {x == L.lc.bswap.bits(L.lc.bswap.bits(x)) : U32}: 130 match x: 131 case U32{WCon{a0, WCon{a1, WCon{a2, WCon{a3, WCon{a4, WCon{a5, WCon{a6, WCon{a7, WCon{a8, WCon{a9, WCon{a10, WCon{a11, WCon{a12, WCon{a13, WCon{a14, WCon{a15, WCon{a16, WCon{a17, WCon{a18, WCon{a19, WCon{a20, WCon{a21, WCon{a22, WCon{a23, WCon{a24, WCon{a25, WCon{a26, WCon{a27, WCon{a28, WCon{a29, WCon{a30, WCon{a31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 132 {==} 133 134 # DES's IP and IP^-1 undo each other, computed on the block's 64 bits 135 def des_ip_fp(h: D.LcDesHalves) -> {h == D.des.ip(D.des.fp(h)) : D.LcDesHalves}: 136 match h: 137 case D.LcDesHalves{U32{WCon{a0, WCon{a1, WCon{a2, WCon{a3, WCon{a4, WCon{a5, WCon{a6, WCon{a7, WCon{a8, WCon{a9, WCon{a10, WCon{a11, WCon{a12, WCon{a13, WCon{a14, WCon{a15, WCon{a16, WCon{a17, WCon{a18, WCon{a19, WCon{a20, WCon{a21, WCon{a22, WCon{a23, WCon{a24, WCon{a25, WCon{a26, WCon{a27, WCon{a28, WCon{a29, WCon{a30, WCon{a31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 138 {==} 139 140 def des_fp_ip(b: L.LcBlock64) -> {b == D.des.fp(D.des.ip(b)) : L.LcBlock64}: 141 match b: 142 case L.LcBlock64{U32{WCon{a0, WCon{a1, WCon{a2, WCon{a3, WCon{a4, WCon{a5, WCon{a6, WCon{a7, WCon{a8, WCon{a9, WCon{a10, WCon{a11, WCon{a12, WCon{a13, WCon{a14, WCon{a15, WCon{a16, WCon{a17, WCon{a18, WCon{a19, WCon{a20, WCon{a21, WCon{a22, WCon{a23, WCon{a24, WCon{a25, WCon{a26, WCon{a27, WCon{a28, WCon{a29, WCon{a30, WCon{a31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 143 {==} 144 145 # the low byte of a XOR depends only on the low bytes 146 def byte_xor_byte(z: U32, k: U32) -> {B.byte(U32.xor(z, k)) == B.byte(U32.xor(B.byte(z), k)) : U32}: 147 match z k: 148 case U32{WCon{a0, WCon{a1, WCon{a2, WCon{a3, WCon{a4, WCon{a5, WCon{a6, WCon{a7, WCon{a8, WCon{a9, WCon{a10, WCon{a11, WCon{a12, WCon{a13, WCon{a14, WCon{a15, WCon{a16, WCon{a17, WCon{a18, WCon{a19, WCon{a20, WCon{a21, WCon{a22, WCon{a23, WCon{a24, WCon{a25, WCon{a26, WCon{a27, WCon{a28, WCon{a29, WCon{a30, WCon{a31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 149 {==} 150 151 # a 64-bit block's bytes, masked and read back 152 def blk_bytes(b: L.LcBlock64) -> {L.lc.block_of(B.mask(L.lc.block_bytes(b, Nil{}))) == Some{b} : Maybe<&2, L.LcBlock64>}: 153 match b: 154 case L.LcBlock64{U32{WCon{a0, WCon{a1, WCon{a2, WCon{a3, WCon{a4, WCon{a5, WCon{a6, WCon{a7, WCon{a8, WCon{a9, WCon{a10, WCon{a11, WCon{a12, WCon{a13, WCon{a14, WCon{a15, WCon{a16, WCon{a17, WCon{a18, WCon{a19, WCon{a20, WCon{a21, WCon{a22, WCon{a23, WCon{a24, WCon{a25, WCon{a26, WCon{a27, WCon{a28, WCon{a29, WCon{a30, WCon{a31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, U32{WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, WCon{c8, WCon{c9, WCon{c10, WCon{c11, WCon{c12, WCon{c13, WCon{c14, WCon{c15, WCon{c16, WCon{c17, WCon{c18, WCon{c19, WCon{c20, WCon{c21, WCon{c22, WCon{c23, WCon{c24, WCon{c25, WCon{c26, WCon{c27, WCon{c28, WCon{c29, WCon{c30, WCon{c31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 155 {==} 156 157 def blk8(hi: U32, lo: U32) -> {L.LcBlock64{hi, lo} == L.lc.block8(B.byte(L.lc.b0.bits(hi)), B.byte(L.lc.b1.bits(hi)), B.byte(L.lc.b2.bits(hi)), B.byte(L.lc.b3.bits(hi)), B.byte(L.lc.b0.bits(lo)), B.byte(L.lc.b1.bits(lo)), B.byte(L.lc.b2.bits(lo)), B.byte(L.lc.b3.bits(lo))) : L.LcBlock64}: 158 match hi lo: 159 case U32{WCon{a0, WCon{a1, WCon{a2, WCon{a3, WCon{a4, WCon{a5, WCon{a6, WCon{a7, WCon{a8, WCon{a9, WCon{a10, WCon{a11, WCon{a12, WCon{a13, WCon{a14, WCon{a15, WCon{a16, WCon{a17, WCon{a18, WCon{a19, WCon{a20, WCon{a21, WCon{a22, WCon{a23, WCon{a24, WCon{a25, WCon{a26, WCon{a27, WCon{a28, WCon{a29, WCon{a30, WCon{a31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, WCon{c8, WCon{c9, WCon{c10, WCon{c11, WCon{c12, WCon{c13, WCon{c14, WCon{c15, WCon{c16, WCon{c17, WCon{c18, WCon{c19, WCon{c20, WCon{c21, WCon{c22, WCon{c23, WCon{c24, WCon{c25, WCon{c26, WCon{c27, WCon{c28, WCon{c29, WCon{c30, WCon{c31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 160 {==} 161 # END GENERATED: bits 162 163 # DES: the swap is its own inverse, and a Feistel round is undone whatever f 164 # is (IP and IP^-1 above) 165 166 def des_swap2(h: D.LcDesHalves) -> {h == D.des.swap(D.des.swap(h)) : D.LcDesHalves}: 167 match h: 168 case D.LcDesHalves{l, r}: 169 {==} 170 171 def des_unstep_step(+k: D.LcDesRk, h: D.LcDesHalves) -> {h == D.des.unstep(k, D.des.step(k, h)) : D.LcDesHalves}: 172 match h: 173 case D.LcDesHalves{l, +r}: 174 %u32_xx(l, D.des.f(k, r)) : {D.LcDesHalves{l, r} == D.LcDesHalves{_, r} : D.LcDesHalves} 175 {==} 176 177 def des_step_unstep(+k: D.LcDesRk, h: D.LcDesHalves) -> {h == D.des.step(k, D.des.unstep(k, h)) : D.LcDesHalves}: 178 match h: 179 case D.LcDesHalves{+a, b}: 180 %u32_xx(b, D.des.f(k, a)) : {D.LcDesHalves{a, b} == D.LcDesHalves{a, _} : D.LcDesHalves} 181 {==} 182 183 def des_unrounds_rounds(ks: List<&2, D.LcDesRk>, +h: D.LcDesHalves) -> {h == D.des.unrounds(ks, D.des.rounds(ks, h)) : D.LcDesHalves}: 184 match ks: 185 case Nil{}: 186 {==} 187 case Con{+k, +t}: 188 %des_unrounds_rounds(t, D.des.step(k, h)) : {h == D.des.unstep(k, _) : D.LcDesHalves} 189 des_unstep_step(k, h) 190 191 def des_rounds_unrounds(ks: List<&2, D.LcDesRk>, +h: D.LcDesHalves) -> {h == D.des.rounds(ks, D.des.unrounds(ks, h)) : D.LcDesHalves}: 192 match ks: 193 case Nil{}: 194 {==} 195 case Con{+k, +t}: 196 %des_step_unstep(k, D.des.unrounds(t, h)) : {h == D.des.rounds(t, _) : D.LcDesHalves} 197 des_rounds_unrounds(t, h) 198 199 def Laws.des_round_trip(k, b): 200 match k: 201 case D.LcDesKey{+ks}: 202 %des_ip_fp(D.des.swap(D.des.rounds(ks, D.des.ip(b)))) : {D.des.fp(D.des.unrounds(ks, D.des.swap(_))) == b : L.LcBlock64} 203 %des_swap2(D.des.rounds(ks, D.des.ip(b))) : {D.des.fp(D.des.unrounds(ks, _)) == b : L.LcBlock64} 204 %des_unrounds_rounds(ks, D.des.ip(b)) : {D.des.fp(_) == b : L.LcBlock64} 205 Equal.sym(L.LcBlock64, b, D.des.fp(D.des.ip(b)), des_fp_ip(b)) 206 207 def Laws.des_round_trip_dual(k, b): 208 match k: 209 case D.LcDesKey{+ks}: 210 %des_ip_fp(D.des.unrounds(ks, D.des.swap(D.des.ip(b)))) : {D.des.fp(D.des.swap(D.des.rounds(ks, _))) == b : L.LcBlock64} 211 %des_rounds_unrounds(ks, D.des.swap(D.des.ip(b))) : {D.des.fp(D.des.swap(_)) == b : L.LcBlock64} 212 %des_swap2(D.des.ip(b)) : {D.des.fp(_) == b : L.LcBlock64} 213 Equal.sym(L.LcBlock64, b, D.des.fp(D.des.ip(b)), des_fp_ip(b)) 214 215 # Triple DES: from DES's two laws 216 217 def des_rt(k: D.LcDesKey, +b: L.LcBlock64) -> {b == D.LcDes.decrypt(k, D.LcDes.encrypt(k, b)) : L.LcBlock64}: 218 Equal.sym(L.LcBlock64, D.LcDes.decrypt(k, D.LcDes.encrypt(k, b)), b, Laws.des_round_trip(k, b)) 219 220 def des_rt_dual(k: D.LcDesKey, +b: L.LcBlock64) -> {b == D.LcDes.encrypt(k, D.LcDes.decrypt(k, b)) : L.LcBlock64}: 221 Equal.sym(L.LcBlock64, D.LcDes.encrypt(k, D.LcDes.decrypt(k, b)), b, Laws.des_round_trip_dual(k, b)) 222 223 def Laws.tdes_round_trip(k, b): 224 match k: 225 case T.LcTdesKey{+k1, +k2, +k3}: 226 %des_rt(k3, D.LcDes.decrypt(k2, D.LcDes.encrypt(k1, b))) : {D.LcDes.decrypt(k1, D.LcDes.encrypt(k2, _)) == b : L.LcBlock64} 227 %des_rt_dual(k2, D.LcDes.encrypt(k1, b)) : {D.LcDes.decrypt(k1, _) == b : L.LcBlock64} 228 Laws.des_round_trip(k1, b) 229 230 def Laws.tdes_round_trip_dual(k, b): 231 match k: 232 case T.LcTdesKey{+k1, +k2, +k3}: 233 %des_rt_dual(k1, D.LcDes.encrypt(k2, D.LcDes.decrypt(k3, b))) : {D.LcDes.encrypt(k3, D.LcDes.decrypt(k2, _)) == b : L.LcBlock64} 234 %des_rt(k2, D.LcDes.decrypt(k3, b)) : {D.LcDes.encrypt(k3, _) == b : L.LcBlock64} 235 Laws.des_round_trip_dual(k3, b) 236 237 # SM4: a round is undone whatever T is; R is its own inverse 238 239 def sm4_unstep_step(+tab: L.LcTab, +rk: U32, s: M.CmBlock) -> {s == S.sm4.unstep(tab, rk, S.sm4.step(tab, rk, s)) : M.CmBlock}: 240 match s: 241 case M.CmBlock{x0, +x1, +x2, +x3}: 242 %u32_xx(x0, S.sm4.t(tab, U32.xor(U32.xor(U32.xor(x1, x2), x3), rk))) : {M.CmBlock{x0, x1, x2, x3} == M.CmBlock{_, x1, x2, x3} : M.CmBlock} 243 {==} 244 245 def sm4_step_unstep(+tab: L.LcTab, +rk: U32, s: M.CmBlock) -> {s == S.sm4.step(tab, rk, S.sm4.unstep(tab, rk, s)) : M.CmBlock}: 246 match s: 247 case M.CmBlock{+y0, +y1, +y2, y3}: 248 %u32_xx(y3, S.sm4.t(tab, U32.xor(U32.xor(U32.xor(y0, y1), y2), rk))) : {M.CmBlock{y0, y1, y2, y3} == M.CmBlock{y0, y1, y2, _} : M.CmBlock} 249 {==} 250 251 def sm4_unrounds_rounds(+tab: L.LcTab, ks: List<&2, U32>, +s: M.CmBlock) -> {s == S.sm4.unrounds(tab, ks, S.sm4.rounds(tab, ks, s)) : M.CmBlock}: 252 match ks: 253 case Nil{}: 254 {==} 255 case Con{+k, +t}: 256 %sm4_unrounds_rounds(tab, t, S.sm4.step(tab, k, s)) : {s == S.sm4.unstep(tab, k, _) : M.CmBlock} 257 sm4_unstep_step(tab, k, s) 258 259 def sm4_rounds_unrounds(+tab: L.LcTab, ks: List<&2, U32>, +s: M.CmBlock) -> {s == S.sm4.rounds(tab, ks, S.sm4.unrounds(tab, ks, s)) : M.CmBlock}: 260 match ks: 261 case Nil{}: 262 {==} 263 case Con{+k, +t}: 264 %sm4_step_unstep(tab, k, S.sm4.unrounds(tab, t, s)) : {s == S.sm4.rounds(tab, t, _) : M.CmBlock} 265 sm4_rounds_unrounds(tab, t, s) 266 267 def sm4_rev2(s: M.CmBlock) -> {s == S.sm4.rev(S.sm4.rev(s)) : M.CmBlock}: 268 match s: 269 case M.CmBlock{a, b, c, d}: 270 {==} 271 272 def Laws.sm4_round_trip(k, b): 273 match k: 274 case S.LcSm4Key{+tab, +ks}: 275 %sm4_rev2(S.sm4.rounds(tab, ks, b)) : {S.sm4.unrounds(tab, ks, _) == b : M.CmBlock} 276 Equal.sym(M.CmBlock, b, S.sm4.unrounds(tab, ks, S.sm4.rounds(tab, ks, b)), sm4_unrounds_rounds(tab, ks, b)) 277 278 def Laws.sm4_round_trip_dual(k, b): 279 match k: 280 case S.LcSm4Key{+tab, +ks}: 281 %sm4_rounds_unrounds(tab, ks, S.sm4.rev(b)) : {S.sm4.rev(_) == b : M.CmBlock} 282 Equal.sym(M.CmBlock, b, S.sm4.rev(S.sm4.rev(b)), sm4_rev2(b)) 283 284 # Camellia: each step of the cipher is undone (FL by FL^-1 and back, the 285 # rounds and whitening by XOR, whatever F is), so the list of steps is 286 287 def cam_fl_inv(x: L.LcBlock64, k: L.LcBlock64) -> {x == C.cam.flinv(C.cam.fl(x, k), k) : L.LcBlock64}: 288 match x k: 289 case L.LcBlock64{+x1, +x2} L.LcBlock64{+k1, +k2}: 290 %u32_xx(x1, U32.or(U32.xor(x2, L.lc.rotl(U32.and(x1, k1), 1n)), k2)) : {L.LcBlock64{x1, x2} == L.LcBlock64{_, U32.xor(U32.xor(x2, L.lc.rotl(U32.and(x1, k1), 1n)), L.lc.rotl(U32.and(_, k1), 1n))} : L.LcBlock64} 291 %u32_xx(x2, L.lc.rotl(U32.and(x1, k1), 1n)) : {L.LcBlock64{x1, x2} == L.LcBlock64{x1, _} : L.LcBlock64} 292 {==} 293 294 def cam_flinv_inv(y: L.LcBlock64, k: L.LcBlock64) -> {y == C.cam.fl(C.cam.flinv(y, k), k) : L.LcBlock64}: 295 match y k: 296 case L.LcBlock64{+y1, +y2} L.LcBlock64{+k1, +k2}: 297 %u32_xx(y2, L.lc.rotl(U32.and(U32.xor(y1, U32.or(y2, k2)), k1), 1n)) : {L.LcBlock64{y1, y2} == L.LcBlock64{U32.xor(U32.xor(y1, U32.or(y2, k2)), U32.or(_, k2)), _} : L.LcBlock64} 298 %u32_xx(y1, U32.or(y2, k2)) : {L.LcBlock64{y1, y2} == L.LcBlock64{_, y2} : L.LcBlock64} 299 {==} 300 301 def cam_white(a: L.LcBlock64, b: L.LcBlock64, +s: M.CmBlock) -> {s == C.cam.white(a, b, C.cam.white(a, b, s)) : M.CmBlock}: 302 match a b: 303 case L.LcBlock64{+a0, +a1} L.LcBlock64{+b0, +b1}: 304 block_xx(s, M.CmBlock{a0, a1, b0, b1}) 305 306 def cam_f1(+t: C.LcCamTabs, +k: L.LcBlock64, s: M.CmBlock) -> {s == C.cam.unop(C.LcCamF1{t, k}, C.cam.op(C.LcCamF1{t, k}, s)) : M.CmBlock}: 307 match s: 308 case M.CmBlock{+s0, +s1, +s2, +s3}: 309 %u32_xx(s2, C.cam.hi(C.cam.f(t, L.LcBlock64{s0, s1}, k))) : {M.CmBlock{s0, s1, s2, s3} == M.CmBlock{s0, s1, _, U32.xor(U32.xor(s3, C.cam.lo(C.cam.f(t, L.LcBlock64{s0, s1}, k))), C.cam.lo(C.cam.f(t, L.LcBlock64{s0, s1}, k)))} : M.CmBlock} 310 %u32_xx(s3, C.cam.lo(C.cam.f(t, L.LcBlock64{s0, s1}, k))) : {M.CmBlock{s0, s1, s2, s3} == M.CmBlock{s0, s1, s2, _} : M.CmBlock} 311 {==} 312 313 def cam_f1d(+t: C.LcCamTabs, +k: L.LcBlock64, s: M.CmBlock) -> {s == C.cam.op(C.LcCamF1{t, k}, C.cam.unop(C.LcCamF1{t, k}, s)) : M.CmBlock}: 314 match s: 315 case M.CmBlock{+s0, +s1, +s2, +s3}: 316 %u32_xx(s2, C.cam.hi(C.cam.f(t, L.LcBlock64{s0, s1}, k))) : {M.CmBlock{s0, s1, s2, s3} == M.CmBlock{s0, s1, _, U32.xor(U32.xor(s3, C.cam.lo(C.cam.f(t, L.LcBlock64{s0, s1}, k))), C.cam.lo(C.cam.f(t, L.LcBlock64{s0, s1}, k)))} : M.CmBlock} 317 %u32_xx(s3, C.cam.lo(C.cam.f(t, L.LcBlock64{s0, s1}, k))) : {M.CmBlock{s0, s1, s2, s3} == M.CmBlock{s0, s1, s2, _} : M.CmBlock} 318 {==} 319 320 def cam_f2(+t: C.LcCamTabs, +k: L.LcBlock64, s: M.CmBlock) -> {s == C.cam.unop(C.LcCamF2{t, k}, C.cam.op(C.LcCamF2{t, k}, s)) : M.CmBlock}: 321 match s: 322 case M.CmBlock{+s0, +s1, +s2, +s3}: 323 %u32_xx(s0, C.cam.hi(C.cam.f(t, L.LcBlock64{s2, s3}, k))) : {M.CmBlock{s0, s1, s2, s3} == M.CmBlock{_, U32.xor(U32.xor(s1, C.cam.lo(C.cam.f(t, L.LcBlock64{s2, s3}, k))), C.cam.lo(C.cam.f(t, L.LcBlock64{s2, s3}, k))), s2, s3} : M.CmBlock} 324 %u32_xx(s1, C.cam.lo(C.cam.f(t, L.LcBlock64{s2, s3}, k))) : {M.CmBlock{s0, s1, s2, s3} == M.CmBlock{s0, _, s2, s3} : M.CmBlock} 325 {==} 326 327 def cam_f2d(+t: C.LcCamTabs, +k: L.LcBlock64, s: M.CmBlock) -> {s == C.cam.op(C.LcCamF2{t, k}, C.cam.unop(C.LcCamF2{t, k}, s)) : M.CmBlock}: 328 match s: 329 case M.CmBlock{+s0, +s1, +s2, +s3}: 330 %u32_xx(s0, C.cam.hi(C.cam.f(t, L.LcBlock64{s2, s3}, k))) : {M.CmBlock{s0, s1, s2, s3} == M.CmBlock{_, U32.xor(U32.xor(s1, C.cam.lo(C.cam.f(t, L.LcBlock64{s2, s3}, k))), C.cam.lo(C.cam.f(t, L.LcBlock64{s2, s3}, k))), s2, s3} : M.CmBlock} 331 %u32_xx(s1, C.cam.lo(C.cam.f(t, L.LcBlock64{s2, s3}, k))) : {M.CmBlock{s0, s1, s2, s3} == M.CmBlock{s0, _, s2, s3} : M.CmBlock} 332 {==} 333 334 def cam_fl_step(a: L.LcBlock64, b: L.LcBlock64, s: M.CmBlock) -> {s == C.cam.unop(C.LcCamFl{a, b}, C.cam.op(C.LcCamFl{a, b}, s)) : M.CmBlock}: 335 match a b s: 336 case L.LcBlock64{+a0, +a1} L.LcBlock64{+b0, +b1} M.CmBlock{+s0, +s1, +s2, +s3}: 337 %cam_fl_inv(L.LcBlock64{s0, s1}, L.LcBlock64{a0, a1}) : {M.CmBlock{s0, s1, s2, s3} == M.CmBlock{C.cam.hi(_), C.cam.lo(_), C.cam.hi(C.cam.fl(C.cam.flinv(L.LcBlock64{s2, s3}, L.LcBlock64{b0, b1}), L.LcBlock64{b0, b1})), C.cam.lo(C.cam.fl(C.cam.flinv(L.LcBlock64{s2, s3}, L.LcBlock64{b0, b1}), L.LcBlock64{b0, b1}))} : M.CmBlock} 338 %cam_flinv_inv(L.LcBlock64{s2, s3}, L.LcBlock64{b0, b1}) : {M.CmBlock{s0, s1, s2, s3} == M.CmBlock{s0, s1, C.cam.hi(_), C.cam.lo(_)} : M.CmBlock} 339 {==} 340 341 def cam_fl_step_dual(a: L.LcBlock64, b: L.LcBlock64, s: M.CmBlock) -> {s == C.cam.op(C.LcCamFl{a, b}, C.cam.unop(C.LcCamFl{a, b}, s)) : M.CmBlock}: 342 match a b s: 343 case L.LcBlock64{+a0, +a1} L.LcBlock64{+b0, +b1} M.CmBlock{+s0, +s1, +s2, +s3}: 344 %cam_flinv_inv(L.LcBlock64{s0, s1}, L.LcBlock64{a0, a1}) : {M.CmBlock{s0, s1, s2, s3} == M.CmBlock{C.cam.hi(_), C.cam.lo(_), C.cam.hi(C.cam.flinv(C.cam.fl(L.LcBlock64{s2, s3}, L.LcBlock64{b0, b1}), L.LcBlock64{b0, b1})), C.cam.lo(C.cam.flinv(C.cam.fl(L.LcBlock64{s2, s3}, L.LcBlock64{b0, b1}), L.LcBlock64{b0, b1}))} : M.CmBlock} 345 %cam_fl_inv(L.LcBlock64{s2, s3}, L.LcBlock64{b0, b1}) : {M.CmBlock{s0, s1, s2, s3} == M.CmBlock{s0, s1, C.cam.hi(_), C.cam.lo(_)} : M.CmBlock} 346 {==} 347 348 def cam_unop_op(o: C.LcCamOp, +s: M.CmBlock) -> {s == C.cam.unop(o, C.cam.op(o, s)) : M.CmBlock}: 349 match o: 350 case C.LcCamWhite{a, b}: 351 cam_white(a, b, s) 352 case C.LcCamF1{t, k}: 353 cam_f1(t, k, s) 354 case C.LcCamF2{t, k}: 355 cam_f2(t, k, s) 356 case C.LcCamFl{a, b}: 357 cam_fl_step(a, b, s) 358 case C.LcCamSwap{}: 359 match s: 360 case M.CmBlock{s0, s1, s2, s3}: 361 {==} 362 363 def cam_op_unop(o: C.LcCamOp, +s: M.CmBlock) -> {s == C.cam.op(o, C.cam.unop(o, s)) : M.CmBlock}: 364 match o: 365 case C.LcCamWhite{a, b}: 366 cam_white(a, b, s) 367 case C.LcCamF1{t, k}: 368 cam_f1d(t, k, s) 369 case C.LcCamF2{t, k}: 370 cam_f2d(t, k, s) 371 case C.LcCamFl{a, b}: 372 cam_fl_step_dual(a, b, s) 373 case C.LcCamSwap{}: 374 match s: 375 case M.CmBlock{s0, s1, s2, s3}: 376 {==} 377 378 def cam_unrun_run(os: List<&2, C.LcCamOp>, +s: M.CmBlock) -> {s == C.cam.unrun(os, C.cam.run(os, s)) : M.CmBlock}: 379 match os: 380 case Nil{}: 381 {==} 382 case Con{+o, +t}: 383 %cam_unrun_run(t, C.cam.op(o, s)) : {s == C.cam.unop(o, _) : M.CmBlock} 384 cam_unop_op(o, s) 385 386 def cam_run_unrun(os: List<&2, C.LcCamOp>, +s: M.CmBlock) -> {s == C.cam.run(os, C.cam.unrun(os, s)) : M.CmBlock}: 387 match os: 388 case Nil{}: 389 {==} 390 case Con{+o, +t}: 391 %cam_op_unop(o, C.cam.unrun(t, s)) : {s == C.cam.run(t, _) : M.CmBlock} 392 cam_run_unrun(t, s) 393 394 def Laws.camellia_round_trip(k, b): 395 match k: 396 case C.LcCamelliaKey{ops}: 397 Equal.sym(M.CmBlock, b, C.cam.unrun(ops, C.cam.run(ops, b)), cam_unrun_run(ops, b)) 398 399 def Laws.camellia_round_trip_dual(k, b): 400 match k: 401 case C.LcCamelliaKey{ops}: 402 Equal.sym(M.CmBlock, b, C.cam.run(ops, C.cam.unrun(ops, b)), cam_run_unrun(ops, b)) 403 404 # Twofish: each step of the cipher is undone (a round whatever F is, by the 405 # XORs and the 1-bit rotations undone), so the list of steps is 406 407 def tf_bswap(s: M.CmBlock) -> {s == F.tf.unop(F.LcTfBswap{}, F.tf.op(F.LcTfBswap{}, s)) : M.CmBlock}: 408 match s: 409 case M.CmBlock{+a, +b, +c, +d}: 410 %bswap2(a) : {M.CmBlock{a, b, c, d} == M.CmBlock{_, L.lc.bswap.bits(L.lc.bswap.bits(b)), L.lc.bswap.bits(L.lc.bswap.bits(c)), L.lc.bswap.bits(L.lc.bswap.bits(d))} : M.CmBlock} 411 %bswap2(b) : {M.CmBlock{a, b, c, d} == M.CmBlock{a, _, L.lc.bswap.bits(L.lc.bswap.bits(c)), L.lc.bswap.bits(L.lc.bswap.bits(d))} : M.CmBlock} 412 %bswap2(c) : {M.CmBlock{a, b, c, d} == M.CmBlock{a, b, _, L.lc.bswap.bits(L.lc.bswap.bits(d))} : M.CmBlock} 413 %bswap2(d) : {M.CmBlock{a, b, c, d} == M.CmBlock{a, b, c, _} : M.CmBlock} 414 {==} 415 416 def tf_bswapd(s: M.CmBlock) -> {s == F.tf.op(F.LcTfBswap{}, F.tf.unop(F.LcTfBswap{}, s)) : M.CmBlock}: 417 match s: 418 case M.CmBlock{+a, +b, +c, +d}: 419 %bswap2(a) : {M.CmBlock{a, b, c, d} == M.CmBlock{_, L.lc.bswap.bits(L.lc.bswap.bits(b)), L.lc.bswap.bits(L.lc.bswap.bits(c)), L.lc.bswap.bits(L.lc.bswap.bits(d))} : M.CmBlock} 420 %bswap2(b) : {M.CmBlock{a, b, c, d} == M.CmBlock{a, _, L.lc.bswap.bits(L.lc.bswap.bits(c)), L.lc.bswap.bits(L.lc.bswap.bits(d))} : M.CmBlock} 421 %bswap2(c) : {M.CmBlock{a, b, c, d} == M.CmBlock{a, b, _, L.lc.bswap.bits(L.lc.bswap.bits(d))} : M.CmBlock} 422 %bswap2(d) : {M.CmBlock{a, b, c, d} == M.CmBlock{a, b, c, _} : M.CmBlock} 423 {==} 424 425 def tf_round(+tb: F.LcTfTabs, +sk: List<&2, U32>, +ka: U32, +kb: U32, s: M.CmBlock) -> {s == F.tf.unop(F.LcTfRound{tb, sk, ka, kb}, F.tf.op(F.LcTfRound{tb, sk, ka, kb}, s)) : M.CmBlock}: 426 match s: 427 case M.CmBlock{+r0, +r1, +r2, +r3}: 428 %rot_1_31(U32.xor(r2, F.tf.f0(F.tf.f(tb, sk, r0, r1, ka, kb)))) : {M.CmBlock{r0, r1, r2, r3} == M.CmBlock{r0, r1, U32.xor(_, F.tf.f0(F.tf.f(tb, sk, r0, r1, ka, kb))), L.lc.rotl31.bits(U32.xor(U32.xor(L.lc.rotl1.bits(r3), F.tf.f1(F.tf.f(tb, sk, r0, r1, ka, kb))), F.tf.f1(F.tf.f(tb, sk, r0, r1, ka, kb))))} : M.CmBlock} 429 %u32_xx(r2, F.tf.f0(F.tf.f(tb, sk, r0, r1, ka, kb))) : {M.CmBlock{r0, r1, r2, r3} == M.CmBlock{r0, r1, _, L.lc.rotl31.bits(U32.xor(U32.xor(L.lc.rotl1.bits(r3), F.tf.f1(F.tf.f(tb, sk, r0, r1, ka, kb))), F.tf.f1(F.tf.f(tb, sk, r0, r1, ka, kb))))} : M.CmBlock} 430 %u32_xx(L.lc.rotl1.bits(r3), F.tf.f1(F.tf.f(tb, sk, r0, r1, ka, kb))) : {M.CmBlock{r0, r1, r2, r3} == M.CmBlock{r0, r1, r2, L.lc.rotl31.bits(_)} : M.CmBlock} 431 %rot_31_1(r3) : {M.CmBlock{r0, r1, r2, r3} == M.CmBlock{r0, r1, r2, _} : M.CmBlock} 432 {==} 433 434 def tf_roundd(+tb: F.LcTfTabs, +sk: List<&2, U32>, +ka: U32, +kb: U32, s: M.CmBlock) -> {s == F.tf.op(F.LcTfRound{tb, sk, ka, kb}, F.tf.unop(F.LcTfRound{tb, sk, ka, kb}, s)) : M.CmBlock}: 435 match s: 436 case M.CmBlock{+a, +b, +c, +d}: 437 %u32_xx(L.lc.rotl1.bits(a), F.tf.f0(F.tf.f(tb, sk, c, d, ka, kb))) : {M.CmBlock{a, b, c, d} == M.CmBlock{L.lc.rotl31.bits(_), U32.xor(L.lc.rotl1.bits(L.lc.rotl31.bits(U32.xor(b, F.tf.f1(F.tf.f(tb, sk, c, d, ka, kb))))), F.tf.f1(F.tf.f(tb, sk, c, d, ka, kb))), c, d} : M.CmBlock} 438 %rot_31_1(a) : {M.CmBlock{a, b, c, d} == M.CmBlock{_, U32.xor(L.lc.rotl1.bits(L.lc.rotl31.bits(U32.xor(b, F.tf.f1(F.tf.f(tb, sk, c, d, ka, kb))))), F.tf.f1(F.tf.f(tb, sk, c, d, ka, kb))), c, d} : M.CmBlock} 439 %rot_1_31(U32.xor(b, F.tf.f1(F.tf.f(tb, sk, c, d, ka, kb)))) : {M.CmBlock{a, b, c, d} == M.CmBlock{a, U32.xor(_, F.tf.f1(F.tf.f(tb, sk, c, d, ka, kb))), c, d} : M.CmBlock} 440 %u32_xx(b, F.tf.f1(F.tf.f(tb, sk, c, d, ka, kb))) : {M.CmBlock{a, b, c, d} == M.CmBlock{a, _, c, d} : M.CmBlock} 441 {==} 442 443 def tf_unop_op(o: F.LcTfOp, +s: M.CmBlock) -> {s == F.tf.unop(o, F.tf.op(o, s)) : M.CmBlock}: 444 match o: 445 case F.LcTfBswap{}: 446 tf_bswap(s) 447 case F.LcTfWhite{k}: 448 block_xx(s, k) 449 case F.LcTfRound{tb, sk, ka, kb}: 450 tf_round(tb, sk, ka, kb, s) 451 case F.LcTfSwap{}: 452 match s: 453 case M.CmBlock{a, b, c, d}: 454 {==} 455 456 def tf_op_unop(o: F.LcTfOp, +s: M.CmBlock) -> {s == F.tf.op(o, F.tf.unop(o, s)) : M.CmBlock}: 457 match o: 458 case F.LcTfBswap{}: 459 tf_bswapd(s) 460 case F.LcTfWhite{k}: 461 block_xx(s, k) 462 case F.LcTfRound{tb, sk, ka, kb}: 463 tf_roundd(tb, sk, ka, kb, s) 464 case F.LcTfSwap{}: 465 match s: 466 case M.CmBlock{a, b, c, d}: 467 {==} 468 469 def tf_unrun_run(os: List<&2, F.LcTfOp>, +s: M.CmBlock) -> {s == F.tf.unrun(os, F.tf.run(os, s)) : M.CmBlock}: 470 match os: 471 case Nil{}: 472 {==} 473 case Con{+o, +t}: 474 %tf_unrun_run(t, F.tf.op(o, s)) : {s == F.tf.unop(o, _) : M.CmBlock} 475 tf_unop_op(o, s) 476 477 def tf_run_unrun(os: List<&2, F.LcTfOp>, +s: M.CmBlock) -> {s == F.tf.run(os, F.tf.unrun(os, s)) : M.CmBlock}: 478 match os: 479 case Nil{}: 480 {==} 481 case Con{+o, +t}: 482 %tf_op_unop(o, F.tf.unrun(t, s)) : {s == F.tf.run(t, _) : M.CmBlock} 483 tf_run_unrun(t, s) 484 485 def Laws.twofish_round_trip(k, b): 486 match k: 487 case F.LcTwofishKey{ops}: 488 Equal.sym(M.CmBlock, b, F.tf.unrun(ops, F.tf.run(ops, b)), tf_unrun_run(ops, b)) 489 490 def Laws.twofish_round_trip_dual(k, b): 491 match k: 492 case F.LcTwofishKey{ops}: 493 Equal.sym(M.CmBlock, b, F.tf.run(ops, F.tf.unrun(ops, b)), tf_run_unrun(ops, b)) 494 495 # Serpent: each step of the cipher is undone: an S-box layer one bit position 496 # at a time (each S-box's inverse checked on all 16 inputs), the linear 497 # transformation step by step (XORs and rotations undone), the key XORs and 498 # the byte swaps; so the list of steps is 499 500 # BEGIN GENERATED by gen/proof.py: serpent 501 # the S-box and its inverse undo each other on every 4-bit input 502 503 def sp_nib_0_t(+n: P.LcSpNib) -> {n == P.sp.nib(P.LcSp0{}, False{}, P.LcSpNib{P.sp.na(P.sp.nib(P.LcSp0{}, True{}, n)), P.sp.nb(P.sp.nib(P.LcSp0{}, True{}, n)), P.sp.nc(P.sp.nib(P.LcSp0{}, True{}, n)), P.sp.nd(P.sp.nib(P.LcSp0{}, True{}, n))}) : P.LcSpNib}: 504 match n: 505 case P.LcSpNib{a, b, c, d}: 506 match a b c d: 507 case True{} True{} True{} True{}: 508 {==} 509 case True{} True{} True{} False{}: 510 {==} 511 case True{} True{} False{} True{}: 512 {==} 513 case True{} True{} False{} False{}: 514 {==} 515 case True{} False{} True{} True{}: 516 {==} 517 case True{} False{} True{} False{}: 518 {==} 519 case True{} False{} False{} True{}: 520 {==} 521 case True{} False{} False{} False{}: 522 {==} 523 case False{} True{} True{} True{}: 524 {==} 525 case False{} True{} True{} False{}: 526 {==} 527 case False{} True{} False{} True{}: 528 {==} 529 case False{} True{} False{} False{}: 530 {==} 531 case False{} False{} True{} True{}: 532 {==} 533 case False{} False{} True{} False{}: 534 {==} 535 case False{} False{} False{} True{}: 536 {==} 537 case False{} False{} False{} False{}: 538 {==} 539 540 def sp_nib_0_f(+n: P.LcSpNib) -> {n == P.sp.nib(P.LcSp0{}, True{}, P.LcSpNib{P.sp.na(P.sp.nib(P.LcSp0{}, False{}, n)), P.sp.nb(P.sp.nib(P.LcSp0{}, False{}, n)), P.sp.nc(P.sp.nib(P.LcSp0{}, False{}, n)), P.sp.nd(P.sp.nib(P.LcSp0{}, False{}, n))}) : P.LcSpNib}: 541 match n: 542 case P.LcSpNib{a, b, c, d}: 543 match a b c d: 544 case True{} True{} True{} True{}: 545 {==} 546 case True{} True{} True{} False{}: 547 {==} 548 case True{} True{} False{} True{}: 549 {==} 550 case True{} True{} False{} False{}: 551 {==} 552 case True{} False{} True{} True{}: 553 {==} 554 case True{} False{} True{} False{}: 555 {==} 556 case True{} False{} False{} True{}: 557 {==} 558 case True{} False{} False{} False{}: 559 {==} 560 case False{} True{} True{} True{}: 561 {==} 562 case False{} True{} True{} False{}: 563 {==} 564 case False{} True{} False{} True{}: 565 {==} 566 case False{} True{} False{} False{}: 567 {==} 568 case False{} False{} True{} True{}: 569 {==} 570 case False{} False{} True{} False{}: 571 {==} 572 case False{} False{} False{} True{}: 573 {==} 574 case False{} False{} False{} False{}: 575 {==} 576 577 def sp_nib_1_t(+n: P.LcSpNib) -> {n == P.sp.nib(P.LcSp1{}, False{}, P.LcSpNib{P.sp.na(P.sp.nib(P.LcSp1{}, True{}, n)), P.sp.nb(P.sp.nib(P.LcSp1{}, True{}, n)), P.sp.nc(P.sp.nib(P.LcSp1{}, True{}, n)), P.sp.nd(P.sp.nib(P.LcSp1{}, True{}, n))}) : P.LcSpNib}: 578 match n: 579 case P.LcSpNib{a, b, c, d}: 580 match a b c d: 581 case True{} True{} True{} True{}: 582 {==} 583 case True{} True{} True{} False{}: 584 {==} 585 case True{} True{} False{} True{}: 586 {==} 587 case True{} True{} False{} False{}: 588 {==} 589 case True{} False{} True{} True{}: 590 {==} 591 case True{} False{} True{} False{}: 592 {==} 593 case True{} False{} False{} True{}: 594 {==} 595 case True{} False{} False{} False{}: 596 {==} 597 case False{} True{} True{} True{}: 598 {==} 599 case False{} True{} True{} False{}: 600 {==} 601 case False{} True{} False{} True{}: 602 {==} 603 case False{} True{} False{} False{}: 604 {==} 605 case False{} False{} True{} True{}: 606 {==} 607 case False{} False{} True{} False{}: 608 {==} 609 case False{} False{} False{} True{}: 610 {==} 611 case False{} False{} False{} False{}: 612 {==} 613 614 def sp_nib_1_f(+n: P.LcSpNib) -> {n == P.sp.nib(P.LcSp1{}, True{}, P.LcSpNib{P.sp.na(P.sp.nib(P.LcSp1{}, False{}, n)), P.sp.nb(P.sp.nib(P.LcSp1{}, False{}, n)), P.sp.nc(P.sp.nib(P.LcSp1{}, False{}, n)), P.sp.nd(P.sp.nib(P.LcSp1{}, False{}, n))}) : P.LcSpNib}: 615 match n: 616 case P.LcSpNib{a, b, c, d}: 617 match a b c d: 618 case True{} True{} True{} True{}: 619 {==} 620 case True{} True{} True{} False{}: 621 {==} 622 case True{} True{} False{} True{}: 623 {==} 624 case True{} True{} False{} False{}: 625 {==} 626 case True{} False{} True{} True{}: 627 {==} 628 case True{} False{} True{} False{}: 629 {==} 630 case True{} False{} False{} True{}: 631 {==} 632 case True{} False{} False{} False{}: 633 {==} 634 case False{} True{} True{} True{}: 635 {==} 636 case False{} True{} True{} False{}: 637 {==} 638 case False{} True{} False{} True{}: 639 {==} 640 case False{} True{} False{} False{}: 641 {==} 642 case False{} False{} True{} True{}: 643 {==} 644 case False{} False{} True{} False{}: 645 {==} 646 case False{} False{} False{} True{}: 647 {==} 648 case False{} False{} False{} False{}: 649 {==} 650 651 def sp_nib_2_t(+n: P.LcSpNib) -> {n == P.sp.nib(P.LcSp2{}, False{}, P.LcSpNib{P.sp.na(P.sp.nib(P.LcSp2{}, True{}, n)), P.sp.nb(P.sp.nib(P.LcSp2{}, True{}, n)), P.sp.nc(P.sp.nib(P.LcSp2{}, True{}, n)), P.sp.nd(P.sp.nib(P.LcSp2{}, True{}, n))}) : P.LcSpNib}: 652 match n: 653 case P.LcSpNib{a, b, c, d}: 654 match a b c d: 655 case True{} True{} True{} True{}: 656 {==} 657 case True{} True{} True{} False{}: 658 {==} 659 case True{} True{} False{} True{}: 660 {==} 661 case True{} True{} False{} False{}: 662 {==} 663 case True{} False{} True{} True{}: 664 {==} 665 case True{} False{} True{} False{}: 666 {==} 667 case True{} False{} False{} True{}: 668 {==} 669 case True{} False{} False{} False{}: 670 {==} 671 case False{} True{} True{} True{}: 672 {==} 673 case False{} True{} True{} False{}: 674 {==} 675 case False{} True{} False{} True{}: 676 {==} 677 case False{} True{} False{} False{}: 678 {==} 679 case False{} False{} True{} True{}: 680 {==} 681 case False{} False{} True{} False{}: 682 {==} 683 case False{} False{} False{} True{}: 684 {==} 685 case False{} False{} False{} False{}: 686 {==} 687 688 def sp_nib_2_f(+n: P.LcSpNib) -> {n == P.sp.nib(P.LcSp2{}, True{}, P.LcSpNib{P.sp.na(P.sp.nib(P.LcSp2{}, False{}, n)), P.sp.nb(P.sp.nib(P.LcSp2{}, False{}, n)), P.sp.nc(P.sp.nib(P.LcSp2{}, False{}, n)), P.sp.nd(P.sp.nib(P.LcSp2{}, False{}, n))}) : P.LcSpNib}: 689 match n: 690 case P.LcSpNib{a, b, c, d}: 691 match a b c d: 692 case True{} True{} True{} True{}: 693 {==} 694 case True{} True{} True{} False{}: 695 {==} 696 case True{} True{} False{} True{}: 697 {==} 698 case True{} True{} False{} False{}: 699 {==} 700 case True{} False{} True{} True{}: 701 {==} 702 case True{} False{} True{} False{}: 703 {==} 704 case True{} False{} False{} True{}: 705 {==} 706 case True{} False{} False{} False{}: 707 {==} 708 case False{} True{} True{} True{}: 709 {==} 710 case False{} True{} True{} False{}: 711 {==} 712 case False{} True{} False{} True{}: 713 {==} 714 case False{} True{} False{} False{}: 715 {==} 716 case False{} False{} True{} True{}: 717 {==} 718 case False{} False{} True{} False{}: 719 {==} 720 case False{} False{} False{} True{}: 721 {==} 722 case False{} False{} False{} False{}: 723 {==} 724 725 def sp_nib_3_t(+n: P.LcSpNib) -> {n == P.sp.nib(P.LcSp3{}, False{}, P.LcSpNib{P.sp.na(P.sp.nib(P.LcSp3{}, True{}, n)), P.sp.nb(P.sp.nib(P.LcSp3{}, True{}, n)), P.sp.nc(P.sp.nib(P.LcSp3{}, True{}, n)), P.sp.nd(P.sp.nib(P.LcSp3{}, True{}, n))}) : P.LcSpNib}: 726 match n: 727 case P.LcSpNib{a, b, c, d}: 728 match a b c d: 729 case True{} True{} True{} True{}: 730 {==} 731 case True{} True{} True{} False{}: 732 {==} 733 case True{} True{} False{} True{}: 734 {==} 735 case True{} True{} False{} False{}: 736 {==} 737 case True{} False{} True{} True{}: 738 {==} 739 case True{} False{} True{} False{}: 740 {==} 741 case True{} False{} False{} True{}: 742 {==} 743 case True{} False{} False{} False{}: 744 {==} 745 case False{} True{} True{} True{}: 746 {==} 747 case False{} True{} True{} False{}: 748 {==} 749 case False{} True{} False{} True{}: 750 {==} 751 case False{} True{} False{} False{}: 752 {==} 753 case False{} False{} True{} True{}: 754 {==} 755 case False{} False{} True{} False{}: 756 {==} 757 case False{} False{} False{} True{}: 758 {==} 759 case False{} False{} False{} False{}: 760 {==} 761 762 def sp_nib_3_f(+n: P.LcSpNib) -> {n == P.sp.nib(P.LcSp3{}, True{}, P.LcSpNib{P.sp.na(P.sp.nib(P.LcSp3{}, False{}, n)), P.sp.nb(P.sp.nib(P.LcSp3{}, False{}, n)), P.sp.nc(P.sp.nib(P.LcSp3{}, False{}, n)), P.sp.nd(P.sp.nib(P.LcSp3{}, False{}, n))}) : P.LcSpNib}: 763 match n: 764 case P.LcSpNib{a, b, c, d}: 765 match a b c d: 766 case True{} True{} True{} True{}: 767 {==} 768 case True{} True{} True{} False{}: 769 {==} 770 case True{} True{} False{} True{}: 771 {==} 772 case True{} True{} False{} False{}: 773 {==} 774 case True{} False{} True{} True{}: 775 {==} 776 case True{} False{} True{} False{}: 777 {==} 778 case True{} False{} False{} True{}: 779 {==} 780 case True{} False{} False{} False{}: 781 {==} 782 case False{} True{} True{} True{}: 783 {==} 784 case False{} True{} True{} False{}: 785 {==} 786 case False{} True{} False{} True{}: 787 {==} 788 case False{} True{} False{} False{}: 789 {==} 790 case False{} False{} True{} True{}: 791 {==} 792 case False{} False{} True{} False{}: 793 {==} 794 case False{} False{} False{} True{}: 795 {==} 796 case False{} False{} False{} False{}: 797 {==} 798 799 def sp_nib_4_t(+n: P.LcSpNib) -> {n == P.sp.nib(P.LcSp4{}, False{}, P.LcSpNib{P.sp.na(P.sp.nib(P.LcSp4{}, True{}, n)), P.sp.nb(P.sp.nib(P.LcSp4{}, True{}, n)), P.sp.nc(P.sp.nib(P.LcSp4{}, True{}, n)), P.sp.nd(P.sp.nib(P.LcSp4{}, True{}, n))}) : P.LcSpNib}: 800 match n: 801 case P.LcSpNib{a, b, c, d}: 802 match a b c d: 803 case True{} True{} True{} True{}: 804 {==} 805 case True{} True{} True{} False{}: 806 {==} 807 case True{} True{} False{} True{}: 808 {==} 809 case True{} True{} False{} False{}: 810 {==} 811 case True{} False{} True{} True{}: 812 {==} 813 case True{} False{} True{} False{}: 814 {==} 815 case True{} False{} False{} True{}: 816 {==} 817 case True{} False{} False{} False{}: 818 {==} 819 case False{} True{} True{} True{}: 820 {==} 821 case False{} True{} True{} False{}: 822 {==} 823 case False{} True{} False{} True{}: 824 {==} 825 case False{} True{} False{} False{}: 826 {==} 827 case False{} False{} True{} True{}: 828 {==} 829 case False{} False{} True{} False{}: 830 {==} 831 case False{} False{} False{} True{}: 832 {==} 833 case False{} False{} False{} False{}: 834 {==} 835 836 def sp_nib_4_f(+n: P.LcSpNib) -> {n == P.sp.nib(P.LcSp4{}, True{}, P.LcSpNib{P.sp.na(P.sp.nib(P.LcSp4{}, False{}, n)), P.sp.nb(P.sp.nib(P.LcSp4{}, False{}, n)), P.sp.nc(P.sp.nib(P.LcSp4{}, False{}, n)), P.sp.nd(P.sp.nib(P.LcSp4{}, False{}, n))}) : P.LcSpNib}: 837 match n: 838 case P.LcSpNib{a, b, c, d}: 839 match a b c d: 840 case True{} True{} True{} True{}: 841 {==} 842 case True{} True{} True{} False{}: 843 {==} 844 case True{} True{} False{} True{}: 845 {==} 846 case True{} True{} False{} False{}: 847 {==} 848 case True{} False{} True{} True{}: 849 {==} 850 case True{} False{} True{} False{}: 851 {==} 852 case True{} False{} False{} True{}: 853 {==} 854 case True{} False{} False{} False{}: 855 {==} 856 case False{} True{} True{} True{}: 857 {==} 858 case False{} True{} True{} False{}: 859 {==} 860 case False{} True{} False{} True{}: 861 {==} 862 case False{} True{} False{} False{}: 863 {==} 864 case False{} False{} True{} True{}: 865 {==} 866 case False{} False{} True{} False{}: 867 {==} 868 case False{} False{} False{} True{}: 869 {==} 870 case False{} False{} False{} False{}: 871 {==} 872 873 def sp_nib_5_t(+n: P.LcSpNib) -> {n == P.sp.nib(P.LcSp5{}, False{}, P.LcSpNib{P.sp.na(P.sp.nib(P.LcSp5{}, True{}, n)), P.sp.nb(P.sp.nib(P.LcSp5{}, True{}, n)), P.sp.nc(P.sp.nib(P.LcSp5{}, True{}, n)), P.sp.nd(P.sp.nib(P.LcSp5{}, True{}, n))}) : P.LcSpNib}: 874 match n: 875 case P.LcSpNib{a, b, c, d}: 876 match a b c d: 877 case True{} True{} True{} True{}: 878 {==} 879 case True{} True{} True{} False{}: 880 {==} 881 case True{} True{} False{} True{}: 882 {==} 883 case True{} True{} False{} False{}: 884 {==} 885 case True{} False{} True{} True{}: 886 {==} 887 case True{} False{} True{} False{}: 888 {==} 889 case True{} False{} False{} True{}: 890 {==} 891 case True{} False{} False{} False{}: 892 {==} 893 case False{} True{} True{} True{}: 894 {==} 895 case False{} True{} True{} False{}: 896 {==} 897 case False{} True{} False{} True{}: 898 {==} 899 case False{} True{} False{} False{}: 900 {==} 901 case False{} False{} True{} True{}: 902 {==} 903 case False{} False{} True{} False{}: 904 {==} 905 case False{} False{} False{} True{}: 906 {==} 907 case False{} False{} False{} False{}: 908 {==} 909 910 def sp_nib_5_f(+n: P.LcSpNib) -> {n == P.sp.nib(P.LcSp5{}, True{}, P.LcSpNib{P.sp.na(P.sp.nib(P.LcSp5{}, False{}, n)), P.sp.nb(P.sp.nib(P.LcSp5{}, False{}, n)), P.sp.nc(P.sp.nib(P.LcSp5{}, False{}, n)), P.sp.nd(P.sp.nib(P.LcSp5{}, False{}, n))}) : P.LcSpNib}: 911 match n: 912 case P.LcSpNib{a, b, c, d}: 913 match a b c d: 914 case True{} True{} True{} True{}: 915 {==} 916 case True{} True{} True{} False{}: 917 {==} 918 case True{} True{} False{} True{}: 919 {==} 920 case True{} True{} False{} False{}: 921 {==} 922 case True{} False{} True{} True{}: 923 {==} 924 case True{} False{} True{} False{}: 925 {==} 926 case True{} False{} False{} True{}: 927 {==} 928 case True{} False{} False{} False{}: 929 {==} 930 case False{} True{} True{} True{}: 931 {==} 932 case False{} True{} True{} False{}: 933 {==} 934 case False{} True{} False{} True{}: 935 {==} 936 case False{} True{} False{} False{}: 937 {==} 938 case False{} False{} True{} True{}: 939 {==} 940 case False{} False{} True{} False{}: 941 {==} 942 case False{} False{} False{} True{}: 943 {==} 944 case False{} False{} False{} False{}: 945 {==} 946 947 def sp_nib_6_t(+n: P.LcSpNib) -> {n == P.sp.nib(P.LcSp6{}, False{}, P.LcSpNib{P.sp.na(P.sp.nib(P.LcSp6{}, True{}, n)), P.sp.nb(P.sp.nib(P.LcSp6{}, True{}, n)), P.sp.nc(P.sp.nib(P.LcSp6{}, True{}, n)), P.sp.nd(P.sp.nib(P.LcSp6{}, True{}, n))}) : P.LcSpNib}: 948 match n: 949 case P.LcSpNib{a, b, c, d}: 950 match a b c d: 951 case True{} True{} True{} True{}: 952 {==} 953 case True{} True{} True{} False{}: 954 {==} 955 case True{} True{} False{} True{}: 956 {==} 957 case True{} True{} False{} False{}: 958 {==} 959 case True{} False{} True{} True{}: 960 {==} 961 case True{} False{} True{} False{}: 962 {==} 963 case True{} False{} False{} True{}: 964 {==} 965 case True{} False{} False{} False{}: 966 {==} 967 case False{} True{} True{} True{}: 968 {==} 969 case False{} True{} True{} False{}: 970 {==} 971 case False{} True{} False{} True{}: 972 {==} 973 case False{} True{} False{} False{}: 974 {==} 975 case False{} False{} True{} True{}: 976 {==} 977 case False{} False{} True{} False{}: 978 {==} 979 case False{} False{} False{} True{}: 980 {==} 981 case False{} False{} False{} False{}: 982 {==} 983 984 def sp_nib_6_f(+n: P.LcSpNib) -> {n == P.sp.nib(P.LcSp6{}, True{}, P.LcSpNib{P.sp.na(P.sp.nib(P.LcSp6{}, False{}, n)), P.sp.nb(P.sp.nib(P.LcSp6{}, False{}, n)), P.sp.nc(P.sp.nib(P.LcSp6{}, False{}, n)), P.sp.nd(P.sp.nib(P.LcSp6{}, False{}, n))}) : P.LcSpNib}: 985 match n: 986 case P.LcSpNib{a, b, c, d}: 987 match a b c d: 988 case True{} True{} True{} True{}: 989 {==} 990 case True{} True{} True{} False{}: 991 {==} 992 case True{} True{} False{} True{}: 993 {==} 994 case True{} True{} False{} False{}: 995 {==} 996 case True{} False{} True{} True{}: 997 {==} 998 case True{} False{} True{} False{}: 999 {==} 1000 case True{} False{} False{} True{}: 1001 {==} 1002 case True{} False{} False{} False{}: 1003 {==} 1004 case False{} True{} True{} True{}: 1005 {==} 1006 case False{} True{} True{} False{}: 1007 {==} 1008 case False{} True{} False{} True{}: 1009 {==} 1010 case False{} True{} False{} False{}: 1011 {==} 1012 case False{} False{} True{} True{}: 1013 {==} 1014 case False{} False{} True{} False{}: 1015 {==} 1016 case False{} False{} False{} True{}: 1017 {==} 1018 case False{} False{} False{} False{}: 1019 {==} 1020 1021 def sp_nib_7_t(+n: P.LcSpNib) -> {n == P.sp.nib(P.LcSp7{}, False{}, P.LcSpNib{P.sp.na(P.sp.nib(P.LcSp7{}, True{}, n)), P.sp.nb(P.sp.nib(P.LcSp7{}, True{}, n)), P.sp.nc(P.sp.nib(P.LcSp7{}, True{}, n)), P.sp.nd(P.sp.nib(P.LcSp7{}, True{}, n))}) : P.LcSpNib}: 1022 match n: 1023 case P.LcSpNib{a, b, c, d}: 1024 match a b c d: 1025 case True{} True{} True{} True{}: 1026 {==} 1027 case True{} True{} True{} False{}: 1028 {==} 1029 case True{} True{} False{} True{}: 1030 {==} 1031 case True{} True{} False{} False{}: 1032 {==} 1033 case True{} False{} True{} True{}: 1034 {==} 1035 case True{} False{} True{} False{}: 1036 {==} 1037 case True{} False{} False{} True{}: 1038 {==} 1039 case True{} False{} False{} False{}: 1040 {==} 1041 case False{} True{} True{} True{}: 1042 {==} 1043 case False{} True{} True{} False{}: 1044 {==} 1045 case False{} True{} False{} True{}: 1046 {==} 1047 case False{} True{} False{} False{}: 1048 {==} 1049 case False{} False{} True{} True{}: 1050 {==} 1051 case False{} False{} True{} False{}: 1052 {==} 1053 case False{} False{} False{} True{}: 1054 {==} 1055 case False{} False{} False{} False{}: 1056 {==} 1057 1058 def sp_nib_7_f(+n: P.LcSpNib) -> {n == P.sp.nib(P.LcSp7{}, True{}, P.LcSpNib{P.sp.na(P.sp.nib(P.LcSp7{}, False{}, n)), P.sp.nb(P.sp.nib(P.LcSp7{}, False{}, n)), P.sp.nc(P.sp.nib(P.LcSp7{}, False{}, n)), P.sp.nd(P.sp.nib(P.LcSp7{}, False{}, n))}) : P.LcSpNib}: 1059 match n: 1060 case P.LcSpNib{a, b, c, d}: 1061 match a b c d: 1062 case True{} True{} True{} True{}: 1063 {==} 1064 case True{} True{} True{} False{}: 1065 {==} 1066 case True{} True{} False{} True{}: 1067 {==} 1068 case True{} True{} False{} False{}: 1069 {==} 1070 case True{} False{} True{} True{}: 1071 {==} 1072 case True{} False{} True{} False{}: 1073 {==} 1074 case True{} False{} False{} True{}: 1075 {==} 1076 case True{} False{} False{} False{}: 1077 {==} 1078 case False{} True{} True{} True{}: 1079 {==} 1080 case False{} True{} True{} False{}: 1081 {==} 1082 case False{} True{} False{} True{}: 1083 {==} 1084 case False{} True{} False{} False{}: 1085 {==} 1086 case False{} False{} True{} True{}: 1087 {==} 1088 case False{} False{} True{} False{}: 1089 {==} 1090 case False{} False{} False{} True{}: 1091 {==} 1092 case False{} False{} False{} False{}: 1093 {==} 1094 1095 def 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) 1145 1146 # a layer's input rebuilt from its fields gives the same layer 1147 def sp_eta(+bx: P.LcSpBox, +inv: Bool, -p: Nat, z: P.LcSpQ

) -> {P.sp.layer(bx, inv, p, z) == P.sp.layer(bx, inv, p, P.LcSpQ{P.sp.qa(p, z), P.sp.qb(p, z), P.sp.qc(p, z), P.sp.qd(p, z)}) : P.LcSpQ

}: 1148 match z: 1149 case P.LcSpQ{a, b, c, d}: 1150 {==} 1151 1152 # an S-box layer and its inverse undo each other on four m-bit words 1153 def sp_layer_inv(+bx: P.LcSpBox, +inv: Bool, m: Nat, +q: P.LcSpQ) -> {q == P.sp.layer(bx, Bool.not(inv), m, P.sp.layer(bx, inv, m, q)) : P.LcSpQ}: 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.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 {==} 1163 1164 # an S-box step and its inverse undo each other on the state 1165 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}: 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 {==} 1170 1171 # the linear transformation's steps, each undone 1172 def sp_lt1(s: M.CmBlock) -> {s == P.sp.ilt1(P.sp.lt1(s)) : M.CmBlock}: 1173 match s: 1174 case M.CmBlock{+x0, +x1, +x2, +x3}: 1175 %rot_19_13(x0) : {M.CmBlock{x0, x1, x2, x3} == M.CmBlock{_, x1, x2, x3} : M.CmBlock} 1176 {==} 1177 1178 def sp_lt1d(s: M.CmBlock) -> {s == P.sp.lt1(P.sp.ilt1(s)) : M.CmBlock}: 1179 match s: 1180 case M.CmBlock{+x0, +x1, +x2, +x3}: 1181 %rot_13_19(x0) : {M.CmBlock{x0, x1, x2, x3} == M.CmBlock{_, x1, x2, x3} : M.CmBlock} 1182 {==} 1183 1184 def sp_lt2(s: M.CmBlock) -> {s == P.sp.ilt2(P.sp.lt2(s)) : M.CmBlock}: 1185 match s: 1186 case M.CmBlock{+x0, +x1, +x2, +x3}: 1187 %rot_29_3(x2) : {M.CmBlock{x0, x1, x2, x3} == M.CmBlock{x0, x1, _, x3} : M.CmBlock} 1188 {==} 1189 1190 def sp_lt2d(s: M.CmBlock) -> {s == P.sp.lt2(P.sp.ilt2(s)) : M.CmBlock}: 1191 match s: 1192 case M.CmBlock{+x0, +x1, +x2, +x3}: 1193 %rot_3_29(x2) : {M.CmBlock{x0, x1, x2, x3} == M.CmBlock{x0, x1, _, x3} : M.CmBlock} 1194 {==} 1195 1196 def sp_lt3(s: M.CmBlock) -> {s == P.sp.lt3(P.sp.lt3(s)) : M.CmBlock}: 1197 match s: 1198 case M.CmBlock{+x0, +x1, +x2, +x3}: 1199 %u32_xx(x1, U32.xor(x0, x2)) : {M.CmBlock{x0, x1, x2, x3} == M.CmBlock{x0, _, x2, x3} : M.CmBlock} 1200 {==} 1201 1202 def sp_lt4(s: M.CmBlock) -> {s == P.sp.lt4(P.sp.lt4(s)) : M.CmBlock}: 1203 match s: 1204 case M.CmBlock{+x0, +x1, +x2, +x3}: 1205 %u32_xx(x3, U32.xor(x2, U32.shln(x0, 3n))) : {M.CmBlock{x0, x1, x2, x3} == M.CmBlock{x0, x1, x2, _} : M.CmBlock} 1206 {==} 1207 1208 def sp_lt5(s: M.CmBlock) -> {s == P.sp.ilt5(P.sp.lt5(s)) : M.CmBlock}: 1209 match s: 1210 case M.CmBlock{+x0, +x1, +x2, +x3}: 1211 %rot_31_1(x1) : {M.CmBlock{x0, x1, x2, x3} == M.CmBlock{x0, _, x2, L.lc.rotl25.bits(L.lc.rotl7.bits(x3))} : M.CmBlock} 1212 %rot_25_7(x3) : {M.CmBlock{x0, x1, x2, x3} == M.CmBlock{x0, x1, x2, _} : M.CmBlock} 1213 {==} 1214 1215 def sp_lt5d(s: M.CmBlock) -> {s == P.sp.lt5(P.sp.ilt5(s)) : M.CmBlock}: 1216 match s: 1217 case M.CmBlock{+x0, +x1, +x2, +x3}: 1218 %rot_1_31(x1) : {M.CmBlock{x0, x1, x2, x3} == M.CmBlock{x0, _, x2, L.lc.rotl7.bits(L.lc.rotl25.bits(x3))} : M.CmBlock} 1219 %rot_7_25(x3) : {M.CmBlock{x0, x1, x2, x3} == M.CmBlock{x0, x1, x2, _} : M.CmBlock} 1220 {==} 1221 1222 def sp_lt6(s: M.CmBlock) -> {s == P.sp.lt6(P.sp.lt6(s)) : M.CmBlock}: 1223 match s: 1224 case M.CmBlock{+x0, +x1, +x2, +x3}: 1225 %u32_xx(x0, U32.xor(x1, x3)) : {M.CmBlock{x0, x1, x2, x3} == M.CmBlock{_, x1, x2, x3} : M.CmBlock} 1226 {==} 1227 1228 def sp_lt7(s: M.CmBlock) -> {s == P.sp.lt7(P.sp.lt7(s)) : M.CmBlock}: 1229 match s: 1230 case M.CmBlock{+x0, +x1, +x2, +x3}: 1231 %u32_xx(x2, U32.xor(x3, U32.shln(x1, 7n))) : {M.CmBlock{x0, x1, x2, x3} == M.CmBlock{x0, x1, _, x3} : M.CmBlock} 1232 {==} 1233 1234 def sp_lt8(s: M.CmBlock) -> {s == P.sp.ilt8(P.sp.lt8(s)) : M.CmBlock}: 1235 match s: 1236 case M.CmBlock{+x0, +x1, +x2, +x3}: 1237 %rot_27_5(x0) : {M.CmBlock{x0, x1, x2, x3} == M.CmBlock{_, x1, L.lc.rotl10.bits(L.lc.rotl22.bits(x2)), x3} : M.CmBlock} 1238 %rot_10_22(x2) : {M.CmBlock{x0, x1, x2, x3} == M.CmBlock{x0, x1, _, x3} : M.CmBlock} 1239 {==} 1240 1241 def sp_lt8d(s: M.CmBlock) -> {s == P.sp.lt8(P.sp.ilt8(s)) : M.CmBlock}: 1242 match s: 1243 case M.CmBlock{+x0, +x1, +x2, +x3}: 1244 %rot_5_27(x0) : {M.CmBlock{x0, x1, x2, x3} == M.CmBlock{_, x1, L.lc.rotl22.bits(L.lc.rotl10.bits(x2)), x3} : M.CmBlock} 1245 %rot_22_10(x2) : {M.CmBlock{x0, x1, x2, x3} == M.CmBlock{x0, x1, _, x3} : M.CmBlock} 1246 {==} 1247 1248 def sp_lt_inv(+s: M.CmBlock) -> {s == P.sp.ilt(P.sp.lt(s)) : M.CmBlock}: 1249 %sp_lt8(P.sp.lt7(P.sp.lt6(P.sp.lt5(P.sp.lt4(P.sp.lt3(P.sp.lt2(P.sp.lt1(s)))))))) : {s == P.sp.ilt1(P.sp.ilt2(P.sp.lt3(P.sp.lt4(P.sp.ilt5(P.sp.lt6(P.sp.lt7(_))))))) : M.CmBlock} 1250 %sp_lt7(P.sp.lt6(P.sp.lt5(P.sp.lt4(P.sp.lt3(P.sp.lt2(P.sp.lt1(s))))))) : {s == P.sp.ilt1(P.sp.ilt2(P.sp.lt3(P.sp.lt4(P.sp.ilt5(P.sp.lt6(_)))))) : M.CmBlock} 1251 %sp_lt6(P.sp.lt5(P.sp.lt4(P.sp.lt3(P.sp.lt2(P.sp.lt1(s)))))) : {s == P.sp.ilt1(P.sp.ilt2(P.sp.lt3(P.sp.lt4(P.sp.ilt5(_))))) : M.CmBlock} 1252 %sp_lt5(P.sp.lt4(P.sp.lt3(P.sp.lt2(P.sp.lt1(s))))) : {s == P.sp.ilt1(P.sp.ilt2(P.sp.lt3(P.sp.lt4(_)))) : M.CmBlock} 1253 %sp_lt4(P.sp.lt3(P.sp.lt2(P.sp.lt1(s)))) : {s == P.sp.ilt1(P.sp.ilt2(P.sp.lt3(_))) : M.CmBlock} 1254 %sp_lt3(P.sp.lt2(P.sp.lt1(s))) : {s == P.sp.ilt1(P.sp.ilt2(_)) : M.CmBlock} 1255 %sp_lt2(P.sp.lt1(s)) : {s == P.sp.ilt1(_) : M.CmBlock} 1256 sp_lt1(s) 1257 1258 def sp_lt_invd(+s: M.CmBlock) -> {s == P.sp.lt(P.sp.ilt(s)) : M.CmBlock}: 1259 %sp_lt1d(P.sp.ilt2(P.sp.lt3(P.sp.lt4(P.sp.ilt5(P.sp.lt6(P.sp.lt7(P.sp.ilt8(s)))))))) : {s == P.sp.lt8(P.sp.lt7(P.sp.lt6(P.sp.lt5(P.sp.lt4(P.sp.lt3(P.sp.lt2(_))))))) : M.CmBlock} 1260 %sp_lt2d(P.sp.lt3(P.sp.lt4(P.sp.ilt5(P.sp.lt6(P.sp.lt7(P.sp.ilt8(s))))))) : {s == P.sp.lt8(P.sp.lt7(P.sp.lt6(P.sp.lt5(P.sp.lt4(P.sp.lt3(_)))))) : M.CmBlock} 1261 %sp_lt3(P.sp.lt4(P.sp.ilt5(P.sp.lt6(P.sp.lt7(P.sp.ilt8(s)))))) : {s == P.sp.lt8(P.sp.lt7(P.sp.lt6(P.sp.lt5(P.sp.lt4(_))))) : M.CmBlock} 1262 %sp_lt4(P.sp.ilt5(P.sp.lt6(P.sp.lt7(P.sp.ilt8(s))))) : {s == P.sp.lt8(P.sp.lt7(P.sp.lt6(P.sp.lt5(_)))) : M.CmBlock} 1263 %sp_lt5d(P.sp.lt6(P.sp.lt7(P.sp.ilt8(s)))) : {s == P.sp.lt8(P.sp.lt7(P.sp.lt6(_))) : M.CmBlock} 1264 %sp_lt6(P.sp.lt7(P.sp.ilt8(s))) : {s == P.sp.lt8(P.sp.lt7(_)) : M.CmBlock} 1265 %sp_lt7(P.sp.ilt8(s)) : {s == P.sp.lt8(_) : M.CmBlock} 1266 sp_lt8d(s) 1267 # END GENERATED: serpent 1268 1269 def sp_bswap(s: M.CmBlock) -> {s == P.sp.unop(P.LcSpBswap{}, P.sp.op(P.LcSpBswap{}, s)) : M.CmBlock}: 1270 match s: 1271 case M.CmBlock{+a, +b, +c, +d}: 1272 %bswap2(a) : {M.CmBlock{a, b, c, d} == M.CmBlock{_, L.lc.bswap.bits(L.lc.bswap.bits(b)), L.lc.bswap.bits(L.lc.bswap.bits(c)), L.lc.bswap.bits(L.lc.bswap.bits(d))} : M.CmBlock} 1273 %bswap2(b) : {M.CmBlock{a, b, c, d} == M.CmBlock{a, _, L.lc.bswap.bits(L.lc.bswap.bits(c)), L.lc.bswap.bits(L.lc.bswap.bits(d))} : M.CmBlock} 1274 %bswap2(c) : {M.CmBlock{a, b, c, d} == M.CmBlock{a, b, _, L.lc.bswap.bits(L.lc.bswap.bits(d))} : M.CmBlock} 1275 %bswap2(d) : {M.CmBlock{a, b, c, d} == M.CmBlock{a, b, c, _} : M.CmBlock} 1276 {==} 1277 1278 def sp_bswapd(s: M.CmBlock) -> {s == P.sp.op(P.LcSpBswap{}, P.sp.unop(P.LcSpBswap{}, s)) : M.CmBlock}: 1279 match s: 1280 case M.CmBlock{+a, +b, +c, +d}: 1281 %bswap2(a) : {M.CmBlock{a, b, c, d} == M.CmBlock{_, L.lc.bswap.bits(L.lc.bswap.bits(b)), L.lc.bswap.bits(L.lc.bswap.bits(c)), L.lc.bswap.bits(L.lc.bswap.bits(d))} : M.CmBlock} 1282 %bswap2(b) : {M.CmBlock{a, b, c, d} == M.CmBlock{a, _, L.lc.bswap.bits(L.lc.bswap.bits(c)), L.lc.bswap.bits(L.lc.bswap.bits(d))} : M.CmBlock} 1283 %bswap2(c) : {M.CmBlock{a, b, c, d} == M.CmBlock{a, b, _, L.lc.bswap.bits(L.lc.bswap.bits(d))} : M.CmBlock} 1284 %bswap2(d) : {M.CmBlock{a, b, c, d} == M.CmBlock{a, b, c, _} : M.CmBlock} 1285 {==} 1286 1287 def sp_unop_op(o: P.LcSpOp, +s: M.CmBlock) -> {s == P.sp.unop(o, P.sp.op(o, s)) : M.CmBlock}: 1288 match o: 1289 case P.LcSpBswap{}: 1290 sp_bswap(s) 1291 case P.LcSpKey{k}: 1292 block_xx(s, k) 1293 case P.LcSpS{bx}: 1294 sp_sop_inv(bx, False{}, s) 1295 case P.LcSpLt{}: 1296 sp_lt_inv(s) 1297 1298 def sp_op_unop(o: P.LcSpOp, +s: M.CmBlock) -> {s == P.sp.op(o, P.sp.unop(o, s)) : M.CmBlock}: 1299 match o: 1300 case P.LcSpBswap{}: 1301 sp_bswapd(s) 1302 case P.LcSpKey{k}: 1303 block_xx(s, k) 1304 case P.LcSpS{bx}: 1305 sp_sop_inv(bx, True{}, s) 1306 case P.LcSpLt{}: 1307 sp_lt_invd(s) 1308 1309 def sp_unrun_run(os: List<&2, P.LcSpOp>, +s: M.CmBlock) -> {s == P.sp.unrun(os, P.sp.run(os, s)) : M.CmBlock}: 1310 match os: 1311 case Nil{}: 1312 {==} 1313 case Con{+o, +t}: 1314 %sp_unrun_run(t, P.sp.op(o, s)) : {s == P.sp.unop(o, _) : M.CmBlock} 1315 sp_unop_op(o, s) 1316 1317 def sp_run_unrun(os: List<&2, P.LcSpOp>, +s: M.CmBlock) -> {s == P.sp.run(os, P.sp.unrun(os, s)) : M.CmBlock}: 1318 match os: 1319 case Nil{}: 1320 {==} 1321 case Con{+o, +t}: 1322 %sp_op_unop(o, P.sp.unrun(t, s)) : {s == P.sp.run(t, _) : M.CmBlock} 1323 sp_run_unrun(t, s) 1324 1325 def Laws.serpent_round_trip(k, b): 1326 match k: 1327 case P.LcSerpentKey{ops}: 1328 Equal.sym(M.CmBlock, b, P.sp.unrun(ops, P.sp.run(ops, b)), sp_unrun_run(ops, b)) 1329 1330 def Laws.serpent_round_trip_dual(k, b): 1331 match k: 1332 case P.LcSerpentKey{ops}: 1333 Equal.sym(M.CmBlock, b, P.sp.run(ops, P.sp.unrun(ops, b)), sp_run_unrun(ops, b)) 1334 1335 # A subtraction undoes an addition, for every word (TEA and XTEA) 1336 1337 # BEGIN GENERATED by gen/proof.py: adc 1338 def adc_add_sub(n: Nat, a: Word(n), b: Word(n), c: Bool) -> {a == Word.adc(n, Word.adc(n, a, b, False{}, c), b, True{}, Bool.not(c)) : Word(n)}: 1339 match n: 1340 case 0n: 1341 match a: 1342 case WNil{}: 1343 {==} 1344 case 1n+p: 1345 match a b c: 1346 case WCon{True{}, at} WCon{True{}, bt} True{}: 1347 %adc_add_sub(p, at, bt, True{}) : {WCon{True{}, at} == WCon{True{}, _} : Word(1n+p)} 1348 {==} 1349 case WCon{True{}, at} WCon{True{}, bt} False{}: 1350 %adc_add_sub(p, at, bt, True{}) : {WCon{True{}, at} == WCon{True{}, _} : Word(1n+p)} 1351 {==} 1352 case WCon{True{}, at} WCon{False{}, bt} True{}: 1353 %adc_add_sub(p, at, bt, True{}) : {WCon{True{}, at} == WCon{True{}, _} : Word(1n+p)} 1354 {==} 1355 case WCon{True{}, at} WCon{False{}, bt} False{}: 1356 %adc_add_sub(p, at, bt, False{}) : {WCon{True{}, at} == WCon{True{}, _} : Word(1n+p)} 1357 {==} 1358 case WCon{False{}, at} WCon{True{}, bt} True{}: 1359 %adc_add_sub(p, at, bt, True{}) : {WCon{False{}, at} == WCon{False{}, _} : Word(1n+p)} 1360 {==} 1361 case WCon{False{}, at} WCon{True{}, bt} False{}: 1362 %adc_add_sub(p, at, bt, False{}) : {WCon{False{}, at} == WCon{False{}, _} : Word(1n+p)} 1363 {==} 1364 case WCon{False{}, at} WCon{False{}, bt} True{}: 1365 %adc_add_sub(p, at, bt, False{}) : {WCon{False{}, at} == WCon{False{}, _} : Word(1n+p)} 1366 {==} 1367 case WCon{False{}, at} WCon{False{}, bt} False{}: 1368 %adc_add_sub(p, at, bt, False{}) : {WCon{False{}, at} == WCon{False{}, _} : Word(1n+p)} 1369 {==} 1370 1371 def adc_sub_add(n: Nat, a: Word(n), b: Word(n), c: Bool) -> {a == Word.adc(n, Word.adc(n, a, b, True{}, c), b, False{}, Bool.not(c)) : Word(n)}: 1372 match n: 1373 case 0n: 1374 match a: 1375 case WNil{}: 1376 {==} 1377 case 1n+p: 1378 match a b c: 1379 case WCon{True{}, at} WCon{True{}, bt} True{}: 1380 %adc_sub_add(p, at, bt, True{}) : {WCon{True{}, at} == WCon{True{}, _} : Word(1n+p)} 1381 {==} 1382 case WCon{True{}, at} WCon{True{}, bt} False{}: 1383 %adc_sub_add(p, at, bt, False{}) : {WCon{True{}, at} == WCon{True{}, _} : Word(1n+p)} 1384 {==} 1385 case WCon{True{}, at} WCon{False{}, bt} True{}: 1386 %adc_sub_add(p, at, bt, True{}) : {WCon{True{}, at} == WCon{True{}, _} : Word(1n+p)} 1387 {==} 1388 case WCon{True{}, at} WCon{False{}, bt} False{}: 1389 %adc_sub_add(p, at, bt, True{}) : {WCon{True{}, at} == WCon{True{}, _} : Word(1n+p)} 1390 {==} 1391 case WCon{False{}, at} WCon{True{}, bt} True{}: 1392 %adc_sub_add(p, at, bt, False{}) : {WCon{False{}, at} == WCon{False{}, _} : Word(1n+p)} 1393 {==} 1394 case WCon{False{}, at} WCon{True{}, bt} False{}: 1395 %adc_sub_add(p, at, bt, False{}) : {WCon{False{}, at} == WCon{False{}, _} : Word(1n+p)} 1396 {==} 1397 case WCon{False{}, at} WCon{False{}, bt} True{}: 1398 %adc_sub_add(p, at, bt, True{}) : {WCon{False{}, at} == WCon{False{}, _} : Word(1n+p)} 1399 {==} 1400 case WCon{False{}, at} WCon{False{}, bt} False{}: 1401 %adc_sub_add(p, at, bt, False{}) : {WCon{False{}, at} == WCon{False{}, _} : Word(1n+p)} 1402 {==} 1403 1404 def u32_add_sub(a: U32, b: U32) -> {a == U32.sub(U32.add(a, b), b) : U32}: 1405 match a b: 1406 case U32{x} U32{y}: 1407 %adc_add_sub(32n, x, y, False{}) : {U32{x} == U32{_} : U32} 1408 {==} 1409 1410 def u32_sub_add(a: U32, b: U32) -> {a == U32.add(U32.sub(a, b), b) : U32}: 1411 match a b: 1412 case U32{x} U32{y}: 1413 %adc_sub_add(32n, x, y, True{}) : {U32{x} == U32{_} : U32} 1414 {==} 1415 # END GENERATED: adc 1416 1417 # Feistel rounds over any round function (legacy-ciphers.bend's lc.fe, for 1418 # CAST-128 and FCrypt): a round is undone whatever f is, so a list of rounds 1419 # is undone by its rounds undone in reverse order 1420 1421 def fe_unstep_step(~RK: Data, ~f: RK -> U32 -> U32, +k: RK, b: L.LcBlock64) -> {b == L.lc.fe.unstep(~RK, ~f, k, L.lc.fe.step(~RK, ~f, k, b)) : L.LcBlock64}: 1422 match b: 1423 case L.LcBlock64{l, +r}: 1424 %u32_xx(l, f(k, r)) : {L.LcBlock64{l, r} == L.LcBlock64{_, r} : L.LcBlock64} 1425 {==} 1426 1427 def fe_step_unstep(~RK: Data, ~f: RK -> U32 -> U32, +k: RK, b: L.LcBlock64) -> {b == L.lc.fe.step(~RK, ~f, k, L.lc.fe.unstep(~RK, ~f, k, b)) : L.LcBlock64}: 1428 match b: 1429 case L.LcBlock64{+l, r}: 1430 %u32_xx(r, f(k, l)) : {L.LcBlock64{l, r} == L.LcBlock64{l, _} : L.LcBlock64} 1431 {==} 1432 1433 def fe_unrun_run(~RK: Data, ~f: RK -> U32 -> U32, ks: List<&2, RK>, +b: L.LcBlock64) -> {b == L.lc.fe.unrun(~RK, ~f, ks, L.lc.fe.run(~RK, ~f, ks, b)) : L.LcBlock64}: 1434 match ks: 1435 case Nil{}: 1436 {==} 1437 case Con{+k, +t}: 1438 %fe_unrun_run(~RK, ~f, t, L.lc.fe.step(~RK, ~f, k, b)) : {b == L.lc.fe.unstep(~RK, ~f, k, _) : L.LcBlock64} 1439 fe_unstep_step(~RK, ~f, k, b) 1440 1441 def fe_run_unrun(~RK: Data, ~f: RK -> U32 -> U32, ks: List<&2, RK>, +b: L.LcBlock64) -> {b == L.lc.fe.run(~RK, ~f, ks, L.lc.fe.unrun(~RK, ~f, ks, b)) : L.LcBlock64}: 1442 match ks: 1443 case Nil{}: 1444 {==} 1445 case Con{+k, +t}: 1446 %fe_step_unstep(~RK, ~f, k, L.lc.fe.unrun(~RK, ~f, t, b)) : {b == L.lc.fe.run(~RK, ~f, t, _) : L.LcBlock64} 1447 fe_run_unrun(~RK, ~f, t, b) 1448 1449 def swap2(b: L.LcBlock64) -> {b == L.lc.swap(L.lc.swap(b)) : L.LcBlock64}: 1450 match b: 1451 case L.LcBlock64{h, l}: 1452 {==} 1453 1454 # FCrypt: its rounds, undone 1455 1456 def Laws.fcrypt_round_trip(k, b): 1457 match k: 1458 case FC.LcFcryptKey{+rks}: 1459 Equal.sym(L.LcBlock64, b, L.lc.fe.unrun(~FC.LcFcRk, ~FC.fc.f, rks, L.lc.fe.run(~FC.LcFcRk, ~FC.fc.f, rks, b)), fe_unrun_run(~FC.LcFcRk, ~FC.fc.f, rks, b)) 1460 1461 def Laws.fcrypt_round_trip_dual(k, b): 1462 match k: 1463 case FC.LcFcryptKey{+rks}: 1464 Equal.sym(L.LcBlock64, b, L.lc.fe.run(~FC.LcFcRk, ~FC.fc.f, rks, L.lc.fe.unrun(~FC.LcFcRk, ~FC.fc.f, rks, b)), fe_run_unrun(~FC.LcFcRk, ~FC.fc.f, rks, b)) 1465 1466 # CAST-128: its rounds, then the exchange of the halves, undone 1467 1468 def Laws.cast5_round_trip(k, b): 1469 match k: 1470 case C5.LcCast5Key{+rks}: 1471 %swap2(L.lc.fe.run(~C5.LcCast5Rk, ~C5.cast5.f, rks, b)) : {L.lc.fe.unrun(~C5.LcCast5Rk, ~C5.cast5.f, rks, _) == b : L.LcBlock64} 1472 Equal.sym(L.LcBlock64, b, L.lc.fe.unrun(~C5.LcCast5Rk, ~C5.cast5.f, rks, L.lc.fe.run(~C5.LcCast5Rk, ~C5.cast5.f, rks, b)), fe_unrun_run(~C5.LcCast5Rk, ~C5.cast5.f, rks, b)) 1473 1474 def Laws.cast5_round_trip_dual(k, b): 1475 match k: 1476 case C5.LcCast5Key{+rks}: 1477 %fe_run_unrun(~C5.LcCast5Rk, ~C5.cast5.f, rks, L.lc.swap(b)) : {L.lc.swap(_) == b : L.LcBlock64} 1478 Equal.sym(L.LcBlock64, b, L.lc.swap(L.lc.swap(b)), swap2(b)) 1479 1480 # TEA and XTEA: each step adds a function of one half to the other, undone 1481 # by subtracting it (the "adc" lemmas below); the byte swaps undone by 1482 # themselves 1483 1484 def tea_unop_op(o: TE.LcTeaOp, b: L.LcBlock64) -> {b == TE.tea.unop(o, TE.tea.op(o, b)) : L.LcBlock64}: 1485 match o: 1486 case TE.LcTeaY{+s, +ka, +kb}: 1487 match b: 1488 case L.LcBlock64{y, +z}: 1489 %u32_add_sub(y, TE.tea.g(z, s, ka, kb)) : {L.LcBlock64{y, z} == L.LcBlock64{_, z} : L.LcBlock64} 1490 {==} 1491 case TE.LcTeaZ{+s, +ka, +kb}: 1492 match b: 1493 case L.LcBlock64{+y, z}: 1494 %u32_add_sub(z, TE.tea.g(y, s, ka, kb)) : {L.LcBlock64{y, z} == L.LcBlock64{y, _} : L.LcBlock64} 1495 {==} 1496 case TE.LcXteaY{+c}: 1497 match b: 1498 case L.LcBlock64{y, +z}: 1499 %u32_add_sub(y, TE.xtea.g(z, c)) : {L.LcBlock64{y, z} == L.LcBlock64{_, z} : L.LcBlock64} 1500 {==} 1501 case TE.LcXteaZ{+c}: 1502 match b: 1503 case L.LcBlock64{+y, z}: 1504 %u32_add_sub(z, TE.xtea.g(y, c)) : {L.LcBlock64{y, z} == L.LcBlock64{y, _} : L.LcBlock64} 1505 {==} 1506 case TE.LcTeaBswap{}: 1507 match b: 1508 case L.LcBlock64{+y, +z}: 1509 %bswap2(y) : {L.LcBlock64{y, z} == L.LcBlock64{_, L.lc.bswap.bits(L.lc.bswap.bits(z))} : L.LcBlock64} 1510 %bswap2(z) : {L.LcBlock64{y, z} == L.LcBlock64{y, _} : L.LcBlock64} 1511 {==} 1512 1513 def tea_op_unop(o: TE.LcTeaOp, b: L.LcBlock64) -> {b == TE.tea.op(o, TE.tea.unop(o, b)) : L.LcBlock64}: 1514 match o: 1515 case TE.LcTeaY{+s, +ka, +kb}: 1516 match b: 1517 case L.LcBlock64{y, +z}: 1518 %u32_sub_add(y, TE.tea.g(z, s, ka, kb)) : {L.LcBlock64{y, z} == L.LcBlock64{_, z} : L.LcBlock64} 1519 {==} 1520 case TE.LcTeaZ{+s, +ka, +kb}: 1521 match b: 1522 case L.LcBlock64{+y, z}: 1523 %u32_sub_add(z, TE.tea.g(y, s, ka, kb)) : {L.LcBlock64{y, z} == L.LcBlock64{y, _} : L.LcBlock64} 1524 {==} 1525 case TE.LcXteaY{+c}: 1526 match b: 1527 case L.LcBlock64{y, +z}: 1528 %u32_sub_add(y, TE.xtea.g(z, c)) : {L.LcBlock64{y, z} == L.LcBlock64{_, z} : L.LcBlock64} 1529 {==} 1530 case TE.LcXteaZ{+c}: 1531 match b: 1532 case L.LcBlock64{+y, z}: 1533 %u32_sub_add(z, TE.xtea.g(y, c)) : {L.LcBlock64{y, z} == L.LcBlock64{y, _} : L.LcBlock64} 1534 {==} 1535 case TE.LcTeaBswap{}: 1536 match b: 1537 case L.LcBlock64{+y, +z}: 1538 %bswap2(y) : {L.LcBlock64{y, z} == L.LcBlock64{_, L.lc.bswap.bits(L.lc.bswap.bits(z))} : L.LcBlock64} 1539 %bswap2(z) : {L.LcBlock64{y, z} == L.LcBlock64{y, _} : L.LcBlock64} 1540 {==} 1541 1542 def tea_unrun_run(os: List<&2, TE.LcTeaOp>, +b: L.LcBlock64) -> {b == TE.tea.unrun(os, TE.tea.run(os, b)) : L.LcBlock64}: 1543 match os: 1544 case Nil{}: 1545 {==} 1546 case Con{+o, +t}: 1547 %tea_unrun_run(t, TE.tea.op(o, b)) : {b == TE.tea.unop(o, _) : L.LcBlock64} 1548 tea_unop_op(o, b) 1549 1550 def tea_run_unrun(os: List<&2, TE.LcTeaOp>, +b: L.LcBlock64) -> {b == TE.tea.run(os, TE.tea.unrun(os, b)) : L.LcBlock64}: 1551 match os: 1552 case Nil{}: 1553 {==} 1554 case Con{+o, +t}: 1555 %tea_op_unop(o, TE.tea.unrun(t, b)) : {b == TE.tea.run(t, _) : L.LcBlock64} 1556 tea_run_unrun(t, b) 1557 1558 def Laws.tea_round_trip(k, b): 1559 match k: 1560 case TE.LcTeaKey{+ops}: 1561 Equal.sym(L.LcBlock64, b, TE.tea.unrun(ops, TE.tea.run(ops, b)), tea_unrun_run(ops, b)) 1562 1563 def Laws.tea_round_trip_dual(k, b): 1564 match k: 1565 case TE.LcTeaKey{+ops}: 1566 Equal.sym(L.LcBlock64, b, TE.tea.run(ops, TE.tea.unrun(ops, b)), tea_run_unrun(ops, b)) 1567 1568 def Laws.xtea_round_trip(k, b): 1569 match k: 1570 case XT.LcXteaKey{+ops}: 1571 Equal.sym(L.LcBlock64, b, TE.tea.unrun(ops, TE.tea.run(ops, b)), tea_unrun_run(ops, b)) 1572 1573 def Laws.xtea_round_trip_dual(k, b): 1574 match k: 1575 case XT.LcXteaKey{+ops}: 1576 Equal.sym(L.LcBlock64, b, TE.tea.run(ops, TE.tea.unrun(ops, b)), tea_run_unrun(ops, b)) 1577 1578 # Blowfish: a round and the final step, each undone by XOR whatever F is 1579 1580 def bf_unop_op(o: BF.LcBfOp, b: L.LcBlock64) -> {b == BF.bf.unop(o, BF.bf.op(o, b)) : L.LcBlock64}: 1581 match o: 1582 case BF.LcBfRound{+p, +t}: 1583 match b: 1584 case L.LcBlock64{+l, +r}: 1585 %u32_xx(l, p) : {L.LcBlock64{l, r} == L.LcBlock64{_, U32.xor(U32.xor(r, BF.bf.f(t, U32.xor(l, p))), BF.bf.f(t, U32.xor(l, p)))} : L.LcBlock64} 1586 %u32_xx(r, BF.bf.f(t, U32.xor(l, p))) : {L.LcBlock64{l, r} == L.LcBlock64{l, _} : L.LcBlock64} 1587 {==} 1588 case BF.LcBfFinal{+p17, +p18}: 1589 match b: 1590 case L.LcBlock64{+l, +r}: 1591 %u32_xx(l, p17) : {L.LcBlock64{l, r} == L.LcBlock64{_, U32.xor(U32.xor(r, p18), p18)} : L.LcBlock64} 1592 %u32_xx(r, p18) : {L.LcBlock64{l, r} == L.LcBlock64{l, _} : L.LcBlock64} 1593 {==} 1594 1595 def bf_op_unop(o: BF.LcBfOp, b: L.LcBlock64) -> {b == BF.bf.op(o, BF.bf.unop(o, b)) : L.LcBlock64}: 1596 match o: 1597 case BF.LcBfRound{+p, +t}: 1598 match b: 1599 case L.LcBlock64{+x, +y}: 1600 %u32_xx(y, p) : {L.LcBlock64{x, y} == L.LcBlock64{U32.xor(U32.xor(x, BF.bf.f(t, y)), BF.bf.f(t, _)), _} : L.LcBlock64} 1601 %u32_xx(x, BF.bf.f(t, y)) : {L.LcBlock64{x, y} == L.LcBlock64{_, y} : L.LcBlock64} 1602 {==} 1603 case BF.LcBfFinal{+p17, +p18}: 1604 match b: 1605 case L.LcBlock64{+x, +y}: 1606 %u32_xx(x, p18) : {L.LcBlock64{x, y} == L.LcBlock64{_, U32.xor(U32.xor(y, p17), p17)} : L.LcBlock64} 1607 %u32_xx(y, p17) : {L.LcBlock64{x, y} == L.LcBlock64{x, _} : L.LcBlock64} 1608 {==} 1609 1610 def bf_unrun_run(os: List<&2, BF.LcBfOp>, +b: L.LcBlock64) -> {b == BF.bf.unrun(os, BF.bf.run(os, b)) : L.LcBlock64}: 1611 match os: 1612 case Nil{}: 1613 {==} 1614 case Con{+o, +t}: 1615 %bf_unrun_run(t, BF.bf.op(o, b)) : {b == BF.bf.unop(o, _) : L.LcBlock64} 1616 bf_unop_op(o, b) 1617 1618 def bf_run_unrun(os: List<&2, BF.LcBfOp>, +b: L.LcBlock64) -> {b == BF.bf.run(os, BF.bf.unrun(os, b)) : L.LcBlock64}: 1619 match os: 1620 case Nil{}: 1621 {==} 1622 case Con{+o, +t}: 1623 %bf_op_unop(o, BF.bf.unrun(t, b)) : {b == BF.bf.run(t, _) : L.LcBlock64} 1624 bf_run_unrun(t, b) 1625 1626 def Laws.blowfish_round_trip(k, b): 1627 match k: 1628 case BF.LcBlowfishKey{+ops}: 1629 Equal.sym(L.LcBlock64, b, BF.bf.unrun(ops, BF.bf.run(ops, b)), bf_unrun_run(ops, b)) 1630 1631 def Laws.blowfish_round_trip_dual(k, b): 1632 match k: 1633 case BF.LcBlowfishKey{+ops}: 1634 Equal.sym(L.LcBlock64, b, BF.bf.run(ops, BF.bf.unrun(ops, b)), bf_run_unrun(ops, b)) 1635 1636 # CAST-256: each step of a quad-round is undone by itself, so QBAR undoes Q 1637 # and Q undoes QBAR 1638 1639 def c6_sc2(k: C6.LcCast6Ks, s: M.CmBlock) -> {s == C6.c6.sc(k, C6.c6.sc(k, s)) : M.CmBlock}: 1640 match k: 1641 case C6.LcCast6Ks{+m0, +m1, +m2, +m3, +r0, +r1, +r2, +r3, +t}: 1642 match s: 1643 case M.CmBlock{a, b, c, +d}: 1644 %u32_xx(c, C5.cast.f(C5.LcCastF1{}, t, d, m0, r0)) : {M.CmBlock{a, b, c, d} == M.CmBlock{a, b, _, d} : M.CmBlock} 1645 {==} 1646 1647 def c6_sb2(k: C6.LcCast6Ks, s: M.CmBlock) -> {s == C6.c6.sb(k, C6.c6.sb(k, s)) : M.CmBlock}: 1648 match k: 1649 case C6.LcCast6Ks{+m0, +m1, +m2, +m3, +r0, +r1, +r2, +r3, +t}: 1650 match s: 1651 case M.CmBlock{a, b, +c, d}: 1652 %u32_xx(b, C5.cast.f(C5.LcCastF2{}, t, c, m1, r1)) : {M.CmBlock{a, b, c, d} == M.CmBlock{a, _, c, d} : M.CmBlock} 1653 {==} 1654 1655 def c6_sa2(k: C6.LcCast6Ks, s: M.CmBlock) -> {s == C6.c6.sa(k, C6.c6.sa(k, s)) : M.CmBlock}: 1656 match k: 1657 case C6.LcCast6Ks{+m0, +m1, +m2, +m3, +r0, +r1, +r2, +r3, +t}: 1658 match s: 1659 case M.CmBlock{a, +b, c, d}: 1660 %u32_xx(a, C5.cast.f(C5.LcCastF3{}, t, b, m2, r2)) : {M.CmBlock{a, b, c, d} == M.CmBlock{_, b, c, d} : M.CmBlock} 1661 {==} 1662 1663 def c6_sd2(k: C6.LcCast6Ks, s: M.CmBlock) -> {s == C6.c6.sd(k, C6.c6.sd(k, s)) : M.CmBlock}: 1664 match k: 1665 case C6.LcCast6Ks{+m0, +m1, +m2, +m3, +r0, +r1, +r2, +r3, +t}: 1666 match s: 1667 case M.CmBlock{+a, b, c, d}: 1668 %u32_xx(d, C5.cast.f(C5.LcCastF1{}, t, a, m3, r3)) : {M.CmBlock{a, b, c, d} == M.CmBlock{a, b, c, _} : M.CmBlock} 1669 {==} 1670 1671 def c6_qq(+k: C6.LcCast6Ks, +s: M.CmBlock) -> {s == C6.c6.qbar(k, C6.c6.q(k, s)) : M.CmBlock}: 1672 %c6_sd2(k, C6.c6.sa(k, C6.c6.sb(k, C6.c6.sc(k, s)))) : {s == C6.c6.sc(k, C6.c6.sb(k, C6.c6.sa(k, _))) : M.CmBlock} 1673 %c6_sa2(k, C6.c6.sb(k, C6.c6.sc(k, s))) : {s == C6.c6.sc(k, C6.c6.sb(k, _)) : M.CmBlock} 1674 %c6_sb2(k, C6.c6.sc(k, s)) : {s == C6.c6.sc(k, _) : M.CmBlock} 1675 c6_sc2(k, s) 1676 1677 def c6_qbq(+k: C6.LcCast6Ks, +s: M.CmBlock) -> {s == C6.c6.q(k, C6.c6.qbar(k, s)) : M.CmBlock}: 1678 %c6_sc2(k, C6.c6.sb(k, C6.c6.sa(k, C6.c6.sd(k, s)))) : {s == C6.c6.sd(k, C6.c6.sa(k, C6.c6.sb(k, _))) : M.CmBlock} 1679 %c6_sb2(k, C6.c6.sa(k, C6.c6.sd(k, s))) : {s == C6.c6.sd(k, C6.c6.sa(k, _)) : M.CmBlock} 1680 %c6_sa2(k, C6.c6.sd(k, s)) : {s == C6.c6.sd(k, _) : M.CmBlock} 1681 c6_sd2(k, s) 1682 1683 def c6_unop_op(o: C6.LcCast6Op, +s: M.CmBlock) -> {s == C6.c6.unop(o, C6.c6.op(o, s)) : M.CmBlock}: 1684 match o: 1685 case C6.LcCast6Op{fwd, +k}: 1686 match fwd: 1687 case True{}: 1688 c6_qq(k, s) 1689 case False{}: 1690 c6_qbq(k, s) 1691 1692 def c6_op_unop(o: C6.LcCast6Op, +s: M.CmBlock) -> {s == C6.c6.op(o, C6.c6.unop(o, s)) : M.CmBlock}: 1693 match o: 1694 case C6.LcCast6Op{fwd, +k}: 1695 match fwd: 1696 case True{}: 1697 c6_qbq(k, s) 1698 case False{}: 1699 c6_qq(k, s) 1700 1701 def c6_unrun_run(os: List<&2, C6.LcCast6Op>, +s: M.CmBlock) -> {s == C6.c6.unrun(os, C6.c6.run(os, s)) : M.CmBlock}: 1702 match os: 1703 case Nil{}: 1704 {==} 1705 case Con{+o, +t}: 1706 %c6_unrun_run(t, C6.c6.op(o, s)) : {s == C6.c6.unop(o, _) : M.CmBlock} 1707 c6_unop_op(o, s) 1708 1709 def c6_run_unrun(os: List<&2, C6.LcCast6Op>, +s: M.CmBlock) -> {s == C6.c6.run(os, C6.c6.unrun(os, s)) : M.CmBlock}: 1710 match os: 1711 case Nil{}: 1712 {==} 1713 case Con{+o, +t}: 1714 %c6_op_unop(o, C6.c6.unrun(t, s)) : {s == C6.c6.run(t, _) : M.CmBlock} 1715 c6_run_unrun(t, s) 1716 1717 def Laws.cast6_round_trip(k, b): 1718 match k: 1719 case C6.LcCast6Key{+ops}: 1720 Equal.sym(M.CmBlock, b, C6.c6.unrun(ops, C6.c6.run(ops, b)), c6_unrun_run(ops, b)) 1721 1722 def Laws.cast6_round_trip_dual(k, b): 1723 match k: 1724 case C6.LcCast6Key{+ops}: 1725 Equal.sym(M.CmBlock, b, C6.c6.run(ops, C6.c6.unrun(ops, b)), c6_run_unrun(ops, b)) 1726 1727 # ARIA: each step of the cipher undone (the "aria" lemmas below), so the 1728 # list of steps is; and a block survives its bytes 1729 1730 # BEGIN GENERATED by gen/proof.py: aria 1731 # each S-box and its inverse undo each other on every byte 1732 def aria_sb31(w0: Word(8n)) -> {w0 == A.aria.sb3(A.aria.sb1(w0)) : Word(8n)}: 1733 match w0: 1734 case WCon{False{}, w1}: 1735 match w1: 1736 case WCon{False{}, w2}: 1737 match w2: 1738 case WCon{False{}, w3}: 1739 match w3: 1740 case WCon{False{}, w4}: 1741 match w4: 1742 case WCon{False{}, w5}: 1743 match w5: 1744 case WCon{False{}, w6}: 1745 match w6: 1746 case WCon{False{}, w7}: 1747 match w7: 1748 case WCon{False{}, w8}: 1749 match w8: 1750 case WNil{}: 1751 {==} 1752 case WCon{True{}, w8}: 1753 match w8: 1754 case WNil{}: 1755 {==} 1756 case WCon{True{}, w7}: 1757 match w7: 1758 case WCon{False{}, w8}: 1759 match w8: 1760 case WNil{}: 1761 {==} 1762 case WCon{True{}, w8}: 1763 match w8: 1764 case WNil{}: 1765 {==} 1766 case WCon{True{}, w6}: 1767 match w6: 1768 case WCon{False{}, w7}: 1769 match w7: 1770 case WCon{False{}, w8}: 1771 match w8: 1772 case WNil{}: 1773 {==} 1774 case WCon{True{}, w8}: 1775 match w8: 1776 case WNil{}: 1777 {==} 1778 case WCon{True{}, w7}: 1779 match w7: 1780 case WCon{False{}, w8}: 1781 match w8: 1782 case WNil{}: 1783 {==} 1784 case WCon{True{}, w8}: 1785 match w8: 1786 case WNil{}: 1787 {==} 1788 case WCon{True{}, w5}: 1789 match w5: 1790 case WCon{False{}, w6}: 1791 match w6: 1792 case WCon{False{}, w7}: 1793 match w7: 1794 case WCon{False{}, w8}: 1795 match w8: 1796 case WNil{}: 1797 {==} 1798 case WCon{True{}, w8}: 1799 match w8: 1800 case WNil{}: 1801 {==} 1802 case WCon{True{}, w7}: 1803 match w7: 1804 case WCon{False{}, w8}: 1805 match w8: 1806 case WNil{}: 1807 {==} 1808 case WCon{True{}, w8}: 1809 match w8: 1810 case WNil{}: 1811 {==} 1812 case WCon{True{}, w6}: 1813 match w6: 1814 case WCon{False{}, w7}: 1815 match w7: 1816 case WCon{False{}, w8}: 1817 match w8: 1818 case WNil{}: 1819 {==} 1820 case WCon{True{}, w8}: 1821 match w8: 1822 case WNil{}: 1823 {==} 1824 case WCon{True{}, w7}: 1825 match w7: 1826 case WCon{False{}, w8}: 1827 match w8: 1828 case WNil{}: 1829 {==} 1830 case WCon{True{}, w8}: 1831 match w8: 1832 case WNil{}: 1833 {==} 1834 case WCon{True{}, w4}: 1835 match w4: 1836 case WCon{False{}, w5}: 1837 match w5: 1838 case WCon{False{}, w6}: 1839 match w6: 1840 case WCon{False{}, w7}: 1841 match w7: 1842 case WCon{False{}, w8}: 1843 match w8: 1844 case WNil{}: 1845 {==} 1846 case WCon{True{}, w8}: 1847 match w8: 1848 case WNil{}: 1849 {==} 1850 case WCon{True{}, w7}: 1851 match w7: 1852 case WCon{False{}, w8}: 1853 match w8: 1854 case WNil{}: 1855 {==} 1856 case WCon{True{}, w8}: 1857 match w8: 1858 case WNil{}: 1859 {==} 1860 case WCon{True{}, w6}: 1861 match w6: 1862 case WCon{False{}, w7}: 1863 match w7: 1864 case WCon{False{}, w8}: 1865 match w8: 1866 case WNil{}: 1867 {==} 1868 case WCon{True{}, w8}: 1869 match w8: 1870 case WNil{}: 1871 {==} 1872 case WCon{True{}, w7}: 1873 match w7: 1874 case WCon{False{}, w8}: 1875 match w8: 1876 case WNil{}: 1877 {==} 1878 case WCon{True{}, w8}: 1879 match w8: 1880 case WNil{}: 1881 {==} 1882 case WCon{True{}, w5}: 1883 match w5: 1884 case WCon{False{}, w6}: 1885 match w6: 1886 case WCon{False{}, w7}: 1887 match w7: 1888 case WCon{False{}, w8}: 1889 match w8: 1890 case WNil{}: 1891 {==} 1892 case WCon{True{}, w8}: 1893 match w8: 1894 case WNil{}: 1895 {==} 1896 case WCon{True{}, w7}: 1897 match w7: 1898 case WCon{False{}, w8}: 1899 match w8: 1900 case WNil{}: 1901 {==} 1902 case WCon{True{}, w8}: 1903 match w8: 1904 case WNil{}: 1905 {==} 1906 case WCon{True{}, w6}: 1907 match w6: 1908 case WCon{False{}, w7}: 1909 match w7: 1910 case WCon{False{}, w8}: 1911 match w8: 1912 case WNil{}: 1913 {==} 1914 case WCon{True{}, w8}: 1915 match w8: 1916 case WNil{}: 1917 {==} 1918 case WCon{True{}, w7}: 1919 match w7: 1920 case WCon{False{}, w8}: 1921 match w8: 1922 case WNil{}: 1923 {==} 1924 case WCon{True{}, w8}: 1925 match w8: 1926 case WNil{}: 1927 {==} 1928 case WCon{True{}, w3}: 1929 match w3: 1930 case WCon{False{}, w4}: 1931 match w4: 1932 case WCon{False{}, w5}: 1933 match w5: 1934 case WCon{False{}, w6}: 1935 match w6: 1936 case WCon{False{}, w7}: 1937 match w7: 1938 case WCon{False{}, w8}: 1939 match w8: 1940 case WNil{}: 1941 {==} 1942 case WCon{True{}, w8}: 1943 match w8: 1944 case WNil{}: 1945 {==} 1946 case WCon{True{}, w7}: 1947 match w7: 1948 case WCon{False{}, w8}: 1949 match w8: 1950 case WNil{}: 1951 {==} 1952 case WCon{True{}, w8}: 1953 match w8: 1954 case WNil{}: 1955 {==} 1956 case WCon{True{}, w6}: 1957 match w6: 1958 case WCon{False{}, w7}: 1959 match w7: 1960 case WCon{False{}, w8}: 1961 match w8: 1962 case WNil{}: 1963 {==} 1964 case WCon{True{}, w8}: 1965 match w8: 1966 case WNil{}: 1967 {==} 1968 case WCon{True{}, w7}: 1969 match w7: 1970 case WCon{False{}, w8}: 1971 match w8: 1972 case WNil{}: 1973 {==} 1974 case WCon{True{}, w8}: 1975 match w8: 1976 case WNil{}: 1977 {==} 1978 case WCon{True{}, w5}: 1979 match w5: 1980 case WCon{False{}, w6}: 1981 match w6: 1982 case WCon{False{}, w7}: 1983 match w7: 1984 case WCon{False{}, w8}: 1985 match w8: 1986 case WNil{}: 1987 {==} 1988 case WCon{True{}, w8}: 1989 match w8: 1990 case WNil{}: 1991 {==} 1992 case WCon{True{}, w7}: 1993 match w7: 1994 case WCon{False{}, w8}: 1995 match w8: 1996 case WNil{}: 1997 {==} 1998 case WCon{True{}, w8}: 1999 match w8: 2000 case WNil{}: Lines 1-2000 of 8799. More: https://jend.leeeet.dev/read.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&start_line=2001