def slices_eq

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

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/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

332# Slices s .. s + n - 1 of a pass.
333def slices_eq(+d: Nat, +n: Nat, +s: Nat, +r: 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}, +hsn: {Nat.is_le(Nat.add(s, n), 4n) == True{} : Bool}) -> {I.slices_go(n, s, r, p, q, sl, mm, t, AR.thaw(U32, MEM.mt(d, mem))) == AR.thaw(U32, MEM.mt(d, SA.slices_go(n, s, r, p, q, sl, mm, t, mem))) : Array<U32>}:
334  match n:
335    case 0n:
336      {==}
337    case 1n+ +rest:
338      +m2 = SA.lanes_go(p, 0n, r, s, p, q, sl, mm, t, mem)
339      +e = lanes_len(p, 0n, r, s, p, q, sl, mm, t, mem)
340      %Equal.sym(Array<U32>, I.lanes_go(p, 0n, r, s, p, q, sl, mm, t, AR.thaw(U32, MEM.mt(d, mem))), AR.thaw(U32, MEM.mt(d, m2)), lanes_eq(d, p, 0n, r, s, p, q, sl, mm, t, mem, hd, hc, hlen, hq, hp, hsl, lt_of_add_succ(s, rest, 4n, hsn), N.le_refl(p))) : {I.slices_go(rest, Nat.add(s, 1n), r, p, q, sl, mm, t, _) == AR.thaw(U32, MEM.mt(d, SA.slices_go(rest, Nat.add(s, 1n), r, p, q, sl, mm, t, m2))) : Array<U32>}
341      slices_eq(d, rest, Nat.add(s, 1n), r, p, q, sl, mm, t, m2, hd, keep_c(d, mem, m2, e, hc), keep_len(mem, m2, Nat.mul(p, q), e, hlen), hq, hp, hsl, le_shift(s, rest, 4n, hsn))