std.ed25519: sign and verify, checked against real openssl

Status: built. docs/sha512.md §5 named this as the slice SHA-512 was a prerequisite for and deliberately did not start: field arithmetic std.bignum could not do, curve point operations, and a constant-time posture nothing here provides. All three are answered below — the first two built, the third answered no, honestly, not deferred a second time.

1. What this is for, and what it is not for

lex-os-capsule signs a capability contract with Ed25519 (ed25519-dalek, in Rust) so a consumer can verify what it is installing before trusting it. Porting that runtime onto cancho (docs/crypto.md §1’s own opening move) eventually needs the same primitive reachable from .cho code — a future lex-os-guest written in cancho, not cancho’s own Rust tooling.

This module is not what crates/cancho-vcs uses to seal its attestation chain. That is Rust code sealing a Rust data structure; ed25519-dalek is already the right tool there, the same way lex-os-audit already uses it, and reaching for this module instead would mean trusting hand-rolled, non-constant-time arithmetic for a job an audited crate already does correctly and safely. This module exists for the day a .cho program itself needs to sign or verify — which today means only the port target above, not yet a real consumer in this repository.

Corrected (#209, review finding C-2): this module has a consumer in this repository. packages/x509 (verify.cho) calls ed25519.verify for a certificate signed with Ed25519 (RFC 8410), in the chain path the pure TLS client relies on. That use is verification only, on values an attacker can already see (the issuer’s key, the to-be-signed bytes and the signature), so §6’s missing constant-time execution does not weaken it. Signing (sign) is still not constant time and is not on the TLS path; #290 tracks making it so.

2. Representation: correctness over speed, throughout

Curve25519 field elements are usually packed into a handful of wide limbs (radix 2^25.5 or 2^51) so a multiply’s cross terms fit efficient hardware multiplication with room for lazy carrying. That representation is exactly the kind of carry-chain arithmetic docs/sha512.md §2 already found one real, non-obvious bug in for a simpler operation (a 64-bit rotate). Ed25519’s own arithmetic — field inversion, point addition, scalar multiplication — is sha512.md’s bar raised by orders of magnitude: hundreds of field operations, each one a fresh chance to get a carry-chain detail wrong in a way four vectors might not catch.

Changed by docs/x25519.md (#200): the field arithmetic is no longer what this section describes. X25519 needs a field with no branch on its data, and #200 asked for one copy shared by both curves. So gf_add/gf_sub/gf_mul/gf_invert/gf_pow2523, bn_modpow and the two exponent tables are gone. Points are now std.field25519 elements (16 limbs of 16 bits, TweetNaCl’s representation), a point is a [int] of 64, and scalar multiplication is a cswap ladder. What follows still describes the scalar arithmetic mod L, which kept the bit-serial bignum. Signing and verifying became 31 and 35 times faster (docs/x25519.md §6), and every vector below gives the same bytes.

So this module makes one deliberate trade, everywhere: a “big number” is a little-endian [byte] slice — usually 32 bytes — and every operation on one is bit-serial. bn_reduce_wide reduces a wide value mod a fixed modulus one bit at a time: shift the running remainder left, bring in the next bit, subtract the modulus back out if the remainder reached it. bn_modpow is ordinary left-to-right square-and-multiply, walking every bit of the exponent whether or not it is set. Both are asymptotically worse than a radix-limbed implementation and neither has a carry chain to get subtly wrong — the whole toolkit is compare, add, subtract, shift-by-one, and schoolbook multiply, four operations simple enough that bn_test’s own hand-computed cases (200 * 300 mod 1000, 3^4 mod 7, 5 - 3 mod 7) were enough to catch the one real bug it had (§4).

Field arithmetic (gf_add/gf_sub/gf_mul/gf_invert/gf_pow2523) is this toolkit fixed to the field modulus p = 2^255 - 19. Scalar arithmetic (k*a mod L, r + k*a mod L) is the same toolkit fixed to the group order L instead — one set of primitives, two moduli, rather than a second implementation for the scalar side the way a performance-first design would need.

A point is one 128-byte buffer — extended coordinates (X, Y, Z, T) as four consecutive 32-byte fields, X*Y = T*Z — so a point is a single region parameter to pass around rather than four kept in sync by hand, and p[0..32]/p[32..64]/etc. read a coordinate the same way any other subslice does. point_add is the one unified formula, used for both addition and doubling (point_scalarmult’s own double-and-add), checked independently in Python before any of this was written: repeated doubling-and-adding of the base point by the group order L returns the identity.

3. Constants, derived, not transcribed

p, the group order L, the curve parameter d, a square root of -1 mod p, and the base point B’s own compressed encoding are each a 32-byte static. None were copied from a reference implementation or from memory: d = -121665/121666 mod p, B’s coordinates from y = 4/5 mod p and the curve equation, both computed directly (modular inverse via Python’s pow(x, p-2, p)) and checked before being written down — B is confirmed on the curve, and L * B computed by repeated doubling-and-adding reduces to the identity, the same check §2 already described as this module’s own point-addition proof.

The two literal-syntax findings docs/sha512.md §2 made — a full 64-bit word with its top bit set does not parse, and (1 << 63) - 1 traps rather than producing int::MIN’s low 63 bits — do not recur here: every constant is stored byte by byte (byte_of(0x..) on a [byte], never a 64-bit int literal), so no individual value ever approaches either ceiling.

4. The one real bug, and how it was found

bn_modpow and sign/verify reuse one scratch buffer across many calls — once per bit of an exponent, once per step of a signature. bn_reduce_wide’s first version assumed its output buffer arrived zeroed and left it to the caller, the same contract alloc_slice’s own zero fill gives a fresh buffer. A reused buffer is not fresh: 3^1 mod 7, computed by hand-inlining bn_modpow’s own loop with the actual scratch buffers it uses, returned 1 instead of 3 — correct in isolation (bn_mulmod on freshly-allocated buffers, tested first, gave the right answer every time), wrong the moment the same scratch buffer was asked to hold a second, unrelated reduction without being cleared first.

Fixed by zeroing o at the top of bn_reduce_wide itself, so the function’s own contract no longer depends on which of its callers remembered to clear a buffer before reuse. 3^0 through 3^4 mod 7 (1, 3, 2, 6, 4) and the original three-case hand check both pass after the fix, and every downstream layer built on bn_reduce_wide — field arithmetic, point arithmetic, sign, verify — was re-checked against real openssl output afterward rather than assumed fixed by association.

5. Checked against real openssl, in both directions

Four fresh Ed25519 keypairs, generated with openssl genpkey -algorithm ed25519 and signed with openssl pkeyutl -sign -rawin — over a 1-byte, an 11-byte, a 43-byte and a 512-byte message — each confirmed with openssl pkeyutl -verify before being used as a fixture:

The 512-byte case is the one worth naming: it is verified against a signature sign never touched, over a message longer than one hash block, the strongest check available without a second independent implementation to compare every intermediate value against. tests/accept/ed25519.cho carries the first three; docs/ed25519.md’s own history (this document) is where the fourth, cross-direction check is recorded, since a fixture can only assert what one program computes, not what an external tool already agreed to.

Both backends agree — the_two_backends_agree_on_ed25519 in crates/cancho/tests/conformance/backends.rs.

Added by docs/x25519.md §4.2: two bugs Wycheproof found. None of the vectors above has a signature of the wrong length, and verify trapped on one (it read sig[32..64] unchecked). And an R with x = 0 and the sign bit set was accepted, because RFC 8032 §5.1.3 step 4 was not applied: -0 is 0. Both are fixed, and all 151 cases of Wycheproof’s ed25519_test.json now pass.

Added by docs/hkdf.md §2. None of these messages was long enough to find that sign copied prefix || msg into a 64 KiB arena: a 65,000-byte message trapped. sign and verify now stream their hashes. tests/accept/ed25519_long.cho signs 70,000 bytes, matches OpenSSL’s signature and verifies it.

6. What this module deliberately does not provide

Corrected by docs/x25519.md §3.1, measured with Valgrind. The field arithmetic and the point ladder no longer branch on data. The scalar arithmetic mod L still does: under the ctgrind check, with the seed marked secret, every report from sign is in bn_mulmod, bn_reduce_wide or sign itself, and none is in the field or point code. So signing is still not constant-time, for the reason below, now confined to bn_*.

Not constant-time. Every branch here — bn_sub_into’s borrow, bn_modpow’s bit test, point_unpack’s sign correction — is an ordinary conditional, and an ordinary conditional’s timing can depend on the secret data it branches on. ed25519-dalek (what lex-os-capsule uses today) is written specifically to make that hard to introduce by accident; nothing here makes it hard at all. A timing-oracle attacker with repeated access to signing under a fixed key is the threat model this matters for, and this module is not written against it. Whether that threat model applies depends on where a future consumer runs this — that is a decision for whoever reaches for this module next, not one this document can make in advance.

No key generation from randomness. public_key_from_seed/sign take a caller-supplied 32-byte seed; cancho has no CSPRNG capability today (no random in the capability list linearity-and-effects.md settles), so there is nothing this module could call to generate a fresh one. A caller gets a seed from wherever it already trusts one to come from.

No batch or double-scalar multiplication. verify’s S*B == R + k*A check does two full scalar multiplications and a point add, where a real implementation typically combines them into one double-scalar multiplication for speed. Correct either way; slower than it needs to be, which is this module’s trade throughout, made once more.