Purpose

Define deterministic, verifier-grade invariants for Settlement domain validation aligned to the canonical dual recordType model:

• SETTLEMENT_INTENT
• SETTLEMENT_EVENT

Scope

This specification applies to governance-layer settlement validation over append-only ledger history. It covers intent creation, event authorization, event ordering, metadata traceability, and cross-domain prerequisites. It does not define execution-layer fund movement.

Definitions

• L: ordered ledger entries by append index.
• subjectId: composite identifier in format <SubjectType>:<SubjectId>.
• policyHash: policy binding hash referenced by settlement records and decisions.
• Intent: record where recordType = SETTLEMENT_INTENT and action = SETTLEMENT.CREATE.
• Event: record where recordType = SETTLEMENT_EVENT and action = SETTLEMENT.<EVENT_TYPE>.
• Decision tuple: (subjectId, action, policyHash) resolved by latest matching ACCESS_DECISION.

Normative Rules

A) Ledger Structure Invariants

1. A1: Append Immutability

• Formal statement: forall i < |L|, entry_i is immutable after append.
• Applies to: all settlement-related records.
• Failure code suggestion: LEDGER_IMMUTABILITY_VIOLATION.
• Minimal counterexample ledger:

[0] SETTLEMENT_INTENT(subjectId=AUCTION:A-1, action=SETTLEMENT.CREATE)
[0'] same index mutated with different policyHash

2. A2: Ordered Replay Determinism

• Formal statement: Replay(L) = Replay(L) under identical L and canonical parsing.
• Applies to: SETTLEMENT_INTENT, SETTLEMENT_EVENT.
• Failure code suggestion: NON_DETERMINISTIC_REPLAY.
• Minimal counterexample ledger:

[0] SETTLEMENT_EVENT(action=SETTLEMENT.ESCROW_OPENED)
[1] SETTLEMENT_EVENT(action=SETTLEMENT.DEPOSIT_CONFIRMED)
Verifier A sorts by timestamp, Verifier B sorts by append index -> divergent output

3. A3: Canonical RecordType Parsing

• Formal statement: recordType in {SETTLEMENT_INTENT, SETTLEMENT_EVENT} for settlement domain records.
• Applies to: settlement domain entries.
• Failure code suggestion: INVALID_SETTLEMENT_RECORDTYPE.
• Minimal counterexample ledger:

[0] recordType=<non-canonical value>, action=SETTLEMENT.CREATE

B) Authorization Invariants

4. B1: Intent Requires ALLOW

• Formal statement: Intent exists at k => exists j < k: Decision(subjectId, SETTLEMENT.CREATE, policyHash) = ALLOW and latest decision before k is ALLOW.
• Applies to: SETTLEMENT_INTENT, action SETTLEMENT.CREATE.
• Failure code suggestion: MISSING_ALLOW_DECISION or DENIED_BY_LATEST_DECISION.
• Minimal counterexample ledger:

[0] SETTLEMENT_INTENT(subjectId=AUCTION:A-1, policyHash=P1, action=SETTLEMENT.CREATE)

5. B2: Event Requires Action-Matching ALLOW

• Formal statement: Event(action=E) at k => latest ACCESS_DECISION(subjectId, E, policyHash) before k is ALLOW.
• Applies to: SETTLEMENT_EVENT, all event actions.
• Failure code suggestion: MISSING_ALLOW_DECISION or DENIED_BY_LATEST_DECISION.
• Minimal counterexample ledger:

[0] ACCESS_DECISION(ALLOW, action=SETTLEMENT.CREATE, subjectId=AUCTION:A-1, policyHash=P1)
[1] SETTLEMENT_EVENT(action=SETTLEMENT.ESCROW_OPENED, subjectId=AUCTION:A-1, policyHash=P1)

6. B3: PolicyHash Binding Consistency

• Formal statement: forall settlement records r, authorization decisions for r must match r.policyHash.
• Applies to: SETTLEMENT_INTENT, SETTLEMENT_EVENT.
• Failure code suggestion: POLICYHASH_MISMATCH.
• Minimal counterexample ledger:

[0] ACCESS_DECISION(ALLOW, subjectId=AUCTION:A-1, action=SETTLEMENT.CREATE, policyHash=P1)
[1] SETTLEMENT_INTENT(subjectId=AUCTION:A-1, action=SETTLEMENT.CREATE, policyHash=P2)

C) Lifecycle Ordering Invariants

7. C1: Escrow-before-Deposit When Escrow Required

• Formal statement: escrowRequired=true and DEPOSIT_CONFIRMED at k => exists j < k with ESCROW_OPENED.
• Applies to: SETTLEMENT_EVENT actions SETTLEMENT.ESCROW_OPENED, SETTLEMENT.DEPOSIT_CONFIRMED.
• Failure code suggestion: DEPOSIT_BEFORE_ESCROW_OPENED.
• Minimal counterexample ledger:

[0] SETTLEMENT_INTENT(metadata.escrowRequired=true)
[1] SETTLEMENT_EVENT(action=SETTLEMENT.DEPOSIT_CONFIRMED)

8. C2: Release Execution Requires Prior Request (same milestone)

