Index.rel_eq: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/index.bend as Index
Lines 179-188 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/index.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/index.bend&start_line=179&end_line=188

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

# rel: |W| - 1 - (|W| * (J1^2 / 2^32)) / 2^32, for |W| < 2^k with k <= 32.
def 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}:
  +xi = X.hi(X.mul32(j1, j1))
  +xs = C.high(32n, Nat.mul(U32.to_nat(j1), U32.to_nat(j1)))
  +ew = U.to_nat_from_nat(w, k, hk, hw)
  +e1 = hi_mul(U32.from_nat(w), xi)
  +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)),
    Equal.cong(Nat, Nat, z => C.high(32n, Nat.mul(z, U32.to_nat(xi))), U32.to_nat(U32.from_nat(w)), w, ew),
    Equal.cong(Nat, Nat, z => C.high(32n, Nat.mul(w, z)), U32.to_nat(xi), xs, hi_mul(j1, j1)))
  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))

Uses (19):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/index.bend&name=hi_mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend&name=to_nat_from_nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend&name=rel
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=high
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=pow2
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/argon2.bend&name=rel
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend&name=hi
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend&name=mul32