1	# Laws about mode-core's public interface: a block survives its byte form;
2	# and the lemmas the modes' proofs share (bend-osdev-cbc, -xts, -ccm, and
3	# -aes for the block's bytes), as laws: a package's proofs can use another
4	# package's laws, not its private lemmas.
5	import Base
6	import bend-osdev-bytes@0.1.1.0/bytes.bend as B
7	import ./mode_core.bend as M
8	
9	# A block written as Octets reads back as the same block, for every block
10	law block_octets_round_trip:
11	  for +b: M.CmBlock
12	  {M.CmBlock.of_octets(M.CmBlock.to_octets(b)) == Some{b} : Maybe<&2, M.CmBlock>}
13	
14	# Lemmas the modes' proofs share, as laws (new with the split of
15	# bend-osdev-cipher-modes; they were private lemmas of its PROOF.bend). They
16	# are about the byte layer every mode is built from (mode-core.bend's cm.*),
17	# bytes' list layer, XOR, and the round-trip hypothesis CmBlock.dec_enc.
18	
19	law byte_byte:
20	  for y: U32
21	  {B.byte(B.byte(y)) == B.byte(y) : U32}
22	
23	law split_cons_blocks:
24	  for b: M.CmBlock
25	  for s: M.CmSplit
26	  {M.cm.split.blocks(M.cm.split.cons(b, s)) == Con{b, M.cm.split.blocks(s)} : List<&2, M.CmBlock>}
27	
28	law split_cons_tail:
29	  for b: M.CmBlock
30	  for s: M.CmSplit
31	  {M.cm.split.tail(M.cm.split.cons(b, s)) == M.cm.split.tail(s) : List<&2, U32>}
32	
33	law split_eta:
34	  for s: M.CmSplit
35	  {M.CmSplit{M.cm.split.blocks(s), M.cm.split.tail(s)} == s : M.CmSplit}
36	
37	law list_take_append:
38	  for +a: List<&2, U32>
39	  for +b: List<&2, U32>
40	  {B.take(B.len(a), B.append(a, b)) == a : List<&2, U32>}
41	
42	law list_drop_append:
43	  for +a: List<&2, U32>
44	  for +b: List<&2, U32>
45	  {B.drop(B.len(a), B.append(a, b)) == b : List<&2, U32>}
46	
47	law list_mask_append:
48	  for +a: List<&2, U32>
49	  for +b: List<&2, U32>
50	  {B.mask(B.append(a, b)) == B.append(B.mask(a), B.mask(b)) : List<&2, U32>}
51	
52	law list_mask_take:
53	  for +n: Nat
54	  for +xs: List<&2, U32>
55	  {B.mask(B.take(n, xs)) == B.take(n, B.mask(xs)) : List<&2, U32>}
56	
57	law list_len_append:
58	  for +a: List<&2, U32>
59	  for +b: List<&2, U32>
60	  {B.len(B.append(a, b)) == Nat.add(B.len(a), B.len(b)) : Nat}
61	
62	law list_len_take:
63	  for +n: Nat
64	  for +xs: List<&2, U32>
65	  for h1: {Nat.is_le(n, B.len(xs)) == True{} : Bool}
66	  {B.len(B.take(n, xs)) == n : Nat}
67	
68	law nat_lt_le:
69	  for +a: Nat
70	  for +b: Nat
71	  for h1: {Nat.is_lt(a, b) == True{} : Bool}
72	  {Nat.is_le(a, b) == True{} : Bool}
73	
74	# splitting the bytes of a block gives the block back
75	law split_bytes_onto:
76	  for b: M.CmBlock
77	  for rest: List<&2, U32>
78	  {M.cm.split(M.cm.bytes_onto(b, rest)) == M.cm.split.cons(b, M.cm.split(rest)) : M.CmSplit}
79	
80	# the bytes of a block are bytes: masking changes nothing
81	law mask_bytes_onto:
82	  for b: M.CmBlock
83	  for rest: List<&2, U32>
84	  {B.mask(M.cm.bytes_onto(b, rest)) == M.cm.bytes_onto(b, B.mask(rest)) : List<&2, U32>}
85	
86	# a masked list is its blocks and its tail joined back
87	law join_split:
88	  for ys: List<&2, U32>
89	  {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>}
90	
91	# the bytes of the block of any 16 values are those values, masked
92	law bytes_onto_block16:
93	  for z0: U32
94	  for z1: U32
95	  for z2: U32
96	  for z3: U32
97	  for z4: U32
98	  for z5: U32
99	  for z6: U32
100	  for z7: U32
101	  for z8: U32
102	  for z9: U32
103	  for z10: U32
104	  for z11: U32
105	  for z12: U32
106	  for z13: U32
107	  for z14: U32
108	  for z15: U32
109	  for rest: List<&2, U32>
110	  {M.cm.bytes_onto(M.cm.block16(z0, z1, z2, z3, z4, z5, z6, z7, z8, z9, z10, z11, z12, z13, z14, z15), rest) == Con{B.byte(z0), Con{B.byte(z1), Con{B.byte(z2), Con{B.byte(z3), Con{B.byte(z4), Con{B.byte(z5), Con{B.byte(z6), Con{B.byte(z7), Con{B.byte(z8), Con{B.byte(z9), Con{B.byte(z10), Con{B.byte(z11), Con{B.byte(z12), Con{B.byte(z13), Con{B.byte(z14), Con{B.byte(z15), rest}}}}}}}}}}}}}}}} : List<&2, U32>}
111	
112	# the tail of a split has fewer than 16 bytes
113	law split_tail_short:
114	  for ys: List<&2, U32>
115	  {Nat.is_lt(B.len(M.cm.split.tail(M.cm.split(B.mask(ys)))), 16n) == True{} : Bool}
116	
117	# the tail of a masked split is masked
118	law split_tail_masked:
119	  for ys: List<&2, U32>
120	  {B.mask(M.cm.split.tail(M.cm.split(B.mask(ys)))) == M.cm.split.tail(M.cm.split(B.mask(ys))) : List<&2, U32>}
121	
122	# fewer than 16 bytes are all tail
123	law split_short:
124	  for ys: List<&2, U32>
125	  for h1: {Nat.is_lt(B.len(ys), 16n) == True{} : Bool}
126	  {M.cm.split(ys) == M.CmSplit{Nil{}, ys} : M.CmSplit}
127	
128	# the block of a block's bytes is the block
129	law block_of_bytes_of:
130	  for b: M.CmBlock
131	  {M.cm.block_of(M.cm.bytes_of(b)) == b : M.CmBlock}
132	
133	# Every Octets is masked: to_list(o) = to_list(of_list(to_list(o))) = mask(to_list(o))
134	law octets_masked:
135	  for +o: B.Octets
136	  {B.mask(B.Octets.to_list(o)) == B.Octets.to_list(o) : List<&2, U32>}
137	
138	law octets_len:
139	  for +o: B.Octets
140	  for +n: Nat
141	  for h: {B.Octets.len(o) == n : Nat}
142	  {B.len(B.Octets.to_list(o)) == n : Nat}
143	
144	law blocks_len_fast:
145	  for +bs: List<&2, M.CmBlock>
146	  {List.length(&2, M.CmBlock, bs) == M.cm.blocks.len(bs) : Nat}
147	
148	law split_fast:
149	  for +xs: List<&2, U32>
150	  {M.cm.split(xs) == M.cm.split.fast(xs) : M.CmSplit}
151	
152	law join_onto_fast:
153	  for +bs: List<&2, M.CmBlock>
154	  for +rest: List<&2, U32>
155	  {M.cm.join_onto(bs, rest) == M.cm.join_onto.fast(bs, rest) : List<&2, U32>}
156	
157	# a bind whose continuations agree on every value agrees
158	law bind_cong:
159	  for r: Result<&2, &2, M.CmError, B.Octets>
160	  for f: B.Octets -> Result<&2, &2, M.CmError, B.Octets>
161	  for g: B.Octets -> Result<&2, &2, M.CmError, B.Octets>
162	  for h: @c: B.Octets -> {f(c) == g(c) : Result<&2, &2, M.CmError, B.Octets>}
163	  {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>}
164	
165	# the first block's round trip, and the rest's
166	law dec_enc_head:
167	  for ~K: Data
168	  for ~enc: K -> M.CmBlock -> M.CmBlock
169	  for ~dec: K -> M.CmBlock -> M.CmBlock
170	  for +k: K
171	  for +x: M.CmBlock
172	  for +xs: List<&2, M.CmBlock>
173	  for +h: {M.CmBlock.dec_enc(~K, ~enc, ~dec, k, Con{x, xs}) == Con{x, xs} : List<&2, M.CmBlock>}
174	  {dec(k, enc(k, x)) == x : M.CmBlock}
175	
176	law dec_enc_tail:
177	  for ~K: Data
178	  for ~enc: K -> M.CmBlock -> M.CmBlock
179	  for ~dec: K -> M.CmBlock -> M.CmBlock
180	  for +k: K
181	  for +x: M.CmBlock
182	  for +xs: List<&2, M.CmBlock>
183	  for +h: {M.CmBlock.dec_enc(~K, ~enc, ~dec, k, Con{x, xs}) == Con{x, xs} : List<&2, M.CmBlock>}
184	  {M.CmBlock.dec_enc(~K, ~enc, ~dec, k, xs) == xs : List<&2, M.CmBlock>}
185	
186	law word_xor_xor:
187	  for n: Nat
188	  for a: Word(n)
189	  for b: Word(n)
190	  {Word.xor(n, Word.xor(n, a, b), b) == a : Word(n)}
191	
192	law u32_xor_xor:
193	  for a: U32
194	  for b: U32
195	  {U32.xor(U32.xor(a, b), b) == a : U32}
196	
197	law block_xor_xor:
198	  for +a: M.CmBlock
199	  for +b: M.CmBlock
200	  {M.CmBlock.xor(M.CmBlock.xor(a, b), b) == a : M.CmBlock}
201	
202	law mask_join_onto:
203	  for bs: List<&2, M.CmBlock>
204	  for +rest: List<&2, U32>
205	  {B.mask(M.cm.join_onto(bs, rest)) == M.cm.join_onto(bs, B.mask(rest)) : List<&2, U32>}
206	
207	# blocks joined in front of a short tail split back into those blocks and tail
208	law split_join_short:
209	  for bs: List<&2, M.CmBlock>
210	  for +rest: List<&2, U32>
211	  for h1: {M.cm.split(rest) == M.CmSplit{Nil{}, rest} : M.CmSplit}
212	  {M.cm.split(M.cm.join_onto(bs, rest)) == M.CmSplit{bs, rest} : M.CmSplit}