BACAP unlinkability at Ed25519

Stated directly at the concrete types: going through Blindable makes Lean unfold ZMod ℓ on a 253-bit literal.

theorem Cryptlib.Protocols.BACAP.Ed25519Unlinkability.ed25519_unlinkable [Fintype Primitives.Sign.Ed25519Blinded.Scalar] [SampleableType Primitives.Sign.Ed25519Blinded.Scalar] [DecidableEq Primitives.Sign.Ed25519Blinded.PubBytes] (s : Primitives.Sign.Ed25519Blinded.Scalar) (hs : s ≠ 0) {target : Primitives.Sign.Ed25519Blinded.PubBytes} (ht : target ∈ Set.range (Primitives.Sign.Ed25519Blinded.blindPub (Primitives.Sign.Ed25519Blinded.publicKey s))) : Pr[= true | do let f ← $ᵗ Primitives.Sign.Ed25519Blinded.Scalar pure (decide (Primitives.Sign.Ed25519Blinded.blindPub (Primitives.Sign.Ed25519Blinded.publicKey s) f = target))] = (↑(Fintype.card Primitives.Sign.Ed25519Blinded.Scalar))⁻¹

For a nonzero root secret s, a uniform blinding factor yields any box ID in the image with probability 1/ℓ (Echomix §4.3).