From d4b527e61e5b301b91f56bd9d5af30a026c235a1 Mon Sep 17 00:00:00 2001 From: onatozmenn Date: Sun, 9 Aug 2026 22:48:48 +0300 Subject: [PATCH] A field keeps what its type said A parameter of type `Positive` was already known to be positive. A field declared `Positive` was not, and the two say the same thing. record Held { by: Positive } fn needs(n: Positive) -> Int where n > 0, { n } fn through(h: Held) -> Int { needs(h.by) } // was Guarded, is Proven The value has no name at that call for anything to have narrowed, and no contract answered for it, so the only thing that knew anything was the type the record was declared with. Nothing asked it. The comment in `facts.rs` said so in as many words: "every other field read is a value nothing here knows". `Env` can ask now. The checker answers out of its type table, because the fact machinery has none, and `Range::ANY` when the type says nothing. Measured before writing any of it, three ways, to find where a refinement stops travelling rather than guessing: needs(b) where b: Positive proven needs(h.by) where by: Positive guarded <- this needs(b) where b: NonZero guarded <- something else The third is a different limit and is left alone: `value != 0` admits everything but one number, which is two intervals and not one, so `Facts` cannot hold it. That is what still stops `std/ratio` from proving `simplified`'s `bottom != 0` at its call sites, along with the product of two numbers, which no interval bounds. No obligation in the corpus moves, and the changelog says so: the records there are declared with plain `Int`. What moved is that the compiler stopped losing something it already had. Break-verified. The first attempt reported both cases survived and was wrong both times -- the script never applied the edit -- so it checks that the text changed and that the run produced a result before reading it. Then: taking the question away is caught by name. The second case really did survive, and it was a redundant guard rather than a missing test: a type that is not refined already answers `Range::ANY`, so asking twice bought nothing. The guard and the `Option` around it are gone. --- CHANGELOG.md | 28 ++++++++++++++++ crates/deed-driver/tests/proving.rs | 50 +++++++++++++++++++++++++++++ crates/deed-typeck/src/check.rs | 43 +++++++++++++++++++++++++ crates/deed-typeck/src/facts.rs | 20 ++++++++++-- 4 files changed, 138 insertions(+), 3 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index c62730c..65da73b 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -20,6 +20,34 @@ release notes. ### Diagnostics +- 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: + + ```deed + record Held { by: Positive } + + fn needs(n: Positive) -> Int where n > 0, { n } + + fn through(h: Held) -> Int { needs(h.by) } // was Guarded, is Proven + ``` + + The value has no name at that call for anything to have narrowed, and no + contract answered for it, so the only thing that knew anything was the type + the record was declared with — and nothing asked it. The comment in + `facts.rs` said so: "every other field read is a value nothing here knows". + + It knows now, and only that. A field declared plainly is still a value + nothing knows, and a refinement the interval machinery cannot hold still + carries nothing either way: `value != 0` admits everything but one number, + which is two intervals and not one. That is a limit of what `Facts` keeps + rather than of fields, and it is the half that still stops `std/ratio` from + proving `simplified`'s `bottom != 0` at its call sites — along with the + product of two numbers, which no interval bounds. + + No obligation in the corpus moves: the records there are declared with plain + `Int`. What moved is that the compiler stopped losing something it had. + - `deed explain` showed programs that do not produce the code being explained. Forty-three of the eighty-nine pages carrying an example, measured by checking each one and running its tests. The example was "the first diff --git a/crates/deed-driver/tests/proving.rs b/crates/deed-driver/tests/proving.rs index 584a9c2..1b9dfd0 100644 --- a/crates/deed-driver/tests/proving.rs +++ b/crates/deed-driver/tests/proving.rs @@ -1480,3 +1480,53 @@ fn a_value_nothing_is_known_about_gets_no_invented_number() { ); assert!(!text.contains("when this is"), "{text}"); } +/// A refinement written on a record's field survives reading the field back. +/// +/// A parameter of type `Positive` is already known to be positive; a field +/// declared `Positive` was not, and the two say the same thing. The value has +/// no name here for anything to have narrowed, so the only thing that knows +/// is the type the record was declared with, and until this the only place +/// that survived was the literal that built it. +#[test] +fn a_field_declared_with_a_refinement_carries_it_when_it_is_read() { + expect_each( + &[("needs requires", Tier::Proven)], + "\ + record Held { by: Positive }\n\n\ + fn needs(n: Positive) -> Int\n where\n n > 0,\n{\n n\n}\n\n\ + fn through(h: Held) -> Int { needs(h.by) }\n", + ); +} + +/// And a plain field still knows nothing, so this is the type talking rather +/// than field reads having quietly become trustworthy. +#[test] +fn a_field_declared_without_one_is_still_a_value_nothing_knows() { + expect_each( + &[ + ("needs requires", Tier::Guarded), + ("Positive", Tier::Guarded), + ], + "\ + record Held { by: Int }\n\n\ + fn needs(n: Positive) -> Int\n where\n n > 0,\n{\n n\n}\n\n\ + fn through(h: Held) -> Int { needs(h.by) }\n", + ); +} + +/// A refinement the interval machinery cannot hold is still not held. +/// +/// `value != 0` admits everything but one number, which is two intervals and +/// not one, so a field declared with it carries nothing. The type is not the +/// limit here and neither is the field: it is that `Facts` keeps ranges. +#[test] +fn a_refinement_that_is_not_an_interval_carries_nothing_either_way() { + expect_each( + &[("needs requires", Tier::Guarded)], + "\ + type NonZero = Int where value != 0\n\n\ + record Held { by: NonZero }\n\n\ + fn needs(n: NonZero) -> Int\n where\n n != 0,\n{\n n\n}\n\n\ + fn through(h: Held) -> Int { needs(h.by) }\n", + ); +} diff --git a/crates/deed-typeck/src/check.rs b/crates/deed-typeck/src/check.rs index 6c492b0..2362ab3 100644 --- a/crates/deed-typeck/src/check.rs +++ b/crates/deed-typeck/src/check.rs @@ -1254,10 +1254,12 @@ impl<'a> Checker<'a> { match &requires.origin { Origin::Here { .. } => { let (def_of, call) = self.env(); + let refined = self.refinements(); let env = facts::Env { def_of: &def_of, length: self.resolutions.builtin("length"), call: &call, + refined: &refined, }; facts::holds(clause, facts, &env) } @@ -1270,6 +1272,9 @@ impl<'a> Checker<'a> { def_of: &def_of, length: Some(imported_name(ClauseName::Length)), call: &|_| Promise::any(), + // No type table on this side of the boundary, and the + // clause arrived without one. + refined: &|_| Range::ANY, }; let outcome = facts::holds(clause, facts, &env); facts::thinned_by_boundary(clause, &env, outcome) @@ -1305,10 +1310,12 @@ impl<'a> Checker<'a> { // brings its own size. let length = { let (def_of, call) = self.env(); + let refined = self.refinements(); let env = facts::Env { def_of: &def_of, length: self.resolutions.builtin("length"), call: &call, + refined: &refined, }; facts::length_of(arg, &self.facts, &env) }; @@ -1336,10 +1343,12 @@ impl<'a> Checker<'a> { /// What a fact could be attached to, for an expression in this body. fn term_of(&self, expr: &Expr) -> Option { let (def_of, call) = self.env(); + let refined = self.refinements(); let env = facts::Env { def_of: &def_of, length: self.resolutions.builtin("length"), call: &call, + refined: &refined, }; facts::term_of(expr, &env) } @@ -2046,10 +2055,14 @@ impl<'a> Checker<'a> { match &alias.refinement { Some(predicate) => { let (def_of, call) = self.env(); + // Blind about fields on purpose: a predicate is read against + // `value`, and asking what a field read in it admits would + // come straight back here for the type being read. let env = facts::Env { def_of: &def_of, length: self.resolutions.builtin("length"), call: &call, + refined: &|_| Range::ANY, }; facts::admitted_by(predicate, &env) } @@ -2130,26 +2143,48 @@ impl<'a> Checker<'a> { (self.resolver(), |callee: &Expr| self.call_promise(callee)) } + /// What a declared type admits, as the fact machinery asks it. + fn refinements(&self) -> impl Fn(&Expr) -> Range + '_ { + |expr: &Expr| self.refined_range(expr) + } + + /// What this expression's declared type admits, when that type is refined. + /// + /// The type table rather than the facts, because the value has no name + /// here for anything to have narrowed. A record declaring `bottom: + /// Positive` has said its field is positive, and until this existed the + /// only place that survived was the literal that built it. + fn refined_range(&self, expr: &Expr) -> Range { + match self.types.type_of(expr.span()) { + Some(Ty::Named { def, .. }) => self.refinement_range(*def), + _ => Range::ANY, + } + } + fn narrowed_by(&self, condition: &Expr, when_true: bool) -> Facts { self.narrowed_from(&self.facts, condition, when_true) } fn narrowed_from(&self, base: &Facts, condition: &Expr, when_true: bool) -> Facts { let (def_of, call) = self.env(); + let refined = self.refinements(); let env = facts::Env { def_of: &def_of, length: self.resolutions.builtin("length"), call: &call, + refined: &refined, }; facts::narrowed(condition, base, &env, when_true) } fn range_of(&self, expr: &Expr) -> Range { let (def_of, call) = self.env(); + let refined = self.refinements(); let env = facts::Env { def_of: &def_of, length: self.resolutions.builtin("length"), call: &call, + refined: &refined, }; facts::range_of(expr, &self.facts, &env) } @@ -2157,10 +2192,12 @@ impl<'a> Checker<'a> { /// The range the value inside the `ok` of `expr` lands in. fn ok_range_of(&self, expr: &Expr) -> Range { let (def_of, call) = self.env(); + let refined = self.refinements(); let env = facts::Env { def_of: &def_of, length: self.resolutions.builtin("length"), call: &call, + refined: &refined, }; facts::ok_range_of(expr, &self.facts, &env) } @@ -2168,10 +2205,12 @@ impl<'a> Checker<'a> { /// What is known about how long an expression is. fn length_of(&self, expr: &Expr) -> Range { let (def_of, call) = self.env(); + let refined = self.refinements(); let env = facts::Env { def_of: &def_of, length: self.resolutions.builtin("length"), call: &call, + refined: &refined, }; facts::length_of(expr, &self.facts, &env) } @@ -2179,10 +2218,12 @@ impl<'a> Checker<'a> { /// Where the arithmetic in `expr` can have no answer, if anywhere. fn overflowing(&self, expr: &Expr) -> Option { let (def_of, call) = self.env(); + let refined = self.refinements(); let env = facts::Env { def_of: &def_of, length: self.resolutions.builtin("length"), call: &call, + refined: &refined, }; facts::overflowing(expr, &self.facts, &env) } @@ -2198,10 +2239,12 @@ impl<'a> Checker<'a> { }; let with_subject = self.facts.with_subject(subject); let (def_of, call) = self.env(); + let refined = self.refinements(); let env = facts::Env { def_of: &def_of, length: self.resolutions.builtin("length"), call: &call, + refined: &refined, }; facts::holds(predicate, &with_subject, &env) } diff --git a/crates/deed-typeck/src/facts.rs b/crates/deed-typeck/src/facts.rs index 8d3b257..28002d9 100644 --- a/crates/deed-typeck/src/facts.rs +++ b/crates/deed-typeck/src/facts.rs @@ -816,6 +816,7 @@ pub fn promised_by(condition: &Expr, subject: &str, names: &[&str]) -> Guarantee def_of: &def_of, length: None, call: &|_| Promise::any(), + refined: &|_| Range::ANY, }; let mut facts = Facts::new(); @@ -953,6 +954,15 @@ pub struct Env<'a> { /// answering for contracts that are themselves checked, since a promise /// nobody keeps is not a fact. pub call: &'a dyn Fn(&Expr) -> Promise, + /// What this expression's declared type admits, when that type is refined. + /// + /// A name carries what the body worked out about it, and a call carries + /// what its contract promises. A field read has neither: nothing narrowed + /// it here and no contract answered for it, and the only thing that knows + /// anything is the type the record declared the field with. Answered by + /// whoever has the type table, since this module has none, and answered + /// with [`Range::ANY`] when the type says nothing. + pub refined: &'a dyn Fn(&Expr) -> Range, } impl Env<'_> { @@ -962,6 +972,7 @@ impl Env<'_> { def_of: &|_| None, length: None, call: &|_| Promise::any(), + refined: &|_| Range::ANY, } } } @@ -1391,11 +1402,13 @@ fn interval_of(expr: &Expr, facts: &Facts, env: &Env<'_>) -> Range { match expr { Expr::Int { value, .. } => Range::exactly(*value), // `Int.max` is the number, so a clause naming it is one the checker - // can settle rather than guard. Every other field read is a value - // nothing here knows. + // can settle rather than guard. Otherwise the only thing that knows + // anything about a field is the type it was declared with: a record + // saying `bottom: Positive` has said it, and reading the field back + // used to lose it. Expr::Field { .. } => match expr.int_limit() { Some(value) => Range::exactly(value), - None => Range::ANY, + None => (env.refined)(expr), }, Expr::Ident(_) => match term_of(expr, env) { Some(term) => facts.get(term), @@ -2235,6 +2248,7 @@ mod tests { }, length: Some(DefId::from_raw(1)), call: &|_| Promise::any(), + refined: &|_| Range::ANY, } }