Specification refinement by Trzyq0712 · Pull Request #133 · Aurel300/prusti-dev

Trzyq0712 · 2026-01-30T20:12:11Z

While the refine_spec procedural macro created the appropriate specification function, it was currently ignored in the verification process. This change wires up the specification function to generate appropriate Viper code.

Example:

#[refine_spec(where T: TraitA + TraitB, U: TraitA, [requires(<refined>)])]
#[requires(<default>)]

will roughly translate to

requires (TraitA_impl(T$0) && TraitB_impl(T$0) && TraitA_impl(T$1)) ==> <refined>
requires !(TraitA_impl(T$0) && TraitB_impl(T$0) && TraitA_impl(T$1)) ==> <default>

Support for:

Multiple generics + multiple traits combinations
Concrete types (where i32: Copy)
requires and ensures clauses
Bounds on projections (where T::Item: Bar)
Type projection predicates (where T: Foo<Item = i32>)

Unsupported:

We will now limit the number of refine_specs to one per function, as the expected behavior with multiple refine specs on a single function is rather unclear.
Const projection predicates ('where T: Foo<N = 42>`) Support for const projections in refine_specs #147

Results:
With this PR, we are now able to verify programs like these. Assuming that Sized, MetaSized and Tuple traits are correctly encoded, and one manually fixes issues caused by #152.

trait MyFnOnce<Args: std::marker::Tuple> {
    type Output;
    #[requires(false)]
    #[refine_spec(where Self: ClosureSpec<Args, Self::Output>, [
        requires(Self::requires(args)),
        ensures(Self::ensures(args, result))
    ])]
    #[trusted]
    fn call_once(self, args: Args) -> Self::Output
    where
        Self: Sized;
}

impl MyFnOnce<(i32,)> for MyClosure {
    type Output = i32;
    fn call_once(self, (v,): (i32,)) -> i32 {
        v + 25
    }
}

trait ClosureSpec<Args, Output> {
    #[pure]
    fn requires(args: Args) -> bool;
    #[pure]
    fn ensures(args: Args, result: Output) -> bool;
}

impl ClosureSpec<(i32,), i32> for MyClosure {
    #[pure]
    fn requires((v,): (i32,)) -> bool {
        v >= 0
    }
    #[pure]
    fn ensures((v,): (i32,), result: i32) -> bool {
        result == v + 25
    }
}

struct MyClosure {
    cap: i32,
}

fn main() {
    let cap = 2137;
    let cl = MyClosure { cap };
    let res = cl.call_once((42,));

    assert!(res == 67);
}

Trzyq0712 · 2026-03-09T09:20:36Z

We currently translate each specification item in a refine_spec macro into a separate rust function with the where clause attached. For example

#[refine_spec(where T: Bar, [requires(v > 0), requires(v < 10)])]

is translated to

fn spec_item_pre_0<T: Bar>(v: i32) -> bool { v > 0 }
fn spec_item_pre_1<T: Bar>(v: i32) -> bool { v < 10 }

This is problematic in the sense that we get two "different" specification refinements despite the fact that they use the same where clause. Currently, such specification will be rejected due to "multiple" spec refine items. To have this working, one would need to write:

#[refine_spec(where T: Bar, [requires(v > 0 && v < 10)])]

We could alternatively try to group the specification items, and then assert that there is only one refinement group. What do you think?

Additionally, it would be now legal to write such a refinement:

#[refine_spec(where T: Foo, [requires(v > 0)])]
#[refine_spec(where T: Bar, [ensures(result == 42)])]

As there is at most one refinement for pre/post conditions, this is deemed legal. Personally, I don't see an issue with this, but I'd like to know if you think this should be allowed or not.

Aurel300 · 2026-03-09T09:39:35Z

This is problematic in the sense that we get two "different" specification refinements despite the fact that they use the same where clause. Currently, such specification will be rejected due to "multiple" spec refine items. To have this working, one would need to write:

Where do we reject this? We can make the spec rewriter produce multiple spec items with, e.g., an extra attribute (containing another UUID I guess) attached to each. When identifying the specs after typing, we would group by this new attribute.

(I prefer this to grouping by the where clause, in particular I worry about syntactically different clauses that actually have the same constraints.)

As there is at most one refinement for pre/post conditions, this is deemed legal. Personally, I don't see an issue with this, but I'd like to know if you think this should be allowed or not.

