t27c v0.5.0 — the Verified Compute tool chain: signed receipts that name the die

t27c can now say which die ran a spec, who signed for it, and whether the run is evidence -- and every one of those judgments is code generated from a .t27 contract, not hand-written Rust.

This is the tool half of epic #6655 (Verified Compute), Rounds 2 and 3.

What a run produces

t27c silicon <spec> ... --pnr-seed N --nonce <hex> builds a sealed spec into a bitstream, loads it, reads the verdict back over JTAG, and writes a receipt into .trinity/receipts/:

field	where it comes from
full_idcode	read live from the part before any load
device_dna	the die's 57-bit DNA, read over JTAG (FUSE_DNA and XSC_DNA) before and after the run; a board swapped mid-run is refused
verdict_word	PASS / FAIL from the design's own USER3 answer
seal_hash	the seal of the image the device ran
toolchain	t27c-bootstrap@<version>+<build commit>, matched against the seal's built_by
seeds, nonce	the placement seed and the verifier's challenge
key_id, signature	Ed25519 over a fixed message: domain line plus ten name=<json> lines

t27c receipt-key init|show makes the signing key outside the repository and registers its public half in .trinity/keys/.

What judges it

t27c run-record <spec> --challenge <hex> reads the receipts and answers, in the contracts' fixed order:

• Run complete? Three placements, every field present, the verdict words agree, and the producer matches the seal (specs/verified/run_record.t27).
• Authentication: NONE < AUTHOR < FRESH. FRESH means signed by a registered key over this verifier's nonce (signed_receipt.t27).
• Die: NAMED when the DNA is inside the signed bytes (die_binding.t27).
• Independence: INDEP_DIES only when the three placements name three distinct dies (independence.t27).

The judgments are not mirrored by hand: t27c gen-rust lowers each contract into bootstrap/gen/rust/verified/, and a drift test fails when a checked-in copy stops matching its spec.

Crypto in our own language

SHA-256, SHA-512 and Ed25519 (RFC 8032) are .t27 specs (specs/tri/crypto/). t27c signs, verifies and hashes seals with the Rust generated from them.

• ed25519-dalek remains only as a dev-dependency: an independent oracle checked byte-for-byte in the tests.
• sha2 has left the build script.
• Verification is strict: a small-order public key or R is rejected, as dalek's verify_strict does.

Evidence on silicon

On a QMTech Wukong XC7A200T, specs/fpga/ternary_link.t27 ran three placements (pnr seeds 1/7/42) with one verifier nonce:

• every placement was bracketed by a wrong-part control (Done 0 -> 1);
• USER3 read ok=1, clauses 1111;
• the die's DNA, 050d58218fd9854, read the same before and after each load.

run-record judged the run: complete, FRESH, Die NAMED, citable. The receipts are committed (#7598). Its independence line reads INDEP_NONE -- INDEP_SHARED_DIE, 1 distinct die: three placements on one board catch place-and-route faults, not a bad die. Agreement across distinct dies waits for the other boards.

What it does not claim

• A DNA is a name, not a secret. DIE_NAMED catches a wrong board or a swapped cable, not a dishonest signer. No level is device-rooted (DIE_ROOTED_LEVELS = 0, INDEP_ROOTED_LEVELS = 0).
• Distinct keys are not distinct people. A verifier without a roster reaches at most INDEP_DIES.

Pull requests

• Round 2: #7044, #7061, #7076, #7130, #7293
• Round 3, signed receipts: #7344, #7363, #7416, #7434
• Round 3, crypto specs and gen-rust: #7424, #7435, #7444, #7468, #7469, #7594
• Round 3, die DNA: #7446, #7484, #7570, #7598
• Round 3, independence: #7516, #7601

1600+ commits since 0.4.0 in all; this note covers the Verified Compute line.