proofs/crypto/argon2/top.bend
bend-collections-laws-crypto@1.0.0.0 · 232 lines · 28 definitions
1import Base
2import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC
3import bend-collections-laws-crypto@1.0.0.0/proofs/lib/array.bend as AR
4import bend-collections-laws-crypto@1.0.0.0/proofs/lib/list.bend as LL
5import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
6import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
7import bend-collections-laws-crypto@1.0.0.0/proofs/lib/arith.bend as AR2
8import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
9import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR
10import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/types.bend as T
11import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/types.bend as A
12import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/blamka.bend as G
13import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/memory.bend as M
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/argon2/blamka.bend as SG
16import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend as SA
17import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/blamka.bend as BL
18import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend as MEM
19import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/hash.bend as HS
20import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/fill.bend as F
21import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/run.bend as R
22
23
24
25
26
27
28def X(+m: Nat, +p: Nat) -> Nat:
29 Nat.div(m, Nat.mul(4n, p))
30
31def mm_swap(+p: Nat, +x: Nat) -> {Nat.mul(Nat.mul(4n, p), x) == Nat.mul(Nat.mul(4n, x), p) : Nat}:
32 Equal.trans(Nat, Nat.mul(Nat.mul(4n, p), x), Nat.mul(4n, Nat.mul(p, x)), Nat.mul(Nat.mul(4n, x), p),
33 NA.mul_assoc(4n, p, x),
34 Equal.trans(Nat, Nat.mul(4n, Nat.mul(p, x)), Nat.mul(4n, Nat.mul(x, p)), Nat.mul(Nat.mul(4n, x), p),
35 Equal.cong(Nat, Nat, z => Nat.mul(4n, z), Nat.mul(p, x), Nat.mul(x, p), NA.mul_comm(p, x)),
36 Equal.sym(Nat, Nat.mul(Nat.mul(4n, x), p), Nat.mul(4n, Nat.mul(x, p)), NA.mul_assoc(4n, x, p))))
37
38
39def div_exact(+y: Nat, +d: Nat, +hd: {Nat.is_le(1n, d) == True{} : Bool}) -> {Nat.div(Nat.mul(y, d), d) == y : Nat}:
40 match d:
41 case 0n:
42 Empty.absurd({Nat.div(Nat.mul(y, 0n), 0n) == y : Nat}, L.false_true(hd))
43 case 1n+ +b:
44 %NA.add_zero(Nat.mul(y, 1n+b)) : {Nat.div(_, 1n+b) == y : Nat}
45 NR.div_of(y, b, 0n, {==})
46
47
48def q_eq(+m: Nat, +p: Nat, +hp: {Nat.is_le(1n, p) == True{} : Bool}) -> {Nat.div(I.blocks(m, p), p) == Nat.mul(4n, X(m, p)) : Nat}:
49 %Equal.sym(Nat, Nat.mul(Nat.mul(4n, p), X(m, p)), Nat.mul(Nat.mul(4n, X(m, p)), p), mm_swap(p, X(m, p))) : {Nat.div(_, p) == Nat.mul(4n, X(m, p)) : Nat}
50 div_exact(Nat.mul(4n, X(m, p)), p, hp)
51
52
53def div4(+x: Nat) -> {Nat.div(Nat.mul(4n, x), 4n) == x : Nat}:
54 %Equal.sym(Nat, Nat.mul(4n, x), Nat.mul(x, 4n), NA.mul_comm(4n, x)) : {Nat.div(_, 4n) == x : Nat}
55 div_exact(x, 4n, {==})
56
57def sl_eq(+m: Nat, +p: Nat, +hp: {Nat.is_le(1n, p) == True{} : Bool}) -> {Nat.div(Nat.div(I.blocks(m, p), p), 4n) == X(m, p) : Nat}:
58 %Equal.sym(Nat, Nat.div(I.blocks(m, p), p), Nat.mul(4n, X(m, p)), q_eq(m, p, hp)) : {Nat.div(_, 4n) == X(m, p) : Nat}
59 div4(X(m, p))
60
61
62def hq(+m: Nat, +p: Nat, +hp: {Nat.is_le(1n, p) == True{} : Bool}) -> {Nat.div(I.blocks(m, p), p) == Nat.mul(4n, Nat.div(Nat.div(I.blocks(m, p), p), 4n)) : Nat}:
63 %Equal.sym(Nat, Nat.div(Nat.div(I.blocks(m, p), p), 4n), X(m, p), sl_eq(m, p, hp)) : {Nat.div(I.blocks(m, p), p) == Nat.mul(4n, _) : Nat}
64 q_eq(m, p, hp)
65
66
67def hlen(+m: Nat, +p: Nat, +hp: {Nat.is_le(1n, p) == True{} : Bool}) -> {I.blocks(m, p) == Nat.mul(p, Nat.div(I.blocks(m, p), p)) : Nat}:
68 %Equal.sym(Nat, Nat.div(I.blocks(m, p), p), Nat.mul(4n, X(m, p)), q_eq(m, p, hp)) : {I.blocks(m, p) == Nat.mul(p, _) : Nat}
69 Equal.trans(Nat, Nat.mul(Nat.mul(4n, p), X(m, p)), Nat.mul(Nat.mul(p, 4n), X(m, p)), Nat.mul(p, Nat.mul(4n, X(m, p))),
70 Equal.cong(Nat, Nat, z => Nat.mul(z, X(m, p)), Nat.mul(4n, p), Nat.mul(p, 4n), NA.mul_comm(4n, p)),
71 NA.mul_assoc(p, 4n, X(m, p)))
72
73
74def x_ge2(+m: Nat, +p: Nat, +hp: {Nat.is_le(1n, p) == True{} : Bool}, +h8: {Nat.is_le(Nat.mul(8n, p), m) == True{} : Bool}) -> {Nat.is_le(2n, X(m, p)) == True{} : Bool}:
75 match p:
76 case 0n:
77 Empty.absurd({Nat.is_le(2n, X(m, 0n)) == True{} : Bool}, L.false_true(hp))
78 case 1n+ +b:
79 +e = NR.le_div(Nat.add(b, Nat.mul(3n, 1n+b)), 2n, m)
80 +h2 = L.subst(Nat, z => {Nat.is_le(z, m) == True{} : Bool}, Nat.mul(8n, 1n+b), Nat.mul(2n, Nat.mul(4n, 1n+b)), NA.mul_assoc(2n, 4n, 1n+b), h8)
81 Equal.trans(Bool, Nat.is_le(2n, X(m, 1n+b)), Nat.is_le(Nat.mul(2n, Nat.mul(4n, 1n+b)), m), True{}, e, h2)
82
83
84
85def pw_eq(+k: Nat) -> {M.pw(k) == SC.pow2(k) : Nat}:
86 match k:
87 case 0n:
88 {==}
89 case 1n+ +j:
90 Equal.cong(Nat, Nat, z => Nat.double(z), M.pw(j), SC.pow2(j), pw_eq(j))
91
92def d8(+b: Nat) -> {Nat.mul(b, 256n) == Nat.double(Nat.double(Nat.double(Nat.double(Nat.double(Nat.double(Nat.double(Nat.double(b)))))))) : Nat}:
93 match b:
94 case 0n:
95 {==}
96 case 1n+ +c:
97 %Equal.sym(Nat, Nat.mul(c, 256n), Nat.double(Nat.double(Nat.double(Nat.double(Nat.double(Nat.double(Nat.double(Nat.double(c)))))))), d8(c)) : {Nat.add(256n, _) == Nat.double(Nat.double(Nat.double(Nat.double(Nat.double(Nat.double(Nat.double(Nat.double(1n+c)))))))) : Nat}
98 {==}
99
100
101def levels_go_ok(+f: Nat, +n: Nat, +k: Nat, +done: Bool, +hd: {done == Nat.is_le(n, M.pw(k)) : Bool}, +hr: {Nat.is_lt(M.levels_go(f, n, k, done), Nat.add(k, f)) == True{} : Bool}) -> {Nat.is_le(n, M.pw(M.levels_go(f, n, k, done))) == True{} : Bool}:
102 match f done:
103 case _ True{}:
104 Equal.sym(Bool, True{}, Nat.is_le(n, M.pw(k)), hd)
105 case 0n False{}:
106 Empty.absurd({Nat.is_le(n, M.pw(k)) == True{} : Bool}, L.false_true(Equal.trans(Bool, False{}, Nat.is_lt(k, Nat.add(k, 0n)), True{}, Equal.trans(Bool, False{}, Nat.is_lt(k, k), Nat.is_lt(k, Nat.add(k, 0n)), Equal.sym(Bool, Nat.is_lt(k, k), False{}, N.lt_irrefl(k)), Equal.cong(Nat, Bool, z => Nat.is_lt(k, z), k, Nat.add(k, 0n), Equal.sym(Nat, Nat.add(k, 0n), k, N.add_zero(k)))), hr)))
107 case 1n+ +g False{}:
108 +r = M.levels_go(g, n, 1n+k, Nat.is_le(n, M.pw(1n+k)))
109 levels_go_ok(g, n, 1n+k, Nat.is_le(n, M.pw(1n+k)), {==}, L.subst(Nat, z => {Nat.is_lt(r, z) == True{} : Bool}, Nat.add(k, 1n+g), 1n+Nat.add(k, g), N.add_succ(k, g), hr))
110
111def levels_ok(+n: Nat, +h: {Nat.is_le(M.levels(n), 23n) == True{} : Bool}) -> {Nat.is_le(n, SC.pow2(M.levels(n))) == True{} : Bool}:
112 +hr = N.le_lt_trans(M.levels(n), 23n, 32n, h, {==})
113 L.subst(Nat, z => {Nat.is_le(n, z) == True{} : Bool}, M.pw(M.levels(n)), SC.pow2(M.levels(n)), pw_eq(M.levels(n)), levels_go_ok(32n, n, 0n, Nat.is_le(n, 1n), {==}, hr))
114
115
116def cap(+n: Nat, +h: {Nat.is_le(M.levels(n), 23n) == True{} : Bool}) -> {Nat.is_le(Nat.mul(SC.length(A.Block, SC.replicate(A.Block, n, SG.zero())), 256n), SC.pow2(Nat.add(8n, M.levels(n)))) == True{} : Bool}:
117 +k = M.levels(n)
118 %Equal.sym(Nat, SC.length(A.Block, SC.replicate(A.Block, n, SG.zero())), n, LL.length_replicate(A.Block, n, SG.zero())) : {Nat.is_le(Nat.mul(_, 256n), SC.pow2(Nat.add(8n, k))) == True{} : Bool}
119 %d8(SC.pow2(k)) : {Nat.is_le(Nat.mul(n, 256n), _) == True{} : Bool}
120 AR2.mul_le(n, SC.pow2(k), 256n, levels_ok(n, h))
121
122def depth_lt(+n: Nat, +h: {Nat.is_le(M.levels(n), 23n) == True{} : Bool}) -> {Nat.is_lt(Nat.add(8n, M.levels(n)), 32n) == True{} : Bool}:
123 N.le_lt_succ(M.levels(n), 23n, h)
124
125
126
127def q2(+q: Nat, +sl: Nat, +hq: {q == Nat.mul(4n, sl) : Nat}, +hsl: {Nat.is_le(2n, sl) == True{} : Bool}) -> {Nat.is_le(2n, q) == True{} : Bool}:
128 L.subst(Nat, z => {Nat.is_le(2n, z) == True{} : Bool}, Nat.mul(4n, sl), q, Equal.sym(Nat, q, Nat.mul(4n, sl), hq), N.le_trans(2n, sl, Nat.mul(4n, sl), hsl, N.le_add_right(sl, Nat.mul(3n, sl))))
129
130def fill_eq(+d: Nat, +t: Nat, +p: Nat, +q: Nat, +sl: Nat, +mm: Nat, +hh: List<&2, U32>, +z: List<&2, A.Block>, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hc: {Nat.is_le(Nat.mul(SC.length(A.Block, z), 256n), SC.pow2(d)) == True{} : Bool}, +hlen: {SC.length(A.Block, z) == Nat.mul(p, q) : Nat}, +hq: {q == Nat.mul(4n, sl) : Nat}, +hp: {Nat.is_le(1n, p) == True{} : Bool}, +hsl: {Nat.is_le(2n, sl) == True{} : Bool}) -> {I.passes_go(t, 0n, p, q, sl, mm, t, I.init_go(p, 0n, q, hh, AR.thaw(U32, MEM.mt(d, z)))) == AR.thaw(U32, MEM.mt(d, SA.passes_go(t, 0n, p, q, sl, mm, t, SA.init_go(p, 0n, q, hh, z)))) : Array<U32>}:
131 +m1 = SA.init_go(p, 0n, q, hh, z)
132 +e = R.init_len(p, 0n, q, hh, z)
133 %Equal.sym(Array<U32>, I.init_go(p, 0n, q, hh, AR.thaw(U32, MEM.mt(d, z))), AR.thaw(U32, MEM.mt(d, m1)), R.init_eq(d, p, 0n, p, q, hh, z, hd, hc, hlen, q2(q, sl, hq, hsl), N.le_refl(p))) : {I.passes_go(t, 0n, p, q, sl, mm, t, _) == AR.thaw(U32, MEM.mt(d, SA.passes_go(t, 0n, p, q, sl, mm, t, m1))) : Array<U32>}
134 F.passes_eq(d, t, 0n, p, q, sl, mm, t, m1, hd, F.keep_c(d, z, m1, e, hc), F.keep_len(z, m1, Nat.mul(p, q), e, hlen), hq, hp, hsl)
135
136
137
138def tail_i(+tl: Nat, +p: Nat, +q: Nat, a: Array<U32>) -> List<&2, U32>:
139 I.hprime(tl, I.block_bytes(I.final_go(Nat.sub(p, 1n), 0n, q, G.zero(), M.get(Nat.sub(q, 1n), a))))
140
141def tail_s(+tl: Nat, +p: Nat, +q: Nat, +mem: List<&2, A.Block>) -> List<&2, U32>:
142 SA.hprime(tl, SA.block_bytes(SA.final_go(Nat.sub(p, 1n), 0n, q, SG.zero(), SA.get(mem, Nat.sub(q, 1n)), mem)))
143
144def tail_eq(+d: Nat, +tl: Nat, +p: Nat, +q: Nat, +mem: List<&2, A.Block>, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hc: {Nat.is_le(Nat.mul(SC.length(A.Block, mem), 256n), SC.pow2(d)) == True{} : Bool}, +hlen: {SC.length(A.Block, mem) == Nat.mul(p, q) : Nat}, +hp: {Nat.is_le(1n, p) == True{} : Bool}, +hq1: {Nat.is_le(1n, q) == True{} : Bool}) -> {tail_i(tl, p, q, AR.thaw(U32, MEM.mt(d, mem))) == tail_s(tl, p, q, mem) : List<&2, U32>}:
145 +b = SA.get(mem, Nat.sub(q, 1n))
146 +c = SA.final_go(Nat.sub(p, 1n), 0n, q, SG.zero(), b, mem)
147 +hb = F.lt_len(Nat.sub(q, 1n), mem, p, q, hlen, N.lt_le_trans(Nat.sub(q, 1n), q, Nat.mul(p, q), F.sub1_lt(q, hq1), F.le_mul_left(p, q, hp)))
148 -ar = AR.thaw(U32, MEM.mt(d, mem))
149 %Equal.sym(Array<U32> & A.Block, M.get(Nat.sub(q, 1n), ar), (ar, b), MEM.get_block(d, mem, Nat.sub(q, 1n), hd, hc, hb)) : {I.hprime(tl, I.block_bytes(I.final_go(Nat.sub(p, 1n), 0n, q, G.zero(), _))) == tail_s(tl, p, q, mem) : List<&2, U32>}
150 %Equal.sym(A.Block, G.zero(), SG.zero(), BL.zero_correct()) : {I.hprime(tl, I.block_bytes(I.final_go(Nat.sub(p, 1n), 0n, q, _, (ar, b)))) == tail_s(tl, p, q, mem) : List<&2, U32>}
151 %Equal.sym(A.Block, I.final_go(Nat.sub(p, 1n), 0n, q, SG.zero(), (ar, b)), c, R.final_eq(d, Nat.sub(p, 1n), 0n, p, q, SG.zero(), b, mem, hd, hc, hlen, hq1, F.sub1_lt(p, hp))) : {I.hprime(tl, I.block_bytes(_)) == tail_s(tl, p, q, mem) : List<&2, U32>}
152 Equal.trans(List<&2, U32>, I.hprime(tl, I.block_bytes(c)), I.hprime(tl, SA.block_bytes(c)), SA.hprime(tl, SA.block_bytes(c)),
153 Equal.cong(List<&2, U32>, List<&2, U32>, x => I.hprime(tl, x), I.block_bytes(c), SA.block_bytes(c), HS.block_bytes_eq(c)),
154 HS.hprime_eq(tl, SA.block_bytes(c)))
155
156
157
158def valid_p1(+pw: List<&2, U32>, +salt: List<&2, U32>, +key: List<&2, U32>, +ad: List<&2, U32>, +t: Nat, +m: Nat, +p: Nat, +tl: Nat, +hv: {SA.valid(pw, salt, key, ad, t, m, p, tl) == True{} : Bool}) -> {Nat.is_le(1n, p) == True{} : Bool}:
159 +a1 = Bool.and(Nat.is_le(1n, p), Nat.is_le(p, 16777215n))
160 +a2 = Bool.and(Nat.is_le(4n, tl), Nat.is_le(tl, 4294967295n))
161 +b1 = Bool.and(Nat.is_le(Nat.mul(8n, p), m), Nat.is_le(m, 4294967295n))
162 +b2 = Bool.and(Nat.is_le(1n, t), Nat.is_le(t, 4294967295n))
163 +cs = Bool.and(Bool.and(Nat.is_le(8n, SA.len(salt)), Nat.is_le(SA.len(salt), 4294967295n)), Bool.and(Nat.is_le(SA.len(pw), 4294967295n), Bool.and(Nat.is_le(SA.len(key), 4294967295n), Nat.is_le(SA.len(ad), 4294967295n))))
164 +ha = L.and_left(Bool.and(a1, a2), Bool.and(Bool.and(b1, b2), cs), hv)
165 +hb = L.and_right(Bool.and(a1, a2), Bool.and(Bool.and(b1, b2), cs), hv)
166 L.and_left(Nat.is_le(1n, p), Nat.is_le(p, 16777215n), L.and_left(a1, a2, ha))
167
168def valid_p8(+pw: List<&2, U32>, +salt: List<&2, U32>, +key: List<&2, U32>, +ad: List<&2, U32>, +t: Nat, +m: Nat, +p: Nat, +tl: Nat, +hv: {SA.valid(pw, salt, key, ad, t, m, p, tl) == True{} : Bool}) -> {Nat.is_le(Nat.mul(8n, p), m) == True{} : Bool}:
169 +a1 = Bool.and(Nat.is_le(1n, p), Nat.is_le(p, 16777215n))
170 +a2 = Bool.and(Nat.is_le(4n, tl), Nat.is_le(tl, 4294967295n))
171 +b1 = Bool.and(Nat.is_le(Nat.mul(8n, p), m), Nat.is_le(m, 4294967295n))
172 +b2 = Bool.and(Nat.is_le(1n, t), Nat.is_le(t, 4294967295n))
173 +cs = Bool.and(Bool.and(Nat.is_le(8n, SA.len(salt)), Nat.is_le(SA.len(salt), 4294967295n)), Bool.and(Nat.is_le(SA.len(pw), 4294967295n), Bool.and(Nat.is_le(SA.len(key), 4294967295n), Nat.is_le(SA.len(ad), 4294967295n))))
174 +ha = L.and_left(Bool.and(a1, a2), Bool.and(Bool.and(b1, b2), cs), hv)
175 +hb = L.and_right(Bool.and(a1, a2), Bool.and(Bool.and(b1, b2), cs), hv)
176 L.and_left(Nat.is_le(Nat.mul(8n, p), m), Nat.is_le(m, 4294967295n), L.and_left(b1, b2, L.and_left(Bool.and(b1, b2), cs, hb)))
177
178def run_body(+pw: List<&2, U32>, +salt: List<&2, U32>, +key: List<&2, U32>, +ad: List<&2, U32>, +t: Nat, +m: Nat, +p: Nat, +tl: Nat, +hp: {Nat.is_le(1n, p) == True{} : Bool}, +h8: {Nat.is_le(Nat.mul(8n, p), m) == True{} : Bool}, +hf: {I.fits(m, p) == True{} : Bool}) -> {I.run(pw, salt, key, ad, t, m, p, tl) == SA.run(pw, salt, key, ad, t, m, p, tl) : List<&2, U32>}:
179 +mm = I.blocks(m, p)
180 +q = Nat.div(mm, p)
181 +sl = Nat.div(q, 4n)
182 +k = M.levels(mm)
183 +d = Nat.add(8n, k)
184 +z = SC.replicate(A.Block, mm, SG.zero())
185 +hi = I.h0(p, tl, m, t, pw, salt, key, ad)
186 +hs = SA.h0(p, tl, m, t, pw, salt, key, ad)
187 +hd = depth_lt(mm, hf)
188 +hc = cap(mm, hf)
189 +hlz = LL.length_replicate(A.Block, mm, SG.zero())
190 +hc0 = L.subst(Nat, x => {Nat.is_le(Nat.mul(x, 256n), SC.pow2(d)) == True{} : Bool}, SC.length(A.Block, z), mm, hlz, hc)
191 +hlen0 = Equal.trans(Nat, SC.length(A.Block, z), mm, Nat.mul(p, q), hlz, hlen(m, p, hp))
192 +hq0 = hq(m, p, hp)
193 +hsl = L.subst(Nat, x => {Nat.is_le(2n, x) == True{} : Bool}, X(m, p), sl, Equal.sym(Nat, sl, X(m, p), sl_eq(m, p, hp)), x_ge2(m, p, hp, h8))
194 +hq1 = N.le_trans(1n, 2n, q, {==}, q2(q, sl, hq0, hsl))
195 +m2 = SA.passes_go(t, 0n, p, q, sl, mm, t, SA.init_go(p, 0n, q, hs, z))
196 +e2 = Equal.trans(Nat, SC.length(A.Block, m2), SC.length(A.Block, SA.init_go(p, 0n, q, hs, z)), SC.length(A.Block, z), F.passes_len(t, 0n, p, q, sl, mm, t, SA.init_go(p, 0n, q, hs, z)), R.init_len(p, 0n, q, hs, z))
197 -goal = SA.run(pw, salt, key, ad, t, m, p, tl)
198 %Equal.sym(Array<U32>, Array.new(U32, d, 0), AR.thaw(U32, MEM.mt(d, z)), MEM.new_mem(d, mm, hc0)) : {tail_i(tl, p, q, I.passes_go(t, 0n, p, q, sl, mm, t, I.init_go(p, 0n, q, hi, _))) == goal : List<&2, U32>}
199 %Equal.sym(List<&2, U32>, hi, hs, HS.h0_eq(p, tl, m, t, pw, salt, key, ad)) : {tail_i(tl, p, q, I.passes_go(t, 0n, p, q, sl, mm, t, I.init_go(p, 0n, q, _, AR.thaw(U32, MEM.mt(d, z))))) == goal : List<&2, U32>}
200 %Equal.sym(Array<U32>, I.passes_go(t, 0n, p, q, sl, mm, t, I.init_go(p, 0n, q, hs, AR.thaw(U32, MEM.mt(d, z)))), AR.thaw(U32, MEM.mt(d, m2)), fill_eq(d, t, p, q, sl, mm, hs, z, hd, hc, hlen0, hq0, hp, hsl)) : {tail_i(tl, p, q, _) == goal : List<&2, U32>}
201 tail_eq(d, tl, p, q, m2, hd, F.keep_c(d, z, m2, e2, hc), F.keep_len(z, m2, Nat.mul(p, q), e2, hlen0), hp, hq1)
202
203def run_eq(+pw: List<&2, U32>, +salt: List<&2, U32>, +key: List<&2, U32>, +ad: List<&2, U32>, +t: Nat, +m: Nat, +p: Nat, +tl: Nat, +hv: {SA.valid(pw, salt, key, ad, t, m, p, tl) == True{} : Bool}, +hf: {I.fits(m, p) == True{} : Bool}) -> {I.run(pw, salt, key, ad, t, m, p, tl) == SA.run(pw, salt, key, ad, t, m, p, tl) : List<&2, U32>}:
204 run_body(pw, salt, key, ad, t, m, p, tl, valid_p1(pw, salt, key, ad, t, m, p, tl, hv), valid_p8(pw, salt, key, ad, t, m, p, tl, hv), hf)
205
206def checked_eq(+ok: Bool, +pw: List<&2, U32>, +salt: List<&2, U32>, +key: List<&2, U32>, +ad: List<&2, U32>, +t: Nat, +m: Nat, +p: Nat, +tl: Nat, +e: {SA.valid(pw, salt, key, ad, t, m, p, tl) == ok : Bool}, +hf: {I.fits(m, p) == True{} : Bool}) -> {I.checked(ok, pw, salt, key, ad, t, m, p, tl) == SA.checked(ok, pw, salt, key, ad, t, m, p, tl) : Maybe<&2, List<&2, U32>>}:
207 match ok:
208 case False{}:
209 {==}
210 case True{}:
211 Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, x => Some{x}, I.run(pw, salt, key, ad, t, m, p, tl), SA.run(pw, salt, key, ad, t, m, p, tl), run_eq(pw, salt, key, ad, t, m, p, tl, e, hf))
212
213def valid_eq(+pw: List<&2, U32>, +salt: List<&2, U32>, +key: List<&2, U32>, +ad: List<&2, U32>, +t: Nat, +m: Nat, +p: Nat, +tl: Nat) -> {I.valid(pw, salt, key, ad, t, m, p, tl) == SA.valid(pw, salt, key, ad, t, m, p, tl) : Bool}:
214 {==}
215
216def and_true(+b: Bool) -> {Bool.and(b, True{}) == b : Bool}:
217 match b:
218 case True{}:
219 {==}
220 case False{}:
221 {==}
222
223
224
225
226def argon2id_correct(+pw: List<&2, U32>, +salt: List<&2, U32>, +key: List<&2, U32>, +ad: List<&2, U32>, +t: Nat, +m: Nat, +p: Nat, +tl: Nat, +hf: {I.fits(m, p) == True{} : Bool}) -> {I.argon2id(pw, salt, key, ad, t, m, p, tl) == SA.argon2id(pw, salt, key, ad, t, m, p, tl) : Maybe<&2, List<&2, U32>>}:
227 +v = SA.valid(pw, salt, key, ad, t, m, p, tl)
228 -goal = SA.argon2id(pw, salt, key, ad, t, m, p, tl)
229 %Equal.sym(Bool, I.fits(m, p), True{}, hf) : {I.checked(Bool.and(I.valid(pw, salt, key, ad, t, m, p, tl), _), pw, salt, key, ad, t, m, p, tl) == goal : Maybe<&2, List<&2, U32>>}
230 %Equal.sym(Bool, I.valid(pw, salt, key, ad, t, m, p, tl), v, valid_eq(pw, salt, key, ad, t, m, p, tl)) : {I.checked(Bool.and(_, True{}), pw, salt, key, ad, t, m, p, tl) == goal : Maybe<&2, List<&2, U32>>}
231 %Equal.sym(Bool, Bool.and(v, True{}), v, and_true(v)) : {I.checked(_, pw, salt, key, ad, t, m, p, tl) == goal : Maybe<&2, List<&2, U32>>}
232 checked_eq(v, pw, salt, key, ad, t, m, p, tl, {==}, hf)