(WIP) Trait specs by Aurel300 · Pull Request #127 · Aurel300/prusti-dev

Aurel300 · 2026-01-26T19:15:28Z

For each trait:

const generics
For each of its associated functions (with or without a default impl):
- symbolic/abstract pre, post functions
- same for pledges
- (later?) separate functions to combine the full base pre/postconditions
- axioms to connect symbolic functions to base specs
- stub method which uses symbolic functions
- pure functions
For associated functions with a default implementation:
- method to show the base specs hold for this implementation
  - (method emitted, make sure base specs are used)

For each trait impl:

const generics
For each associated function (with a refined spec?)
- axioms to connect symbolic functions to refined specs
- methods to verify behavioural subtyping holds (separate for pre, post, pledges for precise error tracking)
- method to show the refined? specs hold for this implementation
  - (method emitted, but need to use refined specs)

If using generic encoding:

call stub method instead of trait method
pure functions?

If monomorphising (which gets us better error tracking):

try to resolve calls https://doc.rust-lang.org/stable/nightly-rustc/rustc_middle/ty/struct.Instance.html#method.try_resolve

Aurel300 · 2026-02-24T15:44:26Z

There is one regression related to generics (not providing the correct substs, somewhere?). @JonasAlaif can you have a look at the overall structure in traits.rs and trait_impls.rs in particular? Feel free to ignore cosmetics, formatting, etc, for now.

JonasAlaif

I didn't fully go through everything, but for now these changes should make things nicer and then I can go through the rest

JonasAlaif · 2026-02-27T10:19:27Z

    type TaskDescription<'tcx> = (
        DefId, // The function annotated with specs
-        bool,  // If to encode as pure or not
+        DefId, // Context, i.e., where the specs are emitted


All uses pass in the same DefId for both? It also doesn't make sense to have a different spec from the point of view of different contexts? Let's remove the second DefId?

This is needed to encode the behavioural subtyping checks: in the proof methods, we need to check the contract of the trait from the context of the implementor, i.e., we need to instantiate the contract with the correct TraitRef substitutions applied.

Where is that? When I find all uses of MirSpecEnc it always takes the exact same two DefIds as input (i.e. (def_id, def_id, ...))

prusti-dev/prusti-encoder/src/encoders/ty/generics/trait_impls.rs

Line 280 in df298b2

(trait_item_def_id, impl_item_def_id, MirSpecEncMode::Impure),

Ah ok, sorry yeah.

we need to instantiate the contract with the correct TraitRef substitutions applied

So you mean casting to concrete/generic correctly? It still seems like a lot of extra complication in MirSpecEnc for this one case - could we not add something like a MirSpecUseEnc wrapper that provides an api with the casts applied as necessary?

