panic related to enum

[msaaltink]

It seems tricky to write pure functions that handle enums. Here's one panicing example:

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() {
    prover::prover::ensures(f2(E::B(1)))
}

fails with

thread 'main' (503435) panicked at crates/move-prover-boogie-backend/src/boogie_backend/bytecode_translator.rs:2867:29:
unexpected operation PackVariant(ModuleId(138), DatatypeId(Symbol(1254)), VariantId(Symbol(1258)), []) in function purity::f2
stack backtrace:
   0: __rustc::rust_begin_unwind
   1: core::panicking::panic_fmt
   2: move_prover_boogie_backend::boogie_backend::bytecode_translator::FunctionTranslator::generate_function_body
   3: move_prover_boogie_backend::boogie_backend::bytecode_translator::FunctionTranslator::translate
   4: move_prover_boogie_backend::boogie_backend::bytecode_translator::BoogieTranslator::translate_function_style
   5: move_prover_boogie_backend::boogie_backend::bytecode_translator::BoogieTranslator::translate
   6: move_prover_boogie_backend::generator::generate_boogie
   7: move_prover_boogie_backend::generator::generate_function_bpl
 ...

I had actually wanted to write the simpler

#[ext(pure)]
public fun f(e: E): bool {
    match(e) {
        E::A => true,
        E::B(v) => v > 0,
    }
}

but that is rejected with the surprising message

error: Pure functions with loops are not supported

[peter941221]

Hi! I’d like to take a shot at this.

I’ve reproduced the issue and I think the problem is in the pure-function translation path not handling enum-related operations consistently (PackVariant / enum matching), which is why the exists! example panics and the match form gets rejected unexpectedly.

My plan is:

1. minimize the repro further,
2. trace how enum construction/matching reaches the purity translation path,
3. implement the smallest fix that keeps the pure fragment sound,
4. add regression tests for both the exists! case and the match-based case.

If there is already work in progress or a preferred direction for handling enum lowering in pure functions, I’d appreciate a pointer.