[P0-25] Prove target-lease crash recovery and stale-writer exclusion #140

New issue

Open

opened 2026-09-02 17:26:33 +00:00 by nsaspy · 0 comments

nsaspy commented

2026-09-02 17:26:33 +00:00

Owner

Objective

Prove the complete StarIntel target-lease system remains safe under expiry, crashes, ambiguous outcomes, restart/failover, revocation, and delayed stale execution.

Current source already implements the core lease primitives: backend-neutral typed outcomes, monotonic fencing, Valkey server-authoritative time, atomic renew/release/revoke, idempotent acquisition receipts, fail-closed corrupt/no-TTL handling, and a fenced authoritative-set seam. This issue therefore owns the recovery/race proof program, not a lease-store rewrite.

Canonical ARDR authority

Research: lost-rob0t/starintel-auto-research/roam/research/star-server/STAR-RESEARCH-033-target-lease-recovery-race-matrix.org
Design/adversarial review: lost-rob0t/starintel-auto-research/roam/design/star-server/STAR-SERVER-045-target-lease-recovery-race-matrix.org
Lease stack index: lost-rob0t/starintel-auto-research/roam/indexes/star-server/STAR-LEASE-INDEX-030-backend-neutral-kv-leases.org
Upstream integration authority: lost-rob0t/starintel-server#32

Required scenarios

Stable matrix identifiers are defined in STAR-SERVER-045:

LR-01 simultaneous acquire A/B
LR-02 renew before expiry
LR-03 renew at/after expiry cannot revive
LR-04 release/reacquire with stale old release
LR-05 backend commit + lost response + same-request replay
LR-06 process crash after acquire
LR-07 actor crash while lease active
LR-08 backend unavailable during renewal
LR-09 A/fence-N stalls, B/fence-N+1 commits, A resumes and is rejected
LR-10 privileged revoke while old work continues
LR-11 client clock skew vs backend-authoritative time
LR-12 same idempotency request/digest replay
LR-13 same idempotency request with changed digest
LR-14 backend restart retaining a safe fencing floor
LR-15 restore/failover where a safe fencing floor cannot be proven -> fail closed

Recovery invariants

Runtime recovery compares persisted execution state with current typed lease authority; persisted running or actor/process liveness never grants authority.
A recovered attempt is explicitly classified as current/resumable, reacquire-required, stale-generation, unknown-outcome-resolution-required, backend-unavailable, or fencing-floor-reconciliation-required.
Unknown mutating outcomes are resolved using the original request ID/digest before issuing new logical work.
Reacquisition creates a new execution authority/generation; old execution history is not rewritten to inherit the new fence.
Orphaned leases expire without graceful cleanup being required for correctness.
Cancellation on lease loss is advisory; every authoritative effect remains fenced.
Client clocks never determine current authority.
Revocation blocks old authoritative effects even before a successor lease exists.
A restore/failover that cannot prove a monotonic fencing floor cannot authorize new acquisition for the affected identity.

Dependency order

Existing lease protocol/Valkey semantics from #29/#30/#31 remain authoritative.
#32 supplies authenticated execution authority and the production fenced-effect seam.
This issue proves recovery/race behavior around those boundaries.

The deterministic classifier/harness slices may proceed independently once operator-authorized. The final stale-writer production acceptance slice depends on #32's concrete fenced side-effect seam.

Proposed implementation slices — PENDING OPERATOR APPROVAL

Slice 1 — pure recovery classifier + deterministic RED fixtures

No network/process orchestration.

Mandatory RED-first target:

Persisted execution A carries lease/fence N; current observed lease for the same identity carries N+1. Untouched current master has no typed recovery classifier. The RED must fail for that missing boundary. GREEN must return stale-generation and prove zero acquire/renew/effect callbacks occur.

Sibling REDs:

outcome-unknown -> resolve original request identity, never fresh acquire;
no active lease -> reacquire-required without mutating old execution authority;
backend unavailable -> fail closed;
exact current authority -> resume only when explicit recovery policy permits.

