Model ledger types and persistence in TLA+

[Copilot]

The ledger protocol spans untrusted requests, validated artifacts, Git-backed persistence, and disposable projections. This PR adds a bounded TLA+ model for the raw ledger and all six built-in types, with results linked to concrete conformance tests.

• Protocol model: Represents queued requests, validation, concurrent branch advances, stale-artifact revalidation, persistence, and maintenance without treating an accepted request as durable.
• Ledger semantics: Models replay for log, set, map, table, counter, and notes. TLC configurations check each type’s reachable states against safety invariants, including:

  ReplayAgreement == projection = Replay(history)

• Implementation alignment: Adds JavaScript witnesses for each type and a concurrent table-insert conflict. Documents the bounded results and what the model does not cover.

The TLC results establish safety within the configured bounds, not an unbounded proof of the implementation.

---

Generated by 👨‍🍳 PR Sous Chef · pi · gpt54 · 22.4 AIC · ⌖ 8.76 AIC · ⊞ 9.4K · ◷
_{Comment /souschef to run again}

[Copilot]

Copilot review overview

🟡 Changes recommended

The documented TLC identifier is not a valid version, preventing reliable reproduction of the reported results.

Review effort: Balanced
Findings: None

What changed in this PR

Adds a bounded TLA+ model of ledger validation, persistence, replay, concurrency, and maintenance semantics.

Changes:

• Models raw ledgers and six built-in ledger types with safety invariants.
• Adds bounded TLC configurations and documented results.
• Adds JavaScript conformance witnesses using production reducers and validation.

File	Description
specs/​ledger/​LedgerProtocol.tla	Defines the protocol model and invariants.
specs/​ledger/​README.md	Documents scope, results, and reproduction steps.
specs/​ledger/​raw.cfg	Configures raw-ledger checking.
specs/​ledger/​log.cfg	Configures log checking.
specs/​ledger/​set.cfg	Configures set checking.
specs/​ledger/​map.cfg	Configures map checking.
specs/​ledger/​table.cfg	Configures table checking.
specs/​ledger/​counter.cfg	Configures counter checking.
specs/​ledger/​notes.cfg	Configures notes checking.
actions/​setup/​js/​ledger_protocol_model.test.cjs	Adds concrete implementation witnesses.

---

💡 Add a code-review agent skill for context-aware, tailored reviews. Learn more in the docs.

[gh-aw-bot]

@copilot PR #64957 still needs follow-up before a maintainer can investigate quickly.

Please address the review feedback on the invalid TLC version in specs/ledger/README.md, push the fixes, and then run the pr-finisher skill to wrap up the PR.

Generated by 👨‍🍳 PR Sous Chef · pi · gpt54 · 22.4 AIC · ⌖ 8.76 AIC · ⊞ 9.4K · ◷
_{Comment /souschef to run again}

[Copilot]

@copilot PR #64957 still needs follow-up before a maintainer can investigate quickly.

Please address the review feedback on the invalid TLC version in specs/ledger/README.md, push the fixes, and th...

Updated specs/ledger/README.md to identify TLA+ Tools 1.8.0 and link to its release. Pushed as 70f8703.

[github-actions]

🎉 This pull request is included in a new release.

Release: v0.90.3