diff --git a/.github/workflows/astra-capu-v1-a7-authenticated-device-receipts.yml b/.github/workflows/astra-capu-v1-a7-authenticated-device-receipts.yml new file mode 100644 index 0000000..d066654 --- /dev/null +++ b/.github/workflows/astra-capu-v1-a7-authenticated-device-receipts.yml @@ -0,0 +1,257 @@ +name: ASTRA-CaPU v1.0-A7 Authenticated Device Receipts + +on: + pull_request: + paths: + - 'rtl/astra_capu_effect_counter_a3.sv' + - 'rtl/astra_capu_persistent_outcome_store_a6.sv' + - 'rtl/astra_capu_outcome_authority_shim_a6.sv' + - 'rtl/astra_capu_reconciled_effect_device_a6.sv' + - 'rtl/astra_capu_authenticated_receipt_gate_a7.sv' + - 'rtl/astra_capu_authenticated_reconciled_effect_device_a7.sv' + - 'rtl/tb/astra_capu_authenticated_reconciled_effect_device_a7_tb.sv' + - 'formal/astra_capu_authenticated_receipt_a7*' + - 'tools/astra_capu_authenticated_receipt_a7.py' + - 'tests/test_astra_capu_authenticated_receipt_a7.py' + - 'schemas/hardware/astra-capu-authenticated-device-receipt-v1.0-a7.schema.json' + - 'examples/hardware/astra-capu-v1-a7-expected.json' + - 'docs/hardware/ASTRA_CAPU_V1_A7_AUTHENTICATED_DEVICE_RECEIPTS.md' + - '.github/workflows/astra-capu-v1-a7-authenticated-device-receipts.yml' + +jobs: + deterministic: + name: A7 authenticated receipt trajectory + runs-on: ubuntu-24.04 + steps: + - uses: actions/checkout@v4 + - name: Install Icarus Verilog + run: | + sudo apt-get update + sudo apt-get install -y iverilog + iverilog -V + - name: Compile A7 authenticated reconciled device + run: | + set -euo pipefail + iverilog -g2012 \ + -o /tmp/astra-capu-a7.vvp \ + rtl/astra_capu_effect_counter_a3.sv \ + rtl/astra_capu_persistent_outcome_store_a6.sv \ + rtl/astra_capu_outcome_authority_shim_a6.sv \ + rtl/astra_capu_reconciled_effect_device_a6.sv \ + rtl/astra_capu_authenticated_receipt_gate_a7.sv \ + rtl/astra_capu_authenticated_reconciled_effect_device_a7.sv \ + rtl/tb/astra_capu_authenticated_reconciled_effect_device_a7_tb.sv + - name: Run deterministic A7 trajectory + run: | + set -euo pipefail + vvp /tmp/astra-capu-a7.vvp | tee astra-capu-v1-a7-rtl.log + grep -F 'a7_attempt0_forwarded outcome=UNKNOWN effect_count=0' astra-capu-v1-a7-rtl.log + grep -F 'a7_forged_receipt_blocked reject_code=5 next_receipt_seq=0' astra-capu-v1-a7-rtl.log + grep -F 'a7_negative_receipt_authenticated seq=0 outcome=NOT_COMMITTED next_receipt_seq=1' astra-capu-v1-a7-rtl.log + grep -F 'a7_attempt1_forwarded outcome=UNKNOWN effect_count=1' astra-capu-v1-a7-rtl.log + grep -F 'a7_stale_receipt_replay_blocked reject_code=4 next_receipt_seq=1' astra-capu-v1-a7-rtl.log + grep -F 'a7_foreign_device_receipt_blocked reject_code=2 next_receipt_seq=1' astra-capu-v1-a7-rtl.log + grep -F 'a7_committed_receipt_authenticated seq=1 terminal_committed=1 next_receipt_seq=2' astra-capu-v1-a7-rtl.log + grep -F 'a7_terminal_replay_blocked reject_code=11 effect_count=1' astra-capu-v1-a7-rtl.log + grep -F 'ASTRA_CAPU_V1_A7_AUTHENTICATED_DEVICE_RECEIPT_PASS' astra-capu-v1-a7-rtl.log + - name: Run A7 reference and unit tests + run: | + set -euo pipefail + python3 -m unittest -v tests/test_astra_capu_authenticated_receipt_a7.py \ + 2>&1 | tee astra-capu-v1-a7-test.log + python3 -m tools.astra_capu_authenticated_receipt_a7 \ + | tee astra-capu-v1-a7-reference.log + grep -F 'Ran 11 tests' astra-capu-v1-a7-test.log + grep -F 'OK' astra-capu-v1-a7-test.log + grep -F 'ASTRA_CAPU_V1_A7_AUTHENTICATED_DEVICE_RECEIPT_PASS' astra-capu-v1-a7-reference.log + - name: Regress A6 outcome reconciliation + run: | + set -euo pipefail + iverilog -g2012 \ + -o /tmp/astra-capu-a6.vvp \ + rtl/astra_capu_effect_counter_a3.sv \ + rtl/astra_capu_persistent_outcome_store_a6.sv \ + rtl/astra_capu_outcome_authority_shim_a6.sv \ + rtl/astra_capu_reconciled_effect_device_a6.sv \ + rtl/tb/astra_capu_reconciled_effect_device_a6_tb.sv + vvp /tmp/astra-capu-a6.vvp | tee astra-capu-v1-a6-regression.log + python3 -m unittest -v tests/test_astra_capu_outcome_reconciliation_a6.py \ + 2>&1 | tee astra-capu-v1-a6-test-regression.log + grep -F 'ASTRA_CAPU_V1_A6_OUTCOME_RECONCILIATION_PASS' astra-capu-v1-a6-regression.log + grep -F 'Ran 13 tests' astra-capu-v1-a6-test-regression.log + grep -F 'OK' astra-capu-v1-a6-test-regression.log + - name: Generate and validate machine-readable result + run: | + set -euo pipefail + python3 - <<'PY' + import json + from pathlib import Path + from tools.astra_capu_authenticated_receipt_a7 import scenario_result + + result = scenario_result() + output = Path('astra-capu-v1-a7-result.json') + output.write_text(json.dumps(result, indent=2, sort_keys=True) + '\n') + schema = json.loads(Path('schemas/hardware/astra-capu-authenticated-device-receipt-v1.0-a7.schema.json').read_text()) + expected = json.loads(Path('examples/hardware/astra-capu-v1-a7-expected.json').read_text())['expected'] + assert schema['title'] == 'ASTRA–CaPU Authenticated Device Receipt v1.0-A7 Result' + assert result == expected + assert result['forged_receipt_reject_code'] == 5 + assert result['stale_receipt_reject_code'] == 4 + assert result['foreign_device_reject_code'] == 2 + assert result['terminal_replay_reject_code'] == 11 + assert result['next_receipt_sequence'] == 2 + print(f"a7_machine_result_digest={result['result_digest_sha256']}") + print('A7_MACHINE_RESULT_PASS') + PY + - name: Seal executable A7 evidence + run: | + cp /tmp/astra-capu-a7.vvp ./astra-capu-a7.vvp + sha256sum \ + rtl/astra_capu_effect_counter_a3.sv \ + rtl/astra_capu_persistent_outcome_store_a6.sv \ + rtl/astra_capu_outcome_authority_shim_a6.sv \ + rtl/astra_capu_reconciled_effect_device_a6.sv \ + rtl/astra_capu_authenticated_receipt_gate_a7.sv \ + rtl/astra_capu_authenticated_reconciled_effect_device_a7.sv \ + rtl/tb/astra_capu_authenticated_reconciled_effect_device_a7_tb.sv \ + tools/astra_capu_authenticated_receipt_a7.py \ + tests/test_astra_capu_authenticated_receipt_a7.py \ + schemas/hardware/astra-capu-authenticated-device-receipt-v1.0-a7.schema.json \ + examples/hardware/astra-capu-v1-a7-expected.json \ + docs/hardware/ASTRA_CAPU_V1_A7_AUTHENTICATED_DEVICE_RECEIPTS.md \ + astra-capu-a7.vvp \ + astra-capu-v1-a7-rtl.log \ + astra-capu-v1-a7-test.log \ + astra-capu-v1-a7-reference.log \ + astra-capu-v1-a6-regression.log \ + astra-capu-v1-a6-test-regression.log \ + astra-capu-v1-a7-result.json \ + > astra-capu-v1-a7.sha256 + cat astra-capu-v1-a7.sha256 + - uses: actions/upload-artifact@v4 + with: + name: astra-capu-v1-a7-authenticated-device-receipt-evidence + path: | + astra-capu-a7.vvp + astra-capu-v1-a7-rtl.log + astra-capu-v1-a7-test.log + astra-capu-v1-a7-reference.log + astra-capu-v1-a6-regression.log + astra-capu-v1-a6-test-regression.log + astra-capu-v1-a7-result.json + astra-capu-v1-a7.sha256 + + formal: + name: Bounded A7 authenticated receipt proof + runs-on: ubuntu-24.04 + steps: + - uses: actions/checkout@v4 + - name: Install Yosys and Z3 + run: | + sudo apt-get update + sudo apt-get install -y yosys z3 git + yosys -V + z3 --version + - name: Install pinned SBY + run: | + set -euo pipefail + SBY_SHA='b1a1e98cba941ec8433f8dc27f416cd7bb7f14be' + git init /tmp/sby + git -C /tmp/sby remote add origin https://github.com/YosysHQ/sby.git + git -C /tmp/sby fetch --depth 1 origin "$SBY_SHA" + git -C /tmp/sby checkout --detach FETCH_HEAD + test "$(git -C /tmp/sby rev-parse HEAD)" = "$SBY_SHA" + printf '%s\n' "$SBY_SHA" > /tmp/sby-sha.txt + - name: Prove bounded A7 safety + run: | + set -euo pipefail + mkdir -p target/astra-capu-a7-formal + python3 /tmp/sby/sbysrc/sby.py -f \ + -d target/astra-capu-a7-formal/safety-work \ + formal/astra_capu_authenticated_receipt_a7.sby \ + 2>&1 | tee target/astra-capu-a7-formal/formal.log + grep -q 'DONE (PASS' target/astra-capu-a7-formal/formal.log + - name: Prove A7 authenticated paths reachable + run: | + set -euo pipefail + python3 /tmp/sby/sbysrc/sby.py -f \ + -d target/astra-capu-a7-formal/cover-work \ + formal/astra_capu_authenticated_receipt_a7_cover.sby \ + 2>&1 | tee target/astra-capu-a7-formal/cover.log + grep -q 'DONE (PASS' target/astra-capu-a7-formal/cover.log + test "$(find target/astra-capu-a7-formal/cover-work -name 'trace*.vcd' | wc -l)" -ge 1 + - name: Regress bounded A6 safety + run: | + set -euo pipefail + python3 /tmp/sby/sbysrc/sby.py -f \ + -d target/astra-capu-a7-formal/a6-regression-work \ + formal/astra_capu_outcome_reconciliation_a6.sby \ + 2>&1 | tee target/astra-capu-a7-formal/a6-regression.log + grep -q 'DONE (PASS' target/astra-capu-a7-formal/a6-regression.log + - name: Seal formal evidence + run: | + python3 - <<'PY' + import hashlib + import json + import subprocess + from pathlib import Path + + root = Path('target/astra-capu-a7-formal') + safety = (root / 'formal.log').read_text(errors='replace') + cover = (root / 'cover.log').read_text(errors='replace') + a6 = (root / 'a6-regression.log').read_text(errors='replace') + inputs = [Path(x) for x in [ + 'rtl/astra_capu_effect_counter_a3.sv', + 'rtl/astra_capu_persistent_outcome_store_a6.sv', + 'rtl/astra_capu_outcome_authority_shim_a6.sv', + 'rtl/astra_capu_reconciled_effect_device_a6.sv', + 'rtl/astra_capu_authenticated_receipt_gate_a7.sv', + 'rtl/astra_capu_authenticated_reconciled_effect_device_a7.sv', + 'formal/astra_capu_authenticated_receipt_a7_formal.sv', + 'formal/astra_capu_authenticated_receipt_a7.sby', + 'formal/astra_capu_authenticated_receipt_a7_cover.sby', + 'tools/astra_capu_authenticated_receipt_a7.py', + ]] + h = hashlib.sha256() + for path in inputs: + h.update(str(path).encode() + b'\0' + path.read_bytes() + b'\0') + proof = { + 'schema': 'capu.hardware.astra-authenticated-device-receipt-formal-proof.v1.0-a7', + 'result': 'PASS', + 'proof_method': 'bounded model checking', + 'depth': 32, + 'cover_depth': 56, + 'cover_witnesses': len(list((root / 'cover-work').rglob('trace*.vcd'))), + 'formal_device_width_bits': 2, + 'formal_tag_width_bits': 2, + 'formal_identity_width_bits': 2, + 'formal_auth_tag_width_bits': 4, + '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, + 'a6_regression': 'PASS', + 'formal_input_sha256': h.hexdigest(), + 'formal_log_sha256': hashlib.sha256(safety.encode()).hexdigest(), + 'cover_log_sha256': hashlib.sha256(cover.encode()).hexdigest(), + 'a6_regression_log_sha256': hashlib.sha256(a6.encode()).hexdigest(), + 'sby_git_sha': Path('/tmp/sby-sha.txt').read_text().strip(), + 'yosys_version': subprocess.check_output(['yosys', '-V'], text=True).strip(), + 'z3_version': subprocess.check_output(['z3', '--version'], text=True).strip(), + 'claim_boundary': 'bounded reduced-width single-device synthetic authenticated-envelope model; the rotate/XOR tag is not production cryptography or SPDM conformance, and key secrecy, key rotation, actual NVRAM, real accelerator transport, liveness and unbounded correctness remain outside scope', + } + (root / 'formal-proof.json').write_text(json.dumps(proof, indent=2, sort_keys=True) + '\n') + print(json.dumps(proof, indent=2, sort_keys=True)) + PY + - uses: actions/upload-artifact@v4 + with: + name: astra-capu-v1-a7-authenticated-device-receipt-formal-evidence + path: | + target/astra-capu-a7-formal/formal.log + target/astra-capu-a7-formal/cover.log + target/astra-capu-a7-formal/a6-regression.log + target/astra-capu-a7-formal/formal-proof.json + target/astra-capu-a7-formal/safety-work/ + target/astra-capu-a7-formal/cover-work/ diff --git a/docs/hardware/ASTRA_CAPU_V1_A7_AUTHENTICATED_DEVICE_RECEIPTS.md b/docs/hardware/ASTRA_CAPU_V1_A7_AUTHENTICATED_DEVICE_RECEIPTS.md new file mode 100644 index 0000000..efa815d --- /dev/null +++ b/docs/hardware/ASTRA_CAPU_V1_A7_AUTHENTICATED_DEVICE_RECEIPTS.md @@ -0,0 +1,195 @@ +# ASTRA–CaPU v1.0-A7 — Authenticated Device Outcome Receipts + +## Purpose + +A6 persists an unresolved accelerator attempt and accepts exact `NOT_COMMITTED`, `COMMITTED`, or `CONFLICT` outcome evidence. It checks that the evidence identity matches the current unresolved attempt, but it intentionally trusts the supplied outcome discriminator. + +A7 inserts an authenticated device-receipt boundary before A6 reconciliation: + +```text +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 an authenticated receipt is exposed to the A6 durable outcome store. + +## Receipt identity + +The authenticated envelope binds: + +```text +device_id ++ key_epoch ++ receipt_seq ++ authority_tag ++ queue_incarnation ++ queue_epoch ++ slot_id ++ command_id ++ attempt_id ++ effect_id ++ outcome +``` + +The trust record retains: + +```text +trusted_device_id +trusted_key_epoch +trusted_secret +trusted_next_receipt_seq +``` + +A receipt must exactly match the trusted device, key epoch, and next sequence number. Its envelope tag must verify over the complete receipt identity. + +## Synthetic authentication function + +The A7 RTL and software mirror use a transparent fixed-width rotate/XOR keyed tag. This is deliberately a **synthetic authentication primitive** for formal state-machine work. It is not claimed to be a secure MAC, digital signature, SPDM implementation, or production cryptography. + +The verified architectural contract is independent of the toy primitive: + +```text +AUTHENTICATED_RECEIPT +=> EXACT_DEVICE +&& EXACT_KEY_EPOCH +&& EXACT_SEQUENCE +&& EXACT_FULL_ATTEMPT_IDENTITY +&& EXACT_OUTCOME_BINDING +``` + +A production implementation must replace the synthetic tag with a reviewed cryptographic trust mechanism. + +## Monotonic anti-replay sequence + +```text +trusted_next_receipt_seq = N +receipt seq = N ++ exact authentication + ↓ +receipt accepted +trusted_next_receipt_seq = N + 1 +``` + +Old, duplicate, delayed, or reordered sequence numbers fail closed. + +Authentication failure does not consume the sequence number. An authenticated receipt does consume its sequence number even when A6 subsequently rejects it as semantically stale. This prevents a correctly authenticated but unusable envelope from being replayed indefinitely against later state. + +## Deterministic discriminator + +```text +attempt 0 → UNKNOWN + ↓ +forged NOT_COMMITTED receipt seq 0 +→ AUTH_TAG reject +→ sequence remains 0 +→ UNKNOWN preserved + ↓ +exact NOT_COMMITTED receipt seq 0 +→ authenticated +→ A6 reconciliation accepted +→ sequence becomes 1 + ↓ +attempt 1 → external effect → UNKNOWN + ↓ +replayed old seq 0 receipt +→ RECEIPT_SEQUENCE reject + ↓ +foreign device receipt seq 1 +→ DEVICE_ID reject + ↓ +exact COMMITTED receipt seq 1 +→ authenticated +→ A6 terminal committed +→ sequence becomes 2 + ↓ +later attempt +→ terminal replay blocked +``` + +## Core invariants + +```text +A6_RECONCILE_VALID +=> A7_AUTH_ACCEPT +``` + +```text +A7_AUTH_ACCEPT +=> TRUST_VALID +&& EXACT_DEVICE_ID +&& EXACT_KEY_EPOCH +&& RECEIPT_SEQ == TRUSTED_NEXT_RECEIPT_SEQ_PRE +&& AUTH_TAG_MATCH +&& !SEQUENCE_EXHAUSTED +``` + +```text +AUTH_REJECT +=> NO_A6_RECONCILIATION +&& NO_TRUST_STATE_MUTATION +``` + +```text +AUTH_ACCEPT +=> TRUSTED_NEXT_RECEIPT_SEQ_POST + == TRUSTED_NEXT_RECEIPT_SEQ_PRE + 1 +``` + +```text +AUTH_ACCEPT + A6_SEMANTIC_REJECT +=> RECEIPT_SEQUENCE_CONSUMED +&& NO_A6_PERSISTENT_OUTCOME_MUTATION +``` + +```text +LOGIC_RESTART +=> TRUST_RECORD_PRESERVED +&& RECEIPT_SEQUENCE_PRESERVED +&& A6_OUTCOME_STATE_PRESERVED +``` + +## Relation to A6 + +- A6 answers: “Does this outcome evidence belong to the exact unresolved attempt, and what authority transition follows?” +- A7 answers first: “Did the trusted accelerator-device identity authenticate this exact receipt envelope at the expected monotonic sequence?” + +Together: + +```text +trusted receipt envelope +→ authenticated device provenance +→ exact A6 attempt identity +→ durable outcome transition +→ replay decision +``` + +## Claim boundary + +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. + +The rotate/XOR keyed tag is a synthetic formal device, not cryptographic security. A7 does not claim: + +- resistance to forgery under a real adversarial cryptographic model; +- SPDM, DICE, TPM, secure-element, PKI, certificate-chain, or attestation conformance; +- key secrecy or side-channel resistance; +- secure key provisioning; +- key rotation or re-attestation; +- multiple trusted devices; +- Byzantine or multi-source outcome reconciliation; +- actual NVRAM or complete power-loss persistence; +- real GPU/TPU/NPU transport; +- CDC, memory ordering, timing, PPA, liveness, production widths, or unbounded correctness. + +A7 verifies the **control-flow boundary around an authenticated receipt predicate**, not the security of a production authentication algorithm. + +## Next useful milestone + +A8 should model trust-key rotation and device re-attestation, including delayed receipts from a retired key epoch and fail-closed recovery when the trust record changes while an accelerator attempt remains unresolved. diff --git a/examples/hardware/astra-capu-v1-a7-expected.json b/examples/hardware/astra-capu-v1-a7-expected.json new file mode 100644 index 0000000..b6b4462 --- /dev/null +++ b/examples/hardware/astra-capu-v1-a7-expected.json @@ -0,0 +1,31 @@ +{ + "expected": { + "committed_receipt_applied": true, + "committed_receipt_authenticated": true, + "exact_device_identity_binding": true, + "exact_key_epoch_binding": true, + "external_effect_count": 1, + "first_attempt_forwarded": true, + "foreign_device_receipt_blocked": true, + "foreign_device_reject_code": 2, + "forged_receipt_blocked": true, + "forged_receipt_reject_code": 5, + "last_outcome": "COMMITTED", + "negative_receipt_applied": true, + "negative_receipt_authenticated": true, + "next_receipt_sequence": 2, + "persistent_next_attempt": 2, + "receipt_sequence_after_forgery": 0, + "receipt_sequence_after_negative": 1, + "result_digest_sha256": "6781dbfbd1b529866709980a3a85a38bd37f505daaddd53fd7c8e106ab863d2f", + "schema": "capu.astra.authenticated-device-receipt.result.v1.0-a7", + "stale_receipt_reject_code": 4, + "stale_receipt_replay_blocked": true, + "successor_attempt_forwarded": true, + "successor_effect_committed": true, + "synthetic_mac_model": true, + "terminal_committed": true, + "terminal_replay_blocked": true, + "terminal_replay_reject_code": 11 + } +} diff --git a/formal/astra_capu_authenticated_receipt_a7.sby b/formal/astra_capu_authenticated_receipt_a7.sby new file mode 100644 index 0000000..0a91eba --- /dev/null +++ b/formal/astra_capu_authenticated_receipt_a7.sby @@ -0,0 +1,19 @@ +[options] +mode bmc +depth 32 + +[engines] +smtbmc --unroll z3 -- --noincr + +[script] +read -formal -sv astra_capu_effect_counter_a3.sv astra_capu_persistent_outcome_store_a6.sv astra_capu_outcome_authority_shim_a6.sv astra_capu_reconciled_effect_device_a6.sv astra_capu_authenticated_receipt_gate_a7.sv astra_capu_authenticated_reconciled_effect_device_a7.sv astra_capu_authenticated_receipt_a7_formal.sv +prep -top astra_capu_authenticated_receipt_a7_formal + +[files] +rtl/astra_capu_effect_counter_a3.sv +rtl/astra_capu_persistent_outcome_store_a6.sv +rtl/astra_capu_outcome_authority_shim_a6.sv +rtl/astra_capu_reconciled_effect_device_a6.sv +rtl/astra_capu_authenticated_receipt_gate_a7.sv +rtl/astra_capu_authenticated_reconciled_effect_device_a7.sv +formal/astra_capu_authenticated_receipt_a7_formal.sv diff --git a/formal/astra_capu_authenticated_receipt_a7_cover.sby b/formal/astra_capu_authenticated_receipt_a7_cover.sby new file mode 100644 index 0000000..6a05a76 --- /dev/null +++ b/formal/astra_capu_authenticated_receipt_a7_cover.sby @@ -0,0 +1,19 @@ +[options] +mode cover +depth 56 + +[engines] +smtbmc --unroll z3 -- --noincr + +[script] +read -formal -sv astra_capu_effect_counter_a3.sv astra_capu_persistent_outcome_store_a6.sv astra_capu_outcome_authority_shim_a6.sv astra_capu_reconciled_effect_device_a6.sv astra_capu_authenticated_receipt_gate_a7.sv astra_capu_authenticated_reconciled_effect_device_a7.sv astra_capu_authenticated_receipt_a7_formal.sv +prep -top astra_capu_authenticated_receipt_a7_formal + +[files] +rtl/astra_capu_effect_counter_a3.sv +rtl/astra_capu_persistent_outcome_store_a6.sv +rtl/astra_capu_outcome_authority_shim_a6.sv +rtl/astra_capu_reconciled_effect_device_a6.sv +rtl/astra_capu_authenticated_receipt_gate_a7.sv +rtl/astra_capu_authenticated_reconciled_effect_device_a7.sv +formal/astra_capu_authenticated_receipt_a7_formal.sv diff --git a/formal/astra_capu_authenticated_receipt_a7_formal.sv b/formal/astra_capu_authenticated_receipt_a7_formal.sv new file mode 100644 index 0000000..9dd0af0 --- /dev/null +++ b/formal/astra_capu_authenticated_receipt_a7_formal.sv @@ -0,0 +1,376 @@ +module astra_capu_authenticated_receipt_a7_formal; + localparam integer DEVICE_WIDTH = 2; + localparam integer TAG_WIDTH = 2; + localparam integer ID_WIDTH = 2; + localparam integer AUTH_WIDTH = 4; + localparam integer COUNT_WIDTH = 3; + + localparam logic [2:0] AUTH_DEVICE_ID = 3'd2; + localparam logic [2:0] AUTH_KEY_EPOCH = 3'd3; + localparam logic [2:0] AUTH_SEQUENCE = 3'd4; + localparam logic [2:0] AUTH_TAG = 3'd5; + localparam logic [3:0] REJECT_OUTCOME_UNKNOWN = 4'd10; + localparam logic [3:0] REJECT_TERMINAL_COMMITTED = 4'd11; + localparam logic [2:0] OUTCOME_NOT_COMMITTED = 3'd2; + localparam logic [2:0] OUTCOME_COMMITTED = 3'd3; + + (* gclk *) logic clk; + (* anyseq *) logic cold_rst_n; + (* anyseq *) logic logic_rst_n; + + logic device_state_load_valid = 1'b0; + logic [COUNT_WIDTH-1:0] device_state_load_count = '0; + + (* anyseq *) logic trust_provision_valid; + (* anyseq *) logic [DEVICE_WIDTH-1:0] trust_provision_device_id; + (* anyseq *) logic [ID_WIDTH-1:0] trust_provision_key_epoch; + (* anyseq *) logic [AUTH_WIDTH-1:0] trust_provision_secret; + (* anyseq *) logic [ID_WIDTH-1:0] trust_provision_next_receipt_seq; + + (* anyseq *) logic provision_valid; + (* anyseq *) logic [TAG_WIDTH-1:0] provision_tag; + (* anyseq *) logic [ID_WIDTH-1:0] provision_incarnation; + (* anyseq *) logic [ID_WIDTH-1:0] provision_queue_epoch; + (* anyseq *) logic [ID_WIDTH-1:0] provision_slot_id; + (* anyseq *) logic [ID_WIDTH-1:0] provision_command_id; + (* anyseq *) logic [ID_WIDTH-1:0] provision_effect_id; + (* anyseq *) logic [ID_WIDTH-1:0] provision_next_attempt; + + (* anyseq *) logic authority_load_valid; + (* anyseq *) logic authority_load_committed; + (* anyseq *) logic [TAG_WIDTH-1:0] authority_load_tag; + (* anyseq *) logic [ID_WIDTH-1:0] authority_load_incarnation; + (* anyseq *) logic [ID_WIDTH-1:0] authority_load_queue_epoch; + (* anyseq *) logic [ID_WIDTH-1:0] authority_load_slot_id; + (* anyseq *) logic [ID_WIDTH-1:0] authority_load_command_id; + (* anyseq *) logic [ID_WIDTH-1:0] authority_load_attempt_id; + (* anyseq *) logic [ID_WIDTH-1:0] authority_load_effect_id; + + (* anyseq *) logic authority_revoke_valid; + (* anyseq *) logic [TAG_WIDTH-1:0] authority_revoke_tag; + (* anyseq *) logic [ID_WIDTH-1:0] authority_revoke_incarnation; + (* anyseq *) logic [ID_WIDTH-1:0] authority_revoke_queue_epoch; + (* anyseq *) logic [ID_WIDTH-1:0] authority_revoke_slot_id; + (* anyseq *) logic [ID_WIDTH-1:0] authority_revoke_command_id; + (* anyseq *) logic [ID_WIDTH-1:0] authority_revoke_attempt_id; + (* anyseq *) logic [ID_WIDTH-1:0] authority_revoke_effect_id; + + (* anyseq *) logic command_valid; + (* anyseq *) logic command_commit; + (* anyseq *) logic [TAG_WIDTH-1:0] command_authority_tag; + (* anyseq *) logic [ID_WIDTH-1:0] command_incarnation; + (* anyseq *) logic [ID_WIDTH-1:0] command_queue_epoch; + (* anyseq *) logic [ID_WIDTH-1:0] command_slot_id; + (* anyseq *) logic [ID_WIDTH-1:0] command_id; + (* anyseq *) logic [ID_WIDTH-1:0] command_attempt_id; + (* anyseq *) logic [ID_WIDTH-1:0] command_effect_id; + + (* anyseq *) logic receipt_valid; + (* anyseq *) logic [DEVICE_WIDTH-1:0] receipt_device_id; + (* anyseq *) logic [ID_WIDTH-1:0] receipt_key_epoch; + (* anyseq *) logic [ID_WIDTH-1:0] receipt_seq; + (* anyseq *) logic [TAG_WIDTH-1:0] receipt_authority_tag; + (* anyseq *) logic [ID_WIDTH-1:0] receipt_incarnation; + (* anyseq *) logic [ID_WIDTH-1:0] receipt_queue_epoch; + (* anyseq *) logic [ID_WIDTH-1:0] receipt_slot_id; + (* anyseq *) logic [ID_WIDTH-1:0] receipt_command_id; + (* anyseq *) logic [ID_WIDTH-1:0] receipt_attempt_id; + (* anyseq *) logic [ID_WIDTH-1:0] receipt_effect_id; + (* anyseq *) logic [2:0] receipt_outcome; + (* anyseq *) logic [AUTH_WIDTH-1:0] receipt_auth_tag; + + logic trust_provision_accept; + logic trust_provision_rejected; + logic receipt_auth_accept; + logic receipt_auth_rejected; + logic [2:0] receipt_auth_reject_code; + logic [AUTH_WIDTH-1:0] receipt_expected_auth_tag; + logic receipt_reconcile_accept; + logic receipt_reconcile_rejected; + logic [2:0] receipt_reconcile_reject_code; + logic provision_accept; + logic provision_rejected; + logic reserve_valid; + logic reserve_accept; + logic reserve_rejected; + logic frontier_exhausted; + logic authority_load_accept; + logic authority_load_rejected; + logic authority_revoke_accept; + logic authority_revoke_rejected; + logic command_forward; + logic command_rejected; + logic [3:0] command_reject_code; + logic device_command_accept; + logic device_completion_valid; + logic [COUNT_WIDTH-1:0] effect_count; + logic trusted_valid; + logic [DEVICE_WIDTH-1:0] trusted_device_id; + logic [ID_WIDTH-1:0] trusted_key_epoch; + logic [AUTH_WIDTH-1:0] trusted_secret; + logic [ID_WIDTH-1:0] trusted_next_receipt_seq; + logic receipt_sequence_exhausted; + logic persistent_valid; + logic [TAG_WIDTH-1:0] persistent_tag; + logic [ID_WIDTH-1:0] persistent_incarnation; + logic [ID_WIDTH-1:0] persistent_queue_epoch; + logic [ID_WIDTH-1:0] persistent_slot_id; + logic [ID_WIDTH-1:0] persistent_command_id; + logic [ID_WIDTH-1:0] persistent_effect_id; + logic [ID_WIDTH-1:0] persistent_next_attempt; + logic unresolved_valid; + logic [ID_WIDTH-1:0] unresolved_attempt; + logic [2:0] last_outcome; + logic [ID_WIDTH-1:0] last_resolved_attempt; + logic terminal_committed; + logic terminal_conflict; + logic active_valid; + logic active_committed; + logic attempt_spent; + logic [TAG_WIDTH-1:0] active_authority_tag; + logic [ID_WIDTH-1:0] active_incarnation; + logic [ID_WIDTH-1:0] active_queue_epoch; + logic [ID_WIDTH-1:0] active_slot_id; + logic [ID_WIDTH-1:0] active_command_id; + logic [ID_WIDTH-1:0] active_attempt_id; + logic [ID_WIDTH-1:0] active_effect_id; + + astra_capu_authenticated_reconciled_effect_device_a7 #( + .DEVICE_WIDTH(DEVICE_WIDTH), + .TAG_WIDTH(TAG_WIDTH), + .ID_WIDTH(ID_WIDTH), + .AUTH_WIDTH(AUTH_WIDTH), + .COUNT_WIDTH(COUNT_WIDTH) + ) dut (.*); + + logic f_past_valid; + logic seen_command; + logic seen_forgery_reject; + logic seen_negative_receipt; + logic seen_successor; + logic seen_stale_sequence; + logic seen_committed_receipt; + logic seen_terminal_block; + logic [ID_WIDTH-1:0] first_receipt_seq; + + initial begin + f_past_valid = 1'b0; + seen_command = 1'b0; + seen_forgery_reject = 1'b0; + seen_negative_receipt = 1'b0; + seen_successor = 1'b0; + seen_stale_sequence = 1'b0; + seen_committed_receipt = 1'b0; + seen_terminal_block = 1'b0; + end + + always @(posedge clk) begin + f_past_valid <= 1'b1; + + if (!f_past_valid) begin + assume(!cold_rst_n); + assume(!logic_rst_n); + end else begin + assume(cold_rst_n); + end + + if (!logic_rst_n) + assume(!trust_provision_valid && !provision_valid && + !authority_load_valid && !authority_revoke_valid && + !command_valid && !receipt_valid); + + assume($onehot0({trust_provision_valid, provision_valid, + authority_load_valid, authority_revoke_valid, + command_valid, receipt_valid})); + + if (cold_rst_n) begin + assert(receipt_auth_rejected == (receipt_valid && !receipt_auth_accept)); + assert(!receipt_reconcile_accept || receipt_auth_accept); + assert(!receipt_reconcile_rejected || receipt_auth_accept); + assert(device_command_accept == command_forward); + assert(device_completion_valid == (command_forward && command_commit)); + + if (receipt_auth_accept) begin + assert(trusted_valid); + assert(receipt_device_id == trusted_device_id); + assert(receipt_key_epoch == trusted_key_epoch); + assert(receipt_seq == trusted_next_receipt_seq); + assert(receipt_auth_tag == receipt_expected_auth_tag); + assert(!receipt_sequence_exhausted); + end + + if (receipt_valid && trusted_valid && + receipt_device_id != trusted_device_id) begin + assert(!receipt_auth_accept); + assert(receipt_auth_reject_code == AUTH_DEVICE_ID); + assert(!receipt_reconcile_accept); + end + + if (receipt_valid && trusted_valid && + receipt_device_id == trusted_device_id && + receipt_key_epoch != trusted_key_epoch) begin + assert(!receipt_auth_accept); + assert(receipt_auth_reject_code == AUTH_KEY_EPOCH); + assert(!receipt_reconcile_accept); + end + + if (receipt_valid && trusted_valid && + receipt_device_id == trusted_device_id && + receipt_key_epoch == trusted_key_epoch && + receipt_seq != trusted_next_receipt_seq) begin + assert(!receipt_auth_accept); + assert(receipt_auth_reject_code == AUTH_SEQUENCE); + assert(!receipt_reconcile_accept); + end + + if (receipt_valid && trusted_valid && + receipt_device_id == trusted_device_id && + receipt_key_epoch == trusted_key_epoch && + receipt_seq == trusted_next_receipt_seq && + receipt_auth_tag != receipt_expected_auth_tag && + !receipt_sequence_exhausted) begin + assert(!receipt_auth_accept); + assert(receipt_auth_reject_code == AUTH_TAG); + assert(!receipt_reconcile_accept); + end + + if (unresolved_valid && command_valid && active_valid && + active_committed && !attempt_spent && !authority_revoke_valid && + persistent_valid && + active_authority_tag == persistent_tag && + active_incarnation == persistent_incarnation && + active_queue_epoch == persistent_queue_epoch && + active_slot_id == persistent_slot_id && + active_command_id == persistent_command_id && + active_effect_id == persistent_effect_id && + !terminal_committed && !terminal_conflict && + command_authority_tag == active_authority_tag && + command_incarnation == active_incarnation && + command_queue_epoch == active_queue_epoch && + command_slot_id == active_slot_id && + command_id == active_command_id && + command_attempt_id == active_attempt_id && + command_effect_id == active_effect_id) begin + assert(!command_forward); + assert(command_reject_code == REJECT_OUTCOME_UNKNOWN); + end + + if (terminal_committed && command_valid && active_valid && + active_committed && !attempt_spent && !authority_revoke_valid && + persistent_valid && + active_authority_tag == persistent_tag && + active_incarnation == persistent_incarnation && + active_queue_epoch == persistent_queue_epoch && + active_slot_id == persistent_slot_id && + active_command_id == persistent_command_id && + active_effect_id == persistent_effect_id && + command_authority_tag == active_authority_tag && + command_incarnation == active_incarnation && + command_queue_epoch == active_queue_epoch && + command_slot_id == active_slot_id && + command_id == active_command_id && + command_attempt_id == active_attempt_id && + command_effect_id == active_effect_id) begin + assert(!command_forward); + assert(command_reject_code == REJECT_TERMINAL_COMMITTED); + end + end + + if (f_past_valid && $past(cold_rst_n)) begin + if ($past(trust_provision_accept)) begin + assert(trusted_valid); + assert(trusted_device_id == $past(trust_provision_device_id)); + assert(trusted_key_epoch == $past(trust_provision_key_epoch)); + assert(trusted_secret == $past(trust_provision_secret)); + assert(trusted_next_receipt_seq == + $past(trust_provision_next_receipt_seq)); + end + + if ($past(receipt_auth_accept)) begin + assert(trusted_next_receipt_seq == + ($past(trusted_next_receipt_seq) + + {{(ID_WIDTH-1){1'b0}}, 1'b1})); + end + + if ($past(receipt_valid && receipt_auth_rejected)) begin + assert(trusted_valid == $past(trusted_valid)); + assert(trusted_device_id == $past(trusted_device_id)); + assert(trusted_key_epoch == $past(trusted_key_epoch)); + assert(trusted_secret == $past(trusted_secret)); + assert(trusted_next_receipt_seq == + $past(trusted_next_receipt_seq)); + end + + if ($past(receipt_auth_accept && receipt_reconcile_rejected)) begin + assert(persistent_next_attempt == $past(persistent_next_attempt)); + assert(unresolved_valid == $past(unresolved_valid)); + assert(unresolved_attempt == $past(unresolved_attempt)); + assert(last_outcome == $past(last_outcome)); + assert(last_resolved_attempt == $past(last_resolved_attempt)); + assert(terminal_committed == $past(terminal_committed)); + assert(terminal_conflict == $past(terminal_conflict)); + end + + if (!$past(logic_rst_n)) begin + assert(!active_valid); + assert(!active_committed); + assert(!attempt_spent); + assert($stable(trusted_valid)); + assert($stable(trusted_device_id)); + assert($stable(trusted_key_epoch)); + assert($stable(trusted_secret)); + assert($stable(trusted_next_receipt_seq)); + assert($stable(persistent_valid)); + assert($stable(persistent_next_attempt)); + assert($stable(unresolved_valid)); + assert($stable(unresolved_attempt)); + assert($stable(last_outcome)); + assert($stable(last_resolved_attempt)); + assert($stable(terminal_committed)); + assert($stable(terminal_conflict)); + assert($stable(effect_count)); + end + end + + if (command_forward && !seen_command) + seen_command <= 1'b1; + + if (seen_command && receipt_valid && receipt_auth_rejected && + receipt_auth_reject_code == AUTH_TAG) + seen_forgery_reject <= 1'b1; + + if (seen_forgery_reject && receipt_auth_accept && + receipt_reconcile_accept && + receipt_outcome == OUTCOME_NOT_COMMITTED) begin + seen_negative_receipt <= 1'b1; + first_receipt_seq <= receipt_seq; + end + + if (seen_negative_receipt && command_forward && command_commit) + seen_successor <= 1'b1; + + if (seen_successor && receipt_valid && receipt_auth_rejected && + receipt_auth_reject_code == AUTH_SEQUENCE && + receipt_seq == first_receipt_seq) + seen_stale_sequence <= 1'b1; + + if (seen_stale_sequence && receipt_auth_accept && + receipt_reconcile_accept && + receipt_outcome == OUTCOME_COMMITTED) + seen_committed_receipt <= 1'b1; + + if (seen_committed_receipt && command_valid && command_rejected && + command_reject_code == REJECT_TERMINAL_COMMITTED) + seen_terminal_block <= 1'b1; + + cover(trust_provision_accept); + cover(provision_accept); + cover(command_forward); + cover(seen_forgery_reject); + cover(seen_negative_receipt); + cover(seen_successor); + cover(seen_stale_sequence); + cover(seen_committed_receipt); + cover(seen_terminal_block); + end +endmodule diff --git a/rtl/astra_capu_authenticated_receipt_gate_a7.sv b/rtl/astra_capu_authenticated_receipt_gate_a7.sv new file mode 100644 index 0000000..085a5fa --- /dev/null +++ b/rtl/astra_capu_authenticated_receipt_gate_a7.sv @@ -0,0 +1,184 @@ +module astra_capu_authenticated_receipt_gate_a7 #( + parameter integer DEVICE_WIDTH = 8, + parameter integer TAG_WIDTH = 8, + parameter integer ID_WIDTH = 4, + parameter integer AUTH_WIDTH = 16 +)( + input logic clk, + input logic cold_rst_n, + + input logic trust_provision_valid, + input logic [DEVICE_WIDTH-1:0] trust_provision_device_id, + input logic [ID_WIDTH-1:0] trust_provision_key_epoch, + input logic [AUTH_WIDTH-1:0] trust_provision_secret, + input logic [ID_WIDTH-1:0] trust_provision_next_receipt_seq, + + input logic receipt_valid, + input logic [DEVICE_WIDTH-1:0] receipt_device_id, + input logic [ID_WIDTH-1:0] receipt_key_epoch, + input logic [ID_WIDTH-1:0] receipt_seq, + input logic [TAG_WIDTH-1:0] receipt_authority_tag, + input logic [ID_WIDTH-1:0] receipt_incarnation, + input logic [ID_WIDTH-1:0] receipt_queue_epoch, + input logic [ID_WIDTH-1:0] receipt_slot_id, + input logic [ID_WIDTH-1:0] receipt_command_id, + input logic [ID_WIDTH-1:0] receipt_attempt_id, + input logic [ID_WIDTH-1:0] receipt_effect_id, + input logic [2:0] receipt_outcome, + input logic [AUTH_WIDTH-1:0] receipt_auth_tag, + + output logic trust_provision_accept, + output logic trust_provision_rejected, + output logic receipt_auth_accept, + output logic receipt_auth_rejected, + output logic [2:0] receipt_auth_reject_code, + output logic [AUTH_WIDTH-1:0] receipt_expected_auth_tag, + + output logic verified_reconcile_valid, + output logic [TAG_WIDTH-1:0] verified_reconcile_tag, + output logic [ID_WIDTH-1:0] verified_reconcile_incarnation, + output logic [ID_WIDTH-1:0] verified_reconcile_queue_epoch, + output logic [ID_WIDTH-1:0] verified_reconcile_slot_id, + output logic [ID_WIDTH-1:0] verified_reconcile_command_id, + output logic [ID_WIDTH-1:0] verified_reconcile_attempt_id, + output logic [ID_WIDTH-1:0] verified_reconcile_effect_id, + output logic [2:0] verified_reconcile_outcome, + + output logic trusted_valid, + output logic [DEVICE_WIDTH-1:0] trusted_device_id, + output logic [ID_WIDTH-1:0] trusted_key_epoch, + output logic [AUTH_WIDTH-1:0] trusted_secret, + output logic [ID_WIDTH-1:0] trusted_next_receipt_seq, + output logic receipt_sequence_exhausted +); + + localparam logic [2:0] AUTH_NONE = 3'd0; + localparam logic [2:0] AUTH_NO_TRUST = 3'd1; + localparam logic [2:0] AUTH_DEVICE_ID = 3'd2; + localparam logic [2:0] AUTH_KEY_EPOCH = 3'd3; + localparam logic [2:0] AUTH_SEQUENCE = 3'd4; + localparam logic [2:0] AUTH_TAG = 3'd5; + localparam logic [2:0] AUTH_EXHAUSTED = 3'd6; + + function automatic [AUTH_WIDTH-1:0] rotl1( + input [AUTH_WIDTH-1:0] value + ); + begin + rotl1 = {value[AUTH_WIDTH-2:0], value[AUTH_WIDTH-1]}; + end + endfunction + + function automatic [AUTH_WIDTH-1:0] receipt_tag_fn( + input [AUTH_WIDTH-1:0] secret_i, + input [DEVICE_WIDTH-1:0] device_id_i, + input [ID_WIDTH-1:0] key_epoch_i, + input [ID_WIDTH-1:0] receipt_seq_i, + input [TAG_WIDTH-1:0] authority_tag_i, + input [ID_WIDTH-1:0] incarnation_i, + input [ID_WIDTH-1:0] queue_epoch_i, + input [ID_WIDTH-1:0] slot_id_i, + input [ID_WIDTH-1:0] command_id_i, + input [ID_WIDTH-1:0] attempt_id_i, + input [ID_WIDTH-1:0] effect_id_i, + input [2:0] outcome_i + ); + logic [AUTH_WIDTH-1:0] acc; + begin + acc = secret_i; + acc = rotl1(acc) ^ device_id_i; + acc = rotl1(acc) ^ key_epoch_i; + acc = rotl1(acc) ^ receipt_seq_i; + acc = rotl1(acc) ^ authority_tag_i; + acc = rotl1(acc) ^ incarnation_i; + acc = rotl1(acc) ^ queue_epoch_i; + acc = rotl1(acc) ^ slot_id_i; + acc = rotl1(acc) ^ command_id_i; + acc = rotl1(acc) ^ attempt_id_i; + acc = rotl1(acc) ^ effect_id_i; + acc = rotl1(acc) ^ outcome_i; + receipt_tag_fn = acc; + end + endfunction + + always_comb begin + receipt_expected_auth_tag = receipt_tag_fn( + trusted_secret, + receipt_device_id, + receipt_key_epoch, + receipt_seq, + receipt_authority_tag, + receipt_incarnation, + receipt_queue_epoch, + receipt_slot_id, + receipt_command_id, + receipt_attempt_id, + receipt_effect_id, + receipt_outcome + ); + + receipt_sequence_exhausted = trusted_valid && (&trusted_next_receipt_seq); + + trust_provision_accept = + cold_rst_n && trust_provision_valid && !trusted_valid && !receipt_valid; + trust_provision_rejected = + trust_provision_valid && !trust_provision_accept; + + receipt_auth_accept = + cold_rst_n && receipt_valid && trusted_valid && + receipt_device_id == trusted_device_id && + receipt_key_epoch == trusted_key_epoch && + receipt_seq == trusted_next_receipt_seq && + receipt_auth_tag == receipt_expected_auth_tag && + !receipt_sequence_exhausted && + !trust_provision_valid; + receipt_auth_rejected = receipt_valid && !receipt_auth_accept; + + receipt_auth_reject_code = AUTH_NONE; + if (receipt_valid && !receipt_auth_accept) begin + if (!trusted_valid) + receipt_auth_reject_code = AUTH_NO_TRUST; + else if (receipt_device_id != trusted_device_id) + receipt_auth_reject_code = AUTH_DEVICE_ID; + else if (receipt_key_epoch != trusted_key_epoch) + receipt_auth_reject_code = AUTH_KEY_EPOCH; + else if (receipt_seq != trusted_next_receipt_seq) + receipt_auth_reject_code = AUTH_SEQUENCE; + else if (receipt_auth_tag != receipt_expected_auth_tag) + receipt_auth_reject_code = AUTH_TAG; + else if (receipt_sequence_exhausted) + receipt_auth_reject_code = AUTH_EXHAUSTED; + else + receipt_auth_reject_code = AUTH_TAG; + end + + verified_reconcile_valid = receipt_auth_accept; + verified_reconcile_tag = receipt_authority_tag; + verified_reconcile_incarnation = receipt_incarnation; + verified_reconcile_queue_epoch = receipt_queue_epoch; + verified_reconcile_slot_id = receipt_slot_id; + verified_reconcile_command_id = receipt_command_id; + verified_reconcile_attempt_id = receipt_attempt_id; + verified_reconcile_effect_id = receipt_effect_id; + verified_reconcile_outcome = receipt_outcome; + end + + always_ff @(posedge clk) begin + if (!cold_rst_n) begin + trusted_valid <= 1'b0; + trusted_device_id <= '0; + trusted_key_epoch <= '0; + trusted_secret <= '0; + trusted_next_receipt_seq <= '0; + end else if (trust_provision_accept) begin + trusted_valid <= 1'b1; + trusted_device_id <= trust_provision_device_id; + trusted_key_epoch <= trust_provision_key_epoch; + trusted_secret <= trust_provision_secret; + trusted_next_receipt_seq <= trust_provision_next_receipt_seq; + end else if (receipt_auth_accept) begin + trusted_next_receipt_seq <= + trusted_next_receipt_seq + {{(ID_WIDTH-1){1'b0}}, 1'b1}; + end + end + +endmodule diff --git a/rtl/astra_capu_authenticated_reconciled_effect_device_a7.sv b/rtl/astra_capu_authenticated_reconciled_effect_device_a7.sv new file mode 100644 index 0000000..9cd698a --- /dev/null +++ b/rtl/astra_capu_authenticated_reconciled_effect_device_a7.sv @@ -0,0 +1,291 @@ +module astra_capu_authenticated_reconciled_effect_device_a7 #( + parameter integer DEVICE_WIDTH = 8, + parameter integer TAG_WIDTH = 8, + parameter integer ID_WIDTH = 4, + parameter integer AUTH_WIDTH = 16, + parameter integer COUNT_WIDTH = 16 +)( + input logic clk, + input logic cold_rst_n, + input logic logic_rst_n, + + input logic device_state_load_valid, + input logic [COUNT_WIDTH-1:0] device_state_load_count, + + input logic trust_provision_valid, + input logic [DEVICE_WIDTH-1:0] trust_provision_device_id, + input logic [ID_WIDTH-1:0] trust_provision_key_epoch, + input logic [AUTH_WIDTH-1:0] trust_provision_secret, + input logic [ID_WIDTH-1:0] trust_provision_next_receipt_seq, + + input logic provision_valid, + input logic [TAG_WIDTH-1:0] provision_tag, + input logic [ID_WIDTH-1:0] provision_incarnation, + input logic [ID_WIDTH-1:0] provision_queue_epoch, + input logic [ID_WIDTH-1:0] provision_slot_id, + input logic [ID_WIDTH-1:0] provision_command_id, + input logic [ID_WIDTH-1:0] provision_effect_id, + input logic [ID_WIDTH-1:0] provision_next_attempt, + + input logic authority_load_valid, + input logic authority_load_committed, + input logic [TAG_WIDTH-1:0] authority_load_tag, + input logic [ID_WIDTH-1:0] authority_load_incarnation, + input logic [ID_WIDTH-1:0] authority_load_queue_epoch, + input logic [ID_WIDTH-1:0] authority_load_slot_id, + input logic [ID_WIDTH-1:0] authority_load_command_id, + input logic [ID_WIDTH-1:0] authority_load_attempt_id, + input logic [ID_WIDTH-1:0] authority_load_effect_id, + + input logic authority_revoke_valid, + input logic [TAG_WIDTH-1:0] authority_revoke_tag, + input logic [ID_WIDTH-1:0] authority_revoke_incarnation, + input logic [ID_WIDTH-1:0] authority_revoke_queue_epoch, + input logic [ID_WIDTH-1:0] authority_revoke_slot_id, + input logic [ID_WIDTH-1:0] authority_revoke_command_id, + input logic [ID_WIDTH-1:0] authority_revoke_attempt_id, + input logic [ID_WIDTH-1:0] authority_revoke_effect_id, + + input logic command_valid, + input logic command_commit, + input logic [TAG_WIDTH-1:0] command_authority_tag, + input logic [ID_WIDTH-1:0] command_incarnation, + input logic [ID_WIDTH-1:0] command_queue_epoch, + input logic [ID_WIDTH-1:0] command_slot_id, + input logic [ID_WIDTH-1:0] command_id, + input logic [ID_WIDTH-1:0] command_attempt_id, + input logic [ID_WIDTH-1:0] command_effect_id, + + input logic receipt_valid, + input logic [DEVICE_WIDTH-1:0] receipt_device_id, + input logic [ID_WIDTH-1:0] receipt_key_epoch, + input logic [ID_WIDTH-1:0] receipt_seq, + input logic [TAG_WIDTH-1:0] receipt_authority_tag, + input logic [ID_WIDTH-1:0] receipt_incarnation, + input logic [ID_WIDTH-1:0] receipt_queue_epoch, + input logic [ID_WIDTH-1:0] receipt_slot_id, + input logic [ID_WIDTH-1:0] receipt_command_id, + input logic [ID_WIDTH-1:0] receipt_attempt_id, + input logic [ID_WIDTH-1:0] receipt_effect_id, + input logic [2:0] receipt_outcome, + input logic [AUTH_WIDTH-1:0] receipt_auth_tag, + + output logic trust_provision_accept, + output logic trust_provision_rejected, + output logic receipt_auth_accept, + output logic receipt_auth_rejected, + output logic [2:0] receipt_auth_reject_code, + output logic [AUTH_WIDTH-1:0] receipt_expected_auth_tag, + output logic receipt_reconcile_accept, + output logic receipt_reconcile_rejected, + output logic [2:0] receipt_reconcile_reject_code, + + output logic provision_accept, + output logic provision_rejected, + output logic reserve_valid, + output logic reserve_accept, + output logic reserve_rejected, + output logic frontier_exhausted, + output logic authority_load_accept, + output logic authority_load_rejected, + output logic authority_revoke_accept, + output logic authority_revoke_rejected, + output logic command_forward, + output logic command_rejected, + output logic [3:0] command_reject_code, + output logic device_command_accept, + output logic device_completion_valid, + output logic [COUNT_WIDTH-1:0] effect_count, + + output logic trusted_valid, + output logic [DEVICE_WIDTH-1:0] trusted_device_id, + output logic [ID_WIDTH-1:0] trusted_key_epoch, + output logic [AUTH_WIDTH-1:0] trusted_secret, + output logic [ID_WIDTH-1:0] trusted_next_receipt_seq, + output logic receipt_sequence_exhausted, + + output logic persistent_valid, + output logic [TAG_WIDTH-1:0] persistent_tag, + output logic [ID_WIDTH-1:0] persistent_incarnation, + output logic [ID_WIDTH-1:0] persistent_queue_epoch, + output logic [ID_WIDTH-1:0] persistent_slot_id, + output logic [ID_WIDTH-1:0] persistent_command_id, + output logic [ID_WIDTH-1:0] persistent_effect_id, + output logic [ID_WIDTH-1:0] persistent_next_attempt, + output logic unresolved_valid, + output logic [ID_WIDTH-1:0] unresolved_attempt, + output logic [2:0] last_outcome, + output logic [ID_WIDTH-1:0] last_resolved_attempt, + output logic terminal_committed, + output logic terminal_conflict, + + output logic active_valid, + output logic active_committed, + output logic attempt_spent, + output logic [TAG_WIDTH-1:0] active_authority_tag, + output logic [ID_WIDTH-1:0] active_incarnation, + output logic [ID_WIDTH-1:0] active_queue_epoch, + output logic [ID_WIDTH-1:0] active_slot_id, + output logic [ID_WIDTH-1:0] active_command_id, + output logic [ID_WIDTH-1:0] active_attempt_id, + output logic [ID_WIDTH-1:0] active_effect_id +); + + logic verified_reconcile_valid; + logic [TAG_WIDTH-1:0] verified_reconcile_tag; + logic [ID_WIDTH-1:0] verified_reconcile_incarnation; + logic [ID_WIDTH-1:0] verified_reconcile_queue_epoch; + logic [ID_WIDTH-1:0] verified_reconcile_slot_id; + logic [ID_WIDTH-1:0] verified_reconcile_command_id; + logic [ID_WIDTH-1:0] verified_reconcile_attempt_id; + logic [ID_WIDTH-1:0] verified_reconcile_effect_id; + logic [2:0] verified_reconcile_outcome; + + astra_capu_authenticated_receipt_gate_a7 #( + .DEVICE_WIDTH(DEVICE_WIDTH), + .TAG_WIDTH(TAG_WIDTH), + .ID_WIDTH(ID_WIDTH), + .AUTH_WIDTH(AUTH_WIDTH) + ) receipt_gate ( + .clk(clk), + .cold_rst_n(cold_rst_n), + .trust_provision_valid(trust_provision_valid), + .trust_provision_device_id(trust_provision_device_id), + .trust_provision_key_epoch(trust_provision_key_epoch), + .trust_provision_secret(trust_provision_secret), + .trust_provision_next_receipt_seq(trust_provision_next_receipt_seq), + .receipt_valid(receipt_valid), + .receipt_device_id(receipt_device_id), + .receipt_key_epoch(receipt_key_epoch), + .receipt_seq(receipt_seq), + .receipt_authority_tag(receipt_authority_tag), + .receipt_incarnation(receipt_incarnation), + .receipt_queue_epoch(receipt_queue_epoch), + .receipt_slot_id(receipt_slot_id), + .receipt_command_id(receipt_command_id), + .receipt_attempt_id(receipt_attempt_id), + .receipt_effect_id(receipt_effect_id), + .receipt_outcome(receipt_outcome), + .receipt_auth_tag(receipt_auth_tag), + .trust_provision_accept(trust_provision_accept), + .trust_provision_rejected(trust_provision_rejected), + .receipt_auth_accept(receipt_auth_accept), + .receipt_auth_rejected(receipt_auth_rejected), + .receipt_auth_reject_code(receipt_auth_reject_code), + .receipt_expected_auth_tag(receipt_expected_auth_tag), + .verified_reconcile_valid(verified_reconcile_valid), + .verified_reconcile_tag(verified_reconcile_tag), + .verified_reconcile_incarnation(verified_reconcile_incarnation), + .verified_reconcile_queue_epoch(verified_reconcile_queue_epoch), + .verified_reconcile_slot_id(verified_reconcile_slot_id), + .verified_reconcile_command_id(verified_reconcile_command_id), + .verified_reconcile_attempt_id(verified_reconcile_attempt_id), + .verified_reconcile_effect_id(verified_reconcile_effect_id), + .verified_reconcile_outcome(verified_reconcile_outcome), + .trusted_valid(trusted_valid), + .trusted_device_id(trusted_device_id), + .trusted_key_epoch(trusted_key_epoch), + .trusted_secret(trusted_secret), + .trusted_next_receipt_seq(trusted_next_receipt_seq), + .receipt_sequence_exhausted(receipt_sequence_exhausted) + ); + + astra_capu_reconciled_effect_device_a6 #( + .TAG_WIDTH(TAG_WIDTH), + .ID_WIDTH(ID_WIDTH), + .COUNT_WIDTH(COUNT_WIDTH) + ) a6_device ( + .clk(clk), + .cold_rst_n(cold_rst_n), + .logic_rst_n(logic_rst_n), + .device_state_load_valid(device_state_load_valid), + .device_state_load_count(device_state_load_count), + .provision_valid(provision_valid), + .provision_tag(provision_tag), + .provision_incarnation(provision_incarnation), + .provision_queue_epoch(provision_queue_epoch), + .provision_slot_id(provision_slot_id), + .provision_command_id(provision_command_id), + .provision_effect_id(provision_effect_id), + .provision_next_attempt(provision_next_attempt), + .authority_load_valid(authority_load_valid), + .authority_load_committed(authority_load_committed), + .authority_load_tag(authority_load_tag), + .authority_load_incarnation(authority_load_incarnation), + .authority_load_queue_epoch(authority_load_queue_epoch), + .authority_load_slot_id(authority_load_slot_id), + .authority_load_command_id(authority_load_command_id), + .authority_load_attempt_id(authority_load_attempt_id), + .authority_load_effect_id(authority_load_effect_id), + .authority_revoke_valid(authority_revoke_valid), + .authority_revoke_tag(authority_revoke_tag), + .authority_revoke_incarnation(authority_revoke_incarnation), + .authority_revoke_queue_epoch(authority_revoke_queue_epoch), + .authority_revoke_slot_id(authority_revoke_slot_id), + .authority_revoke_command_id(authority_revoke_command_id), + .authority_revoke_attempt_id(authority_revoke_attempt_id), + .authority_revoke_effect_id(authority_revoke_effect_id), + .command_valid(command_valid), + .command_commit(command_commit), + .command_authority_tag(command_authority_tag), + .command_incarnation(command_incarnation), + .command_queue_epoch(command_queue_epoch), + .command_slot_id(command_slot_id), + .command_id(command_id), + .command_attempt_id(command_attempt_id), + .command_effect_id(command_effect_id), + .reconcile_valid(verified_reconcile_valid), + .reconcile_tag(verified_reconcile_tag), + .reconcile_incarnation(verified_reconcile_incarnation), + .reconcile_queue_epoch(verified_reconcile_queue_epoch), + .reconcile_slot_id(verified_reconcile_slot_id), + .reconcile_command_id(verified_reconcile_command_id), + .reconcile_attempt_id(verified_reconcile_attempt_id), + .reconcile_effect_id(verified_reconcile_effect_id), + .reconcile_outcome(verified_reconcile_outcome), + .provision_accept(provision_accept), + .provision_rejected(provision_rejected), + .reserve_valid(reserve_valid), + .reserve_accept(reserve_accept), + .reserve_rejected(reserve_rejected), + .reconcile_accept(receipt_reconcile_accept), + .reconcile_rejected(receipt_reconcile_rejected), + .reconcile_reject_code(receipt_reconcile_reject_code), + .frontier_exhausted(frontier_exhausted), + .authority_load_accept(authority_load_accept), + .authority_load_rejected(authority_load_rejected), + .authority_revoke_accept(authority_revoke_accept), + .authority_revoke_rejected(authority_revoke_rejected), + .command_forward(command_forward), + .command_rejected(command_rejected), + .command_reject_code(command_reject_code), + .device_command_accept(device_command_accept), + .device_completion_valid(device_completion_valid), + .effect_count(effect_count), + .persistent_valid(persistent_valid), + .persistent_tag(persistent_tag), + .persistent_incarnation(persistent_incarnation), + .persistent_queue_epoch(persistent_queue_epoch), + .persistent_slot_id(persistent_slot_id), + .persistent_command_id(persistent_command_id), + .persistent_effect_id(persistent_effect_id), + .persistent_next_attempt(persistent_next_attempt), + .unresolved_valid(unresolved_valid), + .unresolved_attempt(unresolved_attempt), + .last_outcome(last_outcome), + .last_resolved_attempt(last_resolved_attempt), + .terminal_committed(terminal_committed), + .terminal_conflict(terminal_conflict), + .active_valid(active_valid), + .active_committed(active_committed), + .attempt_spent(attempt_spent), + .active_authority_tag(active_authority_tag), + .active_incarnation(active_incarnation), + .active_queue_epoch(active_queue_epoch), + .active_slot_id(active_slot_id), + .active_command_id(active_command_id), + .active_attempt_id(active_attempt_id), + .active_effect_id(active_effect_id) + ); + +endmodule diff --git a/rtl/tb/astra_capu_authenticated_reconciled_effect_device_a7_tb.sv b/rtl/tb/astra_capu_authenticated_reconciled_effect_device_a7_tb.sv new file mode 100644 index 0000000..04f99b8 --- /dev/null +++ b/rtl/tb/astra_capu_authenticated_reconciled_effect_device_a7_tb.sv @@ -0,0 +1,483 @@ +`timescale 1ns/1ps + +module astra_capu_authenticated_reconciled_effect_device_a7_tb; + localparam integer DEVICE_WIDTH = 8; + localparam integer TAG_WIDTH = 8; + localparam integer ID_WIDTH = 4; + localparam integer AUTH_WIDTH = 16; + localparam integer COUNT_WIDTH = 16; + + localparam logic [2:0] OUTCOME_NOT_COMMITTED = 3'd2; + localparam logic [2:0] OUTCOME_COMMITTED = 3'd3; + + logic clk; + logic cold_rst_n; + logic logic_rst_n; + + logic device_state_load_valid; + logic [COUNT_WIDTH-1:0] device_state_load_count; + + logic trust_provision_valid; + logic [DEVICE_WIDTH-1:0] trust_provision_device_id; + logic [ID_WIDTH-1:0] trust_provision_key_epoch; + logic [AUTH_WIDTH-1:0] trust_provision_secret; + logic [ID_WIDTH-1:0] trust_provision_next_receipt_seq; + + logic provision_valid; + logic [TAG_WIDTH-1:0] provision_tag; + logic [ID_WIDTH-1:0] provision_incarnation; + logic [ID_WIDTH-1:0] provision_queue_epoch; + logic [ID_WIDTH-1:0] provision_slot_id; + logic [ID_WIDTH-1:0] provision_command_id; + logic [ID_WIDTH-1:0] provision_effect_id; + logic [ID_WIDTH-1:0] provision_next_attempt; + + logic authority_load_valid; + logic authority_load_committed; + logic [TAG_WIDTH-1:0] authority_load_tag; + logic [ID_WIDTH-1:0] authority_load_incarnation; + logic [ID_WIDTH-1:0] authority_load_queue_epoch; + logic [ID_WIDTH-1:0] authority_load_slot_id; + logic [ID_WIDTH-1:0] authority_load_command_id; + logic [ID_WIDTH-1:0] authority_load_attempt_id; + logic [ID_WIDTH-1:0] authority_load_effect_id; + + logic authority_revoke_valid; + logic [TAG_WIDTH-1:0] authority_revoke_tag; + logic [ID_WIDTH-1:0] authority_revoke_incarnation; + logic [ID_WIDTH-1:0] authority_revoke_queue_epoch; + logic [ID_WIDTH-1:0] authority_revoke_slot_id; + logic [ID_WIDTH-1:0] authority_revoke_command_id; + logic [ID_WIDTH-1:0] authority_revoke_attempt_id; + logic [ID_WIDTH-1:0] authority_revoke_effect_id; + + logic command_valid; + logic command_commit; + logic [TAG_WIDTH-1:0] command_authority_tag; + logic [ID_WIDTH-1:0] command_incarnation; + logic [ID_WIDTH-1:0] command_queue_epoch; + logic [ID_WIDTH-1:0] command_slot_id; + logic [ID_WIDTH-1:0] command_id; + logic [ID_WIDTH-1:0] command_attempt_id; + logic [ID_WIDTH-1:0] command_effect_id; + + logic receipt_valid; + logic [DEVICE_WIDTH-1:0] receipt_device_id; + logic [ID_WIDTH-1:0] receipt_key_epoch; + logic [ID_WIDTH-1:0] receipt_seq; + logic [TAG_WIDTH-1:0] receipt_authority_tag; + logic [ID_WIDTH-1:0] receipt_incarnation; + logic [ID_WIDTH-1:0] receipt_queue_epoch; + logic [ID_WIDTH-1:0] receipt_slot_id; + logic [ID_WIDTH-1:0] receipt_command_id; + logic [ID_WIDTH-1:0] receipt_attempt_id; + logic [ID_WIDTH-1:0] receipt_effect_id; + logic [2:0] receipt_outcome; + logic [AUTH_WIDTH-1:0] receipt_auth_tag; + + logic trust_provision_accept; + logic trust_provision_rejected; + logic receipt_auth_accept; + logic receipt_auth_rejected; + logic [2:0] receipt_auth_reject_code; + logic [AUTH_WIDTH-1:0] receipt_expected_auth_tag; + logic receipt_reconcile_accept; + logic receipt_reconcile_rejected; + logic [2:0] receipt_reconcile_reject_code; + + logic provision_accept; + logic provision_rejected; + logic reserve_valid; + logic reserve_accept; + logic reserve_rejected; + logic frontier_exhausted; + logic authority_load_accept; + logic authority_load_rejected; + logic authority_revoke_accept; + logic authority_revoke_rejected; + logic command_forward; + logic command_rejected; + logic [3:0] command_reject_code; + logic device_command_accept; + logic device_completion_valid; + logic [COUNT_WIDTH-1:0] effect_count; + + logic trusted_valid; + logic [DEVICE_WIDTH-1:0] trusted_device_id; + logic [ID_WIDTH-1:0] trusted_key_epoch; + logic [AUTH_WIDTH-1:0] trusted_secret; + logic [ID_WIDTH-1:0] trusted_next_receipt_seq; + logic receipt_sequence_exhausted; + + logic persistent_valid; + logic [TAG_WIDTH-1:0] persistent_tag; + logic [ID_WIDTH-1:0] persistent_incarnation; + logic [ID_WIDTH-1:0] persistent_queue_epoch; + logic [ID_WIDTH-1:0] persistent_slot_id; + logic [ID_WIDTH-1:0] persistent_command_id; + logic [ID_WIDTH-1:0] persistent_effect_id; + logic [ID_WIDTH-1:0] persistent_next_attempt; + logic unresolved_valid; + logic [ID_WIDTH-1:0] unresolved_attempt; + logic [2:0] last_outcome; + logic [ID_WIDTH-1:0] last_resolved_attempt; + logic terminal_committed; + logic terminal_conflict; + + logic active_valid; + logic active_committed; + logic attempt_spent; + logic [TAG_WIDTH-1:0] active_authority_tag; + logic [ID_WIDTH-1:0] active_incarnation; + logic [ID_WIDTH-1:0] active_queue_epoch; + logic [ID_WIDTH-1:0] active_slot_id; + logic [ID_WIDTH-1:0] active_command_id; + logic [ID_WIDTH-1:0] active_attempt_id; + logic [ID_WIDTH-1:0] active_effect_id; + + astra_capu_authenticated_reconciled_effect_device_a7 #( + .DEVICE_WIDTH(DEVICE_WIDTH), + .TAG_WIDTH(TAG_WIDTH), + .ID_WIDTH(ID_WIDTH), + .AUTH_WIDTH(AUTH_WIDTH), + .COUNT_WIDTH(COUNT_WIDTH) + ) dut (.*); + + always #5 clk = ~clk; + + function automatic [AUTH_WIDTH-1:0] rotl1( + input [AUTH_WIDTH-1:0] value + ); + begin + rotl1 = {value[AUTH_WIDTH-2:0], value[AUTH_WIDTH-1]}; + end + endfunction + + function automatic [AUTH_WIDTH-1:0] receipt_tag_fn( + input [DEVICE_WIDTH-1:0] device_id_i, + input [ID_WIDTH-1:0] key_epoch_i, + input [ID_WIDTH-1:0] seq_i, + input [TAG_WIDTH-1:0] authority_tag_i, + input [ID_WIDTH-1:0] incarnation_i, + input [ID_WIDTH-1:0] queue_epoch_i, + input [ID_WIDTH-1:0] slot_id_i, + input [ID_WIDTH-1:0] command_id_i, + input [ID_WIDTH-1:0] attempt_id_i, + input [ID_WIDTH-1:0] effect_id_i, + input [2:0] outcome_i + ); + logic [AUTH_WIDTH-1:0] acc; + begin + acc = 16'hBEEF; + acc = rotl1(acc) ^ device_id_i; + acc = rotl1(acc) ^ key_epoch_i; + acc = rotl1(acc) ^ seq_i; + acc = rotl1(acc) ^ authority_tag_i; + acc = rotl1(acc) ^ incarnation_i; + acc = rotl1(acc) ^ queue_epoch_i; + acc = rotl1(acc) ^ slot_id_i; + acc = rotl1(acc) ^ command_id_i; + acc = rotl1(acc) ^ attempt_id_i; + acc = rotl1(acc) ^ effect_id_i; + acc = rotl1(acc) ^ outcome_i; + receipt_tag_fn = acc; + end + endfunction + + task automatic clear_controls; + begin + device_state_load_valid = 1'b0; + device_state_load_count = '0; + trust_provision_valid = 1'b0; + provision_valid = 1'b0; + authority_load_valid = 1'b0; + authority_revoke_valid = 1'b0; + command_valid = 1'b0; + command_commit = 1'b0; + receipt_valid = 1'b0; + receipt_auth_tag = '0; + end + endtask + + task automatic set_lineage; + begin + trust_provision_device_id = 8'h3C; + trust_provision_key_epoch = 4'd2; + trust_provision_secret = 16'hBEEF; + trust_provision_next_receipt_seq = 4'd0; + + provision_tag = 8'hA7; + provision_incarnation = 4'd2; + provision_queue_epoch = 4'd7; + provision_slot_id = 4'd1; + provision_command_id = 4'd9; + provision_effect_id = 4'd12; + provision_next_attempt = 4'd0; + + authority_load_tag = provision_tag; + authority_load_incarnation = provision_incarnation; + authority_load_queue_epoch = provision_queue_epoch; + authority_load_slot_id = provision_slot_id; + authority_load_command_id = provision_command_id; + authority_load_effect_id = provision_effect_id; + + command_authority_tag = provision_tag; + command_incarnation = provision_incarnation; + command_queue_epoch = provision_queue_epoch; + command_slot_id = provision_slot_id; + command_id = provision_command_id; + command_effect_id = provision_effect_id; + + receipt_device_id = trust_provision_device_id; + receipt_key_epoch = trust_provision_key_epoch; + receipt_authority_tag = provision_tag; + receipt_incarnation = provision_incarnation; + receipt_queue_epoch = provision_queue_epoch; + receipt_slot_id = provision_slot_id; + receipt_command_id = provision_command_id; + receipt_effect_id = provision_effect_id; + + authority_revoke_tag = provision_tag; + authority_revoke_incarnation = provision_incarnation; + authority_revoke_queue_epoch = provision_queue_epoch; + authority_revoke_slot_id = provision_slot_id; + authority_revoke_command_id = provision_command_id; + authority_revoke_effect_id = provision_effect_id; + end + endtask + + task automatic pulse_trust_provision; + logic accept_seen; + begin + @(negedge clk); + trust_provision_valid = 1'b1; + #1 accept_seen = trust_provision_accept; + @(posedge clk); #1; + trust_provision_valid = 1'b0; + if (!accept_seen || !trusted_valid || + trusted_device_id != 8'h3C || + trusted_key_epoch != 4'd2 || + trusted_next_receipt_seq != 4'd0) + $fatal(1, "A7 trust provision failed"); + end + endtask + + task automatic pulse_provision; + logic accept_seen; + begin + @(negedge clk); + provision_valid = 1'b1; + #1 accept_seen = provision_accept; + @(posedge clk); #1; + provision_valid = 1'b0; + if (!accept_seen || !persistent_valid || persistent_next_attempt != 4'd0) + $fatal(1, "A7 outcome-store provision failed"); + end + endtask + + task automatic pulse_load( + input logic [ID_WIDTH-1:0] attempt + ); + logic accept_seen; + begin + @(negedge clk); + authority_load_attempt_id = attempt; + authority_load_committed = 1'b1; + authority_load_valid = 1'b1; + #1 accept_seen = authority_load_accept; + @(posedge clk); #1; + authority_load_valid = 1'b0; + if (!accept_seen || !active_valid || active_attempt_id != attempt) + $fatal(1, "A7 authority load failed"); + end + endtask + + task automatic pulse_command( + input logic [ID_WIDTH-1:0] attempt, + input logic commit_effect, + output logic forward_seen, + output logic [3:0] reject_seen + ); + begin + @(negedge clk); + command_attempt_id = attempt; + command_commit = commit_effect; + command_valid = 1'b1; + #1; + forward_seen = command_forward; + reject_seen = command_reject_code; + @(posedge clk); #1; + command_valid = 1'b0; + command_commit = 1'b0; + end + endtask + + task automatic pulse_receipt( + input logic [DEVICE_WIDTH-1:0] device_id_i, + input logic [ID_WIDTH-1:0] key_epoch_i, + input logic [ID_WIDTH-1:0] seq_i, + input logic [ID_WIDTH-1:0] attempt_i, + input logic [2:0] outcome_i, + input logic forge_tag, + output logic auth_seen, + output logic [2:0] auth_reject_seen, + output logic reconcile_seen, + output logic [2:0] reconcile_reject_seen + ); + logic [AUTH_WIDTH-1:0] exact_tag; + begin + @(negedge clk); + receipt_device_id = device_id_i; + receipt_key_epoch = key_epoch_i; + receipt_seq = seq_i; + receipt_attempt_id = attempt_i; + receipt_outcome = outcome_i; + exact_tag = receipt_tag_fn( + device_id_i, + key_epoch_i, + seq_i, + receipt_authority_tag, + receipt_incarnation, + receipt_queue_epoch, + receipt_slot_id, + receipt_command_id, + attempt_i, + receipt_effect_id, + outcome_i + ); + receipt_auth_tag = forge_tag ? (exact_tag ^ 16'd1) : exact_tag; + receipt_valid = 1'b1; + #1; + auth_seen = receipt_auth_accept; + auth_reject_seen = receipt_auth_reject_code; + reconcile_seen = receipt_reconcile_accept; + reconcile_reject_seen = receipt_reconcile_reject_code; + @(posedge clk); #1; + receipt_valid = 1'b0; + receipt_auth_tag = '0; + end + endtask + + task automatic pulse_logic_reset; + begin + @(negedge clk); + logic_rst_n = 1'b0; + @(posedge clk); #1; + @(negedge clk); + logic_rst_n = 1'b1; + @(posedge clk); #1; + end + endtask + + logic forward_seen; + logic [3:0] command_reject_seen; + logic auth_seen; + logic [2:0] auth_reject_seen; + logic reconcile_seen; + logic [2:0] reconcile_reject_seen; + + initial begin + clk = 1'b0; + cold_rst_n = 1'b0; + logic_rst_n = 1'b0; + clear_controls(); + set_lineage(); + authority_load_attempt_id = '0; + authority_load_committed = 1'b0; + authority_revoke_attempt_id = '0; + command_attempt_id = '0; + receipt_seq = '0; + receipt_attempt_id = '0; + receipt_outcome = '0; + + repeat (2) @(posedge clk); + @(negedge clk); + cold_rst_n = 1'b1; + logic_rst_n = 1'b1; + @(posedge clk); #1; + + pulse_trust_provision(); + pulse_provision(); + + pulse_load(4'd0); + pulse_command(4'd0, 1'b0, forward_seen, command_reject_seen); + if (!forward_seen || effect_count != 16'd0 || + !unresolved_valid || last_outcome != 3'd1) + $fatal(1, "A7 attempt 0 did not enter UNKNOWN"); + $display("a7_attempt0_forwarded outcome=UNKNOWN effect_count=%0d", effect_count); + + pulse_receipt(8'h3C, 4'd2, 4'd0, 4'd0, + OUTCOME_NOT_COMMITTED, 1'b1, + auth_seen, auth_reject_seen, + reconcile_seen, reconcile_reject_seen); + if (auth_seen || auth_reject_seen != 3'd5 || + trusted_next_receipt_seq != 4'd0 || !unresolved_valid) + $fatal(1, "A7 forged receipt was not rejected"); + $display("a7_forged_receipt_blocked reject_code=%0d next_receipt_seq=%0d", + auth_reject_seen, trusted_next_receipt_seq); + + pulse_receipt(8'h3C, 4'd2, 4'd0, 4'd0, + OUTCOME_NOT_COMMITTED, 1'b0, + auth_seen, auth_reject_seen, + reconcile_seen, reconcile_reject_seen); + if (!auth_seen || !reconcile_seen || + trusted_next_receipt_seq != 4'd1 || unresolved_valid || + last_outcome != OUTCOME_NOT_COMMITTED) + $fatal(1, "A7 exact negative receipt failed"); + $display("a7_negative_receipt_authenticated seq=0 outcome=NOT_COMMITTED next_receipt_seq=%0d", + trusted_next_receipt_seq); + + pulse_logic_reset(); + pulse_load(4'd1); + pulse_command(4'd1, 1'b1, forward_seen, command_reject_seen); + if (!forward_seen || effect_count != 16'd1 || + !unresolved_valid || unresolved_attempt != 4'd1) + $fatal(1, "A7 successor attempt failed"); + $display("a7_attempt1_forwarded outcome=UNKNOWN effect_count=%0d", effect_count); + + pulse_logic_reset(); + pulse_receipt(8'h3C, 4'd2, 4'd0, 4'd0, + OUTCOME_NOT_COMMITTED, 1'b0, + auth_seen, auth_reject_seen, + reconcile_seen, reconcile_reject_seen); + if (auth_seen || auth_reject_seen != 3'd4 || + trusted_next_receipt_seq != 4'd1 || !unresolved_valid) + $fatal(1, "A7 stale receipt sequence was not rejected"); + $display("a7_stale_receipt_replay_blocked reject_code=%0d next_receipt_seq=%0d", + auth_reject_seen, trusted_next_receipt_seq); + + pulse_receipt(8'h3D, 4'd2, 4'd1, 4'd1, + OUTCOME_COMMITTED, 1'b0, + auth_seen, auth_reject_seen, + reconcile_seen, reconcile_reject_seen); + if (auth_seen || auth_reject_seen != 3'd2 || + trusted_next_receipt_seq != 4'd1 || !unresolved_valid) + $fatal(1, "A7 foreign device receipt was not rejected"); + $display("a7_foreign_device_receipt_blocked reject_code=%0d next_receipt_seq=%0d", + auth_reject_seen, trusted_next_receipt_seq); + + pulse_receipt(8'h3C, 4'd2, 4'd1, 4'd1, + OUTCOME_COMMITTED, 1'b0, + auth_seen, auth_reject_seen, + reconcile_seen, reconcile_reject_seen); + if (!auth_seen || !reconcile_seen || + trusted_next_receipt_seq != 4'd2 || !terminal_committed || + last_outcome != OUTCOME_COMMITTED) + $fatal(1, "A7 exact committed receipt failed"); + $display("a7_committed_receipt_authenticated seq=1 terminal_committed=%0d next_receipt_seq=%0d", + terminal_committed, trusted_next_receipt_seq); + + pulse_logic_reset(); + pulse_load(4'd2); + pulse_command(4'd2, 1'b1, forward_seen, command_reject_seen); + if (forward_seen || command_reject_seen != 4'd11 || effect_count != 16'd1) + $fatal(1, "A7 terminal replay was not blocked"); + $display("a7_terminal_replay_blocked reject_code=%0d effect_count=%0d", + command_reject_seen, effect_count); + + $display("a7_summary external_effect_count=%0d persistent_next_attempt=%0d next_receipt_seq=%0d last_outcome=COMMITTED", + effect_count, persistent_next_attempt, trusted_next_receipt_seq); + $display("ASTRA_CAPU_V1_A7_AUTHENTICATED_DEVICE_RECEIPT_PASS"); + $finish; + end +endmodule diff --git a/schemas/hardware/astra-capu-authenticated-device-receipt-v1.0-a7.schema.json b/schemas/hardware/astra-capu-authenticated-device-receipt-v1.0-a7.schema.json new file mode 100644 index 0000000..ba76e17 --- /dev/null +++ b/schemas/hardware/astra-capu-authenticated-device-receipt-v1.0-a7.schema.json @@ -0,0 +1,65 @@ +{ + "$schema": "https://json-schema.org/draft/2020-12/schema", + "$id": "https://example.invalid/capu/astra-capu-authenticated-device-receipt-v1.0-a7.schema.json", + "title": "ASTRA–CaPU Authenticated Device Receipt v1.0-A7 Result", + "type": "object", + "additionalProperties": false, + "required": [ + "schema", + "first_attempt_forwarded", + "forged_receipt_blocked", + "forged_receipt_reject_code", + "receipt_sequence_after_forgery", + "negative_receipt_authenticated", + "negative_receipt_applied", + "receipt_sequence_after_negative", + "successor_attempt_forwarded", + "successor_effect_committed", + "stale_receipt_replay_blocked", + "stale_receipt_reject_code", + "foreign_device_receipt_blocked", + "foreign_device_reject_code", + "committed_receipt_authenticated", + "committed_receipt_applied", + "terminal_committed", + "terminal_replay_blocked", + "terminal_replay_reject_code", + "external_effect_count", + "persistent_next_attempt", + "next_receipt_sequence", + "last_outcome", + "synthetic_mac_model", + "exact_device_identity_binding", + "exact_key_epoch_binding", + "result_digest_sha256" + ], + "properties": { + "schema": {"const": "capu.astra.authenticated-device-receipt.result.v1.0-a7"}, + "first_attempt_forwarded": {"const": true}, + "forged_receipt_blocked": {"const": true}, + "forged_receipt_reject_code": {"const": 5}, + "receipt_sequence_after_forgery": {"const": 0}, + "negative_receipt_authenticated": {"const": true}, + "negative_receipt_applied": {"const": true}, + "receipt_sequence_after_negative": {"const": 1}, + "successor_attempt_forwarded": {"const": true}, + "successor_effect_committed": {"const": true}, + "stale_receipt_replay_blocked": {"const": true}, + "stale_receipt_reject_code": {"const": 4}, + "foreign_device_receipt_blocked": {"const": true}, + "foreign_device_reject_code": {"const": 2}, + "committed_receipt_authenticated": {"const": true}, + "committed_receipt_applied": {"const": true}, + "terminal_committed": {"const": true}, + "terminal_replay_blocked": {"const": true}, + "terminal_replay_reject_code": {"const": 11}, + "external_effect_count": {"const": 1}, + "persistent_next_attempt": {"const": 2}, + "next_receipt_sequence": {"const": 2}, + "last_outcome": {"const": "COMMITTED"}, + "synthetic_mac_model": {"const": true}, + "exact_device_identity_binding": {"const": true}, + "exact_key_epoch_binding": {"const": true}, + "result_digest_sha256": {"type": "string", "pattern": "^[0-9a-f]{64}$"} + } +} diff --git a/tests/test_astra_capu_authenticated_receipt_a7.py b/tests/test_astra_capu_authenticated_receipt_a7.py new file mode 100644 index 0000000..b0a6a69 --- /dev/null +++ b/tests/test_astra_capu_authenticated_receipt_a7.py @@ -0,0 +1,252 @@ +import unittest + +from tools.astra_capu_authenticated_receipt_a7 import ( + A7Controller, + DeviceReceipt, + ReceiptRejectCode, + TrustedDeviceStore, + synthetic_receipt_tag, + scenario_result, +) +from tools.astra_capu_outcome_reconciliation_a6 import ( + A6Controller, + AuthorityToken, + Outcome, + PersistentOutcomeStore, + ReconcileRejectCode, + RejectCode, +) + + +class AuthenticatedDeviceReceiptA7Tests(unittest.TestCase): + SECRET = 0xBEEF + DEVICE_ID = 0x3C + KEY_EPOCH = 2 + + def token(self, attempt: int = 0, **changes): + values = dict( + authority_tag=0xA7, + incarnation=2, + queue_epoch=7, + slot_id=1, + command_id=9, + attempt_id=attempt, + effect_id=12, + committed=True, + ) + values.update(changes) + return AuthorityToken(**values) + + def receipt( + self, + token: AuthorityToken, + *, + seq: int, + outcome: Outcome, + device_id: int | None = None, + key_epoch: int | None = None, + secret: int | None = None, + ) -> DeviceReceipt: + return DeviceReceipt.signed( + secret=self.SECRET if secret is None else secret, + device_id=self.DEVICE_ID if device_id is None else device_id, + key_epoch=self.KEY_EPOCH if key_epoch is None else key_epoch, + receipt_seq=seq, + authority_tag=token.authority_tag, + incarnation=token.incarnation, + queue_epoch=token.queue_epoch, + slot_id=token.slot_id, + command_id=token.command_id, + attempt_id=token.attempt_id, + effect_id=token.effect_id, + outcome=outcome, + ) + + def stack(self): + token = self.token() + outcome_store = PersistentOutcomeStore(width_bits=4) + self.assertTrue(outcome_store.provision(token, next_attempt=0)) + a6 = A6Controller(outcome_store) + trust = TrustedDeviceStore( + self.DEVICE_ID, + self.KEY_EPOCH, + self.SECRET, + ) + return token, outcome_store, a6, trust, A7Controller(a6, trust) + + def enter_unknown(self): + token, store, a6, trust, a7 = self.stack() + self.assertTrue(a6.load(token)) + decision = a6.dispatch(token, commit_effect=False) + self.assertTrue(decision.forwarded) + self.assertTrue(store.unresolved_valid) + return token, store, a6, trust, a7 + + def test_synthetic_tag_is_deterministic(self): + fields = [0x3C, 2, 0, 0xA7, 2, 7, 1, 9, 0, 12, 2] + self.assertEqual( + synthetic_receipt_tag(self.SECRET, fields), + synthetic_receipt_tag(self.SECRET, fields), + ) + self.assertNotEqual( + synthetic_receipt_tag(self.SECRET, fields), + synthetic_receipt_tag(self.SECRET ^ 1, fields), + ) + + def test_forged_tag_is_rejected_without_sequence_advance(self): + token, store, _, trust, a7 = self.enter_unknown() + exact = self.receipt(token, seq=0, outcome=Outcome.NOT_COMMITTED) + forged = DeviceReceipt( + **{**exact.__dict__, "auth_tag": exact.auth_tag ^ 1} + ) + decision = a7.process_receipt(forged) + self.assertFalse(decision.authenticated) + self.assertEqual(decision.auth_reject_code, ReceiptRejectCode.AUTH_TAG) + self.assertEqual(trust.next_receipt_seq, 0) + self.assertTrue(store.unresolved_valid) + + def test_wrong_device_is_rejected(self): + token, store, _, trust, a7 = self.enter_unknown() + receipt = self.receipt( + token, + seq=0, + outcome=Outcome.NOT_COMMITTED, + device_id=self.DEVICE_ID + 1, + ) + decision = a7.process_receipt(receipt) + self.assertFalse(decision.authenticated) + self.assertEqual(decision.auth_reject_code, ReceiptRejectCode.DEVICE_ID) + self.assertEqual(trust.next_receipt_seq, 0) + self.assertTrue(store.unresolved_valid) + + def test_wrong_key_epoch_is_rejected(self): + token, store, _, trust, a7 = self.enter_unknown() + receipt = self.receipt( + token, + seq=0, + outcome=Outcome.NOT_COMMITTED, + key_epoch=self.KEY_EPOCH + 1, + ) + decision = a7.process_receipt(receipt) + self.assertFalse(decision.authenticated) + self.assertEqual(decision.auth_reject_code, ReceiptRejectCode.KEY_EPOCH) + self.assertEqual(trust.next_receipt_seq, 0) + self.assertTrue(store.unresolved_valid) + + def test_exact_negative_receipt_releases_successor(self): + token0, store, a6, trust, a7 = self.enter_unknown() + receipt = self.receipt(token0, seq=0, outcome=Outcome.NOT_COMMITTED) + decision = a7.process_receipt(receipt) + self.assertTrue(decision.authenticated) + self.assertTrue(decision.reconcile_accept) + self.assertEqual(trust.next_receipt_seq, 1) + self.assertFalse(store.unresolved_valid) + self.assertEqual(store.last_outcome, Outcome.NOT_COMMITTED) + + token1 = self.token(1) + a6.logic_reset() + self.assertTrue(a6.load(token1)) + successor = a6.dispatch(token1, commit_effect=True) + self.assertTrue(successor.forwarded) + self.assertEqual(a6.external_effect_count, 1) + + def test_authenticated_receipt_consumes_sequence_on_semantic_reject(self): + token0, store, _, trust, a7 = self.enter_unknown() + stale_token = self.token(1) + receipt = self.receipt( + stale_token, + seq=0, + outcome=Outcome.COMMITTED, + ) + decision = a7.process_receipt(receipt) + self.assertTrue(decision.authenticated) + self.assertFalse(decision.reconcile_accept) + self.assertEqual( + decision.reconcile_reject_code, + ReconcileRejectCode.ATTEMPT_MISMATCH, + ) + self.assertEqual(trust.next_receipt_seq, 1) + self.assertTrue(store.unresolved_valid) + self.assertFalse(store.terminal_committed) + + def test_receipt_sequence_replay_is_rejected(self): + token, store, _, trust, a7 = self.enter_unknown() + receipt = self.receipt(token, seq=0, outcome=Outcome.NOT_COMMITTED) + first = a7.process_receipt(receipt) + second = a7.process_receipt(receipt) + self.assertTrue(first.authenticated) + self.assertFalse(second.authenticated) + self.assertEqual( + second.auth_reject_code, + ReceiptRejectCode.RECEIPT_SEQUENCE, + ) + self.assertEqual(trust.next_receipt_seq, 1) + self.assertFalse(store.unresolved_valid) + + def test_exact_committed_receipt_terminally_closes_lineage(self): + token0, store, a6, trust, a7 = self.enter_unknown() + negative = self.receipt(token0, seq=0, outcome=Outcome.NOT_COMMITTED) + self.assertTrue(a7.process_receipt(negative).reconcile_accept) + + token1 = self.token(1) + a6.logic_reset() + a6.load(token1) + a6.dispatch(token1, commit_effect=True) + committed = self.receipt(token1, seq=1, outcome=Outcome.COMMITTED) + decision = a7.process_receipt(committed) + self.assertTrue(decision.authenticated) + self.assertTrue(decision.reconcile_accept) + self.assertTrue(store.terminal_committed) + self.assertEqual(trust.next_receipt_seq, 2) + + token2 = self.token(2) + a6.logic_reset() + a6.load(token2) + replay = a6.dispatch(token2, commit_effect=True) + self.assertFalse(replay.forwarded) + self.assertEqual(replay.reject_code, RejectCode.TERMINAL_COMMITTED) + self.assertEqual(a6.external_effect_count, 1) + + def test_exact_conflict_receipt_fails_closed(self): + token, store, a6, _, a7 = self.enter_unknown() + receipt = self.receipt(token, seq=0, outcome=Outcome.CONFLICT) + decision = a7.process_receipt(receipt) + self.assertTrue(decision.authenticated) + self.assertTrue(decision.reconcile_accept) + self.assertTrue(store.terminal_conflict) + + token1 = self.token(1) + a6.logic_reset() + a6.load(token1) + retry = a6.dispatch(token1, commit_effect=True) + self.assertFalse(retry.forwarded) + self.assertEqual(retry.reject_code, RejectCode.TERMINAL_CONFLICT) + + def test_logic_restart_preserves_trust_sequence_and_outcome(self): + token, store, a6, trust, a7 = self.enter_unknown() + receipt = self.receipt(token, seq=0, outcome=Outcome.NOT_COMMITTED) + a7.process_receipt(receipt) + a6.logic_reset() + self.assertEqual(trust.next_receipt_seq, 1) + self.assertEqual(trust.trusted_device_id, self.DEVICE_ID) + self.assertEqual(trust.trusted_key_epoch, self.KEY_EPOCH) + self.assertEqual(store.last_outcome, Outcome.NOT_COMMITTED) + + def test_scenario_result(self): + result = scenario_result() + self.assertTrue(result["forged_receipt_blocked"]) + self.assertTrue(result["negative_receipt_authenticated"]) + self.assertTrue(result["negative_receipt_applied"]) + self.assertTrue(result["stale_receipt_replay_blocked"]) + self.assertTrue(result["foreign_device_receipt_blocked"]) + self.assertTrue(result["committed_receipt_authenticated"]) + self.assertTrue(result["committed_receipt_applied"]) + self.assertTrue(result["terminal_replay_blocked"]) + self.assertEqual(result["external_effect_count"], 1) + self.assertEqual(result["next_receipt_sequence"], 2) + self.assertEqual(result["last_outcome"], "COMMITTED") + self.assertEqual(len(result["result_digest_sha256"]), 64) + + +if __name__ == "__main__": + unittest.main() diff --git a/tools/astra_capu_authenticated_receipt_a7.py b/tools/astra_capu_authenticated_receipt_a7.py new file mode 100644 index 0000000..b79dcf7 --- /dev/null +++ b/tools/astra_capu_authenticated_receipt_a7.py @@ -0,0 +1,354 @@ +"""Deterministic software mirror for ASTRA–CaPU v1.0-A7. + +A7 adds an authenticated device-receipt boundary in front of the A6 durable +outcome reconciler. The model uses a deliberately small synthetic keyed tag, +not production cryptography. It verifies device identity, key epoch, monotonic +receipt sequence, exact attempt identity and tag before exposing outcome +evidence to A6. +""" + +from __future__ import annotations + +from dataclasses import dataclass +from enum import IntEnum +import hashlib +import json + +from tools.astra_capu_outcome_reconciliation_a6 import ( + A6Controller, + AuthorityToken, + Outcome, + PersistentOutcomeStore, + ReconcileRejectCode, +) + + +class ReceiptRejectCode(IntEnum): + NONE = 0 + TRUST_MISSING = 1 + DEVICE_ID = 2 + KEY_EPOCH = 3 + RECEIPT_SEQUENCE = 4 + AUTH_TAG = 5 + + +OUTCOME_CODE = { + Outcome.NONE: 0, + Outcome.UNKNOWN: 1, + Outcome.NOT_COMMITTED: 2, + Outcome.COMMITTED: 3, + Outcome.CONFLICT: 4, +} + + +def rotate_left(value: int, width_bits: int, amount: int = 1) -> int: + mask = (1 << width_bits) - 1 + amount %= width_bits + return ((value << amount) | (value >> (width_bits - amount))) & mask + + +def synthetic_receipt_tag( + secret: int, + fields: list[int], + *, + width_bits: int = 16, +) -> int: + """Return the exact synthetic keyed tag mirrored by the A7 RTL. + + This rotation/XOR construction is intentionally transparent and is not a + cryptographic MAC. It exists only to exercise authenticated-envelope state + transitions and anti-replay sequence semantics in a bounded model. + """ + + mask = (1 << width_bits) - 1 + tag = secret & mask + for field in fields: + tag = rotate_left(tag, width_bits) ^ (field & mask) + return tag & mask + + +@dataclass(frozen=True) +class DeviceReceipt: + device_id: int + key_epoch: int + receipt_seq: int + authority_tag: int + incarnation: int + queue_epoch: int + slot_id: int + command_id: int + attempt_id: int + effect_id: int + outcome: Outcome + auth_tag: int + + def token(self) -> AuthorityToken: + return AuthorityToken( + self.authority_tag, + self.incarnation, + self.queue_epoch, + self.slot_id, + self.command_id, + self.attempt_id, + self.effect_id, + True, + ) + + def auth_fields(self) -> list[int]: + return [ + self.device_id, + self.key_epoch, + self.receipt_seq, + self.authority_tag, + self.incarnation, + self.queue_epoch, + self.slot_id, + self.command_id, + self.attempt_id, + self.effect_id, + OUTCOME_CODE[self.outcome], + ] + + def expected_tag(self, secret: int, *, width_bits: int = 16) -> int: + return synthetic_receipt_tag( + secret, + self.auth_fields(), + width_bits=width_bits, + ) + + @classmethod + def signed( + cls, + *, + secret: int, + width_bits: int = 16, + **values: object, + ) -> "DeviceReceipt": + unsigned = cls(auth_tag=0, **values) + return cls( + **values, + auth_tag=unsigned.expected_tag(secret, width_bits=width_bits), + ) + + +@dataclass +class TrustedDeviceStore: + trusted_device_id: int + trusted_key_epoch: int + secret: int + next_receipt_seq: int = 0 + auth_width_bits: int = 16 + valid: bool = True + + def authenticate(self, receipt: DeviceReceipt) -> ReceiptRejectCode: + if not self.valid: + return ReceiptRejectCode.TRUST_MISSING + if receipt.device_id != self.trusted_device_id: + return ReceiptRejectCode.DEVICE_ID + if receipt.key_epoch != self.trusted_key_epoch: + return ReceiptRejectCode.KEY_EPOCH + if receipt.receipt_seq != self.next_receipt_seq: + return ReceiptRejectCode.RECEIPT_SEQUENCE + if receipt.auth_tag != receipt.expected_tag( + self.secret, + width_bits=self.auth_width_bits, + ): + return ReceiptRejectCode.AUTH_TAG + + # An authenticated receipt consumes its monotonic sequence number even + # when the downstream A6 semantic reconciler rejects it as stale. + self.next_receipt_seq += 1 + return ReceiptRejectCode.NONE + + +@dataclass(frozen=True) +class ReceiptDecision: + authenticated: bool + auth_reject_code: ReceiptRejectCode + reconcile_accept: bool + reconcile_reject_code: ReconcileRejectCode + + +class A7Controller: + def __init__( + self, + a6: A6Controller, + trust: TrustedDeviceStore, + ) -> None: + self.a6 = a6 + self.trust = trust + + def process_receipt(self, receipt: DeviceReceipt) -> ReceiptDecision: + auth = self.trust.authenticate(receipt) + if auth is not ReceiptRejectCode.NONE: + return ReceiptDecision( + False, + auth, + False, + ReconcileRejectCode.NONE, + ) + + reconcile = self.a6.store.reconcile( + receipt.token(), + receipt.outcome, + ) + return ReceiptDecision( + True, + ReceiptRejectCode.NONE, + reconcile is ReconcileRejectCode.NONE, + reconcile, + ) + + +def canonical_digest(value: dict[str, object]) -> str: + encoded = json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + return hashlib.sha256(encoded).hexdigest() + + +def scenario_result() -> dict[str, object]: + secret = 0xBEEF + device_id = 0x3C + key_epoch = 2 + + token0 = AuthorityToken(0xA7, 2, 7, 1, 9, 0, 12, True) + token1 = AuthorityToken(0xA7, 2, 7, 1, 9, 1, 12, True) + token2 = AuthorityToken(0xA7, 2, 7, 1, 9, 2, 12, True) + + store = PersistentOutcomeStore(width_bits=4) + controller = A6Controller(store) + trust = TrustedDeviceStore(device_id, key_epoch, secret) + a7 = A7Controller(controller, trust) + + assert store.provision(token0, next_attempt=0) + assert controller.load(token0) + first = controller.dispatch(token0, commit_effect=False) + + exact_negative = DeviceReceipt.signed( + secret=secret, + device_id=device_id, + key_epoch=key_epoch, + receipt_seq=0, + authority_tag=token0.authority_tag, + incarnation=token0.incarnation, + queue_epoch=token0.queue_epoch, + slot_id=token0.slot_id, + command_id=token0.command_id, + attempt_id=token0.attempt_id, + effect_id=token0.effect_id, + outcome=Outcome.NOT_COMMITTED, + ) + forged_negative = DeviceReceipt( + **{ + **exact_negative.__dict__, + "auth_tag": exact_negative.auth_tag ^ 1, + } + ) + + forged = a7.process_receipt(forged_negative) + sequence_after_forgery = trust.next_receipt_seq + negative = a7.process_receipt(exact_negative) + sequence_after_negative = trust.next_receipt_seq + + controller.logic_reset() + assert controller.load(token1) + successor = controller.dispatch(token1, commit_effect=True) + controller.logic_reset() + + stale_replay = a7.process_receipt(exact_negative) + + foreign_device = DeviceReceipt.signed( + secret=secret, + device_id=device_id + 1, + key_epoch=key_epoch, + receipt_seq=1, + authority_tag=token1.authority_tag, + incarnation=token1.incarnation, + queue_epoch=token1.queue_epoch, + slot_id=token1.slot_id, + command_id=token1.command_id, + attempt_id=token1.attempt_id, + effect_id=token1.effect_id, + outcome=Outcome.COMMITTED, + ) + foreign = a7.process_receipt(foreign_device) + + exact_committed = DeviceReceipt.signed( + secret=secret, + device_id=device_id, + key_epoch=key_epoch, + receipt_seq=1, + authority_tag=token1.authority_tag, + incarnation=token1.incarnation, + queue_epoch=token1.queue_epoch, + slot_id=token1.slot_id, + command_id=token1.command_id, + attempt_id=token1.attempt_id, + effect_id=token1.effect_id, + outcome=Outcome.COMMITTED, + ) + committed = a7.process_receipt(exact_committed) + + controller.logic_reset() + assert controller.load(token2) + terminal_replay = controller.dispatch(token2, commit_effect=True) + + result: dict[str, object] = { + "schema": "capu.astra.authenticated-device-receipt.result.v1.0-a7", + "first_attempt_forwarded": first.forwarded, + "forged_receipt_blocked": not forged.authenticated, + "forged_receipt_reject_code": int(forged.auth_reject_code), + "receipt_sequence_after_forgery": sequence_after_forgery, + "negative_receipt_authenticated": negative.authenticated, + "negative_receipt_applied": negative.reconcile_accept, + "receipt_sequence_after_negative": sequence_after_negative, + "successor_attempt_forwarded": successor.forwarded, + "successor_effect_committed": successor.effect_committed, + "stale_receipt_replay_blocked": not stale_replay.authenticated, + "stale_receipt_reject_code": int(stale_replay.auth_reject_code), + "foreign_device_receipt_blocked": not foreign.authenticated, + "foreign_device_reject_code": int(foreign.auth_reject_code), + "committed_receipt_authenticated": committed.authenticated, + "committed_receipt_applied": committed.reconcile_accept, + "terminal_committed": store.terminal_committed, + "terminal_replay_blocked": not terminal_replay.forwarded, + "terminal_replay_reject_code": int(terminal_replay.reject_code), + "external_effect_count": controller.external_effect_count, + "persistent_next_attempt": store.next_attempt, + "next_receipt_sequence": trust.next_receipt_seq, + "last_outcome": store.last_outcome.value, + "synthetic_mac_model": True, + "exact_device_identity_binding": True, + "exact_key_epoch_binding": True, + } + result["result_digest_sha256"] = canonical_digest(result) + return result + + +def main() -> None: + result = scenario_result() + print("a7_attempt0_forwarded outcome=UNKNOWN effect_count=0") + print( + "a7_forged_receipt_blocked " + f"reject_code={result['forged_receipt_reject_code']} next_receipt_seq=0" + ) + print("a7_negative_receipt_authenticated seq=0 outcome=NOT_COMMITTED next_receipt_seq=1") + print("a7_attempt1_forwarded outcome=UNKNOWN effect_count=1") + print( + "a7_stale_receipt_replay_blocked " + f"reject_code={result['stale_receipt_reject_code']} next_receipt_seq=1" + ) + print( + "a7_foreign_device_receipt_blocked " + f"reject_code={result['foreign_device_reject_code']} next_receipt_seq=1" + ) + print("a7_committed_receipt_authenticated seq=1 terminal_committed=1 next_receipt_seq=2") + print( + "a7_terminal_replay_blocked " + f"reject_code={result['terminal_replay_reject_code']} effect_count=1" + ) + print(json.dumps(result, sort_keys=True)) + print("ASTRA_CAPU_V1_A7_AUTHENTICATED_DEVICE_RECEIPT_PASS") + + +if __name__ == "__main__": + main()