def lanes_len

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

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

297def lanes_len(+n: Nat, +l: Nat, +r: Nat, +s: Nat, +p: Nat, +q: Nat, +sl: Nat, +mm: Nat, +t: Nat, +mem: List<&2, A.Block>) -> {SC.length(A.Block, SA.lanes_go(n, l, r, s, p, q, sl, mm, t, mem)) == SC.length(A.Block, mem) : Nat}:
298  match n:
299    case 0n:
300      {==}
301    case 1n+ +rest:
302      +m2 = SA.segment(r, s, l, p, q, sl, mm, t, mem)
303      Equal.trans(Nat, SC.length(A.Block, SA.lanes_go(rest, Nat.add(l, 1n), r, s, p, q, sl, mm, t, m2)), SC.length(A.Block, m2), SC.length(A.Block, mem),
304        lanes_len(rest, Nat.add(l, 1n), r, s, p, q, sl, mm, t, m2), segment_len(r, s, l, p, q, sl, mm, t, mem))