law Eq.value
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/subtle/laws.bend as Lawsimport Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/subtle.bend as Subtle
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/subtle.bend as Spec
7# eq returns the reference list equality.
8law Eq.value:
9 for +a: List<&2, U32>
10 for +b: List<&2, U32>
11 {Subtle.eq(a, b) == Spec.equal(a, b) : Bool}
Uses (6)
Used by (6)
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/subtle/laws:Eq.refl
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/subtle/laws:Eq.sound
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead:equal_false
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead:equal_refl
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/gcm:open_checked_ok
- …