spec: Add Channel API contract, generator, and Emerald composition

specs/README.md

@@ -0,0 +1,200 @@
+# Emerald Specifications
+
+Formal specifications for Emerald, a modular framework combining [Malachite](https://github.com/informalsystems/malachite) consensus with [Reth](https://github.com/paradigmxyz/reth) execution for EVM networks.
+
+## Terminology
+
+- **Application**: the system being modeled (Emerald). Composes with external components treated as black boxes.
+- **Component**: an external black box (Malachite, Reth). Publishes a contract + generator.
+- **Boundary**: the API between application and component. Has a request side and a response side.
+
+The application can act as **server** at some boundaries (receives requests, sends responses) and **client** at others (sends requests, receives responses):
+
+| Boundary | Who sends requests | Who sends responses |
+|---|---|---|
+| Channel API | Malachite (component) | Emerald (application) |
+| Engine API | Emerald (application) | Reth (component) |
+
+## Contracts
+
+A **contract** defines properties over a shared boundary (request/response history). The contract is authoritative — it is the specification of the boundary.
+
+Both sides make guarantees about what they produce:
+
+- **Component guarantees**: safety + liveness on the requests it sends (if component sends requests) or on the responses it sends (if component sends responses)
+- **Application guarantees**: safety + liveness on the responses it sends (if application is server) or on the requests it sends (if application is client)
+
+Ordering properties are a subcategory of safety (constraints on valid sequences).
+
+For example:
+- **Channel API contract**: Malachite guarantees safety + ordering on the requests it sends (agreement, validity, height monotonicity). Emerald guarantees correctness on its responses (assumptions in the contract).
+- **Engine API contract**: Reth guarantees safety on the responses it sends (validationStability, buildIntegrity, headProgression). Emerald guarantees ordering on the requests it sends (buildLifecycle).
+
+### Contract Scope
+
+Contract scope depends on the component's nature, not the boundary type:
+- **Channel API**: global (cross-node) — because Malachite is a consensus protocol where safety is defined across nodes
+- **Engine API**: per-node — because each Reth is an independent local process
+
+## Generators
+
+A **generator** is a minimal state machine that produces traces satisfying the contract. The generator is a verified reference implementation — not authoritative, but useful for composition and testing.
+
+Generators publish:
+- **Primitive actions** — one per API method (`send*` for request sources, `respond*` for request handlers)
+- **Stutter action** — for steps that don't touch this boundary (`genUnchanged`, `rethUnchanged`)
+- **Fault actions** — crash/restart following the disk/mem convention from `faults.qnt`
+- **Pure helpers** — extracted logic reusable by the application (e.g., `computePayloadStatus`)
+- **CallSpec + dispatcher** — boilerplate mapping call spec variants to generator actions (candidate for language-level automation)
+
+Generator drive model depends on the component's role:
+- **Nondeterministic** (component sends requests): the generator chooses what to send (Channel API)
+- **Reactive** (component sends responses): the generator responds to application requests (Engine API)
+
+## Composition
+
+The application composes generators by calling their **published actions** — it never writes to generator state variables directly. Reading observable generator state (e.g., `reth::rethStates.get(node).disk.chain`) is fine.
+
+Each composed step follows the pattern:
+```
+all {
+  componentA::action(node),     // or componentA::unchanged
+  componentB::action(node),     // or componentB::unchanged
+  applicationStateUpdate(node),
+}
+```
+
+Every generator's state must be accounted for in every step (either an action or the stutter/unchanged action).
+
+### Work Queue
+
+When a single incoming request requires multiple outgoing actions (to the same or different components) plus local state updates, they go into a sequential **work queue** (`pendingWork: List[WorkItem]`), processed one item per step:
+
+```
+Incoming request → enqueue work items → process one per step → done
+```
+
+`WorkItem` is a sum type combining:
+- `EngineCall(spec)` — external call to a component (dispatched via CallSpec)
+- `FinalizeX(context)` — local application state update
+
+For example, `stepGetValue` enqueues:
+```
+[EngineCall(CallBuildRequest), EngineCall(CallGetPayload), FinalizeGetValue({proposal})]
+```
+
+Work items don't pass data to each other directly. They communicate through **observable component state**: the queue guarantees ordering, so each item reads the effects of prior items from the generator's state.
+
+### Generalization
+
+The work queue generalizes to any application that receives requests from one or more components and sends requests to one or more components:
+
+```
+                   ┌─────────────┐
+   Component A ───►│             │───► Component B
+   (requests in)   │ Application │     (requests out)
+   Component C ───►│             │───► Component D
+   (requests in)   └─────────────┘     (requests out)
+```
+
+Each external component the application sends requests to needs:
+- A **CallSpec** type — one variant per action, carrying parameters (e.g., `EngineCallSpec`)
+- A **dispatcher** — maps CallSpec variants to generator actions (e.g., `dispatchEngineCall`)
+
+The application defines:
+- **WorkItem** — combines CallSpec variants from all external components + local finalize handlers
+- **Work queue** — `List[WorkItem]` processed one per step
+- **Finalize handlers** — local state updates after external calls complete
+
+Adding a new external component (e.g., a mempool service) means adding its `CallSpec` variants to `WorkItem` and interleaving them with existing items. No changes to the queue processing infrastructure.
+
+Note: `CallSpec` types and dispatchers are boilerplate mechanically derivable from generator action signatures — candidates for language-level automation in Quint.
+
+## Conventions
+
+### Disk/Mem State Split
+
+All state follows the convention from `faults.qnt`:
+- **Disk**: survives restart, lost on crash
+- **Mem**: cleared on any fault (crash or restart)
+
+This applies uniformly across Emerald, Malachite (Channel API generator), and Reth (Engine API generator). Request/response histories are mem state.
+
+### Naming
+
+| Pattern | Meaning |
+|---------|---------|
+| `step*` | Composed transition (incoming request + enqueue work items) |
+| `stepAdvanceWork` | Process next work queue item |
+| `finalize*` | Local application state update (last item in a work sequence) |
+| `handle*` | Direct application state update (not queue-dispatched, e.g., `handleConsensusReady`) |
+| `respond*` | Engine API generator action (Reth responds to a request) |
+| `send*` | Channel API generator action (Malachite sends a request) |
+
+### Invariant Categories
+
+Invariants are organized by which component boundaries they check:
+
+| Category | Examples | Reads |
+|----------|----------|-------|
+| Emerald-only | `emerald_agreement`, `no_pending_at_current_height` | `emeraldState` only |
+| Emerald ↔ Malachite | `completion` | `emeraldState` + `gen::decisions` |
+| Emerald ↔ Reth | `head_tracks_consensus`, `validated_before_decided` | `emeraldState` + `reth::rethStates` |
+
+Generator contracts (`gen::contractInv`, `reth::contractInv`) are available as commented-out invariants for full verification that the composition doesn't violate either contract.
+
+## File Map
+
+### Shared
+
+| File | Purpose |
+|------|---------|
+| `faults.qnt` | `FaultEvent` type + disk/mem convention |
+
+### Channel API (Malachite ↔ Emerald)
+
+| File | Purpose |
+|------|---------|
+| `channel_api_contract.qnt` | Declarative properties (safety + ordering on Malachite's requests) |
+| `channel_api_generator.qnt` | Reference state machine producing valid request sequences |
+| `channel_api_generator_test.qnt` | Test module (3 nodes) |
+
+### Engine API (Emerald ↔ Reth)
+
+| File | Purpose |
+|------|---------|
+| `engine_api_contract.qnt` | Declarative properties (response correctness + request ordering) |
+| `engine_api_generator.qnt` | Reactive state machine modeling Reth's responses |
+| `engine_api_generator_test.qnt` | Test module (4 nodes, nondeterministic driver) |
+
+### Composition
+
+| File | Purpose |
+|------|---------|
+| `emerald_with_generator.qnt` | Channel API only composition (Emerald + Malachite) |
+| `emerald_with_generator_test.qnt` | Test module (3 nodes) |
+| `emerald_with_both_generators.qnt` | Three-way composition (Emerald + Malachite + Reth) |
+| `emerald_with_both_generators_test.qnt` | Test module (4 nodes) |
+
+### Legacy
+
+| File | Purpose |
+|------|---------|
+| `emerald.qnt`, `emerald_types.qnt`, `emerald_mbt.qnt`, `emerald_tests.qnt` | Earlier MBT artifacts, not actively maintained |
+
+## Future Work
+
+### State Separation
+Emerald currently reads generator state directly in several places (block construction, validity pre-checks, cross-component data flow, phase checks). Cleaner alternatives:
+- Engine call dispatch writes responses into Emerald's own state
+- Block construction becomes a work item that reads Reth state at execution time
+- Phase checks use observable flags published by generators
+
+### Independent Process Crashes
+Malachite+Emerald run in one process, Reth in another. Currently crashes are coordinated. Should add independent crash/restart actions (`stepEmeraldCrash/Restart`, `stepRethCrash/Restart`). Key constraint: Reth crash must clear Emerald's work queue (deadlock otherwise) and validation cache. Invariants must gate on Reth not being offline.
+
+### Engine API Phase 2
+`exchangeCapabilities`, `getPayloadBodiesByRange/Hash`, SYNCING state.
+
+### Language-Level Automation
+`EngineCallSpec` and `dispatchEngineCall` are boilerplate that Quint could auto-generate when a spec imports a generator. Related to the `satisfies`/`assumes` annotation proposal.

specs/canDecideTwoHeights_debug_report.md

@@ -0,0 +1,163 @@
+# Witness Debug Report: `canDecideTwoHeights`
+
+**Spec:** `emerald/specs/emerald_with_both_generators_witnesses.qnt`
+**Date:** 2026-03-11
+**Result:** Witness not violated by uniform random simulation; violated by biased step (scenario confirmed reachable)
+
+---
+
+## Goal Analysis
+
+**Witness Definition:**
+```quint
+val canDecideTwoHeights: bool =
+  NODES.toSet().forall(n => emeraldState.get(n).disk.last_decided_height < 2)
+```
+
+**Target Condition:** Some node with `last_decided_height >= 2`
+
+**Required Path:**
+```
+init
+→ height-1 full pipeline × quorum (3/4 nodes)
+→ sendDecided(h=1) × quorum → FinalizeDecided → consensus_height = 2
+→ StartedRound(h=2) → GetValue(node2) → newPayload × quorum
+→ sendDecided(h=2) → FinalizeDecided → last_decided_height = 2
+```
+
+---
+
+## Static Analysis
+
+**Actions That Advance Goal:**
+
+- **`sendDecided`** (`channel_api_generator.qnt`) — advances height after quorum
+  - ✓ `phase == InRound or Syncing`
+  - ✓ `proposal.height == ns.mem.height`
+  - ✓ `deliveredProposals.contains(proposal)`
+  - ✓ `proposalSupport.size() * 3 > NODES.length() * 2` (requires ≥3/4 nodes)
+
+- **`sendGetValue`** (`channel_api_generator.qnt`) — creates the height-2 proposal
+  - ✓ `phase == InRound at height 2`
+  - ✗ `node == proposer_for(2, 0) == "node2"` ← **PROPOSER CONSTRAINT**
+
+No static impossibility: 4 nodes, quorum = 3 — mathematically satisfiable.
+
+---
+
+## Dynamic Analysis
+
+**Search Progression:**
+
+| Pass | Samples | Steps | Result |
+|------|---------|-------|--------|
+| 1 | 5,000 | 500 | No violation |
+| 2 | 6,000 | 600 | No violation |
+
+**Relaxation Test:**
+
+| | Condition |
+|---|---|
+| Original | `forall(n => last_decided_height < 2)` |
+| Relaxed | `not(exists(n1, n2 \| n1≠n2, both last_decided_height >= 1))` |
+| Result | **NOT VIOLATED** (2,000 samples × 200 steps) |
+
+**Insight:** The blocker is upstream — two nodes never both complete height-1, so the height-2 pipeline never starts.
+
+**Sample Traces:** One node finishes height-1 and advances, but no second node completes `FinalizeDecided(h=1)`. The Working-at-h=2 state IS reachable (GW3 violated), confirming the first node enters the height-2 round. But without the height-2 proposer (node2) completing height-1 first, no height-2 proposal is ever created.
+
+---
+
+## Guard Analysis
+
+**Goal Variable:** `last_decided_height` (needs to reach >= 2)
+
+**Guard witnesses tested:**
+
+| Guard | Result | Meaning |
+|-------|--------|---------|
+| GW1: one node has `last_decided_height >= 1` and `consensus_height >= 2` | ✓ VIOLATED | One node CAN complete height-1 and advance |
+| GW2: two distinct nodes both have `last_decided_height >= 1` | ✗ NOT VIOLATED | **Confirmed blocker** |
+| GW3: any node in `Working` phase at `consensus_height == 2` | ✓ VIOLATED | StartedRound at height 2 is reachable |
+| GW4: any node has `undecided_proposals != Set()` at `consensus_height == 2` | ✗ NOT VIOLATED | No height-2 proposal ever created |
+
+**Blocking Guards:**
+
+- Two distinct nodes both reaching `last_decided_height >= 1`: the height-2 quorum (3/4 nodes) requires all key nodes to complete height-1 first, but random simulation never drives enough nodes to completion.
+- `undecided_proposals != Set()` at `consensus_height == 2`: no height-2 proposal is ever created because node2 (the only valid proposer at h=2, r=0) never advances past height-1 in observed traces.
+
+**Satisfiable Guards:**
+
+- ✓ One node reaches `last_decided_height >= 1` and `consensus_height >= 2`
+- ✓ One node enters `Working` phase at `consensus_height == 2`
+
+---
+
+## Diagnosis
+
+**Category:** PROBABILISTIC_TRAP
+
+Only one node ever completes height-1 under random simulation; the remaining three are stranded at height-1, making the height-2 quorum structurally unachievable.
+
+By the time the first node calls `sendDecided(h=1)`, the quorum guard is already satisfied (3 nodes supported the proposal), so `sendDecided(h=1)` is also enabled for the other three nodes. However, the random simulator picks uniformly across all enabled actions. Completing the remaining three `sendDecided(h=1)` calls — each followed by ~20 Engine API work steps — before making further progress on the height-2 pipeline is a specific ordering that occurs with very low probability. There is no explicit bias toward one node; the three remaining nodes are probabilistically starved in the uniform random walk.
+
+Round timeouts do not rescue the situation. `sendStartedRoundAfterTimeout` is a per-node action: it advances only the firing node's generator from `InRound(h=2, r=0)` to `InRound(h=2, r=1)`, where `proposer_for(2,1) = "node3"`. But node3's generator is still in `InRound(h=1)` — it never completed height-1. The `sendGetValue` guard requires `phase == InRound` at the target height, so node3 cannot act as proposer at height-2 regardless of how many rounds node1 advances through. The other potential proposers at higher rounds face the same constraint.
+
+The height-2 quorum guard (`proposalSupport.size() * 3 > NODES.length() * 2`, i.e. ≥3 nodes) is therefore unreachable: with only one node at height-2, at most one node can ever support a height-2 proposal.
+
+**Key Evidence:** GW1 violated (one node completes h=1 and advances), GW2 NOT violated (only one node ever completes h=1 — not two), GW3 violated (Working at h=2 reachable for that one node), GW4 NOT violated (no height-2 proposal is ever created), relaxed witness also NOT violated — all consistent with probabilistic starvation of height-1 completion for nodes 2–4, not a spec bug.
+
+---
+
+## Biased Step
+
+The diagnosis was confirmed by implementing a biased step action in `emerald_with_both_generators_witnesses.qnt`. The biased step corrects the scheduler distribution by restricting node selection: while any node has `last_decided_height < 1`, only those behind nodes are eligible to act. Once all four nodes complete height-1, the step reverts to uniform random selection across all nodes.
+
+```quint
+action biasedStep = {
+  val behindNodes = NODES.toSet().filter(n =>
+    emeraldState.get(n).disk.last_decided_height < 1
+  )
+  val nodePool = if (behindNodes != Set()) behindNodes else NODES.toSet()
+  nondet node = nodePool.oneOf()
+  any {
+    stepConsensusReady(node),
+    stepStartedRound(node),
+    stepGetValue(node),
+    nondet proposal = allKnownProposals.oneOf()
+    stepReceivedProposal(node, proposal),
+    nondet proposal = allKnownProposals.oneOf()
+    stepDecided(node, proposal),
+    stepProcessSyncedValue(node),
+    stepAdvanceWork(node),
+  }
+}
+```
+
+**Design notes:**
+- `allKnownProposals` aggregates proposals from each node's `undecided_proposals ∪ pending_proposals ∪ decided_proposals`, avoiding the need for `gen::proposals` which is not re-exported from the composition module.
+- `stepGetDecidedValue` is omitted — it requires `gen::MAX_HEIGHT` (also not re-exported) and is not on the critical path to height-2.
+- Fault actions (`stepNodeCrash`, `stepNodeRestart`) are omitted — a crash resets `last_decided_height` to 0, re-adding the node to `behindNodes` and trapping the simulation before the all-complete condition is ever satisfied.
+
+**Result:** Invariant violated in 594ms (~99 traces/second, 200 samples × 500 steps).
+
+```
+quint run emerald/specs/emerald_with_both_generators_witnesses.qnt \
+  --main=emerald_with_both_generators_witnesses \
+  --step=biasedStep \
+  --invariant=canDecideTwoHeights \
+  --max-steps=500 --max-samples=200 --backend=rust
+# [violation] Found an issue (594ms at 99 traces/second).
+```
+
+This confirms `canDecideTwoHeights` is a valid reachability witness. The scenario is reachable; uniform random simulation simply cannot find it because it requires all four nodes to complete the ~20-step height-1 Engine API pipeline in a coordinated order before any node advances to height-2.
+
+---
+
+## Where to Investigate
+
+1. **`channel_api_generator.qnt` `sendDecided` guard** — once the quorum for height-1 is met, `sendDecided(h=1)` is enabled for all four nodes simultaneously; confirm the ~20-step Engine API work chain that must complete per node before any can advance to height-2.
+
+2. **`channel_api_generator.qnt` `sendGetValue` / `sendStartedRoundAfterTimeout` guards** — `sendGetValue` requires `phase == InRound` at the target height; nodes still at height-1 cannot act as proposer at height-2 even if another node's timeout advances the round there. Confirm no path exists for a height-1 node to skip ahead.
+
+3. ~~**Use a biased scheduler or manual ITF trace** to confirm reachability: force all 4 nodes to complete `sendDecided(h=1)` (and their Engine API chains) before any node's height-2 pipeline begins, then let the simulator proceed to height-2.~~ **Resolved** — see Biased Step below.