axioms for has_resolved (#1857)

Author: tjhance

source/rust_verify/src/fn_call_to_vir.rs

@@ -1606,9 +1606,9 @@ fn verus_item_to_vir<'tcx, 'a>(
                 format!("this builtin item should not appear in user code",),
             );
         }
-        VerusItem::Resolve | VerusItem::HasResolved => {
+        VerusItem::Resolve | VerusItem::HasResolved | VerusItem::HasResolvedUnsized => {
             if !bctx.ctxt.cmd_line_args.new_mut_ref {
-                unsupported_err!(expr.span, "resolved/resolved without '-V new-mut-ref'", &args);
+                unsupported_err!(expr.span, "resolve/has_resolved without '-V new-mut-ref'", &args);
             }
             if matches!(verus_item, VerusItem::Resolve) {
                 record_compilable_operator(bctx, expr, CompilableOperator::Resolve);
@@ -1619,7 +1619,7 @@ fn verus_item_to_vir<'tcx, 'a>(
                 if matches!(verus_item, VerusItem::Resolve) {
                     return err_span(expr.span, "resolve must be in a 'proof' block");
                 } else {
-                    return err_span(expr.span, "resolved must be in a 'proof' block");
+                    return err_span(expr.span, "has_resolved must be in a 'proof' block");
                 }
             }
             let exp = expr_to_vir(bctx, &args[0], ExprModifier::REGULAR)?;

source/rust_verify/src/verifier.rs

@@ -1941,15 +1941,22 @@ impl Verifier {
             reporter
                 .report_now(&note_bare(format!("verifying {bucket_name}{functions_msg}")).to_any());
         }
-        let (pruned_krate, mono_abstract_datatypes, spec_fn_types, used_builtins, fndef_types) =
-            vir::prune::prune_krate_for_module_or_krate(
-                &krate,
-                &Arc::new(self.crate_name.clone().expect("crate_name")),
-                None,
-                Some(bucket_id.module().clone()),
-                bucket_id.function(),
-                true,
-            );
+        let (
+            pruned_krate,
+            mono_abstract_datatypes,
+            spec_fn_types,
+            used_builtins,
+            fndef_types,
+            resolved_typs,
+        ) = vir::prune::prune_krate_for_module_or_krate(
+            &krate,
+            &Arc::new(self.crate_name.clone().expect("crate_name")),
+            None,
+            Some(bucket_id.module().clone()),
+            bucket_id.function(),
+            true,
+            true,
+        );
         let mono_abstract_datatypes = mono_abstract_datatypes.unwrap();
         let module = pruned_krate
             .modules
@@ -1965,6 +1972,7 @@ impl Verifier {
             spec_fn_types,
             used_builtins,
             fndef_types,
+            resolved_typs.unwrap(),
             self.args.debugger,
         )?;
         if self.args.log_all || self.args.log_args.log_vir_poly {
@@ -2754,13 +2762,14 @@ impl Verifier {
         vir_crates.push(vir_crate);
         let unpruned_crate =
             vir::ast_simplify::merge_krates(vir_crates).map_err(map_err_diagnostics)?;
-        let (vir_crate, _, _, _, _) = vir::prune::prune_krate_for_module_or_krate(
+        let (vir_crate, _, _, _, _, _) = vir::prune::prune_krate_for_module_or_krate(
             &unpruned_crate,
             &Arc::new(crate_name.clone()),
             Some(&current_vir_crate),
             None,
             None,
             false,
+            false,
         );
         let vir_crate =
             vir::traits::merge_external_traits(vir_crate).map_err(map_err_diagnostics)?;

source/rust_verify/src/verus_items.rs

@@ -376,6 +376,7 @@ pub(crate) enum VerusItem {
     External(ExternalItem),
     Resolve,
     HasResolved,
+    HasResolvedUnsized,
     MutRefCurrent,
     MutRefFuture,
     ErasedGhostValue,
@@ -587,6 +588,7 @@ fn verus_items_map() -> Vec<(&'static str, VerusItem)> {
         ("verus::verus_builtin::RqEn",             VerusItem::External(ExternalItem::RqEn)),
         ("verus::verus_builtin::resolve",          VerusItem::Resolve),
         ("verus::verus_builtin::has_resolved",     VerusItem::HasResolved),
+        ("verus::verus_builtin::has_resolved_unsized",     VerusItem::HasResolvedUnsized),
         ("verus::verus_builtin::mut_ref_current",  VerusItem::MutRefCurrent),
         ("verus::verus_builtin::mut_ref_future",   VerusItem::MutRefFuture),
     ]

source/rust_verify_test/tests/mut_refs.rs

@@ -4,14 +4,8 @@ mod common;
 use common::*;
 
 test_verify_one_file_with_options! {
-    #[test] test_basic ["new-mut-ref", "--no-lifetime"] => verus_code! {
-        broadcast axiom fn resolved_defn<T>(a: &mut T)
-            ensures
-                #[trigger] has_resolved(a) ==> mut_ref_current(a) == mut_ref_future(a);
-
+    #[test] test_basic ["new-mut-ref"] => verus_code! {
         fn test_no_update() {
-            broadcast use resolved_defn;
-
             let mut u: u64 = 20;
             let u_ref: &mut u64 = &mut u;
 
@@ -21,8 +15,6 @@ test_verify_one_file_with_options! {
         }
 
         fn test_basic_update() {
-            broadcast use resolved_defn;
-
             let mut u: u64 = 20;
             let u_ref: &mut u64 = &mut u;
 
@@ -36,8 +28,6 @@ test_verify_one_file_with_options! {
         struct Pair<A, B>(A, B);
 
         fn test_field_update() {
-            broadcast use resolved_defn;
-
             let mut u: Pair<u64, u64> = Pair(20, 20);
             let u_ref: &mut Pair<u64, u64> = &mut u;
 
@@ -50,8 +40,6 @@ test_verify_one_file_with_options! {
         }
 
         fn test_field_update2() {
-            broadcast use resolved_defn;
-
             let mut u: Pair<u64, u64> = Pair(20, 20);
             let u_ref: &mut u64 = &mut u.0;
 
@@ -64,21 +52,21 @@ test_verify_one_file_with_options! {
         }
 
         fn test_mut_ref_in_pair() {
-            broadcast use resolved_defn;
-
             let mut u: u64 = 20;
             let u_ref: Pair<&mut u64, u64> = Pair(&mut u, 70);
 
             *u_ref.0 = 30;
 
-            proof { resolve(u_ref.0) }
+            proof {
+                resolve(u_ref);
+                assert(has_resolved(u_ref));
+                assert(has_resolved(u_ref.0));
+            }
 
             assert(u == 30);
         }
 
         fn test_reborrow() {
-            broadcast use resolved_defn;
-
             let mut u: u64 = 20;
             let u_ref: &mut u64 = &mut u;
 
@@ -105,7 +93,7 @@ test_verify_one_file_with_options! {
 }
 
 test_verify_one_file_with_options! {
-    #[test] test_spec_functions_ok ["new-mut-ref", "--no-lifetime"] => verus_code! {
+    #[test] test_spec_functions_ok ["new-mut-ref"] => verus_code! {
         spec fn test<T>(x: &mut T) -> T {
             mut_ref_current(x)
         }
@@ -123,17 +111,132 @@ test_verify_one_file_with_options! {
 }
 
 test_verify_one_file_with_options! {
-    #[test] test_mut_ref_future_proph ["new-mut-ref", "--no-lifetime"] => verus_code! {
+    #[test] test_mut_ref_future_proph ["new-mut-ref"] => verus_code! {
         spec fn test<T>(x: &mut T) -> T {
             mut_ref_future(x)
         }
     } => Err(err) => assert_vir_error_msg(err, "cannot use prophecy-dependent function `mut_ref_future` in prophecy-independent context")
 }
 
 test_verify_one_file_with_options! {
-    #[test] test_resolved_proph ["new-mut-ref", "--no-lifetime"] => verus_code! {
+    #[test] test_resolved_proph ["new-mut-ref"] => verus_code! {
         spec fn test<T>(x: &mut T) -> bool {
             has_resolved(x)
         }
     } => Err(err) => assert_vir_error_msg(err, "cannot use prophecy-dependent predicate `has_resolved` in prophecy-independent context")
 }
+
+test_verify_one_file_with_options! {
+    #[test] test_resolved_axioms ["new-mut-ref"] => verus_code! {
+        use vstd::prelude::*;
+
+        proof fn test_pair<A, B>(pair: (A, B)) {
+            assert(has_resolved(pair) ==> has_resolved(pair.0));
+            assert(has_resolved(pair) ==> has_resolved(pair.1));
+        }
+
+        proof fn test_option<A>(opt: Option<A>) {
+            match opt {
+                Some(o) => {
+                    assert(has_resolved(opt) ==> has_resolved(o));
+                }
+                None => { }
+            }
+        }
+
+        struct Pair<A, B> {
+            x: A,
+            y: B,
+        }
+
+        proof fn test_pair_struct<A, B>(pair: Pair<A, B>) {
+            assert(has_resolved(pair) ==> has_resolved(pair.x));
+            assert(has_resolved(pair) ==> has_resolved(pair.y));
+        }
+
+        proof fn test_box<A>(b: Box<A>) {
+            assert(has_resolved(b) ==> has_resolved(*b));
+        }
+
+        proof fn test_tracked<A>(t: Tracked<A>) {
+            assert(has_resolved(t) ==> has_resolved(t@));
+        }
+
+        proof fn test_ghost_fail<A>(t: Ghost<A>) {
+            assert(has_resolved(t) ==> has_resolved(t@)); // FAILS
+        }
+
+        proof fn test_ref_fail<A>(t: &A) {
+            assert(has_resolved(t) ==> has_resolved(*t)); // FAILS
+        }
+
+        proof fn test_rc_fail<A>(t: std::rc::Rc<A>) {
+            assert(has_resolved(t) ==> has_resolved(*t)); // FAILS
+        }
+
+        proof fn test_arc_fail<A>(t: std::sync::Arc<A>) {
+            assert(has_resolved(t) ==> has_resolved(*t)); // FAILS
+        }
+
+        proof fn test_mut_ref<A>(t: &mut A) {
+            assert(has_resolved(t) ==> mut_ref_current(t) == mut_ref_future(t));
+        }
+
+        proof fn test_mut_ref_fail<A>(t: &mut A) {
+            assert(has_resolved(t) ==> has_resolved(mut_ref_current(t))); // FAILS
+        }
+
+        proof fn test_mut_ref_fail2<A>(t: &mut A) {
+            assert(has_resolved(t) ==> has_resolved(mut_ref_future(t))); // FAILS
+        }
+    } => Err(err) => assert_fails(err, 6)
+}
+
+test_verify_one_file_with_options! {
+    #[test] test_resolve_axioms_in_context ["new-mut-ref"] => verus_code! {
+        use vstd::prelude::*;
+
+        fn box_with_mut_ref() {
+            let mut x: u64 = 0;
+
+            let x_ref = &mut x;
+            let x_ref_box = Box::new(x_ref);
+
+            **x_ref_box = 13;
+
+            proof { resolve(x_ref_box); }
+
+            assert(x == 13);
+        }
+
+        fn shr_ref_with_mut_ref() {
+            let mut x: u64 = 0;
+
+            let x_ref = &mut x;
+            let x_ref_ref = &x_ref;
+
+            proof { resolve(x_ref_ref); }
+
+            assert(has_resolved(x_ref)); // FAILS
+
+            *x_ref = 20;
+            proof { resolve(x_ref); }
+        }
+
+        fn mut_ref_with_mut_ref() {
+            let mut x: u64 = 0;
+
+            let mut x_ref = &mut x;
+            let x_ref_ref = &mut x_ref;
+
+            **x_ref_ref = 20;
+
+            proof { resolve(x_ref_ref); }
+
+            assert(has_resolved(x_ref)); // FAILS
+
+            *x_ref = 30;
+            proof { resolve(x_ref); }
+        }
+    } => Err(err) => assert_fails(err, 2)
+}

source/vir/src/context.rs

@@ -87,6 +87,7 @@ pub struct Ctx {
     pub(crate) spec_fn_types: Vec<usize>,
     pub(crate) used_builtins: crate::prune::UsedBuiltins,
     pub(crate) fndef_types: Vec<Fun>,
+    pub(crate) resolved_typs: Vec<crate::resolve_axioms::ResolvableType>,
     pub(crate) fndef_type_set: HashSet<Fun>,
     pub functions: Vec<Function>,
     pub func_map: HashMap<Fun, Function>,
@@ -713,6 +714,7 @@ impl Ctx {
         spec_fn_types: Vec<usize>,
         used_builtins: crate::prune::UsedBuiltins,
         fndef_types: Vec<Fun>,
+        resolved_typs: Vec<crate::resolve_axioms::ResolvableType>,
         debug: bool,
     ) -> Result<Self, VirErr> {
         let mut datatype_is_transparent: HashMap<Dt, bool> = HashMap::new();
@@ -758,6 +760,7 @@ impl Ctx {
             spec_fn_types,
             used_builtins,
             fndef_types,
+            resolved_typs,
             fndef_type_set,
             functions,
             func_map,

source/vir/src/datatype_to_air.rs

@@ -828,6 +828,8 @@ pub fn datatypes_and_primitives_to_air(ctx: &Ctx, datatypes: &crate::ast::Dataty
         vec![]
     };
 
+    let resolve_axiom_commands = crate::resolve_axioms::resolve_axioms(ctx);
+
     let mut commands: Vec<Command> = Vec::new();
     commands.extend(pointee_metadata_commands);
     commands.append(&mut opaque_sort_commands);
@@ -840,5 +842,6 @@ pub fn datatypes_and_primitives_to_air(ctx: &Ctx, datatypes: &crate::ast::Dataty
     commands.append(&mut axiom_commands);
     commands.extend(array_commands);
     commands.extend(strslice_commands);
+    commands.extend(resolve_axiom_commands);
     Arc::new(commands)
 }

source/vir/src/lib.rs

@@ -58,6 +58,7 @@ pub mod printer;
 pub mod prune;
 pub mod recursion;
 pub mod recursive_types;
+mod resolve_axioms;
 pub mod safe_api;
 mod scc;
 pub mod sst;

source/vir/src/poly.rs

@@ -606,7 +606,7 @@ fn visit_exp(ctx: &Ctx, state: &mut State, exp: &Exp) -> Exp {
                 }
                 UnaryOpr::HasResolved(_t) => {
                     let e = coerce_exp_to_poly(ctx, &e1);
-                    mk_exp_typ(&e1.typ, ExpX::UnaryOpr(op.clone(), e.clone()))
+                    mk_exp(ExpX::UnaryOpr(op.clone(), e.clone()))
                 }
             }
         }
@@ -745,6 +745,17 @@ fn visit_trigs(ctx: &Ctx, state: &mut State, trigs: &Trigs) -> Trigs {
     Arc::new(trigs.iter().map(|e| visit_exps(ctx, state, e)).collect())
 }
 
+pub(crate) fn visit_exp_native_for_pure_exp(ctx: &Ctx, exp: &Exp) -> Exp {
+    let mut state = State {
+        remaining_temps: HashSet::new(),
+        types: ScopeMap::new(),
+        temp_types: HashMap::new(),
+        is_trait: false,
+        in_exec_closure: false,
+    };
+    visit_exp_native(ctx, &mut state, exp)
+}
+
 fn take_temp(state: &mut State, dest: &Dest) -> Option<VarIdent> {
     if dest.is_init {
         if let ExpX::VarLoc(x) = &dest.dest.x {