Fix pure enum constructor lowering and improve enum match diagnostics

[peter941221]

Summary

• fix pure lowering for enum variant constructors in issue_452
• report unsupported pure enum matches with a precise enum-match diagnostic
• normalize Windows Boogie CLI options and stabilize snapshot output paths
• sanitize generated artifact and log filenames on Windows

Root cause

generate_pure_expression handled Pack but not PackVariant, so pure enum constructor expressions could reach an invalid lowering path and panic. The match symptom was separate: pure control-flow reconstruction rejected VariantSwitch, but the old diagnostic mislabeled that limitation as a loop problem.

Validation

• cargo fmt --all
• cargo test -p sui-prover -- issue_452 -- --nocapture
• cargo test -p sui-prover -- issue_544 -- --nocapture
• cargo test -p sui-prover -- pure_functions -- --nocapture

Notes for reviewers

• This PR intentionally does not implement full pure enum match lowering.
• It restores issue_452 as a normal full verification regression instead of relying on a local generate-only workaround.
• The Windows compatibility changes are included because they were required to run the full local Boogie + Z3 validation path reliably.

[cursor]

Cursor Bugbot has reviewed your changes and found 2 potential issues.

^{Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, enable autofix in the Cursor dashboard.}

[cursor]

Wrong type instantiation for generic enum field defaults

Medium Severity

self.inst(&field.get_type()) instantiates enum field types using the function's type_inst, but field.get_type() returns types containing the enum's type parameters. For generic enums where the function and enum type parameter indices don't align (e.g., fun g<S, T>(e: E<T>)), enum TypeParameter(0) incorrectly maps to function param S instead of T. The inst parameter (the operation's already-resolved type args) is available and the correct approach — matching the pattern at lines 6489/6511 — is field.get_type().instantiate(inst).

 

[peter941221]

Good catch — this was a real bug for generic enums. I updated format_enum_variant_expression to instantiate field types with the operation-local inst (field.get_type().instantiate(inst)) instead of the function translator type_inst, and added a dedicated regression at crates/sui-prover/tests/inputs/pure_functions/issue_452_generic.move. I also reran the targeted prover tests for issue_452 and the pure_functions suite with the local Boogie/Z3 toolchain, and they pass now.

[cursor]

Duplicated sanitization functions across two crates

Low Severity

sanitize_artifact_file_name in generator.rs and sanitize_log_file_stem in spec_hierarchy.rs have identical logic — both replace the same set of characters (< > : " / \ | ? *) with underscores. Having two copies increases the risk of divergence if the character set needs updating.

Additional Locations (1)

• crates/move-stackless-bytecode/src/spec_hierarchy.rs#L23-L31

 

[peter941221]

Agreed. I followed up by extracting the shared logic into move_stackless_bytecode::file_name_sanitizer::sanitize_file_name_component and switched both call sites over to the common helper, so the character replacement rules now live in one place.

[peter941221]

Hi! It looks like the required workflows are still awaiting approval because this PR comes from a fork. Once the workflows are approved and the checks run, I’m happy to address any CI feedback if needed.

[cursor]

You have used all of your free Bugbot PR reviews.

To receive reviews on all of your PRs, visit the Cursor dashboard to activate Pro and start your 14-day free trial.

[cursor]

You have used all of your free Bugbot PR reviews.

To receive reviews on all of your PRs, visit the Cursor dashboard to activate Pro and start your 14-day free trial.

[cursor]

You have used all of your free Bugbot PR reviews.

To receive reviews on all of your PRs, visit the Cursor dashboard to activate Pro and start your 14-day free trial.

[peter941221]

Quick update following the issue-thread discussion on #452.

I refreshed this branch onto the current main and force-pushed the rebased code path. The new head is a3c97de.

I also closed #563 so the discussion stays focused on the actual code-fix lane.

Targeted validation rerun after the refresh:

• cargo fmt --all --check
• Z3_EXE=... cargo test -p sui-prover --test integration issue_452 -- --nocapture

That targeted integration run passed for all three relevant fixtures:

• issue_452
• issue_452_generic
• issue_452_match

Scope is unchanged from the earlier description:

• restore the pure enum constructor path so PackVariant no longer falls into the invalid pure-lowering panic path
• keep the unsupported pure enum match boundary explicit with a more accurate diagnostic
• do not claim full pure enum match lowering in this PR