SETTLEMENT_FORMAL_VERIFICATION_INVARIANTS.md

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

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

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

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

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)

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)

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

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)

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)

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

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)

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

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)

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)

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:

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

Field	Type	Required	Sample value
recordId	TEXT	Yes	F-CT-01-EXAMPLE-001
procedureInstanceId	TEXT	Yes	F-CT-01-EXAMPLE-001
recordedAt	DATE	Yes	2026-02-20
evidenceSummary	TEXTAREA	Yes	F-CT-01-EXAMPLE-001

Field	Type	Required	Sample value
recordId	TEXT	Yes	F-CT-02-EXAMPLE-001
procedureInstanceId	TEXT	Yes	F-CT-02-EXAMPLE-001
recordedAt	DATE	Yes	2026-02-20
evidenceSummary	TEXTAREA	Yes	F-CT-02-EXAMPLE-001

Field	Type	Required	Sample value
recordId	TEXT	Yes	F-CT-03-EXAMPLE-001
procedureInstanceId	TEXT	Yes	F-CT-03-EXAMPLE-001
recordedAt	DATE	Yes	2026-02-20
evidenceSummary	TEXTAREA	Yes	F-CT-03-EXAMPLE-001

Field	Type	Required	Sample value
recordId	TEXT	Yes	F-CT-04-EXAMPLE-001
procedureInstanceId	TEXT	Yes	F-CT-04-EXAMPLE-001
recordedAt	DATE	Yes	2026-02-20
evidenceSummary	TEXTAREA	Yes	F-CT-04-EXAMPLE-001

Field	Type	Required	Sample value
recordId	TEXT	Yes	F-CT-05-EXAMPLE-001
procedureInstanceId	TEXT	Yes	F-CT-05-EXAMPLE-001
recordedAt	DATE	Yes	2026-02-20
evidenceSummary	TEXTAREA	Yes	F-CT-05-EXAMPLE-001

Field	Type	Required	Sample value
recordId	TEXT	Yes	F-CT-06-EXAMPLE-001
procedureInstanceId	TEXT	Yes	F-CT-06-EXAMPLE-001
recordedAt	DATE	Yes	2026-02-20
evidenceSummary	TEXTAREA	Yes	F-CT-06-EXAMPLE-001

Field	Type	Required	Sample value
recordId	TEXT	Yes	F-CT-07-EXAMPLE-001
procedureInstanceId	TEXT	Yes	F-CT-07-EXAMPLE-001
recordedAt	DATE	Yes	2026-02-20
evidenceSummary	TEXTAREA	Yes	F-CT-07-EXAMPLE-001

Field	Type	Required	Sample value
recordId	TEXT	Yes	F-CT-08-EXAMPLE-001
procedureInstanceId	TEXT	Yes	F-CT-08-EXAMPLE-001
recordedAt	DATE	Yes	2026-02-20
evidenceSummary	TEXTAREA	Yes	F-CT-08-EXAMPLE-001
conditionTrigger	TEXT	No	N/A

Field	Type	Required	Sample value
recordId	TEXT	Yes	F-CT-09-EXAMPLE-001
procedureInstanceId	TEXT	Yes	F-CT-09-EXAMPLE-001
recordedAt	DATE	Yes	2026-02-20
evidenceSummary	TEXTAREA	Yes	F-CT-09-EXAMPLE-001

Field	Type	Required	Sample value
recordId	TEXT	Yes	F-IP-04-01-EXAMPLE-001
procedureInstanceId	TEXT	Yes	F-IP-04-01-EXAMPLE-001
recordedAt	DATE	Yes	2026-02-20
evidenceSummary	TEXTAREA	Yes	F-IP-04-01-EXAMPLE-001

Field	Type	Required	Sample value
recordId	TEXT	Yes	F-PR-01-01-EXAMPLE-001
procedureInstanceId	TEXT	Yes	F-PR-01-01-EXAMPLE-001
recordedAt	DATE	Yes	2026-02-20
evidenceSummary	TEXTAREA	Yes	F-PR-01-01-EXAMPLE-001

Field	Type	Required	Sample value
recordId	TEXT	Yes	F-PR-01-02-EXAMPLE-001
procedureInstanceId	TEXT	Yes	F-PR-01-02-EXAMPLE-001
recordedAt

Field	Type	Required	Sample value
recordId	TEXT	Yes	ST-01-F01-EXAMPLE-001
procedureInstanceId	TEXT	Yes	ST-01-F01-EXAMPLE-001
recordedAt	DATE	Yes	2026-02-20
evidenceSummary	TEXTAREA	Yes	ST-01-F01-EXAMPLE-001

Field	Type	Required	Sample value
recordId	TEXT	Yes	ST-01-F02-EXAMPLE-001
procedureInstanceId	TEXT	Yes	ST-01-F02-EXAMPLE-001

