Variants #1622

arnaudgolfouse · 2025-07-09T18:43:25Z

This allow variants in various places:

simply recursive functions (logic and program)
loops (this allows loops in ghost code!)

Together with a rework of the WellFounded trait, to allow variants on custom types.

Fixes #561, #754.

jhjourdan

Great job!

All in all, I think that most of this is OK, but the way variant assertion are inserted need to be improved:

For loops, it should really rely on the WTO, and therefore I think that this should really be done by the backend. In particular, I'm not sure that we should store sets of variants to check at "continue" blocks. Instead, when entering a WTO component whose head has a variant, create a new handler for the head of the loop that will check the variant decrease, and make all the jumps from inside the component point to this new handler.
For recursive calls in program code, I would really prefer not translating operands to terms. This would be yet another translation from places to XXX, and I'm afraid of subtle semantic differences betwen the versions. Instead, please use a method similar to the one for loop I propose above: create a new sub-handler for recursive calls, and make it check that the variant decreases before performing the actual recursive call.

creusot-contracts/src/well_founded.rs

jhjourdan · 2025-07-09T20:31:05Z

creusot-contracts/src/well_founded.rs

+        self >= 0 && self > other
+    }
+
+    #[trusted] // FIXME: find the right why3 lemma


I don't think that this lemma exists. But it's easy by induction on s[0], and you have access to that in Why3 IDE.

creusot-contracts/src/well_founded.rs

jhjourdan · 2025-07-09T20:57:40Z

why3/src/declaration.rs

@@ -91,7 +90,7 @@ impl Condition {
 pub struct Contract {
    pub requires: Box<[Condition]>,
    pub ensures: Box<[Condition]>,
-    pub variant: Option<Exp>,
+    pub variant: Option<(Exp, Type)>,


What's the purpose of this change? It seems like the type is not used anywhere in the why3 crate.

It's used in creusot/src/backend/program.rs, when defining the variable that holds the variant.

jhjourdan · 2025-07-09T22:42:28Z

creusot/src/gather_spec_closures.rs

+                                let res = !self.before_loop.contains(*p);
+                                if !res && std::mem::replace(&mut has_met_before_loop, true) {
+                                    self.ctx.dcx().span_bug(self.body.span, "a basic block is marked as the entry for multiple loops: this should not happen.")
+                                }
+                                res


That's very fragile. This is essentially assuming that a loop header is always following immediately a block annotated with before_loop. Thus, this rely on rustc not inserting intermediary no-op blocks, etc...

I don't think this is a good design. predecessors should be classified based on the WTO.

jhjourdan · 2025-07-09T23:02:09Z

creusot/src/translation/fmir.rs

@@ -65,6 +64,47 @@ impl<'tcx> Place<'tcx> {
            None
        }
    }
+
+    fn into_term(self, tcx: TyCtxt<'tcx>, locals: &LocalDecls<'tcx>, span: Span) -> Term<'tcx> {


I don't like this much, both because this means that we are introducing yet another translation for places (with maybe subtle semantic differences), and because the resulting code will have some duplication.

Instead, could we not add to FMir the possibility to annotate calls with a variant to check, before substituting the parameters ? In the backend, it should be easy to check the variant when translating the call.

An alternative is to generate a separate handlers for recursive calls, with one additional precondition: the fact that the variant decreased.

I did your second solution, which is somewhat similar to loop variants.

creusot/src/validate/terminates.rs

jhjourdan · 2025-07-09T23:12:26Z

creusot/src/validate/terminates.rs

        };
    }

    // detect mutual recursion
    let cycles = tarjan_scc(&call_graph);
    for cycle in cycles {
+        // FIXME: if there is a variant on all the functions in the cycle, then
+        // - Insert the recursive call in `recursive_calls`


Somehow we eed to check that variants all have the same type. This is tricky because this involves substitutions.

jhjourdan · 2025-07-09T23:15:23Z

creusot/src/validate/terminates.rs

@@ -450,6 +478,11 @@ impl CallGraph {
            if !(is_pearlite(ctx.tcx, def_id) || ctx.sig(def_id).contract.terminates) {
                // Only consider functions marked with `terminates`: we already ensured
                // that a `terminates` functions only calls other `terminates` functions.
+                if let Some(variant) = &ctx.sig(def_id).contract.variant {
+                    ctx.dcx().struct_span_warn(variant.span, "variant will be ignored")


ignored, really ? It seems to me that the variant will be checked, but it is useless to prove the termination of the function.

It is ignored, because we don't even do the analysis in this case. Thus we don't know what recursive calls the function will make, which is needed to know where to insert the variant checks.

arnaudgolfouse force-pushed the loop-variants branch from 6f86486 to 88cb570 Compare July 9, 2025 18:54

jhjourdan reviewed Jul 9, 2025

View reviewed changes

ethanbb mentioned this pull request Aug 1, 2025

Guide: Update language about logic functions and document #[open] #1649

Merged

arnaudgolfouse force-pushed the loop-variants branch 2 times, most recently from ddf49af to 32bed6d Compare August 8, 2025 15:08

arnaudgolfouse added 8 commits August 8, 2025 17:08

Clean up #[variant(...)] macro code

49bb43d

Check for useless gotos in a more future-proof way

ed23bad

Pass LoweringState as an immutable borrow

164ef2f

Insert checks for loop variants

3d076b8

Rework WellFounded and use it in loop variants

2f7fb84

Add some doc to the variant macro

53d401f

Allow loops in terminating functions (and ghost code)

a983f70

Allow break/continue in ghost code

ad583ec

arnaudgolfouse force-pushed the loop-variants branch from 32bed6d to 7f93023 Compare August 8, 2025 15:08

arnaudgolfouse added 6 commits August 8, 2025 17:34

Allow simple recursion checked by a variant

c9fc426

Add a warning for functions where the variant is ignored

2ebc174

Use WellFounded for logic variants

ed8e7ea

Add tests

fd0594e

Update the 'bdd' test

d915dc4

Update tests

3d9bc4e

arnaudgolfouse force-pushed the loop-variants branch from 7f93023 to 3d9bc4e Compare August 10, 2025 09:59

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Variants #1622

Variants #1622

Uh oh!

arnaudgolfouse commented Jul 9, 2025 •

edited by jhjourdan

Loading

Uh oh!

jhjourdan left a comment

Uh oh!

Uh oh!

Uh oh!

jhjourdan Jul 9, 2025

Uh oh!

Uh oh!

jhjourdan Jul 9, 2025

Uh oh!

arnaudgolfouse Aug 4, 2025

Uh oh!

jhjourdan Jul 9, 2025

Uh oh!

jhjourdan Jul 9, 2025

Uh oh!

jhjourdan Jul 9, 2025

Uh oh!

arnaudgolfouse Aug 4, 2025

Uh oh!

Uh oh!

jhjourdan Jul 9, 2025

Uh oh!

jhjourdan Jul 9, 2025

Uh oh!

arnaudgolfouse Aug 8, 2025

Uh oh!

Uh oh!

Variants #1622

Are you sure you want to change the base?

Variants #1622

Uh oh!

Conversation

arnaudgolfouse commented Jul 9, 2025 • edited by jhjourdan Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

jhjourdan left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

arnaudgolfouse commented Jul 9, 2025 •

edited by jhjourdan

Loading