def flat_splice

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

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/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
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

543def flat_splice(+mem: List<&2, A.Block>, +b: Nat, +v: A.Block, +hb: {Nat.is_lt(b, SC.length(A.Block, mem)) == True{} : Bool}) -> {splice(SB.words(v), Nat.mul(b, 256n), flat(mem)) == flat(SA.set(mem, b, v)) : List<&2, U32>}:
544  match mem b:
545    case Nil{} _:
546      Empty.absurd({splice(SB.words(v), Nat.mul(b, 256n), Nil{}) == flat(SA.set(Nil{}, b, v)) : List<&2, U32>}, N.lt_zero_absurd(b, hb))
547    case +x <> +rest 0n:
548      Equal.trans(List<&2, U32>, splice(SB.words(v), 0n, SC.append(U32, SB.words(x), flat(rest))), SC.append(U32, splice(SB.words(v), 0n, SB.words(x)), flat(rest)), SC.append(U32, SB.words(v), flat(rest)),
549        splice_app_left(SB.words(v), 0n, SB.words(x), flat(rest), L.subst(Nat, z => {Nat.is_le(z, SC.length(U32, SB.words(x))) == True{} : Bool}, SC.length(U32, SB.words(x)), SC.length(U32, SB.words(v)), Equal.trans(Nat, SC.length(U32, SB.words(x)), 256n, SC.length(U32, SB.words(v)), words_len(x), Equal.sym(Nat, SC.length(U32, SB.words(v)), 256n, words_len(v))), N.le_refl(SC.length(U32, SB.words(x))))),
550        Equal.cong(List<&2, U32>, List<&2, U32>, z => SC.append(U32, z, flat(rest)), splice(SB.words(v), 0n, SB.words(x)), SB.words(v), splice_full(x, v)))
551    case +x <> +rest 1n+ +c:
552      Equal.trans(List<&2, U32>, splice(SB.words(v), Nat.add(256n, Nat.mul(c, 256n)), SC.append(U32, SB.words(x), flat(rest))), SC.append(U32, SB.words(x), splice(SB.words(v), Nat.mul(c, 256n), flat(rest))), SC.append(U32, SB.words(x), flat(SA.set(rest, c, v))),
553        splice_app_right(SB.words(v), 256n, Nat.mul(c, 256n), SB.words(x), flat(rest), words_len(x)),
554        Equal.cong(List<&2, U32>, List<&2, U32>, z => SC.append(U32, SB.words(x), z), splice(SB.words(v), Nat.mul(c, 256n), flat(rest)), flat(SA.set(rest, c, v)), flat_splice(rest, c, v, hb)))