fix a number of duplicate qid (#2782)

Author: ahuoguo

source/vir/src/assoc_types_to_air.rs

@@ -11,6 +11,7 @@
 //!   (View::V (Vec A)) == (Seq (View::V A))
 
 use crate::ast::{AssocTypeImpl, AssocTypeImplX, Trait};
+use crate::ast_util::path_as_friendly_rust_name;
 use crate::context::Ctx;
 use crate::def::QID_ASSOC_TYPE_IMPL;
 use crate::sst_to_air::typ_to_ids;
@@ -50,7 +51,7 @@ pub fn assoc_type_impls_to_air(ctx: &Ctx, assocs: &Vec<AssocTypeImpl>) -> Comman
     for assoc in assocs {
         let AssocTypeImplX {
             name,
-            impl_path: _,
+            impl_path,
             typ_params,
             typ_bounds,
             trait_path,
@@ -86,7 +87,13 @@ pub fn assoc_type_impls_to_air(ctx: &Ctx, assocs: &Vec<AssocTypeImpl>) -> Comman
             let projection = ident_apply(&projector, &args);
             let typ_id = typ_to_ids(ctx, &typ)[index].clone();
             let eq = mk_eq(&projection, &typ_id);
-            let qname = format!("{}_{}_{}", projector, QID_ASSOC_TYPE_IMPL, decoration);
+            let qname = format!(
+                "{}_{}_{}_{}",
+                projector,
+                path_as_friendly_rust_name(impl_path),
+                QID_ASSOC_TYPE_IMPL,
+                decoration
+            );
             let mut trigs = vec![projection];
             for extra_trigger_term in extra_trigger_terms.iter() {
                 trigs.push(crate::sst_to_air::typ_to_id(ctx, extra_trigger_term));

source/vir/src/prelude.rs

@@ -262,8 +262,8 @@ pub(crate) fn prelude_nodes(name_ctxt: &NameCtxt, config: PreludeConfig) -> Vec<
                 (has_type ([mut_ref_future] m) t)
             )
             :pattern ((has_type m (MUTREF d t)) ([mut_ref_future] m))
-            :qid prelude_mut_ref_current_has_type
-            :skolemid skolem_prelude_mut_ref_current_has_type
+            :qid prelude_mut_ref_future_has_type
+            :skolemid skolem_prelude_mut_ref_future_has_type
         )))
         (axiom (forall ((m [Poly]) (d [decoration]) (t [typ]) (arg [Poly])) (!
             (=>
@@ -475,8 +475,8 @@ pub(crate) fn prelude_nodes(name_ctxt: &NameCtxt, config: PreludeConfig) -> Vec<
                 (= x ([box_int] ([unbox_int] x)))
             )
             :pattern (([has_type] x ([type_id_float] bits)))
-            :qid prelude_box_unbox_sint
-            :skolemid skolem_prelude_box_unbox_sint
+            :qid prelude_box_unbox_float
+            :skolemid skolem_prelude_box_unbox_float
         )))
         (axiom (forall ((x [Poly])) (!
             (=>
@@ -680,8 +680,8 @@ pub(crate) fn prelude_nodes(name_ctxt: &NameCtxt, config: PreludeConfig) -> Vec<
                 ([has_type] ([box_int] x) ([type_id_float] bits))
             )
             :pattern (([has_type] ([box_int] x) ([type_id_float] bits)))
-            :qid prelude_has_type_sint
-            :skolemid skolem_prelude_has_type_sint
+            :qid prelude_has_type_float
+            :skolemid skolem_prelude_has_type_float
         )))
         (axiom (forall ((x Int)) (!
             (=>
@@ -743,8 +743,8 @@ pub(crate) fn prelude_nodes(name_ctxt: &NameCtxt, config: PreludeConfig) -> Vec<
                 ([u_inv] bits ([unbox_int] x))
             )
             :pattern (([has_type] x ([type_id_float] bits)))
-            :qid prelude_unbox_sint
-            :skolemid skolem_prelude_unbox_sint
+            :qid prelude_unbox_float
+            :skolemid skolem_prelude_unbox_float
         )))
 
         // With smt.arith.nl=false, Z3 sometimes fails to prove obvious formulas

