diff --git a/src/verify/declaration.rs b/src/verify/declaration.rs index 44f6e19..441fd7e 100644 --- a/src/verify/declaration.rs +++ b/src/verify/declaration.rs @@ -1996,7 +1996,7 @@ fn assume_axioms(ctx: &mut VerifyContext<'_>, program: &vmir::Program) -> Result // `#ensures` occurs only inside a post, which reaches a caller through // [`post_fact`] and never through a call — so its token is released by // the export instead ([`PostRecipe::token`]). - let pre_token = Some(ctx.alloc.fn_pre_token(id, &name)); + let pre_token = ctx.alloc.fn_pre_token(id, &name); ctx.axiom_rules.push(crate::verify::rewrite::function_rule( &name, func, diff --git a/src/verify/mod.rs b/src/verify/mod.rs index cc8088b..360b4b9 100644 --- a/src/verify/mod.rs +++ b/src/verify/mod.rs @@ -70,8 +70,9 @@ pub fn verify_with_stats( // Verified function bodies, cached in dependency order (callees before // callers). Each unit's `assume_axioms` installs one lazy unfold rule per // entry here (see `rewrite::function_rule`), which installs the - // definitional equality `f(args) == body` the moment a `FuncApp(f, ..)` - // occurrence is seen during that unit's own saturation. + // definitional equality `f(args) == body` (behind the call's `f%pre(args)` + // token) once a called `FuncApp(f, ..)` occurrence is seen during that + // unit's own saturation. let mut fn_certs: crate::dhash::HashMap< vmir::MemberId, std::sync::Arc, diff --git a/src/verify/rewrite/function.rs b/src/verify/rewrite/function.rs index be4016e..16e4347 100644 --- a/src/verify/rewrite/function.rs +++ b/src/verify/rewrite/function.rs @@ -1,22 +1,24 @@ //! Function unfolding: the lazy rule that installs `f(args) == body` and replays //! a verified definition's postcondition at a call site. +use std::collections::BTreeSet; use std::sync::Arc; -use egg::{Applier, EGraph, Id, PatternAst, Rewrite, Subst, Symbol, Var}; +use egg::{Applier, EGraph, Id, PatternAst, Rewrite, SearchMatches, Searcher, Subst, Symbol, Var}; use crate::verify::analysis::ConstFold; use crate::verify::cert::FunctionDefinition; -use crate::verify::lang::{FuncId, Symbolic}; +use crate::verify::lang::{Discriminant, FuncId, Symbolic}; use crate::vmir::{Literal, Polarity, Type, Val}; use super::*; -/// Applier: for each ground `FuncApp(self.func, tys, args)` node in the matched -/// e-class, rebuild the function's **definition recipe** with `build_instance` -/// (params → args, `Generic(i)` → `tys`) and release `f(args) == body` lazily as -/// occurrences are seen during saturation — behind the call's `f%pre` token when -/// the function has one, so the equation lands only on paths that call it. +/// Applier for the **full** rule (keyed on `f`), paired with +/// [`FunctionCallSearcher`]: each match names one call `f(args)` and, when the +/// searcher found one on the clean graph, its `f%pre(args)` token. For that call +/// it rebuilds the function's **definition recipe** with `build_instance` +/// (params → args, `Generic(i)` → `tys`) and releases `f(args) == body` behind the +/// token, so the equation lands only on paths that call it. /// **Imports no e-classes** (`build_instance` only adds), so merges derived while /// verifying the body itself never ride along. It is not literally add-only: a /// body's `AxiomInst::Assume` steps and its propagated callee tokens are merged @@ -26,25 +28,135 @@ use super::*; pub(super) struct FunctionUnfoldApplier { pub(super) func: FuncId, pub(super) def: Arc, - /// `false`: the full rule (keyed on `f`) — definitional union, limited - /// framing, and the post. `true`: the limited-post rule (keyed on `f'`) — - /// the post and nothing else, no unions: unfolding a recursive body yields - /// `f'(smaller)`, and this is what delivers the postcondition there - /// (Silicon's `post` axiom triggering on the limited symbol). - pub(super) limited_post: bool, - /// Guards the (expensive) body build + post replay: done at most once per call. + /// Guards the post replay: done at most once per call. pub(super) memo: Memo, - /// Guards the definitional union separately from the build: a call first built - /// post-only (no token yet) and later reached by a propagation-minted token - /// must still union `f==body`, which `memo` alone would suppress. + /// Guards the definitional union separately from the post: a call first + /// reached without a token (post only) and later reached by a + /// propagation-minted token must still union `f==body`, which `memo` alone + /// would suppress. pub(super) union_memo: Memo, - /// The function's uniform pre-token `f%pre` (`FuncRegistry::fn_pre_token`), - /// used as a `forall`-style **presence** trigger: the definitional - /// `f(fargs)==body` union+build fires only when a `FuncApp(f%pre, fargs)` node - /// is present for the *same* `fargs`, i.e. this occurrence came from a genuine - /// value-position call. Mirrors Silicon's `f%pre ⟹ f==body`. `None` on the - /// post-only rule, where there is no definitional union to gate. - pub(super) pre_token: Option, + /// The searcher's `?tok` binding: the call's `f%pre(args)` class, bound only + /// when the token existed at search time (see [`FunctionCallSearcher`]). + pub(super) tok_var: Var, + /// The searcher's `?a0..?a{n-1}` bindings: the call's value args. + pub(super) arg_vars: Vec, +} + +/// Applier for a **post-only** rule (see [`post_rule`]): replays the +/// definition's post at each call in the matched e-class, ungated, and nothing +/// else — no body, no unions. Unfolding a recursive body yields `f'(smaller)`, +/// and this is what delivers the postcondition there (Silicon's `post` axiom +/// triggering on the limited symbol). +pub(super) struct FunctionPostApplier { + pub(super) func: FuncId, + pub(super) def: Arc, + /// Guards the post replay: done at most once per call. + pub(super) memo: Memo, +} + +/// Searcher for the full function rule: one match per distinct call `f(args)` +/// in each e-class, binding `?a0..` to the args and, when `f%pre(args)` exists, +/// `?tok` to its class. `f%pre` is the function's uniform pre-token +/// (`FuncRegistry::fn_pre_token`), a `forall`-style **presence** trigger: the +/// definitional `f(args)==body` release fires only for a genuine value-position +/// call. Mirrors Silicon's `f%pre ⟹ f==body`. +/// +/// The token is looked up **here** because the runner searches on a freshly +/// rebuilt graph, where the hashcons is exact. An applier runs after earlier +/// rules of the same iteration have merged classes without a rebuild, so a +/// `lookup` there can miss a token that exists — and a miss releases the post +/// ungated. +pub(super) struct FunctionCallSearcher { + func: FuncId, + pre_token: FuncId, + /// `?tok`, bound to the `f%pre(args)` class when one exists. + tok_var: Var, + /// `?a0..?a{n-1}`, one per param, bound to the call's args. + arg_vars: Vec, +} + +impl FunctionCallSearcher { + fn new(func: FuncId, pre_token: FuncId, n_params: usize) -> Self { + Self { + func, + pre_token, + tok_var: "?tok".parse().unwrap(), + arg_vars: (0..n_params) + .map(|i| format!("?a{i}").parse().unwrap()) + .collect(), + } + } +} +impl Searcher for FunctionCallSearcher { + fn vars(&self) -> Vec { + vec![] + } + + fn search_with_limit( + &self, + egraph: &EGraph, + mut limit: usize, + ) -> Vec> { + let Some(classes) = egraph.classes_for_op(&Discriminant::FuncApp(self.func)) else { + return vec![]; + }; + let mut out = vec![]; + for eclass in classes { + if limit == 0 { + break; + } + if let Some(m) = self.search_eclass_with_limit(egraph, eclass, limit) { + limit = limit.saturating_sub(m.substs.len()); + out.push(m); + } + } + out + } + fn search_eclass_with_limit( + &self, + egraph: &EGraph, + eclass: Id, + _limit: usize, + ) -> Option> { + let mut seen: BTreeSet<&Box<[Id]>> = BTreeSet::new(); + let mut subst: Vec = vec![]; + + for node in &egraph[eclass].nodes { + let Symbolic::FuncApp(f, _tys, args) = node else { + continue; + }; + if *f != self.func { + continue; + } + + if seen.contains(args) { + continue; + } + seen.insert(args); + + let mut s = Subst::default(); + + for (var, &arg) in self.arg_vars.iter().zip(args.iter()) { + s.insert(*var, arg); + } + + let probe = Symbolic::FuncApp(self.pre_token, Box::new([]), args.clone()); + + if let Some(tok) = egraph.lookup(probe) { + s.insert(self.tok_var, tok); + } + subst.push(s) + } + if subst.is_empty() { + None + } else { + Some(SearchMatches { + eclass, + substs: subst, + ast: None, + }) + } + } } /// Wrap `inner` in a guard chain over **live ids**: `guards ==> inner`, as nested @@ -98,9 +210,11 @@ pub(super) fn fold_guards( /// the params and `f(params)`, so nothing here materializes the callee's body. /// That is what makes the definitional union's presence gate load-bearing. /// -/// `token` is the callee's `f%pre(args)` class at *this* call, `None` when the -/// definition has no pre-token (a contract function) or when no token exists for -/// these args. It is threaded separately rather than folded into the recipe +/// `token` is the callee's `f%pre(args)` class at *this* call. `None` from a +/// post-only rule ([`FunctionPostApplier`]), or when [`FunctionCallSearcher`] +/// found no token for these args on the clean graph — an occurrence no +/// value-position call produced, e.g. one arriving through another callee's +/// `ensures`. It is threaded separately rather than folded into the recipe /// because the post's `Val`s live in the callee's recipe-temp space, whereas /// this is already a caller-side `Id`. pub(super) fn replay_post( @@ -131,118 +245,61 @@ pub(super) fn replay_post( } } -impl Applier for FunctionUnfoldApplier { - fn apply_one( +impl FunctionUnfoldApplier { + /// Every release for one call `f[tys](args)` in `eclass`, with `tok_id` its + /// `f%pre(args)` class (`None`: no token existed when the searcher ran). + fn unfold_call( &self, egraph: &mut EGraph, eclass: Id, - _subst: &Subst, - _searcher_ast: Option<&PatternAst>, - _rule_name: Symbol, - ) -> Vec { - // Candidate calls in this e-class (deduped locally; the persistent `memo` - // is only consulted once we commit to building — see below). - let mut calls: Vec<(Box<[Type]>, Vec)> = Vec::new(); - for node in &egraph[eclass].nodes { - let Symbolic::FuncApp(f, tys, args) = node else { - continue; - }; - if *f != self.func { - continue; - } - let args: Vec = args.iter().map(|&a| egraph.find(a)).collect(); - let key = (tys.clone(), args); - if !calls.contains(&key) { - calls.push(key); - } + tys: Box<[Type]>, + args: &[Id], + tok_id: Option, + changed: &mut Vec, + ) { + debug_assert_eq!(args.len(), self.def.n_params, "function unfold arity"); + // The body instance is needed for the definitional union, and for + // nothing else: the post is a standalone recipe over the params. So an + // occurrence that no value-position call produced — no token, hence no + // union — materializes no body at all, which is what the presence gate + // was always supposed to buy. It must NOT be union-memoized, so it can + // still union later once propagation mints its token mid-saturation. + let do_union = tok_id.is_some(); + let has_post = self.def.post.is_some(); + if !do_union && !has_post { + return; } - let mut changed = Vec::new(); - for (tys, args) in calls { - debug_assert_eq!(args.len(), self.def.n_params, "function unfold arity"); - // The token (see `pre_token`) plays two distinct roles, mirroring how a - // `Forall` e-class does: its **presence** triggers materialization of - // the callee's body here, and its **truth** releases the axioms that - // materialization produces. Type args are not in the `FuncApp` - // congruence key, so `[]` matches any instantiation. - // - // The token is assumed at each call site under that call's path - // condition (`declaration.rs`, the `FunctionCall` arm), so its class is - // an `ite(pc, tok, true)` shape and is unconditionally `true` only for - // an unconditional call. `tok_id` therefore doubles as the release - // guard below. `pre_token = None` ⇒ released ungated (a contract - // `#requires`/`#ensures` boolean, whose role is to inline its formula). - let tok_id: Option = self.pre_token.and_then(|tok| { - egraph.lookup(Symbolic::FuncApp(tok, Box::new([]), args.clone().into())) - }); - let has_token = self.pre_token.is_none() || tok_id.is_some(); - // The body instance is needed for the definitional union, and for - // nothing else: the post is a standalone recipe over the params. So an - // occurrence that no value-position call produced — no token, hence no - // union — materializes no body at all, which is what the presence gate - // was always supposed to buy. It must NOT be union-memoized, so it can - // still union later once propagation mints its token mid-saturation. - let do_union = !self.limited_post && has_token; - let has_post = self.def.post.is_some(); - if !do_union && !has_post { - continue; - } - let key = (tys.clone(), args.clone()); - // Two independent memos, because the two releases happen at different - // times: `memo` says the post has been replayed at this call, and - // `do_union` is short-circuited before `union_memo` so the union memo is - // only ever touched when the token is present — a fresh union, or a call - // that replayed its post earlier and is now reached by a - // propagation-minted token. - let first_post = has_post && self.memo.insert(key.clone()); - let do_union_now = do_union && self.union_memo.insert(key); - // Nothing new to do: post already replayed and no (new) union due. - if !first_post && !do_union_now { - continue; - } - // Seed slots for the body instance. Only built when the union needs it; - // otherwise there is no body here and `vals` stays unused. - let vals = match do_union_now { - true => build_instance_vals_guarded( - egraph, - &self.def.steps, - &args, - &mut changed, - tok_id, - ), - false => Vec::new(), - }; + let key = (tys.clone(), args.to_vec()); + // Two independent memos, because the two releases happen at different + // times: `memo` says the post has been replayed at this call, and + // `do_union` is short-circuited before `union_memo` so the union memo is + // only ever touched when the token is present — a fresh union, or a call + // that replayed its post earlier and is now reached by a + // propagation-minted token. + let first_post = has_post && self.memo.insert(key.clone()); + let do_union_now = do_union && self.union_memo.insert(key); + // Nothing new to do: post already replayed and no (new) union due. + if !first_post && !do_union_now { + return; + } + if let (true, Some(tok)) = (do_union_now, tok_id) { + let vals = build_instance_vals_guarded(egraph, &self.def.steps, args, changed, tok_id); // Definitional axiom `tok ==> f(args) == body`. Absent for an abstract // function. // - // With a token this cannot be an e-class merge — a merge is - // unconditional and there is no such thing as a conditional one — so it - // is stated as a guarded *equality term*: `ite(tok, f(args) == body, - // true) == true`. Once the token collapses to `true` (an unconditional - // call, or a conditional one inside the probe clone that assumes its - // pc), `ite-reduce` exposes `f(args) == body == true` and - // `eq-true-union` performs the merge. - // - // Without a token (`pre_token = None`, a contract function) it stays a - // direct union: the body is a total function of the args (Deref became - // `unwrap∘proj`, div is total in the e-graph), so the equation holds - // even at pre-violating args, and such a formula must inline freely. - if do_union_now { - if let Some(res) = &self.def.res { - let result = resolve_val(egraph, &vals, res); - match tok_id { - None => { - if egraph.union(eclass, result) { - changed.push(egraph.find(eclass)); - } - } - Some(tok) => { - let true_ = expr!(egraph, true); - let rel = expr!(egraph, {tok} ==> ({eclass} == {result})); - if egraph.union(rel, true_) { - changed.push(egraph.find(rel)); - } - } - } + // This cannot be an e-class merge — a merge is unconditional and there + // is no such thing as a conditional one — so it is stated as a guarded + // *equality term*: `ite(tok, f(args) == body, true) == true`. Once the + // token collapses to `true` (an unconditional call, or a conditional + // one inside the probe clone that assumes its pc), `ite-reduce` + // exposes `f(args) == body == true` and `eq-true-union` performs the + // merge. + if let Some(res) = &self.def.res { + let result = resolve_val(egraph, &vals, res); + let true_ = expr!(egraph, true); + let rel = expr!(egraph, {tok} ==> ({eclass} == {result})); + if egraph.union(rel, true_) { + changed.push(egraph.find(rel)); } } // Propagated callee tokens: `tok ==> g%pre(gargs)` for each nested @@ -257,49 +314,134 @@ impl Applier for FunctionUnfoldApplier { // post-only occurrence built no body, so there is no `g(gargs)` node // here for a `g%pre` token to activate — and minting one would // reintroduce exactly the cascade the presence gate exists to stop. - if do_union_now { - for ts in &self.def.token_steps { - let tok_node = resolve_val(egraph, &vals, &ts.token); - // `guards` is the body-internal condition guarding the nested - // call; `tok_id` is this call's own token. Folding the former - // inside the latter gives `f%pre(a) ==> (b[x:=a] ==> g%pre(..))`. - let guarded = fold_guards(egraph, &vals, &ts.guards, tok_node); - let true_ = egraph.add(Symbolic::Lit(Literal::Bool(true))); - let rel = match tok_id { - Some(tok) => expr!(egraph, {tok} ==> {guarded}), - None => guarded, - }; - if egraph.union(rel, true_) { - changed.push(egraph.find(rel)); - } + for ts in &self.def.token_steps { + let tok_node = resolve_val(egraph, &vals, &ts.token); + // `guards` is the body-internal condition guarding the nested + // call; `tok` is this call's own token. Folding the former + // inside the latter gives `f%pre(a) ==> (b[x:=a] ==> g%pre(..))`. + let guarded = fold_guards(egraph, &vals, &ts.guards, tok_node); + let true_ = egraph.add(Symbolic::Lit(Literal::Bool(true))); + let rel = expr!(egraph, {tok} ==> {guarded}); + if egraph.union(rel, true_) { + changed.push(egraph.find(rel)); } } - // Recursive function: frame the full occurrence to its limited twin - // `f(args) == f'(args)`. `f'` has no unfold rule, so a limited call - // produced by unfolding `f`'s body never re-unfolds (bounding - // saturation); the frame lets a materialized `f(args)` value flow to - // any `f'(args)` a sibling unfold produced. - // - // **Ungated**, matching Silicon's `limitedAxiom`. It must NOT sit - // behind the `f%pre` presence token: the token is minted only at a - // value-position call, so gating strands a recursive function's post - // fact (stated on `f'`) in limited space whenever the occurrence - // arrived via a callee's `ensures` rather than a direct call. - // - // Cannot reintroduce unbounded unfolding: this mints `f'` *from* an - // existing `f` node, never the reverse, and the unfold rule filters - // on `FuncApp(f)`. - if !self.limited_post { - if let Some(lim) = self.def.limited { - let twin = egraph.add(Symbolic::FuncApp(lim, tys.clone(), args.clone().into())); - if egraph.union(eclass, twin) { - changed.push(egraph.find(eclass)); - } - } + } + // Recursive function: frame the full occurrence to its limited twin + // `f(args) == f'(args)`. `f'` has no unfold rule, so a limited call + // produced by unfolding `f`'s body never re-unfolds (bounding + // saturation); the frame lets a materialized `f(args)` value flow to + // any `f'(args)` a sibling unfold produced. + // + // **Ungated**, matching Silicon's `limitedAxiom`. It must NOT sit + // behind the `f%pre` presence token: the token is minted only at a + // value-position call, so gating strands a recursive function's post + // fact (stated on `f'`) in limited space whenever the occurrence + // arrived via a callee's `ensures` rather than a direct call. + // + // Cannot reintroduce unbounded unfolding: this mints `f'` *from* an + // existing `f` node, never the reverse, and the unfold rule filters + // on `FuncApp(f)`. + if let Some(lim) = self.def.limited { + let twin = egraph.add(Symbolic::FuncApp(lim, tys, args.into())); + if egraph.union(eclass, twin) { + changed.push(egraph.find(eclass)); + } + } + // Replay the post once per call (idempotent; guarded internally). + if first_post { + replay_post(egraph, &self.def, args, tok_id, changed); + } + } +} + +impl Applier for FunctionUnfoldApplier { + fn apply_one( + &self, + egraph: &mut EGraph, + eclass: Id, + subst: &Subst, + _searcher_ast: Option<&PatternAst>, + _rule_name: Symbol, + ) -> Vec { + // The call this match names. Re-canonicalized: earlier rules of this + // iteration may have merged classes since the search. + let args: Vec = self + .arg_vars + .iter() + .map(|&v| egraph.find(subst[v])) + .collect(); + // The token (see `FunctionCallSearcher`) plays two distinct roles, + // mirroring how a `Forall` e-class does: its **presence** triggers + // materialization of the callee's body here, and its **truth** releases + // the axioms that materialization produces. + // + // The token is assumed at each call site under that call's path + // condition (`declaration.rs`, the `FunctionCall` arm), so its class is + // an `ite(pc, tok, true)` shape and is unconditionally `true` only for + // an unconditional call. `tok_id` therefore doubles as the release + // guard. + let tok_id = subst.get(self.tok_var).map(|&t| egraph.find(t)); + // The type instantiations applied at these args (a `Subst` cannot carry + // types, so they are re-read from the class). + let mut instantiations: Vec> = Vec::new(); + for node in &egraph[eclass].nodes { + let Symbolic::FuncApp(f, tys, nargs) = node else { + continue; + }; + if *f != self.func || nargs.len() != args.len() { + continue; + } + let same = nargs.iter().zip(&args).all(|(&a, &b)| egraph.find(a) == b); + if same && !instantiations.contains(tys) { + instantiations.push(tys.clone()); + } + } + let mut changed = Vec::new(); + for tys in instantiations { + self.unfold_call(egraph, eclass, tys, &args, tok_id, &mut changed); + } + changed + } + + fn vars(&self) -> Vec { + vec![] + } +} + +impl Applier for FunctionPostApplier { + fn apply_one( + &self, + egraph: &mut EGraph, + eclass: Id, + _subst: &Subst, + _searcher_ast: Option<&PatternAst>, + _rule_name: Symbol, + ) -> Vec { + let mut changed = Vec::new(); + if self.def.post.is_none() { + return changed; + } + // Candidate calls in this e-class (deduped locally; the persistent `memo` + // is only consulted once we commit to replaying). + let mut calls: Vec = Vec::new(); + for node in &egraph[eclass].nodes { + let Symbolic::FuncApp(f, tys, args) = node else { + continue; + }; + if *f != self.func { + continue; } - // Replay the post once per call (idempotent; guarded internally). - if first_post { - replay_post(egraph, &self.def, &args, tok_id, &mut changed); + let args: Vec = args.iter().map(|&a| egraph.find(a)).collect(); + let key = (tys.clone(), args); + if !calls.contains(&key) { + calls.push(key); + } + } + for (tys, args) in calls { + debug_assert_eq!(args.len(), self.def.n_params, "function post arity"); + if self.memo.insert((tys, args.clone())) { + replay_post(egraph, &self.def, &args, None, &mut changed); } } changed @@ -310,23 +452,22 @@ impl Applier for FunctionUnfoldApplier { } } -/// Mint the lazy-unfolding rule for one verified function's definition recipe. -/// Reuses [`AxiomTriggerSearcher`] as-is — it only checks `FuncApp(f, ..)` -/// presence, independent of arity/type-args, exactly what's needed here too. +/// Mint the lazy-unfolding rule for one verified function's definition recipe, +/// gated on its uniform pre-token `f%pre` (`FuncRegistry::fn_pre_token`). pub(crate) fn function_rule( name: &str, func: FuncId, def: Arc, - pre_token: Option, + pre_token: FuncId, ) -> Rule { - let searcher = AxiomTriggerSearcher { func }; + let searcher = FunctionCallSearcher::new(func, pre_token, def.n_params); let applier = FunctionUnfoldApplier { func, + tok_var: searcher.tok_var, + arg_vars: searcher.arg_vars.clone(), def, - limited_post: false, memo: Memo::new(), union_memo: Memo::new(), - pre_token, }; timed(Rewrite::new(format!("fn-{name}"), searcher, applier).expect("function rule")) } @@ -339,14 +480,10 @@ pub(crate) fn function_rule( /// recursive call work (Silicon's phase-1 `post` axiom). pub(crate) fn post_rule(name: &str, func: FuncId, def: Arc) -> Rule { let searcher = AxiomTriggerSearcher { func }; - let applier = FunctionUnfoldApplier { + let applier = FunctionPostApplier { func, def, - limited_post: true, memo: Memo::new(), - union_memo: Memo::new(), - // Post-only rule: no definitional union, so no token gate. - pre_token: None, }; timed(Rewrite::new(format!("fn-post-{name}"), searcher, applier).expect("function post rule")) } diff --git a/tests/cases/failing/functions/unreachable_post_stale_token.vpr b/tests/cases/failing/functions/unreachable_post_stale_token.vpr new file mode 100644 index 0000000..b2bfbc6 --- /dev/null +++ b/tests/cases/failing/functions/unreachable_post_stale_token.vpr @@ -0,0 +1,40 @@ +// A callee's post must stay behind its `f%pre` token even when the args were +// merged earlier in the same saturation iteration. This is the shape of Prusti's +// `*_unreachable() ensures false` arm, which made Helium accept methods Silicon +// rejects (chrono, once_cell, regex-automata in cratesTop100Split2000). +// +// Unfolding `f` creates `unreachable(a(s))` and, behind `f%pre ==> (!b ==> ..)`, +// its token `unreachable%pre(a(s))` — vacuous here, since `b` is `true`. In the +// next iteration the `a(t) == cty()` axiom merges `a(s)` into `cty()`'s class +// before `unreachable`'s rule applies. Looked up from the applier, the token then +// missed in the not-yet-rebuilt hashcons, and the post `false` was released +// ungated, proving `assert false`. The token is now looked up by the searcher, on +// the clean graph. +// +// `k1..k3` are load-bearing: they make `cty()`'s class the larger one, so it +// becomes the root of the merge and `a(s)`'s id goes stale. Without them the +// test passes even on the buggy code. +domain Ty { + function cty(): Ty + function k1(): Ty + function k2(): Ty + function k3(): Ty + function a(t: Ty): Ty + axiom { k1() == cty() } + axiom { k2() == cty() } + axiom { k3() == cty() } + axiom { forall t: Ty :: { a(t) } a(t) == cty() } +} + +function unreachable(t: Ty): Int + ensures false + +function f(t: Ty, b: Bool): Int +{ b ? 0 : unreachable(t) } + +method m(s: Ty) +{ + var y: Int + y := f(a(s), true) // evaluates to 0; unreachable(..) is never evaluated + assert false // must fail +}