The obligation the caller owns - #970
Merged
Merged
Conversation
Every `ensures` clause that came back Guarded said the same thing: "nothing tries to prove this one ahead of time, so it is checked on every call". Counted across `examples/` and `std/`, nine obligations said it, and seven of them are about an effect. Those seven are not waiting on anything. A function is checked once, and the `with` block that decides what `Counter.value()` or `unchanged(Ledger)` means belongs to whoever calls it; a different caller may install a different handler. No pass on this side settles one of those however hard it tries. Saying "nobody tried" invites a reader to wait for a release that cannot come, which is the same failure the reason field was added to fix, one level in. They now carry `Reason::TheCallerInstallsTheHandler`, the one reason here whose answer to "what would make this Proven" is nothing. The two left saying "nothing tries" are `transfer`'s `result.from == from` and `result.amount == amount`, which really are obligations a checker could one day discharge, so the split turns a single number into the one that says where the remaining work is. Asked of the resolver rather than of the text, so an effect called `unchanged` or a local called `Ledger` cannot fool it. `children`, "every expression one step inside this one", moves from the interpreter to `deed-ast`. Which expressions are inside another is a fact about the tree, and this is the second reader; the interpreter had already written it out twice before that and both copies stopped in the same place. Three break-verifications, each failing by name: dropping the `unchanged` arm, dropping the operation arm, and answering yes to everything. `design/02-syntax.md` reports both rows, and `reasons.rs` pins them.
`mutants on the diff` kept the branch asking whether a bare identifier resolves to an effect operation, and it was right to: no program can reach it. An operation is declared as a member of its effect, so nothing puts one in a scope a bare name could find, and every mention in an expression is `Effect.operation`, whether it is being called or handed on as a value. The branch is gone and the assumption behind removing it is now measured rather than asserted. `an_effect_operation_is_only_ever_named_through_its_effect` walks every expression in `examples/` and `std/` and requires that no bare name resolves to one, and that some field name does, so it is not passing on an empty set. Asked of the tree rather than of `Resolutions::names`, because an effect's own `fn note(..)` and the handler's are both bare and both are declarations.
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.
Every
ensuresclause that came backGuardedgave the same reason: "nothing tries to prove this one ahead of time, so it is checked on every call". Nine obligations acrossexamples/andstd/said it. Seven of them are about an effect, and those are not waiting on anything.A function is checked once. The
withblock that decides whatCounter.value()orunchanged(Ledger)means belongs to whoever calls it, and a different caller may install a different handler, so no pass on this side settles one of those however hard it tries. "Nobody tried" reads as a job somebody could finish; it invites a reader to wait for a release that cannot come, which is the same failure the reason field was added to fix, one level in.Those seven now carry
Reason::TheCallerInstallsTheHandler— the one reason here whose answer to "what would make this Proven" is nothing, and the doc comment onReasonnow says so.What the split says
The two left are
transfer'sresult.from == fromandresult.amount == amount. Those really are obligations a checker could one day discharge, so the split turns one number into the one that says where the remaining work is.How it decides
Asked of the resolver, not of the text: a clause reaches an effect if it is
unchanged(E), or if any name in it resolves to an effect operation. An effect calledunchangedor a local calledLedgercannot fool it.children— "every expression one step inside this one" — moves from the interpreter todeed-ast. Which expressions are inside another is a fact about the tree, and this is its second reader; the interpreter had written it out twice before it was factored out once, and both copies had stopped in the same place.Held by
obligations.rs: the split asked of a two-function program, both directions, plusunchangedon its own so that removing the arm recognising it fails with a name rather than with a count. Neither reason may be given by anything that is not anensuresclause.reasons.rs: the corpus counts, pinned alongside the table indesign/02-syntax.md.Three break-verifications, each failing by name: dropping the
unchangedarm, dropping the operation arm, and answering yes to everything.Not in this PR
Proving the remaining two.
result.from == fromneeds the checker to know that the returned record literal put the parameter in that field, which is a mechanism rather than a message, and it is what a next move here would be measured against.