source/vir/src/resolve_axioms.rs

@@ -207,8 +207,8 @@ pub fn resolve_decoration_axiom(dec: &TypDecoration) -> Node {
                         ([resolved] d t x)
                     )
                     :pattern (([resolved] ([decorate_box] d1 t1 d) t x))
-                    :qid prelude_resolved_tracked_decoration
-                    :skolemid skolem_prelude_resolved_tracked_decoration
+                    :qid prelude_resolved_box_decoration
+                    :skolemid skolem_prelude_resolved_box_decoration
                 )))
             )
         }

source/vir/src/sst_to_air_func.rs

@@ -115,6 +115,7 @@ pub(crate) fn func_def_args(ctx: &Ctx, typ_params: &Idents, params: &Pars) -> Ve
 fn func_def_quant(
     ctx: &Ctx,
     name: &Ident,
+    qid_name: &Ident,
     is_trait_default_ensures: bool,
     typ_params: &Idents,
     typ_args: &Typs,
@@ -144,7 +145,7 @@ fn func_def_quant(
         trigs.push(crate::sst_to_air::typ_to_id(ctx, extra_trigger_term));
     }
     Ok(mk_bind_expr(
-        &func_bind_trig(ctx, name.to_string(), typ_params, params, &trigs, opts),
+        &func_bind_trig(ctx, qid_name.to_string(), typ_params, params, &trigs, opts),
         &f_imply,
     ))
 }
@@ -382,8 +383,8 @@ fn func_body_to_air(
         let rec_f_def = ident_apply(&rec_f, &args_def);
         let eq_zero = mk_eq(&rec_f_fuel, &rec_f_zero);
         let eq_body = mk_eq(&rec_f_succ, &body_expr);
-        let name_zero = format!("{}_fuel_to_zero", fun_to_air_ident(&ctx.name_ctxt, &name));
-        let name_body = format!("{}_fuel_to_body", fun_to_air_ident(&ctx.name_ctxt, &name));
+        let name_zero = format!("{}_fuel_to_zero", fun_to_air_ident(&ctx.name_ctxt, &rec_name));
+        let name_body = format!("{}_fuel_to_body", fun_to_air_ident(&ctx.name_ctxt, &rec_name));
         let opts = Some(FuncBindOpts { add_fuel: true, add_default_ensures: false });
         let bind_zero = func_bind(ctx, name_zero, &typ_params, pars, &rec_f_fuel, opts);
         let bind_body = func_bind(ctx, name_body, &typ_params, pars, &rec_f_succ, opts);
@@ -403,6 +404,7 @@ fn func_body_to_air(
     let e_forall = func_def_quant(
         ctx,
         &suffix_global_id(&fun_to_air_ident(&ctx.name_ctxt, &name)),
+        &suffix_global_id(&fun_to_air_ident(&ctx.name_ctxt, &rec_name)),
         false,
         &impl_typ_params,
         &typ_args,
@@ -519,6 +521,7 @@ fn req_ens_to_air(
         let e_forall = func_def_quant(
             ctx,
             &name,
+            &name,
             is_trait_default_ensures,
             &typ_params,
             &typ_args,
@@ -873,6 +876,7 @@ pub fn func_axioms_to_air(
                     let e_forall = func_def_quant(
                         ctx,
                         &suffix_global_id(&fun_to_air_ident(&ctx.name_ctxt, &f_trait)),
+                        &suffix_global_id(&fun_to_air_ident(&ctx.name_ctxt, &function.x.name)),
                         false,
                         &typ_params,
                         &trait_typ_args,