PROOF.bend

bend-osdev-cbc@0.1.0.0 · 349 lines · 38 definitions

1# Proofs of LAWS.bend (CBC). The byte layer's lemmas the modes share
2# (splitting bytes into blocks and joining them back, masks, the tail-call
3# forms) are mode-core's laws, used under the names below.
4import Base
5import bend-osdev-bytes@0.1.1.0/bytes.bend as B
6import bend-osdev-bytes@0.1.1.0/LAWS.bend as BL
7import bend-osdev-bytes@0.1.1.0/PROOF.bend as BP
8import bend-osdev-mode-core@0.1.0.0/mode_core.bend as M
9import bend-osdev-cbc@0.1.0.0/cbc.bend as C
10import bend-osdev-mode-core@0.1.0.0/LAWS.bend as CoreL
11import bend-osdev-mode-core@0.1.0.0/PROOF.bend as CoreP
12import bend-osdev-cbc@0.1.0.0/LAWS.bend as Laws
13
14# mode-core's laws, under the names these proofs use
15
16def sp.cons_tail(b: M.CmBlock, s: M.CmSplit) -> {M.cm.split.tail(M.cm.split.cons(b, s)) == M.cm.split.tail(s) : List<&2, U32>}:
17  CoreL.split_cons_tail(b, s)
18
19def sp.eta(s: M.CmSplit) -> {M.CmSplit{M.cm.split.blocks(s), M.cm.split.tail(s)} == s : M.CmSplit}:
20  CoreL.split_eta(s)
21
22def sp.blk(b: M.CmBlock, rest: List<&2, U32>) -> {M.cm.split(M.cm.bytes_onto(b, rest)) == M.cm.split.cons(b, M.cm.split(rest)) : M.CmSplit}:
23  CoreL.split_bytes_onto(b, rest)
24
25def sp.mask_blk(b: M.CmBlock, rest: List<&2, U32>) -> {B.mask(M.cm.bytes_onto(b, rest)) == M.cm.bytes_onto(b, B.mask(rest)) : List<&2, U32>}:
26  CoreL.mask_bytes_onto(b, rest)
27
28def sp.join_split(ys: List<&2, U32>) -> {M.cm.join_onto(M.cm.split.blocks(M.cm.split(B.mask(ys))), M.cm.split.tail(M.cm.split(B.mask(ys)))) == B.mask(ys) : List<&2, U32>}:
29  CoreL.join_split(ys)
30
31def oc.masked(+o: B.Octets) -> {B.mask(B.Octets.to_list(o)) == B.Octets.to_list(o) : List<&2, U32>}:
32  CoreL.octets_masked(o)
33
34def oc.len(+o: B.Octets, +n: Nat, h: {B.Octets.len(o) == n : Nat}) -> {B.len(B.Octets.to_list(o)) == n : Nat}:
35  CoreL.octets_len(o, n, h)
36
37def tr.split_eq(+xs: List<&2, U32>) -> {M.cm.split(xs) == M.cm.split.fast(xs) : M.CmSplit}:
38  CoreL.split_fast(xs)
39
40def tr.join_eq(+bs: List<&2, M.CmBlock>, +rest: List<&2, U32>) -> {M.cm.join_onto(bs, rest) == M.cm.join_onto.fast(bs, rest) : List<&2, U32>}:
41  CoreL.join_onto_fast(bs, rest)
42
43def tr.bind_cong(r: Result<&2, &2, M.CmError, B.Octets>, f: B.Octets -> Result<&2, &2, M.CmError, B.Octets>, g: B.Octets -> Result<&2, &2, M.CmError, B.Octets>, h: @c: B.Octets -> {f(c) == g(c) : Result<&2, &2, M.CmError, B.Octets>}) -> {Result.bind(&2, &2, M.CmError, B.Octets, B.Octets, r, f) == Result.bind(&2, &2, M.CmError, B.Octets, B.Octets, r, g) : Result<&2, &2, M.CmError, B.Octets>}:
44  CoreL.bind_cong(r, f, g, h)
45
46def cmp.hd(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, +x: M.CmBlock, +xs: List<&2, M.CmBlock>, +h: {M.CmBlock.dec_enc(~K, ~enc, ~dec, k, Con{x, xs}) == Con{x, xs} : List<&2, M.CmBlock>}) -> {dec(k, enc(k, x)) == x : M.CmBlock}:
47  CoreL.dec_enc_head(~K, ~enc, ~dec, k, x, xs, h)
48
49def cmp.tl(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, +x: M.CmBlock, +xs: List<&2, M.CmBlock>, +h: {M.CmBlock.dec_enc(~K, ~enc, ~dec, k, Con{x, xs}) == Con{x, xs} : List<&2, M.CmBlock>}) -> {M.CmBlock.dec_enc(~K, ~enc, ~dec, k, xs) == xs : List<&2, M.CmBlock>}:
50  CoreL.dec_enc_tail(~K, ~enc, ~dec, k, x, xs, h)
51
52# XOR
53
54def bx.bool(a: Bool, b: Bool) -> {Bool.xor(a, Bool.xor(a, b)) == b : Bool}:
55  match a b:
56    case False{} False{}:
57      {==}
58    case False{} True{}:
59      {==}
60    case True{} False{}:
61      {==}
62    case True{} True{}:
63      {==}
64
65def bx.word(n: Nat, a: Word(n), b: Word(n)) -> {Word.xor(n, a, Word.xor(n, a, b)) == b : Word(n)}:
66  match n:
67    case 0n:
68      match b:
69        case WNil{}:
70          {==}
71    case 1n+p:
72      match a b:
73        case WCon{ah, at} WCon{bh, bt}:
74          %bx.bool(ah, bh) : {WCon{Bool.xor(ah, Bool.xor(ah, bh)), Word.xor(p, at, Word.xor(p, at, bt))} == WCon{_, bt} : Word(1n+p)}
75          %bx.word(p, at, bt) : {WCon{Bool.xor(ah, Bool.xor(ah, bh)), Word.xor(p, at, Word.xor(p, at, bt))} == WCon{Bool.xor(ah, Bool.xor(ah, bh)), _} : Word(1n+p)}
76          {==}
77
78def bx.u32(a: U32, b: U32) -> {U32.xor(a, U32.xor(a, b)) == b : U32}:
79  match a b:
80    case U32{x} U32{y}:
81      %bx.word(32n, x, y) : {U32{Word.xor(32n, x, Word.xor(32n, x, y))} == U32{_} : U32}
82      {==}
83
84# xor(a, xor(a, b)) == b on blocks
85def bx.block(+a: M.CmBlock, +b: M.CmBlock) -> {M.CmBlock.xor(a, M.CmBlock.xor(a, b)) == b : M.CmBlock}:
86  match a b:
87    case M.CmBlock{a0, a1, a2, a3} M.CmBlock{b0, b1, b2, b3}:
88      %bx.u32(a0, b0) : {M.CmBlock.xor(M.CmBlock{a0, a1, a2, a3}, M.CmBlock.xor(M.CmBlock{a0, a1, a2, a3}, M.CmBlock{b0, b1, b2, b3})) == M.CmBlock{_, b1, b2, b3} : M.CmBlock}
89      %bx.u32(a1, b1) : {M.CmBlock.xor(M.CmBlock{a0, a1, a2, a3}, M.CmBlock.xor(M.CmBlock{a0, a1, a2, a3}, M.CmBlock{b0, b1, b2, b3})) == M.CmBlock{U32.xor(a0, U32.xor(a0, b0)), _, b2, b3} : M.CmBlock}
90      %bx.u32(a2, b2) : {M.CmBlock.xor(M.CmBlock{a0, a1, a2, a3}, M.CmBlock.xor(M.CmBlock{a0, a1, a2, a3}, M.CmBlock{b0, b1, b2, b3})) == M.CmBlock{U32.xor(a0, U32.xor(a0, b0)), U32.xor(a1, U32.xor(a1, b1)), _, b3} : M.CmBlock}
91      %bx.u32(a3, b3) : {M.CmBlock.xor(M.CmBlock{a0, a1, a2, a3}, M.CmBlock.xor(M.CmBlock{a0, a1, a2, a3}, M.CmBlock{b0, b1, b2, b3})) == M.CmBlock{U32.xor(a0, U32.xor(a0, b0)), U32.xor(a1, U32.xor(a1, b1)), U32.xor(a2, U32.xor(a2, b2)), _} : M.CmBlock}
92      {==}
93
94# Arithmetic: n + 16 and n leave the same remainder mod 16
95
96def sp.disc(n: Nat) -> Type:
97  match n:
98    case 0n:
99      Empty
100    case 1n+p:
101      Unit
102
103def sp.absurd(p: Nat, h: {1n+p == 0n : Nat}) -> Empty:
104  %h : sp.disc(_)
105  Unit{}
106
107def sp.absurd_tail(p: Nat, xs: List<&2, U32>, h: {1n+p == 0n : Nat}) -> {M.cm.split.tail(M.cm.split(B.mask(xs))) == Nil{} : List<&2, U32>}:
108  Empty.absurd({M.cm.split.tail(M.cm.split(B.mask(xs))) == Nil{} : List<&2, U32>}, sp.absurd(p, h))
109
110def sp.snd_go(n: Nat, m: Nat, d1: Nat, d2: Nat, r: Nat) -> {Pair.snd(Nat, Nat, Nat.divmod.go(n, m, d1, r)) == Pair.snd(Nat, Nat, Nat.divmod.go(n, m, d2, r)) : Nat}:
111  match n:
112    case 0n:
113      {==}
114    case 1n+np:
115      match m:
116        case 0n:
117          sp.snd_go(np, r, 1n+d1, 1n+d2, 0n)
118        case 1n+mp:
119          sp.snd_go(np, mp, d1, d2, 1n+r)
120
121def sp.mod16(n: Nat) -> {Nat.mod(Nat.add(16n, n), 16n) == Nat.mod(n, 16n) : Nat}:
122  sp.snd_go(n, 15n, 1n, 0n, 0n)
123
124# a list of whole blocks splits with no tail
125def sp.mod_tail(ys: List<&2, U32>) -> {Nat.mod(B.len(ys), 16n) == 0n : Nat} -> {M.cm.split.tail(M.cm.split(B.mask(ys))) == Nil{} : List<&2, U32>}:
126  match ys:
127    case Nil{}:
128      h => {==}
129    case Con{+y0, +r0}:
130      match r0:
131        case Nil{}:
132          h => sp.absurd_tail(0n, Con{y0, Nil{}}, h)
133        case Con{+y1, +r1}:
134          match r1:
135            case Nil{}:
136              h => sp.absurd_tail(1n, Con{y0, Con{y1, Nil{}}}, h)
137            case Con{+y2, +r2}:
138              match r2:
139                case Nil{}:
140                  h => sp.absurd_tail(2n, Con{y0, Con{y1, Con{y2, Nil{}}}}, h)
141                case Con{+y3, +r3}:
142                  match r3:
143                    case Nil{}:
144                      h => sp.absurd_tail(3n, Con{y0, Con{y1, Con{y2, Con{y3, Nil{}}}}}, h)
145                    case Con{+y4, +r4}:
146                      match r4:
147                        case Nil{}:
148                          h => sp.absurd_tail(4n, Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Nil{}}}}}}, h)
149                        case Con{+y5, +r5}:
150                          match r5:
151                            case Nil{}:
152                              h => sp.absurd_tail(5n, Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Nil{}}}}}}}, h)
153                            case Con{+y6, +r6}:
154                              match r6:
155                                case Nil{}:
156                                  h => sp.absurd_tail(6n, Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Nil{}}}}}}}}, h)
157                                case Con{+y7, +r7}:
158                                  match r7:
159                                    case Nil{}:
160                                      h => sp.absurd_tail(7n, Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Nil{}}}}}}}}}, h)
161                                    case Con{+y8, +r8}:
162                                      match r8:
163                                        case Nil{}:
164                                          h => sp.absurd_tail(8n, Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Nil{}}}}}}}}}}, h)
165                                        case Con{+y9, +r9}:
166                                          match r9:
167                                            case Nil{}:
168                                              h => sp.absurd_tail(9n, Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Con{y9, Nil{}}}}}}}}}}}, h)
169                                            case Con{+y10, +r10}:
170                                              match r10:
171                                                case Nil{}:
172                                                  h => sp.absurd_tail(10n, Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Con{y9, Con{y10, Nil{}}}}}}}}}}}}, h)
173                                                case Con{+y11, +r11}:
174                                                  match r11:
175                                                    case Nil{}:
176                                                      h => sp.absurd_tail(11n, Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Con{y9, Con{y10, Con{y11, Nil{}}}}}}}}}}}}}, h)
177                                                    case Con{+y12, +r12}:
178                                                      match r12:
179                                                        case Nil{}:
180                                                          h => sp.absurd_tail(12n, Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Con{y9, Con{y10, Con{y11, Con{y12, Nil{}}}}}}}}}}}}}}, h)
181                                                        case Con{+y13, +r13}:
182                                                          match r13:
183                                                            case Nil{}:
184                                                              h => sp.absurd_tail(13n, Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Con{y9, Con{y10, Con{y11, Con{y12, Con{y13, Nil{}}}}}}}}}}}}}}}, h)
185                                                            case Con{+y14, +r14}:
186                                                              match r14:
187                                                                case Nil{}:
188                                                                  h => sp.absurd_tail(14n, Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Con{y9, Con{y10, Con{y11, Con{y12, Con{y13, Con{y14, Nil{}}}}}}}}}}}}}}}}, h)
189                                                                case Con{+y15, +t}:
190                                                                  h => %Equal.sym(List<&2, U32>, M.cm.split.tail(M.cm.split.cons(M.cm.block16(B.byte(y0), B.byte(y1), B.byte(y2), B.byte(y3), B.byte(y4), B.byte(y5), B.byte(y6), B.byte(y7), B.byte(y8), B.byte(y9), B.byte(y10), B.byte(y11), B.byte(y12), B.byte(y13), B.byte(y14), B.byte(y15)), M.cm.split(B.mask(t)))), M.cm.split.tail(M.cm.split(B.mask(t))), sp.cons_tail(M.cm.block16(B.byte(y0), B.byte(y1), B.byte(y2), B.byte(y3), B.byte(y4), B.byte(y5), B.byte(y6), B.byte(y7), B.byte(y8), B.byte(y9), B.byte(y10), B.byte(y11), B.byte(y12), B.byte(y13), B.byte(y14), B.byte(y15)), M.cm.split(B.mask(t)))) : {_ == Nil{} : List<&2, U32>}
191                                                                    sp.mod_tail(t)(Equal.trans(Nat, Nat.mod(B.len(t), 16n), Nat.mod(Nat.add(16n, B.len(t)), 16n), 0n, Equal.sym(Nat, Nat.mod(Nat.add(16n, B.len(t)), 16n), Nat.mod(B.len(t), 16n), sp.mod16(B.len(t))), h))
192
193# Joining and splitting
194
195def sp.split_join(bs: List<&2, M.CmBlock>) -> {M.cm.split(M.cm.join_onto(bs, Nil{})) == M.CmSplit{bs, Nil{}} : M.CmSplit}:
196  match bs:
197    case Nil{}:
198      {==}
199    case Con{+b, +t}:
200      %Equal.sym(M.CmSplit, M.cm.split(M.cm.bytes_onto(b, M.cm.join_onto(t, Nil{}))), M.cm.split.cons(b, M.cm.split(M.cm.join_onto(t, Nil{}))), sp.blk(b, M.cm.join_onto(t, Nil{}))) : {_ == M.CmSplit{Con{b, t}, Nil{}} : M.CmSplit}
201      %Equal.sym(M.CmSplit, M.cm.split(M.cm.join_onto(t, Nil{})), M.CmSplit{t, Nil{}}, sp.split_join(t)) : {M.cm.split.cons(b, _) == M.CmSplit{Con{b, t}, Nil{}} : M.CmSplit}
202      {==}
203
204def sp.mask_join(bs: List<&2, M.CmBlock>) -> {B.mask(M.cm.join_onto(bs, Nil{})) == M.cm.join_onto(bs, Nil{}) : List<&2, U32>}:
205  match bs:
206    case Nil{}:
207      {==}
208    case Con{+b, +t}:
209      %Equal.sym(List<&2, U32>, B.mask(M.cm.bytes_onto(b, M.cm.join_onto(t, Nil{}))), M.cm.bytes_onto(b, B.mask(M.cm.join_onto(t, Nil{}))), sp.mask_blk(b, M.cm.join_onto(t, Nil{}))) : {_ == M.cm.bytes_onto(b, M.cm.join_onto(t, Nil{})) : List<&2, U32>}
210      %Equal.sym(List<&2, U32>, B.mask(M.cm.join_onto(t, Nil{})), M.cm.join_onto(t, Nil{}), sp.mask_join(t)) : {M.cm.bytes_onto(b, _) == M.cm.bytes_onto(b, M.cm.join_onto(t, Nil{})) : List<&2, U32>}
211      {==}
212
213def oc.mod(+o: B.Octets, h: {Nat.mod(B.Octets.len(o), 16n) == 0n : Nat}) -> {Nat.mod(B.len(B.Octets.to_list(o)), 16n) == 0n : Nat}:
214  Equal.trans(Nat, Nat.mod(B.len(B.Octets.to_list(o)), 16n), Nat.mod(B.Octets.len(o), 16n), 0n, Equal.sym(Nat, Nat.mod(B.Octets.len(o), 16n), Nat.mod(B.len(B.Octets.to_list(o)), 16n), Equal.cong(Nat, Nat, n => Nat.mod(n, 16n), B.Octets.len(o), B.len(B.Octets.to_list(o)), BL.octets_len_list(o))), h)
215
216# a 16-byte IV is the block of its bytes
217def cbcp.iv(+iv: B.Octets, h: {B.Octets.len(iv) == 16n : Nat}) -> {C.cbc.iv(iv) == Done{M.cm.block_of(B.Octets.to_list(iv))} : Result<&2, &2, M.CmError, M.CmBlock>}:
218  %Equal.sym(Nat, B.len(B.Octets.to_list(iv)), 16n, oc.len(iv, 16n, h)) : {M.cm.need_block.pick(Nat.is_eq(_, 16n), B.Octets.to_list(iv), M.CmBadIvLength{B.len(B.Octets.to_list(iv))}) == Done{M.cm.block_of(B.Octets.to_list(iv))} : Result<&2, &2, M.CmError, M.CmBlock>}
219  {==}
220
221# The modes on blocks
222
223def tr.cbc_enc_go(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, bs: List<&2, M.CmBlock>, +iv: M.CmBlock, +acc: List<&2, M.CmBlock>) -> {C.cbc.enc.go(~K, ~enc, k, bs, iv, acc) == M.cm.blocks.rev_onto(acc, C.cbc.enc(~K, ~enc, k, bs, iv)) : List<&2, M.CmBlock>}:
224  match bs:
225    case Nil{}:
226      {==}
227    case Con{+p, +t}:
228      tr.cbc_enc_go(~K, ~enc, k, t, enc(k, M.CmBlock.xor(iv, p)), Con{enc(k, M.CmBlock.xor(iv, p)), acc})
229
230def tr.cbc_enc_eq(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, +bs: List<&2, M.CmBlock>, +iv: M.CmBlock) -> {C.cbc.enc(~K, ~enc, k, bs, iv) == C.cbc.enc.fast(~K, ~enc, k, bs, iv) : List<&2, M.CmBlock>}:
231  Equal.sym(List<&2, M.CmBlock>, C.cbc.enc.fast(~K, ~enc, k, bs, iv), C.cbc.enc(~K, ~enc, k, bs, iv), tr.cbc_enc_go(~K, ~enc, k, bs, iv, Nil{}))
232
233def tr.cbc_dec_go(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, bs: List<&2, M.CmBlock>, +iv: M.CmBlock, +acc: List<&2, M.CmBlock>) -> {C.cbc.dec.go(~K, ~dec, k, bs, iv, acc) == M.cm.blocks.rev_onto(acc, C.cbc.dec(~K, ~dec, k, bs, iv)) : List<&2, M.CmBlock>}:
234  match bs:
235    case Nil{}:
236      {==}
237    case Con{+c, +t}:
238      tr.cbc_dec_go(~K, ~dec, k, t, c, Con{M.CmBlock.xor(iv, dec(k, c)), acc})
239
240def tr.cbc_dec_eq(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, +bs: List<&2, M.CmBlock>, +iv: M.CmBlock) -> {C.cbc.dec(~K, ~dec, k, bs, iv) == C.cbc.dec.fast(~K, ~dec, k, bs, iv) : List<&2, M.CmBlock>}:
241  Equal.sym(List<&2, M.CmBlock>, C.cbc.dec.fast(~K, ~dec, k, bs, iv), C.cbc.dec(~K, ~dec, k, bs, iv), tr.cbc_dec_go(~K, ~dec, k, bs, iv, Nil{}))
242
243# The byte layers
244
245def tr.cbc_e2(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, +v: M.CmBlock, s: M.CmSplit, +n: Nat) -> {C.cbc.e2(~K, ~enc, k, v, s, n) == C.cbc.e2.fast(~K, ~enc, k, v, s, n) : Result<&2, &2, M.CmError, B.Octets>}:
246  match s:
247    case M.CmSplit{+bs, tail}:
248      match tail:
249        case Nil{}:
250          %tr.cbc_enc_eq(~K, ~enc, k, bs, v) : {Done{B.Octets.of_list(M.cm.join_onto(C.cbc.enc(~K, ~enc, k, bs, v), Nil{}))} == Done{B.Octets.of_list(M.cm.join_onto.fast(_, Nil{}))} : Result<&2, &2, M.CmError, B.Octets>}
251          %tr.join_eq(C.cbc.enc(~K, ~enc, k, bs, v), Nil{}) : {Done{B.Octets.of_list(M.cm.join_onto(C.cbc.enc(~K, ~enc, k, bs, v), Nil{}))} == Done{B.Octets.of_list(_)} : Result<&2, &2, M.CmError, B.Octets>}
252          {==}
253        case Con{h, t}:
254          {==}
255
256def tr.cbc_e1(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, r: Result<&2, &2, M.CmError, M.CmBlock>, +xs: List<&2, U32>) -> {C.cbc.e1(~K, ~enc, k, r, xs) == C.cbc.e1.fast(~K, ~enc, k, r, xs) : Result<&2, &2, M.CmError, B.Octets>}:
257  match r:
258    case Fail{e}:
259      {==}
260    case Done{+v}:
261      %tr.split_eq(xs) : {C.cbc.e2(~K, ~enc, k, v, M.cm.split(xs), B.len(xs)) == C.cbc.e2.fast(~K, ~enc, k, v, _, B.len.fast(xs)) : Result<&2, &2, M.CmError, B.Octets>}
262      %BL.len_fast(xs) : {C.cbc.e2(~K, ~enc, k, v, M.cm.split(xs), B.len(xs)) == C.cbc.e2.fast(~K, ~enc, k, v, M.cm.split(xs), _) : Result<&2, &2, M.CmError, B.Octets>}
263      tr.cbc_e2(~K, ~enc, k, v, M.cm.split(xs), B.len(xs))
264
265def tr.cbc_d2(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, +v: M.CmBlock, s: M.CmSplit, +n: Nat) -> {C.cbc.d2(~K, ~dec, k, v, s, n) == C.cbc.d2.fast(~K, ~dec, k, v, s, n) : Result<&2, &2, M.CmError, B.Octets>}:
266  match s:
267    case M.CmSplit{+bs, tail}:
268      match tail:
269        case Nil{}:
270          %tr.cbc_dec_eq(~K, ~dec, k, bs, v) : {Done{B.Octets.of_list(M.cm.join_onto(C.cbc.dec(~K, ~dec, k, bs, v), Nil{}))} == Done{B.Octets.of_list(M.cm.join_onto.fast(_, Nil{}))} : Result<&2, &2, M.CmError, B.Octets>}
271          %tr.join_eq(C.cbc.dec(~K, ~dec, k, bs, v), Nil{}) : {Done{B.Octets.of_list(M.cm.join_onto(C.cbc.dec(~K, ~dec, k, bs, v), Nil{}))} == Done{B.Octets.of_list(_)} : Result<&2, &2, M.CmError, B.Octets>}
272          {==}
273        case Con{h, t}:
274          {==}
275
276def tr.cbc_d1(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, r: Result<&2, &2, M.CmError, M.CmBlock>, +xs: List<&2, U32>) -> {C.cbc.d1(~K, ~dec, k, r, xs) == C.cbc.d1.fast(~K, ~dec, k, r, xs) : Result<&2, &2, M.CmError, B.Octets>}:
277  match r:
278    case Fail{e}:
279      {==}
280    case Done{+v}:
281      %tr.split_eq(xs) : {C.cbc.d2(~K, ~dec, k, v, M.cm.split(xs), B.len(xs)) == C.cbc.d2.fast(~K, ~dec, k, v, _, B.len.fast(xs)) : Result<&2, &2, M.CmError, B.Octets>}
282      %BL.len_fast(xs) : {C.cbc.d2(~K, ~dec, k, v, M.cm.split(xs), B.len(xs)) == C.cbc.d2.fast(~K, ~dec, k, v, M.cm.split(xs), _) : Result<&2, &2, M.CmError, B.Octets>}
283      tr.cbc_d2(~K, ~dec, k, v, M.cm.split(xs), B.len(xs))
284
285def tr.cbc_encrypt(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, +iv: B.Octets, +m: B.Octets) -> {C.Cbc.encrypt.ref(~K, ~enc, k, iv, m) == C.Cbc.encrypt(~K, ~enc, k, iv, m) : Result<&2, &2, M.CmError, B.Octets>}:
286  tr.cbc_e1(~K, ~enc, k, C.cbc.iv(iv), B.Octets.to_list(m))
287
288def tr.cbc_decrypt(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, +iv: B.Octets, +c: B.Octets) -> {C.Cbc.decrypt.ref(~K, ~dec, k, iv, c) == C.Cbc.decrypt(~K, ~dec, k, iv, c) : Result<&2, &2, M.CmError, B.Octets>}:
289  tr.cbc_d1(~K, ~dec, k, C.cbc.iv(iv), B.Octets.to_list(c))
290
291# the blocks CBC encryption gives the cipher: each plaintext block XOR the
292# block before it (the IV first)
293def cbcp.ins(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, bs: List<&2, M.CmBlock>, +iv: M.CmBlock) -> List<&2, M.CmBlock>:
294  match bs:
295    case Nil{}:
296      Nil{}
297    case Con{+p, t}:
298      Con{M.CmBlock.xor(iv, p), cbcp.ins(~K, ~enc, k, t, enc(k, M.CmBlock.xor(iv, p)))}
299
300# CBC on blocks
301
302def cbcp.go(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, bs: List<&2, M.CmBlock>, +iv: M.CmBlock) -> {M.CmBlock.dec_enc(~K, ~enc, ~dec, k, cbcp.ins(~K, ~enc, k, bs, iv)) == cbcp.ins(~K, ~enc, k, bs, iv) : List<&2, M.CmBlock>} -> {C.cbc.dec(~K, ~dec, k, C.cbc.enc(~K, ~enc, k, bs, iv), iv) == bs : List<&2, M.CmBlock>}:
303  match bs:
304    case Nil{}:
305      h => {==}
306    case Con{+p, +t}:
307      +h => %Equal.sym(M.CmBlock, dec(k, enc(k, M.CmBlock.xor(iv, p))), M.CmBlock.xor(iv, p), cmp.hd(~K, ~enc, ~dec, k, M.CmBlock.xor(iv, p), cbcp.ins(~K, ~enc, k, t, enc(k, M.CmBlock.xor(iv, p))), h)) : {Con{M.CmBlock.xor(iv, _), C.cbc.dec(~K, ~dec, k, C.cbc.enc(~K, ~enc, k, t, enc(k, M.CmBlock.xor(iv, p))), enc(k, M.CmBlock.xor(iv, p)))} == Con{p, t} : List<&2, M.CmBlock>}
308        %bx.block(iv, p) : {Con{M.CmBlock.xor(iv, M.CmBlock.xor(iv, p)), C.cbc.dec(~K, ~dec, k, C.cbc.enc(~K, ~enc, k, t, enc(k, M.CmBlock.xor(iv, p))), enc(k, M.CmBlock.xor(iv, p)))} == Con{_, t} : List<&2, M.CmBlock>}
309        %cbcp.go(~K, ~enc, ~dec, k, t, enc(k, M.CmBlock.xor(iv, p)))(cmp.tl(~K, ~enc, ~dec, k, M.CmBlock.xor(iv, p), cbcp.ins(~K, ~enc, k, t, enc(k, M.CmBlock.xor(iv, p))), h)) : {Con{M.CmBlock.xor(iv, M.CmBlock.xor(iv, p)), C.cbc.dec(~K, ~dec, k, C.cbc.enc(~K, ~enc, k, t, enc(k, M.CmBlock.xor(iv, p))), enc(k, M.CmBlock.xor(iv, p)))} == Con{M.CmBlock.xor(iv, M.CmBlock.xor(iv, p)), _} : List<&2, M.CmBlock>}
310        {==}
311
312def Laws.cbc_blocks_round_trip(K, enc, dec, k, inv, iv, bs):
313  +v = iv
314  +b = bs
315  # the tail-recursive forms are the structural ones
316  %tr.cbc_enc_eq(~K, ~enc, k, b, v) : {C.cbc.dec.fast(~K, ~dec, k, _, iv) == bs : List<&2, M.CmBlock>}
317  %tr.cbc_dec_eq(~K, ~dec, k, C.cbc.enc(~K, ~enc, k, b, v), v) : {_ == bs : List<&2, M.CmBlock>}
318  cbcp.go(~K, ~enc, ~dec, k, b, v)(inv(cbcp.ins(~K, ~enc, k, b, v)))
319
320def Laws.cbc_round_trip(K, enc, dec, k, inv, iv, m, hi, hm):
321  +et = sp.mod_tail(B.Octets.to_list(m))(oc.mod(m, hm))
322  # the public defs are the structural ones
323  %tr.cbc_encrypt(~K, ~enc, k, iv, m) : {Result.bind(&2, &2, M.CmError, B.Octets, B.Octets, _, c => C.Cbc.decrypt(~K, ~dec, k, iv, c)) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
324  %tr.bind_cong(C.Cbc.encrypt.ref(~K, ~enc, k, iv, m), c => C.Cbc.decrypt.ref(~K, ~dec, k, iv, c), c => C.Cbc.decrypt(~K, ~dec, k, iv, c), c => tr.cbc_decrypt(~K, ~dec, k, iv, c)) : {_ == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
325  # the IV is a block
326  %Equal.sym(Result<&2, &2, M.CmError, M.CmBlock>, C.cbc.iv(iv), Done{M.cm.block_of(B.Octets.to_list(iv))}, cbcp.iv(iv, hi)) : {Result.bind(&2, &2, M.CmError, B.Octets, B.Octets, C.cbc.e1(~K, ~enc, k, _, B.Octets.to_list(m)), c => C.cbc.d1(~K, ~dec, k, _, B.Octets.to_list(c))) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
327  # the message is masked
328  %oc.masked(m) : {Result.bind(&2, &2, M.CmError, B.Octets, B.Octets, C.cbc.e2(~K, ~enc, k, M.cm.block_of(B.Octets.to_list(iv)), M.cm.split(_), B.len(B.Octets.to_list(m))), c => C.cbc.d1(~K, ~dec, k, Done{M.cm.block_of(B.Octets.to_list(iv))}, B.Octets.to_list(c))) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
329  # its split is its blocks and tail
330  %sp.eta(M.cm.split(B.mask(B.Octets.to_list(m)))) : {Result.bind(&2, &2, M.CmError, B.Octets, B.Octets, C.cbc.e2(~K, ~enc, k, M.cm.block_of(B.Octets.to_list(iv)), _, B.len(B.Octets.to_list(m))), c => C.cbc.d1(~K, ~dec, k, Done{M.cm.block_of(B.Octets.to_list(iv))}, B.Octets.to_list(c))) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
331  # whole blocks leave no tail, so encryption succeeds
332  %Equal.sym(List<&2, U32>, M.cm.split.tail(M.cm.split(B.mask(B.Octets.to_list(m)))), Nil{}, et) : {Result.bind(&2, &2, M.CmError, B.Octets, B.Octets, C.cbc.e2(~K, ~enc, k, M.cm.block_of(B.Octets.to_list(iv)), M.CmSplit{M.cm.split.blocks(M.cm.split(B.mask(B.Octets.to_list(m)))), _}, B.len(B.Octets.to_list(m))), c => C.cbc.d1(~K, ~dec, k, Done{M.cm.block_of(B.Octets.to_list(iv))}, B.Octets.to_list(c))) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
333  # decryption reads the ciphertext's bytes back, masked
334  %Equal.sym(List<&2, U32>, B.Octets.to_list(B.Octets.of_list(M.cm.join_onto(C.cbc.enc(~K, ~enc, k, M.cm.split.blocks(M.cm.split(B.mask(B.Octets.to_list(m)))), M.cm.block_of(B.Octets.to_list(iv))), Nil{}))), B.mask(M.cm.join_onto(C.cbc.enc(~K, ~enc, k, M.cm.split.blocks(M.cm.split(B.mask(B.Octets.to_list(m)))), M.cm.block_of(B.Octets.to_list(iv))), Nil{})), BL.octets_to_of(M.cm.join_onto(C.cbc.enc(~K, ~enc, k, M.cm.split.blocks(M.cm.split(B.mask(B.Octets.to_list(m)))), M.cm.block_of(B.Octets.to_list(iv))), Nil{}))) : {C.cbc.d2(~K, ~dec, k, M.cm.block_of(B.Octets.to_list(iv)), M.cm.split(_), B.len(B.Octets.to_list(B.Octets.of_list(M.cm.join_onto(C.cbc.enc(~K, ~enc, k, M.cm.split.blocks(M.cm.split(B.mask(B.Octets.to_list(m)))), M.cm.block_of(B.Octets.to_list(iv))), Nil{}))))) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
335  # which they already are
336  %Equal.sym(List<&2, U32>, B.mask(M.cm.join_onto(C.cbc.enc(~K, ~enc, k, M.cm.split.blocks(M.cm.split(B.mask(B.Octets.to_list(m)))), M.cm.block_of(B.Octets.to_list(iv))), Nil{})), M.cm.join_onto(C.cbc.enc(~K, ~enc, k, M.cm.split.blocks(M.cm.split(B.mask(B.Octets.to_list(m)))), M.cm.block_of(B.Octets.to_list(iv))), Nil{}), sp.mask_join(C.cbc.enc(~K, ~enc, k, M.cm.split.blocks(M.cm.split(B.mask(B.Octets.to_list(m)))), M.cm.block_of(B.Octets.to_list(iv))))) : {C.cbc.d2(~K, ~dec, k, M.cm.block_of(B.Octets.to_list(iv)), M.cm.split(_), B.len(B.Octets.to_list(B.Octets.of_list(M.cm.join_onto(C.cbc.enc(~K, ~enc, k, M.cm.split.blocks(M.cm.split(B.mask(B.Octets.to_list(m)))), M.cm.block_of(B.Octets.to_list(iv))), Nil{}))))) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
337  # and they split into the ciphertext blocks
338  %Equal.sym(M.CmSplit, M.cm.split(M.cm.join_onto(C.cbc.enc(~K, ~enc, k, M.cm.split.blocks(M.cm.split(B.mask(B.Octets.to_list(m)))), M.cm.block_of(B.Octets.to_list(iv))), Nil{})), M.CmSplit{C.cbc.enc(~K, ~enc, k, M.cm.split.blocks(M.cm.split(B.mask(B.Octets.to_list(m)))), M.cm.block_of(B.Octets.to_list(iv))), Nil{}}, sp.split_join(C.cbc.enc(~K, ~enc, k, M.cm.split.blocks(M.cm.split(B.mask(B.Octets.to_list(m)))), M.cm.block_of(B.Octets.to_list(iv))))) : {C.cbc.d2(~K, ~dec, k, M.cm.block_of(B.Octets.to_list(iv)), _, B.len(B.Octets.to_list(B.Octets.of_list(M.cm.join_onto(C.cbc.enc(~K, ~enc, k, M.cm.split.blocks(M.cm.split(B.mask(B.Octets.to_list(m)))), M.cm.block_of(B.Octets.to_list(iv))), Nil{}))))) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
339  # CBC on blocks
340  %Equal.sym(List<&2, M.CmBlock>, C.cbc.dec(~K, ~dec, k, C.cbc.enc(~K, ~enc, k, M.cm.split.blocks(M.cm.split(B.mask(B.Octets.to_list(m)))), M.cm.block_of(B.Octets.to_list(iv))), M.cm.block_of(B.Octets.to_list(iv))), M.cm.split.blocks(M.cm.split(B.mask(B.Octets.to_list(m)))), cbcp.go(~K, ~enc, ~dec, k, M.cm.split.blocks(M.cm.split(B.mask(B.Octets.to_list(m)))), M.cm.block_of(B.Octets.to_list(iv)))(inv(cbcp.ins(~K, ~enc, k, M.cm.split.blocks(M.cm.split(B.mask(B.Octets.to_list(m)))), M.cm.block_of(B.Octets.to_list(iv)))))) : {Done{B.Octets.of_list(M.cm.join_onto(_, Nil{}))} == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
341  # the plaintext blocks and the empty tail
342  %et : {Done{B.Octets.of_list(M.cm.join_onto(M.cm.split.blocks(M.cm.split(B.mask(B.Octets.to_list(m)))), _))} == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
343  # join back to the message
344  %Equal.sym(List<&2, U32>, M.cm.join_onto(M.cm.split.blocks(M.cm.split(B.mask(B.Octets.to_list(m)))), M.cm.split.tail(M.cm.split(B.mask(B.Octets.to_list(m))))), B.mask(B.Octets.to_list(m)), sp.join_split(B.Octets.to_list(m))) : {Done{B.Octets.of_list(_)} == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
345  # 
346  %Equal.sym(List<&2, U32>, B.mask(B.Octets.to_list(m)), B.Octets.to_list(m), oc.masked(m)) : {Done{B.Octets.of_list(_)} == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
347  # 
348  %Equal.sym(B.Octets, B.Octets.of_list(B.Octets.to_list(m)), m, BL.octets_of_to(m)) : {Done{_} == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
349  {==}