Invariants

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

Download the source artifact

# Invariants Registry
# OpenFreytProtocol — machine-readable safety and security invariants
#
# Fields per entry:
#   id          — stable identifier, format INV-NNN
#   title       — short human name
#   requirement — linked requirement ID(s)
#   statement   — the invariant in plain terms (what must always be true)
#   type        — safety | security | liveness | consistency
#   formal      — true if this is modeled in formal/tla/
#   tests       — list of test IDs that verify this invariant
#   status      — active | deprecated

invariants:

  - id: INV-001
    title: No commitment without all required decisions
    requirement: [R-002]
    statement: >
      For any proposal P, a commitment record for P cannot exist unless every decision
      required by the bilateral policy of P's relationship has been recorded as accepted.
    type: safety
    formal: true
    tests: []
    status: active

  - id: INV-002
    title: No commitment after valid withdrawal or expiry
    requirement: [R-002]
    statement: >
      If a withdrawal or expiry event for offer O or proposal P has been accepted,
      no subsequent command can produce a commitment record referencing O or P.
    type: safety
    formal: true
    tests: []
    status: active

  - id: INV-003
    title: Idempotency — one key, one effect
    requirement: [R-002, R-003]
    statement: >
      A command bearing idempotency key K produces the same effect on every replay.
      Duplicate delivery of K cannot produce two different effects or two different
      commitment records.
    type: consistency
    formal: true
    tests: []
    status: active

  - id: INV-004
    title: Unauthorized organization cannot observe protected resource
    requirement: [R-001]
    statement: >
      For any organization O and resource R, if O is not an authorized participant
      in the relationship owning R, then O receives no data from R in any API response,
      event, or audit record.
    type: security
    formal: false
    tests: []
    status: active

  - id: INV-005
    title: Duplicate or reordered events cannot regress resource state
    requirement: [R-003]
    statement: >
      Receiving the same event twice, or receiving events out of causal order,
      must not move a resource to an earlier lifecycle state or erase an accepted decision.
    type: consistency
    formal: true
    tests: []
    status: active

  - id: INV-006
    title: Evidence deduplication — one execution, one contribution
    requirement: [R-003]
    statement: >
      A single execution record cannot contribute to avoided-kilometre totals or
      evidence aggregations more than once, regardless of how many times the
      evidence record is submitted.
    type: consistency
    formal: true
    tests: []
    status: active

  - id: INV-007
    title: Corrections are append-only
    requirement: [R-003]
    statement: >
      A correction command produces a new superseding record that references the
      prior record. The prior record is never mutated or deleted.
    type: safety
    formal: false
    tests: []
    status: active

  - id: INV-008
    title: One handover creates at most one destination execution
    requirement: [R-007, R-009]
    statement: >
      Replaying or reordering delivery of one execution handover cannot create a
      second destination execution record or a conflicting acknowledgement.
    type: consistency
    formal: true
    tests: []
    status: active

  - id: INV-009
    title: Accepted terms cannot change silently
    requirement: [R-010]
    statement: >
      No amendment or counterproposal can replace the decision-relevant payload of
      an accepted tender revision without preserving the accepted snapshot and
      recording every renewed decision required by bilateral policy.
    type: safety
    formal: true
    tests: []
    status: active

  - id: INV-010
    title: Authenticated organization binding cannot be overridden
    requirement: [R-001, R-008]
    statement: >
      For every connector command, the effective organization is the organization
      bound to the authenticated connector registration. No payload, external
      reference, tenant field, or callback can change that effective organization.
    type: security
    formal: false
    tests: []
    status: active

  - id: INV-011
    title: Commitment and handover remain distinct
    requirement: [R-007]
    statement: >
      Creating a commitment cannot by itself place the corresponding handover in an
      imported or linked state. Only an authorized destination acknowledgement can
      establish technical handover success.
    type: safety
    formal: true
    tests: []
    status: active