From 8589f15eda68c2779a9dca33359cb4b2c791d2ee Mon Sep 17 00:00:00 2001 From: onatozmenn Date: Mon, 10 Aug 2026 21:42:47 +0300 Subject: [PATCH 1/2] The obligation the caller owns 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. --- CHANGELOG.md | 20 ++++ crates/deed-ast/src/lib.rs | 88 ++++++++++++++ crates/deed-driver/src/lib.rs | 57 +++++++-- crates/deed-driver/tests/obligations.rs | 146 +++++++++++++++++++++--- crates/deed-driver/tests/reasons.rs | 13 ++- crates/deed-interp/src/interp.rs | 89 +-------------- crates/deed-typeck/src/facts.rs | 16 ++- design/02-syntax.md | 24 ++-- 8 files changed, 327 insertions(+), 126 deletions(-) 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..269f608 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,39 @@ 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. +fn reaches_an_effect(expr: &Expr, resolutions: &Resolutions) -> bool { + if let Expr::Unchanged { .. } = expr { + return true; + } + let named = match expr { + Expr::Ident(ident) => Some(ident.span), + Expr::Field { name, .. } => Some(name.span), + _ => None, + }; + let operation = named + .and_then(|span| resolutions.resolution(span)) + .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..9617683 100644 --- a/crates/deed-driver/tests/obligations.rs +++ b/crates/deed-driver/tests/obligations.rs @@ -13,6 +13,12 @@ //! 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; @@ -167,6 +173,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 +191,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 +208,124 @@ 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" + ); +} 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 From 25d5e6cd219f7c60db105dff6ca410fc2b6b2cfd Mon Sep 17 00:00:00 2001 From: onatozmenn Date: Mon, 10 Aug 2026 21:50:57 +0300 Subject: [PATCH 2/2] A bare name cannot be an operation `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. --- crates/deed-driver/src/lib.rs | 16 +++--- crates/deed-driver/tests/obligations.rs | 72 +++++++++++++++++++++++++ 2 files changed, 81 insertions(+), 7 deletions(-) diff --git a/crates/deed-driver/src/lib.rs b/crates/deed-driver/src/lib.rs index 269f608..f9c96e2 100644 --- a/crates/deed-driver/src/lib.rs +++ b/crates/deed-driver/src/lib.rs @@ -629,18 +629,20 @@ fn check_parsed( /// /// 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 named = match expr { - Expr::Ident(ident) => Some(ident.span), - Expr::Field { name, .. } => Some(name.span), + let operation = match expr { + Expr::Field { name, .. } => resolutions.resolution(name.span), _ => None, - }; - let operation = named - .and_then(|span| resolutions.resolution(span)) - .is_some_and(|def| resolutions.def(def).kind == DefKind::EffectOp); + } + .is_some_and(|def| resolutions.def(def).kind == DefKind::EffectOp); if operation { return true; } diff --git a/crates/deed-driver/tests/obligations.rs b/crates/deed-driver/tests/obligations.rs index 9617683..597aee8 100644 --- a/crates/deed-driver/tests/obligations.rs +++ b/crates/deed-driver/tests/obligations.rs @@ -23,8 +23,10 @@ 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; @@ -329,3 +331,73 @@ fn peek() -> Int "`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" + ); +}