Slice 2 — shared LR-* deterministic scenario harness

Reuse the existing memory lease backend/contract. Add explicit barriers and controlled time; do not create a second fake lease algebra or sleep-driven semantic suite.

Slice 3 — real Valkey race/TTL/ambiguous-response evidence

Extend existing t/valkey-lease-integration-test.lisp with LR-01/02/03/05/11 and controllable restart evidence. Preserve Valkey TIME as authority.

Slice 4 — production stale-writer acceptance

After #32 exposes one real fenced side-effect boundary:

A acquires N and stalls before effect.
A loses authority.
B acquires N+1 and commits.
A resumes with N.
A effect is rejected.
Authoritative sink contains B only; no A outbox/publication/terminal settlement is accepted.

A renew/release stale-token test alone does not satisfy this acceptance criterion.

Slice 5 — restart/restore fencing-floor proof

Test normal restart with retained fence state and fail-closed recovery when restored/failover state cannot prove a fence greater than generations already accepted downstream. Do not claim stronger Valkey failover semantics than the actual tested durability configuration.

Acceptance criteria

deterministic unit tests cover the recovery classifier and exact race schedules;
backend-neutral tests continue to prove lease state semantics without duplicate implementations;
real Valkey tests prove concurrency, server-time expiry, idempotent ambiguous-response recovery, and restart behavior;
production fenced-effect test proves one accepted writer per target generation;
privileged revocation prevents post-revoke stale effects;
client clock skew cannot extend lease authority;
unknown outcome resolution cannot allocate accidental new generations;
fencing generations never regress across a recovery path claimed safe;
uncertain fencing floor fails closed;
audit/metrics expose recovery classification, lease loss, unknown-outcome resolution, reacquisition, revoke, and stale-effect rejection;
no new StarLang syntax or second lease authority is introduced.

Implementation authorization

PENDING / AWAITING_OPERATOR_APPROVAL

P0 priority, research readiness, completed design/adversarial review, issue state, or green tests do not authorize implementation. Only an explicit operator authorization recorded in the canonical approval workflow may expose a slice to RAGE.

