def slices_len

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

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/src/crypto/argon2/types.bend as A
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend as SA

323def slices_len(+n: Nat, +s: Nat, +r: Nat, +p: Nat, +q: Nat, +sl: Nat, +mm: Nat, +t: Nat, +mem: List<&2, A.Block>) -> {SC.length(A.Block, SA.slices_go(n, s, r, p, q, sl, mm, t, mem)) == SC.length(A.Block, mem) : Nat}:
324  match n:
325    case 0n:
326      {==}
327    case 1n+ +rest:
328      +m2 = SA.lanes_go(p, 0n, r, s, p, q, sl, mm, t, mem)
329      Equal.trans(Nat, SC.length(A.Block, SA.slices_go(rest, Nat.add(s, 1n), r, p, q, sl, mm, t, m2)), SC.length(A.Block, m2), SC.length(A.Block, mem),
330        slices_len(rest, Nat.add(s, 1n), r, p, q, sl, mm, t, m2), lanes_len(p, 0n, r, s, p, q, sl, mm, t, mem))