def step_eq

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/fill.bend:175

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/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/types.bend as T
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/index.bend as IX

175# One block of a segment.
176def step_eq(+d: Nat, +mem: List<&2, A.Block>, +r: Nat, +l: Nat, +s: Nat, +idx: Nat, +p: Nat, +q: Nat, +sl: Nat, +cur: Nat, +indep: Bool, +addr: A.Block, +pb: 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}, +hq: {q == Nat.mul(4n, sl) : Nat}, +hp: {Nat.is_le(1n, p) == True{} : Bool}, +hsl: {Nat.is_le(1n, sl) == True{} : Bool}, +hl: {Nat.is_lt(l, p) == True{} : Bool}, +hs: {Nat.is_lt(s, 4n) == True{} : Bool}, +hi: {Nat.is_lt(idx, sl) == True{} : Bool}, +hcur: {Nat.is_lt(cur, SC.length(A.Block, mem)) == True{} : Bool}) -> {I.step(r, l, s, idx, p, q, sl, cur, indep, addr, (AR.thaw(U32, MEM.mt(d, mem)), pb)) == AR.thaw(U32, MEM.mt(d, SA.step(r, l, s, idx, p, q, sl, cur, indep, addr, pb, mem))) : Array<U32>}:
177  +r0 = Nat.is_eq(r, 0n)
178  +pri = I.pick(indep, addr, idx, pb)
179  +prs = SA.pick(indep, addr, idx, pb)
180  +n = SC.length(A.Block, mem)
181  +hq1 = q_pos(q, sl, hq, hsl)
182  +hqn = L.subst(Nat, z => {Nat.is_le(q, z) == True{} : Bool}, Nat.mul(p, q), n, Equal.sym(Nat, n, Nat.mul(p, q), hlen), le_mul_left(p, q, hp))
183  +ei = Equal.trans(Nat, ixi(r0, s, l, idx, p, q, sl, pri), ixi(r0, s, l, idx, p, q, sl, prs), ixs(r0, s, l, idx, p, q, sl, prs),
184    Equal.cong(T.Lane, Nat, z => ixi(r0, s, l, idx, p, q, sl, z), pri, prs, IX.pick_eq(indep, addr, idx, pb)),
185    ix_eq(d, n, r0, s, l, idx, p, q, sl, prs, hd, hq, hs, hi, hqn, hc))
186  +ix = ixs(r0, s, l, idx, p, q, sl, prs)
187  +hix = L.subst(Nat, z => {Nat.is_lt(ix, z) == True{} : Bool}, Nat.mul(p, q), n, Equal.sym(Nat, n, Nat.mul(p, q), hlen), ix_lt(r0, s, l, idx, p, q, sl, prs, hl, hp, hq1))
188  %Equal.sym(Nat, ixi(r0, s, l, idx, p, q, sl, pri), ix, ei) : {I.with_ref(r0, cur, pb, M.get(_, AR.thaw(U32, MEM.mt(d, mem)))) == AR.thaw(U32, MEM.mt(d, SA.store(r0, cur, pb, SA.get(mem, ix), mem))) : Array<U32>}
189  %Equal.sym(Array<U32> & A.Block, M.get(ix, AR.thaw(U32, MEM.mt(d, mem))), (AR.thaw(U32, MEM.mt(d, mem)), SA.get(mem, ix)), MEM.get_block(d, mem, ix, hd, hc, hix)) : {I.with_ref(r0, cur, pb, _) == AR.thaw(U32, MEM.mt(d, SA.store(r0, cur, pb, SA.get(mem, ix), mem))) : Array<U32>}
190  store_eq(d, mem, r0, cur, pb, SA.get(mem, ix), hd, hc, hcur)