def final_eq

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/run.bend:79

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/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/fill.bend as F

79# C = B[l][q-1] XOR .. for the lanes l .. l + n (b is B[l][q-1]).
80def final_eq(+d: Nat, +n: Nat, +l: Nat, +p: Nat, +q: Nat, +c: A.Block, +b: A.Block, +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}, +hq1: {Nat.is_le(1n, q) == True{} : Bool}, +hln: {Nat.is_lt(Nat.add(l, n), p) == True{} : Bool}) -> {I.final_go(n, l, q, c, (AR.thaw(U32, MEM.mt(d, mem)), b)) == SA.final_go(n, l, q, c, b, mem) : A.Block}:
81  match n:
82    case 0n:
83      BL.xor_correct(c, b)
84    case 1n+ +rest:
85      +ix = Nat.add(Nat.mul(Nat.add(l, 1n), q), Nat.sub(q, 1n))
86      +hl1 = N.le_lt_trans(Nat.add(l, 1n), Nat.add(l, 1n+rest), p, N.le_trans(Nat.add(l, 1n), Nat.add(Nat.add(l, 1n), rest), Nat.add(l, 1n+rest), N.le_add_right(Nat.add(l, 1n), rest), N.eq_le(Nat.add(Nat.add(l, 1n), rest), Nat.add(l, 1n+rest), MEM.add_one_assoc(l, rest))), hln)
87      +hix = F.lt_len(ix, mem, p, q, hlen, F.lt_mul_add(Nat.add(l, 1n), p, Nat.sub(q, 1n), q, hl1, F.sub1_lt(q, hq1)))
88      +hln2 = L.subst(Nat, z => {Nat.is_lt(z, p) == True{} : Bool}, Nat.add(l, 1n+rest), Nat.add(Nat.add(l, 1n), rest), Equal.sym(Nat, Nat.add(Nat.add(l, 1n), rest), Nat.add(l, 1n+rest), MEM.add_one_assoc(l, rest)), hln)
89      -ar = AR.thaw(U32, MEM.mt(d, mem))
90      -goal = SA.final_go(rest, Nat.add(l, 1n), q, SG.xor(c, b), SA.get(mem, ix), mem)
91      %Equal.sym(Array<U32> & A.Block, M.get(ix, ar), (ar, SA.get(mem, ix)), MEM.get_block(d, mem, ix, hd, hc, hix)) : {I.final_go(rest, Nat.add(l, 1n), q, G.xor(c, b), _) == goal : A.Block}
92      %Equal.sym(A.Block, G.xor(c, b), SG.xor(c, b), BL.xor_correct(c, b)) : {I.final_go(rest, Nat.add(l, 1n), q, _, (ar, SA.get(mem, ix))) == goal : A.Block}
93      final_eq(d, rest, Nat.add(l, 1n), p, q, SG.xor(c, b), SA.get(mem, ix), mem, hd, hc, hlen, hq1, hln2)