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 @@ -1899,6 +1899,33 @@ Per stage, this increment implements:
follow-up capture, and a leased completion in one store identity while the
registry root gains neither a candidate lineage nor lease state; and
`migrate-state` seeds a fresh lineage without legacy bytes.
- Stage 2C parity half: ten `s2c2.*` rows drive one explicitly enabled
`coordination.runtime_shadow` goal through the public CLI and assert only
through `authority-shadow status|drain`, `coordination-shadow
bootstrap|inspect|qualify|read-candidate|rollback` and `migrate-state`,
reading history through the retained TypeScript store. A Python Todo writer
and a TypeScript lease writer leave prepared records with committed markers
that one drain delivers once; bounded drains are cumulative, an idle drain
changes nothing and a writer replay mints no entry; a SIGKILL around the
primary replace settles as `abandoned` or `committed_proven_by_readback`,
and a SIGKILL inside the inline drain is recovered from exact receipts
without a second delivery; rollback archives pending entries, holds capture
as `bootstrap_required`, rebootstraps a fresh lineage and replays; three
cycles of interleaved writers (add, note update with a no-change repeat,
explicit exclusion set and clear with a no-change repeat, acquire, renew,
transfer, leased complete and supersede with their fence closes,
capture-followups) keep every bounded qualification matched with
`sustained_parity_verdict=not_evaluated`; a
direct primary edit reports `shadow_projection_drift`, a later write holds
on `source_partition_continuity_unproved`, and only rollback plus rebootstrap
recovers; an event-only Todo source holds `inspect`, `qualify` and
`read-candidate` with `event_log_writer_not_bound` while the primary keeps
committing; `migrate-state` refuses an active capture source with
`shadow_source_replacement_requires_rebootstrap` until rollback and disabled
capture, after which the migrated goal bootstraps a fresh lineage that
drains; and ten transactions measure file-v0 history growth with complete
projections retained, per-transaction growth accelerating by at most one
live record, and no capacity horizon claimed.

Live rows are environment-gated (`LOOPX_TEST_POSTGRES_URL`;
`NOKV_COORDINATION_LIVE=1` plus the `NOKV_*` stack variables;
Expand All @@ -1917,12 +1944,17 @@ 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
(`s2c2.*`: outbox entries, idempotent drain, SIGKILL before and during drain,
rollback with pending entries, parity equal and divergent,
migration seed-and-drain, growth measurement) are declared as pending rows,
not claimed. This subsection records executable evidence for the stages above;
it does not promote any provider or complete the Stage 2C promotion.
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`.
`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
evidence for the stages above; it does not promote any provider or complete
the Stage 2C promotion.

### 11.3 Remaining qualification and promotion plan

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -1512,6 +1512,27 @@ CLI runner、observation-lock 窗口、候选回读)、只读 TypeScript 探
不同时,todo add、task-lease acquire、todo update、follow-up 捕获与带 lease 的
complete 仍落入同一个 store identity,registry root 既不产生候选 lineage 也不
产生 lease 状态;`migrate-state` 在不携带 legacy 字节的前提下建立新 lineage。
- Stage 2C parity 后半段:十个 `s2c2.*` 行只通过公开 CLI 驱动一个显式开启
`coordination.runtime_shadow` 的 goal,并且只经 `authority-shadow status|drain`、
`coordination-shadow bootstrap|inspect|qualify|read-candidate|rollback` 与
`migrate-state` 断言,历史只经保留的 TypeScript store 读回。Python Todo writer
与 TypeScript lease writer 各留下 prepared 记录与 committed 标记,一次 drain 恰好
投递一次;有界 drain 可累积、空转 drain 不改变任何东西、writer 重放不铸造条目;
主写 replace 前后的 SIGKILL 结算为 `abandoned` 或 `committed_proven_by_readback`,
inline drain 内的 SIGKILL 由精确 receipt 恢复且不会二次投递;rollback 归档 pending
条目、把 capture 置于 `bootstrap_required`、重新 bootstrap 出新 lineage 并可重放;
三轮交错 writer(add、note update 及其无变化重复、显式 exclusion 设置与清除及其
无变化重复、acquire、renew、transfer、带 lease 的 complete 与 supersede 及其
fence close、capture-followups)让每次有界 qualification 都保持 matched,且
`sustained_parity_verdict=not_evaluated`;
直接改主文件会报告 `shadow_projection_drift`,其后的写入以
`source_partition_continuity_unproved` 挂起,只有 rollback 加重新 bootstrap 才能恢复;
event-only Todo 来源让 `inspect`、`qualify`、`read-candidate` 以
`event_log_writer_not_bound` 失败关闭而主写继续提交;`migrate-state` 对处于
active capture 的来源以 `shadow_source_replacement_requires_rebootstrap` 拒绝,
直到 rollback 并关闭 capture 之后才执行,迁移后的 goal 重新 bootstrap 出新 lineage
并完成 drain;十笔事务度量 file-v0 历史增长:完整投影全部保留、每笔增量最多增加
一条 live 记录,不宣称任何容量水平线。

