[major] Merging features for 4.0

[tnelson]

Draft Forge 4.0.0 Release Notes

Forge 4.0.0 contains a number of new features and fixes from the previous version (3.7). There are breaking changes; please read the first 2 paragraphs carefully.

Anyone using the Forge VSCode extension should make sure to update that extension alongside updating Forge. We recommend enabling automatic updates for the extension.

Major Change: Sterling Run Menu

Sterling will now show a menu of available commands to execute, rather than commands being executed in sequence at the command prompt. Run Forge as normal (either via the Play button in the VSCode extension or via `racket in the command prompt) and Sterling will immediately load. Select a command from the drop-down and click "Run" to start the solver process and view instances for that command.

Breaking Change: #lang forge/froglet

For consistency, the Froglet language can now only be accessed via #lang forge/froglet. Forge had previously supported #lang froglet and #lang froglet/bsl (for "Beginner Student Language"). The new language name both avoids ambiguity and the need to install a separate Racket package.

Attempting to use #lang forge/bsl in Forge 4.0.0 will produce an error message.

Breaking Change: is checked vs. is theorem

The syntax of a test expect test that expects the predicate body to be valid has changed. Previously, one would write {<property>} is theorem, but this was inaccurate: Forge performs bounded verification of <property>, and so will now enforce the use of is checked so as not to connote completeness.

Sterling Fixes

Giving a filename to the run_sterling option will now properly pre-load the contents of that file into the script view window.

Theming will now persist between instances for the same command. Previously, theming was cleared for every new instance.

New Syntax

This release adds new assertion forms for consistency checking:

• assert <constraint> is consistent with <pred name> for <bounds>; and
• assert <constraint> is inconsistent with <pred name> for <bounds>.
  Moreover, the assert ... is necessary for ... and assert ... is sufficient for ... commands now support an arbitrary constraint block on the left hand side. Previously only a predicate name was allowed.

We strongly encourage the use of these new constructs rather than the old-style test expect {... is sat } and ... is unsat forms where possible.

For internal use, test expect now supports the is forge_error <?substr> expectation, which passes only if the run generates an error in Forge. Optionally, a substring may be provided that is matched against any error thrown.

Domain-Specific Model Fixes

The #lang forge/domains/crypto visualizer now properly displays the plaintext and key for encrypted terms if those terms have unexpected atom names.

The #lang forge/domains/crypto examples now include the missing Needham-Schroeder protocol as well as the fixed version of the protocol.