From db3fb8a97f9b62149b0e7b812453f7a04e21abbd Mon Sep 17 00:00:00 2001 From: "claude[bot]" <41898282+claude[bot]@users.noreply.github.com> Date: Tue, 10 Mar 2026 21:03:02 +0000 Subject: [PATCH 1/3] feat: implement #[ext(uninterpreted)] global annotation and interpreted=foo per-spec override MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Add globally_uninterpreted_functions to PackageTargets: functions annotated with #[ext(pure, uninterpreted)] are treated as uninterpreted in all verified specs by default - Add spec_interpreted_functions to PackageTargets: #[spec(prove, interpreted=foo)] opts a spec out of the global uninterpreted default for that specific spec only - Update check_abort_check_scope to detect #[ext(uninterpreted)] and validate that #[ext(pure)] is also present (error otherwise) - Update check_uninterpreted_scope to also process interpreted field from VerificationAttribute::Spec, validating that the target is globally uninterpreted - Update is_uninterpreted_for_spec() with 3-tier logic: 1. spec's interpreted list → return false (per-spec override) 2. globally_uninterpreted_functions → return true (global default) 3. spec-local uninterpreted list → existing behavior - Add 4 test cases covering: no-pure error, global default, interpreted override, and interpreted-wrong-target error Closes #547 Co-authored-by: andrii-a8c --- .../src/package_targets.rs | 126 ++++++++++++++++-- .../ext_interpreted_override.ok.move | 22 +++ .../ext_interpreted_wrong_target.fail.move | 19 +++ .../ext_uninterpreted_default.ok.move | 21 +++ .../ext_uninterpreted_no_pure.fail.move | 19 +++ 5 files changed, 198 insertions(+), 9 deletions(-) create mode 100644 crates/sui-prover/tests/inputs/uninterpreted/ext_interpreted_override.ok.move create mode 100644 crates/sui-prover/tests/inputs/uninterpreted/ext_interpreted_wrong_target.fail.move create mode 100644 crates/sui-prover/tests/inputs/uninterpreted/ext_uninterpreted_default.ok.move create mode 100644 crates/sui-prover/tests/inputs/uninterpreted/ext_uninterpreted_no_pure.fail.move diff --git a/crates/move-stackless-bytecode/src/package_targets.rs b/crates/move-stackless-bytecode/src/package_targets.rs index a5a3e0264e..eb094ea122 100644 --- a/crates/move-stackless-bytecode/src/package_targets.rs +++ b/crates/move-stackless-bytecode/src/package_targets.rs @@ -38,8 +38,12 @@ pub struct PackageTargets { omit_opaque_specs: BTreeSet>, focus_specs: BTreeSet>, scenario_specs: BTreeSet>, + // functions that are globally uninterpreted (annotated with #[ext(uninterpreted)]). + globally_uninterpreted_functions: BTreeSet>, // functions that should be uninterpreted when verifying a specific spec function. spec_uninterpreted_functions: BTreeMap, BTreeSet>>, + // per-spec override: functions that should be interpreted (not uninterpreted) for a spec. + spec_interpreted_functions: BTreeMap, BTreeSet>>, spec_boogie_options: BTreeMap, String>, spec_timeouts: BTreeMap, u64>, loop_invariant_candidates: BTreeMap, Vec<(QualifiedId, usize)>>, @@ -78,7 +82,9 @@ impl PackageTargets { omit_opaque_specs: BTreeSet::new(), focus_specs: BTreeSet::new(), scenario_specs: BTreeSet::new(), + globally_uninterpreted_functions: BTreeSet::new(), spec_uninterpreted_functions: BTreeMap::new(), + spec_interpreted_functions: BTreeMap::new(), spec_boogie_options: BTreeMap::new(), spec_timeouts: BTreeMap::new(), loop_invariant_candidates: BTreeMap::new(), @@ -524,10 +530,17 @@ impl PackageTargets { .get_(&AttributeKind_::External) .map(|attr| &attr.value) { - if attrs + let has_no_abort = attrs .into_iter() - .any(|attr| attr.2.value.name().value.as_str() == "no_abort") - { + .any(|attr| attr.2.value.name().value.as_str() == "no_abort"); + let has_pure = attrs + .into_iter() + .any(|attr| attr.2.value.name().value.as_str() == "pure"); + let has_uninterpreted = attrs + .into_iter() + .any(|attr| attr.2.value.name().value.as_str() == "uninterpreted"); + + if has_no_abort { self.abort_check_functions .insert(func_env.get_qualified_id()); if self.is_target(func_env) { @@ -535,21 +548,35 @@ impl PackageTargets { .insert(func_env.get_qualified_id()); } } - if attrs - .into_iter() - .any(|attr| attr.2.value.name().value.as_str() == "pure") - { + if has_pure { self.pure_functions.insert(func_env.get_qualified_id()); if self.is_target(func_env) { self.target_no_abort_check_functions .insert(func_env.get_qualified_id()); } } + if has_uninterpreted { + if !has_pure { + let env = func_env.module_env.env; + env.diag( + Severity::Error, + &func_env.get_loc(), + &format!( + "#[ext(uninterpreted)] on '{}' requires #[ext(pure)]", + func_env.get_full_name_str(), + ), + ); + } else { + self.globally_uninterpreted_functions + .insert(func_env.get_qualified_id()); + } + } } } - /// Process uninterpreted attributes with validation. - /// This runs after check_abort_check_scope, so pure_functions is complete and we can validate. + /// Process uninterpreted/interpreted attributes with validation. + /// This runs after check_abort_check_scope, so pure_functions and + /// globally_uninterpreted_functions are complete and we can validate. fn check_uninterpreted_scope(&mut self, func_env: &FunctionEnv) { let env = func_env.module_env.env; if let Some(KnownAttribute::Verification(VerificationAttribute::Spec { @@ -565,6 +592,7 @@ impl PackageTargets { explicit_specs: _, extra_bpl: _, uninterpreted, + interpreted, .. })) = func_env .get_toplevel_attributes() @@ -631,6 +659,65 @@ impl PackageTargets { } } } + + for module_access in interpreted { + match Self::parse_module_access(module_access, &func_env.module_env) { + Some((module_name, fun_name)) => { + if let Some(target_module_env) = env.find_module(&module_name) { + if let Some(target_func_env) = + target_module_env.find_function(env.symbol_pool().make(&fun_name)) + { + // Validate that the target is globally uninterpreted + if !self + .globally_uninterpreted_functions + .contains(&target_func_env.get_qualified_id()) + { + env.diag( + Severity::Error, + &func_env.get_loc(), + &format!( + "interpreted target '{}' must be marked with #[ext(uninterpreted)]", + target_func_env.get_full_name_str(), + ), + ); + continue; + } + + self.spec_interpreted_functions + .entry(func_env.get_qualified_id()) + .or_insert_with(BTreeSet::new) + .insert(target_func_env.get_qualified_id()); + } else { + env.diag( + Severity::Error, + &func_env.get_loc(), + &format!( + "interpreted target function '{}' not found in module '{}'", + fun_name, + target_module_env.get_full_name_str(), + ), + ); + } + } else { + env.diag( + Severity::Error, + &func_env.get_loc(), + &format!( + "interpreted target module not found for path '{}'", + module_name.display(env.symbol_pool()) + ), + ); + } + } + None => { + env.diag( + Severity::Error, + &func_env.get_loc(), + "Error parsing interpreted target path", + ); + } + } + } } } @@ -1000,11 +1087,32 @@ impl PackageTargets { spec_id: &QualifiedId, callee_id: &QualifiedId, ) -> bool { + // If this spec explicitly opts in to interpreting the function, it is not uninterpreted. + if self + .spec_interpreted_functions + .get(spec_id) + .map_or(false, |set| set.contains(callee_id)) + { + return false; + } + // If the function is globally uninterpreted, it is uninterpreted for this spec. + if self.globally_uninterpreted_functions.contains(callee_id) { + return true; + } + // Fall back to spec-local uninterpreted list. self.spec_uninterpreted_functions .get(spec_id) .map_or(false, |set| set.contains(callee_id)) } + pub fn is_globally_uninterpreted(&self, func_id: &QualifiedId) -> bool { + self.globally_uninterpreted_functions.contains(func_id) + } + + pub fn globally_uninterpreted_functions(&self) -> &BTreeSet> { + &self.globally_uninterpreted_functions + } + pub fn spec_uninterpreted_functions( &self, ) -> &BTreeMap, BTreeSet>> { diff --git a/crates/sui-prover/tests/inputs/uninterpreted/ext_interpreted_override.ok.move b/crates/sui-prover/tests/inputs/uninterpreted/ext_interpreted_override.ok.move new file mode 100644 index 0000000000..bad966b75e --- /dev/null +++ b/crates/sui-prover/tests/inputs/uninterpreted/ext_interpreted_override.ok.move @@ -0,0 +1,22 @@ +/// bar() is globally uninterpreted by default. +/// foo_spec_a cannot prove bar() == 42 (uninterpreted), but +/// foo_spec_b uses interpreted=bar to get the actual value and can prove bar() == 42. +module 0x42::foo; + +use prover::prover::ensures; + +#[ext(pure, uninterpreted)] +fun bar(): u64 { + 42 +} + +fun foo(): u64 { + bar() +} + +#[spec(prove, interpreted = bar)] +fun foo_spec(): u64 { + let result = foo(); + ensures(result == 42); // passes: bar is interpreted here, so foo() == bar() == 42 + result +} diff --git a/crates/sui-prover/tests/inputs/uninterpreted/ext_interpreted_wrong_target.fail.move b/crates/sui-prover/tests/inputs/uninterpreted/ext_interpreted_wrong_target.fail.move new file mode 100644 index 0000000000..f4c38cdaec --- /dev/null +++ b/crates/sui-prover/tests/inputs/uninterpreted/ext_interpreted_wrong_target.fail.move @@ -0,0 +1,19 @@ +module 0x42::foo; + +use prover::prover::ensures; + +#[ext(pure)] // pure but NOT globally uninterpreted +fun bar(): u64 { + 42 +} + +fun foo(): u64 { + bar() +} + +#[spec(prove, interpreted = bar)] // should error: bar is not #[ext(uninterpreted)] +fun foo_spec(): u64 { + let result = foo(); + ensures(result == 42); + result +} diff --git a/crates/sui-prover/tests/inputs/uninterpreted/ext_uninterpreted_default.ok.move b/crates/sui-prover/tests/inputs/uninterpreted/ext_uninterpreted_default.ok.move new file mode 100644 index 0000000000..3ce2d6220f --- /dev/null +++ b/crates/sui-prover/tests/inputs/uninterpreted/ext_uninterpreted_default.ok.move @@ -0,0 +1,21 @@ +/// bar() is globally uninterpreted. The spec can prove bar() == bar() (reflexivity), +/// but cannot prove bar() == 42 (the actual implementation is hidden). +module 0x42::foo; + +use prover::prover::ensures; + +#[ext(pure, uninterpreted)] +fun bar(): u64 { + 42 +} + +fun foo(): u64 { + bar() +} + +#[spec(prove)] +fun foo_spec(): u64 { + let result = foo(); + ensures(result == bar()); // passes: both calls are the same uninterpreted value + result +} diff --git a/crates/sui-prover/tests/inputs/uninterpreted/ext_uninterpreted_no_pure.fail.move b/crates/sui-prover/tests/inputs/uninterpreted/ext_uninterpreted_no_pure.fail.move new file mode 100644 index 0000000000..07a0932e67 --- /dev/null +++ b/crates/sui-prover/tests/inputs/uninterpreted/ext_uninterpreted_no_pure.fail.move @@ -0,0 +1,19 @@ +module 0x42::foo; + +use prover::prover::ensures; + +#[ext(uninterpreted)] // should error: missing #[ext(pure)] +fun bar(): u64 { + 42 +} + +fun foo(): u64 { + bar() +} + +#[spec(prove)] +fun foo_spec(): u64 { + let result = foo(); + ensures(result == bar()); + result +} From 0f18c9bdc9b863142fd92052256f6ce3cee51503 Mon Sep 17 00:00:00 2001 From: "claude[bot]" <41898282+claude[bot]@users.noreply.github.com> Date: Tue, 10 Mar 2026 21:43:09 +0000 Subject: [PATCH 2/3] fix: remove uncompilable interpreted field reference from package_targets The `interpreted` field does not exist in `VerificationAttribute::Spec` in the current move_compiler dependency (commit 4c8b2c98). Remove the pattern match on this missing field and the associated processing block. The per-spec `interpreted=foo` override feature requires an upstream change to asymptotic-code/sui to add the field before it can be enabled. Also remove test files that depend on this unimplemented feature (`ext_interpreted_override.ok.move`, `ext_interpreted_wrong_target.fail.move`) and add snapshots for the working tests (`ext_uninterpreted_default.ok.move`, `ext_uninterpreted_no_pure.fail.move`). Co-authored-by: andrii-a8c --- .../src/package_targets.rs | 68 ------------------- .../ext_interpreted_override.ok.move | 22 ------ .../ext_interpreted_wrong_target.fail.move | 19 ------ .../ext_uninterpreted_default.ok.move.snap | 5 ++ .../ext_uninterpreted_no_pure.fail.move.snap | 13 ++++ 5 files changed, 18 insertions(+), 109 deletions(-) delete mode 100644 crates/sui-prover/tests/inputs/uninterpreted/ext_interpreted_override.ok.move delete mode 100644 crates/sui-prover/tests/inputs/uninterpreted/ext_interpreted_wrong_target.fail.move create mode 100644 crates/sui-prover/tests/snapshots/uninterpreted/ext_uninterpreted_default.ok.move.snap create mode 100644 crates/sui-prover/tests/snapshots/uninterpreted/ext_uninterpreted_no_pure.fail.move.snap diff --git a/crates/move-stackless-bytecode/src/package_targets.rs b/crates/move-stackless-bytecode/src/package_targets.rs index eb094ea122..9c3d35437e 100644 --- a/crates/move-stackless-bytecode/src/package_targets.rs +++ b/crates/move-stackless-bytecode/src/package_targets.rs @@ -38,11 +38,9 @@ pub struct PackageTargets { omit_opaque_specs: BTreeSet>, focus_specs: BTreeSet>, scenario_specs: BTreeSet>, - // functions that are globally uninterpreted (annotated with #[ext(uninterpreted)]). globally_uninterpreted_functions: BTreeSet>, // functions that should be uninterpreted when verifying a specific spec function. spec_uninterpreted_functions: BTreeMap, BTreeSet>>, - // per-spec override: functions that should be interpreted (not uninterpreted) for a spec. spec_interpreted_functions: BTreeMap, BTreeSet>>, spec_boogie_options: BTreeMap, String>, spec_timeouts: BTreeMap, u64>, @@ -574,9 +572,6 @@ impl PackageTargets { } } - /// Process uninterpreted/interpreted attributes with validation. - /// This runs after check_abort_check_scope, so pure_functions and - /// globally_uninterpreted_functions are complete and we can validate. fn check_uninterpreted_scope(&mut self, func_env: &FunctionEnv) { let env = func_env.module_env.env; if let Some(KnownAttribute::Verification(VerificationAttribute::Spec { @@ -592,7 +587,6 @@ impl PackageTargets { explicit_specs: _, extra_bpl: _, uninterpreted, - interpreted, .. })) = func_env .get_toplevel_attributes() @@ -659,65 +653,6 @@ impl PackageTargets { } } } - - for module_access in interpreted { - match Self::parse_module_access(module_access, &func_env.module_env) { - Some((module_name, fun_name)) => { - if let Some(target_module_env) = env.find_module(&module_name) { - if let Some(target_func_env) = - target_module_env.find_function(env.symbol_pool().make(&fun_name)) - { - // Validate that the target is globally uninterpreted - if !self - .globally_uninterpreted_functions - .contains(&target_func_env.get_qualified_id()) - { - env.diag( - Severity::Error, - &func_env.get_loc(), - &format!( - "interpreted target '{}' must be marked with #[ext(uninterpreted)]", - target_func_env.get_full_name_str(), - ), - ); - continue; - } - - self.spec_interpreted_functions - .entry(func_env.get_qualified_id()) - .or_insert_with(BTreeSet::new) - .insert(target_func_env.get_qualified_id()); - } else { - env.diag( - Severity::Error, - &func_env.get_loc(), - &format!( - "interpreted target function '{}' not found in module '{}'", - fun_name, - target_module_env.get_full_name_str(), - ), - ); - } - } else { - env.diag( - Severity::Error, - &func_env.get_loc(), - &format!( - "interpreted target module not found for path '{}'", - module_name.display(env.symbol_pool()) - ), - ); - } - } - None => { - env.diag( - Severity::Error, - &func_env.get_loc(), - "Error parsing interpreted target path", - ); - } - } - } } } @@ -1087,7 +1022,6 @@ impl PackageTargets { spec_id: &QualifiedId, callee_id: &QualifiedId, ) -> bool { - // If this spec explicitly opts in to interpreting the function, it is not uninterpreted. if self .spec_interpreted_functions .get(spec_id) @@ -1095,11 +1029,9 @@ impl PackageTargets { { return false; } - // If the function is globally uninterpreted, it is uninterpreted for this spec. if self.globally_uninterpreted_functions.contains(callee_id) { return true; } - // Fall back to spec-local uninterpreted list. self.spec_uninterpreted_functions .get(spec_id) .map_or(false, |set| set.contains(callee_id)) diff --git a/crates/sui-prover/tests/inputs/uninterpreted/ext_interpreted_override.ok.move b/crates/sui-prover/tests/inputs/uninterpreted/ext_interpreted_override.ok.move deleted file mode 100644 index bad966b75e..0000000000 --- a/crates/sui-prover/tests/inputs/uninterpreted/ext_interpreted_override.ok.move +++ /dev/null @@ -1,22 +0,0 @@ -/// bar() is globally uninterpreted by default. -/// foo_spec_a cannot prove bar() == 42 (uninterpreted), but -/// foo_spec_b uses interpreted=bar to get the actual value and can prove bar() == 42. -module 0x42::foo; - -use prover::prover::ensures; - -#[ext(pure, uninterpreted)] -fun bar(): u64 { - 42 -} - -fun foo(): u64 { - bar() -} - -#[spec(prove, interpreted = bar)] -fun foo_spec(): u64 { - let result = foo(); - ensures(result == 42); // passes: bar is interpreted here, so foo() == bar() == 42 - result -} diff --git a/crates/sui-prover/tests/inputs/uninterpreted/ext_interpreted_wrong_target.fail.move b/crates/sui-prover/tests/inputs/uninterpreted/ext_interpreted_wrong_target.fail.move deleted file mode 100644 index f4c38cdaec..0000000000 --- a/crates/sui-prover/tests/inputs/uninterpreted/ext_interpreted_wrong_target.fail.move +++ /dev/null @@ -1,19 +0,0 @@ -module 0x42::foo; - -use prover::prover::ensures; - -#[ext(pure)] // pure but NOT globally uninterpreted -fun bar(): u64 { - 42 -} - -fun foo(): u64 { - bar() -} - -#[spec(prove, interpreted = bar)] // should error: bar is not #[ext(uninterpreted)] -fun foo_spec(): u64 { - let result = foo(); - ensures(result == 42); - result -} diff --git a/crates/sui-prover/tests/snapshots/uninterpreted/ext_uninterpreted_default.ok.move.snap b/crates/sui-prover/tests/snapshots/uninterpreted/ext_uninterpreted_default.ok.move.snap new file mode 100644 index 0000000000..95d8a7083e --- /dev/null +++ b/crates/sui-prover/tests/snapshots/uninterpreted/ext_uninterpreted_default.ok.move.snap @@ -0,0 +1,5 @@ +--- +source: crates/sui-prover/tests/integration.rs +expression: output +--- +Verification successful diff --git a/crates/sui-prover/tests/snapshots/uninterpreted/ext_uninterpreted_no_pure.fail.move.snap b/crates/sui-prover/tests/snapshots/uninterpreted/ext_uninterpreted_no_pure.fail.move.snap new file mode 100644 index 0000000000..038e33875b --- /dev/null +++ b/crates/sui-prover/tests/snapshots/uninterpreted/ext_uninterpreted_no_pure.fail.move.snap @@ -0,0 +1,13 @@ +--- +source: crates/sui-prover/tests/integration.rs +expression: output +--- +exiting with bytecode transformation errors +error: #[ext(uninterpreted)] on 'foo::bar' requires #[ext(pure)] + ┌─ tests/inputs/uninterpreted/ext_uninterpreted_no_pure.fail.move:6:1 + │ +6 │ ╭ fun bar(): u64 { +7 │ │ 42 +8 │ │ } + │ ╰─^ + From e3c6b4529a8da9d0ee78fc6045948096725a2c52 Mon Sep 17 00:00:00 2001 From: Andrii Date: Wed, 11 Mar 2026 10:59:25 +0200 Subject: [PATCH 3/3] fix: test case --- .../uninterpreted/ext_uninterpreted_no_pure.fail.move.snap | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/crates/sui-prover/tests/snapshots/uninterpreted/ext_uninterpreted_no_pure.fail.move.snap b/crates/sui-prover/tests/snapshots/uninterpreted/ext_uninterpreted_no_pure.fail.move.snap index 038e33875b..1a62721d7f 100644 --- a/crates/sui-prover/tests/snapshots/uninterpreted/ext_uninterpreted_no_pure.fail.move.snap +++ b/crates/sui-prover/tests/snapshots/uninterpreted/ext_uninterpreted_no_pure.fail.move.snap @@ -5,9 +5,8 @@ expression: output exiting with bytecode transformation errors error: #[ext(uninterpreted)] on 'foo::bar' requires #[ext(pure)] ┌─ tests/inputs/uninterpreted/ext_uninterpreted_no_pure.fail.move:6:1 - │ + │ 6 │ ╭ fun bar(): u64 { 7 │ │ 42 8 │ │ } │ ╰─^ -