[move prover] ghost carrier and iterator validity for intrinsic maps

Intrinsic map types may declare ghost fields; such maps are represented
by a per-instance carrier datatype wrapping the raw table, giving the
ghosts constructor arguments to live in. Structural mutations havoc the
ghosts; value writes through borrows preserve them. Ghost-less maps keep
their raw table representation byte-identically.

This enables per-object iterator validity as plain Move-level specs: a
ghost brand on the map plus a ghost stamp on the iterator, with validity
a spec fun over the two — no pragmas, AST ops, or loop instrumentation.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Author: rahxephon89

third_party/move/move-model/src/builder/module_builder.rs

@@ -29,7 +29,7 @@ use crate::{
     },
     pragmas::{
         is_pragma_valid_for_block, is_property_valid_for_condition, CONDITION_DEACTIVATED_PROP,
-        CONDITION_EXPORT_PROP, CONDITION_INJECTED_PROP, INTRINSIC_PRAGMA,
+        CONDITION_EXPORT_PROP, CONDITION_INJECTED_PROP, INTRINSIC_PRAGMA, INTRINSIC_TYPE_MAP,
     },
     symbol::{Symbol, SymbolPool},
     ty::{
@@ -4310,6 +4310,11 @@ impl ModuleBuilder<'_, '_> {
                 );
                 return;
             }
+            // Ghost fields on intrinsic map types are read-only from spec
+            // blocks; that check lives in spec instrumentation, where the
+            // intrinsics annotation is reliably complete for same-module
+            // declarations too (the builder's spec tables are not yet
+            // populated when inline code specs are translated here).
             // Bitwise operators on the RHS produce bitvector-typed Boogie
             // expressions, but ghost fields are declared as unbounded integer
             // in Boogie (they are model-only and don't participate in
