def init_len

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/run.bend:34

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

34def init_len(+n: Nat, +l: Nat, +q: Nat, +hh: List<&2, U32>, +mem: List<&2, A.Block>) -> {SC.length(A.Block, SA.init_go(n, l, q, hh, mem)) == SC.length(A.Block, mem) : Nat}:
35  match n:
36    case 0n:
37      {==}
38    case 1n+ +rest:
39      +b0 = SA.block_of(SA.hprime(1024n, SA.cat(hh, SA.cat(SA.le32(0n), SA.le32(l)))))
40      +b1 = SA.block_of(SA.hprime(1024n, SA.cat(hh, SA.cat(SA.le32(1n), SA.le32(l)))))
41      +m1 = SA.set(mem, Nat.mul(l, q), b0)
42      +m2 = SA.set(m1, Nat.add(Nat.mul(l, q), 1n), b1)
43      Equal.trans(Nat, SC.length(A.Block, SA.init_go(rest, Nat.add(l, 1n), q, hh, m2)), SC.length(A.Block, m2), SC.length(A.Block, mem),
44        init_len(rest, Nat.add(l, 1n), q, hh, m2),
45        Equal.trans(Nat, SC.length(A.Block, m2), SC.length(A.Block, m1), SC.length(A.Block, mem), LL.length_update(A.Block, m1, Nat.add(Nat.mul(l, q), 1n), b1), LL.length_update(A.Block, mem, Nat.mul(l, q), b0)))