I would say this is not consistent with the rules we are trying to enforce, but I am also not completely opposed to lifting the restriction. However, we need to enforce behavioural subtyping correctly. For example, suppose a method had:

(A) a base spec,
(B) a spec with Self: A,
(C) a spec with Self: B, and
(D) a spec with Self: A + B.

For this method, we should enforce that B is a b.s. of A, C is a b.s. of A, and D is a b.s. of both B and C.

This PR doesn't implement any behavioural subtyping checks yet, but maybe that's what your goal was for now @JonasAlaif?

Trzyq0712 · 2026-03-09T09:44:14Z

A more general question is about how we treat specification items more generally. Consider the following example:

#[requires(y > 0)]
#[ensures(result == 42)]
fn fun<T>(x: T, y: i32) -> i32 { ... }

In reality, this should really be:

#[requires(false)]
#[ensures(true)]
#[refine_spec(where T: Sized, [requires(y > 0), ensures(result == 42)])]

This is due to the implicit Sized bound on T.
My broader question is whether we actually treat all specification items (refinements or not) in the same general way. This, of course, only complicates reasoning about how we pick a specifications that should apply given a generic, but I wanted to get some closure on this.

Trzyq0712 · 2026-03-09T09:46:02Z

This PR doesn't implement any behavioural subtyping checks yet, but maybe that's what your goal was for now @JonasAlaif?

We have discussed with @JonasAlaif to implement behavioral subtyping checks in a separate PR later.

Aurel300 · 2026-03-09T09:52:35Z

In reality, this should really be:

#[requires(false)]
#[ensures(true)]
#[refine_spec(where T: Sized, [requires(y > 0), ensures(result == 42)])]

I don't think so? The method is not callable when T: Sized doesn't hold. This is enforced by rustc, not us, so we don't even have to worry about downstream crates (which don't use Prusti to compile/verify) breaking the requirement.

Besides, the b.s. check for the above is trivially true, so we don't really need to emit it, and any actual refine_specs written by the user would also include the T: Sized bound so they would be refining the non-trivial spec.

Trzyq0712 · 2026-03-09T10:03:32Z

I would say this is not consistent with the rules we are trying to enforce, but I am also not completely opposed to lifting the restriction. However, we need to enforce behavioral subtyping correctly. For example, suppose a method had:
* (A) a base spec,

* (B) a spec with `Self: A`,

* (C) a spec with `Self: B`, and

* (D) a spec with `Self: A + B`.

Since we are talking about multiple refine_specs, what should we generate in this case?

#[requires(<cond1>)
#[refine_spec(where <where1>, [requires(<cond2>])]
#[refine_spec(where <where2>, [requires(<cond3>])]

Should we generate the following?

requires !<where1> && !<where2> ==> <cond1>
requires <where1> && !<where2> ==> <cond2>
requires !<where1> && <where2> ==> <cond3>
requires <where1> && <where2> ==> <cond2> && <cond3>

What if the user were to now manually add a refinement with where <where1> + <where2>? This would be problematic if we encoded it this way as we would have generated a requires !<where1> && !<where2> && (<where1> && <where2>) which is never true.
Alternatively, we could skip checking that other refinements are not matched, but this in turn would be problematic for the post conditions:

ensures !<where1> && !<where2> ==> result >= 0
ensures <where1> ==> result == 0
ensures <where2> ==> result == 1

If the user would now supply a type that is both <where1> and <where2>, what should be the effective post condition?

Trzyq0712 · 2026-03-09T10:17:02Z

Where do we reject this? We can make the spec rewriter produce multiple spec items with, e.g., an extra attribute (containing another UUID I guess) attached to each. When identifying the specs after typing, we would group by this new attribute.

I have not yet pushed the changes that would reject multiple refinements as I'm still figuring out the exact semantics.

Maybe we could aim for a structure like so: https://hackmd.io/@7_G-0elATUmQnp4YTzUs0A/SkYJtr3YWl

Trzyq0712 · 2026-03-12T09:22:52Z

This is problematic in the sense that we get two "different" specification refinements despite the fact that they use the same where clause. Currently, such specification will be rejected due to "multiple" spec refine items. To have this working, one would need to write:

