Add support for Opaque types defined by function returns #1785

FeizaiYiHao · 2025-06-26T23:20:10Z

This PR adds basic support for opaque types defined by function returns. The changes include:

In external.rs, all opaque type definitions are visited, and only opaque types under external functions are marked as VerifOrExternal::External , since the opaque type is part of the function declaration.
In lifetime check, all opaque types are normalized to concrete types.
In HIR to VIR:
- a new enum TypX::Opaque{def_path:Path,args:Typs} is added, in which the def_path is the path where the opaque type is defined. And args are the type parameters used to instantiate this instance of the opaque type.
- a new structOpaquetypeX{pub name: Path, pub typ_params: Typs, pub typ_bounds: GenericBounds,} is added for each opaque type definition. A KrateX carries a list of OpaquetypeX that are used in the crate.
in VIR to AIR
- each OpaquetypeX generates two functions DCR%path and TYPE%path (or consts if takes no args) that return a Dcr and Type for given args. And also generates a range of axioms to encode the trait bounds for the instantiated opaque types.
- for each instance of opaque type with args, we instantiate the opaque type by calling the DCR%path args and TYPE%path args functions.

If in opaque.rs we have the following Rust code

trait Tr{
    type Output;
}
impl<T> Tr for T{
    type Output = T;
}
fn foo<T>() -> impl Tr{
    true
}
fn bar(){
    let x = foo::<usize>();
    assert(x == x);
}

Produces the following z3 code

;; Opaque-Type-Constructors
(declare-fun DCR%opaque!foo.opaque0. (Dcr Type) Dcr)
(declare-fun TYPE%opaque!foo.opaque0. (Dcr Type) Type)
(assert
 (forall ((T&. Dcr) (T& Type)) (!
   (and
    (tr_bound%opaque!Tr. (DCR%opaque!foo.opaque0. T&. T&) (TYPE%opaque!foo.opaque0. T&.
      T&
    ))
    (sized (DCR%opaque!foo.opaque0. T&. T&))
   )
   :pattern ((DCR%opaque!foo.opaque0. T&. T&))
   :pattern ((TYPE%opaque!foo.opaque0. T&. T&))
   :qid internal_opaque__foo__opaque0_opaque_type_bound_definition
   :skolemid skolem_internal_opaque__foo__opaque0_opaque_type_bound_definition
)))

;; Function-Specs opaque::foo
(declare-fun ens%opaque!foo. (Dcr Type Poly) Bool)
(assert
 (forall ((T&. Dcr) (T& Type) (%return! Poly)) (!
   (= (ens%opaque!foo. T&. T& %return!) (has_type %return! (TYPE%opaque!foo.opaque0. T&.
      T&
   )))
   :pattern ((ens%opaque!foo. T&. T& %return!))
   :qid internal_ens__opaque!foo._definition
   :skolemid skolem_internal_ens__opaque!foo._definition
)))

