1	import Base
2	import bend-osdev-bytes@0.1.1.0/bytes.bend as B
3	import bend-osdev-bytes@0.1.1.0/LAWS.bend as BL
4	import bend-osdev-bytes@0.1.1.0/PROOF.bend as BP
5	import ./cipher_core.bend as L
6	import ./modes64.bend as X
7	import ./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	
12	def 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	
23	def 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	
36	def 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	
45	def 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	
50	def 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	
55	def 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
61	def 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	
66	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}:
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	
76	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}:
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	
82	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}:
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	
88	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}:
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	
96	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}:
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	
106	def 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)
113	def 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	
120	def b64.mdisc(m: Maybe<&2, L.LcBlock64>) -> Type:
121	  match m:
122	    case Some{b}:
123	      Empty
124	    case None{}:
125	      Unit
126	
127	def 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)
132	def 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, W
135	      {==}
136	
137	
138	# a block read from a list of bytes is written back as those bytes
139	def 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	
180	def 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	
183	def 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
186	def 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	
193	def 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	
200	def 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	
208	def 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	
218	def 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	
229	def 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	
242	def 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	
248	def 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	
255	def 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	
262	def 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	
269	def 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	
278	def 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	
283	def 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	
288	def 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	
292	def 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	
298	def Laws.word_xor_cancel(n, a, b):
299	  word_xx(n, a, b)
300	
301	def Laws.u32_xor_cancel(a, b):
302	  u32_xx(a, b)
303	
304	def Laws.block64_xor_cancel(a, b):
305	  b64_xx2(a, b)
306	
307	def Laws.rotl1_rotl31(x):
308	  rot_1_31(x)
309	
310	def Laws.rotl31_rotl1(x):
311	  rot_31_1(x)
312	
313	def Laws.bswap_bswap(x):
314	  bswap2(x)
315	
316	def Laws.feistel_unrun_run(RK, f, ks, b):
317	  fe_unrun_run(~RK, ~f, ks, b)
318	
319	def 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	
326	def 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	
331	def 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	
336	def 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	
341	def 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	
348	def Laws.modes64_not_whole_blocks():
349	  {==}