def flat_slice

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/memory.bend:376

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

376# The 256 words of block b of the flattened blocks.
377def flat_slice(+mem: List<&2, A.Block>, +b: Nat, +hb: {Nat.is_lt(b, SC.length(A.Block, mem)) == True{} : Bool}) -> {slice(flat(mem), Nat.mul(b, 256n), 256n) == SB.words(SA.get(mem, b)) : List<&2, U32>}:
378  match mem b:
379    case Nil{} _:
380      Empty.absurd({slice(Nil{}, Nat.mul(b, 256n), 256n) == SB.words(SA.get(Nil{}, b)) : List<&2, U32>}, N.lt_zero_absurd(b, hb))
381    case +x <> +rest 0n:
382      +e1 = drop_zero(SC.append(U32, SB.words(x), flat(rest)))
383      +e2 = LL.sc_take_append_left(U32, SB.words(x), flat(rest), 256n, N.eq_le(256n, SC.length(U32, SB.words(x)), Equal.sym(Nat, SC.length(U32, SB.words(x)), 256n, words_len(x))))
384      +e3 = take_all(SB.words(x), 256n, words_len(x))
385      Equal.trans(List<&2, U32>, SC.take(U32, SC.drop(U32, SC.append(U32, SB.words(x), flat(rest)), 0n), 256n), SC.take(U32, SC.append(U32, SB.words(x), flat(rest)), 256n), SB.words(x),
386        Equal.cong(List<&2, U32>, List<&2, U32>, z => SC.take(U32, z, 256n), SC.drop(U32, SC.append(U32, SB.words(x), flat(rest)), 0n), SC.append(U32, SB.words(x), flat(rest)), e1),
387        Equal.trans(List<&2, U32>, SC.take(U32, SC.append(U32, SB.words(x), flat(rest)), 256n), SC.take(U32, SB.words(x), 256n), SB.words(x), e2, e3))
388    case +x <> +rest 1n+ +c:
389      Equal.trans(List<&2, U32>, SC.take(U32, SC.drop(U32, SC.append(U32, SB.words(x), flat(rest)), Nat.add(256n, Nat.mul(c, 256n))), 256n), slice(flat(rest), Nat.mul(c, 256n), 256n), SB.words(SA.get(rest, c)),
390        Equal.cong(List<&2, U32>, List<&2, U32>, z => SC.take(U32, z, 256n), SC.drop(U32, SC.append(U32, SB.words(x), flat(rest)), Nat.add(256n, Nat.mul(c, 256n))), SC.drop(U32, flat(rest), Nat.mul(c, 256n)), drop_append_add(SB.words(x), flat(rest), 256n, Nat.mul(c, 256n), words_len(x))),
391        flat_slice(rest, c, hb))