spec: Add Channel API contract, generator, and Emerald composition#236
Draft
spec: Add Channel API contract, generator, and Emerald composition#236
Conversation
Co-Authored-By: Claude Opus 4.6 <[email protected]>
… both channel and engine API
Replace PendingWork/ProcessingContext split with a flat List[WorkItem] queue where engine API calls and local Emerald state updates are interleaved as equal work items. This generalizes naturally to apps talking to multiple external components. Key changes: - WorkItem sum type: EngineCall | FinalizeGetValue | FinalizeReceivedProposal | FinalizeDecided - pendingWork: List[WorkItem] replaces Option[PendingWork] - stepAdvanceWork processes one item per step with uniform queue pop - Handlers renamed handle* → finalize* to reflect they update Emerald state - Stale proposal check moved to stepReceivedProposal (before enqueueing) - Removed rethUnchanged alias, PendingWork type, ProcessingContext type - Added TODOs for EngineCallSpec boilerplate and state separation Co-Authored-By: Claude Opus 4.6 <[email protected]>
- Categorize invariants by scope: Emerald-only, Emerald↔Malachite, Emerald↔Reth - Remove chain_continuity_inv (Reth contract property, duplicated from reth::contractInv) - Add commented channelContractInv/engineContractInv for full contract verification - Update independent crash TODO with concrete design: deadlock analysis, work queue clearing, validated_cache handling, invariant gating on Reth phase Co-Authored-By: Claude Opus 4.6 <[email protected]>
- Add biasedStep action to witnesses module: restricts node selection to nodes with last_decided_height < 1 until all nodes complete height-1, correcting the probabilistic starvation that prevents uniform random simulation from finding the witness - Add allKnownProposals helper to derive proposal set from Emerald state, avoiding the need for gen:: which is not re-exported from the composition - Update canDecideTwoHeights_debug_report.md: correct diagnosis (uniform random walk starvation, not scheduler preference), add round-timeout analysis, add Biased Step section with confirmed violation result Co-Authored-By: Claude Sonnet 4.6 <[email protected]>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Work in progress. DO NOT MERGE
Goal: Component-Based Specification in Quint
Each reusable component publishes: Spec (internal logic), Contract (declarative API guarantees), Generator (small state machine producing valid traces). The contract is authoritative; the generator is a verified tool. Consumers trust the contract and check only their own invariants.
Current Spec Artifacts (Channel API)
All in
emerald/specs/:faults.qntReusable fault event types and disk/mem convention
channel_api_contract.qntProperties over
ChannelState = { disk: { all_proposals, decisions }, mem: { event_history } }:channel_api_generator.qntMinimal state machine producing valid Channel API message sequences:
emerald_with_generator.qntComposition via
all { gen::sendX(node), handleX(node) }: