RS4A-04 — Phase Model and Proof Obligations — 2026-06-21
Macro: RS4A · Mục tiêu D
Deliverable: 04 of 14 · design-only (no transaction code; phase specification only)
Inputs: RS4A-02 (contract v0.2), RS3B-05/RS3C-07 (replay), RS3B-06 (sink), RS3B-08/RS3C-09 (triggers), RS2-PATCH1 atomic-boundary correction.
Gate: REGISTRATION_HOLD · REGISTRATION_CAN_PROCEED = NO
Seven phases. Each block is born / tested / replaced / rolled-back separately; they are joined only by the envelopes named below — no mega-pipeline. Phases 0–2 are prerequisites/consume outside or at the boundary; Phase 3 is the single atomic in-transaction write; Phase 4 verifies post-commit; Phase 5 audits durably outside any rolled-back transaction; Phase 6 keeps activation entirely separate and closed.
Phase 0 — Source / artifact resolution
| Aspect |
Specification |
| Input contract |
request_proposed.{artifact_path, artifact_hash, hash_algorithm, canonicalization_version, artifact_type, origin, admission_ref} (scalar; reject glob/list → MASS_REGISTRATION_ATTEMPTED) |
| Trusted producer |
Interface F deployed-artifact resolver (RS4A-06) — produces trusted_attested.artifact_hash from a PROVEN carrier, never the caller copy |
| Consumer |
Phase 1 (authority validation) and Phase 3 (write intent) |
| Fail-closed condition |
no proven carrier / hash mismatch / non-canonical path / unknown algorithm / type mismatch ⇒ SOURCE_NOT_DEPLOYED | HASH_MISMATCH | ARTIFACT_TYPE_MISMATCH; emit no trusted hash |
| Rollback rule |
none (no write); pure resolution |
| Audit rule |
resolution failure logged advisory; no registry effect |
| Proof artifact |
resolver decision record: {canonical_path, origin, drift_state=NONE, source_carrier_ref} or fail-closed reason |
| Independent test cases |
T-P0-1 glob input; T-P0-2 caller hash only (no carrier); T-P0-3 carrier hash ≠ proposed; T-P0-4 .ts type vs bash artifact; T-P0-5 symlink/.. path (see RS4A-11 P0 block) |
Phase 1 — Authority validation
| Aspect |
Specification |
| Input contract |
owner_envelope_ref, approval_envelope_ref, trusted_attested.artifact_hash (from Phase 0) |
| Trusted producer |
Owner/APR authority contract (RS4A-05): governance_object_ownership head row + register_dot APR quorum proof bound to the artifact_hash |
| Consumer |
Phase 2 (nonce consume) and Phase 3 |
| Fail-closed condition |
governance_object_ownership head absent (live: 0 rows) ⇒ OWNER_ABSENT; no register_dot action / not bound to artifact (live: action absent) ⇒ APR_NOT_BOUND_TO_ARTIFACT; no authority ⇒ no write |
| Rollback rule |
none (no write) |
| Audit rule |
authority denial recorded to durable sink (Phase 5) |
| Proof artifact |
authority decision: {owner_head_ref, apr_ref, quorum_proof_ref, artifact_hash_bound} |
| Independent test cases |
T-P1-1 owner absent; T-P1-2 register_dot absent; T-P1-3 APR bound to a different artifact_hash; T-P1-4 quorum not proven |
Phase 2 — Nonce / logical-key consume
| Aspect |
Specification |
| Input contract |
logical_request_key, authorization_nonce, attempt_id (C1 three identities, RS4A-07) |
| Trusted producer |
replay/nonce surface (RS4A-07) — REQUIRED, not present today (REPLAY_SURFACE_REQUIRED_NOT_PRESENT) |
| Consumer |
Phase 3 (same atomic transaction) |
| Fail-closed condition |
logical_request_key already consumed ⇒ REPLAY_DUPLICATE (return prior decision); nonce reused ⇒ REPLAY_NONCE_CONSUMED; nonce unbound ⇒ NONCE_UNBOUND; attempt used as effect key ⇒ REPLAY_ATTEMPT_NO_BYPASS |
| Rollback rule |
consume happens inside Phase-3 transaction; pre-commit failure rolls the consume back together with the write (no orphan consume) |
| Audit rule |
replay rejection recorded to durable sink |
| Proof artifact |
consume record with UNIQUE(logical_request_key) and separate UNIQUE(authorization_nonce) |
| Independent test cases |
T-P2-1 nonce reuse; T-P2-2 fresh nonce, same logical effect; T-P2-3 attempt_no bypass; T-P2-4 concurrent attempts |
Phase 3 — Inert registration write (the single atomic boundary)
| Aspect |
Specification |
| Input contract |
validated registered_row_intent (RS4A-02 §3) with inert/non-active status |
| Trusted producer |
the governed registrar replacement (RS4A-10) |
| Consumer |
Phase 4 verifier |
| Fail-closed condition |
DB UNIQUE on identity axis rejects duplicate (IDENTITY_UNIQUE_ABSENT is a defect today); status='active' or gate flip ⇒ WOULD_OPEN_GATE/ACTIVATION_AT_REGISTRATION; insecure transport/privileged path ⇒ INSECURE_TRANSPORT/PRIVILEGED_PATH_USED |
| Atomic-unit content |
{consume nonce (P2), write one inert dot_tools row, record attempt} commit together (RS2-PATCH1 R1/R2: prerequisites resolved in P0–P1 outside the txn; gate NOT flipped inside the txn) |
| Rollback rule |
any pre-commit failure rolls back consume + write atomically; no committed-prefix rows (closes D06/D07) |
| Audit rule |
on rollback, Phase 5 writes a durable failure record outside the rolled-back txn |
| Proof artifact |
committed inert row + consume record; registered_row_intent echoed |
| Independent test cases |
T-P3-1 duplicate identity; T-P3-2 active status attempt; T-P3-3 gate-flip attempt; T-P3-4 mid-write crash → full rollback |
Phase 4 — Post-commit verifier
| Aspect |
Specification |
| Input contract |
committed dot_code, trusted_attested.artifact_hash, expected inert status |
| Trusted producer |
paired verifier in the DOT-HEALTH-DOT family (reuse precedent: dot-apr-types-register/-audit, DOT-TAC-COLLECTION-REGISTER/-VERIFY) |
| Consumer |
caller / compensation logic |
| Fail-closed condition |
not exactly one row for dot_code, metadata ≠ admitted artifact, status is activating, or audit envelope not durably written ⇒ POST_COMMIT_VERIFY_FAIL |
| Rollback rule |
the committed row is not silently deleted; verifier failure → compensation path (RS4A-07 S3), logical key stays consumed |
| Audit rule |
verify result recorded to durable sink |
| Proof artifact |
verifier readback record; success = HTTP-2xx + readback match (closes D10/D23) |
| Independent test cases |
T-P4-1 row drift; T-P4-2 two rows for one code; T-P4-3 active status detected; T-P4-4 false-success (process-exit) rejected |
Phase 5 — Durable failure audit
| Aspect |
Specification |
| Input contract |
failure/decision envelope {phase, reject_codes, logical_request_key, run_id, payload_classification} |
| Trusted producer |
the registrar, writing to the selected sink (RS4A-08; lead candidate event_outbox, fail-closed until immutability+retention proven) |
| Consumer |
forensics / Owner review |
| Fail-closed condition |
sink not writable / not append-only ⇒ AUDIT_SINK_UNAVAILABLE; registration must not report success when audit is unwritten |
| Rollback rule |
the audit write is outside any rolled-back Phase-3 txn (RS2-PATCH1 R3) — it survives rollback |
| Audit rule |
the audit record itself must be append-only (no UPDATE/DELETE) — not enforced on any candidate today (G6) |
| Proof artifact |
durable audit row with payload_classification; no activation lane used |
| Independent test cases |
T-P5-1 audit-from-rolled-back-txn survives; T-P5-2 sink unavailable → fail-closed; T-P5-3 audit not on an execution delivery_lane |
Phase 6 — Activation remains separate and closed
| Aspect |
Specification |
| Input contract |
a distinct activation request with its own authority nonce (not the registration nonce) |
| Trusted producer |
a separate Owner-gated activation flow (out of registrar scope) |
| Consumer |
runtime gates (dot_config), agent API |
| Fail-closed condition |
registration must complete with owner_real_run_gate_open closed; any activation at registration ⇒ ACTIVATION_AT_REGISTRATION |
| Rollback rule |
n/a to registration (activation is a later, independent transaction) |
| Audit rule |
activation is audited by its own flow, not the registrar |
| Proof artifact |
proof that registration set inert status, did not flip process_dot_runtime.real_run_enabled/iu_core.operator_runtime_enabled (both false live), and did not satisfy the notify condition (tier∈watch ∧ status='active') |
| Independent test cases |
T-P6-1 watch-tier active insert blocked; T-P6-2 gate untouched after registration; T-P6-3 agent API not wired |
Cross-phase proof obligations
- Atomic boundary correctness — only Phase 3 holds a transaction; prerequisites (P0–P1) are resolved before it and the gate is not flipped inside it (fixes RS2-PATCH1 R1/R2).
- Audit-after-rollback — Phase 5 writes survive a Phase-3 rollback (fixes R3).
- Consumed-state durability — a post-commit failure (Phase 4) never un-consumes the logical key / nonce (RS4A-07 §4).
- No-activation — Phases 3 & 6 jointly prove registration is inert (RS4A-09).
- No-mega — no phase calls another governed pipeline; the chain ends at Phase 5/registration boundary.
Status
- Phase model:
PHASE_MODEL_AND_PROOF_OBLIGATIONS_DEFINED (7 phases, each with input/producer/consumer/fail-closed/rollback/audit/proof/tests).
- No transaction code authored. Gate
REGISTRATION_HOLD · CAN_PROCEED = NO.