Sequencer documentation

app-sequencer/advanced/divergence.md

@@ -0,0 +1,112 @@
+---
+title: "Divergence and the content-identity check"
+sidebar_label: "Divergence detection"
+description: "How accepted base-layer batch content is compared with local sealed content, what the check cannot prove, and why divergence stops the sequencer."
+---
+
+Canonical divergence occurs when a batch accepted at a given nonce does not match the valid batch the sequencer sealed for that nonce, or when no matching valid local batch exists.
+
+This condition invalidates the assumption that the local batch tree mirrors canonical history. The sequencer records the mismatch and stops before the accepted frontier, snapshot lifecycle, or recovery logic can advance from an incorrect identity.
+
+## What the check compares
+
+When the sequencer seals a batch, it encodes the exact payload the submitter will broadcast and stores its Keccak-256 hash with the batch record. The payload hash is written in the same database operation that seals the batch and is protected from later modification.
+
+When base-layer synchronization encounters a batch that the scheduler acceptance predicate considers fully accepted, the sequencer:
+
+1. reads the accepted batch nonce and payload from the safe input stream;
+2. finds the valid closed local batch carrying that nonce;
+3. hashes the landed payload bytes;
+4. compares the landed hash with the seal-time local hash.
+
+![The sequencer hashes a batch when it is sealed and hashes the accepted payload observed in the safe base-layer view. A matching local batch with equal hashes advances the accepted frontier. A missing local batch is foreign, while different hashes are a mismatch; either failure records persistent divergence and freezes the frontier.](../images/divergence-check.jpg)
+
+Content-equal copies are accepted. The identity of the physical base-layer transaction does not matter because identical batch bytes have the same scheduler effect.
+
+## Divergence classifications
+
+The implementation records two kinds of content-identity violation:
+
+| Kind       | Meaning                                                                                                          |
+| ---------- | ---------------------------------------------------------------------------------------------------------------- |
+| `foreign`  | The scheduler accepted a nonce for which no valid closed local batch exists                                      |
+| `mismatch` | A valid closed local batch exists at the nonce, but its sealed payload hash differs from the landed payload hash |
+
+Possible causes include a delayed transaction from an abandoned branch, use of the submitter key outside the sequencer, database corruption, or a defect that changed sealed or submitted content.
+
+## When the comparison runs
+
+The comparison runs only after the off-chain scheduler predicate accepts a batch from the base-layer safe input stream. It does not compare payloads that are:
+
+- undecodable as batches;
+- stale;
+- carrying the wrong batch nonce;
+- below the batch-tree anchor after checkpoint recovery.
+
+The first three cases have no scheduler effect, so their content cannot change canonical application state. Inputs below a recovery anchor belong to trusted history already folded into the checkpoint. The rebuilt local tree begins at the anchor and intentionally contains no earlier batch rows.
+
+## Detection timing
+
+Detection begins when the landing appears in the configured RPC endpoint's safe view and the input reader synchronizes that range. It therefore follows the base layer's safe-head delay and the input reader's polling cadence.
+
+There is no fixed detection duration that applies to every supported chain or provider. The batch submitter's configurable confirmation depth also does not control this check. The authoritative trigger is inclusion in the safe input view used to construct the accepted frontier.
+
+Soft confirmations issued before detection may already depend on a local state that canonical execution will not reproduce. This residual window is part of the optimistic design.
+
+## Atomic marker and frozen frontier
+
+The divergence marker is inserted in the same database transaction as the safe-head synchronization that detects the violation. The accepted landing is not added to `safe_accepted_batches`.
+
+Once the marker exists:
+
+- accepted-frontier population returns without scanning further;
+- snapshot promotion cannot advance through the mismatched landing;
+- the danger check reports canonical divergence before every staleness condition;
+- startup refuses automatic recovery;
+- the process exits with terminal code `30`.
+
+The marker persists across restarts. A supervisor that ignores code `30` will repeatedly start a process that immediately refuses the same state.
+
+## Why automatic recovery is unsafe
+
+Preemptive recovery assumes that every accepted nonce identifies the matching local batch. It uses that accepted frontier to select a cascade point and preserve the valid prefix.
+
+A content-identity violation disproves that assumption. Cascading from the local tree could preserve state that was never canonical or discard the wrong branch. The sequencer therefore refuses to derive a repair from the record whose identity is in question.
+
+The supported remedy is to preserve evidence, stop the old deployment, and rebuild a fresh data directory using [Cockroach recovery](../recovery/cockroach.md).
+
+## What the check does not prove
+
+The content-identity check proves that accepted batch bytes match the bytes sealed locally for the same nonce. It does not compare resulting application state.
+
+Matching bytes can still produce different state if:
+
+- the application is nondeterministic;
+- the Cartesi machine and live prediction run different application versions;
+- the scheduler implementations disagree about execution;
+- direct inputs are applied differently outside the compared batch payload.
+
+The independent watchdog addresses this broader class by replaying canonical base-layer inputs and comparing resulting state bytes with the sequencer's finalized snapshot. See [Monitoring and watchdog operation](../operations/monitoring.md).
+
+## Prevention and residual risk
+
+Wallet-nonce resolution reduces the chance that an abandoned submission later claims a relevant slot, but it does not remove the need for content comparison. A checkpoint rebuild has the additional limitation that its fresh database lacks the original wallet-nonce watermark. See [Flush unresolved wallet nonces](../operations/orchestration.md#flush-unresolved-wallet-nonces) and [Cockroach recovery](../recovery/cockroach.md#resolve-the-submitter-wallet).
+
+## Operator response
+
+When canonical divergence is reported:
+
+1. stop automatic restarts and prevent use of the submitter key;
+2. preserve the database, logs, RPC observations, and base-layer transaction evidence;
+3. identify whether the marker is `foreign` or `mismatch`;
+4. investigate key use, delayed transactions, software versions, and storage integrity;
+5. fix the underlying cause before rebuilding;
+6. rebuild from a verified checkpoint and validate the result with the watchdog.
+
+Removing the marker from the database is not a repair. It would allow frontier processing to continue without restoring the rejected identity assumption.
+
+## Next steps
+
+- Review the acceptance algorithm in [Scheduler semantics](./scheduler-semantics.md).
+- Review the freeze and wallet-nonce properties in [Invariants](./invariants.md).
+- Prepare terminal-failure handling with [Failure modes](../recovery/failure-modes.md).

app-sequencer/advanced/formal-verification.md

@@ -0,0 +1,191 @@
+---
+title: "Formal verification"
+sidebar_label: "Formal verification"
+description: "What the bounded TLA+ model proves about preemptive recovery, its configured state space, and the behavior outside its scope."
+---
+
+The sequencer repository contains a TLA+ specification of the slot-level preemptive recovery design. TLC explores every reachable state within the configured bounds and checks that declared safety invariants remain true.
+
+This provides stronger evidence than a set of hand-selected examples for the behavior represented by the model. It does not prove the complete sequencer implementation correct.
+
+## Why model the recovery protocol
+
+Recovery depends on interleavings between:
+
+- local batch creation and submission;
+- wallet-nonce assignment;
+- base-layer inclusion or replacement by a flush transaction;
+- movement from included to safe;
+- scheduler acceptance or rejection;
+- suffix invalidation and replacement branching.
+
+Many failures require an unusual order, such as an abandoned transaction winning a nonce slot after recovery has started. A model checker systematically explores those orders within a finite configuration and returns a concrete trace if one reaches an invalid state.
+
+## Model state
+
+The specification represents:
+
+- a valid batch spine with `Gold`, `Silver`, `Bronze`, `Pending`, and open `Tip` states;
+- invalidated branches;
+- the current safe block;
+- the submitter's next wallet nonce;
+- the next wallet-nonce slot processed by the base layer;
+- included base-layer entries;
+- the scheduler cursor and next expected batch nonce;
+- submitted batches detached from the valid spine by recovery.
+
+A genesis sentinel provides an initial accepted ancestor in the model. The implementation handles the first-batch edge structurally and does not submit a sentinel batch.
+
+## Modeled transitions
+
+TLC explores combinations of these actions:
+
+| Action             | Meaning                                                    |
+| ------------------ | ---------------------------------------------------------- |
+| `AdvanceTip`       | Close the open batch and append a new tip                  |
+| `SubmitBatch`      | Assign wallet nonces to every unsubmitted pending batch    |
+| `L1IncludeSpine`   | Let a valid submitted batch win its wallet-nonce slot      |
+| `L1SkipSpine`      | Let a flush no-op win and displace a valid submitted batch |
+| `L1IncludeDead`    | Let a previously invalidated batch win its unresolved slot |
+| `L1SkipDead`       | Let a flush no-op displace an invalidated batch            |
+| `AdvanceSafeBlock` | Move included batches into the safe view                   |
+| `SchedulerStep`    | Process a safe entry and accept it or reject it            |
+| `SchedulerSkip`    | Advance over a wallet-nonce slot consumed by a no-op       |
+| `Resolve`          | Invalidate a stale suffix and create a replacement tip     |
+
+At a contested wallet-nonce slot, the model allows either the batch or the flush transaction to win. This captures the adversarial outcome recovery must tolerate.
+
+![The bounded recovery model moves from an open batch to a closed and submitted batch, lets either the batch or a flush transaction win the base-layer nonce slot, advances an included batch to the safe scheduler view, and either accepts it or resolves an invalid suffix by creating a replacement branch.](../images/recovery-model-transitions.jpg)
+
+## Checked safety invariants
+
+The configured invariant `Inv` combines the following properties:
+
+| Invariant               | Property checked                                                               |
+| ----------------------- | ------------------------------------------------------------------------------ |
+| `TypeOK`                | The spine remains non-empty and the model's counters remain natural numbers    |
+| `BatchNoncesContiguous` | Non-tip batches on the valid spine carry contiguous nonces                     |
+| `InvalidOnlyOnGold`     | Invalid branches attach only to accepted `Gold` ancestors                      |
+| `ZombieSafety`          | The scheduler's expected nonce equals the length of the accepted `Gold` prefix |
+| `L1WNonceUnique`        | No two included base-layer entries occupy the same wallet nonce                |
+| `L1BeforeCursor`        | Every included entry is below the next unprocessed base-layer wallet slot      |
+| `SchedulerBehindL1`     | The scheduler cursor never advances beyond base-layer slot processing          |
+| `DeadNotYetIncluded`    | Detached submitted batches retain only unresolved wallet-nonce slots           |
+
+`ZombieSafety` is the central recovery property. It states that late, displaced, or invalidated submissions never make the scheduler accept more or fewer batches than the valid `Gold` prefix represents.
+
+## Safety is not liveness
+
+The model checks invariants in every reachable state. These are safety claims: specified bad states are not reached.
+
+It does not establish that:
+
+- the base layer eventually includes a transaction;
+- the safe head eventually advances;
+- a flush eventually completes;
+- recovery always terminates;
+- the sequencer resumes serving users within a time bound.
+
+Those are liveness and operational claims. They depend on the base layer, provider availability, supervisor behavior, configuration, and implementation tests.
+
+## Configured bounds
+
+The committed TLC configuration uses:
+
+| Constant          | Value |
+| ----------------- | ----: |
+| `MaxBatchIndex`   |     5 |
+| `MaxSafeBlock`    |     5 |
+| `MAX_WAIT_BLOCKS` |     2 |
+| `MaxWalletNonce`  |     8 |
+
+The implementation's staleness constant is `1200`, while the model uses `2`. This reduction preserves the transition from fresh to stale but does not reproduce production timing or scale.
+
+Wallet nonces need a separate bound because repeated displacement and resubmission can keep generating new values. Increasing any bound can expand the state space sharply.
+
+The recovery design notes record a completed exploration of approximately 157 million states with no invariant violations for the committed model and configuration. That result applies only to the specification version and bounds that produced it.
+
+## What the model does not cover
+
+The TLA+ model intentionally excludes major parts of the deployed system:
+
+- the danger threshold and preemptive margin;
+- wall-clock estimation during an RPC outage;
+- the complete runtime sequence of stop, restart, flush, wait, synchronize, and resume;
+- process crashes and SQLite or filesystem transaction boundaries;
+- the implementation's danger-threshold invalidation of an open tip;
+- the implementation's direct cascade of a pending batch displaced by a flush;
+- direct-input queuing, censorship backstop, frames, transaction fees, and application execution;
+- content-identity divergence detection;
+- snapshots, checkpoint recovery, feeds, and HTTP behavior;
+- signatures, chain identity, RPC completeness checks, and cryptographic assumptions.
+
+Two differences deserve particular attention:
+
+1. The model resolves an aging open tip at `MAX_WAIT_BLOCKS`; the implementation can replace it earlier at the configured danger threshold.
+2. The model does not directly represent the implementation path that cascades a pending frontier batch after a flush no-op displaced it.
+
+The safety of those implementation paths is supported by separate reasoning and tests. TLC has not explored them as equivalent actions.
+
+## Relationship between model and code
+
+The specification is maintained manually. There is no refinement proof, trace conformance check, verified compiler, or generated implementation connecting it to the Rust code.
+
+A successful TLC run means:
+
+- the model satisfies its declared invariants within the selected bounds;
+- TLC found no represented execution that violates those properties.
+
+It does not mean:
+
+- the Rust implementation exactly matches every modeled transition;
+- the model contains every relevant failure;
+- larger bounds cannot reveal a counterexample;
+- the surrounding application and infrastructure are correct.
+
+Treat model checking as one layer of evidence alongside implementation review, unit tests, end-to-end recovery scenarios, and production monitoring.
+
+## Run the model checker
+
+The specification, configuration, and task file are located at:
+
+```text
+sequencer/docs/recovery/
+  preemptive.tla
+  preemptive.cfg
+  justfile
+```
+
+With TLC installed and available as `tlc`, run:
+
+```bash
+cd sequencer/docs/recovery
+just check-preemptive
+```
+
+The task executes:
+
+```bash
+tlc -workers auto -deadlock preemptive.tla
+```
+
+You can point the task at another TLC executable with the `TLC` environment variable. Start with the committed bounds. Record the specification revision, configuration, TLC version, worker count, state count, runtime, and result for every verification run.
+
+## Interpreting a counterexample
+
+When TLC reports an invariant violation:
+
+1. identify the first transition after which the property becomes false;
+2. determine whether the trace represents permitted production behavior;
+3. check whether the specification, implementation, or invariant is wrong;
+4. convert the trace into a focused implementation test when applicable;
+5. rerun the original and corrected models with the same bounds;
+6. increase relevant bounds to look for a larger related counterexample.
+
+A counterexample can reveal an incorrect design or an inaccurate model. It should not be dismissed solely because production code is structured differently.
+
+## Next steps
+
+- Review the modeled recovery path in [Preemptive recovery](../recovery/preemptive.md).
+- Compare the checked properties with [Cross-module invariants](./invariants.md).
+- Review unmodeled ordering behavior in [Scheduler semantics](./scheduler-semantics.md).