Field	Type	Required	Sample value
recordId	TEXT	Yes	F-TN-01-EXAMPLE-001
procedureInstanceId	TEXT	Yes	F-TN-01-EXAMPLE-001
recordedAt	DATE	Yes	2026-02-20
evidenceSummary	TEXTAREA	Yes	F-TN-01-EXAMPLE-001

Field	Type	Required	Sample value
recordId	TEXT	Yes	F-TN-02-EXAMPLE-001
procedureInstanceId	TEXT	Yes	F-TN-02-EXAMPLE-001
recordedAt

Field	Type	Required	Sample value
policyVersion	TEXT	Yes	N/A
justification	TEXTAREA	Yes	Placeholder value from governance form catalogue.
requestedActivationDate	DATE	Yes	2026-02-20

Field	Type	Required	Sample value
incidentId	TEXT	Yes	IncidentReportForm-EXAMPLE-001
detectedAt	DATE	Yes	2026-02-20
impactSummary	TEXTAREA	Yes

recordId	TEXT	Yes	F-IP-04-02-EXAMPLE-001
procedureInstanceId	TEXT	Yes	F-IP-04-02-EXAMPLE-001
recordedAt	DATE	Yes	2026-02-20
evidenceSummary	TEXTAREA	Yes	F-IP-04-02-EXAMPLE-001

Field	Type	Required	Sample value
recordId	TEXT	Yes	F-IP-04-03-EXAMPLE-001
procedureInstanceId	TEXT	Yes	F-IP-04-03-EXAMPLE-001
recordedAt	DATE	Yes	2026-02-20
evidenceSummary	TEXTAREA	Yes	F-IP-04-03-EXAMPLE-001

Field	Type	Required	Sample value
recordId	TEXT	Yes	F-IP-04-04-EXAMPLE-001
procedureInstanceId	TEXT	Yes	F-IP-04-04-EXAMPLE-001
recordedAt	DATE	Yes	2026-02-20
evidenceSummary	TEXTAREA	Yes	F-IP-04-04-EXAMPLE-001

Field	Type	Required	Sample value
recordId	TEXT	Yes	F-IP-04-05-EXAMPLE-001
procedureInstanceId	TEXT	Yes	F-IP-04-05-EXAMPLE-001
recordedAt	DATE	Yes	2026-02-20
evidenceSummary	TEXTAREA	Yes	F-IP-04-05-EXAMPLE-001
conditionTrigger	TEXT	No	N/A

Field	Type	Required	Sample value
recordId	TEXT	Yes	F-IP-04-06-EXAMPLE-001
procedureInstanceId	TEXT	Yes	F-IP-04-06-EXAMPLE-001
recordedAt	DATE	Yes	2026-02-20
evidenceSummary	TEXTAREA	Yes	F-IP-04-06-EXAMPLE-001

Field	Type	Required	Sample value
recordId	TEXT	Yes	F-IP-04-07-EXAMPLE-001
procedureInstanceId	TEXT	Yes	F-IP-04-07-EXAMPLE-001
recordedAt	DATE	Yes	2026-02-20
evidenceSummary	TEXTAREA	Yes	F-IP-04-07-EXAMPLE-001
conditionTrigger	TEXT	No	N/A

Field	Type	Required	Sample value
recordId	TEXT	Yes	F-IP-04-08-EXAMPLE-001
procedureInstanceId	TEXT	Yes	F-IP-04-08-EXAMPLE-001
recordedAt	DATE	Yes	2026-02-20
evidenceSummary	TEXTAREA	Yes	F-IP-04-08-EXAMPLE-001

Loading workspace

Loading module

Loading workspace

SETTLEMENT_FORMAL_VERIFICATION_INVARIANTS.md

Purpose

Scope

Definitions

Normative Rules

A) Ledger Structure Invariants

B) Authorization Invariants

C) Lifecycle Ordering Invariants

D) Metadata Trace Invariants

E) Cross-Domain Invariants

Mapping to Code

Non-normative Notes

Testability

Verification Strategy

Read-only form framework

F-CT-01 Award Proposal Record

F-CT-02 Award Approval Record

F-CT-03 Contract Draft Record

F-CT-04 Legal Review Record

F-CT-05 Final Contract Record

F-CT-06 Signature Authorization Record

F-CT-07 Contract Signature Record

F-CT-08 Award Cancellation / Withdrawal Record

F-CT-09 Contract Closure Record

F-IP-04-01 Cost Estimate Submission Record

F-IP-04-02 Assignment Record

F-PR-01-01 Procurement Request

F-PR-01-02 Supplier Offer Submission

ST-01-F01 Settlement Request Record

ST-01-F02 Proof of Payment Record

F-TN-01 Tender Notice / Invitation

F-TN-02 Eligibility Declaration (Bidder)

