def ixi_mid

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

import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/fill.bend as Fill
import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/types.bend as T
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/argon2.bend as I

102# The same after the reference lane, and as the specification computes it.
103def ixi_mid(+r0: Bool, +s: Nat, +l: Nat, +idx: Nat, +q: Nat, +sl: Nat, +pr: T.Lane, +rl: Nat) -> Nat:
104  Nat.add(Nat.mul(rl, q), Nat.mod(Nat.add(I.start(r0, s, sl), I.rel(I.area(I.area_base(r0, s, sl, q), idx, Nat.is_eq(rl, l)), G.lo(pr))), q))

Uses (12)

Used by (2)