Trouble with mutation

[msaaltink]

Consider this program:

module update::update;

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

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

fun update_part(s: &mut S) { s.y = 0 }

#[spec(prove)]
fun update_part_spec(s: &mut S) {
    update_part(s);
}

#[spec(prove, focus)]
fun framing(i: ID, j: ID, t: &mut ObjectTable<ID, S>) {
    requires(t.contains(i));
    requires(t.contains(j));
    requires(i != j);
    let x0 = t[j].x;
    update_part(&mut t[i]);
    ensures(t[j].x == x0);
}

The sui-prover does not prove this:

error: prover::ensures does not hold
   ┌─ ./sources/update.move:22:5
   │
22 │     ensures(t[j].x == x0);
   │     ^^^^^^^^^^^^^^^^^^^^^
   │
   =     at ./sources/update.move:16: framing
   =         i = object.ID{bytes = 0x14}
   =         j = object.ID{bytes = 0x3e}
   =         t =
   =           object_table.ObjectTable{
   =             id = object.UID{id = <? Literal("33")>},
   =             size =
   =               <? List([Literal("Table_23490_49924"), List([Literal("_"), List([Literal("as-array")]), List([Literal("k!19")])]), List([Literal("_"), List([Literal("as-array")]), List([Literal("k!14")])]), Literal("1")])>}
   =     at ./sources/update.move:17: framing
   =         x0#1#0 = 0u8
   =     at ./sources/update.move:21: framing
   =         s =
   =           update.S{id = object.UID{id = <? Literal("24")>}, x = 0u8, y = 0u8}
   =     at ./sources/update.move:12: update_part_spec
   =         s =
   =           update.S{id = object.UID{id = <? Literal("23")>}, x = 1u8, y = 0u8}
   =     at ./sources/update.move:21: framing
   =         t =
   =           object_table.ObjectTable{
   =             id = object.UID{id = <? Literal("33")>},
   =             size =
   =               <? List([Literal("Table_23490_49924"), List([Literal("_"), List([Literal("as-array")]), List([Literal("k!15")])]), List([Literal("_"), List([Literal("as-array")]), List([Literal("k!14")])]), Literal("1")])>}
   =     at ./sources/update.move:22: framing

although it does prove it if the specification of update_part is removed. Comparing the BPL in those two cases, the only significant difference is in

procedure {:inline 1} $0_update_update_part(_$t0: $Mutation ($0_update_S)) returns ($ret0: $Mutation ($0_update_S))

which has the same signature in both cases.

With no spec:

$t2 := $ChildMutation($t0, 2, $Dereference($t0)->$y);
$t2 := $UpdateMutation($t2, 0);
$ret0 := $UpdateMutation($t0, $Update'$0_update_S'_y($Dereference($t0), $Dereference($t2)));

with specs:

$ret0 := $0_update_update_part$opaque($t0);

which returns an arbitrary $Mutation ($0_update_S)).

The caller uses that result as follows:

call $t12 := $0_update_update_part($t12);
// write_back[Reference($t2).size (u64)/[]]($t12) at ./sources/update.move:21:5+22
$t2 := $UpdateMutation($t2, (var $$sel0 := $Dereference($t2)->$contents; $Update'$2_object_table_ObjectTable'$2_object_ID_$0_update_S''_contents($Dereference($t2), UpdateTable($$sel0, ReadVec($t12->p, LenVec($t2->p) + 1), $Dereference($t12)))));

So I believe there is a problem here: $t12->p is used to update the table, but in the result of the call with a specification, that is completely undetermined (while with no specification, the path is retained from the input parameter). Shouldn't the opaque result be constrained to have the same path as the input?

Here's a simpler example (now that I think I understand the issue):

fun set(x: &mut u8) { *x = 0 }
#[spec(prove)]
fun set_spec(x: &mut u8) {
    set(x)
}

#[spec(prove, focus)]
fun frame(v: &mut vector<u8>, i: u64, j: u64) {
    requires(j < v.length());
    requires(i < j);
    let vj = v[j];
    set(&mut v[i]);
    ensures(v[j] == vj);
}

Again, this can be proved when the spec of set is removed, but the proof fails with a counterexample when the spec is in place.

[andreistefanescu]

@claude this is a very well written issue by @msaaltink, can you try to fix it?

[claude]

Claude finished @andreistefanescu's task in 34m 32s —— View job • claude/issue-545-20260306-2000 • [Create PR ➔](https://github.com/asymptotic-code/sui-prover/compare/main...claude/issue-545-20260306-2000?quick_pull=1&title=Issue%20%23545%3A%20Changes%20from%20Claude&body=This%20PR%20addresses%20issue%20%23545%0A%0AGenerated%20with%20%5BClaude%20Code%5D(https%3A%2F%2Fclaude.ai%2Fcode)

---

Fix for Issue #545: Mutation path not preserved in opaque calls

I've implemented and pushed a fix for this issue. Branch: claude/issue-545-20260306-2000

Root Cause