ActivationRequestForm Activation Request Form

IncidentReportForm Incident Report Form

F-IP-04-03 Inspection Observation Record

F-IP-04-04 Verification Record

F-IP-04-05 Review Findings Record

F-IP-04-06 Decision Record

F-IP-04-07 Correction Request / Response Record

F-IP-04-08 Closure Record

F-IP-04-09 Independence / Impartiality Declaration

F-PR-01-03 Offer Evaluation Record

F-PR-01-04 Selection Justification

F-PR-01-05 Procurement Decision Record

F-PR-01-06 Conflict of Interest Declaration

F-PR-01-07 Procurement Closure Record

ST-01-F03 Verification Record

ST-01-F04 Settlement Confirmation Record

ST-01-F05 Audit Log Reference

F-TN-03 Bid Submission Record

F-TN-04 Bid Confidentiality & Integrity

F-TN-05 Bid Opening Record

F-TN-06 Evaluation Committee Declaration

F-TN-07 Evaluation Record

F-TN-08 Selection / Award Justification

F-TN-09 Non-selection Rationale Record

F-TN-10 Tender Closure Record

NamespaceCreationForm Namespace Creation Form

PolicyAmendmentForm Policy Amendment Form

Field	Type	Required	Sample value
recordId	TEXT	Yes	F-IP-04-09-EXAMPLE-001
procedureInstanceId	TEXT	Yes	F-IP-04-09-EXAMPLE-001
recordedAt	DATE	Yes	2026-02-20
evidenceSummary	TEXTAREA	Yes	F-IP-04-09-EXAMPLE-001
conditionTrigger	TEXT	No	N/A

Field	Type	Required	Sample value
recordId	TEXT	Yes	F-PR-01-03-EXAMPLE-001
procedureInstanceId	TEXT	Yes	F-PR-01-03-EXAMPLE-001
recordedAt	DATE	Yes	2026-02-20
evidenceSummary	TEXTAREA	Yes	F-PR-01-03-EXAMPLE-001

Field	Type	Required	Sample value
recordId	TEXT	Yes	F-PR-01-04-EXAMPLE-001
procedureInstanceId	TEXT	Yes	F-PR-01-04-EXAMPLE-001
recordedAt	DATE	Yes	2026-02-20
evidenceSummary	TEXTAREA	Yes	F-PR-01-04-EXAMPLE-001

Field	Type	Required	Sample value
recordId	TEXT	Yes	F-PR-01-05-EXAMPLE-001
procedureInstanceId	TEXT	Yes	F-PR-01-05-EXAMPLE-001
recordedAt	DATE	Yes	2026-02-20
evidenceSummary	TEXTAREA	Yes	F-PR-01-05-EXAMPLE-001

Field	Type	Required	Sample value
recordId	TEXT	Yes	F-PR-01-06-EXAMPLE-001
procedureInstanceId	TEXT	Yes	F-PR-01-06-EXAMPLE-001
recordedAt	DATE	Yes	2026-02-20
evidenceSummary	TEXTAREA	Yes	F-PR-01-06-EXAMPLE-001

Field	Type	Required	Sample value
recordId	TEXT	Yes	F-PR-01-07-EXAMPLE-001
procedureInstanceId	TEXT	Yes	F-PR-01-07-EXAMPLE-001
recordedAt	DATE	Yes	2026-02-20
evidenceSummary	TEXTAREA	Yes	F-PR-01-07-EXAMPLE-001

Field	Type	Required	Sample value
recordId	TEXT	Yes	ST-01-F03-EXAMPLE-001
procedureInstanceId	TEXT	Yes	ST-01-F03-EXAMPLE-001
recordedAt	DATE	Yes	2026-02-20
evidenceSummary	TEXTAREA	Yes	ST-01-F03-EXAMPLE-001

Field	Type	Required	Sample value
recordId	TEXT	Yes	ST-01-F04-EXAMPLE-001
procedureInstanceId	TEXT	Yes	ST-01-F04-EXAMPLE-001
recordedAt	DATE	Yes	2026-02-20
evidenceSummary	TEXTAREA	Yes	ST-01-F04-EXAMPLE-001

Field	Type	Required	Sample value
recordId	TEXT	Yes	ST-01-F05-EXAMPLE-001
procedureInstanceId	TEXT	Yes	ST-01-F05-EXAMPLE-001
recordedAt	DATE	Yes	2026-02-20
evidenceSummary	TEXTAREA	Yes	ST-01-F05-EXAMPLE-001

Field	Type	Required	Sample value
recordId	TEXT	Yes	F-TN-03-EXAMPLE-001
procedureInstanceId	TEXT	Yes	F-TN-03-EXAMPLE-001
recordedAt	DATE	Yes	2026-02-20
evidenceSummary	TEXTAREA	Yes	F-TN-03-EXAMPLE-001