def eq_refl

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

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/src/crypto/subtle.bend as Subtle

247# subtle.eq(a, a) == True (proofs/crypto/subtle proves it too, as Eq.refl).
248def eq_refl(+a: List<&2, U32>) -> {Subtle.eq(a, a) == True{} : Bool}:
249  L.and_intro(Nat.is_eq(List.length(&2, U32, a), List.length(&2, U32, a)), U32.is_eq(Subtle.diff(a, a, 0), 0), N.is_eq_refl(List.length(&2, U32, a)), diff_self(a, 0, {==}))