5.2. Ed25519🔗

opaque

Jar.Crypto.ed25519Verify (key : Ed25519PublicKey) (message : ByteArray)
  (sig : Ed25519Signature) : Bool
Jar.Crypto.ed25519Verify
  (key : Ed25519PublicKey)
  (message : ByteArray)
  (sig : Ed25519Signature) : Bool

V̄_k⟨m⟩ : Ed25519 signature verification. GP §3.8.2. Returns true iff sig is a valid Ed25519 signature of message m under public key k. Deliberately left abstract — intended to be axiomatically specified or linked via FFI to a concrete cryptographic implementation.

opaque

Jar.Crypto.ed25519Sign (secretKey message : ByteArray) :
  Ed25519Signature
Jar.Crypto.ed25519Sign
  (secretKey message : ByteArray) :
  Ed25519Signature

V̄_k⟨m⟩ : Ed25519 signing (requires secret key knowledge). GP §3.8.2. sign_k(m) ∈ V̄_k⟨m⟩ ⊂ 𝔹_64. Deliberately left abstract — intended to be axiomatically specified or linked via FFI to a concrete cryptographic implementation.