ASTRA–CaPU v1.0-A7: authenticated device outcome receipts

[safal207]

Summary

Adds an authenticated device-receipt boundary in front of the A6 durable outcome reconciler.

accelerator device receipt
+ trusted device identity
+ trusted key epoch
+ monotonic receipt sequence
+ exact attempt identity
+ authenticated envelope tag
        ↓
receipt authentication gate
        ↓
A6 exact outcome reconciliation

Only a receipt that matches the trusted device, key epoch, exact next sequence number, complete attempt identity, outcome field and keyed envelope tag is exposed to A6.

Exact verified head

base A6 head:
2cf971e6f9cdefd213e72b4e79d4840c6ed83808

verified A7 head:
5cdaa5280348841bf8448c5a7844c273df257c5d

pull-request merge ref checked by Actions:
c8de47b9e2f4968bb72400854049b7cdc3325eec

The A7 implementation head was not changed after exact-head verification.

Added

• synthesizable trusted-device receipt gate;
• persistent trusted device ID, key epoch, keyed-tag secret and next receipt sequence;
• exact envelope binding over device, key epoch, sequence, full authority/attempt identity and outcome;
• integrated A7 authenticated device + A6 persistent outcome reconciler;
• deterministic forged / stale / foreign-device / exact receipt trajectory;
• deterministic software mirror, JSON schema and canonical expected result;
• 11 focused tests;
• bounded safety and cover harnesses;
• A6 deterministic, unit and formal regressions;
• machine-readable and hash-sealed evidence artifacts.

Threat discriminator

attempt 0 → UNKNOWN
        ↓
forged NOT_COMMITTED receipt seq 0
→ AUTH_TAG reject
→ sequence stays 0
→ UNKNOWN preserved
        ↓
exact NOT_COMMITTED receipt seq 0
→ authenticated and applied
→ sequence becomes 1
        ↓
attempt 1 → external effect → UNKNOWN
        ↓
replayed seq 0 receipt
→ RECEIPT_SEQUENCE reject
        ↓
foreign device receipt seq 1
→ DEVICE_ID reject
        ↓
exact COMMITTED receipt seq 1
→ authenticated and applied
→ terminal committed
→ sequence becomes 2
        ↓
later attempts remain blocked

Exact-head CI

Primary run:

ASTRA-CaPU v1.0-A7 Authenticated Device Receipts
33256771503                                      PASS
├─ A7 authenticated receipt trajectory
│  99111772866                                   PASS
└─ Bounded A7 authenticated receipt proof
   99111773047                                   PASS

Additional exact-head workflows:

Validate Examples           33256771604  PASS
CaPU Core v0 RTL Smoke      33256771575  PASS

Deterministic/model checks:

A7 SystemVerilog trajectory             PASS
A7 software reference                   PASS
A7 unit tests                     11/11 PASS
A6 RTL regression                        PASS
A6 unit regression                 13/13 PASS
A6 bounded formal regression             PASS
machine-readable expected result         PASS

Formal result

proof method: bounded model checking
safety depth: 32                     PASS
cover depth: 56                      PASS
VCD witnesses: 9
A6 bounded safety regression:        PASS

formal device width: 2 bits
formal tag width: 2 bits
formal identity width: 2 bits
formal auth-tag width: 4 bits
trusted device count: 1
trusted key-epoch count: 1
max unresolved attempts: 1
synthetic MAC model: true
monotonic receipt sequence: true
authenticated semantic reject consumes sequence: true

Formal hashes:

formal input:
66c56e74e3ce48b29205e6d401e3175a2482cb3b1783db504dd249a4dcf36815

safety log:
d80f67ea54c05bb494dd0cc4a9886b890e6863242704dc5a2c426fdec756d397

cover log:
191d838f5a71acbf3cb06c26d3979c7205675833b6c8a9ee8449536584909dc1

A6 regression log:
1686343dca7671a25fe1536f089bcdc4ecbf5f300ac79cd6888ede4766bd185e

Pinned toolchain:

SBY b1a1e98cba941ec8433f8dc27f416cd7bb7f14be
Yosys 0.33 (git sha1 2584903a060)
Z3 4.8.12

Evidence artifacts

Executable evidence:

artifact: astra-capu-v1-a7-authenticated-device-receipt-evidence
ID: 9716040264
ZIP SHA-256:
eb9e1c6c6a03642a83c8c395f6dea97e0eb230c1db03f9484f0c2863c0744268

Formal evidence:

artifact: astra-capu-v1-a7-authenticated-device-receipt-formal-evidence
ID: 9716074483
ZIP SHA-256:
ad63eb4a1dfd4735a0c7294b179a1341582417d9e3635d75c26931a5162d11b5

Canonical deterministic result:

schema:
capu.astra.authenticated-device-receipt.result.v1.0-a7

result digest:
6781dbfbd1b529866709980a3a85a38bd37f505daaddd53fd7c8e106ab863d2f

external_effect_count: 1
persistent_next_attempt: 2
next_receipt_sequence: 2
last_outcome: COMMITTED
forged receipt reject code: 5
stale sequence reject code: 4
foreign device reject code: 2
terminal replay reject code: 11

Core invariants

A6_RECONCILE_VALID
=> A7_AUTH_ACCEPT

A7_AUTH_ACCEPT
=> EXACT_DEVICE_ID
&& EXACT_KEY_EPOCH
&& RECEIPT_SEQ == TRUSTED_NEXT_RECEIPT_SEQ_PRE
&& EXACT_FULL_ATTEMPT_IDENTITY
&& EXACT_OUTCOME_BINDING
&& AUTH_TAG_MATCH

AUTH_REJECT
=> NO_A6_RECONCILIATION
&& NO_TRUST_STATE_MUTATION

AUTH_ACCEPT
=> TRUSTED_NEXT_RECEIPT_SEQ_POST
   == TRUSTED_NEXT_RECEIPT_SEQ_PRE + 1

AUTH_ACCEPT + A6_SEMANTIC_REJECT
=> SEQUENCE_CONSUMED
&& NO_A6_PERSISTENT_OUTCOME_MUTATION

Claim boundary

The A7 keyed tag is a transparent rotate/XOR synthetic authentication primitive for bounded state-machine verification. It is not production cryptography and this PR does not claim SPDM, DICE, TPM, secure-element, PKI, certificate-chain or attestation conformance.

A7 is a bounded, reduced-width, single-trusted-device model with one key epoch, one persistent receipt sequence, one A6 lineage and at most one unresolved attempt.

This PR does not prove cryptographic unforgeability, key secrecy, secure provisioning, key rotation, re-attestation, Byzantine or multi-source reconciliation, actual NVRAM, complete power-loss durability, real accelerator transport, CDC/memory ordering, timing/PPA, liveness, production widths or unbounded correctness.

This PR remains draft and is not merged in this step.

[coderabbitai]

Important

Draft PR not reviewed

Draft PRs are not automatically reviewed by default.

• Trigger a manual review

To automatically review draft PRs, update your CodeRabbit configuration:

reviews:
  auto_review:
    drafts: true

---

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands.}