36 unsound behaviour in recursive function

src/verify/cert.rs

@@ -255,6 +255,10 @@ pub(crate) struct RecipeBuilder {
     /// In-SCC callees (a recursion cycle's members), lowered to their limited
     /// twin so a downstream unfold halts after one level.
     recursive_scc: Option<crate::dhash::HashSet<MemberId>>,
+    /// Set when the walked body is a postcondition (`f#ensures`). A recursive
+    /// call there propagates no `f%pre` token (see
+    /// [`Self::propagates_recursive_token`]).
+    post_contract: bool,
     /// Footprint slots recorded by a resource body's `acc`s, in body order:
     /// the slot's location kind, element type, and the recipe temps of its
     /// address and permission (sliced into standalone [`SlotRecipe`]s at the
@@ -280,11 +284,18 @@ impl RecipeBuilder {
             n_params,
             steps: Vec::new(),
             recursive_scc,
+            post_contract: false,
             pending_slots: Vec::new(),
             token_steps: Vec::new(),
         }
     }
 
+    /// Mark the walked body as a postcondition (`f#ensures`).
+    pub(crate) fn post_contract(mut self) -> Self {
+        self.post_contract = true;
+        self
+    }
+
     /// Record an orphan `g%pre` token step so [`Self::slice`] keeps it (see
     /// [`Self::token_steps`]), together with the callee-internal path condition of
     /// the call it accompanies — empty when the walk has no recipe-space pc to
@@ -324,6 +335,20 @@ impl RecipeBuilder {
         self.recursive_scc.as_ref().is_some_and(|s| s.contains(&m))
     }
 
+    /// Whether a recursive call in this body propagates its `f%pre` token.
+    ///
+    /// In a function body it must: that token is what gates the post the
+    /// limited twin's rule replays at the recursive unroll (Silicon's
+    /// `bodyPreconditionPropagation` covers recursive calls too). In a
+    /// postcondition it must not: the posts of an SCC whose members mention each
+    /// other in their `ensures` (Prusti's `make_generic_s_T`/`make_concrete_s_T`)
+    /// would then mint each other's tokens without end, building ever deeper
+    /// `g'(f'(g'(..)))` terms wherever the path condition keeps the equalities
+    /// that would collapse them undecided.
+    pub(crate) fn propagates_recursive_token(&self) -> bool {
+        !self.post_contract
+    }
+
     /// Consume the builder into a function definition's parts. A function
     /// stream contains no `Seed` steps (params are pre-seeded), so it converts
     /// 1:1 — `token_steps` index into the same shared stream, as does the post

src/verify/declaration.rs

