proofs/crypto/aead/subtle_eq.bend
bend-collections-laws-crypto@1.0.0.0 · 84 lines · 5 definitions
1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/subtle.bend as Subtle
3import bend-collections-laws-crypto@1.0.0.0/spec/crypto/subtle.bend as SS
4import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
5import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/subtle/word.bend as SW
6
7
8
9
10law step:
11 for +acc: U32
12 for +x: U32
13 for +y: U32
14 for +e: Bool
15 {Bool.and(U32.is_eq(U32.or(acc, U32.xor(x, y)), 0), e) == Bool.and(U32.is_eq(acc, 0), Bool.and(U32.is_eq(x, y), e)) : Bool}
16
17def step(acc, x, y, e):
18 %Equal.sym(Bool, U32.is_eq(U32.or(acc, U32.xor(x, y)), 0),
19 Bool.and(U32.is_eq(acc, 0), U32.is_eq(U32.xor(x, y), 0)), SW.u32_or_zero(acc, U32.xor(x, y))) :
20 {Bool.and(_, e) == Bool.and(U32.is_eq(acc, 0), Bool.and(U32.is_eq(x, y), e)) : Bool}
21 %Equal.sym(Bool, U32.is_eq(U32.xor(x, y), 0), U32.is_eq(x, y), SW.u32_xor_zero(x, y)) :
22 {Bool.and(Bool.and(U32.is_eq(acc, 0), _), e) == Bool.and(U32.is_eq(acc, 0), Bool.and(U32.is_eq(x, y), e)) : Bool}
23 SW.and_assoc(U32.is_eq(acc, 0), U32.is_eq(x, y), e)
24
25law fold:
26 for +a: List<&2, U32>
27 for +b: List<&2, U32>
28 for +acc: U32
29 {Bool.and(Nat.is_eq(List.length(&2, U32, a), List.length(&2, U32, b)), U32.is_eq(Subtle.diff(a, b, acc), 0)) ==
30 Bool.and(U32.is_eq(acc, 0), SS.equal(a, b)) : Bool}
31
32def fold(a, b, acc):
33 match a b:
34 case Nil{} Nil{}:
35 Equal.sym(Bool, Bool.and(U32.is_eq(acc, 0), True{}), U32.is_eq(acc, 0), SW.and_true(U32.is_eq(acc, 0)))
36 case Nil{} y <> ys:
37 Equal.sym(Bool, Bool.and(U32.is_eq(acc, 0), False{}), False{}, SW.and_false(U32.is_eq(acc, 0)))
38 case x <> xs Nil{}:
39 Equal.sym(Bool, Bool.and(U32.is_eq(acc, 0), False{}), False{}, SW.and_false(U32.is_eq(acc, 0)))
40 case x <> xs y <> ys:
41 +acc2 = U32.or(acc, U32.xor(x, y))
42 Equal.trans(Bool,
43 Bool.and(Nat.is_eq(List.length(&2, U32, xs), List.length(&2, U32, ys)), U32.is_eq(Subtle.diff(xs, ys, acc2), 0)),
44 Bool.and(U32.is_eq(acc2, 0), SS.equal(xs, ys)),
45 Bool.and(U32.is_eq(acc, 0), Bool.and(U32.is_eq(x, y), SS.equal(xs, ys))),
46 fold(xs, ys, acc2),
47 step(acc, x, y, SS.equal(xs, ys)))
48
49law equal_sound:
50 for +a: List<&2, U32>
51 for +b: List<&2, U32>
52 for +h: {SS.equal(a, b) == True{} : Bool}
53 {a == b : List<&2, U32>}
54
55def equal_sound(a, b, h):
56 match a b:
57 case Nil{} Nil{}: {==}
58 case Nil{} y <> ys: Empty.absurd({Nil{} == y <> ys : List<&2, U32>}, L.false_true(h))
59 case x <> xs Nil{}: Empty.absurd({x <> xs == Nil{} : List<&2, U32>}, L.false_true(h))
60 case x <> xs y <> ys:
61 +exy = SW.u32_sound(x, y, L.and_left(U32.is_eq(x, y), SS.equal(xs, ys), h))
62 +et = equal_sound(xs, ys, L.and_right(U32.is_eq(x, y), SS.equal(xs, ys), h))
63 %et : {x <> xs == y <> _ : List<&2, U32>}
64 %exy : {x <> xs == _ <> xs : List<&2, U32>}
65 {==}
66
67law equal_refl:
68 for +a: List<&2, U32>
69 {SS.equal(a, a) == True{} : Bool}
70
71def equal_refl(a):
72 match a:
73 case Nil{}: {==}
74 case x <> xs:
75 %Equal.sym(Bool, U32.is_eq(x, x), True{}, SW.u32_refl(x)) : {Bool.and(_, SS.equal(xs, xs)) == True{} : Bool}
76 equal_refl(xs)
77
78law eq_value:
79 for +a: List<&2, U32>
80 for +b: List<&2, U32>
81 {Subtle.eq(a, b) == SS.equal(a, b) : Bool}
82
83def eq_value(a, b):
84 fold(a, b, 0)