Properly qualify references to vstd when desugaring for-loops (#2647)

Author: parno

source/builtin_macros/src/syntax.rs

@@ -3546,7 +3546,7 @@ impl Visitor {
         ));
         let ghost_inv: Expr = Expr::Verbatim(quote_spanned_vstd!(vstd, expr.span() =>
             #[verifier::custom_err(#ghost_inv_msg)]
-            match vstd::prelude::infer_spec_for_loop_iter(
+            match #vstd::prelude::infer_spec_for_loop_iter(
                 &::core::iter::IntoIterator::into_iter(#x_verus_iter_init),
                 &::core::iter::IntoIterator::into_iter(#expr_inv),
                 #print_hint,
@@ -3567,7 +3567,7 @@ impl Visitor {
             for inv in &mut invariant.exprs.exprs {
                 *inv = Expr::Verbatim(quote_spanned_vstd!(vstd, inv.span() => {
                     let #pat = #vstd::std_specs::iter::IteratorSpec::peek(&#x_iter_name.snapshot.view(), #x_iter_name.index.view())
-                        .unwrap_or(vstd::pervasive::arbitrary());
+                        .unwrap_or(#vstd::pervasive::arbitrary());
                     #inv
                 }));
             }
@@ -3590,7 +3590,7 @@ impl Visitor {
             for inv in &mut invariant_except_break.exprs.exprs {
                 *inv = Expr::Verbatim(quote_spanned_vstd!(vstd, inv.span() => {
                     let #pat = #vstd::std_specs::iter::IteratorSpec::peek(&#x_iter_name.snapshot.view(), #x_iter_name.index.view())
-                        .unwrap_or(vstd::pervasive::arbitrary());
+                        .unwrap_or(#vstd::pervasive::arbitrary());
                     #inv
                 }));
             }
@@ -3610,7 +3610,7 @@ impl Visitor {
             for expr in &mut decreases.exprs.exprs {
                 *expr = Expr::Verbatim(quote_spanned_vstd!(vstd, expr.span() => {
                     let #pat = #vstd::std_specs::iter::IteratorSpec::peek(&#x_iter_name.snapshot.view(), #x_iter_name.index.view())
-                        .unwrap_or(vstd::pervasive::arbitrary());
+                        .unwrap_or(#vstd::pervasive::arbitrary());
                     #expr
                 }));
             }
@@ -3697,7 +3697,7 @@ impl Visitor {
                 #x_exec_iter,
                 // Spec-level iterator (relies on `when_used_as_spec` on into_iter)
                 #[verifier::ghost_wrapper]
-                ::vstd::prelude::ghost_exec(#[verifier::ghost_block_wrapped] Some(&#x_exec_iter)),
+                #vstd::prelude::ghost_exec(#[verifier::ghost_block_wrapped] Some(&#x_exec_iter)),
             );
             // Hold on to the initial snapshot value so that after the loop, we know it didn't change
             #[allow(non_snake_case)]