LAWS.bend

bend-osdev-mode-core@0.1.0.0 · 212 lines · 33 definitions

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.
5import Base
6import bend-osdev-bytes@0.1.1.0/bytes.bend as B
7import bend-osdev-mode-core@0.1.0.0/mode_core.bend as M
8
9# A block written as Octets reads back as the same block, for every block
10law 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
19law byte_byte:
20  for y: U32
21  {B.byte(B.byte(y)) == B.byte(y) : U32}
22
23law 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
28law 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
33law split_eta:
34  for s: M.CmSplit
35  {M.CmSplit{M.cm.split.blocks(s), M.cm.split.tail(s)} == s : M.CmSplit}
36
37law 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
42law 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
47law 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
52law 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
57law 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
62law 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
68law 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
75law 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
81law 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
87law 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
92law 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
113law 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
118law 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
123law 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
129law 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))
134law octets_masked:
135  for +o: B.Octets
136  {B.mask(B.Octets.to_list(o)) == B.Octets.to_list(o) : List<&2, U32>}
137
138law 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
144law blocks_len_fast:
145  for +bs: List<&2, M.CmBlock>
146  {List.length(&2, M.CmBlock, bs) == M.cm.blocks.len(bs) : Nat}
147
148law split_fast:
149  for +xs: List<&2, U32>
150  {M.cm.split(xs) == M.cm.split.fast(xs) : M.CmSplit}
151
152law 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
158law 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
166law 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
176law 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
186law 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
192law u32_xor_xor:
193  for a: U32
194  for b: U32
195  {U32.xor(U32.xor(a, b), b) == a : U32}
196
197law 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
202law 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
208law 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}