proof/AES_TagCompareProof.bend
qasim-bend-kit@0.1.0.2 · 121 lines · 8 definitions
1import Base
2import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES
3import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/subtle/word.bend as SW
4import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as Logic
5
6def diff_same(+a: List<&2, U32>, +acc: U32,
7 acc_zero: {U32.is_eq(acc, 0) == True{} : Bool}) ->
8 {U32.is_eq(AES.bytes_difference.go(a, a, acc), 0) == True{} : Bool}:
9 match a:
10 case Nil{}: acc_zero
11 case x <> xs:
12 xor_zero = Equal.trans(Bool,
13 U32.is_eq(U32.xor(x, x), 0), U32.is_eq(x, x), True{},
14 SW.u32_xor_zero(x, x), SW.u32_refl(x))
15 both = Logic.and_intro(U32.is_eq(acc, 0),
16 U32.is_eq(U32.xor(x, x), 0), acc_zero, xor_zero)
17 next_zero = Equal.trans(Bool,
18 U32.is_eq(U32.or(acc, U32.xor(x, x)), 0),
19 Bool.and(U32.is_eq(acc, 0), U32.is_eq(U32.xor(x, x), 0)),
20 True{}, SW.u32_or_zero(acc, U32.xor(x, x)), both)
21 diff_same(xs, U32.or(acc, U32.xor(x, x)), next_zero)
22
23def equal_same(+a: List<&2, U32>) ->
24 {AES.bytes_equal_full_scan(a, a) == True{} : Bool}:
25 diff_same(a, 0, {==})
26
27def equal_of_equal(+a: List<&2, U32>, +b: List<&2, U32>,
28 same: {a == b : List<&2, U32>}) ->
29 {AES.bytes_equal_full_scan(a, b) == True{} : Bool}:
30 Equal.trans(Bool, AES.bytes_equal_full_scan(a, b),
31 AES.bytes_equal_full_scan(b, b), True{},
32 Equal.cong(List<&2, U32>, Bool,
33 left => AES.bytes_equal_full_scan(left, b), a, b, same),
34 equal_same(b))
35
36def diff_acc_zero(+a: List<&2, U32>, +b: List<&2, U32>, +acc: U32,
37 zero: {U32.is_eq(AES.bytes_difference.go(a, b, acc), 0) == True{} : Bool}) ->
38 {U32.is_eq(acc, 0) == True{} : Bool}:
39 match a b:
40 case Nil{} Nil{}: zero
41 case Nil{} y <> ys:
42 Empty.absurd({U32.is_eq(acc, 0) == True{} : Bool},
43 Logic.false_true(zero))
44 case x <> xs Nil{}:
45 Empty.absurd({U32.is_eq(acc, 0) == True{} : Bool},
46 Logic.false_true(zero))
47 case x <> xs y <> ys:
48 acc2 = U32.or(acc, U32.xor(x, y))
49 step_zero = diff_acc_zero(xs, ys, acc2, zero)
50 both = Equal.trans(Bool,
51 Bool.and(U32.is_eq(acc, 0), U32.is_eq(U32.xor(x, y), 0)),
52 U32.is_eq(acc2, 0), True{},
53 Equal.sym(Bool, U32.is_eq(acc2, 0),
54 Bool.and(U32.is_eq(acc, 0),
55 U32.is_eq(U32.xor(x, y), 0)),
56 SW.u32_or_zero(acc, U32.xor(x, y))),
57 step_zero)
58 Logic.and_left(U32.is_eq(acc, 0),
59 U32.is_eq(U32.xor(x, y), 0), both)
60
61def diff_list_sound(+a: List<&2, U32>, +b: List<&2, U32>, +acc: U32,
62 +zero: {U32.is_eq(AES.bytes_difference.go(a, b, acc), 0) == True{} : Bool}) ->
63 {a == b : List<&2, U32>}:
64 match a b:
65 case Nil{} Nil{}: {==}
66 case Nil{} y <> ys:
67 Empty.absurd({Nil{} == y <> ys : List<&2, U32>},
68 Logic.false_true(zero))
69 case x <> xs Nil{}:
70 Empty.absurd({x <> xs == Nil{} : List<&2, U32>},
71 Logic.false_true(zero))
72 case x <> xs y <> ys:
73 +acc2 = U32.or(acc, U32.xor(x, y))
74 acc2_zero = diff_acc_zero(xs, ys, acc2, zero)
75 both = Equal.trans(Bool,
76 Bool.and(U32.is_eq(acc, 0), U32.is_eq(U32.xor(x, y), 0)),
77 U32.is_eq(acc2, 0), True{},
78 Equal.sym(Bool, U32.is_eq(acc2, 0),
79 Bool.and(U32.is_eq(acc, 0),
80 U32.is_eq(U32.xor(x, y), 0)),
81 SW.u32_or_zero(acc, U32.xor(x, y))),
82 acc2_zero)
83 xor_zero = Logic.and_right(U32.is_eq(acc, 0),
84 U32.is_eq(U32.xor(x, y), 0), both)
85 byte_equal = SW.u32_sound(x, y,
86 Equal.trans(Bool, U32.is_eq(x, y),
87 U32.is_eq(U32.xor(x, y), 0), True{},
88 Equal.sym(Bool, U32.is_eq(U32.xor(x, y), 0),
89 U32.is_eq(x, y), SW.u32_xor_zero(x, y)),
90 xor_zero))
91 tail_equal = diff_list_sound(xs, ys, acc2, zero)
92 Equal.trans(List<&2, U32>, x <> xs, y <> xs, y <> ys,
93 Equal.cong(U32, List<&2, U32>, h => h <> xs,
94 x, y, byte_equal),
95 Equal.cong(List<&2, U32>, List<&2, U32>,
96 t => y <> t, xs, ys, tail_equal))
97
98def equal_sound(+a: List<&2, U32>, +b: List<&2, U32>,
99 accepted: {AES.bytes_equal_full_scan(a, b) == True{} : Bool}) ->
100 {a == b : List<&2, U32>}:
101 diff_list_sound(a, b, 0, accepted)
102
103def unequal_from_bool(+a: List<&2, U32>, +b: List<&2, U32>,
104 compared: Bool,
105 link: {compared == AES.bytes_equal_full_scan(a, b) : Bool},
106 unequal: {a != b : List<&2, U32>}) ->
107 {AES.bytes_equal_full_scan(a, b) == False{} : Bool}:
108 match compared:
109 case False{}:
110 Equal.sym(Bool, False{}, AES.bytes_equal_full_scan(a, b), link)
111 case True{}:
112 accepted = Equal.sym(Bool, True{},
113 AES.bytes_equal_full_scan(a, b), link)
114 Empty.absurd(
115 {AES.bytes_equal_full_scan(a, b) == False{} : Bool},
116 unequal(equal_sound(a, b, accepted)))
117
118def unequal_is_false(+a: List<&2, U32>, +b: List<&2, U32>,
119 unequal: {a != b : List<&2, U32>}) ->
120 {AES.bytes_equal_full_scan(a, b) == False{} : Bool}:
121 unequal_from_bool(a, b, AES.bytes_equal_full_scan(a, b), {==}, unequal)