## Objective Prove the complete StarIntel target-lease system remains safe under expiry, crashes, ambiguous outcomes, restart/failover, revocation, and delayed stale execution. Current source already implements the core lease primitives: backend-neutral typed outcomes, monotonic fencing, Valkey server-authoritative time, atomic renew/release/revoke, idempotent acquisition receipts, fail-closed corrupt/no-TTL handling, and a fenced authoritative-set seam. This issue therefore owns the **recovery/race proof program**, not a lease-store rewrite. ## Canonical ARDR authority - Research: `lost-rob0t/starintel-auto-research/roam/research/star-server/STAR-RESEARCH-033-target-lease-recovery-race-matrix.org` - Design/adversarial review: `lost-rob0t/starintel-auto-research/roam/design/star-server/STAR-SERVER-045-target-lease-recovery-race-matrix.org` - Lease stack index: `lost-rob0t/starintel-auto-research/roam/indexes/star-server/STAR-LEASE-INDEX-030-backend-neutral-kv-leases.org` - Upstream integration authority: `lost-rob0t/starintel-server#32` ## Required scenarios Stable matrix identifiers are defined in `STAR-SERVER-045`: - LR-01 simultaneous acquire A/B - LR-02 renew before expiry - LR-03 renew at/after expiry cannot revive - LR-04 release/reacquire with stale old release - LR-05 backend commit + lost response + same-request replay - LR-06 process crash after acquire - LR-07 actor crash while lease active - LR-08 backend unavailable during renewal - LR-09 A/fence-N stalls, B/fence-N+1 commits, A resumes and is rejected - LR-10 privileged revoke while old work continues - LR-11 client clock skew vs backend-authoritative time - LR-12 same idempotency request/digest replay - LR-13 same idempotency request with changed digest - LR-14 backend restart retaining a safe fencing floor - LR-15 restore/failover where a safe fencing floor cannot be proven -> fail closed ## Recovery invariants - Runtime recovery compares persisted execution state with current typed lease authority; persisted `running` or actor/process liveness never grants authority. - A recovered attempt is explicitly classified as current/resumable, reacquire-required, stale-generation, unknown-outcome-resolution-required, backend-unavailable, or fencing-floor-reconciliation-required. - Unknown mutating outcomes are resolved using the **original request ID/digest** before issuing new logical work. - Reacquisition creates a new execution authority/generation; old execution history is not rewritten to inherit the new fence. - Orphaned leases expire without graceful cleanup being required for correctness. - Cancellation on lease loss is advisory; every authoritative effect remains fenced. - Client clocks never determine current authority. - Revocation blocks old authoritative effects even before a successor lease exists. - A restore/failover that cannot prove a monotonic fencing floor cannot authorize new acquisition for the affected identity. ## Dependency order 1. Existing lease protocol/Valkey semantics from #29/#30/#31 remain authoritative. 2. #32 supplies authenticated execution authority and the production fenced-effect seam. 3. This issue proves recovery/race behavior around those boundaries. The deterministic classifier/harness slices may proceed independently once operator-authorized. The final stale-writer production acceptance slice depends on #32's concrete fenced side-effect seam. ## Proposed implementation slices — PENDING OPERATOR APPROVAL ### Slice 1 — pure recovery classifier + deterministic RED fixtures No network/process orchestration. Mandatory RED-first target: Persisted execution A carries lease/fence `N`; current observed lease for the same identity carries `N+1`. Untouched current `master` has no typed recovery classifier. The RED must fail for that missing boundary. GREEN must return `stale-generation` and prove **zero** acquire/renew/effect callbacks occur. Sibling REDs: - `outcome-unknown` -> resolve original request identity, never fresh acquire; - no active lease -> `reacquire-required` without mutating old execution authority; - backend unavailable -> fail closed; - exact current authority -> resume only when explicit recovery policy permits. ### Slice 2 — shared LR-* deterministic scenario harness Reuse the existing memory lease backend/contract. Add explicit barriers and controlled time; do not create a second fake lease algebra or sleep-driven semantic suite. ### Slice 3 — real Valkey race/TTL/ambiguous-response evidence Extend existing `t/valkey-lease-integration-test.lisp` with LR-01/02/03/05/11 and controllable restart evidence. Preserve Valkey `TIME` as authority. ### Slice 4 — production stale-writer acceptance After #32 exposes one real fenced side-effect boundary: 1. A acquires N and stalls before effect. 2. A loses authority. 3. B acquires N+1 and commits. 4. A resumes with N. 5. A effect is rejected. 6. Authoritative sink contains B only; no A outbox/publication/terminal settlement is accepted. A renew/release `stale-token` test alone does **not** satisfy this acceptance criterion. ### Slice 5 — restart/restore fencing-floor proof Test normal restart with retained fence state and fail-closed recovery when restored/failover state cannot prove a fence greater than generations already accepted downstream. Do not claim stronger Valkey failover semantics than the actual tested durability configuration. ## Acceptance criteria - deterministic unit tests cover the recovery classifier and exact race schedules; - backend-neutral tests continue to prove lease state semantics without duplicate implementations; - real Valkey tests prove concurrency, server-time expiry, idempotent ambiguous-response recovery, and restart behavior; - production fenced-effect test proves one accepted writer per target generation; - privileged revocation prevents post-revoke stale effects; - client clock skew cannot extend lease authority; - unknown outcome resolution cannot allocate accidental new generations; - fencing generations never regress across a recovery path claimed safe; - uncertain fencing floor fails closed; - audit/metrics expose recovery classification, lease loss, unknown-outcome resolution, reacquisition, revoke, and stale-effect rejection; - no new StarLang syntax or second lease authority is introduced. ## Implementation authorization `PENDING / AWAITING_OPERATOR_APPROVAL` P0 priority, research readiness, completed design/adversarial review, issue state, or green tests **do not authorize implementation**. Only an explicit operator authorization recorded in the canonical approval workflow may expose a slice to RAGE.