• Formal statement: RELEASE_EXECUTED(m) at k => exists j < k with RELEASE_REQUESTED(m).
• Applies to: SETTLEMENT_EVENT release actions.
• Failure code suggestion: RELEASE_EXECUTED_BEFORE_REQUESTED.
• Minimal counterexample ledger:

[0] SETTLEMENT_EVENT(action=SETTLEMENT.RELEASE_EXECUTED, metadata.milestoneId=M1)

9. C3: No Release After Refund

• Formal statement: exists j: REFUND_EXECUTED at j => for all k > j, action(k) not in {RELEASE_REQUESTED, RELEASE_EXECUTED}.
• Applies to: SETTLEMENT_EVENT refund/release actions.
• Failure code suggestion: RELEASE_AFTER_REFUND.
• Minimal counterexample ledger:

[0] SETTLEMENT_EVENT(action=SETTLEMENT.REFUND_EXECUTED)
[1] SETTLEMENT_EVENT(action=SETTLEMENT.RELEASE_REQUESTED)

D) Metadata Trace Invariants

10. D1: Decision Trace Presence on Events

• Formal statement: forall SETTLEMENT_EVENT e, metadata contains authDecisionEntryHash and authDecisionPayloadHash.
• Applies to: SETTLEMENT_EVENT.
• Failure code suggestion: MISSING_AUTH_TRACE.
• Minimal counterexample ledger:

[0] ACCESS_DECISION(ALLOW, action=SETTLEMENT.ESCROW_OPENED)
[1] SETTLEMENT_EVENT(action=SETTLEMENT.ESCROW_OPENED, metadata without authDecisionEntryHash)

11. D2: Trace Consistency with Resolved Decision

• Formal statement: event.metadata.authDecisionEntryHash == resolvedDecision.entryHash and event.metadata.authDecisionPayloadHash == resolvedDecision.payloadHash.
• Applies to: SETTLEMENT_EVENT.
• Failure code suggestion: AUTH_TRACE_MISMATCH.
• Minimal counterexample ledger:

[0] ACCESS_DECISION(ALLOW, action=SETTLEMENT.DEPOSIT_CONFIRMED, entryHash=H1, payloadHash=P1)
[1] SETTLEMENT_EVENT(action=SETTLEMENT.DEPOSIT_CONFIRMED, metadata.authDecisionEntryHash=H2)

E) Cross-Domain Invariants

12. E1: Policy Freeze Prerequisite

• Formal statement: settlement record using policyHash p => exists earlier POLICY_FREEZE(policyHash=p).
• Applies to: SETTLEMENT_INTENT, SETTLEMENT_EVENT.
• Failure code suggestion: POLICY_NOT_FROZEN.
• Minimal counterexample ledger:

[0] SETTLEMENT_INTENT(policyHash=P1, action=SETTLEMENT.CREATE)

13. E2: Parent Process Closure Prerequisite

• Formal statement: subjectId=AUCTION:x => AUCTION state CLOSED before SETTLEMENT_INTENT; subjectId=TENDER:y => TENDER closure equivalent before SETTLEMENT_INTENT.
• Applies to: SETTLEMENT_INTENT.
• Failure code suggestion: PARENT_NOT_CLOSED.
• Minimal counterexample ledger:

[0] AUCTION_TRANSITION(from=CREATED,to=OPEN,subjectId=AUCTION:A-1)
[1] SETTLEMENT_INTENT(subjectId=AUCTION:A-1, action=SETTLEMENT.CREATE)

14. E3: Optional KES Binding Prerequisite

• Formal statement: if settlement references kesVersionHash then matching KES_VERSION_RATIFIED must exist earlier.
• Applies to: settlement records with KES references.
• Failure code suggestion: KES_NOT_RATIFIED.
• Minimal counterexample ledger:

[0] SETTLEMENT_INTENT(metadata.kesVersionHash=K1)

Mapping to Code

• Intent authorization: packages/core/settlement/verifySettlementAuthorization.ts
• Event authorization: packages/core/settlement/verifySettlementEventAuthorization.ts
• Lifecycle ordering: packages/core/settlement/verifySettlementLifecycle.ts
• Record construction/appending: packages/core/settlement/buildSettlementIntentRecord.ts, buildSettlementEventRecord.ts, appendSettlementIntent.ts, appendSettlementEvent.ts

Non-normative Notes

• Invariant failure codes are suggested canonical identifiers and can be mapped to implementation-specific error surfaces.
• Cross-domain checks may be implemented in governance-wide integrity validators, but outcomes must remain deterministic and ledger-only.

Testability

• Each invariant MUST have at least one negative test with the listed minimal counterexample shape.
• Replay tests SHOULD include mixed valid/invalid event streams for same subjectId and for unrelated subjectId values.
• Authorization tests MUST cover latest-decision-wins behavior with ALLOW->DENY and DENY->ALLOW sequences.
• Trace integrity tests MUST assert exact hash equality for decision references.

Verification Strategy

A deterministic verifier processes ledger L in append order and for each settlement subject:

1. Project intent and event records by subjectId.
2. Resolve authorization tuples from ACCESS_DECISION using latest-decision-wins.
3. Apply lifecycle constraints in one pass over projected events.
4. Validate trace metadata presence and consistency.
5. Apply cross-domain prerequisites using previously derived domain states.
6. Return {valid, errors[]} with stable error ordering by ledger index.