Repository navigation
docs: record stage 11's decisions with their measurements and probe - #93
Merged
Merged
Conversation
The port's obligations, shaped as Accord writes them, are proved by cvc5 in under 0.4 s but not by Z3: it doesn't decide four of the recursive comparator's precedence clauses, and refutes neither list fault. The numeric fault is refuted by both. Refs #83
The first round left Z3 unable to prove the existential clauses of the recursive comparator and the equality clauses of the version comparators, and unable to refute two planted faults. This round asks whether a Z3 option, a different contract shape or a replayed counterexample changes that. No shape and no option meets the success rule. One shape (the existential form only, equality element by element) is proved by both solvers with smt.relevancy=1, but that result moves with Z3's seed, and no solver refutes the skip fault in it. A replayed counterexample from cvc5 refutes both list faults only in shapes that Z3 cannot prove. Adds the generator's contract shapes, run.sh options, a counterexample replay evaluator, a summary script and the results. Fixes the identity line to name the commit the cases were written at. Refs #83
cvc5 1.4.2 with --mbqi recurses without bound on a quantifier over a sequence variable (cvc5/cvc5#13161), which the fuel-limited spec function axioms have. Writing each axiom per sequence term avoids it, and a ground call-site reveal makes the last unstable Z3 case stable. Refs #83
Before choosing the syntax of records, sums, match and spec functions, check how readers who have never seen Accord read three spellings of the semver comparator. Every spelling read as Accord means it, so the rule written before the runs keeps the shortest. Refs #83
The probe read every spelling as meant, and an independent review found what it couldn't show: swapped fields under positional patterns, a second row syntax beside decide's, and records that could read as blocks. Record the accepted syntax, settle the recursion, record and Text rows of the native code constraints, and fix the roadmap's stage 11 row. Refs #83
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 the decisions for stage 11 (#83) before any compiler code, with the evidence behind them.
docs/design/measurements/2026-11-13-semver-contract/): four rounds on the SemVer comparator's obligations. The contract in two forms left Z3 undecided; spec functions encoded with a fuel-limited axiom, written per sequence term with a call-site reveal, are stable in both solvers over 21 variants per case (slowest 134 ms), on Windows and Linux. Enumerating small inputs catches all three planted faults. cvc5 1.4.2 recurses without bound with--mbqion a quantifier over a sequence (Unbounded recursion with --mbqi on a quantifier over a Seq variable cvc5/cvc5#13161), which the per-term encoding avoids.docs/design/probes/2026-11-13-structured-data/): three spellings of records, sums,matchand spec functions, read by twelve readers, all as meant; the result, the independent review's changes and the decision.syntax.md; rows 4, 5 and 6 of the native code constraints settled; the Dafny row of the influences updated; the roadmap's stage 11 row fixed.The decisions themselves are recorded on #83.
Verification:
cargo fmt --all --check,cargo clippy --workspace --all-targets --locked -- -D warningsandcargo test --workspace --locked(97 passed, 1 ignored) with the pinned solvers;score.py --self-testandmaterials.pypass. No code changes. Key measurement cases were rerun independently with both pinned solvers.Risk note: two-way door, no behavior change. Blast radius: design documents and measurement folders. Evidence: the measurement results, the probe replies and the checks above.
Refs #83