Top.run_body: def of bend-collections-laws-crypto@1.0.0.0 Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/top.bend as Top Lines 178-201 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/top.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/top.bend&start_line=178&end_line=201 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 def 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>}: +mm = I.blocks(m, p) +q = Nat.div(mm, p) +sl = Nat.div(q, 4n) +k = M.levels(mm) +d = Nat.add(8n, k) +z = SC.replicate(A.Block, mm, SG.zero()) +hi = I.h0(p, tl, m, t, pw, salt, key, ad) +hs = SA.h0(p, tl, m, t, pw, salt, key, ad) +hd = depth_lt(mm, hf) +hc = cap(mm, hf) +hlz = LL.length_replicate(A.Block, mm, SG.zero()) +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) +hlen0 = Equal.trans(Nat, SC.length(A.Block, z), mm, Nat.mul(p, q), hlz, hlen(m, p, hp)) +hq0 = hq(m, p, hp) +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)) +hq1 = N.le_trans(1n, 2n, q, {==}, q2(q, sl, hq0, hsl)) +m2 = SA.passes_go(t, 0n, p, q, sl, mm, t, SA.init_go(p, 0n, q, hs, z)) +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)) -goal = SA.run(pw, salt, key, ad, t, m, p, tl) %Equal.sym(Array, 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>} %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>} %Equal.sym(Array, 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>} 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) Uses (50): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.new https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.div https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/fill.bend&name=keep_c https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/fill.bend&name=keep_len https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/fill.bend&name=passes_len https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/hash.bend&name=h0_eq https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend&name=mt https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend&name=new_mem https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/run.bend&name=init_len https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/top.bend&name=X https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/top.bend&name=cap https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/top.bend&name=depth_lt https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/top.bend&name=fill_eq https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/top.bend&name=hlen https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/top.bend&name=hq https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/top.bend&name=q2 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/top.bend&name=sl_eq https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/top.bend&name=tail_eq https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/top.bend&name=tail_i https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/top.bend&name=x_ge2 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/array.bend&name=thaw https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/list.bend&name=length_replicate https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend&name=subst https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=le_trans https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend&name=h0 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend&name=init_go https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend&name=passes_go https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend&name=run https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/blamka.bend&name=zero https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=length https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=pow2 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=replicate https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/argon2.bend&name=blocks https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/argon2.bend&name=fits https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/argon2.bend&name=h0 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/argon2.bend&name=init_go https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/argon2.bend&name=passes_go https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/argon2.bend&name=run https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/memory.bend&name=levels https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/types.bend&name=Block