This has been fixed by grouping related refine_spec items using an identifier. This means that if there are multiple items with the same where clause, they will still get rejected due to not being the exact same refine_spec.

#[refine_spec(where T: Foo, [requires(v > 0)])]
#[refine_spec(where T: Bar, [ensures(result == 42)])]

This is now not allowed and will cause a compiler crash (we opt for crashing over reporting an error as there might be an external refine_spec that is not immediately visible).

Trzyq0712 · 2026-03-12T09:30:14Z

One last thing that we might want to address at some point is the fact that the way we currently construct the impl bounds includes extra constraints that the user did not write. Looking at this example:

#[refine_spec(where T: Foo, [requires(v > 0])]
fn fun<T, U: Bar>(v: i32) {}

This results in the following requires item:

fn fun_pre<T, U: Bar>(v: i32) where T: Foo {}

Causing us to generate a check:

impl_Foo(T) && impl_Sized(T) && impl_Bar(U) && impl_Sized(U)

While the following would suffice:

impl_Foo(T)

To my knowledge this does not affect correctness, but does introduce unnecessary overhead.
One potential issue is if the user were to write the following (useless) refinement.

#[refine_spec(where T: ?Sized, [requires(v > 0)])]
#[requires(v > 127)]
#[trusted]
fn my_function<T>(v: i32) {}

This results in something a bit unexpected. The effective bound becomes T: ?Sized + Sized ==> T: Sized, and thus makes the refined specification the only one that will ever be used. (Similarly if the user states trait bounds that are a subset of bounds implied by the signature itself)

Trzyq0712 · 2026-03-12T10:01:00Z

-                self.specs_with_constraints
-                    .values_mut()
-                    .for_each(|s| s.posts.push(post.to_def_id()));


Not sure about this change. I think what we will want to do is to check behavioral subtyping by emitting appropriate checks, and thus I think we should keep the refined and unrefined postconditions separate as we do with preconditions. Having them together makes it tricky to find the correct specification item to generate a viper condition.

Trzyq0712 · 2026-03-12T10:49:35Z

+                    ty::TermKind::Ty(ty) => {
+                        let projection = trait_.assoc_types[&proj_pred.def_id()](
+                            args.get_ty(),
+                            args.get_const(),
+                        );
+                        let decomp = RustTyDecomposition::from_ty(ty, did);
+                        let gparams = deps.require_dep::<GenericParamsEnc>(did.into()).unwrap();
+                        let ty_expr = gparams.ty_expr(deps, decomp);
+                        checks.push(vcx.mk_eq_expr(projection, ty_expr));
+                    }
+                    ty::TermKind::Const(_) => {
+                        todo!("Implement const projections in `refine_spec` bounds")
+                    }


There is quite a bit overlap in what I do here and what I do in #137 in trait_impls.rs. We could try to reuse the functionality from there, or extract it for reusability.

Aurel300 · 2026-03-12T11:59:10Z

    ///
    /// If this postcondition has a constraint it will be attached to the corresponding
-    /// constrained spec **and** the base spec, otherwise just to the base spec.
+    /// constrained spec, otherwise just to the base spec.


Let's be careful (this isn't just about the comment): the constraints here aren't just the ones from the refine spec clause. Consider:

#[requires(base_pre)] #[refine_spec(where T: Bar, [requires(refined_pre)])] fn foo<T: Foo>(x: T);

(The T: Foo above is equivalent to the clause where T: Foo.)

The spec items we want to generate are:

fn spec_item_pre_1<T>(x: T) -> bool where T: Foo, // constraint from method { base_pre } fn spec_item_pre_2<T>(x: T) -> bool where T: Foo, // constraint from method T: Bar, // constraint from refine_spec { refined_pre }

Unless I misunderstand your comment, the code you are pointing at is not really responsible for what the doc comment seems to imply. Here, it's not about attaching the type constraints, but rather the constraint itself. The generated spec items are still as expected.

#[prusti::spec_only] #[prusti::spec_id = "18c13dce80414c678bf977582ea4520d"] fn prusti_pre_item_foo_18c13dce80414c678bf977582ea4520d<T: Foo>(x: T) -> bool { let val: bool = (true) || (false); val } #[prusti::spec_only] #[prusti::spec_id = "e96feb1f9dee4b93a1eb03f11cb5a94c"] #[prusti::type_cond_spec_trait_bounds_in_where_clause = "ff0b081e-b912-4643-8298-bd50c8d06910"] fn prusti_pre_item_foo_e96feb1f9dee4b93a1eb03f11cb5a94c<T: Foo>(x: T) -> bool where T: Bar { let val: bool = true; val }