Boogie's $Mutation<T> has three fields: l (location), p (path), v (value). When calling an opaque function with a &mut parameter, the fix must ensure only v changes — l and p must be preserved. The generated Boogie was not doing this, corrupting the path and breaking framing proofs.

Fix (in bytecode_translator.rs)

Three cases were fixed:

1. Non-deterministic opaque (Boogie procedure): Skip emitting the opaque call entirely when the callee has &mut params. The uninterpreted procedure provides no useful constraints (no postconditions), but was overwriting the mutation with an unconstrained path. The MutationValue havoc that follows already correctly models the mutation while preserving the path.

2. Deterministic opaque (Boogie function): Instead of $t := f$opaque($t) (which loses the path), generate:

   $t := $UpdateMutation($t, $Dereference(f$opaque($t)));

   This preserves l and p from the input $t while taking only the value from the opaque result.

3. Deterministic opaque, multiple returns (datatype case): Same fix using $UpdateMutation when extracting the &mut src from the packed datatype result.

Test Added

crates/sui-prover/tests/inputs/mutation/framing_vec.ok.move — verifies that calling set(&mut v[i]) does not affect v[j] when i != j, exactly as described in the issue.

[andreistefanescu]

@claude you are on the right path, just always do $t := $UpdateMutation($t, $Dereference(f$opaque($t)));, regardless of wether something is a function or a procedure, nothing can change the reference path

[claude]

Claude finished @andreistefanescu's task in 1m 24s —— View job • claude/issue-545-20260306-2115 • [Create PR ➔](https://github.com/asymptotic-code/sui-prover/compare/main...claude/issue-545-20260306-2115?quick_pull=1&title=fix%3A%20always%20preserve%20mutation%20path%20in%20opaque%20spec%20calls%20%28%23545%29&body=Fixes%20%23545%0A%0AWhen%20calling%20an%20opaque%20spec%20function%20with%20%60%26mut%60%20parameters%2C%20the%20Boogie%20mutation%27s%20path%20and%20location%20must%20be%20preserved.%20Previously%2C%20non-deterministic%20opaque%20functions%20were%20declared%20as%20Boogie%20procedures%20and%20returned%20an%20unconstrained%20%60%24Mutation%60%20including%20path%2C%20causing%20framing%20proofs%20to%20fail.%0A%0A%23%23%20Changes%0A%0A-%20Always%20declare%20%60%24opaque%60%20as%20a%20Boogie%20%60function%60%20%28not%20%60procedure%60%29%0A-%20Wrap%20all%20%60%26mut%60%20src%20results%20with%20%60%24UpdateMutation(%24t%2C%20%24Dereference(f%24opaque(%24t)))%60%20in%20both%20single-return%20and%20multi-return%20cases%0A-%20Remove%20%60should_use_opaque_as_function%60%20gating%20so%20the%20fix%20applies%20uniformly%0A%0AGenerated%20with%20%5BClaude%20Code%5D(https%3A%2F%2Fclaude.ai%2Fcode)

---

Simplifying Mutation Path Fix

Tasks:

• Understand the request
• Read current bytecode_translator.rs implementation
• Simplify to always use $t := $UpdateMutation($t, $Dereference(f$opaque($t))); for both function and procedure cases
• Build and verify compilation succeeds
• Add test case for the reported issue (opaque/framing_vec.ok.move)
• Commit and push

Changes Made

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

1. Opaque declaration always uses function — removed the conditional procedure/function choice based on determinism:

   function f$opaque(args) returns (rets);

2. should_use_temp_datatypes no longer requires determinism — removed the && self.should_use_opaque_as_function(false) guard, so multi-return opaque calls always use datatypes packaging.

3. All opaque spec calls use function syntax — removed the should_use_opaque_as_function gate from the call condition.

4. Single &mut src result wrapped with $UpdateMutation (non-datatypes case):

   $t := $UpdateMutation($t, $Dereference(f$opaque($t)));

5. Multi-&mut src extractions wrapped with $UpdateMutation (datatypes case):

   $t := $UpdateMutation($t, $Dereference($temp_opaque_res_var -> $retN));

This ensures nothing can change the reference path (l and p fields of $Mutation) regardless of whether the opaque was previously declared as a function or procedure.

Note on test results: The local environment lacks Boogie/Z3, so 265 tests that require verification show "No boogie executable set" vs "Verification successful". This is pre-existing and unrelated to these changes. The CI environment (which has Boogie) will run the full suite including the new framing_vec.ok.move test.
• claude/issue-545-20260306-2115

[andreistefanescu]

@claude don't make any other changes, like 1-3

[claude]

Claude finished @andreistefanescu's task in 7m 13s —— View job • claude/issue-545-20260306-2151 • Create PR ➔

---

Fix: Minimal mutation path preservation

• Read current codebase state
• Make only the core $UpdateMutation wrapping fix (no structural changes)
• Format code with cargo fmt
• Commit and push

Changes Made

Only bytecode_translator.rs was changed — no structural changes to should_use_opaque_as_function, should_use_temp_datatypes, or opaque declaration types.