@@ -5324,18 +5329,37 @@ impl ModuleBuilder<'_, '_> {
             // New struct in this module
             let spec = self.struct_specs.remove(&name.symbol).unwrap_or_default();
             // Intrinsic types have no generated Boogie datatype to carry
-            // ghost constructor arguments; reject ghosts on them. This is
-            // the earliest point where the intrinsic pragma is reliably
-            // known (spec blocks are fully analyzed).
-            if !entry.ghost_fields.is_empty()
-                && spec
-                    .properties
-                    .contains_key(&self.parent.env.symbol_pool().make(INTRINSIC_PRAGMA))
-            {
-                for f in entry.ghost_fields.values() {
-                    self.parent
-                        .env
-                        .error(&f.loc, "ghost fields are not supported on intrinsic types");
+            // ghost constructor arguments; reject ghosts on them — except
+            // intrinsic MAP types, whose backend representation gains a
+            // carrier datatype when ghosts are declared (used for iterator
+            // validity). This is the earliest point where the intrinsic
+            // pragma is reliably known (spec blocks are fully analyzed).
+            if !entry.ghost_fields.is_empty() {
+                let pool = self.parent.env.symbol_pool();
+                let is_intrinsic_map = matches!(
+                    spec.properties.get(&pool.make(INTRINSIC_PRAGMA)),
+                    Some(PropertyValue::Symbol(s))
+                        if pool.string(*s).as_str() == INTRINSIC_TYPE_MAP
+                );
+                if !is_intrinsic_map && spec.properties.contains_key(&pool.make(INTRINSIC_PRAGMA)) {
+                    for f in entry.ghost_fields.values() {
+                        self.parent
+                            .env
+                            .error(&f.loc, "ghost fields are not supported on intrinsic types");
+                    }
+                } else if is_intrinsic_map {
+                    // The carrier datatype is declared once per map type with the
+                    // ghost argument types baked in; map ghosts are restricted to
+                    // `num` (sufficient for identity/version state, and avoids
+                    // per-instance ghost typing in the carrier).
+                    for f in entry.ghost_fields.values() {
+                        if !matches!(f.ty, Type::Primitive(crate::ty::PrimitiveType::Num)) {
+                            self.parent.env.error(
+                                &f.loc,
+                                "ghost fields on intrinsic map types must have type `num`",
+                            );
+                        }
+                    }
                 }
             }
             let mut field_data: BTreeMap<FieldId, FieldData> = BTreeMap::new();

third_party/move/move-prover/boogie-backend/src/boogie_helpers.rs

@@ -59,6 +59,20 @@ pub fn boogie_module_name(env: &ModuleEnv<'_>) -> String {
 /// Return boogie name of given structure.
 pub fn boogie_struct_name(struct_env: &StructEnv<'_>, inst: &[Type], bv_flag: bool) -> String {
     if struct_env.is_intrinsic_of(INTRINSIC_TYPE_MAP) {
+        if struct_env.get_ghost_fields().next().is_some() {
+            // Intrinsic maps that declare ghost fields use a per-instance
+            // carrier datatype wrapping the table, so the ghosts have
+            // constructor arguments to live in. The name must agree with the
+            // suffix convention (`boogie_type_suffix_for_struct`), including
+            // the bv twin of the value type, so twin instances reference
+            // their own carrier consistently.
+            return format!(
+                "${}_{}{}",
+                boogie_module_name(&struct_env.module_env),
+                struct_env.get_name().display(struct_env.symbol_pool()),
+                boogie_inst_suffix(struct_env.module_env.env, inst, &[false, bv_flag])
+            );
+        }
         // Map to the theory type representation, which is `Table int V`. The key
         // is encoded as an integer to avoid extensionality problems, and to support
         // $Mutation paths, which are sequences of ints.

third_party/move/move-prover/boogie-backend/src/bytecode_translator.rs

@@ -46,7 +46,7 @@ use move_model::{
         QualifiedInstId, StructEnv, StructId,
     },
     pragmas::{
-        ADDITION_OVERFLOW_UNCHECKED_PRAGMA, SEED_PRAGMA, TIMEOUT_PRAGMA,
+        ADDITION_OVERFLOW_UNCHECKED_PRAGMA, INTRINSIC_TYPE_MAP, SEED_PRAGMA, TIMEOUT_PRAGMA,
         VERIFY_DURATION_ESTIMATE_PRAGMA,
     },
     symbol::Symbol,
@@ -7306,13 +7306,19 @@ impl FunctionTranslator<'_> {
                 if matches!(edge, BorrowEdge::Invoke) {
                     emitln!(writer, "call $t{} := $HavocMutation($t{});", idx, idx);
                 } else {
+                    // Type of the value behind the destination reference, for
+                    // ghost-carrier detection along the write-back chain.
+                    let root_ty = self
+                        .inst(self.get_local_type(*idx).skip_reference())
+                        .clone();
                     let update = if let BorrowEdge::Hyper(edges) = edge {
                         self.translate_write_back_update(
                             &mut || dst_value.clone(),
                             &get_path_index,
                             src_value,
                             edges,
                             0,
+                            &root_ty,
                         )
                     } else {
                         self.translate_write_back_update(
@@ -7321,6 +7327,7 @@ impl FunctionTranslator<'_> {
                             src_value,
                             &[edge.to_owned()],
                             0,
+                            &root_ty,
                         )
                     };
                     emitln!(
@@ -7358,21 +7365,31 @@ impl FunctionTranslator<'_> {
         None
     }
 
+    /// `dest_ty` is the type of the value denoted by `mk_dest()` at this edge
+    /// position (threaded from the borrow root), used to detect intrinsic-map
+    /// ghost carriers on `Index(Table)` edges. `Type::Error` when unknown
+    /// (custom index edges), which never matches a carrier.
     fn translate_write_back_update(
         &self,
         mk_dest: &mut dyn FnMut() -> String,
         get_path_index: &dyn Fn(usize) -> String,
         src: String,
         edges: &[BorrowEdge],
         at: usize,
+        dest_ty: &Type,
     ) -> String {
         if at >= edges.len() {
             src
         } else {
             match &edges[at] {
-                BorrowEdge::Direct => {
-                    self.translate_write_back_update(mk_dest, get_path_index, src, edges, at + 1)
-                },
+                BorrowEdge::Direct => self.translate_write_back_update(
+                    mk_dest,
+                    get_path_index,
+                    src,
+                    edges,
+                    at + 1,
+                    dest_ty,
+                ),
                 BorrowEdge::Field(memory, variant, offset) => {
                     let memory = memory.to_owned().instantiate(self.type_inst);
                     let struct_env = &self.parent.env.get_struct_qid(memory.to_qualified_id());
@@ -7384,6 +7401,7 @@ impl FunctionTranslator<'_> {
                             *offset,
                         )
                     };
+                    let field_ty = field_env.get_type().instantiate(&memory.inst);
                     let field_sel = boogie_field_sel(&field_env);
                     let new_dest = format!("{}->{}", (*mk_dest)(), field_sel);
                     let mut new_dest_needed = false;
@@ -7396,6 +7414,7 @@ impl FunctionTranslator<'_> {
                         src,
                         edges,
                         at + 1,
+                        &field_ty,
                     );
                     let update_fun = if variant.is_none() {
                         boogie_field_update(&field_env, &memory.inst)
@@ -7441,14 +7460,54 @@ impl FunctionTranslator<'_> {
                             self.get_borrow_native_aggregate_names(name).unwrap()
                         },
                     };
+                    let env = self.parent.env;
+                    // A ghost-carrier map (an intrinsic map declaring ghost
+                    // fields) wraps its table: content is read through `->$t`,
+                    // and the update rebuilds the carrier PRESERVING the ghost
+                    // arguments — a write through a borrowed value entry is not
+                    // a structural mutation and must not disturb e.g. the
+                    // iterator-validity brand.
+                    let carrier = if matches!(index_edge_kind, IndexEdgeKind::Table) {
+                        if let Type::Struct(mid, sid, targs) = dest_ty.skip_reference() {
+                            let struct_env = env.get_struct(mid.qualified(*sid));
+                            let ghost_sels: Vec<String> = struct_env
+                                .get_ghost_fields()
+                                .map(|f| boogie_field_sel(&f))
+                                .collect();
+                            if struct_env.is_intrinsic_of(INTRINSIC_TYPE_MAP)
+                                && !ghost_sels.is_empty()
+                            {
+                                Some((boogie_struct_name(&struct_env, targs, false), ghost_sels))
+                            } else {
+                                None
+                            }
+                        } else {
+                            None
+                        }
+                    } else {
+                        None
+                    };
+                    // The element/value type for the recursion step.
+                    let elem_ty = match (index_edge_kind, dest_ty.skip_reference()) {
+                        (IndexEdgeKind::Vector, Type::Vector(elem)) => (**elem).clone(),
+                        (IndexEdgeKind::Table, Type::Struct(_, _, targs)) if targs.len() >= 2 => {
+                            targs[1].clone()
+                        },
+                        _ => Type::Error,
+                    };
 
                     // Compute the offset into the path where to retrieve the index.
                     let offset = edges[0..at]
                         .iter()
                         .filter(|e| !matches!(e, BorrowEdge::Direct))
                         .count();
                     let index = (*get_path_index)(offset);
-                    let new_dest = format!("{}({}, {})", read_aggregate, (*mk_dest)(), index);
+                    let content = |dest: String| match &carrier {
+                        Some(_) => format!("{}->$t", dest),
+                        None => dest,
+                    };
+                    let new_dest =
+                        format!("{}({}, {})", read_aggregate, content((*mk_dest)()), index);
                     let mut new_dest_needed = false;
                     // Recursively perform write backs for next edges
                     let new_src = self.translate_write_back_update(
@@ -7460,25 +7519,32 @@ impl FunctionTranslator<'_> {
                         src,
                         edges,
                         at + 1,
+                        &elem_ty,
                     );
+                    let mk_update = |dest: String, new_src: &str| match &carrier {
+                        Some((carrier_name, ghost_sels)) => {
+                            let ghosts = ghost_sels
+                                .iter()
+                                .map(|sel| format!(", {}->{}", dest, sel))
+                                .join("");
+                            format!(
+                                "{}({}({}->$t, {}, {}){})",
+                                carrier_name, update_aggregate, dest, index, new_src, ghosts
+                            )
+                        },
+                        None => {
+                            format!("{}({}, {}, {})", update_aggregate, dest, index, new_src)
+                        },
+                    };
                     if new_dest_needed {
                         format!(
-                            "(var $$sel{} := {}; {}({}, {}, {}))",
+                            "(var $$sel{} := {}; {})",
                             at,
                             new_dest,
-                            update_aggregate,
-                            (*mk_dest)(),
-                            index,
-                            new_src
+                            mk_update((*mk_dest)(), &new_src)
                         )
                     } else {
-                        format!(
-                            "{}({}, {}, {})",
-                            update_aggregate,
-                            (*mk_dest)(),
-                            index,
-                            new_src
-                        )
+                        mk_update((*mk_dest)(), &new_src)
                     }
                 },
                 BorrowEdge::Hyper(_) | BorrowEdge::Invoke => unreachable!("unexpected borrow edge"),

third_party/move/move-prover/boogie-backend/src/lib.rs

@@ -6,7 +6,9 @@
 #![forbid(unsafe_code)]
 
 use crate::{
-    boogie_helpers::{boogie_module_name, boogie_num_type_base, boogie_type, boogie_type_suffix},
+    boogie_helpers::{
+        boogie_field_sel, boogie_module_name, boogie_num_type_base, boogie_type, boogie_type_suffix,
+    },
     bytecode_translator::has_native_equality,
     options::{BoogieOptions, VectorTheory},
 };
@@ -105,6 +107,12 @@ struct BvInfo {
     max: String,
 }
 
+#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize, Default)]
+struct GhostArg {
+    sel: String,
+    ty: String,
+}
+
 #[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize, Default)]
 struct MapImpl {
     struct_name: String,
@@ -132,6 +140,20 @@ struct MapImpl {
     iter_ptr_prefix: String,
     iter_variant: String,
     iter_key_sel: String,
+    // Ghost carrier: an intrinsic map that declares ghost fields is
+    // represented as a per-instance datatype wrapping the table, so the
+    // ghosts have constructor arguments to live in. `struct_base` plus the
+    // instance suffix is the carrier datatype name (agreeing with
+    // `boogie_struct_name`); `ghost_args` are the ghost selectors and their
+    // (type-parameter-free) Boogie types.
+    has_ghost_carrier: bool,
+    struct_base: String,
+    ghost_args: Vec<GhostArg>,
+    gb_args: String,
+    gb_decls: String,
+    gb_havoc: String,
+    ghost_preserve_args: String,
+    ghost_zero_args: String,
     fun_get: String,
     fun_borrow_front: String,
     fun_borrow_back: String,
@@ -555,7 +577,7 @@ impl MapImpl {
         ty_args: &BTreeSet<(Type, Type)>,
         bv_flag: bool,
     ) -> Self {
-        let insts = ty_args
+        let insts: Vec<(TypeInfo, TypeInfo)> = ty_args
             .iter()
             .map(|(kty, vty)| {
                 (
@@ -580,6 +602,38 @@ impl MapImpl {
             env,
             decl.get_fun_triple(env, INTRINSIC_FUN_MAP_ITER_BORROW_MUT),
         );
+        let ghost_args: Vec<GhostArg> = struct_env
+            .get_ghost_fields()
+            .map(|f| GhostArg {
+                sel: boogie_field_sel(&f),
+                ty: boogie_type(env, &f.get_type(), false),
+            })
+            .collect();
+        let has_ghost_carrier = !ghost_args.is_empty();
+        let struct_base = struct_name.clone();
+        // Rebuild plumbing for mutating templates: fresh (havoced) ghost
+        // values per rebuild site, shared between the rebuilt value and any
+        // post-state spec-function application describing it.
+        let (gb_args, gb_decls, gb_havoc) = if has_ghost_carrier {
+            let idxs = 0..ghost_args.len();
+            (
+                idxs.clone().map(|i| format!(", $gb{}", i)).join(""),
+                idxs.clone()
+                    .map(|i| format!("\n    var $gb{}: int;", i))
+                    .join(""),
+                idxs.map(|i| format!("havoc $gb{}; ", i)).join(""),
+            )
+        } else {
+            (String::new(), String::new(), String::new())
+        };
+        // Pure spec functions cannot havoc: map-returning spec funs preserve
+        // the input's ghost args (whole-map equalities are ghost-excluding,
+        // so the choice is immaterial) or use zeros when there is no input.
+        let ghost_preserve_args = ghost_args
+            .iter()
+            .map(|g| format!(", t->{}", g.sel))
+            .join("");
+        let ghost_zero_args = ghost_args.iter().map(|_| ", 0".to_string()).join("");
 
         MapImpl {
             struct_name,
@@ -646,6 +700,14 @@ impl MapImpl {
             iter_ptr_prefix: iter_parts.0,
             iter_variant: iter_parts.1,
             iter_key_sel: iter_parts.2,
+            has_ghost_carrier,
+            struct_base,
+            ghost_args,
+            gb_args,
+            gb_decls,
+            gb_havoc,
+            ghost_preserve_args,
+            ghost_zero_args,
             fun_get: Self::triple_opt_to_name(env, decl.get_fun_triple(env, INTRINSIC_FUN_MAP_GET)),
             fun_borrow_front: Self::triple_opt_to_name(
                 env,