diff --git a/CHANGELOG.md b/CHANGELOG.md index 65da73b..bca8b36 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -20,6 +20,26 @@ release notes. ### Diagnostics +- An obligation nobody could ever prove no longer reads like one nobody has got + round to. Every `ensures` clause that came back `Guarded` said "nothing tries + to prove this one ahead of time"; seven of the nine in `examples/` are about + an effect, and those are not waiting on anything: + + ```deed + fn peek() -> Int uses Counter.value, ensures ok => unchanged(Counter), { .. } + ``` + + A function is checked once. The `with` block deciding what `Counter` means is + written by whoever calls it, and a different caller may install a different + handler, so no pass on this side settles that clause however hard it tries. + Those now say the caller installs the handler that answers it, which is 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. Splitting the count is what makes the difference visible: + `design/02-syntax.md` now reports both rows separately. + - A refinement written on a record's field survives reading the field back. A parameter of type `Positive` was already known to be positive; a field declared `Positive` was not, and the two say the same thing: diff --git a/crates/deed-ast/src/lib.rs b/crates/deed-ast/src/lib.rs index 95fba41..b0f854f 100644 --- a/crates/deed-ast/src/lib.rs +++ b/crates/deed-ast/src/lib.rs @@ -799,6 +799,94 @@ impl Expr { } } +/// Every expression one step inside `expr`. +/// +/// Here rather than in a pass, because which expressions are inside another +/// one is a fact about the tree and every reader of it wants the same answer. +/// The interpreter used to keep this and had written it out twice before that; +/// both copies stopped in the same place, a closure body, and `DEED6006`'s own +/// note describes the hole that left. +/// +/// Matched without a wildcard, so a new kind of expression is a build error +/// here rather than a walk that silently stops covering it. +pub fn children<'a>(expr: &'a Expr, out: &mut Vec<&'a Expr>) { + match expr { + Expr::Field { receiver, .. } => out.push(receiver), + Expr::Call { callee, args, .. } => { + out.push(callee); + out.extend(args); + } + Expr::List { elements, .. } => out.extend(elements), + Expr::StructLit { path, fields, .. } => { + out.push(path); + out.extend(fields.iter().filter_map(|field| field.value.as_ref())); + } + Expr::Unary { operand, .. } | Expr::Try { operand, .. } => out.push(operand), + Expr::Binary { lhs, rhs, .. } => { + out.push(lhs); + out.push(rhs); + } + Expr::If { + condition, + then_branch, + else_branch, + .. + } => { + out.push(condition); + block_children(then_branch, out); + out.extend(else_branch.as_deref()); + } + Expr::Match { + scrutinee, arms, .. + } => { + out.push(scrutinee); + out.extend(arms.iter().map(|arm| &arm.body)); + } + Expr::For { + iterable, + accumulator, + keep, + body, + .. + } => { + out.push(iterable); + out.extend(accumulator.iter().map(|acc| acc.init.as_ref())); + out.extend(keep.as_deref()); + block_children(body, out); + } + Expr::Block(block) => block_children(block, out), + Expr::Closure { body, .. } => out.push(body), + Expr::Old { expr, .. } => out.push(expr), + Expr::With { handlers, body, .. } => { + out.extend(handlers); + block_children(body, out); + } + Expr::Int { .. } + | Expr::Str { .. } + | Expr::Bool { .. } + | Expr::Unit(_) + | Expr::Ident(_) + | Expr::Unchanged { .. } + | Expr::Error(_) => {} + } +} + +/// Every expression one step inside a block. +pub fn block_children<'a>(block: &'a Block, out: &mut Vec<&'a Expr>) { + for stmt in &block.stmts { + match stmt { + Stmt::Let { init, .. } => out.push(init), + Stmt::Assign { value, .. } => out.push(value), + Stmt::Return { value, .. } => out.extend(value), + Stmt::Assert { condition, .. } => out.push(condition), + Stmt::Refuses { subject, .. } => out.push(subject), + Stmt::Expr(expr) => out.push(expr), + Stmt::Abandon { .. } => {} + } + } + out.extend(block.tail.as_deref()); +} + #[derive(Clone, Debug)] pub struct PatternField { pub name: Ident, diff --git a/crates/deed-driver/src/lib.rs b/crates/deed-driver/src/lib.rs index 3504618..f9c96e2 100644 --- a/crates/deed-driver/src/lib.rs +++ b/crates/deed-driver/src/lib.rs @@ -110,13 +110,13 @@ mod clock_tests { } } -use deed_ast::{Item, Module, Outcome}; +use deed_ast::{Expr, Item, Module, Outcome, children}; use deed_diagnostics::{Diagnostic, FileId, Severity, SourceMap, Span}; use deed_effects::Effects; use deed_interp::{DeclaredRows, Guard, Guards, OperatorCalls, Program, RowItem}; use deed_lexer::tokenize; use deed_parser::parse; -use deed_resolve::{Resolutions, Universe}; +use deed_resolve::{DefKind, Resolutions, Universe}; use deed_typeck::{Reason, Tier, Types, World}; /// One obligation and how it was discharged. @@ -565,12 +565,13 @@ fn check_parsed( // can be generated gets exercised by a property test as well, which is the // `Tested` tier and the only place it comes from. // - // A guarded one carries `NothingTriesToProveThis` rather than no reason at - // all. The distinction matters more here than anywhere else: the other - // guarded obligations are the checker having looked and failed, and these - // are the checker never having looked, and until this said so the two were - // the same word with nothing to tell them apart. Thirteen of the sixteen - // guarded obligations in `examples/` are this case. + // A guarded one says why it is guarded, and there are two answers. Most of + // these clauses are about an effect, and the `with` block that decides + // what the effect means belongs to whoever calls the function: nothing + // here can settle those, ever. The rest are simply not attempted, which is + // the checker never having looked rather than having looked and failed. + // Until these two were told apart, an obligation nobody could ever prove + // read the same as one nobody had got round to. for item in &parsed_module.items { let Item::Function(function) = item else { continue; @@ -592,7 +593,12 @@ fn check_parsed( // answer rather than the absence of one. reason: match tested { true => None, - false => Some(deed_typeck::facts::Reason::NothingTriesToProveThis), + false => Some( + match reaches_an_effect(&obligation.condition, &resolved.resolutions) { + true => Reason::TheCallerInstallsTheHandler, + false => Reason::NothingTriesToProveThis, + }, + ), }, }); } @@ -612,6 +618,41 @@ fn check_parsed( } } +/// Whether a contract clause talks about an effect. +/// +/// Two shapes reach one: `unchanged(Ledger)`, which names an effect and +/// nothing else, and any mention of an operation, whether it is performed +/// directly or read through `old(...)`. Both mean the same thing for the +/// tier, and it is a fact about the caller rather than about this function: +/// the body is checked once, and which handler answers is decided by whoever +/// wrote the `with` block above the call. +/// +/// Asked of the resolver rather than of the text, so an effect called +/// `unchanged` or a local called `Ledger` cannot fool it. +/// +/// A bare name is not asked, because an operation is declared as a member of +/// its effect and there is no scope a bare name could find one in: every +/// mention of one is `Effect.operation`, whether it is being called or handed +/// on as a value. Asking anyway was a branch no program could reach. +fn reaches_an_effect(expr: &Expr, resolutions: &Resolutions) -> bool { + if let Expr::Unchanged { .. } = expr { + return true; + } + let operation = match expr { + Expr::Field { name, .. } => resolutions.resolution(name.span), + _ => None, + } + .is_some_and(|def| resolutions.def(def).kind == DefKind::EffectOp); + if operation { + return true; + } + let mut inside = Vec::new(); + children(expr, &mut inside); + inside + .into_iter() + .any(|child| reaches_an_effect(child, resolutions)) +} + /// Convenience for callers holding text rather than a populated map. pub fn check_text( sources: &mut SourceMap, diff --git a/crates/deed-driver/tests/obligations.rs b/crates/deed-driver/tests/obligations.rs index 38aac21..597aee8 100644 --- a/crates/deed-driver/tests/obligations.rs +++ b/crates/deed-driver/tests/obligations.rs @@ -13,12 +13,20 @@ //! the checker never having looked. A reader could not tell "I could not prove //! this" from "nobody tried", which is the distinction the whole tier exists to //! draw. +//! +//! One reason for all of them was still one reason too few. Most of these +//! clauses are about an effect, and no pass here will ever settle one of those: +//! the function is checked once, and the `with` block deciding what the effect +//! means is written by whoever calls it. "Nobody tried" reads as a job somebody +//! could finish, so those now say the caller installs the handler instead. use std::fs; use std::path::PathBuf; +use deed_ast::{Expr, Item, block_children, children}; use deed_diagnostics::SourceMap; use deed_driver::{Checked, check_all, shipped_modules, shipped_source}; +use deed_resolve::DefKind; use deed_typeck::Tier; use deed_typeck::facts::Reason; @@ -167,6 +175,7 @@ fn every_reason_reads_as_advice() { Reason::CrossedAModuleBoundary, Reason::NotAShapeTheCheckerReasonsAbout, Reason::NothingTriesToProveThis, + Reason::TheCallerInstallsTheHandler, ] { let text = reason.text(); assert!(text.len() > 20, "{reason:?} says almost nothing: {text:?}"); @@ -184,17 +193,16 @@ fn every_reason_reads_as_advice() { /// The measurement that made this worth doing, kept so it stays true. /// /// An `ensures` clause is checked on every call and nothing settles one ahead -/// of time, so it is the floor of what lands in `Guarded`. It used to be the -/// majority as well, and stopped being one when `std/ratio` grew preconditions -/// that its own arithmetic cannot discharge. What the paragraph this file -/// opens with rests on is that no `ensures` clause is ever settled early, not -/// that they outnumber everything else, so that is what this holds: every -/// unattempted obligation is one, and there are some. +/// of time, so it is the floor of what lands in `Guarded`. Both reasons that +/// belong to one say so in different words, and no other kind of obligation is +/// allowed to borrow either: a `where` clause or a refinement that came back +/// with one of these would mean the reason had stopped being about contracts. #[test] -fn an_ensures_clause_is_the_common_reason_the_corpus_is_guarded() { +fn only_an_ensures_clause_gives_a_reason_about_a_contract() { let checks = everything(); - let mut unproven = 0; + let mut unattempted = 0; + let mut the_callers = 0; let mut total = 0; for checked in &checks { for obligation in &checked.obligations { @@ -202,20 +210,194 @@ fn an_ensures_clause_is_the_common_reason_the_corpus_is_guarded() { continue; } total += 1; - if obligation.reason == Some(Reason::NothingTriesToProveThis) { - unproven += 1; - assert!( - obligation.subject.contains(" ensures "), - "`{}` says nothing tries to prove it, but it is not an `ensures` clause", - obligation.subject - ); - } + let contract = match obligation.reason { + Some(Reason::NothingTriesToProveThis) => { + unattempted += 1; + true + } + Some(Reason::TheCallerInstallsTheHandler) => { + the_callers += 1; + true + } + _ => false, + }; + assert!( + !contract || obligation.subject.contains(" ensures "), + "`{}` gives a reason only an `ensures` clause should give", + obligation.subject + ); } } assert!( - unproven > 0 && total > unproven, - "{unproven} of {total} guarded obligations are unattempted `ensures` clauses, \ + unattempted > 0 && the_callers > 0 && total > unattempted + the_callers, + "{unattempted} unattempted and {the_callers} the caller's, of {total} guarded, \ which is not the shape this file was written about" ); } + +/// The split, asked of a program small enough to read. +/// +/// Both directions, because a rule that only ever says yes would satisfy the +/// counts above just as well as one that reads the clause. The two functions +/// differ in one thing: whether the postcondition mentions the effect. +#[test] +fn a_clause_about_an_effect_says_the_caller_answers_it_and_one_that_is_not_does_not() { + let source = "module scratch/handlers + +effect Counter { + fn value() -> Int +} + +fn watched(by: Int) -> Int + uses + Counter.value, + ensures + ok => Counter.value() >= by, +{ + Counter.value() + by +} + +fn plain(by: Int) -> Int + uses + Counter.value, + ensures + ok => result >= by, +{ + Counter.value() + by +} +"; + + let mut sources = SourceMap::new(); + let checked = deed_driver::check_text(&mut sources, "scratch/handlers.deed", source); + assert!(!checked.has_errors(), "the fixture should check cleanly"); + + let reason_for = |name: &str| { + checked + .obligations + .iter() + .find(|obligation| obligation.subject == format!("{name} ensures ok")) + .unwrap_or_else(|| panic!("`{name}` should carry one obligation")) + .reason + }; + + assert_eq!( + reason_for("watched"), + Some(Reason::TheCallerInstallsTheHandler), + "a clause performing an operation is one only the caller's handler can answer" + ); + assert_eq!( + reason_for("plain"), + Some(Reason::NothingTriesToProveThis), + "a clause about the returned value is one nothing here tried" + ); +} + +/// `unchanged(E)` reaches the same answer by naming the effect alone. +/// +/// It is the shape that is hardest to read off the text, since it performs no +/// operation and mentions no dot. Held separately so that removing the arm +/// that recognises it fails with a name rather than with a count. +#[test] +fn an_unchanged_clause_is_the_callers_to_answer_as_well() { + let source = "module scratch/still + +effect Counter { + fn value() -> Int +} + +fn peek() -> Int + uses + Counter.value, + ensures + ok => unchanged(Counter), +{ + Counter.value() +} +"; + + let mut sources = SourceMap::new(); + let checked = deed_driver::check_text(&mut sources, "scratch/still.deed", source); + assert!(!checked.has_errors(), "the fixture should check cleanly"); + + let obligation = checked + .obligations + .iter() + .find(|obligation| obligation.subject == "peek ensures ok") + .expect("`peek` should carry one obligation"); + assert_eq!( + obligation.reason, + Some(Reason::TheCallerInstallsTheHandler), + "`unchanged` names an effect, and the handler behind it belongs to the caller" + ); +} + +/// The assumption the rule above rests on, measured rather than assumed. +/// +/// An effect operation is declared as a member of its effect, so there is no +/// scope a bare name in an expression could find one in and every mention is +/// `Effect.operation`. `reaches_an_effect` asks about a field name and nothing +/// else because of that; the first version asked about bare names too, and no +/// program in this repository could reach the branch. If the resolver ever +/// starts putting an operation somewhere a bare name can see it, that branch +/// has to come back, and this is what says so. +/// +/// About expressions, not about every mention: `fn note(message: String)` in +/// an effect and in the handler implementing it are both bare, and both are +/// declarations rather than uses. +#[test] +fn an_effect_operation_is_only_ever_named_through_its_effect() { + let checks = everything(); + + let mut through_an_effect = 0; + for checked in &checks { + let mut queue: Vec<&Expr> = Vec::new(); + for item in &checked.module.items { + match item { + Item::Function(function) => { + queue.extend(&function.contract.requires); + queue.extend(function.contract.ensures.iter().map(|e| &e.condition)); + block_children(&function.body, &mut queue); + } + Item::Handler(handler) => { + for operation in &handler.operations { + block_children(&operation.body, &mut queue); + } + if let Some(finally) = &handler.finally { + block_children(finally, &mut queue); + } + } + Item::Test(test) => block_children(&test.body, &mut queue), + _ => {} + } + } + + while let Some(expr) = queue.pop() { + let bare = match expr { + Expr::Ident(ident) => checked.resolutions.resolution(ident.span), + Expr::Field { name, .. } => { + if checked + .resolutions + .resolution(name.span) + .is_some_and(|def| checked.resolutions.def(def).kind == DefKind::EffectOp) + { + through_an_effect += 1; + } + None + } + _ => None, + }; + assert!( + !bare.is_some_and(|def| checked.resolutions.def(def).kind == DefKind::EffectOp), + "an operation is named by itself in an expression, so the bare-name branch \ + `reaches_an_effect` dropped has to come back" + ); + children(expr, &mut queue); + } + } + + assert!( + through_an_effect > 0, + "no expression anywhere names an operation, so this holds nothing" + ); +} diff --git a/crates/deed-driver/tests/reasons.rs b/crates/deed-driver/tests/reasons.rs index a99619c..9c80b6d 100644 --- a/crates/deed-driver/tests/reasons.rs +++ b/crates/deed-driver/tests/reasons.rs @@ -123,6 +123,10 @@ fn the_corpus_is_counted_by_tier_and_by_reason() { .iter() .filter(|o| o.reason.map(reason_text) == Some(Reason::NothingTriesToProveThis.text())) .count(); + let the_caller_installs = guarded + .iter() + .filter(|o| o.reason.map(reason_text) == Some(Reason::TheCallerInstallsTheHandler.text())) + .count(); let no_reason_at_all = guarded.iter().filter(|o| o.reason.is_none()).count(); // Every Guarded obligation is accounted for by exactly one of the buckets @@ -133,8 +137,9 @@ fn the_corpus_is_counted_by_tier_and_by_reason() { // holds it there. It used to be nine, all of them `ensures` clauses, which // `check_all` never routes through `facts::holds`: nothing tries to settle // one ahead of time, so the floor is Guarded whatever the body looks like. - // Saying nothing made that look like the same answer as "I looked and could - // not", so those nine now carry `NothingTriesToProveThis` instead. + // Those nine have since split in two, and the split is the interesting + // number: seven of them are about an effect, so no pass here could ever + // settle them, and only two are waiting on a checker that has not looked. assert_eq!( name_not_narrowed + length_not_established @@ -142,6 +147,7 @@ fn the_corpus_is_counted_by_tier_and_by_reason() { + crossed_a_boundary + not_a_shape + nothing_tries + + the_caller_installs + no_reason_at_all, guarded.len(), "every Guarded obligation should fall into exactly one reason bucket, including \"none\"" @@ -157,9 +163,10 @@ fn the_corpus_is_counted_by_tier_and_by_reason() { crossed_a_boundary, not_a_shape, nothing_tries, + the_caller_installs, no_reason_at_all, ), - (167, 11, 13, 1, 0, 0, 0, 9, 0), + (167, 11, 13, 1, 0, 0, 0, 2, 7, 0), "the corpus's obligation counts changed; update this test and the table in \ design/02-syntax.md together" ); diff --git a/crates/deed-interp/src/interp.rs b/crates/deed-interp/src/interp.rs index 689b62d..4c27d49 100644 --- a/crates/deed-interp/src/interp.rs +++ b/crates/deed-interp/src/interp.rs @@ -28,7 +28,7 @@ use std::time::{Duration, Instant}; use deed_ast::{ BinaryOp, Block, Ensures, Expr, FieldInit, FnDecl, HandlerDecl, Ident, Item, Module, Outcome, - Param, Pattern, Stmt, UnaryOp, + Param, Pattern, Stmt, UnaryOp, children, }; use deed_diagnostics::{ByNumber, Diagnostic, FileId, Span}; use deed_resolve::{DefId, DefKind, ExportKind, Resolutions}; @@ -3638,93 +3638,6 @@ fn split(text: &str, separator: &str) -> Vec { text.split(separator).map(Value::str).collect() } -/// Every expression one step inside `expr`. -/// -/// The two walkers below are the only readers, and both used to spell this out -/// for themselves. Both stopped in the same place: a closure body. `deed check` -/// accepts `result` and `old(..)` inside one, and the interpreter then had -/// nothing to bind them to, which is the hole `DEED6006`'s own note describes. -/// -/// Matched without a wildcard, so a new kind of expression is a build error -/// here rather than a contract that silently stops being checked. -fn children<'a>(expr: &'a Expr, out: &mut Vec<&'a Expr>) { - match expr { - Expr::Field { receiver, .. } => out.push(receiver), - Expr::Call { callee, args, .. } => { - out.push(callee); - out.extend(args); - } - Expr::List { elements, .. } => out.extend(elements), - Expr::StructLit { path, fields, .. } => { - out.push(path); - out.extend(fields.iter().filter_map(|field| field.value.as_ref())); - } - Expr::Unary { operand, .. } | Expr::Try { operand, .. } => out.push(operand), - Expr::Binary { lhs, rhs, .. } => { - out.push(lhs); - out.push(rhs); - } - Expr::If { - condition, - then_branch, - else_branch, - .. - } => { - out.push(condition); - block_children(then_branch, out); - out.extend(else_branch.as_deref()); - } - Expr::Match { - scrutinee, arms, .. - } => { - out.push(scrutinee); - out.extend(arms.iter().map(|arm| &arm.body)); - } - Expr::For { - iterable, - accumulator, - keep, - body, - .. - } => { - out.push(iterable); - out.extend(accumulator.iter().map(|acc| acc.init.as_ref())); - out.extend(keep.as_deref()); - block_children(body, out); - } - Expr::Block(block) => block_children(block, out), - Expr::Closure { body, .. } => out.push(body), - Expr::Old { expr, .. } => out.push(expr), - Expr::With { handlers, body, .. } => { - out.extend(handlers); - block_children(body, out); - } - Expr::Int { .. } - | Expr::Str { .. } - | Expr::Bool { .. } - | Expr::Unit(_) - | Expr::Ident(_) - | Expr::Unchanged { .. } - | Expr::Error(_) => {} - } -} - -/// Every expression one step inside a block. -fn block_children<'a>(block: &'a Block, out: &mut Vec<&'a Expr>) { - for stmt in &block.stmts { - match stmt { - Stmt::Let { init, .. } => out.push(init), - Stmt::Assign { value, .. } => out.push(value), - Stmt::Return { value, .. } => out.extend(value), - Stmt::Assert { condition, .. } => out.push(condition), - Stmt::Refuses { subject, .. } => out.push(subject), - Stmt::Expr(expr) => out.push(expr), - Stmt::Abandon { .. } => {} - } - } - out.extend(block.tail.as_deref()); -} - /// The definition `result` refers to inside an obligation, if it is used. fn result_def(expr: &Expr, resolutions: &Resolutions) -> Option { if let Expr::Ident(ident) = expr diff --git a/crates/deed-typeck/src/facts.rs b/crates/deed-typeck/src/facts.rs index 28002d9..1850b09 100644 --- a/crates/deed-typeck/src/facts.rs +++ b/crates/deed-typeck/src/facts.rs @@ -254,7 +254,8 @@ pub enum Truth { /// meant to. Each one is the answer to "what would make this Proven instead": /// narrow the name, establish the length, give the value a name, keep the /// clause on this side of a module boundary, or write the condition in a -/// shape this checker reasons about at all. +/// shape this checker reasons about at all. One of them answers "nothing", +/// and saying so is the point of it. #[derive(Clone, Copy, PartialEq, Eq, Debug)] pub enum Reason { /// A name is being compared, but nothing in scope narrowed its range @@ -281,6 +282,16 @@ pub enum Reason { /// its floor is `Guarded` whatever the body looks like, and no pass tries /// to settle one ahead of time. NothingTriesToProveThis, + /// The clause is about an effect, and the caller picks the handler. + /// + /// The only reason here whose answer to "what would make this Proven" + /// is nothing. A function is checked once; the `with` block that decides + /// what `Counter.value()` or `unchanged(Ledger)` means is written by + /// whoever calls it, and a different caller may install a different + /// handler. Filing these under [`Reason::NothingTriesToProveThis`] said + /// the compiler had not got round to them, which invites a reader to wait + /// for a release that cannot come. + TheCallerInstallsTheHandler, } impl Reason { @@ -299,6 +310,9 @@ impl Reason { Reason::NothingTriesToProveThis => { "nothing tries to prove this one ahead of time, so it is checked on every call" } + Reason::TheCallerInstallsTheHandler => { + "this is about an effect, and the caller installs the handler that answers it" + } } } } diff --git a/design/02-syntax.md b/design/02-syntax.md index d2d9174..f33722d 100644 --- a/design/02-syntax.md +++ b/design/02-syntax.md @@ -827,10 +827,11 @@ by reason. | Guarded, nothing names this value | 0 | | Guarded, crossed a module boundary | 0 | | Guarded, not a shape the checker reasons about | 0 | -| Guarded, nothing tries to prove this one ahead of time (an `ensures` clause) | 9 | +| Guarded, nothing tries to prove this one ahead of time (an `ensures` clause) | 2 | +| Guarded, this is about an effect and the caller installs the handler | 7 | | Guarded, no reason at all | 0 | -The last two rows used to be one row saying nothing. Nine of the twenty-three `Guarded` +The last three rows used to be one row saying nothing. Nine of the twenty-three `Guarded` obligations are `ensures` clauses, which `check_all` never routes through `facts::holds`: nothing tries to settle one ahead of time, so the floor is `Guarded` whatever the body looks like. Reporting that as an absent reason made it read as the same answer the other three @@ -839,17 +840,26 @@ deciding whether they have a bug needs "nobody tried" and "I could not" to be di sentences. `crates/deed-driver/tests/obligations.rs` now refuses any `Guarded` obligation that carries no reason at all. +Counting those nine split them again, and the split is the number worth having. Seven of them +are about an effect: `unchanged(Ledger)`, or a postcondition reading `Counter.value()`. A +function is checked once and the `with` block that decides what the effect means belongs to +whoever calls it, so a different caller can install a different handler and no pass on this +side could settle these however hard it tried. Telling a reader "nobody tried" invites them to +wait for a release that cannot come. Only the remaining two — `transfer`'s `result.from == +from` and `result.amount == amount` — are obligations a checker could one day discharge, and +those are what a future move here would be measured against. + The thirteen in the first `Guarded` row are almost all one thing: `std/ratio` writes preconditions saying its numbers are not the smallest `Int`, and the calls that cannot discharge them are the ones whose arguments are arithmetic. That is the honest answer for them, since `left.top * right.bottom` really can be anything. **What this decides.** Zero of the corpus's `Guarded` obligations are "not a shape the -checker reasons about", and zero crossed a module boundary. The two that are categorised at -all are both "nothing narrowed this name": a name the body never bothered to narrow, not a -predicate the interval machinery is structurally unable to read. That is documentation and -message work, not evidence for a solver, so the question in the next section is answered -against a count rather than an impression. +checker reasons about", and zero crossed a module boundary. Every one the checker actually +attempted came back "nothing narrowed this name" or "nothing established this length": a name +the body never bothered to narrow, not a predicate the interval machinery is structurally +unable to read. That is documentation and message work, not evidence for a solver, so the +question in the next section is answered against a count rather than an impression. ### Whether this checker ever calls a solver