Fill.passes_eq: def of bend-collections-laws-crypto@1.0.0.0 Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/fill.bend as Fill Lines 352-361 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/fill.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/fill.bend&start_line=352&end_line=361 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/nat.bend as N 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/argon2.bend as I 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 # Passes r .. r + n - 1. def passes_eq(+d: Nat, +n: Nat, +r: Nat, +p: Nat, +q: Nat, +sl: Nat, +mm: Nat, +t: 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}, +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(n, r, p, q, sl, mm, t, AR.thaw(U32, MEM.mt(d, mem))) == AR.thaw(U32, MEM.mt(d, SA.passes_go(n, r, p, q, sl, mm, t, mem))) : Array}: match n: case 0n: {==} case 1n+ +rest: +m2 = SA.slices_go(4n, 0n, r, p, q, sl, mm, t, mem) +e = slices_len(4n, 0n, r, p, q, sl, mm, t, mem) %Equal.sym(Array, I.slices_go(4n, 0n, r, p, q, sl, mm, t, AR.thaw(U32, MEM.mt(d, mem))), AR.thaw(U32, MEM.mt(d, m2)), slices_eq(d, 4n, 0n, r, p, q, sl, mm, t, mem, hd, hc, hlen, hq, hp, hsl, N.le_refl(4n))) : {I.passes_go(rest, Nat.add(r, 1n), p, q, sl, mm, t, _) == AR.thaw(U32, MEM.mt(d, SA.passes_go(rest, Nat.add(r, 1n), p, q, sl, mm, t, m2))) : Array} passes_eq(d, rest, Nat.add(r, 1n), p, q, sl, mm, t, m2, hd, keep_c(d, mem, m2, e, hc), keep_len(mem, m2, Nat.mul(p, q), e, hlen), hq, hp, hsl) Uses (24): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array 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=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.is_le https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt 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=slices_eq https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/fill.bend&name=slices_len 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/lib/array.bend&name=thaw https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=le_refl 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=slices_go 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/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=slices_go https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/types.bend&name=Block