panic: unexpected 0 destinations for operation TraceLocal(0)

[msaaltink]

module nesting::nesting;

use sui::object_table::ObjectTable;
use prover::prover::{asserts, ensures, forall, requires};

public struct S has store, key {id: UID, x: u8, y: u8}

#[ext(pure)]
public fun is_good_S(s: &S): bool {
    s.x > 0
}

public fun table_is_good(t: &ObjectTable<ID, S>): bool {
    forall!(|i| id_is_good(*i, t))
}

#[ext(pure)]
public fun id_is_good(i: ID, t: &ObjectTable<ID, S>): bool {
    !t.contains(i) || is_good_S(&t[i])
}

public struct T {m: ObjectTable<ID, S>, z: u8}

#[ext(pure)]
fun is_good_T(t: &T): bool {
    table_is_good(&t.m) && t.z < 100
}

gives a panic:

thread 'main' (152078) panicked at crates/move-prover-boogie-backend/src/boogie_backend/bytecode_translator.rs:3112:25:
unexpected 0 destinations for operation TraceLocal(0) in function nesting::table_is_good

This does not happen if the pure marker is removed from is_good_T.

[andreistefanescu]

@claude can you debug this?

[claude]

Claude finished @andreistefanescu's task in 25m 18s —— View job • claude/issue-544-20260306-1958 • Create PR ➔

---

Debugging panic: unexpected 0 destinations for operation TraceLocal(0)

• Gather context: read the panic location and surrounding code
• Trace the root cause of the 0 destinations issue
• Understand how #[ext(pure)] affects TraceLocal handling
• Implement a fix
• Add a test case
• Commit and push

Root Cause

When a function is marked #[ext(pure)], any non-pure function it calls becomes a "pure callee". Both pure functions and pure callees get translated with FunctionTranslationStyle::Pure, which generates Boogie function declarations (inline expressions) instead of procedures.

The bug was in the FunctionTranslationStyle::Pure arm of the bytecode builder (translate_function_style): it emitted all bytecodes including trace operations (TraceLocal, TraceReturn, TraceMessage, TraceGhost). These trace operations have 0 destinations — they are side-effectful no-ops.

generate_pure_expression (called for Pure-style functions) expected all Call operations to have exactly 1 destination (since pure functions produce a value), and panicked:

unexpected 0 destinations for operation TraceLocal(0) in function nesting::table_is_good

The DebugInstrumenter emits TraceLocal for function parameters when debug_trace=true (the default for CLI usage). The chain was:

1. is_good_T (#[ext(pure)]) calls table_is_good
2. table_is_good becomes a "pure callee" → translated with Pure style
3. table_is_good's bytecode has TraceLocal(0) for parameter t (from DebugInstrumenter)
4. generate_pure_expression panics on the 0-destination Call

Fix (bytecode_translator.rs)

The FunctionTranslationStyle::Pure arm now skips trace operations before emitting bytecode, mirroring what the Asserts/Aborts style already does at line 893:

FunctionTranslationStyle::Pure => match bc {
    Call(_, _, op, _, _)
        if matches!(
            op,
            Operation::TraceLocal { .. }
                | Operation::TraceReturn { .. }
                | Operation::TraceMessage { .. }
                | Operation::TraceGhost { .. }
        ) => {} // Skip trace operations - no place in pure function translation
    _ => {
        let mut bc = bc.update_abort_action(|_| None);
        if self.targets.prover_options().bv_int_encoding {
            bc = bc.replace_cast_with_assign();
        }
        builder.emit(bc);
    }
},

Test Note

Integration tests run with debug_trace=false, so they don't trigger the exact panic path (which needs debug_trace=true). The regression test exercises the structural pattern (pure function → non-pure callee using forall!) and validates the fix doesn't break anything. The panic path is triggered in real CLI usage with default settings.