Live 行按环境门控(`LOOPX_TEST_POSTGRES_URL`;`NOKV_COORDINATION_LIVE=1` 加
`NOKV_*` 栈变量;`LOOPX_NOKV_AUTHORITY_LIVE=1` 加 `LOOPX_NOKV_AUTHORITY_*` 输入)。
Expand All @@ -1524,11 +1545,14 @@ Live 行按环境门控(`LOOPX_TEST_POSTGRES_URL`;`NOKV_COORDINATION_LIVE=1`
`summary.privacy_violations` 阻止 green 退出,任何开关都不能放宽。

交付边界:test-only。没有任何生产入口构造任何 store;ladder 不新增产品路径,
只经保留的 TypeScript store 读取候选。Stage 2C parity 后半段
(`s2c2.*`:outbox 条目、幂等 drain、drain 前与 drain 中的 SIGKILL、带 pending
条目的 rollback、parity 相等与分歧、迁移 seed-and-drain、增长
度量)以 pending 行声明,而非宣称已完成。本小节记录的是上述阶段的可执行证据;
它不晋升任何 provider,也不完成 Stage 2C promotion。
只经保留的 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`。
`s2c2.sustained_parity_soak` 是由 7.2 节与车道 L 负责的 >=10 天合成 goal soak,
有界 qualification 继续报告 `sustained_parity_verdict=not_evaluated`。本小节记录
的是上述阶段的可执行证据;它不晋升任何 provider,也不完成 Stage 2C promotion。

### 11.3 剩余验证与晋升计划

Expand Down
55 changes: 42 additions & 13 deletions examples/shared-goal-authority-e2e/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -9,9 +9,10 @@ candidate only through the production TypeScript `FileAuthorityStore`, and
never reports green while a selected row is unverified.

```bash
python examples/shared-goal-authority-e2e/ladder.py # exit 1 here: live rows unverified, parity rows pending
python examples/shared-goal-authority-e2e/ladder.py # exit 1 here: live rows unverified, the soak row pending
python examples/shared-goal-authority-e2e/ladder.py --allow-unverified --allow-pending
python examples/shared-goal-authority-e2e/ladder.py --stage 2c1 --report-json ladder-report.json
python examples/shared-goal-authority-e2e/ladder.py --stage 2c2 --allow-pending --report-json ladder-report.json
python examples/shared-goal-authority-e2e/ladder.py --list
```

Expand All @@ -22,7 +23,10 @@ skips on Windows. Five `s2c1.*` rows whose assertions
through the same product path (configure round trip, default-off isolation,
candidate failure, crash gap, dual runtime root) are skipped in the default CI
projection to stay within the pytest job budget; `LOOPX_LADDER_FULL=1` runs
them in pytest, and the example runner always runs every row.
them in pytest, and the example runner always runs every row. The ten
`s2c2.*` rows carry the `stage2c_e2e` marker, so CI runs them in the stage2c
correctness job next to the other real-CLI, process-death and recovery
suites rather than in the pytest shards.

## Rows

Expand All @@ -40,14 +44,38 @@ them in pytest, and the example runner always runs every row.
| `s2c1.crash_gap_loses_observation` | 2c1 | real_cli | deterministic (POSIX) | a writer SIGKILLed while the observation lock is held commits its todo but leaves no candidate document; the next write captures the full two-todo snapshot without claiming an outbox or correlation |
| `s2c1.dual_runtime_root_consistency` | 2c1 | real_cli | deterministic | with `common_runtime_root` different from `--runtime-root`, todo add, task-lease acquire, todo update, capture-followups, and a leased completion all observe into one store identity; the head holds both todos and the released lease; the registry root gains neither a candidate lineage nor lease state |
| `s2c1.migration_seeds_new_lineage` | 2c1 | real_cli | deterministic | `migrate-state` dry run plans the seed without writing; execute seeds one fresh `file:` lineage at cursor `1` that carries no legacy identity, revision, source path, or private byte |
| `s2c2.outbox_prepared_then_committed_entries` | 2c2 | real_cli | deterministic | with the maintenance lock held, `todo add` (Python) and `task-lease acquire` (TypeScript) report `drain_deferred/drain_lock_busy`, `status` shows one `committed_pending` entry per partition with one prepared record and one committed marker on disk; one `drain` delivers both (`delivered=2`), history holds the bootstrap plus two committed receipts from both writer runtimes, and the next write delivers inline at cursor `4` |
| `s2c2.drain_idempotent` | 2c2 | real_cli | deterministic | three deferred entries: `drain --max-entries 1` delivers one (`pending_after=2`, `budget_exhausted`), the next `drain` delivers two, an idle `drain` reports `nothing_pending` with unchanged cursor, `head_digest` and `provider_revision`; receipts settle sequences 1..3; an idempotent same-key re-acquire carries no capture evidence and adds no transaction |
| `s2c2.sigkill_between_primary_write_and_drain` | 2c2 | real_cli | deterministic (POSIX) | `todo add` SIGKILLed at `before_replace`, `after_replace` and `before_marker` leaves one prepared-only entry each; `drain` settles it as `abandoned` (no-op, primary unchanged) or `committed_proven_by_readback`, the projection equals the primary, and `inspect` ends `matched` |
| `s2c2.sigkill_mid_drain` | 2c2 | real_cli | deterministic (POSIX) | `todo add` SIGKILLed at `before_commit`, `after_commit`, `after_cursor` and `between_unlinks`: the next `drain` delivers the uncommitted entry once or replays the committed one (`replayed=1, delivered=0`), history holds exactly one delivery, only the cursor remains, and a further drain is idle |
| `s2c2.rollback_with_pending_entries` | 2c2 | real_cli | deterministic (POSIX) | with one committed-pending and one prepared-only entry, `inspect` reports `outbox_pending` at the exact revision, a rollback preview writes nothing, `rollback --execute` applies and archives the outbox with both entries, the marker, the cursor and the manifest; capture then reports `bootstrap_required` while primary writes continue, a rebootstrap starts a new lineage from the current primary (three todos), and the historical rollback replays against it |
| `s2c2.parity_equal` | 2c2 | real_cli | deterministic | three cycles interleave Python Markdown writers (add, note update plus a no-change repeat, explicit exclusion set and clear plus a no-change repeat, complete, supersede, capture-followups) with TypeScript lease writers (acquire, renew, transfer, and the fence close of a leased complete or supersede); after each cycle `inspect` is `matched`, `qualify` with every required write class is `qualified` with `operation_count` equal to the delivered mutations, `read-candidate` returns the anchor todo, and `sustained_parity_verdict` stays `not_evaluated` |
| `s2c2.parity_divergent_detects_foreign_edit` | 2c2 | real_cli | deterministic | a direct edit of the primary makes `inspect` report `drifted/shadow_projection_drift`, `qualify` and `read-candidate` reject, a later `todo add` commits but its capture holds on `source_partition_continuity_unproved`; restoring the bytes does not requalify (`outbox_pending`), `drain` stays `stopped`, and only `rollback --execute` plus a fresh bootstrap qualifies again |
| `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`) |

Pending rows are declared in the report as `pending`, never counted as pass,
and they block a green exit unless `--allow-pending` is passed. The Stage 2C
parity rows are pending: `s2c2.outbox_prepared_then_committed_entries`, `s2c2.drain_idempotent`,
`s2c2.sigkill_between_primary_write_and_drain`, `s2c2.sigkill_mid_drain`,
`s2c2.rollback_with_pending_entries`, `s2c2.parity_equal`, `s2c2.parity_divergent_detects_foreign_edit`,
`s2c2.migration_seeds_and_drains`, `s2c2.growth_measurement_gate` (until the
Stage 2C parity PRs land).
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
qualification reports `sustained_parity_verdict=not_evaluated`, and no
`s2c2.*` row promotes a provider or completes the Stage 2C promotion.

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
POSIX crash worker that pauses one real CLI process at a named persistence
window so the row can SIGKILL it there. Neither substitutes a result or edits a
byte; every assertion still goes through `status`, `drain`, `inspect`,
`qualify`, `read-candidate`, `rollback`, `migrate-state` and the retained
TypeScript store read.

## Gates and environment variables

Expand All @@ -73,7 +101,7 @@ Exit code is `0` iff `fail == 0` and `privacy_violations == 0` and
(`unverified == 0` or `--allow-unverified`) and (`pending == 0` or
`--allow-pending`): a selected
row that never executed, whether gated or declared pending, is an unmet
obligation, so `--row s2c2.parity_equal` exits 1 with zero executions, and a
obligation, so `--row s2c2.sustained_parity_soak` exits 1 with zero executions, and a
mixed selection exits 1 even when its executable rows pass. `--list` only
prints the registry and never claims verification. A privacy scan runs over
the finished report: any occurrence of a temporary root, the home directory,
Expand All @@ -94,10 +122,11 @@ boundaries. [Installed-package E2E](installed.py) repeats the public lifecycle
outside the checkout for both wheel and sdist. [Negative controls](mutants.py)
deliberately remove correctness checks in disposable source copies.

These checks do not change the nine pending `s2c2.*` ladder declarations above.
Sustained production parity, the migration/growth gates, and promotion remain
separate obligations. A bounded qualification result reports
`sustained_parity_verdict=not_evaluated`.
The ten `s2c2.*` ladder rows above exercise the same lifecycle through the
public interfaces and read history only through the retained TypeScript store.
Sustained (elapsed-time) parity and promotion remain separate obligations: the
soak and the archive-after-lease capture gap stay pending declarations, and a
bounded qualification result reports `sustained_parity_verdict=not_evaluated`.

Future ladder rows must use the actual product interfaces:

Expand Down
Loading
Loading