PROOF.bend

bend-osdev-cipher-core@0.1.0.0 · 349 lines · 32 definitions

1import Base
2import bend-osdev-bytes@0.1.1.0/bytes.bend as B
3import bend-osdev-bytes@0.1.1.0/LAWS.bend as BL
4import bend-osdev-bytes@0.1.1.0/PROOF.bend as BP
5import bend-osdev-cipher-core@0.1.0.0/cipher_core.bend as L
6import bend-osdev-cipher-core@0.1.0.0/modes64.bend as X
7import bend-osdev-cipher-core@0.1.0.0/LAWS.bend as Laws
8
9# XOR undone: a == (a xor b) xor b, for every bit, word and block. Each lemma
10# is stated simple side first, the form a rewrite (%e : P) takes.
11
12def bool_xx(a: Bool, b: Bool) -> {a == Bool.xor(Bool.xor(a, b), b) : Bool}:
13  match a b:
14    case True{} True{}:
15      {==}
16    case True{} False{}:
17      {==}
18    case False{} True{}:
19      {==}
20    case False{} False{}:
21      {==}
22
23def word_xx(n: Nat, a: Word(n), b: Word(n)) -> {a == Word.xor(n, Word.xor(n, a, b), b) : Word(n)}:
24  match n:
25    case 0n:
26      match a b:
27        case WNil{} WNil{}:
28          {==}
29    case 1n+p:
30      match a b:
31        case WCon{ah, at} WCon{bh, bt}:
32          %bool_xx(ah, bh) : {WCon{ah, at} == WCon{_, Word.xor(p, Word.xor(p, at, bt), bt)} : Word(1n+p)}
33          %word_xx(p, at, bt) : {WCon{ah, at} == WCon{ah, _} : Word(1n+p)}
34          {==}
35
36def u32_xx(a: U32, b: U32) -> {a == U32.xor(U32.xor(a, b), b) : U32}:
37  match a b:
38    case U32{x} U32{y}:
39      %word_xx(32n, x, y) : {U32{x} == U32{_} : U32}
40      {==}
41
42# BEGIN GENERATED by gen/proof.py: bits
43# Rotations and byte swaps undone, for every word: computed on its 32 bits
44
45def rot_1_31(x: U32) -> {x == L.lc.rotl1.bits(L.lc.rotl31.bits(x)) : U32}:
46  match x:
47    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{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
48      {==}
49
50def rot_31_1(x: U32) -> {x == L.lc.rotl31.bits(L.lc.rotl1.bits(x)) : U32}:
51  match x:
52    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{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
53      {==}
54
55def bswap2(x: U32) -> {x == L.lc.bswap.bits(L.lc.bswap.bits(x)) : U32}:
56  match x:
57    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{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
58      {==}
59
60# a 64-bit block's bytes, masked and read back
61def blk_bytes(b: L.LcBlock64) -> {L.lc.block_of(B.mask(L.lc.block_bytes(b, Nil{}))) == Some{b} : Maybe<&2, L.LcBlock64>}:
62  match b:
63    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{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
64      {==}
65
66def 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}:
67  match hi lo:
68    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{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
69      {==}
70# END GENERATED: bits
71
72# Feistel rounds over any round function (cipher-core.bend's lc.fe, for
73# CAST-128 and FCrypt): a round is undone whatever f is, so a list of rounds
74# is undone by its rounds undone in reverse order
75
76def 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}:
77  match b:
78    case L.LcBlock64{l, +r}:
79      %u32_xx(l, f(k, r)) : {L.LcBlock64{l, r} == L.LcBlock64{_, r} : L.LcBlock64}
80      {==}
81
82def 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}:
83  match b:
84    case L.LcBlock64{+l, r}:
85      %u32_xx(r, f(k, l)) : {L.LcBlock64{l, r} == L.LcBlock64{l, _} : L.LcBlock64}
86      {==}
87
88def 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}:
89  match ks:
90    case Nil{}:
91      {==}
92    case Con{+k, +t}:
93      %fe_unrun_run(~RK, ~f, t, L.lc.fe.step(~RK, ~f, k, b)) : {b == L.lc.fe.unstep(~RK, ~f, k, _) : L.LcBlock64}
94      fe_unstep_step(~RK, ~f, k, b)
95
96def 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}:
97  match ks:
98    case Nil{}:
99      {==}
100    case Con{+k, +t}:
101      %fe_step_unstep(~RK, ~f, k, L.lc.fe.unrun(~RK, ~f, t, b)) : {b == L.lc.fe.run(~RK, ~f, t, _) : L.LcBlock64}
102      fe_run_unrun(~RK, ~f, t, b)
103
104# 64-bit blocks as bytes (blk_bytes and blk8 above)
105
106def Laws.block64_octets_round_trip(b):
107  %Equal.sym(List<&2, U32>, B.Octets.to_list(B.Octets.of_list(L.lc.block_bytes(b, Nil{}))), B.mask(L.lc.block_bytes(b, Nil{})), BL.octets_to_of(L.lc.block_bytes(b, Nil{}))) : {L.lc.block_of(_) == Some{b} : Maybe<&2, L.LcBlock64>}
108  blk_bytes(b)
109
110
111# a block read from 8 bytes is written back as those bytes (on their bits,
112# and then off a list of any length)
113def b64.mget(m: Maybe<&2, L.LcBlock64>, +d: L.LcBlock64) -> L.LcBlock64:
114  match m:
115    case Some{b}:
116      b
117    case None{}:
118      d
119
120def b64.mdisc(m: Maybe<&2, L.LcBlock64>) -> Type:
121  match m:
122    case Some{b}:
123      Empty
124    case None{}:
125      Unit
126
127def b64.nsome(+bl: L.LcBlock64, h: {None{} == Some{bl} : Maybe<&2, L.LcBlock64>}) -> Empty:
128  %h : b64.mdisc(_)
129  Unit{}
130
131# a block's bytes read from 8 bytes are those bytes (on their bits)
132def b64.dbits(a0: U32, a1: U32, a2: U32, a3: U32, a4: U32, a5: U32, a6: U32, a7: U32) -> {L.LcBlock64.to_octets(b64.mget(L.lc.block_of(Con{a0, Con{a1, Con{a2, Con{a3, Con{a4, Con{a5, Con{a6, Con{a7, Nil{}}}}}}}}}), L.LcBlock64{0, 0})) == B.Octets.of_list(Con{a0, Con{a1, Con{a2, Con{a3, Con{a4, Con{a5, Con{a6, Con{a7, Nil{}}}}}}}}}) : B.Octets}:
133  match a0 a1 a2 a3 a4 a5 a6 a7:
134    case U32{WCon{b0_0, WCon{b0_1, WCon{b0_2, WCon{b0_3, WCon{b0_4, WCon{b0_5, WCon{b0_6, WCon{b0_7, WCon{b0_8, WCon{b0_9, WCon{b0_10, WCon{b0_11, WCon{b0_12, WCon{b0_13, WCon{b0_14, WCon{b0_15, WCon{b0_16, WCon{b0_17, WCon{b0_18, WCon{b0_19, WCon{b0_20, WCon{b0_21, WCon{b0_22, WCon{b0_23, WCon{b0_24, WCon{b0_25, WCon{b0_26, WCon{b0_27, WCon{b0_28, WCon{b0_29, WCon{b0_30, WCon{b0_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{b1_0, WCon{b1_1, WCon{b1_2, WCon{b1_3, WCon{b1_4, WCon{b1_5, WCon{b1_6, WCon{b1_7, WCon{b1_8, WCon{b1_9, WCon{b1_10, WCon{b1_11, WCon{b1_12, WCon{b1_13, WCon{b1_14, WCon{b1_15, WCon{b1_16, WCon{b1_17, WCon{b1_18, WCon{b1_19, WCon{b1_20, WCon{b1_21, WCon{b1_22, WCon{b1_23, WCon{b1_24, WCon{b1_25, WCon{b1_26, WCon{b1_27, WCon{b1_28, WCon{b1_29, WCon{b1_30, WCon{b1_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{b2_0, WCon{b2_1, WCon{b2_2, WCon{b2_3, WCon{b2_4, WCon{b2_5, WCon{b2_6, WCon{b2_7, WCon{b2_8, WCon{b2_9, WCon{b2_10, WCon{b2_11, WCon{b2_12, WCon{b2_13, WCon{b2_14, WCon{b2_15, WCon{b2_16, WCon{b2_17, WCon{b2_18, WCon{b2_19, WCon{b2_20, WCon{b2_21, WCon{b2_22, WCon{b2_23, WCon{b2_24, WCon{b2_25, WCon{b2_26, WCon{b2_27, WCon{b2_28, WCon{b2_29, WCon{b2_30, WCon{b2_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{b3_0, WCon{b3_1, WCon{b3_2, WCon{b3_3, WCon{b3_4, WCon{b3_5, WCon{b3_6, WCon{b3_7, WCon{b3_8, WCon{b3_9, WCon{b3_10, WCon{b3_11, WCon{b3_12, WCon{b3_13, WCon{b3_14, WCon{b3_15, WCon{b3_16, WCon{b3_17, WCon{b3_18, WCon{b3_19, WCon{b3_20, WCon{b3_21, WCon{b3_22, WCon{b3_23, WCon{b3_24, WCon{b3_25, WCon{b3_26, WCon{b3_27, WCon{b3_28, WCon{b3_29, WCon{b3_30, WCon{b3_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{b4_0, WCon{b4_1, WCon{b4_2, WCon{b4_3, WCon{b4_4, WCon{b4_5, WCon{b4_6, WCon{b4_7, WCon{b4_8, WCon{b4_9, WCon{b4_10, WCon{b4_11, WCon{b4_12, WCon{b4_13, WCon{b4_14, WCon{b4_15, WCon{b4_16, WCon{b4_17, WCon{b4_18, WCon{b4_19, WCon{b4_20, WCon{b4_21, WCon{b4_22, WCon{b4_23, WCon{b4_24, WCon{b4_25, WCon{b4_26, WCon{b4_27, WCon{b4_28, WCon{b4_29, WCon{b4_30, WCon{b4_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{b5_0, WCon{b5_1, WCon{b5_2, WCon{b5_3, WCon{b5_4, WCon{b5_5, WCon{b5_6, WCon{b5_7, WCon{b5_8, WCon{b5_9, WCon{b5_10, WCon{b5_11, WCon{b5_12, WCon{b5_13, WCon{b5_14, WCon{b5_15, WCon{b5_16, WCon{b5_17, WCon{b5_18, WCon{b5_19, WCon{b5_20, WCon{b5_21, WCon{b5_22, WCon{b5_23, WCon{b5_24, WCon{b5_25, WCon{b5_26, WCon{b5_27, WCon{b5_28, WCon{b5_29, WCon{b5_30, WCon{b5_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{b6_0, WCon{b6_1, WCon{b6_2, WCon{b6_3, WCon{b6_4, WCon{b6_5, WCon{b6_6, WCon{b6_7, WCon{b6_8, WCon{b6_9, WCon{b6_10, WCon{b6_11, WCon{b6_12, WCon{b6_13, WCon{b6_14, WCon{b6_15, WCon{b6_16, WCon{b6_17, WCon{b6_18, WCon{b6_19, WCon{b6_20, WCon{b6_21, WCon{b6_22, WCon{b6_23, WCon{b6_24, WCon{b6_25, WCon{b6_26, WCon{b6_27, WCon{b6_28, WCon{b6_29, WCon{b6_30, WCon{b6_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{b7_0, WCon{b7_1, WCon{b7_2, WCon{b7_3, WCon{b7_4, WCon{b7_5, WCon{b7_6, WCon{b7_7, WCon{b7_8, WCon{b7_9, WCon{b7_10, WCon{b7_11, WCon{b7_12, WCon{b7_13, WCon{b7_14, WCon{b7_15, WCon{b7_16, WCon{b7_17, WCon{b7_18, WCon{b7_19, WCon{b7_20, WCon{b7_21, WCon{b7_22, WCon{b7_23, WCon{b7_24, WCon{b7_25, WCon{b7_26, WCon{b7_27, WCon{b7_28, WCon{b7_29, WCon{b7_30, WCon{b7_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
135      {==}
136
137
138# a block read from a list of bytes is written back as those bytes
139def b64.dualL(+xs: List<&2, U32>, +bl: L.LcBlock64) -> {L.lc.block_of(xs) == Some{bl} : Maybe<&2, L.LcBlock64>} -> {L.LcBlock64.to_octets(bl) == B.Octets.of_list(xs) : B.Octets}:
140  match xs:
141    case Nil{}:
142      h => Empty.absurd({L.LcBlock64.to_octets(bl) == B.Octets.of_list(Nil{}) : B.Octets}, b64.nsome(bl, h))
143    case Con{+a0, +x1}:
144      match x1:
145        case Nil{}:
146          h => Empty.absurd({L.LcBlock64.to_octets(bl) == B.Octets.of_list(Con{a0, Nil{}}) : B.Octets}, b64.nsome(bl, h))
147        case Con{+a1, +x2}:
148          match x2:
149            case Nil{}:
150              h => Empty.absurd({L.LcBlock64.to_octets(bl) == B.Octets.of_list(Con{a0, Con{a1, Nil{}}}) : B.Octets}, b64.nsome(bl, h))
151            case Con{+a2, +x3}:
152              match x3:
153                case Nil{}:
154                  h => Empty.absurd({L.LcBlock64.to_octets(bl) == B.Octets.of_list(Con{a0, Con{a1, Con{a2, Nil{}}}}) : B.Octets}, b64.nsome(bl, h))
155                case Con{+a3, +x4}:
156                  match x4:
157                    case Nil{}:
158                      h => Empty.absurd({L.LcBlock64.to_octets(bl) == B.Octets.of_list(Con{a0, Con{a1, Con{a2, Con{a3, Nil{}}}}}) : B.Octets}, b64.nsome(bl, h))
159                    case Con{+a4, +x5}:
160                      match x5:
161                        case Nil{}:
162                          h => Empty.absurd({L.LcBlock64.to_octets(bl) == B.Octets.of_list(Con{a0, Con{a1, Con{a2, Con{a3, Con{a4, Nil{}}}}}}) : B.Octets}, b64.nsome(bl, h))
163                        case Con{+a5, +x6}:
164                          match x6:
165                            case Nil{}:
166                              h => Empty.absurd({L.LcBlock64.to_octets(bl) == B.Octets.of_list(Con{a0, Con{a1, Con{a2, Con{a3, Con{a4, Con{a5, Nil{}}}}}}}) : B.Octets}, b64.nsome(bl, h))
167                            case Con{+a6, +x7}:
168                              match x7:
169                                case Nil{}:
170                                  h => Empty.absurd({L.LcBlock64.to_octets(bl) == B.Octets.of_list(Con{a0, Con{a1, Con{a2, Con{a3, Con{a4, Con{a5, Con{a6, Nil{}}}}}}}}) : B.Octets}, b64.nsome(bl, h))
171                                case Con{+a7, +x8}:
172                                  match x8:
173                                    case Nil{}:
174                                      h => %Equal.cong(Maybe<&2, L.LcBlock64>, L.LcBlock64, mm => b64.mget(mm, bl), L.lc.block_of(Con{a0, Con{a1, Con{a2, Con{a3, Con{a4, Con{a5, Con{a6, Con{a7, Nil{}}}}}}}}}), Some{bl}, h) : {L.LcBlock64.to_octets(_) == B.Octets.of_list(Con{a0, Con{a1, Con{a2, Con{a3, Con{a4, Con{a5, Con{a6, Con{a7, Nil{}}}}}}}}}) : B.Octets}
175                                        b64.dbits(a0, a1, a2, a3, a4, a5, a6, a7)
176                                    case Con{+a8, +x9}:
177                                      h => Empty.absurd({L.LcBlock64.to_octets(bl) == B.Octets.of_list(Con{a0, Con{a1, Con{a2, Con{a3, Con{a4, Con{a5, Con{a6, Con{a7, Con{a8, x9}}}}}}}}}) : B.Octets}, b64.nsome(bl, h))
178
179
180def b64.dual(+o: B.Octets, +bl: L.LcBlock64, em: {L.LcBlock64.of_octets(o) == Some{bl} : Maybe<&2, L.LcBlock64>}) -> {L.LcBlock64.to_octets(bl) == o : B.Octets}:
181  Equal.trans(B.Octets, L.LcBlock64.to_octets(bl), B.Octets.of_list(B.Octets.to_list(o)), o, b64.dualL(B.Octets.to_list(o), bl)(em), BL.octets_of_to(o))
182
183def Laws.block64_octets_dual(o, b, e):
184  b64.dual(o, b, e)
185# the bytes of the blocks bs in front of ys, structurally
186def m64_joins(bs: List<&2, L.LcBlock64>, ys: List<&2, U32>) -> List<&2, U32>:
187  match bs:
188    case Nil{}:
189      ys
190    case Con{b, t}:
191      L.lc.block_bytes(b, m64_joins(t, ys))
192
193def m64_join_rev(bs: List<&2, L.LcBlock64>, +zs: List<&2, L.LcBlock64>, +ys: List<&2, U32>) -> {X.m64.join(zs, m64_joins(bs, ys)) == X.m64.join(X.m64.rev_onto(bs, zs), ys) : List<&2, U32>}:
194  match bs:
195    case Nil{}:
196      {==}
197    case Con{b, t}:
198      m64_join_rev(t, Con{b, zs}, ys)
199
200def m64_split_joins(bs: List<&2, L.LcBlock64>, +acc: List<&2, L.LcBlock64>) -> {X.m64.split(B.mask(m64_joins(bs, Nil{})), acc) == Some{X.m64.rev_onto(acc, bs)} : Maybe<&2, List<&2, L.LcBlock64>>}:
201  match bs:
202    case Nil{}:
203      {==}
204    case Con{L.LcBlock64{+hi, +lo}, +t}:
205      %blk8(hi, lo) : {X.m64.split(B.mask(m64_joins(t, Nil{})), Con{_, acc}) == Some{X.m64.rev_onto(acc, Con{L.LcBlock64{hi, lo}, t})} : Maybe<&2, List<&2, L.LcBlock64>>}
206      m64_split_joins(t, Con{L.LcBlock64{hi, lo}, acc})
207
208def Laws.blocks64_octets_round_trip(bs):
209  %Equal.sym(List<&2, U32>, B.Octets.to_list(B.Octets.of_list(X.m64.join(X.m64.rev_onto(bs, Nil{}), Nil{}))), B.mask(X.m64.join(X.m64.rev_onto(bs, Nil{}), Nil{})), BL.octets_to_of(X.m64.join(X.m64.rev_onto(bs, Nil{}), Nil{}))) : {X.m64.blocks(B.Octets.len(X.Lc64.octets_of(bs)), X.m64.split(_, Nil{})) == Done{bs} : Result<&2, &2, L.LcError, List<&2, L.LcBlock64>>}
210  %m64_join_rev(bs, Nil{}, Nil{}) : {X.m64.blocks(B.Octets.len(X.Lc64.octets_of(bs)), X.m64.split(B.mask(_), Nil{})) == Done{bs} : Result<&2, &2, L.LcError, List<&2, L.LcBlock64>>}
211  %Equal.sym(Maybe<&2, List<&2, L.LcBlock64>>, X.m64.split(B.mask(m64_joins(bs, Nil{})), Nil{}), Some{X.m64.rev_onto(Nil{}, bs)}, m64_split_joins(bs, Nil{})) : {X.m64.blocks(B.Octets.len(X.Lc64.octets_of(bs)), _) == Done{bs} : Result<&2, &2, L.LcError, List<&2, L.LcBlock64>>}
212  {==}
213
214# The modes: the tail-recursive loops are the structural forms; then XOR and
215# decryption undo each block, for any cipher whose decryption undoes its
216# encryption (for DES and 3DES, by their laws)
217
218def bool_xx2(a: Bool, b: Bool) -> {b == Bool.xor(a, Bool.xor(a, b)) : Bool}:
219  match a b:
220    case True{} True{}:
221      {==}
222    case True{} False{}:
223      {==}
224    case False{} True{}:
225      {==}
226    case False{} False{}:
227      {==}
228
229def word_xx2(n: Nat, a: Word(n), b: Word(n)) -> {b == Word.xor(n, a, Word.xor(n, a, b)) : Word(n)}:
230  match n:
231    case 0n:
232      match a b:
233        case WNil{} WNil{}:
234          {==}
235    case 1n+p:
236      match a b:
237        case WCon{ah, at} WCon{bh, bt}:
238          %bool_xx2(ah, bh) : {WCon{bh, bt} == WCon{_, Word.xor(p, at, Word.xor(p, at, bt))} : Word(1n+p)}
239          %word_xx2(p, at, bt) : {WCon{bh, bt} == WCon{bh, _} : Word(1n+p)}
240          {==}
241
242def u32_xx2(a: U32, b: U32) -> {b == U32.xor(a, U32.xor(a, b)) : U32}:
243  match a b:
244    case U32{x} U32{y}:
245      %word_xx2(32n, x, y) : {U32{y} == U32{_} : U32}
246      {==}
247
248def b64_xx2(a: L.LcBlock64, b: L.LcBlock64) -> {b == L.LcBlock64.xor(a, L.LcBlock64.xor(a, b)) : L.LcBlock64}:
249  match a b:
250    case L.LcBlock64{+a0, +a1} L.LcBlock64{+b0, +b1}:
251      %u32_xx2(a0, b0) : {L.LcBlock64{b0, b1} == L.LcBlock64{_, U32.xor(a1, U32.xor(a1, b1))} : L.LcBlock64}
252      %u32_xx2(a1, b1) : {L.LcBlock64{b0, b1} == L.LcBlock64{b0, _} : L.LcBlock64}
253      {==}
254
255def ecb_ref(~K: Data, ~f: K -> L.LcBlock64 -> L.LcBlock64, +k: K, bs: List<&2, L.LcBlock64>, +acc: List<&2, L.LcBlock64>) -> {X.m64.ecb.go(~K, ~f, k, bs, acc) == X.m64.rev_onto(acc, X.m64.ecb(~K, ~f, k, bs)) : List<&2, L.LcBlock64>}:
256  match bs:
257    case Nil{}:
258      {==}
259    case Con{b, t}:
260      ecb_ref(~K, ~f, k, t, Con{f(k, b), acc})
261
262def cbc_enc_ref(~K: Data, ~enc: K -> L.LcBlock64 -> L.LcBlock64, +k: K, bs: List<&2, L.LcBlock64>, +iv: L.LcBlock64, +acc: List<&2, L.LcBlock64>) -> {X.m64.cbc.enc.go(~K, ~enc, k, bs, iv, acc) == X.m64.rev_onto(acc, X.m64.cbc.enc(~K, ~enc, k, bs, iv)) : List<&2, L.LcBlock64>}:
263  match bs:
264    case Nil{}:
265      {==}
266    case Con{+p, t}:
267      cbc_enc_ref(~K, ~enc, k, t, enc(k, L.LcBlock64.xor(iv, p)), Con{enc(k, L.LcBlock64.xor(iv, p)), acc})
268
269def cbc_dec_ref(~K: Data, ~dec: K -> L.LcBlock64 -> L.LcBlock64, +k: K, bs: List<&2, L.LcBlock64>, +iv: L.LcBlock64, +acc: List<&2, L.LcBlock64>) -> {X.m64.cbc.dec.go(~K, ~dec, k, bs, iv, acc) == X.m64.rev_onto(acc, X.m64.cbc.dec(~K, ~dec, k, bs, iv)) : List<&2, L.LcBlock64>}:
270  match bs:
271    case Nil{}:
272      {==}
273    case Con{+c, t}:
274      cbc_dec_ref(~K, ~dec, k, t, c, Con{L.LcBlock64.xor(iv, dec(k, c)), acc})
275
276# The byte layers, on the bytes of whole blocks under the bytes of an IV
277
278def cbc_enc_ok(~K: Data, ~enc: K -> L.LcBlock64 -> L.LcBlock64, +k: K, +iv: L.LcBlock64, +bs: List<&2, L.LcBlock64>) -> {X.Lc64.cbc_encrypt(~K, ~enc, k, L.LcBlock64.to_octets(iv), X.Lc64.octets_of(bs)) == Done{X.Lc64.octets_of(X.Lc64.cbc_encrypt_blocks(~K, ~enc, k, iv, bs))} : Result<&2, &2, L.LcError, B.Octets>}:
279  %Equal.sym(Maybe<&2, L.LcBlock64>, L.LcBlock64.of_octets(L.LcBlock64.to_octets(iv)), Some{iv}, Laws.block64_octets_round_trip(iv)) : {X.m64.cbc.e1(~K, ~enc, k, X.m64.iv(_, B.Octets.len(L.LcBlock64.to_octets(iv))), X.Lc64.octets_of(bs)) == Done{X.Lc64.octets_of(X.Lc64.cbc_encrypt_blocks(~K, ~enc, k, iv, bs))} : Result<&2, &2, L.LcError, B.Octets>}
280  %Equal.sym(Result<&2, &2, L.LcError, List<&2, L.LcBlock64>>, X.Lc64.blocks_of(X.Lc64.octets_of(bs)), Done{bs}, Laws.blocks64_octets_round_trip(bs)) : {X.m64.cbc.e2(~K, ~enc, k, iv, _) == Done{X.Lc64.octets_of(X.Lc64.cbc_encrypt_blocks(~K, ~enc, k, iv, bs))} : Result<&2, &2, L.LcError, B.Octets>}
281  {==}
282
283def cbc_dec_ok(~K: Data, ~dec: K -> L.LcBlock64 -> L.LcBlock64, +k: K, +iv: L.LcBlock64, +bs: List<&2, L.LcBlock64>) -> {X.Lc64.cbc_decrypt(~K, ~dec, k, L.LcBlock64.to_octets(iv), X.Lc64.octets_of(bs)) == Done{X.Lc64.octets_of(X.Lc64.cbc_decrypt_blocks(~K, ~dec, k, iv, bs))} : Result<&2, &2, L.LcError, B.Octets>}:
284  %Equal.sym(Maybe<&2, L.LcBlock64>, L.LcBlock64.of_octets(L.LcBlock64.to_octets(iv)), Some{iv}, Laws.block64_octets_round_trip(iv)) : {X.m64.cbc.d1(~K, ~dec, k, X.m64.iv(_, B.Octets.len(L.LcBlock64.to_octets(iv))), X.Lc64.octets_of(bs)) == Done{X.Lc64.octets_of(X.Lc64.cbc_decrypt_blocks(~K, ~dec, k, iv, bs))} : Result<&2, &2, L.LcError, B.Octets>}
285  %Equal.sym(Result<&2, &2, L.LcError, List<&2, L.LcBlock64>>, X.Lc64.blocks_of(X.Lc64.octets_of(bs)), Done{bs}, Laws.blocks64_octets_round_trip(bs)) : {X.m64.cbc.d2(~K, ~dec, k, iv, _) == Done{X.Lc64.octets_of(X.Lc64.cbc_decrypt_blocks(~K, ~dec, k, iv, bs))} : Result<&2, &2, L.LcError, B.Octets>}
286  {==}
287
288def ecb_enc_ok(~K: Data, ~f: K -> L.LcBlock64 -> L.LcBlock64, +k: K, +bs: List<&2, L.LcBlock64>) -> {Result.map(&2, &2, L.LcError, List<&2, L.LcBlock64>, B.Octets, xs => X.Lc64.octets_of(X.Lc64.ecb_encrypt_blocks(~K, ~f, k, xs)), X.Lc64.blocks_of(X.Lc64.octets_of(bs))) == Done{X.Lc64.octets_of(X.Lc64.ecb_encrypt_blocks(~K, ~f, k, bs))} : Result<&2, &2, L.LcError, B.Octets>}:
289  %Equal.sym(Result<&2, &2, L.LcError, List<&2, L.LcBlock64>>, X.Lc64.blocks_of(X.Lc64.octets_of(bs)), Done{bs}, Laws.blocks64_octets_round_trip(bs)) : {Result.map(&2, &2, L.LcError, List<&2, L.LcBlock64>, B.Octets, xs => X.Lc64.octets_of(X.Lc64.ecb_encrypt_blocks(~K, ~f, k, xs)), _) == Done{X.Lc64.octets_of(X.Lc64.ecb_encrypt_blocks(~K, ~f, k, bs))} : Result<&2, &2, L.LcError, B.Octets>}
290  {==}
291
292def ecb_dec_ok(~K: Data, ~f: K -> L.LcBlock64 -> L.LcBlock64, +k: K, +bs: List<&2, L.LcBlock64>) -> {Result.map(&2, &2, L.LcError, List<&2, L.LcBlock64>, B.Octets, xs => X.Lc64.octets_of(X.Lc64.ecb_decrypt_blocks(~K, ~f, k, xs)), X.Lc64.blocks_of(X.Lc64.octets_of(bs))) == Done{X.Lc64.octets_of(X.Lc64.ecb_decrypt_blocks(~K, ~f, k, bs))} : Result<&2, &2, L.LcError, B.Octets>}:
293  %Equal.sym(Result<&2, &2, L.LcError, List<&2, L.LcBlock64>>, X.Lc64.blocks_of(X.Lc64.octets_of(bs)), Done{bs}, Laws.blocks64_octets_round_trip(bs)) : {Result.map(&2, &2, L.LcError, List<&2, L.LcBlock64>, B.Octets, xs => X.Lc64.octets_of(X.Lc64.ecb_decrypt_blocks(~K, ~f, k, xs)), _) == Done{X.Lc64.octets_of(X.Lc64.ecb_decrypt_blocks(~K, ~f, k, bs))} : Result<&2, &2, L.LcError, B.Octets>}
294  {==}
295
296# The shared lemmas as laws
297
298def Laws.word_xor_cancel(n, a, b):
299  word_xx(n, a, b)
300
301def Laws.u32_xor_cancel(a, b):
302  u32_xx(a, b)
303
304def Laws.block64_xor_cancel(a, b):
305  b64_xx2(a, b)
306
307def Laws.rotl1_rotl31(x):
308  rot_1_31(x)
309
310def Laws.rotl31_rotl1(x):
311  rot_31_1(x)
312
313def Laws.bswap_bswap(x):
314  bswap2(x)
315
316def Laws.feistel_unrun_run(RK, f, ks, b):
317  fe_unrun_run(~RK, ~f, ks, b)
318
319def Laws.feistel_run_unrun(RK, f, ks, b):
320  fe_run_unrun(~RK, ~f, ks, b)
321
322# the modes: the loops that run are the structural forms (ecb_ref,
323# cbc_enc_ref, cbc_dec_ref); the byte layers are the block layers (the *_ok
324# lemmas above)
325
326def Laws.modes64_ecb_blocks(K, enc, dec, k, bs):
327  %Equal.sym(List<&2, L.LcBlock64>, X.m64.ecb.go(~K, ~enc, k, bs, Nil{}), X.m64.rev_onto(Nil{}, X.m64.ecb(~K, ~enc, k, bs)), ecb_ref(~K, ~enc, k, bs, Nil{})) : {X.m64.ecb(~K, ~dec, k, X.m64.ecb(~K, ~enc, k, bs)) == X.m64.ecb.go(~K, ~dec, k, _, Nil{}) : List<&2, L.LcBlock64>}
328  %Equal.sym(List<&2, L.LcBlock64>, X.m64.ecb.go(~K, ~dec, k, X.m64.ecb(~K, ~enc, k, bs), Nil{}), X.m64.rev_onto(Nil{}, X.m64.ecb(~K, ~dec, k, X.m64.ecb(~K, ~enc, k, bs))), ecb_ref(~K, ~dec, k, X.m64.ecb(~K, ~enc, k, bs), Nil{})) : {X.m64.ecb(~K, ~dec, k, X.m64.ecb(~K, ~enc, k, bs)) == _ : List<&2, L.LcBlock64>}
329  {==}
330
331def Laws.modes64_cbc_blocks(K, enc, dec, k, iv, bs):
332  %Equal.sym(List<&2, L.LcBlock64>, X.m64.cbc.enc.go(~K, ~enc, k, bs, iv, Nil{}), X.m64.rev_onto(Nil{}, X.m64.cbc.enc(~K, ~enc, k, bs, iv)), cbc_enc_ref(~K, ~enc, k, bs, iv, Nil{})) : {X.m64.cbc.dec(~K, ~dec, k, X.m64.cbc.enc(~K, ~enc, k, bs, iv), iv) == X.m64.cbc.dec.go(~K, ~dec, k, _, iv, Nil{}) : List<&2, L.LcBlock64>}
333  %Equal.sym(List<&2, L.LcBlock64>, X.m64.cbc.dec.go(~K, ~dec, k, X.m64.cbc.enc(~K, ~enc, k, bs, iv), iv, Nil{}), X.m64.rev_onto(Nil{}, X.m64.cbc.dec(~K, ~dec, k, X.m64.cbc.enc(~K, ~enc, k, bs, iv), iv)), cbc_dec_ref(~K, ~dec, k, X.m64.cbc.enc(~K, ~enc, k, bs, iv), iv, Nil{})) : {X.m64.cbc.dec(~K, ~dec, k, X.m64.cbc.enc(~K, ~enc, k, bs, iv), iv) == _ : List<&2, L.LcBlock64>}
334  {==}
335
336def Laws.modes64_ecb_octets(K, enc, dec, k, bs):
337  %Equal.sym(Result<&2, &2, L.LcError, B.Octets>, Result.map(&2, &2, L.LcError, List<&2, L.LcBlock64>, B.Octets, xs => X.Lc64.octets_of(X.Lc64.ecb_encrypt_blocks(~K, ~enc, k, xs)), X.Lc64.blocks_of(X.Lc64.octets_of(bs))), Done{X.Lc64.octets_of(X.Lc64.ecb_encrypt_blocks(~K, ~enc, k, bs))}, ecb_enc_ok(~K, ~enc, k, bs)) : {Done{X.Lc64.octets_of(X.Lc64.ecb_decrypt_blocks(~K, ~dec, k, X.Lc64.ecb_encrypt_blocks(~K, ~enc, k, bs)))} == Result.bind(&2, &2, L.LcError, B.Octets, B.Octets, _, c => X.Lc64.ecb_decrypt(~K, ~dec, k, c)) : Result<&2, &2, L.LcError, B.Octets>}
338  %Equal.sym(Result<&2, &2, L.LcError, B.Octets>, Result.map(&2, &2, L.LcError, List<&2, L.LcBlock64>, B.Octets, xs => X.Lc64.octets_of(X.Lc64.ecb_decrypt_blocks(~K, ~dec, k, xs)), X.Lc64.blocks_of(X.Lc64.octets_of(X.Lc64.ecb_encrypt_blocks(~K, ~enc, k, bs)))), Done{X.Lc64.octets_of(X.Lc64.ecb_decrypt_blocks(~K, ~dec, k, X.Lc64.ecb_encrypt_blocks(~K, ~enc, k, bs)))}, ecb_dec_ok(~K, ~dec, k, X.Lc64.ecb_encrypt_blocks(~K, ~enc, k, bs))) : {Done{X.Lc64.octets_of(X.Lc64.ecb_decrypt_blocks(~K, ~dec, k, X.Lc64.ecb_encrypt_blocks(~K, ~enc, k, bs)))} == _ : Result<&2, &2, L.LcError, B.Octets>}
339  {==}
340
341def Laws.modes64_cbc_octets(K, enc, dec, k, iv, bs):
342  %Equal.sym(Result<&2, &2, L.LcError, B.Octets>, X.Lc64.cbc_encrypt(~K, ~enc, k, L.LcBlock64.to_octets(iv), X.Lc64.octets_of(bs)), Done{X.Lc64.octets_of(X.Lc64.cbc_encrypt_blocks(~K, ~enc, k, iv, bs))}, cbc_enc_ok(~K, ~enc, k, iv, bs)) : {Done{X.Lc64.octets_of(X.Lc64.cbc_decrypt_blocks(~K, ~dec, k, iv, X.Lc64.cbc_encrypt_blocks(~K, ~enc, k, iv, bs)))} == Result.bind(&2, &2, L.LcError, B.Octets, B.Octets, _, c => X.Lc64.cbc_decrypt(~K, ~dec, k, L.LcBlock64.to_octets(iv), c)) : Result<&2, &2, L.LcError, B.Octets>}
343  %Equal.sym(Result<&2, &2, L.LcError, B.Octets>, X.Lc64.cbc_decrypt(~K, ~dec, k, L.LcBlock64.to_octets(iv), X.Lc64.octets_of(X.Lc64.cbc_encrypt_blocks(~K, ~enc, k, iv, bs))), Done{X.Lc64.octets_of(X.Lc64.cbc_decrypt_blocks(~K, ~dec, k, iv, X.Lc64.cbc_encrypt_blocks(~K, ~enc, k, iv, bs)))}, cbc_dec_ok(~K, ~dec, k, iv, X.Lc64.cbc_encrypt_blocks(~K, ~enc, k, iv, bs))) : {Done{X.Lc64.octets_of(X.Lc64.cbc_decrypt_blocks(~K, ~dec, k, iv, X.Lc64.cbc_encrypt_blocks(~K, ~enc, k, iv, bs)))} == _ : Result<&2, &2, L.LcError, B.Octets>}
344  {==}
345
346# the 64-bit modes refuse a message that is not whole blocks (by computation)
347
348def Laws.modes64_not_whole_blocks():
349  {==}