Traceability

Generated from requirements/traceability.yaml. Edit the canonical source file, not this page.

Download the source artifact

# 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.