Suggestions & updates #3

srunquist-certora · 2025-10-09T03:26:20Z

No description provided.

This was removed from CLI in 8.0(?)

The assumptions are logical, but not needed. Rules pass without them: https://prover.certora.com/output/7749274/46268bb1c02c41f4b86527108f9d2e1d?anonymousKey=c1e61c81e55a93cc3f7ea965a2e7996c264dbdd1 https://prover.certora.com/output/7749274/a02f870d1c4b429ca144f761e9e39020?anonymousKey=6adb620b99e67df55335533f344b4dd13a8b04e1 ... so, better to generalize and simplify, I think.

Jobs run ok without them, so seems better to hide these details.

srunquist-certora · 2025-10-09T03:33:11Z

docs/source/token/mutations.rst

+  Note that there are other ways to assess the quality of your rule.
+  You can mutate the rule to see if it is vacuous, you can check if the rule is a
+  tautology, and you can use UNSAT cores to understand what parts of the code were
+  covered by the rule.


Do we have resources we can link to for these approaches?
If not, I think we can leave it out since it doesn't stand alone very well.

Vacuity: https://docs.certora.com/en/latest/docs/prover/checking/sanity.html#vacuity-checks

Tautologies:
https://docs.certora.com/en/latest/docs/prover/checking/sanity.html#assert-tautology-checks

UNSAT cores: we don't have a link for this, should probably be dropped.

Updated - thanks!

srunquist-certora · 2025-10-09T03:55:42Z

projects/token/confs/exercise1.conf

    ],
-    "precise_bitwise_ops": true,
-    "prover_version": "master",
-    "server": "production"


Any reason to keep prover_version and server in the confs?
My tests with 8.1.1 worked ok without them, so seems better to simplify.

yes no good reason IMO

agreed! sorry this was my bad. Thanks for fixing.

srunquist-certora · 2025-10-09T04:01:01Z

projects/token/solutions/solution_specs.rs

 #[rule]
 fn transfer_is_correct(e: Env, to: Address, from: Address, amount: i64) {
-    cvlr_assume!(
-        e.storage().persistent().has(&from) && e.storage().persistent().has(&to) && to != from);


It makes logical sense to require these addresses to exist, but the rule passes without this:
https://prover.certora.com/output/7749274/46268bb1c02c41f4b86527108f9d2e1d?anonymousKey=c1e61c81e55a93cc3f7ea965a2e7996c264dbdd1

you can remove them! I think i was just trying to make something to show the usage of assume but might have been too contrived because at the time I didn't have as many examples.

srunquist-certora · 2025-10-09T04:03:12Z

projects/token/solutions/solution_specs.rs

-        e.storage().persistent().has(&from)
-            && e.storage().persistent().has(&to)
-            && to != from
-            && Token::balance(&e, from.clone()) < amount);


The rule passes without these:
https://prover.certora.com/output/7749274/a02f870d1c4b429ca144f761e9e39020?anonymousKey=6adb620b99e67df55335533f344b4dd13a8b04e1

So, better to simplify and generalize the rule(?)

agreed, remove it!

urikirsh

Minor nits. Please fix and wait for Chandra's review before merging.

docs/source/token/mutations.rst

urikirsh · 2025-10-23T10:28:16Z

docs/source/token/mutations.rst

+  Note that there are other ways to assess the quality of your rule.
+  You can mutate the rule to see if it is vacuous, you can check if the rule is a
+  tautology, and you can use UNSAT cores to understand what parts of the code were
+  covered by the rule.


Vacuity: https://docs.certora.com/en/latest/docs/prover/checking/sanity.html#vacuity-checks

Tautologies:
https://docs.certora.com/en/latest/docs/prover/checking/sanity.html#assert-tautology-checks

UNSAT cores: we don't have a link for this, should probably be dropped.

docs/source/token/mutations.rst

docs/source/token/warmup.rst

urikirsh · 2025-10-23T10:30:40Z

docs/source/token/warmup.rst

 .. important::

-   If you are not able to run certoraRun, see the `Sunbeam Troubleshooting`_ section in
+   If you are not able to run ``certoraSorobanProver``, see the `Sunbeam Troubleshooting`_ section in


urikirsh · 2025-10-23T10:31:10Z

projects/token/confs/exercise1.conf

    ],
-    "precise_bitwise_ops": true,
-    "prover_version": "master",
-    "server": "production"


yes no good reason IMO

Fixes from Uri Co-authored-by: urikirsh <[email protected]>

chandrakananandi

Sorry for the late review. Looks great to me. I think you can remove the assumes.

chandrakananandi · 2025-10-28T15:58:32Z

projects/token/confs/exercise1.conf

    ],
-    "precise_bitwise_ops": true,
-    "prover_version": "master",
-    "server": "production"


agreed! sorry this was my bad. Thanks for fixing.

chandrakananandi · 2025-10-28T16:01:38Z

projects/token/solutions/solution_specs.rs

 #[rule]
 fn transfer_is_correct(e: Env, to: Address, from: Address, amount: i64) {
-    cvlr_assume!(
-        e.storage().persistent().has(&from) && e.storage().persistent().has(&to) && to != from);


you can remove them! I think i was just trying to make something to show the usage of assume but might have been too contrived because at the time I didn't have as many examples.

chandrakananandi · 2025-10-28T16:01:46Z

projects/token/solutions/solution_specs.rs

-        e.storage().persistent().has(&from)
-            && e.storage().persistent().has(&to)
-            && to != from
-            && Token::balance(&e, from.clone()) < amount);


agreed, remove it!

srunquist-certora added 6 commits October 8, 2025 16:39

Remove "process": "emv" from conf files

6f8f16c

This was removed from CLI in 8.0(?)

Content suggestions

e68df99

Remove "server" and "prover_version" from confs

57237cf

Jobs run ok without them, so seems better to hide these details.

Commented out a paragraph that isn't needed (or needs work).

3beb954

Add preface linking to main Prover tutorial

54959e4

srunquist-certora commented Oct 9, 2025

View reviewed changes

srunquist-certora requested review from chandrakananandi and urikirsh October 9, 2025 04:09

urikirsh approved these changes Oct 23, 2025

View reviewed changes

srunquist-certora and others added 2 commits October 24, 2025 07:47

Apply suggestions from code review

0cdf76d

Fixes from Uri Co-authored-by: urikirsh <[email protected]>

Added links to docs sections about vacuity and tautologies

acbd3b4

chandrakananandi approved these changes Oct 28, 2025

View reviewed changes

Suggestions & updates #3

Are you sure you want to change the base?

Suggestions & updates #3

Uh oh!

Conversation

srunquist-certora commented Oct 9, 2025

Uh oh!

srunquist-certora Oct 9, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

urikirsh left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

chandrakananandi left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

srunquist-certora Oct 9, 2025 •

edited

Loading