JonasAlaif · 2026-02-27T10:49:02Z

    for def_id in tcx.hir_crate_items(()).definitions() {
-        if let hir::def::DefKind::Impl { of_trait: true } = tcx.def_kind(def_id) {
-            TraitImplEnc::encode(def_id.to_def_id(), false).unwrap();
+        match tcx.def_kind(def_id) {


We should think about if these are necessary (since we're also skipping all the traits defined outside this crate anyway). Or do we need this to check behavioural subtyping? In #137 the hir::def::DefKind::Impl case is removed, since the TraitEnc goes through all impls anyway.

Yes, TraitImplEnc causes the behavioural subtyping checks to be emitted. Any crate can define:

types
We don't have to force the encoding of a type if it appears in a crate but doesn't get used; though it would be surprising from a Prusti user perspective if a type that causes Prusti to error out only does this when verifying a downstream crate that uses that type.

traits
When there are method bodies, we already encode them (it is a body owner in the crate). For methods without a default implementation, we should make sure the specs are well-formed, which will happen in (WIP) Encode spec items as methods #138. Associated types etc probably don't matter much when the trait is not used.

trait impl blocks connecting (sets of) types to traits, where either the type or the trait may be coming from an upstream crate
Here we should emit the behavioural subtyping check, and it shouldn't be pushed to downstream crates, i.e., iterating through all known impls (as in Concrete trait impl checks #137) seems wrong to me here.

JonasAlaif · 2026-02-27T10:54:07Z

                                substs,
                                // TODO: should this be `def_id` or `caller_def_id`
-                                caller_def_id: Some(def_id),
+                                caller_def_id: Some(context_def_id),


We should have a deep think about if this caller_def_id is necessary. Maybe there should be a MirPureUseEnc which does all the required casting of arguments to/from generic?

Ok I guess this is ultimately a question of whether we want to trust that our encoding of generics will lead to the same results as rustc monomorphisation. A different caller_def_ids here will cause MirPureEnc to request a different body monomorphisation, which eventually affects the choice of the typing environment here:

prusti-dev/prusti-interface/src/environment/body.rs

Line 174 in 60ee0c0

let typing_env = TypingEnv::post_analysis(self.tcx, caller_def_id.unwrap_or(def_id));

(Which can then change whether we know a particular associated type resolves to a concrete type, for example.)

Either way I would prefer to postpone this to after this PR.

Aurel300 · 2026-03-02T12:16:35Z

Ok so this causes a cycle:

trait Bar {
    type Target;
    fn deref(x: Self::Target);
}

And of course it would -- in trying to create the function identifier for deref, we need to already have a way to refer to the associated type (and it's a different encoder, MirLocalDefEnc, that's actually responsible for creating the types for the variables).

So as you suggested at some point @JonasAlaif I think I need to change this to have a separate encoder for the trait itself (its impl_* function, its associated types) and one for trait methods and functions.

Aurel300 · 2026-03-04T15:57:11Z

Merged to unblock other PRs, in particular #137.

* Trait impl check for simple types * Trait impl check for unknown types * Change the encoding to use exists clauses * Fix impl_unknown to contain the trait generics * Include the check for the unknown type in the impl function * Encode trait bound requirements * Emit early impl_fun ref to avoid dependency cycles * Modify encoding to avoid using existentials * Clean up the type check encoding function * Clean up of the impl_fun_body * Fix wrong encoding of trait generic arguments * Add corrected trait bound checks * Remove existential from unknown type check * Add initial special encoding for the `Sized` trait * Add const generics to trait impl function defs * Implement handling of const generics in trait impls * Correctly handle concretely valued const generics * Implement the Sized check without opaque and unknown * Move sizedness resolution to RustTy * Add unknown type check for the sized trait * Make sizedness check work in general case * Initial trait associated type predicates * Const generics in trait impls * Remove full dep output for trait encoder * Make assoc const Snap + more assoc type bound cases * Discover generics inside projection terms * Fix GATs * Clean up the implementation * Collect const generics from projections * Naming consistency fix * Remove a dbg Co-authored-by: Aurea <Aurel300@users.noreply.github.com> * Integrate context erasure for types into `identity_for_ty` * Resolve some issues and clean up in `rust_ty.rs` * Revert unnecessary change * Add support of checking sizedness of aliases * Move trait impl check to impl encoder * Seperate encoder for the sized trait * Remove type aliases * Skip emitting local output for `Sized` trait * Clippy * Revert some unnecessary changes * Match parts of trait_impls with #127 * Remove unnecessary rename * Omit dependent sizedness check if it is known to be sized * Revert unnecessary change * Cleanup, restructuring and renaming The main change is to use proper visibility attributes for the various defined functions and to put these functions in an `impl` of an associated struct (code style in Prusti) * Emit the domain for the Sized trait * Correctly implement the `Alias` case of `ty_expr` * Simplify the task for SizedTraitEnc * Add optional suffix for generics renaming * Simplified clauses encoding prototype * Let binding encoding * Clean up trait impl check * Simplify encoding of Sized * Remove sizedness from `RustTy` * Merge imports * Remove unnecessary changes in `TyConstructorEnc` * Return `Result`s instead of unwrapping to avoid cyclic errors * Move trait check into an `ensures` instead of the body * Accessor for the `erased_ty` * Clippy * fmt * Fix type erasure for closures * Update the erased_ty accessor * Use trait enc output for encoding sized * Remove Sized trait implementation * Revert unnecessary changes * Use FxIndexMap instead * Revert returning result to avoid unwrap * More cleanup * Fix compile * Simplify * Fix missing quantification over consts * Add trigger system to encode `impl` only when needed * Change algo for `order_projections` * Pass proper `args` to `is_function_pure` * Use `FxIndexMap` * Update comments * Additionally gate on trait arguments of an `impl` * Construct balanced tree for `conj`/`disj` to limit ast depth * Properly handle `context` in `mir_shared` --------- Co-authored-by: Aurea <Aurel300@users.noreply.github.com> Co-authored-by: Jonáš Fiala <jonas.fiala@inf.ethz.ch>

* Trait impl check for simple types * Trait impl check for unknown types * Change the encoding to use exists clauses * Fix impl_unknown to contain the trait generics * Include the check for the unknown type in the impl function * Encode trait bound requirements * Emit early impl_fun ref to avoid dependency cycles * Modify encoding to avoid using existentials * Clean up the type check encoding function * Clean up of the impl_fun_body * Fix wrong encoding of trait generic arguments * Add corrected trait bound checks * Remove existential from unknown type check * Add initial special encoding for the `Sized` trait * Add const generics to trait impl function defs * Implement handling of const generics in trait impls * Correctly handle concretely valued const generics * Implement the Sized check without opaque and unknown * Move sizedness resolution to RustTy * Add unknown type check for the sized trait * Make sizedness check work in general case * Initial trait associated type predicates * Const generics in trait impls * Remove full dep output for trait encoder * Make assoc const Snap + more assoc type bound cases * Discover generics inside projection terms * Fix GATs * Clean up the implementation * Collect const generics from projections * Naming consistency fix * Remove a dbg Co-authored-by: Aurea <Aurel300@users.noreply.github.com> * Integrate context erasure for types into `identity_for_ty` * Resolve some issues and clean up in `rust_ty.rs` * Revert unnecessary change * Add support of checking sizedness of aliases * Move trait impl check to impl encoder * Seperate encoder for the sized trait * Remove type aliases * Skip emitting local output for `Sized` trait * Clippy * Revert some unnecessary changes * Match parts of trait_impls with Aurel300#127 * Remove unnecessary rename * Omit dependent sizedness check if it is known to be sized * Revert unnecessary change * Cleanup, restructuring and renaming The main change is to use proper visibility attributes for the various defined functions and to put these functions in an `impl` of an associated struct (code style in Prusti) * Emit the domain for the Sized trait * Correctly implement the `Alias` case of `ty_expr` * Simplify the task for SizedTraitEnc * Add optional suffix for generics renaming * Simplified clauses encoding prototype * Let binding encoding * Clean up trait impl check * Simplify encoding of Sized * Remove sizedness from `RustTy` * Merge imports * Remove unnecessary changes in `TyConstructorEnc` * Return `Result`s instead of unwrapping to avoid cyclic errors * Move trait check into an `ensures` instead of the body * Accessor for the `erased_ty` * Clippy * fmt * Fix type erasure for closures * Update the erased_ty accessor * Use trait enc output for encoding sized * Remove Sized trait implementation * Revert unnecessary changes * Use FxIndexMap instead * Revert returning result to avoid unwrap * More cleanup * Fix compile * Simplify * Fix missing quantification over consts * Add trigger system to encode `impl` only when needed * Change algo for `order_projections` * Pass proper `args` to `is_function_pure` * Use `FxIndexMap` * Update comments * Additionally gate on trait arguments of an `impl` * Construct balanced tree for `conj`/`disj` to limit ast depth * Properly handle `context` in `mir_shared` --------- Co-authored-by: Aurea <Aurel300@users.noreply.github.com> Co-authored-by: Jonáš Fiala <jonas.fiala@inf.ethz.ch>

Aurel300 commented Jan 29, 2026

View reviewed changes

Comment thread prusti-interface/src/specs/specifications.rs

Aurel300 commented Jan 30, 2026

View reviewed changes

Comment thread prusti-encoder/src/encoders/ty/kinds/immref.rs Outdated

Aurel300 force-pushed the feature/trait-specs branch from 21e3688 to a7c4fb4 Compare February 2, 2026 12:23

Aurel300 added 23 commits February 24, 2026 15:11

shuffle assockind handler a bit

e9bae59

emit symbolic pre/post functions for traits

ba662a1

axioms to connect trait symbolic pre/post to base specs

6c0d121

emit stub method for trait fns

e1a9e20

shuffle trait impl encoder a bit

2728a5d

call stub method, use refined specs for impl

b5af668

trait impl axioms

ab881c7

use Self when emitting outputs in encoders

7cb2f60

fix find_trait_method_substs

6452663

allow spec encoder to encode relative to a caller context

d3baf44

emit methods to check behavioural subtyping

a0168e5

allow encoding postcondition specs without access to function result

f608567

use correct substs when encoding locals even without a body

5bd4841

always emit trait definitions when present in the crate

4fdcb1a

require param encoding when emitting ref encoding

6e5c820

don't try to encode body of pure fns without a body

4250984

use decompose to force s_Param encoding in immref

d624a60

handle const generics in trait impls

dbc6a33

minor, separate pure and impure call stubs

dca2e8b

pure functions in traits

a176c54

fmt, clippy

cee57a4

resolve cyclic dependencies

815d75a

cast correctly in trait spec axioms

c7e9910

Aurel300 force-pushed the feature/trait-specs branch from 9afce0c to c7e9910 Compare February 24, 2026 14:12

Aurel300 mentioned this pull request Feb 24, 2026

(WIP) Encode spec items as methods #138

Draft

2 tasks

Aurel300 requested a review from JonasAlaif February 24, 2026 15:44

Aurel300 mentioned this pull request Feb 24, 2026

Concrete trait impl checks #137

Merged

5 tasks

more generics issues

33a3966

Trzyq0712 added a commit to Trzyq0712/prusti-dev that referenced this pull request Feb 26, 2026

Match parts of trait_impls with Aurel300#127

1cfc892

JonasAlaif added 2 commits February 27, 2026 11:37

Extract trait_call logic

1dcc6d3

Clean up FunctionEnc

294721d

JonasAlaif force-pushed the feature/trait-specs branch from 5c9a842 to 294721d Compare February 27, 2026 10:46

JonasAlaif marked this pull request as ready for review February 27, 2026 10:57

JonasAlaif added 6 commits February 27, 2026 11:59

Correctly implement the Alias case of ty_expr

8662e30

Merge branch 'rewrite-2023' into feature/trait-specs

833c840

Replace get + unwrap with indexing

c5a96a3

Cleanup trait_impls.rs and bugfix

a457e52

Replace get + unwrap with indexing in other places

fdaba1d

Fix mess with GArgs in trait_impls.rs

df298b2

JonasAlaif requested changes Feb 27, 2026

View reviewed changes

Aurel300 added 4 commits March 2, 2026 16:09

separate out trait function encoder

164d70c

use context DefId for the typing env in local defs enc

60ee0c0

address comments

77b24f0

fmt

d02d14c

Aurel300 merged commit d23d931 into rewrite-2023 Mar 4, 2026
5 of 7 checks passed

Conversation

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

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Aurel300 commented Feb 24, 2026

Uh oh!

JonasAlaif left a comment

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!

JonasAlaif Feb 27, 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!

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!

Uh oh!

Uh oh!

Uh oh!

Aurel300 commented Mar 2, 2026

Uh oh!

Uh oh!

Aurel300 commented Mar 4, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Aurel300 commented Jan 26, 2026 •

edited

Loading

JonasAlaif Feb 27, 2026 •

edited

Loading