law addresses_correct

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

import Base
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

74# The address blocks of the data-independent segments.
75law addresses_correct:
76  for +r: Nat
77  for +l: Nat
78  for +s: Nat
79  for +mm: Nat
80  for +t: Nat
81  for +ctr: Nat
82  {I.addresses(r, l, s, mm, t, ctr) == SA.addresses(r, l, s, mm, t, ctr) : A.Block}