diff --git a/crates/move-stackless-bytecode/src/package_targets.rs b/crates/move-stackless-bytecode/src/package_targets.rs index a5a3e0264e..9c3d35437e 100644 --- a/crates/move-stackless-bytecode/src/package_targets.rs +++ b/crates/move-stackless-bytecode/src/package_targets.rs @@ -38,8 +38,10 @@ pub struct PackageTargets { omit_opaque_specs: BTreeSet>, focus_specs: BTreeSet>, scenario_specs: BTreeSet>, + globally_uninterpreted_functions: BTreeSet>, // functions that should be uninterpreted when verifying a specific spec function. spec_uninterpreted_functions: BTreeMap, BTreeSet>>, + spec_interpreted_functions: BTreeMap, BTreeSet>>, spec_boogie_options: BTreeMap, String>, spec_timeouts: BTreeMap, u64>, loop_invariant_candidates: BTreeMap, Vec<(QualifiedId, usize)>>, @@ -78,7 +80,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 +528,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 +546,32 @@ 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. fn check_uninterpreted_scope(&mut self, func_env: &FunctionEnv) { let env = func_env.module_env.env; if let Some(KnownAttribute::Verification(VerificationAttribute::Spec { @@ -1000,11 +1022,29 @@ impl PackageTargets { spec_id: &QualifiedId, callee_id: &QualifiedId, ) -> bool { + if self + .spec_interpreted_functions + .get(spec_id) + .map_or(false, |set| set.contains(callee_id)) + { + return false; + } + if self.globally_uninterpreted_functions.contains(callee_id) { + return true; + } 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_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 +} 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..1a62721d7f --- /dev/null +++ b/crates/sui-prover/tests/snapshots/uninterpreted/ext_uninterpreted_no_pure.fail.move.snap @@ -0,0 +1,12 @@ +--- +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 │ │ } + │ ╰─^