Strict Ed25519 verification and public-key acceptance (rule S1).

This module is the single owner of the Ed25519 point and scalar rules for every Ed25519 surface of the protocol. It is pure: no clock, randomness, process state, or I/O.

Rule S1

verify_strict/3 accepts a signature R || S over a message under a public key A only if all of the following hold, checked in this order before any backend call:

1. the key is exactly 32 bytes and the signature exactly 64 bytes;
2. A and R are canonical encodings: the encoded y is below p = 2^255 - 19, and the sign bit is clear whenever x = 0 (RFC 8032 §5.1.3);
3. neither A nor R is one of the eight small-order encodings (one shared table serves both);
4. S < L, the prime order of the base point (RFC 8032 §5.1.7);
5. the cofactorless equation encode([S]B - [k]A) == R holds byte for byte, computed by the :crypto backend.

Curve membership of A is left to the backend at verification; it rejects off-curve keys. There is no subgroup check at verification: a key with a small torsion component passes S1 if its signature satisfies the cofactorless equation. Hosts close that gap once per key with torsion_free?/1.

Key acceptance

acceptable_public_key?/1 is the check for a key entering any verification input: canonical, not small-order, and on the curve (the RFC 8032 §5.1.3 decoding succeeds).

torsion_free?/1 additionally requires [L]A = O. It costs a full scalar multiplication (about 0.45 ms) and is meant for hosts at key enrollment, trust install, and before any deny-list or revocation comparison; it never runs on the verification path. A canonical, torsion-free key has exactly one encoding per secret, so key equality is identity equality.

A true result proves only that the bytes satisfy the rule. It never selects trusted keys or grants authority.