Proof development primitives #1637

StateContT transformer, which gives us the ability to capture continuations. This allows us to implement `callcc` as a saw-script command. Additionally, implement a "checkpoint" command that will capture the TopLevel monad state and allow it to be restored later. Also, rework some aspects of error handling. The previous method no longer worked properly with a continuation-based TopLevel monad.

When invoked from a batch file (or from an ongoing REPL session) starts a "subshell" REPL session. The intent here is to allow for exploration and experimentation in the middle of a larger run. For now, subshells are not very useful, as there isn't a good way to expose the local SAW environment to the shell.

of the TopLevel monad. This allows it to interact with primitive operations; in particular, we can start a subshell with local SAW script bindings in scope.

be leaving alone (async and exit exceptions).

`NameSeeds` value used internally by Cryptol to be carried forward across checkpoints. This prevents internal nonce values from being reused, which, in turn, avoids errors about registering duplicate names. It is unclear if this is the correct long-term fix, but it allows checkpoint to work more reliably when importing Cryptol modules or using `let {{ ... }}` constructs.

mutable state part of the TopLevel monad. This allows them to participate in the checkpoint/restore mechanism.

``` void saw_assert( uint32_t ); ``` This allows the program source to directly assert a proposition inline which is then assumed as part of the path condition. This can sometimes help the path sat checker by stating helpful lemmas whose proof can be deferred to the VC-checking phase. It can also be helpful for program/proof exploration, allowing the user to directly state inline hypotheses about program behavior, and then attempt to prove them.

allows the user to restore proof states.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Proof development primitives #1637

Proof development primitives #1637

Commits on Aug 8, 2022