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.
4	import Base
5	import bend-osdev-bytes@0.1.1.0/bytes.bend as B
6	import bend-osdev-bytes@0.1.1.0/LAWS.bend as BL
7	import bend-osdev-bytes@0.1.1.0/PROOF.bend as BP
8	import bend-osdev-mode-core@0.1.0.0/mode_core.bend as M
9	import ./cbc.bend as C
10	import bend-osdev-mode-core@0.1.0.0/LAWS.bend as CoreL
11	import bend-osdev-mode-core@0.1.0.0/PROOF.bend as CoreP
12	import ./LAWS.bend as Laws
13	
14	# mode-core's laws, under the names these proofs use
15	
16	def 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	
19	def 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	
22	def 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	
25	def 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	
28	def 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	
31	def 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	
34	def 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	
37	def tr.split_eq(+xs: List<&2, U32>) -> {M.cm.split(xs) == M.cm.split.fast(xs) : M.CmSplit}:
38	  CoreL.split_fast(xs)
39	
40	def 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	
43	def 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	
46	def 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	
49	def 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	
54	def 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	
65	def 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	
78	def 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
85	def 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	
96	def sp.disc(n: Nat) -> Type:
97	  match n:
98	    case 0n:
99	      Empty
100	    case 1n+p:
101	      Unit
102	
103	def sp.absurd(p: Nat, h: {1n+p == 0n : Nat}) -> Empty:
104	  %h : sp.disc(_)
105	  Unit{}
106	
107	def 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	
110	def 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	
121	def 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
125	def 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	
195	def 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	
204	def 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	
213	def 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
217	def 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	
223	def 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	
230	def 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	
233	def 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	
240	def 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	
245	def 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	
256	def 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	
265	def 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	
276	def 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	
285	def 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	
288	def 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)
293	def 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	
302	def 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	
312	def 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	
320	def 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	  {==}