;; Function-Def opaque::foo
;; ../examples/opaque.rs:16:1: 16:23 (#0)
(get-info :all-statistics)
(push)
 (declare-const T&. Dcr)
 (declare-const T& Type)
 (declare-const %return! Poly)
 (assert
  fuel_defaults
 )
 (assert
  (sized T&.)
 )
 (assert
  (not true)
 )
 (get-info :version)
 (set-option :rlimit 30000000)
 (check-sat)
 (set-option :rlimit 0)
(pop)

;; Function-Def opaque::bar
;; ../examples/opaque.rs:19:1: 19:9 (#0)
(get-info :all-statistics)
(push)
 (declare-const no%param Int)
 (declare-const tmp%1 Bool)
 (declare-const x@ Poly)
 (assert
  fuel_defaults
 )
 ;; assertion failed
 (declare-const %%location_label%%0 Bool)
 (assert
  (not (=>
    (ens%opaque!foo. $ USIZE x@)
    (=>
     (= tmp%1 (= x@ x@))
     (=>
      %%location_label%%0
      tmp%1
 )))))
 (get-info :version)
 (set-option :rlimit 30000000)
 (check-sat)
 (set-option :rlimit 0)
(pop)

This seems to also enable returning impl Fn().

TODO

Figure out where to do the well-form checks for OpaqueTy
There are a few places where the typing mode is changed from post-analysis to non_body_analysis to stop normalizing opaque types based on the body of the functions that define the opaque types. I'm not sure if I have changed all the right places.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

FeizaiYiHao · 2025-08-18T21:45:59Z

Passing all the tests now. I'm looking at all the usages of PostAnalysis...

source/rust_verify_test/tests/safe_api.rs

source/vir/src/ast.rs

source/vir/src/ast_util.rs

source/vir/src/ast_visitor.rs

source/vir/src/opaque_type_to_air.rs

source/vir/src/prune.rs

source/vir/src/sst_to_air.rs

source/rust_verify/src/external.rs

FeizaiYiHao · 2025-08-23T07:52:29Z

@tjhance fixed most of the things. Would you take another look? TY!

tjhance

This mostly looks good to me; with respect to the code, I only have some minor nitpicks.

The last main thing I would like to see is a few more tests regarding interacting features:

A function marked external_body which returns an opaque type.
An assume_specification for a function that returns an opaque type.
A function with a returns clause and which returns an opaque type.
A function with a returns clause and which returns an opaque type, and which is marked allow_in_spec

It's fine if some of these are "not implemented" errors, I mostly want to get tests in so it's clear what the expected behavior is in these cases.

source/rust_verify/src/external.rs

source/rust_verify/src/rust_to_vir_base.rs

FeizaiYiHao · 2025-08-30T14:25:00Z

@tjhance
external_body works with no problem.
assume_specification requires some additional checks for the trait bounds of the two OpaqueDefs from the external function and the assume_specification . Not sure if I did the right thing in compare_clasue_kind. Would you take a look?
returns will cause an error now. Not sure we should ever support it, since no way we can make the expression opaque?

FeizaiYiHao · 2025-09-14T03:45:22Z

@tjhance ping in case the email notification didn't work

tjhance

Sorry for the delay. This looks good to me.

Chris-Hawblitzel · 2025-07-07T16:38:17Z

source/vir/src/ast_visitor.rs

            TypX::ConstInt(_) => R::ret(|| typ.clone()),
            TypX::ConstBool(_) => R::ret(|| typ.clone()),
            TypX::Air(_) => R::ret(|| typ.clone()),
+            TypX::Opaque { .. } => R::ret(|| typ.clone()),


This needs to visit the args, like the TypX::Datatype and TypX::Primitive cases.

Chris-Hawblitzel · 2025-07-07T16:43:46Z

source/vir/src/ast.rs

+    pub typ_bounds: GenericBounds,
+}
+
+pub type Opaquetype = Arc<Spanned<OpaquetypeX>>;


Minor comment: OpaqueType would be better than Opaquetype, since it's two words (whereas "datatype" is often just one word).

parno · 2025-10-13T14:27:38Z

@FeizaiYiHao Is this ready to be merged?

FeizaiYiHao · 2025-10-13T15:05:53Z

@FeizaiYiHao Is this ready to be merged?

Wow sorry. Somehow the notification didn't work... Will quickly address the comments from @Chris-Hawblitzel and resolve the conflicts and then it should be good to be merged.

parno · 2025-10-13T15:17:07Z

Great, thanks!

…rojection types

…s in traits

… in opaque function

FeizaiYiHao · 2025-10-20T19:51:36Z

@parno Somehow the comments from Chirs were addressed a long time ago but the they poped out again in the threads. But anyways, this is ready to be merged. Sorry for the delay

FeizaiYiHao · 2025-10-30T00:24:30Z

I found an unhandled case: for nested opaque types, we are missing the equality statements in AIR generation. Let me quickly fix and push again. Sorry.

Example:

    trait DummyTrait{
        spec fn dummy_spec(&self) -> bool;
    }
    impl DummyTrait for bool{
        spec fn dummy_spec(&self) -> bool{
            true
        }
    }    
    async fn foo() -> (ret: (impl DummyTrait, impl DummyTrait))
        ensures
            ret.awaited() ==> [email protected]_spec(),
    {
        (true, true)
    }
    async fn bar() -> (ret:())
    {
        let future = foo();
        assert(future.awaited() ==> [email protected]_spec());
        let ret_0 = future.await.0;
        assert(ret_0.dummy_spec());
    }
    fn baz() -> (ret: impl Future<Output = (impl DummyTrait, impl DummyTrait)>)
        ensures
            ret.awaited() ==> [email protected]_spec(),
    {
        foo() // Here Z3 doesn't know that the Output type of baz()'s return value equals to Output type of foo()'s
    }

FeizaiYiHao · 2025-10-31T04:25:43Z

OK. fixed. Ready to be merged

FeizaiYiHao closed this Aug 11, 2025

FeizaiYiHao force-pushed the main branch from bacf54b to e8d43b8 Compare August 11, 2025 19:31

FeizaiYiHao reopened this Aug 12, 2025

FeizaiYiHao force-pushed the main branch from 9180656 to 4e34328 Compare August 15, 2025 21:44

FeizaiYiHao marked this pull request as draft August 15, 2025 21:45

FeizaiYiHao marked this pull request as ready for review August 18, 2025 21:44

dschoepe requested review from Chris-Hawblitzel and tjhance August 19, 2025 16:13

tjhance requested changes Aug 20, 2025

View reviewed changes

FeizaiYiHao force-pushed the main branch from 89ba132 to 6051a26 Compare August 23, 2025 07:42

tjhance requested changes Aug 26, 2025

View reviewed changes

source/rust_verify/src/external.rs Show resolved Hide resolved

source/rust_verify/src/rust_to_vir_base.rs Show resolved Hide resolved

FeizaiYiHao requested a review from tjhance September 2, 2025 02:46

tjhance approved these changes Sep 23, 2025

View reviewed changes

Chris-Hawblitzel approved these changes Sep 23, 2025

View reviewed changes

FeizaiYiHao added 9 commits October 20, 2025 09:50

Add support for Opaque types defined by function returns

9ebf310

update to rustc 1.88

334fe44

Set type for opaque function return value. Analysis typing mode for p…

b808dc8

…rojection types

catch up to new lifetime checks

c76391e

run vargo fmt

ac011fb

fix broken tests

7688900

fix external.rs for opaque types and add early checks for opaque type…

8430686

…s in traits

remove unused comments. Use helper function

7578407

add support for assume_spec for opaque types. throw error for returns…

fa35449

… in opaque function

rebase

e70af2f

FeizaiYiHao force-pushed the main branch from 01df125 to e70af2f Compare October 20, 2025 18:16

run fmt

c4c7d32

FeizaiYiHao added 4 commits October 22, 2025 02:23

recurse on nested return types

0f8d329

also recurse for sst to air

ca85605

remove

cb80437

recurse on nested opaque

97bf3a6

recurse on associate types

d1f880e

Add support for Opaque types defined by function returns #1785

Are you sure you want to change the base?

Add support for Opaque types defined by function returns #1785

Conversation

FeizaiYiHao commented Jun 26, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

TODO

Uh oh!

FeizaiYiHao commented Aug 18, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

FeizaiYiHao commented Aug 23, 2025

Uh oh!

tjhance left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

FeizaiYiHao commented Aug 30, 2025

Uh oh!

FeizaiYiHao commented Sep 14, 2025

Uh oh!

tjhance left a comment

Choose a reason for hiding this comment

Uh oh!

Chris-Hawblitzel Jul 7, 2025

Choose a reason for hiding this comment

Uh oh!

Chris-Hawblitzel Jul 7, 2025

Choose a reason for hiding this comment

Uh oh!

parno commented Oct 13, 2025

Uh oh!

FeizaiYiHao commented Oct 13, 2025

Uh oh!

parno commented Oct 13, 2025

Uh oh!

FeizaiYiHao commented Oct 20, 2025

Uh oh!

FeizaiYiHao commented Oct 30, 2025

Uh oh!

FeizaiYiHao commented Oct 31, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

FeizaiYiHao commented Jun 26, 2025 •

edited

Loading