Repository navigation
docs: settle stage 10's semantics before its code - #84
Merged
Merged
Conversation
Stage 10 adds machines, and the native code constraints list effects, value semantics, normalization and the boundary as costly to reverse. Record each decision before any code, with two probes behind them: a hand-written stand-in replacing opossum's breaker state with opossum's tests unchanged, and ProviderRetry's inductive obligations under both solvers with and without helper invariants. Both probes are kept with their scripts so they can be rerun. Refs #82
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
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.
Records stage 10's decisions before any code, as #69 did for stage 9, with the evidence behind them.
What changes
ROADMAP.md: a decision for stage 10's semantics, and stage 10 marked next.Bools; events are pure functions with their choices as parameters; and time is an ordinary field.not_inductive. Exploration is an annotation on the obligation, not an outcome.accord buildwrites a machine only when its invariants are proved.docs/design/native-code-constraints.md: rows 2, 5, 8 and 10 record what machines decide for effects, value semantics, normalization and the boundary, and a bullet under "approved but not implemented" records how an invariant's outcomes are reached.docs/design/measurements/2026-11-12-stage-10-machines/: the two probes, with scripts to rerun them.The owner's decisions behind the opossum port are recorded in #82.
Verification
opossum/run.shandprovider-retry/run.sh, both run from a fresh folder, reproduce every result in the measurement's README.cargo fmt --all --check,cargo clippy --workspace --all-targets --locked -- -D warningsandcargo test --workspace --locked(with the pinned solvers) pass. This change touches no code.Not established: both probes are hand-written, so they don't show what Accord will generate. ProviderRetry's 148 reachable states haven't been compared with TLC.
Risk note
Two-way door, no behavior change: documentation and scripts only. Blast radius: the design record that stage 10's code will follow. The decisions are costly to reverse once code depends on them, which is why they're recorded first. Evidence: the two reproducible runs above.
Refs #82