Run.final_eq: def of bend-collections-laws-crypto@1.0.0.0 Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/run.bend as Run Lines 79-93 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/run.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/run.bend&start_line=79&end_line=93 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/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/blamka.bend as G 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/blamka.bend as BL 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/fill.bend as F # C = B[l][q-1] XOR .. for the lanes l .. l + n (b is B[l][q-1]). def final_eq(+d: Nat, +n: Nat, +l: Nat, +p: Nat, +q: Nat, +c: A.Block, +b: A.Block, +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}, +hq1: {Nat.is_le(1n, q) == True{} : Bool}, +hln: {Nat.is_lt(Nat.add(l, n), p) == True{} : Bool}) -> {I.final_go(n, l, q, c, (AR.thaw(U32, MEM.mt(d, mem)), b)) == SA.final_go(n, l, q, c, b, mem) : A.Block}: match n: case 0n: BL.xor_correct(c, b) case 1n+ +rest: +ix = Nat.add(Nat.mul(Nat.add(l, 1n), q), Nat.sub(q, 1n)) +hl1 = N.le_lt_trans(Nat.add(l, 1n), Nat.add(l, 1n+rest), p, N.le_trans(Nat.add(l, 1n), Nat.add(Nat.add(l, 1n), rest), Nat.add(l, 1n+rest), N.le_add_right(Nat.add(l, 1n), rest), N.eq_le(Nat.add(Nat.add(l, 1n), rest), Nat.add(l, 1n+rest), MEM.add_one_assoc(l, rest))), hln) +hix = F.lt_len(ix, mem, p, q, hlen, F.lt_mul_add(Nat.add(l, 1n), p, Nat.sub(q, 1n), q, hl1, F.sub1_lt(q, hq1))) +hln2 = L.subst(Nat, z => {Nat.is_lt(z, p) == True{} : Bool}, Nat.add(l, 1n+rest), Nat.add(Nat.add(l, 1n), rest), Equal.sym(Nat, Nat.add(Nat.add(l, 1n), rest), Nat.add(l, 1n+rest), MEM.add_one_assoc(l, rest)), hln) -ar = AR.thaw(U32, MEM.mt(d, mem)) -goal = SA.final_go(rest, Nat.add(l, 1n), q, SG.xor(c, b), SA.get(mem, ix), mem) %Equal.sym(Array & A.Block, M.get(ix, ar), (ar, SA.get(mem, ix)), MEM.get_block(d, mem, ix, hd, hc, hix)) : {I.final_go(rest, Nat.add(l, 1n), q, G.xor(c, b), _) == goal : A.Block} %Equal.sym(A.Block, G.xor(c, b), SG.xor(c, b), BL.xor_correct(c, b)) : {I.final_go(rest, Nat.add(l, 1n), q, _, (ar, SA.get(mem, ix))) == goal : A.Block} final_eq(d, rest, Nat.add(l, 1n), p, q, SG.xor(c, b), SA.get(mem, ix), mem, hd, hc, hlen, hq1, hln2) Uses (35): 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=Nat.sub https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma 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/blamka.bend&name=xor_correct https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/fill.bend&name=lt_len https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/fill.bend&name=lt_mul_add https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/fill.bend&name=sub1_lt https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend&name=add_one_assoc https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend&name=get_block 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/logic.bend&name=subst https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=eq_le 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_lt_trans 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=final_go 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/crypto/argon2/blamka.bend&name=xor 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=final_go https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/blamka.bend&name=xor https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/memory.bend&name=get https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/types.bend&name=Block