Memory.slice_W: def of bend-collections-laws-crypto@1.0.0.0 Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend as Memory Lines 412-425 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend&start_line=412&end_line=425 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/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/sub.bend as SB import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend as SA def slice_W(+d: Nat, +mem: List<&2, A.Block>, +b: Nat, +hb: {Nat.is_lt(b, SC.length(A.Block, mem)) == True{} : Bool}) -> {slice(W(d, mem), Nat.mul(b, 256n), 256n) == SB.words(SA.get(mem, b)) : List<&2, U32>}: +F = flat(mem) +P = pad(d, SC.length(A.Block, mem)) +base = Nat.mul(b, 256n) +hn = mul_lt(b, SC.length(A.Block, mem), hb) +hfl = Equal.sym(Nat, SC.length(U32, F), Nat.mul(SC.length(A.Block, mem), 256n), flat_len(mem)) +hle = N.le_trans(base, Nat.add(base, 256n), SC.length(U32, F), N.le_add_right(base, 256n), L.subst(Nat, z => {Nat.is_le(Nat.add(base, 256n), z) == True{} : Bool}, Nat.mul(SC.length(A.Block, mem), 256n), SC.length(U32, F), hfl, hn)) +h256 = L.subst(Nat, z => {Nat.is_le(256n, z) == True{} : Bool}, Nat.sub(SC.length(U32, F), base), SC.length(U32, SC.drop(U32, F, base)), Equal.sym(Nat, SC.length(U32, SC.drop(U32, F, base)), Nat.sub(SC.length(U32, F), base), length_drop(F, base)), le_sub(base, 256n, SC.length(U32, F), L.subst(Nat, z => {Nat.is_le(Nat.add(base, 256n), z) == True{} : Bool}, Nat.mul(SC.length(A.Block, mem), 256n), SC.length(U32, F), hfl, hn))) Equal.trans(List<&2, U32>, SC.take(U32, SC.drop(U32, SC.append(U32, F, P), base), 256n), SC.take(U32, SC.drop(U32, F, base), 256n), SB.words(SA.get(mem, b)), Equal.trans(List<&2, U32>, SC.take(U32, SC.drop(U32, SC.append(U32, F, P), base), 256n), SC.take(U32, SC.append(U32, SC.drop(U32, F, base), P), 256n), SC.take(U32, SC.drop(U32, F, base), 256n), Equal.cong(List<&2, U32>, List<&2, U32>, z => SC.take(U32, z, 256n), SC.drop(U32, SC.append(U32, F, P), base), SC.append(U32, SC.drop(U32, F, base), P), drop_append_le(F, P, base, hle)), LL.sc_take_append_left(U32, SC.drop(U32, F, base), P, 256n, h256)), flat_slice(mem, b, hb)) Uses (33): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong 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.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=Nat.sub 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/memory.bend&name=W https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend&name=drop_append_le https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend&name=flat https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend&name=flat_len https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend&name=flat_slice https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend&name=le_sub https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend&name=length_drop https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend&name=mul_lt https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend&name=pad https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend&name=slice https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/list.bend&name=sc_take_append_left 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_add_right 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=get https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=append https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=drop 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=take https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/sub.bend&name=words https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/types.bend&name=Block