def set_block

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

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

568# Writing block b of the memory of mem.
569def set_block(+d: Nat, +mem: List<&2, A.Block>, +b: Nat, +v: 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}, +hb: {Nat.is_lt(b, SC.length(A.Block, mem)) == True{} : Bool}) -> {M.set(b, v, AR.thaw(U32, mt(d, mem))) == AR.thaw(U32, mt(d, SA.set(mem, b, v))) : Array<U32>}:
570  +hi = L.subst(Nat, z => {Nat.is_le(Nat.add(Nat.mul(b, 256n), z), SC.pow2(d)) == True{} : Bool}, 256n, SC.length(U32, SB.words(v)), Equal.sym(Nat, SC.length(U32, SB.words(v)), 256n, words_len(v)), N.le_trans(Nat.add(Nat.mul(b, 256n), 256n), Nat.mul(SC.length(A.Block, mem), 256n), SC.pow2(d), mul_lt(b, SC.length(A.Block, mem), hb), hc))
571  Equal.trans(Array<U32>, M.wr(SB.words(v), Nat.mul(b, 256n), AR.thaw(U32, tree(d, W(d, mem)))), AR.thaw(U32, tree(d, splice(SB.words(v), Nat.mul(b, 256n), W(d, mem)))), AR.thaw(U32, mt(d, SA.set(mem, b, v))),
572    wr_words(d, SB.words(v), Nat.mul(b, 256n), W(d, mem), hd, W_len(d, mem, hc), hi),
573    Equal.cong(List<&2, U32>, Array<U32>, z => AR.thaw(U32, tree(d, z)), splice(SB.words(v), Nat.mul(b, 256n), W(d, mem)), W(d, SA.set(mem, b, v)), W_splice(d, mem, b, v, hb)))