def tail_eq

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/top.bend:144

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/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/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/hash.bend as HS
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/fill.bend as F
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/run.bend as R

144def tail_eq(+d: Nat, +tl: Nat, +p: Nat, +q: 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}, +hp: {Nat.is_le(1n, p) == True{} : Bool}, +hq1: {Nat.is_le(1n, q) == True{} : Bool}) -> {tail_i(tl, p, q, AR.thaw(U32, MEM.mt(d, mem))) == tail_s(tl, p, q, mem) : List<&2, U32>}:
145  +b = SA.get(mem, Nat.sub(q, 1n))
146  +c = SA.final_go(Nat.sub(p, 1n), 0n, q, SG.zero(), b, mem)
147  +hb = F.lt_len(Nat.sub(q, 1n), mem, p, q, hlen, N.lt_le_trans(Nat.sub(q, 1n), q, Nat.mul(p, q), F.sub1_lt(q, hq1), F.le_mul_left(p, q, hp)))
148  -ar = AR.thaw(U32, MEM.mt(d, mem))
149  %Equal.sym(Array<U32> & A.Block, M.get(Nat.sub(q, 1n), ar), (ar, b), MEM.get_block(d, mem, Nat.sub(q, 1n), hd, hc, hb)) : {I.hprime(tl, I.block_bytes(I.final_go(Nat.sub(p, 1n), 0n, q, G.zero(), _))) == tail_s(tl, p, q, mem) : List<&2, U32>}
150  %Equal.sym(A.Block, G.zero(), SG.zero(), BL.zero_correct()) : {I.hprime(tl, I.block_bytes(I.final_go(Nat.sub(p, 1n), 0n, q, _, (ar, b)))) == tail_s(tl, p, q, mem) : List<&2, U32>}
151  %Equal.sym(A.Block, I.final_go(Nat.sub(p, 1n), 0n, q, SG.zero(), (ar, b)), c, R.final_eq(d, Nat.sub(p, 1n), 0n, p, q, SG.zero(), b, mem, hd, hc, hlen, hq1, F.sub1_lt(p, hp))) : {I.hprime(tl, I.block_bytes(_)) == tail_s(tl, p, q, mem) : List<&2, U32>}
152  Equal.trans(List<&2, U32>, I.hprime(tl, I.block_bytes(c)), I.hprime(tl, SA.block_bytes(c)), SA.hprime(tl, SA.block_bytes(c)),
153    Equal.cong(List<&2, U32>, List<&2, U32>, x => I.hprime(tl, x), I.block_bytes(c), SA.block_bytes(c), HS.block_bytes_eq(c)),
154    HS.hprime_eq(tl, SA.block_bytes(c)))