Module verify_core

Expand description

Known-key strict verification core.

KnownKeyVerifyCore verifies Ed25519 signatures of 64-byte messages for up to KEY_SLOTS public keys loaded in advance (8, or 16 with the feature key-slots-16), with the strict rules and error codes of the StrictVerifyCore in rhdl_ed25519_fast_core: S must be canonical, A and R must be canonical curve points and not of low order, and [S]B = R + [k]A must hold (no cofactor).

§Dataflow

request ──> admission ──> SHA ring: H(R || A || M) ──> scalar ring: k = H mod l
              │ (key slot, S < l, R canonical, R low order)        │
              │                                                    v
              │         verify machine: [S]B + [k](-A) <── recode S and k
              │                       │ X, Y, Z
              v                       v
           result <── compare with R <── CompressStage (32 points per inversion)
              ^                  │ mismatch
              └── aux machine: decode R (BAD_R or EQUATION_FAILURE)

Each verify machine scans two tables per verification: the base-point table (ROM) for S and the key’s table for k, so the equation costs two fixed-base walks (775 bundles) instead of a variable-base multiplication. The key table holds multiples of -A, so the machine computes [S]B + [k](-A), which equals R exactly when the equation holds.

§Contexts and tags

A request is accepted into a one-entry admission register, where its key is matched and its immediate result decided. On the next cycle (or as soon as a context, a credit and a SHA resource are free) it is admitted: an admitted request takes one of 2,048 contexts from a free list. The context number indexes the per-request memories (VerifyMems: R, S and the request facts), so only the 11-bit context and the 3- or 4-bit key slot travel with the job. They are packed into the 16-bit tag as slot << 11 | ctx through the SHA and scalar rings; the verify machine and the compress stage carry the context alone. The context returns to the free list when its result is reported. Requests that fail at admission (unknown key, invalid key, non-canonical R) never take one.

§Key loading

load_key_valid with an encoded A and a slot starts a key load on the aux machine: decode A (decode_candidate), compute the 54 table bases of -A (table_bases), then 54 digit jobs (digit_table) whose outputs are written into every verify machine’s key table. The writes pass from machine to machine, one per cycle, so a slot becomes usable NV + 2 cycles after its last digit job retires (about 105k cycles in all). A key that does not decode is kept as invalid, so its requests get VERIFY_BAD_PUBLIC_KEY. ready is low while any key loads, and while a key load is offered: a load offered in the same cycle as a request goes first. A load starts only with no request held or in flight.

The aux machine’s 32 contexts are split by job: context 0 decodes (a key or an R), context 1 computes table bases, and contexts 2..32 run digit jobs, up to 30 at once. Its tags carry the job kind in bits 8.. (one of the AUX_* constants) and, for digit jobs, the digit number in bits 0..8.

In the key tables, digit i occupies the rows from digit_row(i): eight rows (16 entries, two per row) for the 39 radix-32 digits and four rows (8 entries) for the 15 radix-16 digits, 372 rows per key. Key slot s owns rows s * 512 ...

§Errors

In priority order: VERIFY_BAD_PUBLIC_KEY, VERIFY_BAD_R, VERIFY_SMALL_PUBLIC_KEY, VERIFY_SMALL_R, VERIFY_NONCANONICAL_S, VERIFY_EQUATION_FAILURE; VERIFY_UNKNOWN_KEY for a key that is not loaded. When the computed point does not encode to R, the aux machine decodes R to tell an invalid R from a failed equation (a slow path only invalid signatures take).

The errors are found in three places:

At admission: unknown key, invalid key, and R whose y is not below p (VERIFY_BAD_R). These are reported at once.
At the compare: if the computed point encodes to R, then R is a valid point encoding, so VERIFY_BAD_R cannot apply and the result is the first of the small-key, small-R and non-canonical-S facts recorded at admission, or VERIFY_OK.
After the R decode (mismatch only): VERIFY_BAD_R if R does not decode, else the same admission facts, else VERIFY_EQUATION_FAILURE.

The admission facts are not reported at admission because VERIFY_BAD_R outranks them and needs the decode, which the compare avoids in the common case. So every request past admission runs the equation, even one whose S is already known to be non-canonical; its computed point is then irrelevant.

§Deadlock freedom

Admission takes a compress credit, as in crate::sign_core, so every verify-machine output finds a compress slot. The rest of the flow has no cycle: compare waits only for the result register, which drains every cycle, and the aux machine’s jobs (key loading, R decodes) never wait on the verification path.

Structs§

KnownKeyVerifyCore: Known-key strict verifier with NV verify machines, NSHA SHA-512 rings and NSC scalar rings; with SH = 1 it hashes through the shared SHA-512 port (VerifyOut::sha_ext) instead and its rings stay idle (use NSHA = 1; synthesis removes an idle ring).
VerifyIn: Inputs of KnownKeyVerifyCore.
VerifyMems: Per-context memories, plus the free list and the key-load bases.
VerifyMemsIn: Port bundle of VerifyMems.
VerifyMemsOut: Read data of VerifyMems.
VerifyOut: Outputs of KnownKeyVerifyCore.

Constants§

VERIFY_BAD_PUBLIC_KEY: The public key is not a canonical curve point.
VERIFY_BAD_R: R is not a canonical curve point.
VERIFY_EQUATION_FAILURE: [S]B = R + [k]A does not hold.
VERIFY_NONCANONICAL_S: S is not below l.
VERIFY_OK: Verification succeeded.
VERIFY_SMALL_PUBLIC_KEY: The public key has low order.
VERIFY_SMALL_R: R has low order.
VERIFY_UNKNOWN_KEY: The public key is not loaded in any slot.

Functions§

aux_programs: The aux machine’s ROM and the entry of each program (decode, bases, 16-entry digit table, 8-entry digit table).
below_l: S < l for four little-endian words, l = 2^252 + 27742317777372353535851937790883648493 the group order.
canonical_y: y < p for a 32-byte encoding (sign bit ignored).
digit_row: Row of digit i’s first entry pair within a key’s 512-row table.
encoding_y: y of an encoding (sign bit cleared) as field digits.
join_digits: Key and base-point digits in the machine’s 128 slots.
known_key_verify_kernel: State transition for KnownKeyVerifyCore.
neg_from: -v from the limbs of p - v (as field_neg: zero stays zero).
p_minus_step: One limb of p - v = !v + (2^255 - 18) mod 2^255: limb step of the result from limb step of v and the carry out of the limbs below (c); the other limbs of acc pass through. One 85-bit carry chain.
pick_machine: The verify machine a new request goes to: the one with the most free contexts, the lowest index on a tie (R-11). Fixed priority filled machine 0’s 32 contexts before any other, so with the uBFT service’s 16 tags outstanding a second machine never received work.
small_order_encoding: The eight low-order encodings strict verification rejects.
split_entry: (entry, coordinate) of a digit-table output index 3e + c.
verify_mems_kernel: Wiring for VerifyMems: each port goes straight to its RAM.

Type Aliases§

AuxMachine: Aux machine: key loading and R decoding (four programs in one ROM).
VerifyMachine: Verify machine: 32 contexts, base-point table, key tables for 8 keys.