Repository navigation
t27c: verify the die's DNA inside a signed receipt -- R3-2 slice 2 tool half (Refs #7452) - #7484
Merged
Merged
Conversation
…Refs #7439) specs/verified/device_dna.t27 pins every decision about the 7-series device DNA read with no user bitstream: IR length 6, FUSE_DNA 0x32 (64-bit register) and XSC_DNA 0x17 between ISC_ENABLE 0x10 and ISC_DISABLE 0x16 (57-bit register); how the raw shift decodes to the DNA (first shifted bit is the most significant, the order openFPGALoader --read-dna prints); well-formedness (not all zero, not all one, XSC fill ones, FUSE tail as observed); fixed-width hex; and when a FUSE read and an XSC read name one die. Oracle: 14 live reads of each instruction on the attached XC7A200T over two transports (libftdi MPSSE and openocd), all identical; decoded DNA 050d58218fd9854. 13 tests, 0 vacuous; 20 of 20 hand mutants killed on the Railway lab. The reader is the openocd command line in the spec header: the Only-t27 gate refuses a new or edited .py, and the read needs no new code. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
t27c test-report: 13 tests, 13 pass, 0 vacuous. Seal written by t27c seal --save on the lab (t27c-bootstrap@0.4.0+cfda070b2). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…tract (Refs #7439) The v2 receipt message adds device_dna after full_idcode under a new domain line. The producer writes it only when FUSE_DNA and XSC_DNA name one die before and after the run; the verifier counts it only inside verified bytes. distinct_dies3 gives R3-3 its die count. Honest ceiling: the DNA is a name, not a secret, so DIE_NAMED is the signer's claim. DIE_ROOTED_LEVELS stays 0. signed_receipt.t27's comment that called a signed DNA read device-rooted is corrected. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
#7439) A receipt is v2 exactly when its device_dna is text, so stripping or adding the field changes the signed bytes. The DNA reader runs only when exactly one JTAG cable is attached (openocd opens the first FTDI cable it finds, W838). Both checks run at runtime: test-report 13/13, 0 vacuous; 7 hand mutants (version swap x3, cable rule x4) all fail a test. Resealed on the Railway lab. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
die_binding.t27 reaches t27c through gen-rust (bootstrap/gen/rust/verified/die_binding.rs, drift-tested). A receipt whose device_dna is text signs the v2 message (SIGNED_FIELDS_V2), so the DNA is inside the signed bytes: change one hex digit or strip the field and verification fails with AUTH_BAD_SIGNATURE. run-record prints the die level (NAMED / NONE) from die_level and the run fold; no level is device-rooted, because the DNA is a public name, not a secret. Hand Rust is glue only: main.rs +4, service.rs +39/-6, reader test +5/-3. The producer (reading the DNA on the bench) is the next slice. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
gHashTag
enabled auto-merge (squash)
October 7, 2026 11:00
This was referenced Oct 7, 2026
5 tasks
This was referenced Oct 7, 2026
Closed
Merged
This was referenced Oct 7, 2026
Merged
corpus: judge 26 new type conflicts from the port batches; types ledger 84 -> 110 (Refs #5906)
#7482
Merged
Contributor
This was referenced Oct 7, 2026
Merged
Merged
This was referenced Oct 7, 2026
This was referenced Oct 7, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
R3-2 slice 2, tool half: t27c now verifies the die's DNA as part of a signed receipt.
Refs #7452 (contract: #7455, stacked here; slice 1: #7446). Epic #6655, round #7332.
What changes
specs/verified/die_binding.t27gainsreceipt_version(a receipt is v2 exactly when itsdevice_dnais text) anddna_read_allowed(the reader runs only with exactly one JTAG cable attached: openocd opens the first FTDI cable it finds, W838).die_binding.t27reaches t27c through gen-rust:bootstrap/gen/rust/verified/die_binding.rs, wired with#[path], and drift-tested inbootstrap/tests/signed_receipt_reader.rs.device_dnais text signs the v2 message (SIGNED_FIELDS_V2), so the DNA is inside the signed bytes. Changing one hex digit or nulling the field fails asAUTH_BAD_SIGNATURE(new testthe_device_dna_is_inside_the_signed_bytes).run-recordprints the die level (NAMED/NONE) fromdie_leveland the run fold, and states plainly that no level is device-rooted: the DNA is a public name, not a die-held secret.Own-language budget
Hand Rust here is glue only:
main.rs+4,service.rs+39/-6, the reader test +5/-3. Every decision comes from the generated module.Evidence (Railway lab, rebased head f943ba3)
t27c test-report specs/verified/die_binding.t27: 13/13 pass, 0 vacuous.>= 1,<= 1,!= 0,true).seal --verifyMATCH for device_dna, die_binding and signed_receipt.r3_signed_receipt/r2_silicon_receipt/run_record17 pass,signed_receipt_reader14 pass,run_record_reader6 pass.Not in this PR
The producer, which reads the DNA on the bench and writes it into the silicon receipt, is the next slice.
🤖 Generated with Claude Code