# Traceability Registry # OpenFreytProtocol — links requirements and invariants to tests and evidence # # CI fails when: # - a critical requirement from requirements.yaml has no entry here # - an entry references a test file that does not exist # - an invariant marked formal:true has no tla_model entry # # Fields per entry: # requirement — R-NNN from requirements.yaml (or INV-NNN for invariant entries) # criticality — mirrors requirements.yaml criticality (used by CI check) # evidence: # unit_tests — list of test file paths # property_tests — list of test file paths # integration_tests — list of test file paths # conformance_tests — list of test file paths # tla_model — path to TLA+ spec (required when invariants.yaml formal: true) # status — pending | partial | covered # notes — free text traceability: # ── Requirements R-001 through R-015 ────────────────────────────────────── - requirement: R-001 criticality: critical evidence: unit_tests: [] property_tests: [] integration_tests: [] conformance_tests: [] tla_model: ~ status: pending notes: > Coverage provided by security/authorization-matrix.md (9 scopes × 7 resources × 4 roles) and conformance isolation tests that verify cross-organization access returns HTTP 403. Both artifacts are planned for the assurance-foundation milestone. - requirement: R-002 criticality: critical evidence: unit_tests: [] property_tests: [] integration_tests: [] conformance_tests: [] tla_model: formal/tla/LifecycleSafety.tla status: pending notes: > Formal model formal/tla/LifecycleSafety.tla verifies the no-commitment-without-decision invariant (INV-001, INV-002). Integration tests for concurrent accept/reject/withdraw race resolution and commitment invariant tests are planned for the assurance-foundation milestone. - requirement: R-003 criticality: critical evidence: unit_tests: [] property_tests: [] integration_tests: [] conformance_tests: [] tla_model: ~ status: pending notes: > Coverage provided by formal/tla/LifecycleSafety.tla (INV-005, INV-006, INV-007) and append-only persistence integration tests that verify correction commands produce superseding records referencing prior records. No PUT/PATCH contract test planned. - requirement: R-004 criticality: critical evidence: unit_tests: [] property_tests: [] integration_tests: [] conformance_tests: [] tla_model: ~ status: pending notes: > Coverage provided by conformance/README.md and the black-box conformance suite skeleton. Suite must run without importing reference-broker or Freyt-client code. Interoperability demonstration deferred to stable-release milestone. - requirement: R-005 criticality: critical evidence: unit_tests: [] property_tests: [] integration_tests: [] conformance_tests: [] tla_model: ~ status: pending notes: > Coverage provided by specification/schemas/ and field-level disclosure contract tests that assert pre-match API responses contain no customer name, exact address, or price fields. Schema examples to be verified against disclosure rules. - requirement: R-006 criticality: critical evidence: unit_tests: [] property_tests: [] integration_tests: [] conformance_tests: [] tla_model: formal/tla/LifecycleSafety.tla status: pending notes: > Coverage provided by formal/tla/LifecycleSafety.tla (INV-003: idempotency invariant) and contract tests replaying each mutating operation with an identical Idempotency-Key. Tests will verify same response body and 2xx, plus 422 on key collision across different organizations or operation types. - requirement: R-007 criticality: high evidence: unit_tests: [] property_tests: [] integration_tests: [] conformance_tests: [] tla_model: ~ status: pending notes: > Coverage provided by integration tests verifying that a command referencing a prior resourceVersion returns HTTP 409 Conflict with application/problem+json body, and that a successful command increments the version. Concurrent update race test planned. - requirement: R-008 criticality: high evidence: unit_tests: [] property_tests: [] integration_tests: [] conformance_tests: [] tla_model: ~ status: pending notes: > Coverage provided by specification/schemas/ and schema diff tooling in CI. Compatibility gate must detect removal or type change of any existing field. A minor-version bump adding an optional field must pass the diff check. - requirement: R-009 criticality: high evidence: unit_tests: [] property_tests: [] integration_tests: [] conformance_tests: [] tla_model: ~ status: pending notes: > Coverage provided by contract tests on match proposal responses that verify the compatibility-checks array includes pass/fail/abstain per check. A deterministic re-run property test verifies identical inputs produce identical results. Missing vehicle-type abstain case verified by unit test. - requirement: R-010 criticality: high evidence: unit_tests: [] property_tests: [] integration_tests: [] conformance_tests: [] tla_model: ~ status: pending notes: > Coverage provided by specification/errors/ error catalogue (all protocol-specific problem types) and contract tests validating every 4xx/5xx response carries Content-Type application/problem+json with type, title, status, detail, and instance fields as defined by RFC 9457. - requirement: R-011 criticality: medium evidence: unit_tests: [] property_tests: [] integration_tests: [] conformance_tests: [] tla_model: ~ status: pending notes: > Coverage provided by LICENSE file at repository root and docs/adr/ directory. CI gate verifies schema and conformance directories carry the declared license header. All normative changes tracked as ADRs; current decisions referenced via D001-D012. - requirement: R-012 criticality: critical evidence: unit_tests: [] property_tests: [] integration_tests: [] conformance_tests: [] tla_model: formal/tla/LifecycleSafety.tla status: pending notes: > Coverage provided directly by formal/tla/LifecycleSafety.tla verified by TLC with zero violations. Model covers all six invariants INV-001 through INV-006 and all state transitions in offer, request, proposal, and commitment lifecycle. CI TLC verification step planned for assurance-foundation milestone. - requirement: R-013 criticality: high evidence: unit_tests: [] property_tests: [] integration_tests: [] conformance_tests: [] tla_model: ~ status: pending notes: > Coverage provided by specification review confirming no Freyt-owned identifier registry reference, conformance test demonstrating broker-scoped organizationId accepted without Freyt lookup, and schema validation rejecting proprietary namespace field types. - requirement: R-014 criticality: critical evidence: unit_tests: [] property_tests: [] integration_tests: [] conformance_tests: [] tla_model: ~ status: pending notes: > Coverage provided by security/threat-model.md (at least one threat entry per protocol resource) and security/abuse-cases.md (at least one abuse case per authentication boundary). CI gate verifies both files exist before any implementation PR is merged. Both artifacts planned for assurance-foundation milestone. - requirement: R-015 criticality: critical evidence: unit_tests: [] property_tests: [] integration_tests: [] conformance_tests: [] tla_model: ~ status: pending notes: > Coverage provided by security/authorization-matrix.md covering all 9 OAuth scopes, 7 protocol resources, and 4 roles with explicit allow/deny/condition per cell. CI gate verifies matrix completeness. Contract test validates at least one allow and one deny path per resource per role. # ── Invariants INV-001 through INV-007 ──────────────────────────────────── - requirement: INV-001 criticality: critical evidence: unit_tests: [] property_tests: [] integration_tests: [] conformance_tests: - conformance/src/profiles/consumer/commitment-safety.suite.ts - conformance/src/profiles/consumer/race-conditions.suite.ts tla_model: formal/tla/LifecycleSafety.tla status: verified notes: > Formal property: no commitment record can exist unless every required decision has been recorded as accepted. Verified by TLC against formal/tla/LifecycleSafety.tla and by executable checkInv001 predicate assertions in the Consumer conformance suite. - requirement: INV-002 criticality: critical evidence: unit_tests: [] property_tests: [] integration_tests: [] conformance_tests: - conformance/src/profiles/consumer/commitment-safety.suite.ts - conformance/src/profiles/consumer/race-conditions.suite.ts tla_model: formal/tla/LifecycleSafety.tla status: verified notes: > Formal property: no command can produce a commitment referencing a withdrawn or expired offer or proposal. Verified by TLC against formal/tla/LifecycleSafety.tla and by executable checkInv002 predicate assertions in the Consumer conformance suite. - requirement: INV-003 criticality: critical evidence: unit_tests: [] property_tests: [] integration_tests: [] conformance_tests: [] tla_model: formal/tla/LifecycleSafety.tla status: verified notes: > Formal property: a command bearing idempotency key K produces the same effect on every replay. Verified by TLC against formal/tla/LifecycleSafety.tla. - requirement: INV-004 criticality: critical evidence: unit_tests: [] property_tests: [] integration_tests: [] conformance_tests: [] tla_model: formal/tla/LifecycleSafety.tla status: verified notes: > Security invariant: unauthorized organization receives no data from protected resources. Formally modeled as OrganizationIsolation in formal/tla/LifecycleSafety.tla (verified by TLC, 0 violations, 10,296 distinct states). Full coverage also requires authorization-matrix conformance tests and integration isolation tests. - requirement: INV-005 criticality: critical evidence: unit_tests: [] property_tests: [] integration_tests: [] conformance_tests: [] tla_model: formal/tla/LifecycleSafety.tla status: verified notes: > Formal property: duplicate or reordered events cannot regress resource state. Verified by TLC against formal/tla/LifecycleSafety.tla. - requirement: INV-006 criticality: critical evidence: unit_tests: [] property_tests: [] integration_tests: [] conformance_tests: [] tla_model: formal/tla/LifecycleSafety.tla status: verified notes: > Formal property: a single execution record cannot contribute to evidence aggregations more than once. Verified by TLC against formal/tla/LifecycleSafety.tla. - requirement: INV-007 criticality: high evidence: unit_tests: [] property_tests: [] integration_tests: [] conformance_tests: [] tla_model: ~ status: pending notes: > Safety invariant: corrections are append-only; the prior record is never mutated. Not formally modeled (formal: false); verified by append-only persistence integration tests and correction-command contract tests. # ── Requirements R-016 through R-021 (merged from main) ─────────────────── - requirement: R-016 criticality: high evidence: unit_tests: [] property_tests: [] integration_tests: - scripts/check-content.mjs - scripts/sync-docs.mjs conformance_tests: - .github/workflows/docs.yml tla_model: ~ status: verified notes: pnpm check validates content, synchronizes canonical sources, type-checks the site, and builds the static artifact. - requirement: R-017 criticality: critical evidence: unit_tests: [] property_tests: [] integration_tests: [] conformance_tests: [] tla_model: formal/tla/LifecycleSafety.tla status: pending notes: Handover schema, destination deduplication, acknowledgement, and quarantine tests are pending. - requirement: R-018 criticality: critical evidence: unit_tests: [] property_tests: [] integration_tests: [] conformance_tests: [] tla_model: ~ status: pending notes: Organization binding and layered authorization matrix tests are pending. - requirement: R-019 criticality: critical evidence: unit_tests: [] property_tests: [] integration_tests: [] conformance_tests: [] tla_model: formal/tla/LifecycleSafety.tla status: pending notes: Duplicate, reorder, outage, dead-letter, and reconciliation tests are pending. - requirement: R-020 criticality: critical evidence: unit_tests: [] property_tests: [] integration_tests: [] conformance_tests: [] tla_model: formal/tla/LifecycleSafety.tla status: pending notes: Tender revision, renewed acceptance, cancellation race, and accepted-snapshot tests are pending. - requirement: R-021 criticality: high evidence: unit_tests: [] property_tests: [] integration_tests: [] conformance_tests: [] tla_model: ~ status: pending notes: Capability document schema and independent-client negotiation tests are pending. # ── Invariants INV-008 through INV-011 (merged from main) ───────────────── - requirement: INV-008 criticality: critical evidence: unit_tests: [] property_tests: [] integration_tests: [] conformance_tests: [] tla_model: formal/tla/LifecycleSafety.tla status: pending notes: Formal and integration proof of one destination execution per handover is pending. - requirement: INV-009 criticality: critical evidence: unit_tests: [] property_tests: [] integration_tests: [] conformance_tests: [] tla_model: formal/tla/LifecycleSafety.tla status: pending notes: Formal proof that accepted decision terms cannot change silently is pending. - requirement: INV-010 criticality: critical evidence: unit_tests: [] property_tests: [] integration_tests: [] conformance_tests: [] tla_model: ~ status: pending notes: Cross-organization payload override and callback isolation tests are pending. - requirement: INV-011 criticality: critical evidence: unit_tests: [] property_tests: [] integration_tests: [] conformance_tests: [] tla_model: formal/tla/LifecycleSafety.tla status: pending notes: Formal proof that commitment cannot imply destination import is pending.