Ask the proof model about a fraction - #929
Merged
Merged
Conversation
onatozmenn
enabled auto-merge (squash)
August 5, 2026 13:59
`design/fractional-values.md` closed with a threshold: a contract that has to say something about a fractional quantity, which writing the library never tested. This writes them and rereads the page. The answer does not change, and the reason is better than the argument the page had. A `Ratio` is two `Int`s, so a clause about one is a clause about integers: `ensures ok => result.bottom > 0` is a fact about a field the interval model already reasons about. Ninety-two obligations in that module are proven, three are tested by generated inputs, and eleven are guarded, every one of them a call whose arguments are arithmetic. The worry that a fractional type would reach into `facts` was a worry about a representation, and a fraction made of two integers reaches into nothing. Writing them found a bug nothing else had. `absolute(n)` answers `0 - n`, and the smallest `Int` has no positive counterpart, so `ratio(Int.min, 1)` stopped the program. Nothing had noticed, because nothing had been asked what `absolute` promises. The precondition is `n > Int.min` and `ratio` turns the number away at the door, so everything below it is proven rather than checked again. One thing the checker could not follow, written down where it bit: the door is `if top <= Int.min` rather than `if top == Int.min`. The two say the same thing about an `Int`, but a comparison narrows a range and a disequality does not, so one spelling leaves the call below proven and the other leaves it guarded. The threshold test turns around with the threshold: it used to watch for the clauses appearing and now holds them there, along with a program that uses the library still running. Also measured, and written into the open question rather than left as a quote from a stale count: of the twenty-nine calls to `at` in the library and the corpus, twelve pay for a failure and exactly one is a bound the checker could discharge today. The rest index a list that came back from a call, and `length(f(x))` is not a term the prover holds. What is in the way of spending an index proof is not the prelude name.
onatozmenn
force-pushed
the
contracts-over-a-fraction
branch
from
August 5, 2026 14:01
82d426b to
e7ba407
Compare
Merged
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.
design/fractional-values.md closed with a threshold: a contract that has to say something about a fractional quantity. This writes them and rereads the page.
The answer does not change and the reason is better than the argument the page had: a Ratio is two Ints, so a clause about one is a clause about integers. 92 obligations in the module are proven, 3 tested by generated inputs, 11 guarded, and every guarded one is a call whose arguments are arithmetic.
Writing them found a bug: ratio(Int.min, 1) stopped the program, because absolute(n) answers 0 - n and the smallest Int has no positive counterpart. Nothing had noticed, because nothing had been asked what absolute promises.
One prover gap written down where it bit: the door is written with <= rather than ==, because a comparison narrows a range and a disequality does not.
Also measured: of the 29 calls to at, 12 pay for a failure and exactly one is a bound the checker could discharge today. The rest index a list that came back from a call. That moves the open question about a total indexing form.