def passes_eq

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/fill.bend:352

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

352# Passes r .. r + n - 1.
353def 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<U32>}:
354  match n:
355    case 0n:
356      {==}
357    case 1n+ +rest:
358      +m2 = SA.slices_go(4n, 0n, r, p, q, sl, mm, t, mem)
359      +e = slices_len(4n, 0n, r, p, q, sl, mm, t, mem)
360      %Equal.sym(Array<U32>, 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<U32>}
361      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)