Skip to content

Commit 2ba9e17

Browse files
andreistefanescuclaude
andreistefanescu
and
claude
authored
Allow multiple loop invariants for the same function, prefer same-module (#549)
* Allow multiple loop invariants for the same function, prefer same-module When multiple modules provide a loop invariant for the same target function and label, prefer the one from the same module as the target function instead of erroring. Still errors on genuinely ambiguous cases. Moves loop invariant resolution from PackageTargets to FunctionTargetsHolder, collecting candidates during attribute scanning and resolving them at holder construction time. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * Add secondary location labels to ambiguous loop invariant errors Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * Restore flaky vec_map/remove.move.snap from main Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
1 parent 83fd4dd commit 2ba9e17

File tree

8 files changed

+164
-64
lines changed

8 files changed

+164
-64
lines changed

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

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -790,6 +790,7 @@ pub fn create_and_process_bytecode(
790790
targets.add_target(&func_env);
791791
}
792792
}
793+
targets.resolve_loop_invariants(env);
793794

794795
// Populate initial number operation state for each function and struct based on the pragma
795796
create_init_num_operation_state(env, &options.prover);
@@ -855,6 +856,7 @@ fn run_escape(env: &GlobalEnv, targets: &PackageTargets, options: &Options, now:
855856
targets.add_target(&func_env);
856857
}
857858
}
859+
targets.resolve_loop_invariants(env);
858860
println!(
859861
"Analyzing {} modules, {} declared functions, {} declared structs, {} total bytecodes",
860862
env.get_module_count(),

‎crates/move-stackless-bytecode/src/function_target_pipeline.rs‎

Lines changed: 93 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -44,6 +44,7 @@ pub struct FunctionTargetsHolder {
4444
package_targets: PackageTargets,
4545
function_specs: BiBTreeMap<QualifiedId<FunId>, QualifiedId<FunId>>,
4646
datatype_invs: BiBTreeMap<QualifiedId<DatatypeId>, QualifiedId<FunId>>,
47+
loop_invariants: BTreeMap<QualifiedId<FunId>, BiBTreeMap<QualifiedId<FunId>, usize>>,
4748
target: FunctionHolderTarget,
4849
prover_options: ProverOptions,
4950
}
@@ -186,6 +187,7 @@ impl FunctionTargetsHolder {
186187
targets: BTreeMap::new(),
187188
function_specs: BiBTreeMap::new(),
188189
datatype_invs: BiBTreeMap::new(),
190+
loop_invariants: BTreeMap::new(),
189191
prover_options,
190192
target,
191193
package_targets: package_targets.clone(),
@@ -366,11 +368,100 @@ impl FunctionTargetsHolder {
366368
self.package_targets.spec_timeouts().get(id)
367369
}
368370

371+
/// Resolve loop invariant candidates into the final map.
372+
/// When multiple invariant functions target the same (target_func, label),
373+
/// prefer the one from the same module as the spec selected by this holder.
374+
pub fn resolve_loop_invariants(&mut self, env: &GlobalEnv) {
375+
for (target_id, entries) in self.package_targets.loop_invariant_candidates() {
376+
// group by label, checking for duplicate inv_funcs
377+
let mut by_label: BTreeMap<usize, Vec<QualifiedId<FunId>>> = BTreeMap::new();
378+
let mut func_to_label: BTreeMap<QualifiedId<FunId>, usize> = BTreeMap::new();
379+
let mut has_error = false;
380+
381+
for (inv_id, label) in entries {
382+
if let Some(&existing_label) = func_to_label.get(inv_id) {
383+
if existing_label != *label {
384+
env.diag(
385+
Severity::Error,
386+
&env.get_function(*inv_id).get_loc(),
387+
&format!(
388+
"Loop invariant function {} targets multiple labels ({} and {}) in {}",
389+
env.get_function(*inv_id).get_full_name_str(),
390+
existing_label,
391+
label,
392+
env.get_function(*target_id).get_full_name_str()
393+
),
394+
);
395+
has_error = true;
396+
}
397+
continue;
398+
}
399+
func_to_label.insert(*inv_id, *label);
400+
by_label.entry(*label).or_default().push(*inv_id);
401+
}
402+
403+
if has_error {
404+
continue;
405+
}
406+
407+
// find the spec module for this target function;
408+
// if the target itself is a spec, use its own module
409+
let spec_module = self
410+
.get_spec_by_fun(target_id)
411+
.map(|spec_id| spec_id.module_id)
412+
.unwrap_or(target_id.module_id);
413+
414+
let mut resolved: BiBTreeMap<QualifiedId<FunId>, usize> = BiBTreeMap::new();
415+
416+
for (label, inv_ids) in by_label {
417+
let winner = if inv_ids.len() == 1 {
418+
inv_ids[0]
419+
} else {
420+
// prefer the invariant from the same module as the spec
421+
let in_spec_module: Vec<_> = inv_ids
422+
.iter()
423+
.filter(|id| id.module_id == spec_module)
424+
.copied()
425+
.collect();
426+
427+
if in_spec_module.len() == 1 {
428+
in_spec_module[0]
429+
} else {
430+
let labels = inv_ids
431+
.iter()
432+
.map(|id| {
433+
let f = env.get_function(*id);
434+
(f.get_loc(), f.get_full_name_str())
435+
})
436+
.collect::<Vec<_>>();
437+
env.diag_with_labels(
438+
Severity::Error,
439+
&env.get_function(*target_id).get_loc(),
440+
&format!(
441+
"Ambiguous loop invariants for label {} in {}",
442+
label,
443+
env.get_function(*target_id).get_full_name_str(),
444+
),
445+
labels,
446+
);
447+
continue;
448+
}
449+
};
450+
451+
resolved.insert(winner, label);
452+
}
453+
454+
if !resolved.is_empty() {
455+
self.loop_invariants.insert(*target_id, resolved);
456+
}
457+
}
458+
}
459+
369460
pub fn get_loop_invariants(
370461
&self,
371462
id: &QualifiedId<FunId>,
372463
) -> Option<&BiBTreeMap<QualifiedId<FunId>, usize>> {
373-
self.package_targets.loop_invariants().get(id)
464+
self.loop_invariants.get(id)
374465
}
375466

376467
pub fn get_uninterpreted_functions(
@@ -445,8 +536,7 @@ impl FunctionTargetsHolder {
445536
pub fn get_loop_inv_with_targets(
446537
&self,
447538
) -> BiBTreeMap<QualifiedId<FunId>, BTreeSet<QualifiedId<FunId>>> {
448-
self.package_targets
449-
.loop_invariants()
539+
self.loop_invariants
450540
.iter()
451541
.map(|(target_fun_id, invs)| {
452542
(

‎crates/move-stackless-bytecode/src/package_targets.rs‎

Lines changed: 9 additions & 53 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,4 @@
11
use crate::target_filter::TargetFilterOptions;
2-
use bimap::BiBTreeMap;
32
use codespan_reporting::diagnostic::Severity;
43
use move_binary_format::file_format::FunctionHandleIndex;
54
use move_compiler::{
@@ -43,7 +42,7 @@ pub struct PackageTargets {
4342
spec_uninterpreted_functions: BTreeMap<QualifiedId<FunId>, BTreeSet<QualifiedId<FunId>>>,
4443
spec_boogie_options: BTreeMap<QualifiedId<FunId>, String>,
4544
spec_timeouts: BTreeMap<QualifiedId<FunId>, u64>,
46-
loop_invariants: BTreeMap<QualifiedId<FunId>, BiBTreeMap<QualifiedId<FunId>, usize>>,
45+
loop_invariant_candidates: BTreeMap<QualifiedId<FunId>, Vec<(QualifiedId<FunId>, usize)>>,
4746
module_external_attributes: BTreeMap<ModuleId, BTreeSet<ModuleExternalSpecAttribute>>,
4847
function_external_attributes:
4948
BTreeMap<QualifiedId<FunId>, BTreeSet<ModuleExternalSpecAttribute>>,
@@ -82,7 +81,7 @@ impl PackageTargets {
8281
spec_uninterpreted_functions: BTreeMap::new(),
8382
spec_boogie_options: BTreeMap::new(),
8483
spec_timeouts: BTreeMap::new(),
85-
loop_invariants: BTreeMap::new(),
84+
loop_invariant_candidates: BTreeMap::new(),
8685
module_external_attributes: BTreeMap::new(),
8786
function_external_attributes: BTreeMap::new(),
8887
module_extra_bpl: BTreeMap::new(),
@@ -200,53 +199,10 @@ impl PackageTargets {
200199
if let Some(target_func_env) =
201200
module_env.find_function(func_env.symbol_pool().make(fun_name.as_str()))
202201
{
203-
if let Some(existing) = self
204-
.loop_invariants
205-
.get_mut(&target_func_env.get_qualified_id())
206-
{
207-
match existing.insert(func_env.get_qualified_id(), label) {
208-
bimap::Overwritten::Neither => {}
209-
bimap::Overwritten::Left(..) => {
210-
env.diag(
211-
Severity::Error,
212-
&func_env.get_loc(),
213-
&format!(
214-
"Duplicated Loop Invariant Function {} in {}",
215-
func_env.get_full_name_str(),
216-
fun_name
217-
),
218-
);
219-
return;
220-
}
221-
bimap::Overwritten::Right(..) => {
222-
env.diag(
223-
Severity::Error,
224-
&func_env.get_loc(),
225-
&format!("Duplicated Loop Invariant Label {} in {}", label, fun_name),
226-
);
227-
return;
228-
}
229-
bimap::Overwritten::Both(..) | bimap::Overwritten::Pair(..) => {
230-
env.diag(
231-
Severity::Error,
232-
&func_env.get_loc(),
233-
&format!(
234-
"Duplicated Loop Invariant Function {} and Label {} in {}",
235-
func_env.get_full_name_str(),
236-
label,
237-
fun_name
238-
),
239-
);
240-
}
241-
}
242-
} else {
243-
self.loop_invariants
244-
.insert(target_func_env.get_qualified_id(), {
245-
let mut map = BiBTreeMap::new();
246-
map.insert(func_env.get_qualified_id(), label);
247-
map
248-
});
249-
}
202+
self.loop_invariant_candidates
203+
.entry(target_func_env.get_qualified_id())
204+
.or_default()
205+
.push((func_env.get_qualified_id(), label));
250206
} else {
251207
env.diag(
252208
Severity::Error,
@@ -1011,10 +967,10 @@ impl PackageTargets {
1011967
&self.spec_timeouts
1012968
}
1013969

1014-
pub fn loop_invariants(
970+
pub fn loop_invariant_candidates(
1015971
&self,
1016-
) -> &BTreeMap<QualifiedId<FunId>, BiBTreeMap<QualifiedId<FunId>, usize>> {
1017-
&self.loop_invariants
972+
) -> &BTreeMap<QualifiedId<FunId>, Vec<(QualifiedId<FunId>, usize)>> {
973+
&self.loop_invariant_candidates
1018974
}
1019975

1020976
pub fn get_module_extra_bpl(&self, module_id: &ModuleId) -> Option<&String> {

‎crates/move-stackless-bytecode/tests/testsuite.rs‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -195,6 +195,7 @@ fn test_runner(path: &Path) -> datatest_stable::Result<()> {
195195
targets.add_target(&func_env);
196196
}
197197
}
198+
targets.resolve_loop_invariants(&env);
198199
let show_livevars = std::env::var("STACKLESS_TEST_SHOW_LIVENESS").is_ok();
199200
let show_borrow = true;
200201
let show_reach = std::env::var("STACKLESS_TEST_SHOW_REACHING_DEFS").is_ok();

‎crates/sui-prover/src/build_model.rs‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -126,6 +126,7 @@ pub fn build_model_with_target(
126126
targets.add_target(&func_env);
127127
}
128128
}
129+
targets.resolve_loop_invariants(&model);
129130

130131
Ok((model, rerooted_path, targets))
131132
}

‎crates/sui-prover/tests/inputs/loop_invariant/external_multi_module.ok.move‎

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
// Two modules provide a loop invariant for the same spec function.
2+
// The invariant in the same module as the spec should be selected.
3+
module 0x42::other_specs {
4+
#[allow(unused_variable)]
5+
#[spec_only(loop_inv(target = 0x42::my_specs::test_spec))]
6+
#[ext(no_abort)]
7+
fun loop_inv_other(i: u64, n: u64): bool {
8+
// This invariant is intentionally too weak; it would fail if selected.
9+
true
10+
}
11+
}
12+
13+
module 0x42::my_specs {
14+
use prover::prover::ensures;
15+
16+
#[spec_only(loop_inv(target = test_spec))]
17+
#[ext(no_abort)]
18+
fun loop_inv(i: u64, n: u64): bool {
19+
i <= n
20+
}
21+
22+
#[spec(prove)]
23+
fun test_spec(n: u64) {
24+
let mut i = 0;
25+
26+
while (i < n) {
27+
i = i + 1;
28+
};
29+
30+
ensures(i == n);
31+
}
32+
}

‎crates/sui-prover/tests/snapshots/loop_invariant/external_multi_module.ok.move.snap‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
---
2+
source: crates/sui-prover/tests/integration.rs
3+
expression: output
4+
---
5+
Verification successful

‎crates/sui-prover/tests/snapshots/loop_invariant/external_wrong_label_2.fail.move.snap‎

Lines changed: 21 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,26 @@
11
---
22
source: crates/sui-prover/tests/integration.rs
3-
assertion_line: 262
43
expression: output
54
---
65
exiting with bytecode transformation errors
7-
error: Duplicated Loop Invariant Label 0 in test_spec
8-
┌─ tests/inputs/loop_invariant/external_wrong_label_2.fail.move:13:1
9-
│
10-
13 │ ╭ fun loop_inv_2(i: u64, n: u64, s: u128): bool {
11-
14 │ │ i <= n && (s == (i as u128) * ((i as u128) + 1) / 2)
12-
15 │ │ }
13-
│ ╰─^
6+
error: Ambiguous loop invariants for label 0 in loop_invariant_external_wrong_label_2_fail::test_spec
7+
┌─ tests/inputs/loop_invariant/external_wrong_label_2.fail.move:18:1
8+
│
9+
7 │ ╭ fun loop_inv_1(i: u64, n: u64, s: u128): bool {
10+
8 │ │ i <= n && (s == (i as u128) * ((i as u128) + 1) / 2)
11+
9 │ │ }
12+
│ ╰───' loop_invariant_external_wrong_label_2_fail::loop_inv_1
13+
· │
14+
13 │ ╭ fun loop_inv_2(i: u64, n: u64, s: u128): bool {
15+
14 │ │ i <= n && (s == (i as u128) * ((i as u128) + 1) / 2)
16+
15 │ │ }
17+
│ ╰─' loop_invariant_external_wrong_label_2_fail::loop_inv_2
18+
· │
19+
18 │ ╭ fun test_spec(n: u64): u128 {
20+
19 │ │ let mut s: u128 = 0;
21+
20 │ │ let mut i = 0;
22+
21 │ │
23+
· │
24+
28 │ │ s
25+
29 │ │ }
26+
│ ╰─────^

0 commit comments

Comments
 (0)