Add formal verification for the Governor system

[Amxx]

Fixes LIB-746

WIP

[changeset-bot]

⚠️ No Changeset found

Latest commit: aaa5a5a

Merging this PR will not cause a version bump for any packages. If these changes should not result in a new version, you're good to go. If these changes should result in a version bump, you need to add a changeset.

This PR includes no changesets

When changesets are added to this PR, you'll see the packages that this PR includes changesets for and the associated semver types

Click here to learn what changesets are, and how to add one.

Click here if you're a maintainer who wants to add a changeset to this PR

[changeset-bot]

⚠️ No Changeset found

Latest commit: f35c824

Merging this PR will not cause a version bump for any packages. If these changes should not result in a new version, you're good to go. If these changes should result in a version bump, you need to add a changeset.

This PR includes no changesets

When changesets are added to this PR, you'll see the packages that this PR includes changesets for and the associated semver types

Click here to learn what changesets are, and how to add one.

Click here if you're a maintainer who wants to add a changeset to this PR

[Amxx]

Note: I wanted to do

node certora/run.js GovernorStates --options="--rule stateTransitionWait"

But that caused issues with options including spaces. So I moved the .flatMap(opt => opt.split(' ')) to inside the runCertora function

@frangio can you see any issue with that ?

[frangio]

No, that makes sense. I don't think it's ideal the way we're handling options but it works.

[Amxx]

FYI: main (only?) remaining blocker is the stateTransitionFn function timming out.

It appears that it only reason it used to pass was because of poorly written formula and mistakes in the associativity of operators. Rewritting them cleanly (or adding parenthesis) causes it to timeout. An option could be to split that rule into multiple rules with limited logic in each one.