Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
Expand Up @@ -2122,12 +2122,14 @@ relaxes.

Delivery boundary: test-only. No production entry point constructs any store;
the ladder adds no product path and reads the candidate only through the
retained TypeScript store. The Stage 2C parity half executes through the ten
`s2c2.*` rows above; two declarations stay pending.
`s2c2.archive_after_leased_completion_parity` records a capture gap the parity
row exposed: `todo archive-completed` on a Todo holding a released lease record
keeps that lease in the candidate head while the source projection drops the
orphaned lease, so bounded qualification reports `shadow_projection_drift`.
retained TypeScript store. The Stage 2C parity half executes through the eleven
`s2c2.*` rows above; one declaration stays pending.
`s2c2.archive_after_leased_completion_parity` was declared from the capture gap
the parity row exposed and is now an executable deterministic row: the parity
half folds the Todo partition against the same current-graph rule the source
projection applies, so archiving a Todo that holds a released lease record
keeps the candidate head matched instead of reporting
`shadow_projection_drift`.
`s2c2.sustained_parity_soak` is the >=10-day synthetic-goal soak owned by
Section 7.2 and lane L, and bounded qualification keeps reporting
`sustained_parity_verdict=not_evaluated`. This subsection records executable
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -1688,11 +1688,12 @@ Live 行按环境门控(`LOOPX_TEST_POSTGRES_URL`;`NOKV_COORDINATION_LIVE=1`
`summary.privacy_violations` 阻止 green 退出,任何开关都不能放宽。

交付边界:test-only。没有任何生产入口构造任何 store;ladder 不新增产品路径,
只经保留的 TypeScript store 读取候选。Stage 2C parity 后半段由上述十个
`s2c2.*` 行执行;仍有两条声明保持 pending。`s2c2.archive_after_leased_completion_parity`
记录 parity 行暴露的一个 capture 缺口:对持有已释放 lease 记录的 Todo 执行
`todo archive-completed` 后,候选 head 仍保留该 lease,而 source 投影会丢弃这条
已成孤儿的 lease,于是有界 qualification 报告 `shadow_projection_drift`。
只经保留的 TypeScript store 读取候选。Stage 2C parity 后半段由上述十一个
`s2c2.*` 行执行;只有一条声明保持 pending。`s2c2.archive_after_leased_completion_parity`
原先是 parity 行暴露的 capture 缺口声明,现已成为可执行的确定性行:parity 后半段
在对 Todo 分区做折叠时套用与 source 投影同一条当前图规则,因此对持有已释放 lease
记录的 Todo 执行 `todo archive-completed` 后,候选 head 仍保持 matched,而不再报告
`shadow_projection_drift`。
`s2c2.sustained_parity_soak` 是由 7.2 节与车道 L 负责的 >=10 天合成 goal soak,
有界 qualification 继续报告 `sustained_parity_verdict=not_evaluated`。本小节记录
的是上述阶段的可执行证据;它不晋升任何 provider,也不完成 Stage 2C promotion。
Expand Down
20 changes: 11 additions & 9 deletions examples/shared-goal-authority-e2e/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -54,20 +54,22 @@ suites rather than in the pytest shards.
| `s2c2.event_only_todo_source_holds` | 2c2 | real_cli | deterministic | an event-only Todo appended to the goal's state event log makes `inspect`, `qualify` and `read-candidate` fail closed with `event_log_writer_not_bound`, `status` stays readable, a Markdown write still commits with its capture held, the event log is untouched; removing the event source does not requalify, and rollback plus rebootstrap recovers |
| `s2c2.migration_seeds_and_drains` | 2c2 | real_cli | deterministic | `migrate-state` previews an actively captured goal without writing, refuses `--execute` with `shadow_source_replacement_requires_rebootstrap` (also when capture is merely disabled), and executes only after `rollback`; the migrated goal carries its disabled capture configuration, plans no observation seed, requires its own `bootstrap`, then captures a write to cursor `2` and qualifies on it while the legacy archive is retained |
| `s2c2.growth_measurement_gate` | 2c2 | real_cli | deterministic | ten fixed-size `todo add` writes: the cursor advances by one each time, `store_bytes` grows monotonically, the per-transaction delta accelerates by at most 2048 bytes (one live record), every retained transaction carries its complete projection, `retention_pressure` stays false; the report carries final and cumulative publication bytes and claims no capacity horizon (`capacity_verdict=not_evaluated`) |
| `s2c2.archive_after_leased_completion_parity` | 2c2 | real_cli | deterministic | a leased Todo is completed through its fence and then archived by `todo archive-completed`: the archive retires the Todo from the current graph while its released lease file stays on disk as audit history, and `inspect` still reports `matched` with `parity_matches=true`, no drift reason, a qualified bounded read of a co-resident open Todo, and a `qualify` that requires the archive event kind; the released lease file remains on disk |

Pending rows are declared in the report as `pending`, never counted as pass,
and they block a green exit unless `--allow-pending` is passed. Two
declarations remain. `s2c2.archive_after_leased_completion_parity` records a
capture gap found while building the parity row: `todo archive-completed` on a
Todo that holds a released lease record leaves that lease in the candidate
head while the source projection drops the now-orphaned lease, so `inspect`
reports `shadow_projection_drift`; the parity row therefore archives nothing
and the gap stays visible until the archive writer captures the lease it
orphans. `s2c2.sustained_parity_soak` is the >=10-day synthetic-goal soak of
the selected local profile owned by RFC Section 7.2 (lane L). Bounded
and they block a green exit unless `--allow-pending` is passed. One
declaration remains: `s2c2.sustained_parity_soak`, the >=10-day synthetic-goal
soak of the selected local profile owned by RFC Section 7.2 (lane L). Bounded
qualification reports `sustained_parity_verdict=not_evaluated`, and no
`s2c2.*` row promotes a provider or completes the Stage 2C promotion.

The former `s2c2.archive_after_leased_completion_parity` declaration is now an
executable row. The gap it recorded is closed at the fold: a Todo partition
carries the published Todo read records, and the candidate head now keeps a
lease edge only for Todos still in the current graph
(`archive_state === "active"`), matching the rule the source projection and the
TypeScript source verification already apply.

The `s2c2.*` rows use two scheduling-only seams outside every product decision:
holding the stable maintenance lock, which makes a writer report
`drain_deferred/drain_lock_busy` and leave its committed entry pending, and a
Expand Down
8 changes: 4 additions & 4 deletions examples/shared-goal-authority-e2e/correctness.md
Original file line number Diff line number Diff line change
Expand Up @@ -314,10 +314,10 @@ Python/TS/JSON provenance, and reads back through an independent native process.

The mandatory repair set must have zero failures, skips, pending, or unverified
cases. Broader ladder rows retain their declared pending/environment gates:
`s2c2.archive_after_leased_completion_parity` stays pending until the
archive-completed writer captures the released lease it orphans, and
`s2c2.sustained_parity_soak` until the Section 7.2 soak exists; these tests
grant neither production promotion nor a completed Stage 2C claim.
`s2c2.archive_after_leased_completion_parity` is now an executable
deterministic row rather than a declaration, and `s2c2.sustained_parity_soak`
stays pending until the Section 7.2 soak exists; these tests grant neither
production promotion nor a completed Stage 2C claim.

For a caller comparison, run both `test_shadow_observable*_e2e.py` files with
`LOOPX_SHADOW_COMPARISON_SOURCE` set to an immutable baseline checkout, then to
Expand Down
25 changes: 25 additions & 0 deletions loopx/control_plane/coordination/local_authority_shadow.ts
Original file line number Diff line number Diff line change
Expand Up @@ -688,6 +688,24 @@ function partitionsOf(head: JsonObject | null): JsonObject {
return partitions;
}

/**
* Todo ids still present in the current Todo graph.
*
* A published Todo partition also retains archived rows for audit, so the raw
* record list is not the graph. The source projection
* (`build_todo_runtime_shadow_projection`) and the TypeScript source
* verification both define the graph as `archive_state === "active"`; capture
* and fold must apply that same typed membership rule or the candidate head
* keeps a lease edge the source never emits.
*/
export function currentGraphTodoIds(todos: readonly JsonObject[]): Set<string> {
return new Set(
todos
.filter((item) => item.archive_state === "active")
.map((item) => String(item.todo_id)),
);
}

/**
* Fold one partition into the candidate head. A v0 head (whole-snapshot
* observation) is accepted as the starting point with no partition markers.
Expand All @@ -711,6 +729,13 @@ export function composeLocalAuthorityShadowHead(
if (entry.partition === "todos") {
handoffMode = String(projection.handoff_mode);
todos = structuredClone(projection.todos as JsonObject[]);
// The Todo partition carries the published Todo read records, including
// archived rows retained for audit. The candidate head, like the source
// projection, keeps live lease edges only for Todos that are still in the
// current graph (`archive_state === "active"`); a retained archived row
// must not re-admit the lease its archive just orphaned.
const graphTodoIds = currentGraphTodoIds(todos);
leases = leases.filter((lease) => graphTodoIds.has(String(lease.todo_id)));
} else {
leases = structuredClone(projection.leases as JsonObject[]);
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -160,10 +160,25 @@ async function nextSeq(directory: string, runtimeRoot: string, goalId: string, l
return highest + 1;
}

/**
* Read the lease partition for one capture.
*
* The legacy lease directory is append-retained history: archiving a Todo
* leaves its released lease file on disk. The source projection models only
* the current Todo graph, so it drops a lease whose Todo is no longer part of
* that graph (see `build_todo_runtime_shadow_projection`). Capture must apply
* the same rule, or archiving a Todo after a released lease writes an orphan
* edge into the candidate head and parity reports `shadow_projection_drift`.
*
* `activeTodoIds` is the current Todo graph supplied by the caller; `null`
* means the caller could not read it, and the capture stays strict rather
* than guessing a projection.
*/
async function readLeasePartition(
leaseDirectory: string,
plannedStem: string,
plannedLease: JsonObject | null,
activeTodoIds: ReadonlySet<string> | null,
): Promise<JsonObject[]> {
const records = new Map<string, JsonObject>();
let names: string[] = [];
Expand All @@ -176,6 +191,7 @@ async function readLeasePartition(
if (!LEASE_FILE.test(name) || name.startsWith(".")) continue;
const stem = name.slice(0, -".json".length);
if (stem === plannedStem) continue;
if (activeTodoIds !== null && !activeTodoIds.has(stem)) continue;
const raw: unknown = JSON.parse(await readFile(join(leaseDirectory, name), "utf8"));
if (raw !== null && typeof raw === "object" && !Array.isArray(raw)) {
records.set(stem, raw as JsonObject);
Expand Down Expand Up @@ -208,6 +224,12 @@ export interface LeaseOutboxCaptureInput {
operation_id: string | null;
previous_lease: JsonObject | null;
planned_lease: JsonObject;
/**
* Current Todo graph for the goal, used to drop leases orphaned by an
* archived Todo exactly as the source projection does. `null` keeps the
* strict pre-existing behavior.
*/
active_todo_ids: readonly string[] | null;
}

export interface LeaseOutboxCapture {
Expand Down Expand Up @@ -257,8 +279,11 @@ export async function beginLeaseOutboxEntry(
canonicalAuthorityBytes(input.previous_lease).equals(canonicalAuthorityBytes(input.planned_lease))) {
return { ...inert, skipped_reason: "partition_unchanged" };
}
const projection = { leases: await readLeasePartition(input.lease_directory, plannedStem, input.planned_lease) };
const previousRecords = await readLeasePartition(input.lease_directory, plannedStem, input.previous_lease);
const activeTodoIds = input.active_todo_ids === null
? null
: new Set(input.active_todo_ids);
const projection = { leases: await readLeasePartition(input.lease_directory, plannedStem, input.planned_lease, activeTodoIds) };
const previousRecords = await readLeasePartition(input.lease_directory, plannedStem, input.previous_lease, activeTodoIds);
for (const item of [...previousRecords, ...projection.leases]) {
const record = item.record as JsonObject;
if (record.goal_id !== input.goal_id || record.todo_id !== item.file_stem) {
Expand Down
17 changes: 10 additions & 7 deletions loopx/control_plane/testing/authority_e2e_ladder.py
Original file line number Diff line number Diff line change
Expand Up @@ -50,6 +50,7 @@
row_migration_seeds_new_lineage,
)
from .authority_e2e_rows_stage2c2 import (
row_archive_after_leased_completion_parity,
row_drain_idempotent,
row_event_only_todo_source_holds,
row_growth_measurement_gate,
Expand Down Expand Up @@ -750,16 +751,18 @@ def _row_postgresql_conformance_live(context: RowContext) -> RowOutcome:
posix_only=False,
run=row_growth_measurement_gate,
),
LadderRow(
id="s2c2.archive_after_leased_completion_parity",
stage="2c2",
title="archiving a Todo whose released lease stays on disk keeps the candidate head matched and qualifiable",
product_path="real_cli",
gate="deterministic",
posix_only=False,
run=row_archive_after_leased_completion_parity,
),
)

PENDING_ROWS: tuple[PendingRow, ...] = (
PendingRow(
"s2c2.archive_after_leased_completion_parity",
"2c2",
"the archive-completed writer captures the released lease it orphans: archiving a Todo "
"that holds a released lease record leaves that lease in the candidate head while the "
"source projection drops it, so bounded qualification reports shadow_projection_drift",
),
PendingRow(
"s2c2.sustained_parity_soak",
"2c2",
Expand Down
Loading