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