proofs/crypto/subtle/word.bend

bend-collections-laws-crypto@1.0.0.0 · 278 lines · 16 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
3
4# Bit-level facts about zero tests on words, for any width, then at U32.
5# A word is zero when it compares EQ with Word.zero; Word.cmp compares the
6# tail first and settles ties with the head (Word.cmp.fin).
7
8law and_true:
9  for +b: Bool
10  {Bool.and(b, True{}) == b : Bool}
11
12def and_true(b):
13  match b:
14    case False{}:
15      {==}
16    case True{}:
17      {==}
18
19law and_false:
20  for +b: Bool
21  {Bool.and(b, False{}) == False{} : Bool}
22
23def and_false(b):
24  match b:
25    case False{}:
26      {==}
27    case True{}:
28      {==}
29
30law and_assoc:
31  for +a: Bool
32  for +b: Bool
33  for +c: Bool
34  {Bool.and(Bool.and(a, b), c) == Bool.and(a, Bool.and(b, c)) : Bool}
35
36def and_assoc(a, b, c):
37  match a:
38    case False{}:
39      {==}
40    case True{}:
41      {==}
42
43# A comparison is EQ exactly when the tails compare EQ and the heads agree.
44law fin_eq:
45  for +ab: Bool
46  for +bb: Bool
47  for +t: Cmp
48  {Cmp.is_eq(Word.cmp.fin(ab, bb, t)) == Bool.and(Cmp.is_eq(t), Cmp.is_eq(Bool.cmp(ab, bb))) : Bool}
49
50def fin_eq(ab, bb, t):
51  match t:
52    case LT{}:
53      {==}
54    case EQ{}:
55      {==}
56    case GT{}:
57      {==}
58
59law bits_or:
60  for +a: Bool
61  for +b: Bool
62  for +x: Bool
63  for +y: Bool
64  {Bool.and(Bool.and(a, b), Cmp.is_eq(Bool.cmp(Bool.or(x, y), False{}))) ==
65    Bool.and(Bool.and(a, Cmp.is_eq(Bool.cmp(x, False{}))), Bool.and(b, Cmp.is_eq(Bool.cmp(y, False{})))) : Bool}
66
67def bits_or(a, b, x, y):
68  match a b x y:
69    case False{} _ _ _:
70      {==}
71    case True{} False{} False{} _:
72      {==}
73    case True{} False{} True{} _:
74      {==}
75    case True{} True{} False{} False{}:
76      {==}
77    case True{} True{} False{} True{}:
78      {==}
79    case True{} True{} True{} False{}:
80      {==}
81    case True{} True{} True{} True{}:
82      {==}
83
84law bits_xor:
85  for +k: Bool
86  for +x: Bool
87  for +y: Bool
88  {Bool.and(k, Cmp.is_eq(Bool.cmp(Bool.xor(x, y), False{}))) == Bool.and(k, Cmp.is_eq(Bool.cmp(x, y))) : Bool}
89
90def bits_xor(k, x, y):
91  match x y:
92    case False{} False{}:
93      {==}
94    case False{} True{}:
95      {==}
96    case True{} False{}:
97      {==}
98    case True{} True{}:
99      {==}
100
101law bit_eq:
102  for +x: Bool
103  for +y: Bool
104  for +h: {Cmp.is_eq(Bool.cmp(x, y)) == True{} : Bool}
105  {x == y : Bool}
106
107def bit_eq(x, y, h):
108  match x y:
109    case False{} False{}:
110      {==}
111    case False{} True{}:
112      Empty.absurd({False{} == True{} : Bool}, L.false_true(h))
113    case True{} False{}:
114      Empty.absurd({True{} == False{} : Bool}, L.false_true(h))
115    case True{} True{}:
116      {==}
117
118law bit_refl:
119  for +k: Bool
120  for +x: Bool
121  {Bool.and(k, Cmp.is_eq(Bool.cmp(x, x))) == k : Bool}
122
123def bit_refl(k, x):
124  match x:
125    case False{}:
126      and_true(k)
127    case True{}:
128      and_true(k)
129
130# zero(x | y) == zero(x) && zero(y)
131law or_zero:
132  for +n: Nat
133  for +x: Word(n)
134  for +y: Word(n)
135  {Cmp.is_eq(Word.cmp(n, Word.or(n, x, y), Word.zero(n))) ==
136    Bool.and(Cmp.is_eq(Word.cmp(n, x, Word.zero(n))), Cmp.is_eq(Word.cmp(n, y, Word.zero(n)))) : Bool}
137
138def or_zero(n, x, y):
139  match n:
140    case 0n:
141      {==}
142    case 1n+p:
143      match x y:
144        case WCon{a, xt} WCon{b, yt}:
145          +co = Word.cmp(p, Word.or(p, xt, yt), Word.zero(p))
146          +cx = Word.cmp(p, xt, Word.zero(p))
147          +cy = Word.cmp(p, yt, Word.zero(p))
148          %Equal.sym(Bool, Cmp.is_eq(Word.cmp.fin(Bool.or(a, b), False{}, co)),
149            Bool.and(Cmp.is_eq(co), Cmp.is_eq(Bool.cmp(Bool.or(a, b), False{}))),
150            fin_eq(Bool.or(a, b), False{}, co)) :
151            {_ == Bool.and(Cmp.is_eq(Word.cmp.fin(a, False{}, cx)), Cmp.is_eq(Word.cmp.fin(b, False{}, cy))) : Bool}
152          %Equal.sym(Bool, Cmp.is_eq(Word.cmp.fin(a, False{}, cx)),
153            Bool.and(Cmp.is_eq(cx), Cmp.is_eq(Bool.cmp(a, False{}))),
154            fin_eq(a, False{}, cx)) :
155            {Bool.and(Cmp.is_eq(co), Cmp.is_eq(Bool.cmp(Bool.or(a, b), False{}))) == Bool.and(_, Cmp.is_eq(Word.cmp.fin(b, False{}, cy))) : Bool}
156          %Equal.sym(Bool, Cmp.is_eq(Word.cmp.fin(b, False{}, cy)),
157            Bool.and(Cmp.is_eq(cy), Cmp.is_eq(Bool.cmp(b, False{}))),
158            fin_eq(b, False{}, cy)) :
159            {Bool.and(Cmp.is_eq(co), Cmp.is_eq(Bool.cmp(Bool.or(a, b), False{}))) == Bool.and(Bool.and(Cmp.is_eq(cx), Cmp.is_eq(Bool.cmp(a, False{}))), _) : Bool}
160          %Equal.sym(Bool, Cmp.is_eq(co), Bool.and(Cmp.is_eq(cx), Cmp.is_eq(cy)), or_zero(p, xt, yt)) :
161            {Bool.and(_, Cmp.is_eq(Bool.cmp(Bool.or(a, b), False{}))) == Bool.and(Bool.and(Cmp.is_eq(cx), Cmp.is_eq(Bool.cmp(a, False{}))), Bool.and(Cmp.is_eq(cy), Cmp.is_eq(Bool.cmp(b, False{})))) : Bool}
162          bits_or(Cmp.is_eq(cx), Cmp.is_eq(cy), a, b)
163
164# zero(x ^ y) == (x == y)
165law xor_zero:
166  for +n: Nat
167  for +x: Word(n)
168  for +y: Word(n)
169  {Cmp.is_eq(Word.cmp(n, Word.xor(n, x, y), Word.zero(n))) == Cmp.is_eq(Word.cmp(n, x, y)) : Bool}
170
171def xor_zero(n, x, y):
172  match n:
173    case 0n:
174      {==}
175    case 1n+p:
176      match x y:
177        case WCon{a, xt} WCon{b, yt}:
178          +co = Word.cmp(p, Word.xor(p, xt, yt), Word.zero(p))
179          +c = Word.cmp(p, xt, yt)
180          %Equal.sym(Bool, Cmp.is_eq(Word.cmp.fin(Bool.xor(a, b), False{}, co)),
181            Bool.and(Cmp.is_eq(co), Cmp.is_eq(Bool.cmp(Bool.xor(a, b), False{}))),
182            fin_eq(Bool.xor(a, b), False{}, co)) :
183            {_ == Cmp.is_eq(Word.cmp.fin(a, b, c)) : Bool}
184          %Equal.sym(Bool, Cmp.is_eq(Word.cmp.fin(a, b, c)),
185            Bool.and(Cmp.is_eq(c), Cmp.is_eq(Bool.cmp(a, b))), fin_eq(a, b, c)) :
186            {Bool.and(Cmp.is_eq(co), Cmp.is_eq(Bool.cmp(Bool.xor(a, b), False{}))) == _ : Bool}
187          %Equal.sym(Bool, Cmp.is_eq(co), Cmp.is_eq(c), xor_zero(p, xt, yt)) :
188            {Bool.and(_, Cmp.is_eq(Bool.cmp(Bool.xor(a, b), False{}))) == Bool.and(Cmp.is_eq(c), Cmp.is_eq(Bool.cmp(a, b))) : Bool}
189          bits_xor(Cmp.is_eq(c), a, b)
190
191law cmp_sound:
192  for +n: Nat
193  for +x: Word(n)
194  for +y: Word(n)
195  for +h: {Cmp.is_eq(Word.cmp(n, x, y)) == True{} : Bool}
196  {x == y : Word(n)}
197
198def cmp_sound(n, x, y, h):
199  match n:
200    case 0n:
201      match x y:
202        case WNil{} WNil{}:
203          {==}
204    case 1n+p:
205      match x y:
206        case WCon{a, xt} WCon{b, yt}:
207          +c = Word.cmp(p, xt, yt)
208          +h2 = Equal.trans(Bool, Bool.and(Cmp.is_eq(c), Cmp.is_eq(Bool.cmp(a, b))),
209            Cmp.is_eq(Word.cmp.fin(a, b, c)), True{},
210            Equal.sym(Bool, Cmp.is_eq(Word.cmp.fin(a, b, c)),
211              Bool.and(Cmp.is_eq(c), Cmp.is_eq(Bool.cmp(a, b))), fin_eq(a, b, c)), h)
212          +et = cmp_sound(p, xt, yt, L.and_left(Cmp.is_eq(c), Cmp.is_eq(Bool.cmp(a, b)), h2))
213          +eb = bit_eq(a, b, L.and_right(Cmp.is_eq(c), Cmp.is_eq(Bool.cmp(a, b)), h2))
214          %et : {WCon{a, xt} == WCon{b, _} : Word(1n+p)}
215          %eb : {WCon{a, xt} == WCon{_, xt} : Word(1n+p)}
216          {==}
217
218law cmp_refl:
219  for +n: Nat
220  for +x: Word(n)
221  {Cmp.is_eq(Word.cmp(n, x, x)) == True{} : Bool}
222
223def cmp_refl(n, x):
224  match n:
225    case 0n:
226      {==}
227    case 1n+p:
228      match x:
229        case WCon{a, xt}:
230          +c = Word.cmp(p, xt, xt)
231          %Equal.sym(Bool, Cmp.is_eq(Word.cmp.fin(a, a, c)),
232            Bool.and(Cmp.is_eq(c), Cmp.is_eq(Bool.cmp(a, a))), fin_eq(a, a, c)) :
233            {_ == True{} : Bool}
234          %Equal.sym(Bool, Bool.and(Cmp.is_eq(c), Cmp.is_eq(Bool.cmp(a, a))), Cmp.is_eq(c), bit_refl(Cmp.is_eq(c), a)) : {_ == True{} : Bool}
235          cmp_refl(p, xt)
236
237# ---- at U32
238
239law u32_or_zero:
240  for +x: U32
241  for +y: U32
242  {U32.is_eq(U32.or(x, y), 0) == Bool.and(U32.is_eq(x, 0), U32.is_eq(y, 0)) : Bool}
243
244def u32_or_zero(x, y):
245  match x y:
246    case U32{a} U32{b}:
247      or_zero(32n, a, b)
248
249law u32_xor_zero:
250  for +x: U32
251  for +y: U32
252  {U32.is_eq(U32.xor(x, y), 0) == U32.is_eq(x, y) : Bool}
253
254def u32_xor_zero(x, y):
255  match x y:
256    case U32{a} U32{b}:
257      xor_zero(32n, a, b)
258
259law u32_sound:
260  for +x: U32
261  for +y: U32
262  for +h: {U32.is_eq(x, y) == True{} : Bool}
263  {x == y : U32}
264
265def u32_sound(x, y, h):
266  match x y:
267    case U32{a} U32{b}:
268      %cmp_sound(32n, a, b, h) : {U32{a} == U32{_} : U32}
269      {==}
270
271law u32_refl:
272  for +x: U32
273  {U32.is_eq(x, x) == True{} : Bool}
274
275def u32_refl(x):
276  match x:
277    case U32{a}:
278      cmp_refl(32n, a)