proofs/crypto/argon2/password.bend
bend-collections-laws-crypto@1.0.0.0 · 307 lines · 38 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/proofs/lib/nat.bend as N
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/lib/lemmas/proofs/nat_algebra.bend as NA
6import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR
7import bend-collections-laws-crypto@1.0.0.0/proofs/math/hash/hash.bend as HH
8import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/words.bend as LW
9import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW
10import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/shrn.bend as SR
11import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/subtle/word.bend as SW
12import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/types.bend as T
13import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/sized.bend as H
14import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/argon2.bend as A2
15import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/blamka.bend as G
16import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/memory.bend as M
17import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/phc.bend as PH
18import bend-collections-laws-crypto@1.0.0.0/src/crypto/password.bend as PW
19import bend-collections-laws-crypto@1.0.0.0/src/crypto/subtle.bend as Subtle
20import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/phc.bend as PP
21
22
23
24
25
26
27
28def len(xs: List<&2, U32>) -> Nat:
29 List.length(&2, U32, xs)
30
31def len_append(+a: List<&2, U32>, +b: List<&2, U32>) -> {len(List.append(&2, U32, a, b)) == Nat.add(len(a), len(b)) : Nat}:
32 match a:
33 case Nil{}:
34 {==}
35 case +x <> +r:
36 Equal.cong(Nat, Nat, z => 1n+z, len(List.append(&2, U32, r, b)), Nat.add(len(r), len(b)), len_append(r, b))
37
38def len_take(+xs: List<&2, U32>, +k: Nat, +h: {Nat.is_le(k, len(xs)) == True{} : Bool}) -> {len(List.take(&2, U32, xs, k)) == k : Nat}:
39 match xs k:
40 case Nil{} 0n:
41 {==}
42 case Nil{} 1n+j:
43 Empty.absurd({len(List.take(&2, U32, Nil{}, 1n+j)) == 1n+j : Nat}, L.false_true(h))
44 case Con{x, r} 0n:
45 {==}
46 case Con{+x, +r} 1n+ +j:
47 Equal.cong(Nat, Nat, z => 1n+z, len(List.take(&2, U32, r, j)), j, len_take(r, j, h))
48
49def chain_len(+h: T.Chain) -> {len(H.chain_bytes(h)) == 64n : Nat}:
50 match h:
51 case T.H{T.W{a0, b0}, T.W{a1, b1}, T.W{a2, b2}, T.W{a3, b3}, T.W{a4, b4}, T.W{a5, b5}, T.W{a6, b6}, T.W{a7, b7}}:
52 {==}
53
54def hash_len(+nn: Nat, +bs: List<&2, U32>, +h: {Nat.is_le(nn, 64n) == True{} : Bool}) -> {len(H.hash(nn, bs)) == nn : Nat}:
55 +c = H.chain(nn, H.pack(bs), List.length(&2, U32, bs))
56 len_take(H.chain_bytes(c), nn, L.subst(Nat, z => {Nat.is_le(nn, z) == True{} : Bool}, 64n, len(H.chain_bytes(c)), Equal.sym(Nat, len(H.chain_bytes(c)), 64n, chain_len(c)), h))
57
58
59def hp_go_len(+n: Nat, +v: List<&2, U32>, +last: Nat, +hv: {len(v) == 64n : Nat}, +hl: {Nat.is_le(last, 64n) == True{} : Bool}) -> {len(A2.hp_go(n, v, last)) == Nat.add(Nat.mul(1n+n, 32n), last) : Nat}:
60 match n v:
61 case _ Nil{}:
62 Empty.absurd({len(Nil{}) == Nat.add(Nat.mul(1n+n, 32n), last) : Nat}, N.zero_succ(63n, hv))
63 case 0n +x <> +r:
64 %Equal.sym(Nat, len(List.append(&2, U32, List.take(&2, U32, x <> r, 32n), H.hash(last, x <> r))), Nat.add(len(List.take(&2, U32, x <> r, 32n)), len(H.hash(last, x <> r))), len_append(List.take(&2, U32, x <> r, 32n), H.hash(last, x <> r))) : {_ == Nat.add(32n, last) : Nat}
65 %Equal.sym(Nat, len(List.take(&2, U32, x <> r, 32n)), 32n, len_take(x <> r, 32n, L.subst(Nat, z => {Nat.is_le(32n, z) == True{} : Bool}, 64n, len(x <> r), Equal.sym(Nat, len(x <> r), 64n, hv), {==}))) : {Nat.add(_, len(H.hash(last, x <> r))) == Nat.add(32n, last) : Nat}
66 %Equal.sym(Nat, len(H.hash(last, x <> r)), last, hash_len(last, x <> r, hl)) : {Nat.add(32n, _) == Nat.add(32n, last) : Nat}
67 {==}
68 case 1n+ +p +x <> +r:
69 +w = H.hash(64n, x <> r)
70 %Equal.sym(Nat, len(List.append(&2, U32, List.take(&2, U32, x <> r, 32n), A2.hp_go(p, w, last))), Nat.add(len(List.take(&2, U32, x <> r, 32n)), len(A2.hp_go(p, w, last))), len_append(List.take(&2, U32, x <> r, 32n), A2.hp_go(p, w, last))) : {_ == Nat.add(Nat.mul(2n+p, 32n), last) : Nat}
71 %Equal.sym(Nat, len(List.take(&2, U32, x <> r, 32n)), 32n, len_take(x <> r, 32n, L.subst(Nat, z => {Nat.is_le(32n, z) == True{} : Bool}, 64n, len(x <> r), Equal.sym(Nat, len(x <> r), 64n, hv), {==}))) : {Nat.add(_, len(A2.hp_go(p, w, last))) == Nat.add(Nat.mul(2n+p, 32n), last) : Nat}
72 %Equal.sym(Nat, len(A2.hp_go(p, w, last)), Nat.add(Nat.mul(1n+p, 32n), last), hp_go_len(p, w, last, hash_len(64n, x <> r, {==}), hl)) : {Nat.add(32n, _) == Nat.add(Nat.mul(2n+p, 32n), last) : Nat}
73 Equal.sym(Nat, Nat.add(Nat.add(32n, Nat.mul(1n+p, 32n)), last), Nat.add(32n, Nat.add(Nat.mul(1n+p, 32n), last)), NA.add_assoc(32n, Nat.mul(1n+p, 32n), last))
74
75def lt96(+q: Nat, +r: Nat, +hq: {Nat.is_lt(q, 3n) == True{} : Bool}, +hr: {Nat.is_lt(r, 32n) == True{} : Bool}) -> {Nat.is_lt(Nat.add(Nat.mul(q, 32n), r), 96n) == True{} : Bool}:
76 match q:
77 case 0n:
78 N.lt_trans(r, 32n, 96n, hr, {==})
79 case 1n:
80 N.lt_trans(r, 32n, 64n, hr, {==})
81 case 2n:
82 hr
83 case 3n+j:
84 Empty.absurd({Nat.is_lt(Nat.add(Nat.mul(3n+j, 32n), r), 96n) == True{} : Bool}, N.lt_zero_absurd(j, hq))
85
86def ge96(+tl: Nat, +h: {Nat.is_le(65n, tl) == True{} : Bool}) -> {Nat.is_le(96n, Nat.add(tl, 31n)) == True{} : Bool}:
87 %Equal.sym(Nat, Nat.add(tl, 31n), Nat.add(31n, tl), N.add_comm(tl, 31n)) : {Nat.is_le(96n, _) == True{} : Bool}
88 h
89
90def sub_cancel(+c: Nat, +m: Nat, +r: Nat) -> {Nat.sub(Nat.add(c, Nat.add(m, r)), m) == Nat.add(c, r) : Nat}:
91 %Equal.sym(Nat, Nat.add(c, Nat.add(m, r)), Nat.add(m, Nat.add(c, r)), NA.add_swap(c, m, r)) : {Nat.sub(_, m) == Nat.add(c, r) : Nat}
92 N.add_sub_cancel(m, Nat.add(c, r))
93
94def big(+tl: Nat, +q: Nat, +r: Nat, +e: {Nat.add(tl, 31n) == Nat.add(Nat.mul(q, 32n), r) : Nat}, +hr: {Nat.is_lt(r, 32n) == True{} : Bool}, +ht: {Nat.is_le(65n, tl) == True{} : Bool}, +hq: {Nat.is_lt(q, 3n) == True{} : Bool}) -> Empty:
95 +h1 = ge96(tl, ht)
96 +h2 = L.subst(Nat, z => {Nat.is_lt(z, 96n) == True{} : Bool}, Nat.add(Nat.mul(q, 32n), r), Nat.add(tl, 31n), Equal.sym(Nat, Nat.add(tl, 31n), Nat.add(Nat.mul(q, 32n), r), e), lt96(q, r, hq, hr))
97 L.true_false(Equal.trans(Bool, True{}, Nat.is_lt(96n, 96n), False{}, Equal.sym(Bool, Nat.is_lt(96n, 96n), True{}, N.le_lt_trans(96n, Nat.add(tl, 31n), 96n, h1, h2)), N.lt_irrefl(96n)))
98
99
100def long_len(+tl: Nat, +q: Nat, +r: Nat, +v: List<&2, U32>, +e: {Nat.add(tl, 31n) == Nat.add(Nat.mul(q, 32n), r) : Nat}, +hr: {Nat.is_lt(r, 32n) == True{} : Bool}, +ht: {Nat.is_le(65n, tl) == True{} : Bool}, +hv: {len(v) == 64n : Nat}) -> {len(A2.hp_go(Nat.sub(Nat.sub(q, 2n), 1n), v, Nat.sub(tl, Nat.mul(32n, Nat.sub(q, 2n))))) == tl : Nat}:
101 match q:
102 case 0n:
103 Empty.absurd({len(A2.hp_go(0n, v, Nat.sub(tl, 0n))) == tl : Nat}, big(tl, 0n, r, e, hr, ht, {==}))
104 case 1n:
105 Empty.absurd({len(A2.hp_go(0n, v, Nat.sub(tl, 0n))) == tl : Nat}, big(tl, 1n, r, e, hr, ht, {==}))
106 case 2n:
107 Empty.absurd({len(A2.hp_go(0n, v, Nat.sub(tl, 0n))) == tl : Nat}, big(tl, 2n, r, e, hr, ht, {==}))
108 case 3n+ +j:
109 +m = Nat.mul(j, 32n)
110 +et = NR.add_cancel(31n, tl, Nat.add(65n, Nat.add(m, r)), Equal.trans(Nat, Nat.add(31n, tl), Nat.add(tl, 31n), Nat.add(Nat.mul(3n+j, 32n), r), N.add_comm(31n, tl), e))
111 %Equal.sym(Nat, tl, Nat.add(65n, Nat.add(m, r)), et) : {len(A2.hp_go(Nat.sub(j, 0n), v, Nat.sub(_, Nat.mul(32n, 1n+j)))) == _ : Nat}
112 %Equal.sym(Nat, Nat.sub(j, 0n), j, N.sub_zero(j)) : {len(A2.hp_go(_, v, Nat.sub(Nat.add(65n, Nat.add(m, r)), Nat.mul(32n, 1n+j)))) == Nat.add(65n, Nat.add(m, r)) : Nat}
113 %Equal.sym(Nat, Nat.mul(32n, 1n+j), Nat.mul(1n+j, 32n), NA.mul_comm(32n, 1n+j)) : {len(A2.hp_go(j, v, Nat.sub(Nat.add(65n, Nat.add(m, r)), _))) == Nat.add(65n, Nat.add(m, r)) : Nat}
114 %Equal.sym(Nat, Nat.sub(Nat.add(33n, Nat.add(m, r)), m), Nat.add(33n, r), sub_cancel(33n, m, r)) : {len(A2.hp_go(j, v, _)) == Nat.add(65n, Nat.add(m, r)) : Nat}
115 %Equal.sym(Nat, len(A2.hp_go(j, v, Nat.add(33n, r))), Nat.add(Nat.mul(1n+j, 32n), Nat.add(33n, r)), hp_go_len(j, v, Nat.add(33n, r), hv, N.lt_succ_le(r, 31n, hr))) : {_ == Nat.add(65n, Nat.add(m, r)) : Nat}
116 %Equal.sym(Nat, Nat.add(m, Nat.add(33n, r)), Nat.add(33n, Nat.add(m, r)), NA.add_swap(m, 33n, r)) : {Nat.add(32n, _) == Nat.add(65n, Nat.add(m, r)) : Nat}
117 {==}
118
119def pick_len(+tl: Nat, +x: List<&2, U32>, +short: Bool, +es: {Nat.is_le(tl, 64n) == short : Bool}) -> {len(A2.hp_pick(tl, x, short)) == tl : Nat}:
120 match short:
121 case True{}:
122 hash_len(tl, x, es)
123 case False{}:
124 +a = Nat.add(tl, 31n)
125 +ht = N.lt_succ_le_succ(64n, tl, N.not_le_lt(tl, 64n, es))
126 long_len(tl, Nat.div(a, 32n), Nat.mod(a, 32n), H.hash(64n, x), NR.dm_eq(31n, a), NR.dm_lt(31n, a), ht, hash_len(64n, x, {==}))
127
128
129def hprime_len(+tl: Nat, +a: List<&2, U32>) -> {len(A2.hprime(tl, a)) == tl : Nat}:
130 pick_len(tl, A2.cat(A2.le32(tl), a), Nat.is_le(tl, 64n), {==})
131
132
133
134def ok_append(+a: List<&2, U32>, +b: List<&2, U32>, +ha: {PP.ok(a) == True{} : Bool}, +hb: {PP.ok(b) == True{} : Bool}) -> {PP.ok(List.append(&2, U32, a, b)) == True{} : Bool}:
135 match a:
136 case Nil{}:
137 hb
138 case +x <> +r:
139 L.and_intro(Nat.is_lt(U32.to_nat(x), 256n), PP.ok(List.append(&2, U32, r, b)), PP.ok_head(x, r, ha), ok_append(r, b, PP.ok_tail(x, r, ha), hb))
140
141def ok_take(+xs: List<&2, U32>, +k: Nat, +h: {PP.ok(xs) == True{} : Bool}) -> {PP.ok(List.take(&2, U32, xs, k)) == True{} : Bool}:
142 match xs k:
143 case Nil{} _:
144 {==}
145 case Con{x, r} 0n:
146 {==}
147 case Con{+x, +r} 1n+ +j:
148 L.and_intro(Nat.is_lt(U32.to_nat(x), 256n), PP.ok(List.take(&2, U32, r, j)), PP.ok_head(x, r, h), ok_take(r, j, PP.ok_tail(x, r, h)))
149
150def and255(+w: U32) -> {Nat.is_lt(U32.to_nat(U32.and(w, 255)), 256n) == True{} : Bool}:
151 N.le_lt_succ(U32.to_nat(U32.and(w, 255)), 255n, HH.and_le32(w, 255))
152
153def top8(+w: U32) -> {Nat.is_lt(U32.to_nat(U32.shrn(w, 24n)), 256n) == True{} : Bool}:
154 +f = LW.fits_high(24n, 8n, LW.v(w), LW.vb(w))
155 %Equal.sym(Nat, SR.v(U32.shrn(w, 24n)), C.high(24n, SR.v(w)), SR.shrn_high(w, 24n)) : {Nat.is_lt(_, 256n) == True{} : Bool}
156 WW.lt_of_fits(8n, C.high(24n, LW.v(w)), f)
157
158def le_ok(+w: U32) -> {PP.ok(H.le(w)) == True{} : Bool}:
159 L.and_intro(Nat.is_lt(U32.to_nat(U32.and(w, 255)), 256n), PP.ok([U32.and(U32.shrn(w, 8n), 255), U32.and(U32.shrn(w, 16n), 255), U32.shrn(w, 24n)]), and255(w),
160 L.and_intro(Nat.is_lt(U32.to_nat(U32.and(U32.shrn(w, 8n), 255)), 256n), PP.ok([U32.and(U32.shrn(w, 16n), 255), U32.shrn(w, 24n)]), and255(U32.shrn(w, 8n)),
161 L.and_intro(Nat.is_lt(U32.to_nat(U32.and(U32.shrn(w, 16n), 255)), 256n), PP.ok([U32.shrn(w, 24n)]), and255(U32.shrn(w, 16n)),
162 L.and_intro(Nat.is_lt(U32.to_nat(U32.shrn(w, 24n)), 256n), True{}, top8(w), {==}))))
163
164def lane_ok(+l: T.Lane) -> {PP.ok(H.lane_bytes(l)) == True{} : Bool}:
165 match l:
166 case T.W{+a, +b}:
167 ok_append(H.le(a), H.le(b), le_ok(a), le_ok(b))
168
169def chain_ok(+h: T.Chain) -> {PP.ok(H.chain_bytes(h)) == True{} : Bool}:
170 match h:
171 case T.H{+h0, +h1, +h2, +h3, +h4, +h5, +h6, +h7}:
172 ok_append(H.lane_bytes(h0), List.concat(&2, U32, [H.lane_bytes(h1), H.lane_bytes(h2), H.lane_bytes(h3), H.lane_bytes(h4), H.lane_bytes(h5), H.lane_bytes(h6), H.lane_bytes(h7)]), lane_ok(h0),
173 ok_append(H.lane_bytes(h1), List.concat(&2, U32, [H.lane_bytes(h2), H.lane_bytes(h3), H.lane_bytes(h4), H.lane_bytes(h5), H.lane_bytes(h6), H.lane_bytes(h7)]), lane_ok(h1),
174 ok_append(H.lane_bytes(h2), List.concat(&2, U32, [H.lane_bytes(h3), H.lane_bytes(h4), H.lane_bytes(h5), H.lane_bytes(h6), H.lane_bytes(h7)]), lane_ok(h2),
175 ok_append(H.lane_bytes(h3), List.concat(&2, U32, [H.lane_bytes(h4), H.lane_bytes(h5), H.lane_bytes(h6), H.lane_bytes(h7)]), lane_ok(h3),
176 ok_append(H.lane_bytes(h4), List.concat(&2, U32, [H.lane_bytes(h5), H.lane_bytes(h6), H.lane_bytes(h7)]), lane_ok(h4),
177 ok_append(H.lane_bytes(h5), List.concat(&2, U32, [H.lane_bytes(h6), H.lane_bytes(h7)]), lane_ok(h5),
178 ok_append(H.lane_bytes(h6), List.concat(&2, U32, [H.lane_bytes(h7)]), lane_ok(h6),
179 ok_append(H.lane_bytes(h7), Nil{}, lane_ok(h7), {==}))))))))
180
181def hash_ok(+nn: Nat, +bs: List<&2, U32>) -> {PP.ok(H.hash(nn, bs)) == True{} : Bool}:
182 +c = H.chain(nn, H.pack(bs), List.length(&2, U32, bs))
183 ok_take(H.chain_bytes(c), nn, chain_ok(c))
184
185def hp_go_ok(+n: Nat, +v: List<&2, U32>, +last: Nat, +hv: {PP.ok(v) == True{} : Bool}) -> {PP.ok(A2.hp_go(n, v, last)) == True{} : Bool}:
186 match n v:
187 case _ Nil{}:
188 {==}
189 case 0n +x <> +r:
190 ok_append(List.take(&2, U32, x <> r, 32n), H.hash(last, x <> r), ok_take(x <> r, 32n, hv), hash_ok(last, x <> r))
191 case 1n+ +p +x <> +r:
192 ok_append(List.take(&2, U32, x <> r, 32n), A2.hp_go(p, H.hash(64n, x <> r), last), ok_take(x <> r, 32n, hv), hp_go_ok(p, H.hash(64n, x <> r), last, hash_ok(64n, x <> r)))
193
194def pick_ok(+tl: Nat, +x: List<&2, U32>, +short: Bool) -> {PP.ok(A2.hp_pick(tl, x, short)) == True{} : Bool}:
195 match short:
196 case True{}:
197 hash_ok(tl, x)
198 case False{}:
199 +r = Nat.sub(Nat.div(Nat.add(tl, 31n), 32n), 2n)
200 hp_go_ok(Nat.sub(r, 1n), H.hash(64n, x), Nat.sub(tl, Nat.mul(32n, r)), hash_ok(64n, x))
201
202
203def hprime_ok(+tl: Nat, +a: List<&2, U32>) -> {PP.ok(A2.hprime(tl, a)) == True{} : Bool}:
204 pick_ok(tl, A2.cat(A2.le32(tl), a), Nat.is_le(tl, 64n))
205
206
207
208def tag_of(+ok: Bool, +pw: List<&2, U32>, +salt: List<&2, U32>, +t: Nat, +m: Nat, +p: Nat, +tl: Nat, +tag: List<&2, U32>, +e: {A2.checked(ok, pw, salt, Nil{}, Nil{}, t, m, p, tl) == Some{tag} : Maybe<&2, List<&2, U32>>}) -> {A2.run(pw, salt, Nil{}, Nil{}, t, m, p, tl) == tag : List<&2, U32>}:
209 match ok:
210 case True{}:
211 L.some_inj(List<&2, U32>, A2.run(pw, salt, Nil{}, Nil{}, t, m, p, tl), tag, e)
212 case False{}:
213 Empty.absurd({A2.run(pw, salt, Nil{}, Nil{}, t, m, p, tl) == tag : List<&2, U32>}, L.none_some(List<&2, U32>, tag, e))
214
215
216def run_arg(+pw: List<&2, U32>, +salt: List<&2, U32>, +t: Nat, +m: Nat, +p: Nat, +tl: Nat) -> List<&2, U32>:
217 +mm = A2.blocks(m, p)
218 +q = Nat.div(mm, p)
219 A2.block_bytes(A2.final_go(Nat.sub(p, 1n), 0n, q, G.zero(), M.get(Nat.sub(q, 1n), A2.passes_go(t, 0n, p, q, Nat.div(q, 4n), mm, t, A2.init_go(p, 0n, q, A2.h0(p, tl, m, t, pw, salt, Nil{}, Nil{}), M.new(M.levels(mm)))))))
220
221def run_ok(+pw: List<&2, U32>, +salt: List<&2, U32>, +t: Nat, +m: Nat, +p: Nat, +tl: Nat) -> {PP.ok(A2.run(pw, salt, Nil{}, Nil{}, t, m, p, tl)) == True{} : Bool}:
222 hprime_ok(tl, run_arg(pw, salt, t, m, p, tl))
223
224def run_len(+pw: List<&2, U32>, +salt: List<&2, U32>, +t: Nat, +m: Nat, +p: Nat, +tl: Nat) -> {len(A2.run(pw, salt, Nil{}, Nil{}, t, m, p, tl)) == tl : Nat}:
225 hprime_len(tl, run_arg(pw, salt, t, m, p, tl))
226
227def tag_ok(+pw: List<&2, U32>, +salt: List<&2, U32>, +t: Nat, +m: Nat, +p: Nat, +tl: Nat, +tag: List<&2, U32>, +er: {A2.argon2id(pw, salt, Nil{}, Nil{}, t, m, p, tl) == Some{tag} : Maybe<&2, List<&2, U32>>}) -> {PP.ok(tag) == True{} : Bool}:
228 +ok = Bool.and(A2.valid(pw, salt, Nil{}, Nil{}, t, m, p, tl), A2.fits(m, p))
229 L.subst(List<&2, U32>, z => {PP.ok(z) == True{} : Bool}, A2.run(pw, salt, Nil{}, Nil{}, t, m, p, tl), tag, tag_of(ok, pw, salt, t, m, p, tl, tag, er), run_ok(pw, salt, t, m, p, tl))
230
231def tag_len(+pw: List<&2, U32>, +salt: List<&2, U32>, +t: Nat, +m: Nat, +p: Nat, +tl: Nat, +tag: List<&2, U32>, +er: {A2.argon2id(pw, salt, Nil{}, Nil{}, t, m, p, tl) == Some{tag} : Maybe<&2, List<&2, U32>>}) -> {len(tag) == tl : Nat}:
232 +ok = Bool.and(A2.valid(pw, salt, Nil{}, Nil{}, t, m, p, tl), A2.fits(m, p))
233 L.subst(List<&2, U32>, z => {len(z) == tl : Nat}, A2.run(pw, salt, Nil{}, Nil{}, t, m, p, tl), tag, tag_of(ok, pw, salt, t, m, p, tl, tag, er), run_len(pw, salt, t, m, p, tl))
234
235
236
237def diff_self(+a: List<&2, U32>, +acc: U32, +h: {U32.is_eq(acc, 0) == True{} : Bool}) -> {U32.is_eq(Subtle.diff(a, a, acc), 0) == True{} : Bool}:
238 match a:
239 case Nil{}:
240 h
241 case +x <> +xs:
242 +acc2 = U32.or(acc, U32.xor(x, x))
243 +e = Equal.trans(Bool, U32.is_eq(acc2, 0), Bool.and(U32.is_eq(acc, 0), U32.is_eq(U32.xor(x, x), 0)), True{}, SW.u32_or_zero(acc, U32.xor(x, x)),
244 L.and_intro(U32.is_eq(acc, 0), U32.is_eq(U32.xor(x, x), 0), h, Equal.trans(Bool, U32.is_eq(U32.xor(x, x), 0), U32.is_eq(x, x), True{}, SW.u32_xor_zero(x, x), SW.u32_refl(x))))
245 diff_self(xs, acc2, e)
246
247
248def eq_refl(+a: List<&2, U32>) -> {Subtle.eq(a, a) == True{} : Bool}:
249 L.and_intro(Nat.is_eq(List.length(&2, U32, a), List.length(&2, U32, a)), U32.is_eq(Subtle.diff(a, a, 0), 0), N.is_eq_refl(List.length(&2, U32, a)), diff_self(a, 0, {==}))
250
251
252
253
254def verified(+pw: List<&2, U32>, r: Maybe<&2, String>) -> Bool:
255 match r:
256 case None{}:
257 True{}
258 case Some{s}:
259 PW.verify_password(pw, s)
260
261
262def fresh(r: Maybe<&2, String>, +params: PW.Params) -> Bool:
263 match r:
264 case None{}:
265 False{}
266 case Some{s}:
267 PW.needs_rehash(s, params)
268
269def enc_ver(+pw: List<&2, U32>, +salt: List<&2, U32>, +m: Nat, +t: Nat, +p: Nat, +tl: Nat, +r: Maybe<&2, List<&2, U32>>, +er: {A2.argon2id(pw, salt, Nil{}, Nil{}, t, m, p, tl) == r : Maybe<&2, List<&2, U32>>}, +hs: {PP.ok(salt) == True{} : Bool}) -> {verified(pw, PW.encode(m, t, p, salt, r)) == True{} : Bool}:
270 match r:
271 case None{}:
272 {==}
273 case Some{+h}:
274 %Equal.sym(Maybe<&2, PH.Phc>, PH.parse(PH.format(PH.Phc{m, t, p, salt, h})), Some{PH.Phc{m, t, p, salt, h}}, PP.parse_format(m, t, p, salt, h, hs, tag_ok(pw, salt, t, m, p, tl, h, er))) : {PW.verify_parsed(pw, _) == True{} : Bool}
275 %Equal.sym(Nat, len(h), tl, tag_len(pw, salt, t, m, p, tl, h, er)) : {PW.verify_tag(h, A2.argon2id(pw, salt, Nil{}, Nil{}, t, m, p, _)) == True{} : Bool}
276 %Equal.sym(Maybe<&2, List<&2, U32>>, A2.argon2id(pw, salt, Nil{}, Nil{}, t, m, p, tl), Some{h}, er) : {PW.verify_tag(h, _) == True{} : Bool}
277 eq_refl(h)
278
279
280
281def verify_hash(+pw: List<&2, U32>, +salt: List<&2, U32>, +params: PW.Params, +hs: {PP.ok(salt) == True{} : Bool}) -> {verified(pw, PW.hash_password(pw, salt, params)) == True{} : Bool}:
282 match params:
283 case PW.Params{+m, +t, +p, +tl, +sl}:
284 enc_ver(pw, salt, m, t, p, tl, A2.argon2id(pw, salt, Nil{}, Nil{}, t, m, p, tl), {==}, hs)
285
286def enc_fresh(+pw: List<&2, U32>, +salt: List<&2, U32>, +m: Nat, +t: Nat, +p: Nat, +tl: Nat, +sl: Nat, +r: Maybe<&2, List<&2, U32>>, +er: {A2.argon2id(pw, salt, Nil{}, Nil{}, t, m, p, tl) == r : Maybe<&2, List<&2, U32>>}, +hs: {PP.ok(salt) == True{} : Bool}, +hl: {len(salt) == sl : Nat}) -> {fresh(PW.encode(m, t, p, salt, r), PW.Params{m, t, p, tl, sl}) == False{} : Bool}:
287 match r:
288 case None{}:
289 {==}
290 case Some{+h}:
291 %Equal.sym(Maybe<&2, PH.Phc>, PH.parse(PH.format(PH.Phc{m, t, p, salt, h})), Some{PH.Phc{m, t, p, salt, h}}, PP.parse_format(m, t, p, salt, h, hs, tag_ok(pw, salt, t, m, p, tl, h, er))) : {PW.rehash_parsed(_, PW.Params{m, t, p, tl, sl}) == False{} : Bool}
292 %Equal.sym(Nat, len(h), tl, tag_len(pw, salt, t, m, p, tl, h, er)) : {Bool.not(Bool.and(Bool.and(Nat.is_eq(m, m), Bool.and(Nat.is_eq(t, t), Nat.is_eq(p, p))), Bool.and(Nat.is_eq(_, tl), Nat.is_eq(PW.len(salt), sl)))) == False{} : Bool}
293 %Equal.sym(Nat, len(salt), sl, hl) : {Bool.not(Bool.and(Bool.and(Nat.is_eq(m, m), Bool.and(Nat.is_eq(t, t), Nat.is_eq(p, p))), Bool.and(Nat.is_eq(tl, tl), Nat.is_eq(_, sl)))) == False{} : Bool}
294 %Equal.sym(Bool, Nat.is_eq(m, m), True{}, N.is_eq_refl(m)) : {Bool.not(Bool.and(Bool.and(_, Bool.and(Nat.is_eq(t, t), Nat.is_eq(p, p))), Bool.and(Nat.is_eq(tl, tl), Nat.is_eq(sl, sl)))) == False{} : Bool}
295 %Equal.sym(Bool, Nat.is_eq(t, t), True{}, N.is_eq_refl(t)) : {Bool.not(Bool.and(Bool.and(True{}, Bool.and(_, Nat.is_eq(p, p))), Bool.and(Nat.is_eq(tl, tl), Nat.is_eq(sl, sl)))) == False{} : Bool}
296 %Equal.sym(Bool, Nat.is_eq(p, p), True{}, N.is_eq_refl(p)) : {Bool.not(Bool.and(Bool.and(True{}, Bool.and(True{}, _)), Bool.and(Nat.is_eq(tl, tl), Nat.is_eq(sl, sl)))) == False{} : Bool}
297 %Equal.sym(Bool, Nat.is_eq(tl, tl), True{}, N.is_eq_refl(tl)) : {Bool.not(Bool.and(Bool.and(True{}, Bool.and(True{}, True{})), Bool.and(_, Nat.is_eq(sl, sl)))) == False{} : Bool}
298 %Equal.sym(Bool, Nat.is_eq(sl, sl), True{}, N.is_eq_refl(sl)) : {Bool.not(Bool.and(Bool.and(True{}, Bool.and(True{}, True{})), Bool.and(True{}, _))) == False{} : Bool}
299 {==}
300
301
302
303
304def rehash_hash(+pw: List<&2, U32>, +salt: List<&2, U32>, +params: PW.Params, +hs: {PP.ok(salt) == True{} : Bool}, +hl: {len(salt) == PW.salt_len(params) : Nat}) -> {fresh(PW.hash_password(pw, salt, params), params) == False{} : Bool}:
305 match params:
306 case PW.Params{+m, +t, +p, +tl, +sl}:
307 enc_fresh(pw, salt, m, t, p, tl, sl, A2.argon2id(pw, salt, Nil{}, Nil{}, t, m, p, tl), {==}, hs, hl)