def segment_eq

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

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/src/crypto/argon2/types.bend as A
import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/blamka.bend as G
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/blamka.bend as SG
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/blamka.bend as BL
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

282# One segment.
283def segment_eq(+d: Nat, +r: Nat, +s: Nat, +l: Nat, +p: Nat, +q: Nat, +sl: Nat, +mm: Nat, +t: Nat, +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}, +hq: {q == Nat.mul(4n, sl) : Nat}, +hp: {Nat.is_le(1n, p) == True{} : Bool}, +hsl: {Nat.is_le(2n, sl) == True{} : Bool}, +hl: {Nat.is_lt(l, p) == True{} : Bool}, +hs: {Nat.is_lt(s, 4n) == True{} : Bool}) -> {I.segment(r, s, l, p, q, sl, mm, t, AR.thaw(U32, MEM.mt(d, mem))) == AR.thaw(U32, MEM.mt(d, SA.segment(r, s, l, p, q, sl, mm, t, mem))) : Array<U32>}:
284  +r0 = Nat.is_eq(r, 0n)
285  +f = Bool.and(r0, Nat.is_eq(s, 0n))
286  +ind = Bool.and(r0, Nat.is_lt(s, 2n))
287  +sti = I.start_index(f)
288  +sts = SA.start_index(f)
289  +hsl1 = N.le_trans(1n, 2n, sl, {==}, hsl)
290  +hidx = N.eq_le(Nat.add(sts, Nat.sub(sl, sts)), sl, N.sub_add(sl, sts, start_index_le(f, sl, hsl)))
291  -ar = AR.thaw(U32, MEM.mt(d, mem))
292  -goal = AR.thaw(U32, MEM.mt(d, SA.segment(r, s, l, p, q, sl, mm, t, mem)))
293  %Equal.sym(Nat, sti, sts, IX.start_index_eq(f)) : {I.seg_go(Nat.sub(sl, _), _, True{}, G.zero(), ar, r, l, s, p, q, sl, mm, t, ind) == goal : Array<U32>}
294  %Equal.sym(A.Block, G.zero(), SG.zero(), BL.zero_correct()) : {I.seg_go(Nat.sub(sl, sts), sts, True{}, _, ar, r, l, s, p, q, sl, mm, t, ind) == goal : Array<U32>}
295  seg_eq(d, Nat.sub(sl, sts), sts, True{}, SG.zero(), mem, r, l, s, p, q, sl, mm, t, ind, hd, hc, hlen, hq, hp, hsl1, hl, hs, hidx)