def init_eq

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

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/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/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/argon2.bend as SA
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

53# B[l][0] and B[l][1] for the lanes l .. l + n - 1.
54def init_eq(+d: Nat, +n: Nat, +l: Nat, +p: Nat, +q: Nat, +hh: List<&2, U32>, +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}, +hq2: {Nat.is_le(2n, q) == True{} : Bool}, +hln: {Nat.is_le(Nat.add(l, n), p) == True{} : Bool}) -> {I.init_go(n, l, q, hh, AR.thaw(U32, MEM.mt(d, mem))) == AR.thaw(U32, MEM.mt(d, SA.init_go(n, l, q, hh, mem))) : Array<U32>}:
55  match n:
56    case 0n:
57      {==}
58    case 1n+ +rest:
59      +b0i = I.block_of(I.hprime(1024n, I.cat(hh, I.cat(I.le32(0n), I.le32(l)))))
60      +b1i = I.block_of(I.hprime(1024n, I.cat(hh, I.cat(I.le32(1n), I.le32(l)))))
61      +b0 = SA.block_of(SA.hprime(1024n, SA.cat(hh, SA.cat(SA.le32(0n), SA.le32(l)))))
62      +b1 = SA.block_of(SA.hprime(1024n, SA.cat(hh, SA.cat(SA.le32(1n), SA.le32(l)))))
63      +i0 = Nat.mul(l, q)
64      +i1 = Nat.add(Nat.mul(l, q), 1n)
65      +m1 = SA.set(mem, i0, b0)
66      +m2 = SA.set(m1, i1, b1)
67      +hl = F.lt_of_add_succ(l, rest, p, hln)
68      +e1 = LL.length_update(A.Block, mem, i0, b0)
69      +e2 = Equal.trans(Nat, SC.length(A.Block, m2), SC.length(A.Block, m1), SC.length(A.Block, mem), LL.length_update(A.Block, m1, i1, b1), e1)
70      -goal = AR.thaw(U32, MEM.mt(d, SA.init_go(rest, Nat.add(l, 1n), q, hh, m2)))
71      %Equal.sym(A.Block, b0i, b0, init_block_eq(hh, 0n, l)) : {I.init_go(rest, Nat.add(l, 1n), q, hh, M.set(i1, b1i, M.set(i0, _, AR.thaw(U32, MEM.mt(d, mem))))) == goal : Array<U32>}
72      %Equal.sym(A.Block, b1i, b1, init_block_eq(hh, 1n, l)) : {I.init_go(rest, Nat.add(l, 1n), q, hh, M.set(i1, _, M.set(i0, b0, AR.thaw(U32, MEM.mt(d, mem))))) == goal : Array<U32>}
73      %Equal.sym(Array<U32>, M.set(i0, b0, AR.thaw(U32, MEM.mt(d, mem))), AR.thaw(U32, MEM.mt(d, m1)), MEM.set_block(d, mem, i0, b0, hd, hc, F.lt_len(i0, mem, p, q, hlen, lt_first(l, p, q, hl, hq2)))) : {I.init_go(rest, Nat.add(l, 1n), q, hh, M.set(i1, b1, _)) == goal : Array<U32>}
74      %Equal.sym(Array<U32>, M.set(i1, b1, AR.thaw(U32, MEM.mt(d, m1))), AR.thaw(U32, MEM.mt(d, m2)), MEM.set_block(d, m1, i1, b1, hd, F.keep_c(d, mem, m1, e1, hc), F.lt_len(i1, m1, p, q, F.keep_len(mem, m1, Nat.mul(p, q), e1, hlen), lt_second(l, p, q, hl, hq2)))) : {I.init_go(rest, Nat.add(l, 1n), q, hh, _) == goal : Array<U32>}
75      init_eq(d, rest, Nat.add(l, 1n), p, q, hh, m2, hd, F.keep_c(d, mem, m2, e2, hc), F.keep_len(mem, m2, Nat.mul(p, q), e2, hlen), hq2, F.le_shift(l, rest, p, hln))