def run_body

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/top.bend:178

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/array.bend as AR
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/list.bend as LL
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/types.bend as A
import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/memory.bend as M
import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/argon2.bend as I
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/blamka.bend as SG
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend as SA
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend as MEM
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/hash.bend as HS
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/fill.bend as F
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/run.bend as R

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)