Fix pure enum constructor lowering and improve enum match diagnostics

.gitignore

@@ -56,3 +56,8 @@ output/
 
 crates/sui-prover/tests/sources/*
 settings.local.json
+
+# Local project memory / operator docs
+AGENTS.md
+MEMORY.md
+RUNBOOK.md

crates/move-prover-boogie-backend/src/boogie_backend/bytecode_translator.rs

@@ -3026,6 +3026,58 @@ impl<'env> FunctionTranslator<'env> {
         }
     }
 
+    fn format_default_value(&self, ty: &Type) -> String {
+        use PrimitiveType::*;
+        use Type::*;
+
+        match ty {
+            Primitive(Bool) => "false".to_string(),
+            Primitive(U8 | U16 | U32 | U64 | U128 | U256 | Num | Address) => "0".to_string(),
+            Primitive(Signer) => "$signer(0)".to_string(),
+            Vector(_) => "EmptyVec()".to_string(),
+            Datatype(..) | TypeParameter(_) => "DefaultVecElem()".to_string(),
+            Reference(..)
+            | Fun(..)
+            | Tuple(..)
+            | TypeDomain(..)
+            | ResourceDomain(..)
+            | Error
+            | Var(..)
+            | Primitive(Range | EventStore) => {
+                panic!("unexpected pure default value type: {:?}", ty)
+            }
+        }
+    }
+
+    fn format_enum_variant_expression(
+        &self,
+        enum_env: &EnumEnv<'_>,
+        variant_env: &VariantEnv<'_>,
+        inst: &[Type],
+        field_values: &[String],
+    ) -> String {
+        let mut provided_fields = field_values.iter();
+        let all_fields = enum_env
+            .get_all_fields()
+            .map(|field| {
+                let field_ty = field.get_type().instantiate(inst);
+                let EnclosingEnv::Variant(parent_variant) = &field.parent_env else {
+                    unreachable!();
+                };
+                if parent_variant.get_id() == variant_env.get_id() {
+                    provided_fields
+                        .next()
+                        .cloned()
+                        .unwrap_or_else(|| self.format_default_value(&field_ty))
+                } else {
+                    self.format_default_value(&field_ty)
+                }
+            })
+            .chain(iter::once(variant_env.get_tag().to_string()))
+            .join(", ");
+        format!("{}({})", boogie_enum_name(enum_env, inst), all_fields)
+    }
+
     /// Generate Boogie pure function body using let/var expression nesting
     fn generate_pure_expression(&mut self, code: &[Bytecode]) {
         use Bytecode::*;
@@ -3176,6 +3228,16 @@ impl<'env> FunctionTranslator<'env> {
                             let all_args = regular_args.into_iter().chain(dynamic_args).join(", ");
 
                             format!("{}({})", boogie_struct_name(&struct_env, inst), all_args)
+                        } else if let Operation::PackVariant(mid, eid, vid, inst) = op {
+                            let inst = &self.inst_slice(inst);
+                            let enum_env = fun_target.global_env().get_module(*mid).into_enum(*eid);
+                            let args = srcs.iter().map(|src| fmt_temp(*src)).collect_vec();
+                            self.format_enum_variant_expression(
+                                &enum_env,
+                                &enum_env.get_variant(*vid),
+                                inst,
+                                &args,
+                            )
                         } else if matches!(op, Operation::Eq | Operation::Neq) {
                             // Handle equality/inequality using $IsEqual functions to support
                             // non-extensional types like vectors and tables

crates/move-prover-boogie-backend/src/boogie_backend/options.rs

@@ -245,6 +245,20 @@ impl Default for BoogieOptions {
 }
 
 impl BoogieOptions {
+    #[cfg(windows)]
+    fn normalize_boogie_option(option: &str) -> String {
+        if let Some(rest) = option.strip_prefix('-') {
+            format!("/{rest}")
+        } else {
+            option.to_string()
+        }
+    }
+
+    #[cfg(not(windows))]
+    fn normalize_boogie_option(option: &str) -> String {
+        option.to_string()
+    }
+
     /// Derive options based on other set options.
     pub fn derive_options(&mut self) {
         use VectorTheory::*;
@@ -296,9 +310,10 @@ impl BoogieOptions {
         let mut seen_options = HashSet::new();
         let mut add = |sl: &[&str]| {
             for s in sl {
-                let key = Self::get_option_key(s);
+                let normalized = Self::normalize_boogie_option(s);
+                let key = Self::get_option_key(&normalized).to_string();
                 seen_options.retain(|existing: &String| Self::get_option_key(existing) != key);
-                seen_options.insert(s.to_string());
+                seen_options.insert(normalized);
             }
         };
 

crates/move-prover-boogie-backend/src/generator.rs

@@ -25,6 +25,7 @@ use move_model::{
 use move_stackless_bytecode::package_targets::PackageTargets;
 use move_stackless_bytecode::{
     escape_analysis::EscapeAnalysisProcessor,
+    file_name_sanitizer::sanitize_file_name_component,
     function_target_pipeline::{
         FunctionHolderTarget, FunctionTargetPipeline, FunctionTargetsHolder,
     },
@@ -311,11 +312,11 @@ fn generate_function_bpl<W: WriteColor>(
 ) -> anyhow::Result<FileOptions> {
     env.cleanup();
 
-    let file_name = format!(
+    let file_name = sanitize_file_name_component(&format!(
         "{}_{:?}",
         env.get_function(*qid).get_full_name_str(),
         asserts_mode
-    );
+    ));
     let target_type = FunctionHolderTarget::Function(*qid);
     let (mut targets, _) = create_and_process_bytecode(options, env, package_targets, target_type);
 
@@ -385,11 +386,11 @@ fn generate_module_bpl<W: WriteColor>(
 ) -> anyhow::Result<FileOptions> {
     env.cleanup();
 
-    let file_name = format!(
+    let file_name = sanitize_file_name_component(&format!(
         "{}_{:?}",
         env.get_module(*mid).get_full_name_str(),
         asserts_mode
-    );
+    ));
     let target_type = if asserts_mode == AssertsMode::SpecNoAbortCheck {
         FunctionHolderTarget::SpecNoAbortCheck(*mid)
     } else {

crates/move-stackless-bytecode/src/conditional_merge_insertion.rs

@@ -511,11 +511,21 @@ impl FunctionTargetProcessor for ConditionalMergeInsertionProcessor {
             None => {
                 // cannot reconstruct (loops, switches, etc.)
                 if is_pure {
-                    func_env.module_env.env.diag(
-                        Severity::Error,
-                        &func_env.get_loc(),
-                        "Pure functions with loops are not supported",
-                    );
+                    let message = if state
+                        .builder
+                        .data
+                        .code
+                        .iter()
+                        .any(|bc| matches!(bc, Bytecode::VariantSwitch(..)))
+                    {
+                        "Pure functions with enum matches are not supported"
+                    } else {
+                        "Pure functions with loops are not supported"
+                    };
+                    func_env
+                        .module_env
+                        .env
+                        .diag(Severity::Error, &func_env.get_loc(), message);
                 }
                 return state.builder.data;
             }

crates/move-stackless-bytecode/src/file_name_sanitizer.rs

@@ -0,0 +1,8 @@
+pub fn sanitize_file_name_component(name: &str) -> String {
+    name.chars()
+        .map(|character| match character {
+            '<' | '>' | ':' | '"' | '/' | '\\' | '|' | '?' | '*' => '_',
+            _ => character,
+        })
+        .collect()
+}

crates/move-stackless-bytecode/src/lib.rs

@@ -28,6 +28,7 @@ pub mod eliminate_imm_refs;
 pub mod escape_analysis;
 pub mod exp_generator;
 pub mod exp_rewriter;
+pub mod file_name_sanitizer;
 pub mod function_data_builder;
 pub mod function_stats;
 pub mod function_target;

crates/move-stackless-bytecode/src/spec_hierarchy.rs

@@ -8,6 +8,7 @@
 //! The hierarchies respect opaque boundaries (specs without `no_opaque`) and filter out
 //! system functions from standard libraries.
 
+use crate::file_name_sanitizer::sanitize_file_name_component;
 use crate::function_target_pipeline::FunctionTargetsHolder;
 use move_model::model::{FunId, FunctionEnv, GlobalEnv, QualifiedId};
 use num::BigUint;
@@ -109,7 +110,11 @@ fn write_spec_log_file(
     output_dir: &Path,
     excluded_addresses: &[BigUint],
 ) {
-    let log_file_path = output_dir.join(format!("{}{}", spec_name, LOG_FILE_EXTENSION));
+    let log_file_path = output_dir.join(format!(
+        "{}{}",
+        sanitize_file_name_component(&spec_name),
+        LOG_FILE_EXTENSION
+    ));
 
     let mut content = String::new();
     let mut displayed = BTreeSet::new();

crates/sui-prover/tests/inputs/pure_functions/issue_452.move

@@ -0,0 +1,25 @@
+// Repro for https://github.com/asymptotic-code/sui-prover/issues/452
+// Panic when a pure function uses `exists!` with enum variant construction.
+module 0x42::issue_452;
+
+use prover::prover::ensures;
+
+public enum E has copy, drop {
+    A,
+    B(u8),
+}
+
+#[ext(pure)]
+public fun f2(e: E): bool {
+    e == E::A || prover::prover::exists!(|v| is_b(*v, e))
+}
+
+#[ext(pure)]
+public fun is_b(v: u8, e: E): bool {
+    e == E::B(v)
+}
+
+#[spec(prove)]
+fun test() {
+    ensures(f2(E::B(1)))
+}

crates/sui-prover/tests/inputs/pure_functions/issue_452_generic.move

@@ -0,0 +1,25 @@
+// Generic regression for issue 452:
+// enum constructor lowering must instantiate fields with the enum operation instantiation.
+module 0x42::issue_452_generic;
+
+use prover::prover::ensures;
+
+public enum E<T> has copy, drop {
+    A,
+    B(T),
+}
+
+#[ext(pure)]
+public fun wrap_u8(e: E<u8>): bool {
+    prover::prover::exists!(|v| matches_b(*v, e))
+}
+
+#[ext(pure)]
+fun matches_b<T: copy + drop>(v: T, e: E<T>): bool {
+    e == E::B(v)
+}
+
+#[spec(prove)]
+fun test() {
+    ensures(wrap_u8(E::B(1)))
+}

crates/sui-prover/tests/inputs/pure_functions/issue_452_match.move

@@ -0,0 +1,23 @@
+/// Alternate repro from https://github.com/asymptotic-code/sui-prover/issues/452
+/// Matching on an enum inside a pure function reports a misleading loop error.
+module 0x42::issue_452_match;
+
+use prover::prover::ensures;
+
+public enum E has copy, drop {
+    A,
+    B(u8),
+}
+
+#[ext(pure)]
+public fun f(e: E): bool {
+    match (e) {
+        E::A => true,
+        E::B(v) => v > 0,
+    }
+}
+
+#[spec(prove)]
+fun test() {
+    ensures(f(E::B(1)))
+}

crates/sui-prover/tests/integration.rs

@@ -14,6 +14,11 @@ use sui_prover::prove::DEFAULT_EXECUTION_TIMEOUT_SECONDS;
 
 /// Runs the prover on the given file path and returns the output as a string
 fn run_prover(file_path: &Path) -> String {
+    let test_source = read_to_string(file_path).unwrap_or_default();
+    let generate_only = test_source
+        .lines()
+        .any(|line| line.trim() == "// prover-test: generate-only");
+
     let prover_dir = Path::new(env!("CARGO_MANIFEST_DIR"))
         .parent()
         .unwrap()
@@ -117,6 +122,8 @@ integration-test = "0x9"
                 options.backend.debug_trace = false;
                 options.prover.debug_trace = false;
                 options.backend.keep_artifacts = true;
+                options.prover.generate_only = generate_only;
+                options.backend.no_verify = generate_only;
                 options.output_path = Path::new(&options.output_path)
                     .join(relative_path.with_extension(""))
                     .to_string_lossy()
@@ -192,6 +199,9 @@ fn post_process_output(output: String, sources_dir: PathBuf) -> String {
     let re_git_branch = Regex::new(r"(https___github_com_[^/]+_sui)_git_[^/]+/").unwrap();
     let output = re_git_branch.replace_all(&output, "${1}_git_NORMALIZED/");
 
+    // Normalize Windows path separators so snapshot output stays stable across platforms.
+    let output = output.replace('\\', "/");
+
     // Use regex to replace numbers with more than one digit followed by u64 with ELIDEDu64
     let re = Regex::new(r"\d{2,}u64").unwrap();
     re.replace_all(&output, "ELIDEDu64").to_string()

crates/sui-prover/tests/snapshots/pure_functions/issue_452.move.snap

@@ -0,0 +1,6 @@
+---
+source: crates/sui-prover/tests/integration.rs
+assertion_line: 304
+expression: output
+---
+Verification successful

crates/sui-prover/tests/snapshots/pure_functions/issue_452_generic.move.snap

@@ -0,0 +1,6 @@
+---
+source: crates/sui-prover/tests/integration.rs
+assertion_line: 307
+expression: output
+---
+Verification successful

crates/sui-prover/tests/snapshots/pure_functions/issue_452_match.move.snap

@@ -0,0 +1,16 @@
+---
+source: crates/sui-prover/tests/integration.rs
+assertion_line: 307
+expression: output
+---
+exiting with bytecode transformation errors
+error: Pure functions with enum matches are not supported
+   ┌─ tests/inputs/pure_functions/issue_452_match.move:13:1
+   │  
+13 │ ╭ public fun f(e: E): bool {
+14 │ │     match (e) {
+15 │ │         E::A => true,
+16 │ │         E::B(v) => v > 0,
+17 │ │     }
+18 │ │ }
+   │ ╰─^