diff --git a/crates/sui-prover/tests/inputs/assert.ok.move b/crates/sui-prover/tests/inputs/assert.ok.move new file mode 100644 index 0000000000..47f5c5f5bc --- /dev/null +++ b/crates/sui-prover/tests/inputs/assert.ok.move @@ -0,0 +1,20 @@ +module 0x42::foo { + public fun foo(input: u64): u64 { + assert!(input != 10); + + input + } +} + +module 0x43::bar { + use prover::prover::asserts; + use 0x42::foo::foo; + + #[spec(prove, target = 0x42::foo::foo)] + fun foo_spec(input: u64): u64 { + asserts(input != 10); + + let result = foo(input); + result + } +} \ No newline at end of file diff --git a/crates/sui-prover/tests/inputs/assert.scenario.fail.move b/crates/sui-prover/tests/inputs/assert.scenario.fail.move new file mode 100644 index 0000000000..3b4ea45d96 --- /dev/null +++ b/crates/sui-prover/tests/inputs/assert.scenario.fail.move @@ -0,0 +1,19 @@ +module 0x42::foo { + public fun foo(input: u64): u64 { + assert!(input != 10); + + input + } +} + +module 0x43::bar { + use prover::prover::asserts; + use 0x42::foo::foo; + + #[spec(prove)] + fun scenario_spec(input: u64): u64 { + asserts(input != 10); // asserts are supported in scenario specs + let result = foo(input); + result + } +} diff --git a/crates/sui-prover/tests/snapshots/assert.ok.move.snap b/crates/sui-prover/tests/snapshots/assert.ok.move.snap new file mode 100644 index 0000000000..95d8a7083e --- /dev/null +++ b/crates/sui-prover/tests/snapshots/assert.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/assert.scenario.fail.move.snap b/crates/sui-prover/tests/snapshots/assert.scenario.fail.move.snap new file mode 100644 index 0000000000..c2a66a1c68 --- /dev/null +++ b/crates/sui-prover/tests/snapshots/assert.scenario.fail.move.snap @@ -0,0 +1,15 @@ +--- +source: crates/sui-prover/tests/integration.rs +assertion_line: 277 +expression: output +--- +exiting with bytecode transformation errors +error: Scenario specs either ignore aborts or do not have any asserts. + ┌─ tests/inputs/assert.scenario.fail.move:14:5 + │ +14 │ ╭ fun scenario_spec(input: u64): u64 { +15 │ │ asserts(input != 10); // asserts are supported in scenario specs +16 │ │ let result = foo(input); +17 │ │ result +18 │ │ } + │ ╰─────^