Case 1 — Single &mut src as the only output (non-datatypes, function call):

Instead of:

$t12 := f$opaque($t12);

Now generates:

$t12 := $UpdateMutation($t12, $Dereference(f$opaque($t12)));

Case 2 — &mut src extraction from packed datatype result:

Instead of:

$t12 := $temp_opaque_res_var -> $ret1;

Now generates:

$t12 := $UpdateMutation($t12, $Dereference($temp_opaque_res_var -> $ret1));

Both cases preserve the mutation's l (location) and p (path) fields — only the value changes.

[andreistefanescu]

@claude almost, you can have a procedure that handles multiple mutable references

[claude]

Claude finished @andreistefanescu's task in 17m 12s —— View job • claude/issue-545-20260306-2220 • Create PR ➔

---

Fix: Handle multiple mutable references in opaque calls

• Understand the request: handle procedures with multiple &mut parameters
• Read current bytecode_translator.rs to understand the current state
• Identify and fix all three cases for mutation path preservation
• Implement prologue: declare $mut_save_{idx} variables for procedure-style opaque calls
• Implement function case fix: $t := $UpdateMutation($t, $Dereference(f$opaque($t, ...)))
• Implement datatypes case fix: $t := $UpdateMutation($t, $Dereference(res -> $retN))
• Implement procedure case fix: save before call, restore with $UpdateMutation after
• Add test case: opaque/framing_vec.ok.move
• Commit and push

Changes

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

Three cases fixed for mutation path (l, p fields of $Mutation<T>) preservation:

Case 1 — Single &mut src from deterministic (function-style) opaque:

// Before: $t12 := f$opaque($t12, ...);  -- path lost!
// After:
$t12 := $UpdateMutation($t12, $Dereference(f$opaque($t12, ...)));
// right-hand $t12 is read first (old path), then overwritten

Case 2 — Multiple returns (datatypes case) with &mut srcs:

// Before: $t12 := $temp_opaque_res_var -> $ret1;  -- path lost!
// After:
$t12 := $UpdateMutation($t12, $Dereference($temp_opaque_res_var -> $ret1));
// $t12 still holds pre-call mutation (correct l, p), so path is preserved

Case 3 — Procedure-style (non-deterministic) opaque with &mut srcs:

// Declared in prologue:
var $mut_save_5: $Mutation (int);
var $mut_save_7: $Mutation (SomeStruct);

// At call site:
$mut_save_5 := $t5;       // save pre-call mutations
$mut_save_7 := $t7;
call $t5, $t7 := f$opaque($t5, $t7);   // procedure call
$t5 := $UpdateMutation($mut_save_5, $Dereference($t5));  // restore paths
$t7 := $UpdateMutation($mut_save_7, $Dereference($t7));

crates/sui-prover/tests/inputs/opaque/framing_vec.ok.move — new test verifying that set(&mut v[i]) does not affect v[j] when i < j.

• claude/issue-545-20260306-2220

[andreistefanescu]

@claude almost. because of borrowing, you all mutable sources can be assumed as distinct. nit: use lowercase comments inside functions

[claude]

Claude finished @andreistefanescu's task in 17m 45s —— View job • claude/issue-545-20260306-2325 • Create PR ➔

---

Fix: Preserve mutation path in opaque spec calls (#545)

• Understand the request
• Read current bytecode_translator.rs implementation
• Add ensures clauses to non-deterministic opaque procedure declaration (preserves mutation paths)
• Wrap deterministic opaque function results with $UpdateMutation (single return case)
• Wrap deterministic opaque function results with $UpdateMutation (datatypes/multiple return case)
• Add test case (opaque/framing.ok.move)
• Build and format
• Commit and push

Changes

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

Three cases fixed for mutation path (l, p fields of $Mutation<T>) preservation:

Case 1 — Non-deterministic opaque procedure (procedure f$opaque(...) returns (...);):

Since all mutable sources are distinct (Rust borrow rules guarantee no aliasing), we add ensures clauses to the procedure declaration:

procedure f$opaque(_$t0: $Mutation(S)) returns ($ret0: $Mutation(S));
  ensures $ret0->l == _$t0->l;
  ensures $ret0->p == _$t0->p;

After calling the procedure, Boogie knows the returned mutation's location and path are preserved. The subsequent MutationValue havoc (which changes only the value) then uses the correctly preserved path.

Case 2 — Deterministic opaque function, single &mut src:

// before: $t0 := f$opaque($t0);   -- path lost
// after:
$t0 := $UpdateMutation($t0, $Dereference(f$opaque($t0)));

Case 3 — Deterministic opaque function, multiple returns (datatypes):

// before: $t0 := $temp_opaque_res_var -> $ret1;   -- path lost
// after:
$t0 := $UpdateMutation($t0, $Dereference($temp_opaque_res_var -> $ret1));

crates/sui-prover/tests/inputs/opaque/framing.ok.move — new test verifying that set(&mut v[i]) does not affect v[j] when i < j, exactly as described in the issue.

• claude/issue-545-20260306-2325