def rel_eq

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/index.bend:179

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend as U
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

179# rel: |W| - 1 - (|W| * (J1^2 / 2^32)) / 2^32, for |W| < 2^k with k <= 32.
180def rel_eq(+w: Nat, +j1: U32, +k: Nat, +hk: {Nat.is_le(k, 32n) == True{} : Bool}, +hw: {Nat.is_lt(w, C.pow2(k)) == True{} : Bool}) -> {I.rel(w, j1) == SA.rel(w, j1) : Nat}:
181  +xi = X.hi(X.mul32(j1, j1))
182  +xs = C.high(32n, Nat.mul(U32.to_nat(j1), U32.to_nat(j1)))
183  +ew = U.to_nat_from_nat(w, k, hk, hw)
184  +e1 = hi_mul(U32.from_nat(w), xi)
185  +e2 = Equal.trans(Nat, C.high(32n, Nat.mul(U32.to_nat(U32.from_nat(w)), U32.to_nat(xi))), C.high(32n, Nat.mul(w, U32.to_nat(xi))), C.high(32n, Nat.mul(w, xs)),
186    Equal.cong(Nat, Nat, z => C.high(32n, Nat.mul(z, U32.to_nat(xi))), U32.to_nat(U32.from_nat(w)), w, ew),
187    Equal.cong(Nat, Nat, z => C.high(32n, Nat.mul(w, z)), U32.to_nat(xi), xs, hi_mul(j1, j1)))
188  Equal.cong(Nat, Nat, z => Nat.sub(Nat.sub(w, 1n), z), U32.to_nat(X.hi(X.mul32(U32.from_nat(w), xi))), C.high(32n, Nat.mul(w, xs)), Equal.trans(Nat, U32.to_nat(X.hi(X.mul32(U32.from_nat(w), xi))), C.high(32n, Nat.mul(U32.to_nat(U32.from_nat(w)), U32.to_nat(xi))), C.high(32n, Nat.mul(w, xs)), e1, e2))