@@ -423,9 +423,19 @@ fn eval_pure_inst(
             // function-unfold encoding; every axiom above inherits it transitively
             // through the token. `.rev()` because `pc_lits` is outermost-first and
             // `implication` folds innermost-first (cf. `InstKind::Assume`).
-            if ctx
-                .fn_certs
-                .is_none_or(|certs| certs.contains_key(&fc.function))
+            //
+            // A callee in the recursion cycle being verified has no cert yet, but
+            // still gets its token: the spec-derived post rule of the batch
+            // (`rewrite::post_rule`) replays the induction hypothesis only behind
+            // it, i.e. only on the path that makes the call.
+            let in_scc = ctx
+                .recipe
+                .as_ref()
+                .is_some_and(|rb| rb.is_recursive_callee(fc.function));
+            if in_scc
+                || ctx
+                    .fn_certs
+                    .is_none_or(|certs| certs.contains_key(&fc.function))
             {
                 let name = ctx.member_name(fc.function);
                 let tok = ctx.alloc.fn_pre_token(fc.function, &name);
@@ -442,11 +452,9 @@ fn eval_pure_inst(
                 // limited twin `f'` — uninterpreted, so unfolding this recipe
                 // at a call site stops after one level. Every other callee
                 // keeps its full id and unfolds normally.
-                let recursive = ctx
-                    .recipe
-                    .as_ref()
-                    .unwrap()
-                    .is_recursive_callee(fc.function);
+                let rb = ctx.recipe.as_ref().unwrap();
+                let recursive = rb.is_recursive_callee(fc.function);
+                let propagates_recursive = rb.propagates_recursive_token();
                 let func = if recursive {
                     let name = ctx.member_name(fc.function);
                     ctx.alloc.limited(fc.function, &name)
@@ -462,11 +470,16 @@ fn eval_pure_inst(
                 // Which calls those are is the **translator's** call, carried on the
                 // inst as `FunctionCall::export`: a value-position use of a Silver
                 // function exports, an obligation call / a call inside a contract
-                // definition / an `@addr` or domain application does not. A
-                // recursive call is excluded here rather than there, because SCC
-                // membership is a verifier fact: it already targets the limited twin
-                // `f'`, which has no unfold rule for a token to trigger.
-                let propagate = fc.export && !recursive;
+                // definition / an `@addr` or domain application does not.
+                //
+                // A recursive call propagates too, although it targets the limited
+                // twin `f'`, which has no unfold rule for the token to trigger: the
+                // token is what releases `f`'s post at `f'(gargs)`
+                // (`rewrite::function_post_rule`), and nothing else may. Except in a
+                // postcondition, which is a verifier fact (SCC membership) rather
+                // than the translator's: see
+                // `RecipeBuilder::propagates_recursive_token`.
+                let propagate = fc.export && (!recursive || propagates_recursive);
                 let g_pre = propagate.then(|| {
                     let name = ctx.member_name(fc.function);
                     ctx.alloc.fn_pre_token(fc.function, &name)
@@ -1996,7 +2009,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,
@@ -2005,12 +2018,15 @@ fn assume_axioms(ctx: &mut VerifyContext<'_>, program: &vmir::Program) -> Result
             ));
             // A recursive function's post fact also triggers on its limited
             // twin `f'` — that is what delivers the postcondition at a
-            // recursive unroll (the twin has no unfold rule by design).
+            // recursive unroll (the twin has no unfold rule by design). Behind
+            // the same `f%pre` token, which the unrolled body propagates for its
+            // recursive call.
             if def.limited.is_some() && def.post.is_some() {
                 ctx.axiom_rules
                     .push(crate::verify::rewrite::function_post_rule(
                         &name,
                         std::sync::Arc::clone(def),
+                        pre_token,
                     ));
             }
         }
@@ -2626,15 +2642,26 @@ pub(crate) fn verify_function(
     // `ensures` link once the walk is done (`post_fact`). No precondition guard
     // is prepared: a function's facts are gated by its `f%pre` token, released
     // at the call.
-    ctx.recipe = Some(crate::verify::cert::RecipeBuilder::new(
-        function.params.len(),
-        recursive_scc.cloned(),
-    ));
+    let recipe =
+        crate::verify::cert::RecipeBuilder::new(function.params.len(), recursive_scc.cloned());
+    // A postcondition is the `ensures` link of some function. Only matters for
+    // recursive calls, so only looked for in a recursion cycle.
+    let is_post_contract = recursive_scc.is_some()
+        && program.decls.iter().any(|d| {
+            matches!(d, vmir::Declaration::Function(g)
+                if g.ensures.as_ref().is_some_and(|e| e.member == self_id))
+        });
+    ctx.recipe = Some(match is_post_contract {
+        true => recipe.post_contract(),
+        false => recipe,
+    });
     // Recursive batch: every SCC member's spec-derived post axiom is available
     // while this body is checked (Silicon emits `post` in phase 1, before the
     // phase-2 body check) — this is what lets the exit assert use a recursive
     // call's postcondition (induction; termination is not checked, same as
-    // Silicon without `decreases`).
+    // Silicon without `decreases`). Like any post, it is gated by the call's
+    // `f%pre` token, which the `FunctionCall` arm mints under the call's path
+    // condition.
     if let Some(scc) = recursive_scc {
         for &m in scc {
             let vmir::Declaration::Function(mf) = &program.decls[m] else {
@@ -2643,8 +2670,10 @@ pub(crate) fn verify_function(
             if let Some(post) = contract_post_definition(ctx.alloc, program, m, mf, false) {
                 let name = ctx.member_name(m);
                 let func = crate::verify::func_registry::func_id_for_member(m);
-                ctx.axiom_rules
-                    .push(crate::verify::rewrite::post_rule(&name, func, post));
+                let pre_token = ctx.alloc.fn_pre_token(m, &name);
+                ctx.axiom_rules.push(crate::verify::rewrite::post_rule(
+                    &name, func, post, pre_token,
+                ));
             }
         }
     }

src/verify/declaration/e2e/mod.rs

@@ -3332,9 +3332,16 @@ function safediv(x: Int, y: Int): Int
 fn recursive_function_postcondition_by_induction() {
     // Induction via the limited encoding: while checking `f`'s body, `f`'s own
     // spec-derived post rule is installed (Silicon's phase-1 `post` axiom), so
-    // the recursive call's post (`f(next(x)) == 0`, guarded by
-    // `ok(next(x))` from the axiom) discharges the exit assert. At the outer
-    // call site the post rides the certificate's post fact.
+    // the recursive call's post (`f(next(x)) == 0`, behind the call's
+    // `f%pre(next(x))` token, whose precondition `ok(next(x))` the axiom
+    // discharges) proves the exit assert. At the outer call site the post rides
+    // the certificate's post fact.
+    //
+    // The recursive call is unconditional (no termination check, as in Silicon
+    // without `decreases`): the token, and with it the hypothesis, holds on every
+    // path. Under a branch, `x == 0 ? 0 : f(next(x))`, the hypothesis holds only on
+    // the call's path, and the exit assert needs a case split Helium does not make:
+    // `known_limitations/goal_needs_case_split_recursive_post.vpr`.
     let input = r#"
 domain D {
     function ok(x: Int): Bool
@@ -3345,7 +3352,7 @@ domain D {
 function f(x: Int): Int
     requires ok(x)
     ensures result == 0
-{ x == 0 ? 0 : f(next(x)) }
+{ f(next(x)) }
 
 method m(x: Int)
     requires ok(x)

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<cert::FunctionDefinition>,