This was never correct as it was processing order dependent.

JonasAlaif · 2026-03-20T11:57:20Z

        self.set_monomorphised(def_id, substs, caller_def_id, body)
    }

+    pub fn get_caller_bounds(&self, def_id: DefId) -> Vec<ty::Clause<'tcx>> {


This is not the right place for this. I would incorporate this as part of GParams (they already have the param_env): you could even have an encoder that takes a GParams as input and returns the bounds as viper expressions as output.

Introduced ClausesEnc in #158.

I would just introduce it in this PR: it's strange to have it in a separate one where it's completely unused/untested

I will close that PR then.

JonasAlaif · 2026-03-25T13:57:55Z

            .entry(constraint)
-            .or_insert_with(|| self.base_spec.clone())
+            .or_insert_with(|| {
+                let mut spec = self.base_spec.clone();


I remember discussing that we wouldn't clone the whole base_spec here. Could you make that change?

Trzyq0712 force-pushed the spec_refinements branch from 9d38699 to 5d792c1 Compare January 30, 2026 22:19

Trzyq0712 added 4 commits March 11, 2026 12:03

Make spec refinements with trait bounds work

1cb13ec

Progress

72d8924

Do not attach base post-conditions to refined ones

f4c6201

Correctly allow only one refine_spec

9db797a

Trzyq0712 force-pushed the spec_refinements branch from 5d792c1 to 9db797a Compare March 12, 2026 09:15

Clean up

e43b304

Trzyq0712 commented Mar 12, 2026

View reviewed changes

Trzyq0712 added 2 commits March 12, 2026 11:05

Clippy

0e56070

Add support for type projections in refine_spec

56d22ea

Trzyq0712 commented Mar 12, 2026

View reviewed changes

Trzyq0712 mentioned this pull request Mar 12, 2026

Support for const projections in refine_specs #147

Open

Aurel300 reviewed Mar 12, 2026

View reviewed changes

Trzyq0712 and others added 2 commits March 12, 2026 13:14

Fix wrong merge resolution

29b7646

Do not clone the pre/post conditions to refined ones

a1796da

This was never correct as it was processing order dependent.

JonasAlaif reviewed Mar 20, 2026

View reviewed changes

Trzyq0712 added 4 commits March 20, 2026 14:54

Create CallerBoundsEnc

65caecd

Implement the ClausesEnc

087a91a

Merge branch 'caller_bounds_enc' into spec_refinements

4bd1156

Use ClausesEnc to encode the refinement checks

5bcc82c

JonasAlaif reviewed Mar 20, 2026

View reviewed changes

Comment thread prusti-encoder/src/encoders/ty/generics/params.rs

Fix inheriting refined specs

50feee3

Trzyq0712 changed the title ~~Implement specification refinement using trait bounds~~ Specification refinement Mar 22, 2026

Trzyq0712 added 2 commits March 22, 2026 16:34

Use substitutions when encoding clauses

6413ff4

Clippy + fmt

4d3af5c

JonasAlaif reviewed Mar 25, 2026

View reviewed changes

Conversation

Trzyq0712 commented Jan 30, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Trzyq0712 commented Mar 9, 2026

Uh oh!

Aurel300 commented Mar 9, 2026

Uh oh!

Trzyq0712 commented Mar 9, 2026

Uh oh!

Trzyq0712 commented Mar 9, 2026

Uh oh!

Aurel300 commented Mar 9, 2026

Uh oh!

Trzyq0712 commented Mar 9, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Trzyq0712 commented Mar 9, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Trzyq0712 commented Mar 12, 2026

Uh oh!

Trzyq0712 commented Mar 12, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Aurel300 Mar 12, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

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!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Trzyq0712 commented Jan 30, 2026 •

edited

Loading

Trzyq0712 commented Mar 9, 2026 •

edited

Loading

Trzyq0712 commented Mar 9, 2026 •

edited

Loading

Trzyq0712 commented Mar 12, 2026 •

edited

Loading

Aurel300 Mar 12, 2026 •

edited

Loading