proofs/crypto/sha3/conformance.bend
bend-collections-laws-crypto@1.0.0.0 · 171 lines · 8 definitions
1
2import Base
3import bend-collections-laws-crypto@1.0.0.0/src/crypto/keccak/types.bend as T
4import bend-collections-laws-crypto@1.0.0.0/src/crypto/keccak/permutation.bend as P
5import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha3/core.bend as C
6import bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha3.bend as F
7import bend-collections-laws-crypto@1.0.0.0/spec/crypto/keccak/permutation.bend as K
8import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/keccak/permutation.bend as KP
9
10
11
12
13
14
15
16law inject_correct:
17 for +s: T.State
18 for +l0: T.Lane
19 for +l1: T.Lane
20 for +l2: T.Lane
21 for +l3: T.Lane
22 for +l4: T.Lane
23 for +l5: T.Lane
24 for +l6: T.Lane
25 for +l7: T.Lane
26 for +l8: T.Lane
27 for +l9: T.Lane
28 for +l10: T.Lane
29 for +l11: T.Lane
30 for +l12: T.Lane
31 for +l13: T.Lane
32 for +l14: T.Lane
33 for +l15: T.Lane
34 for +l16: T.Lane
35 {C.inject(s, l0, l1, l2, l3, l4, l5, l6, l7, l8, l9, l10, l11, l12, l13, l14, l15, l16) == F.of_lanes(F.xor_lanes(F.to_lanes(s), [l0, l1, l2, l3, l4, l5, l6, l7, l8, l9, l10, l11, l12, l13, l14, l15, l16])) : T.State}
36
37def inject_correct(s, l0, l1, l2, l3, l4, l5, l6, l7, l8, l9, l10, l11, l12, l13, l14, l15, l16):
38 match s l0 l1 l2 l3 l4 l5 l6 l7 l8 l9 l10 l11 l12 l13 l14 l15 l16:
39 case T.S{T.W{p0, q0}, T.W{p1, q1}, T.W{p2, q2}, T.W{p3, q3}, T.W{p4, q4}, T.W{p5, q5}, T.W{p6, q6}, T.W{p7, q7}, T.W{p8, q8}, T.W{p9, q9}, T.W{p10, q10}, T.W{p11, q11}, T.W{p12, q12}, T.W{p13, q13}, T.W{p14, q14}, T.W{p15, q15}, T.W{p16, q16}, T.W{p17, q17}, T.W{p18, q18}, T.W{p19, q19}, T.W{p20, q20}, T.W{p21, q21}, T.W{p22, q22}, T.W{p23, q23}, T.W{p24, q24}} T.W{u0, v0} T.W{u1, v1} T.W{u2, v2} T.W{u3, v3} T.W{u4, v4} T.W{u5, v5} T.W{u6, v6} T.W{u7, v7} T.W{u8, v8} T.W{u9, v9} T.W{u10, v10} T.W{u11, v11} T.W{u12, v12} T.W{u13, v13} T.W{u14, v14} T.W{u15, v15} T.W{u16, v16}:
40 {==}
41
42law absorb_correct:
43 for +ls: List<&2, T.Lane>
44 for +rounds: Nat
45 for +s: T.State
46 {C.absorb(ls, rounds, s) == F.absorb(ls, rounds, s) : T.State}
47
48def absorb_correct(ls, rounds, s):
49 match ls:
50 case l0 <> l1 <> l2 <> l3 <> l4 <> l5 <> l6 <> l7 <> l8 <> l9 <> l10 <> l11 <> l12 <> l13 <> l14 <> l15 <> l16 <> rest:
51 +x = F.of_lanes(F.xor_lanes(F.to_lanes(s), [l0, l1, l2, l3, l4, l5, l6, l7, l8, l9, l10, l11, l12, l13, l14, l15, l16]))
52 %inject_correct(s, l0, l1, l2, l3, l4, l5, l6, l7, l8, l9, l10, l11, l12, l13, l14, l15, l16) :
53 {C.absorb(l0 <> l1 <> l2 <> l3 <> l4 <> l5 <> l6 <> l7 <> l8 <> l9 <> l10 <> l11 <> l12 <> l13 <> l14 <> l15 <> l16 <> rest, rounds, s) == F.absorb(rest, rounds, K.rounds(rounds, 0n, _)) : T.State}
54 %KP.rounds_correct(rounds, 0n, C.inject(s, l0, l1, l2, l3, l4, l5, l6, l7, l8, l9, l10, l11, l12, l13, l14, l15, l16)) :
55 {C.absorb(l0 <> l1 <> l2 <> l3 <> l4 <> l5 <> l6 <> l7 <> l8 <> l9 <> l10 <> l11 <> l12 <> l13 <> l14 <> l15 <> l16 <> rest, rounds, s) == F.absorb(rest, rounds, _) : T.State}
56 absorb_correct(rest, rounds, P.rounds(rounds, 0n, C.inject(s, l0, l1, l2, l3, l4, l5, l6, l7, l8, l9, l10, l11, l12, l13, l14, l15, l16)))
57 case Nil{}:
58 {==}
59 case l0 <> Nil{}:
60 {==}
61 case l0 <> l1 <> Nil{}:
62 {==}
63 case l0 <> l1 <> l2 <> Nil{}:
64 {==}
65 case l0 <> l1 <> l2 <> l3 <> Nil{}:
66 {==}
67 case l0 <> l1 <> l2 <> l3 <> l4 <> Nil{}:
68 {==}
69 case l0 <> l1 <> l2 <> l3 <> l4 <> l5 <> Nil{}:
70 {==}
71 case l0 <> l1 <> l2 <> l3 <> l4 <> l5 <> l6 <> Nil{}:
72 {==}
73 case l0 <> l1 <> l2 <> l3 <> l4 <> l5 <> l6 <> l7 <> Nil{}:
74 {==}
75 case l0 <> l1 <> l2 <> l3 <> l4 <> l5 <> l6 <> l7 <> l8 <> Nil{}:
76 {==}
77 case l0 <> l1 <> l2 <> l3 <> l4 <> l5 <> l6 <> l7 <> l8 <> l9 <> Nil{}:
78 {==}
79 case l0 <> l1 <> l2 <> l3 <> l4 <> l5 <> l6 <> l7 <> l8 <> l9 <> l10 <> Nil{}:
80 {==}
81 case l0 <> l1 <> l2 <> l3 <> l4 <> l5 <> l6 <> l7 <> l8 <> l9 <> l10 <> l11 <> Nil{}:
82 {==}
83 case l0 <> l1 <> l2 <> l3 <> l4 <> l5 <> l6 <> l7 <> l8 <> l9 <> l10 <> l11 <> l12 <> Nil{}:
84 {==}
85 case l0 <> l1 <> l2 <> l3 <> l4 <> l5 <> l6 <> l7 <> l8 <> l9 <> l10 <> l11 <> l12 <> l13 <> Nil{}:
86 {==}
87 case l0 <> l1 <> l2 <> l3 <> l4 <> l5 <> l6 <> l7 <> l8 <> l9 <> l10 <> l11 <> l12 <> l13 <> l14 <> Nil{}:
88 {==}
89 case l0 <> l1 <> l2 <> l3 <> l4 <> l5 <> l6 <> l7 <> l8 <> l9 <> l10 <> l11 <> l12 <> l13 <> l14 <> l15 <> Nil{}:
90 {==}
91
92law lanes_correct:
93 for +bytes: List<&2, U32>
94 {C.lanes(bytes) == F.lanes(bytes) : List<&2, T.Lane>}
95
96def lanes_correct(bytes):
97 match bytes:
98 case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
99 %lanes_correct(rest) :
100 {C.lanes(b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest) == T.W{F.le32(b0, b1, b2, b3), F.le32(b4, b5, b6, b7)} <> _ : List<&2, T.Lane>}
101 {==}
102 case Nil{}:
103 {==}
104 case b0 <> Nil{}:
105 {==}
106 case b0 <> b1 <> Nil{}:
107 {==}
108 case b0 <> b1 <> b2 <> Nil{}:
109 {==}
110 case b0 <> b1 <> b2 <> b3 <> Nil{}:
111 {==}
112 case b0 <> b1 <> b2 <> b3 <> b4 <> Nil{}:
113 {==}
114 case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> Nil{}:
115 {==}
116 case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> Nil{}:
117 {==}
118
119law tail_correct:
120 for +q: Nat
121 {C.tail(q) == F.padding_bytes(q) : List<&2, U32>}
122
123def tail_correct(q):
124 match q:
125 case 0n:
126 {==}
127 case 1n:
128 {==}
129 case 2n+k:
130 {==}
131
132law suffix_correct:
133 for +n: Nat
134 {C.suffix(n) == F.padding(n) : List<&2, U32>}
135
136def suffix_correct(n):
137 tail_correct(Nat.sub(136n, Nat.mod(n, 136n)))
138
139law digest_correct:
140 for +s: T.State
141 {C.digest_bytes(s) == F.squeeze(s) : List<&2, U32>}
142
143def digest_correct(s):
144 match s:
145 case T.S{T.W{p0, q0}, T.W{p1, q1}, T.W{p2, q2}, T.W{p3, q3}, T.W{p4, q4}, T.W{p5, q5}, T.W{p6, q6}, T.W{p7, q7}, T.W{p8, q8}, T.W{p9, q9}, T.W{p10, q10}, T.W{p11, q11}, T.W{p12, q12}, T.W{p13, q13}, T.W{p14, q14}, T.W{p15, q15}, T.W{p16, q16}, T.W{p17, q17}, T.W{p18, q18}, T.W{p19, q19}, T.W{p20, q20}, T.W{p21, q21}, T.W{p22, q22}, T.W{p23, q23}, T.W{p24, q24}}:
146 {==}
147
148law digest_length:
149 for +s: T.State
150 {List.length(&2, U32, C.digest_bytes(s)) == 32n : Nat}
151
152def digest_length(s):
153 match s:
154 case T.S{T.W{p0, q0}, T.W{p1, q1}, T.W{p2, q2}, T.W{p3, q3}, T.W{p4, q4}, T.W{p5, q5}, T.W{p6, q6}, T.W{p7, q7}, T.W{p8, q8}, T.W{p9, q9}, T.W{p10, q10}, T.W{p11, q11}, T.W{p12, q12}, T.W{p13, q13}, T.W{p14, q14}, T.W{p15, q15}, T.W{p16, q16}, T.W{p17, q17}, T.W{p18, q18}, T.W{p19, q19}, T.W{p20, q20}, T.W{p21, q21}, T.W{p22, q22}, T.W{p23, q23}, T.W{p24, q24}}:
155 {==}
156
157law keccak_correct:
158 for +bytes: List<&2, U32>
159 for +rounds: Nat
160 {C.keccak(bytes, rounds) == F.keccak(bytes, rounds) : List<&2, U32>}
161
162def keccak_correct(bytes, rounds):
163 +n = List.length(&2, U32, bytes)
164 %suffix_correct(n) :
165 {C.keccak(bytes, rounds) == F.squeeze(F.absorb(F.lanes(List.append(&2, U32, bytes, _)), rounds, F.initial())) : List<&2, U32>}
166 +padded = List.append(&2, U32, bytes, C.suffix(n))
167 %lanes_correct(padded) :
168 {C.keccak(bytes, rounds) == F.squeeze(F.absorb(_, rounds, F.initial())) : List<&2, U32>}
169 %absorb_correct(C.lanes(padded), rounds, C.zero()) :
170 {C.keccak(bytes, rounds) == F.squeeze(_) : List<&2, U32>}
171 digest_correct(C.absorb(C.lanes(padded), rounds, C.zero()))