proofs/crypto/argon2/index.bend
bend-collections-laws-crypto@1.0.0.0 · 212 lines · 20 definitions
1import Base
2import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-crypto@1.0.0.0/spec/math/w64.bend as SW
4import bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend as X
5import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as WU
6import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend as U
7import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
8import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64mul.bend as W64M
9import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/words.bend as LW
10import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW
11import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/types.bend as T
12import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/types.bend as A
13import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/blamka.bend as G
14import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/argon2.bend as I
15import bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake2b.bend as B
16import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/blamka.bend as SG
17import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend as SA
18import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/gb.bend as GB
19import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/blamka.bend as BL
20
21
22
23
24
25
26
27
28def row_at_eq(+b: A.Block, +i: Nat) -> {I.row_at(b, i) == SG.row(b, i) : T.State}:
29 match b i:
30 case A.B{r0, r1, r2, r3, r4, r5, r6, r7} 0n:
31 {==}
32 case A.B{r0, r1, r2, r3, r4, r5, r6, r7} 1n:
33 {==}
34 case A.B{r0, r1, r2, r3, r4, r5, r6, r7} 2n:
35 {==}
36 case A.B{r0, r1, r2, r3, r4, r5, r6, r7} 3n:
37 {==}
38 case A.B{r0, r1, r2, r3, r4, r5, r6, r7} 4n:
39 {==}
40 case A.B{r0, r1, r2, r3, r4, r5, r6, r7} 5n:
41 {==}
42 case A.B{r0, r1, r2, r3, r4, r5, r6, r7} 6n:
43 {==}
44 case A.B{r0, r1, r2, r3, r4, r5, r6, r7} 7n+z:
45 {==}
46
47def at_eq(+v: T.State, +j: Nat) -> {I.at(v, j) == B.at(v, j) : T.Lane}:
48 match v j:
49 case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 0n:
50 {==}
51 case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 1n:
52 {==}
53 case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 2n:
54 {==}
55 case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 3n:
56 {==}
57 case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 4n:
58 {==}
59 case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 5n:
60 {==}
61 case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 6n:
62 {==}
63 case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 7n:
64 {==}
65 case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 8n:
66 {==}
67 case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 9n:
68 {==}
69 case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 10n:
70 {==}
71 case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 11n:
72 {==}
73 case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 12n:
74 {==}
75 case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 13n:
76 {==}
77 case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 14n:
78 {==}
79 case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 15n:
80 {==}
81 case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 16n+z:
82 {==}
83
84def lane_eq(+b: A.Block, +n: Nat) -> {I.lane(b, n) == SG.lane(b, n) : T.Lane}:
85 Equal.trans(T.Lane, I.at(I.row_at(b, Nat.div(n, 16n)), Nat.mod(n, 16n)), I.at(SG.row(b, Nat.div(n, 16n)), Nat.mod(n, 16n)), SG.lane(b, n),
86 Equal.cong(T.State, T.Lane, z => I.at(z, Nat.mod(n, 16n)), I.row_at(b, Nat.div(n, 16n)), SG.row(b, Nat.div(n, 16n)), row_at_eq(b, Nat.div(n, 16n))),
87 at_eq(SG.row(b, Nat.div(n, 16n)), Nat.mod(n, 16n)))
88
89def pick_eq(+indep: Bool, +addr: A.Block, +idx: Nat, +prev: A.Block) -> {I.pick(indep, addr, idx, prev) == SA.pick(indep, addr, idx, prev) : T.Lane}:
90 match indep:
91 case True{}:
92 lane_eq(addr, Nat.mod(idx, 128n))
93 case False{}:
94 lane_eq(prev, 0n)
95
96def hi_eq(+x: T.Lane) -> {I.hi(x) == SA.hi(x) : U32}:
97 match x:
98 case T.W{l, h}:
99 {==}
100
101def lo_eq(+x: T.Lane) -> {G.lo(x) == SA.lo(x) : U32}:
102 match x:
103 case T.W{l, h}:
104 {==}
105
106
107
108def ref_lane_eq(+forced: Bool, +l: Nat, +j2: U32, +p: Nat) -> {I.ref_lane(forced, l, j2, p) == SA.ref_lane(forced, l, j2, p) : Nat}:
109 match forced:
110 case True{}:
111 {==}
112 case False{}:
113 {==}
114
115def area_base_eq(+r0: Bool, +s: Nat, +sl: Nat, +q: Nat) -> {I.area_base(r0, s, sl, q) == SA.area_base(r0, s, sl, q) : Nat}:
116 match r0:
117 case True{}:
118 {==}
119 case False{}:
120 {==}
121
122def area_other_eq(+base: Nat, +zero: Bool) -> {I.area_other(base, zero) == SA.area_other(base, zero) : Nat}:
123 match zero:
124 case True{}:
125 {==}
126 case False{}:
127 {==}
128
129def area_eq(+base: Nat, +idx: Nat, +same: Bool) -> {I.area(base, idx, same) == SA.area(base, idx, same) : Nat}:
130 match same:
131 case True{}:
132 {==}
133 case False{}:
134 area_other_eq(base, Nat.is_eq(idx, 0n))
135
136def start_last_eq(+s: Nat, +sl: Nat, +last: Bool) -> {I.start_last(s, sl, last) == SA.start_last(s, sl, last) : Nat}:
137 match last:
138 case True{}:
139 {==}
140 case False{}:
141 {==}
142
143def start_eq(+r0: Bool, +s: Nat, +sl: Nat) -> {I.start(r0, s, sl) == SA.start(r0, s, sl) : Nat}:
144 match r0:
145 case True{}:
146 {==}
147 case False{}:
148 start_last_eq(s, sl, Nat.is_eq(s, 3n))
149
150def prev_index_eq(+l: Nat, +q: Nat, +j: Nat, +first: Bool) -> {I.prev_index(l, q, j, first) == SA.prev_index(l, q, j, first) : Nat}:
151 match first:
152 case True{}:
153 {==}
154 case False{}:
155 {==}
156
157def start_index_eq(+first: Bool) -> {I.start_index(first) == SA.start_index(first) : Nat}:
158 match first:
159 case True{}:
160 {==}
161 case False{}:
162 {==}
163
164def fits_value(+x: WU.U64) -> {C.fits(64n, SW.value(x)) == True{} : Bool}:
165 match x:
166 case WU.U64{+l, +h}:
167 WW.limbs_fit(32n, 32n, LW.v(l), LW.v(h), LW.vb(l), LW.vb(h))
168
169
170
171
172def hi_mul(+a: U32, +b: U32) -> {U32.to_nat(X.hi(X.mul32(a, b))) == C.high(32n, Nat.mul(U32.to_nat(a), U32.to_nat(b))) : Nat}:
173 +n = Nat.mul(U32.to_nat(a), U32.to_nat(b))
174 +f64 = L.subst(Nat, z => {C.fits(64n, z) == True{} : Bool}, SW.value(X.mul32(a, b)), n, W64M.mul32_value(a, b), fits_value(X.mul32(a, b)))
175 +f32 = LW.fits_high(32n, 32n, n, f64)
176 %Equal.sym(WU.U64, X.mul32(a, b), SW.of_nat(n), GB.mul32_of(a, b)) : {U32.to_nat(X.hi(_)) == C.high(32n, n) : Nat}
177 LW.vo(C.high(32n, n), f32)
178
179
180def rel_eq(+w: Nat, +j1: U32, +k: Nat, +hk: {Nat.is_le(k, 32n) == True{} : Bool}, +hw: {Nat.is_lt(w, C.pow2(k)) == True{} : Bool}) -> {I.rel(w, j1) == SA.rel(w, j1) : Nat}:
181 +xi = X.hi(X.mul32(j1, j1))
182 +xs = C.high(32n, Nat.mul(U32.to_nat(j1), U32.to_nat(j1)))
183 +ew = U.to_nat_from_nat(w, k, hk, hw)
184 +e1 = hi_mul(U32.from_nat(w), xi)
185 +e2 = Equal.trans(Nat, C.high(32n, Nat.mul(U32.to_nat(U32.from_nat(w)), U32.to_nat(xi))), C.high(32n, Nat.mul(w, U32.to_nat(xi))), C.high(32n, Nat.mul(w, xs)),
186 Equal.cong(Nat, Nat, z => C.high(32n, Nat.mul(z, U32.to_nat(xi))), U32.to_nat(U32.from_nat(w)), w, ew),
187 Equal.cong(Nat, Nat, z => C.high(32n, Nat.mul(w, z)), U32.to_nat(xi), xs, hi_mul(j1, j1)))
188 Equal.cong(Nat, Nat, z => Nat.sub(Nat.sub(w, 1n), z), U32.to_nat(X.hi(X.mul32(U32.from_nat(w), xi))), C.high(32n, Nat.mul(w, xs)), Equal.trans(Nat, U32.to_nat(X.hi(X.mul32(U32.from_nat(w), xi))), C.high(32n, Nat.mul(U32.to_nat(U32.from_nat(w)), U32.to_nat(xi))), C.high(32n, Nat.mul(w, xs)), e1, e2))
189
190
191
192def input_eq(+r: Nat, +l: Nat, +s: Nat, +mm: Nat, +t: Nat, +ctr: Nat) -> {I.input_block(r, l, s, mm, t, ctr) == SA.input_block(r, l, s, mm, t, ctr) : A.Block}:
193 match r:
194 case 0n:
195 {==}
196 case 1n+x:
197 {==}
198
199def addresses_eq(+r: Nat, +l: Nat, +s: Nat, +mm: Nat, +t: Nat, +ctr: Nat) -> {I.addresses(r, l, s, mm, t, ctr) == SA.addresses(r, l, s, mm, t, ctr) : A.Block}:
200 +z = SA.input_block(r, l, s, mm, t, ctr)
201 Equal.trans(A.Block, G.compress(G.zero(), G.compress(G.zero(), I.input_block(r, l, s, mm, t, ctr))), G.compress(G.zero(), G.compress(G.zero(), z)), SG.G(SG.zero(), SG.G(SG.zero(), z)),
202 Equal.cong(A.Block, A.Block, x => G.compress(G.zero(), G.compress(G.zero(), x)), I.input_block(r, l, s, mm, t, ctr), z, input_eq(r, l, s, mm, t, ctr)),
203 Equal.trans(A.Block, G.compress(G.zero(), G.compress(G.zero(), z)), G.compress(G.zero(), SG.G(SG.zero(), z)), SG.G(SG.zero(), SG.G(SG.zero(), z)),
204 Equal.cong(A.Block, A.Block, x => G.compress(G.zero(), x), G.compress(G.zero(), z), SG.G(SG.zero(), z), BL.compress_correct(G.zero(), z)),
205 BL.compress_correct(G.zero(), SG.G(SG.zero(), z))))
206
207def regen_eq(+need: Bool, +addr: A.Block, +r: Nat, +l: Nat, +s: Nat, +mm: Nat, +t: Nat, +idx: Nat) -> {I.regen(need, addr, r, l, s, mm, t, idx) == SA.regen(need, addr, r, l, s, mm, t, idx) : A.Block}:
208 match need:
209 case True{}:
210 addresses_eq(r, l, s, mm, t, Nat.add(Nat.div(idx, 128n), 1n))
211 case False{}:
212 {==}