Prover Studio

This Visual Studio Code extension provides support for several languages and formats:

• HLL and sHLL
• LCF
• PiSPEC
• RJSON
• Prover iLock proof obligation deviation files

It is developed by Prover.

Requirements

The following dependencies need to be installed before you can use Prover Studio:

• .NET 8 runtime, see https://learn.microsoft.com/en-us/dotnet/core/install/.

Features

• Syntax highlighting
• Reports syntax errors

• Reports semantic errors (such as references to unknown functions)

• Provides "Go to definition", "Find references", and document outlines.

• Helps with creating Prover iLock package bundles (.pipkgs files) out of the packages in the workspace and their dependencies, by providing a 'Make package bundle' command. Access it via the command palette (Ctrl+Shift+P). This command is only availble on Windows.

• Manages Prover Studio projects for HLL and sHLL: creation of projects, adding and removing files, selecting the active project, etc. Access projected related commands via the command palette or with the file explorer context menu.

• Pretty print the output of the Prover PSL why tool output. The output needs to be either an XML or a TXT file. This feature can be invoked by entering "Preview Prover PSL why output" in the command palette.

Setting up your workspace

The following doesn't apply if you are using HLL and/or sHLL only.

Prover Studio will look through your workspace for any package directories (directories containing a "package.xml" file) and project directories (directories containing ".isy" files). Make sure to add these folders to your workspace to make Prover Studio recognize them.

For project directories, only files in the "config" directory will be considered by the extension. Files outside the "config" directory are not picked up (unless explicitly opened in VS code).

Multi-file projects for HLL and sHLL

Use a Prover Studio project file to create multi-file models (for HLL and sHLL):

• Open in VS Code a folder containing all the files needed in your project.
• Create a Prover Studio project using the "New Prover Studio project" command accessible from the command palette (Ctrl+Shift+P). You will need to choose a name for the project and some files belonging to the project.
• You can add or remove files to the project using the commands "Add file to Prover Studio project" and "Remove file from Prover Studio project" accessible from the command palette or with a right click on the file of your choice in the VS code file explorer. It is also possible to select multiple files in the explorer and add all of them with one command (accessible with a right click on any of the selected files). All the files from a subdirectory can also be added or removed with "Add/Remove contained HLL/sHLL files to Prover Studio project".
• All the files of the project must be in the opened folder or a subdirectory. The "Go to definition" and "Go to declaration" commands will search in all the project files, and the semantic checks will be performed on the project as a whole.
• The project specifications are stored in a file named <project_name>.psprj that is automatically edited by Prover Studio.

Several Prover Studio projects in the same folder, and active project:

• You may create several projects in the same folder. For that you have to follow the same steps as mentioned in the previous paragraph.
• If a file belongs to several projects, it will be considered as part of the "active project" which can be changed with the "Change active Prover Studio project" command, which is also accessible with a right click on the project file in the file explorer.
• In the file explorer, the files of the active project are green, and the files that belong to no project are in light grey.

If an error is found in the project, the project file will be red in the explorer. Open it to see the details and fix the problem.

Semantic checks for HLL

Semantic checks for HLL rely on Prover Expander 1 which is distributed with Prover Certifier. Make sure you have it installed with a valid license. Then go to the extensions settings and:

• Specify the path to Prover Expander 1 binary in "Hll Semantic Checks: Prover Expander1 Path"
• Specify the path to the license in "Hll Semantic Checks: Prover License Path"
• For Windows, specify the path to cygwin bash.exe in "Hll Semantic Checks: Cygwin Bash Path"
• Enable "Hll Semantics Checks"

Once everything is set up properly, semantic errors will appear in the editor, including for properly configured multi-file projects (see above). In the current version, sHLL is not covered.

Reachability Obligations

Prover Studio has rudimentary support for Reachability Obligations for now. This means that the syntax checks are performed, but for the semantic checks it requires Prover Expander 1 version 3.3 or later. For earlier versions of Prover Expander 1, it is recommended to isolate all Reachability Obligations into a separate file, as Prover Expander 1 will stop at the first syntax error.

sHLL debugging

sHLL debugging requires that Prover PSL 6.0.6 or later is installed and available on the PATH. To debug a sHLL model, open the model in the editor, and select the "Run and debug" panel. Click the "create a launch.json file" link. This will open a debug configuration file. Save the file and click the "Start debugging" button in the debug panel to launch the debugger.

You can manually configure which HLL and sHLL files are passed on to Prover PSL using the "hllFiles" and "shllFiles" settings in the launch.json file. If these settings are left out, the files to use are determined as follows:

• If you have an active Prover Studio project, the files will be picked up from there.
• Otherwise, all sHLL and HLL files in the workspace will be used.

By default, Prover PSL will be launched using its default strategy. You can override the strategy to use with the "strategy" setting in the launch.json file.

Editing LCF tables

The extension provides a spreadsheet-style editor for LCF tables. To open the editor, right click on the file containing the table you want to edit, and select "Open With..." and then "LCF table editor". Alternatively, right click on one of your open editor tabs and select "Reopen Editor With..." in the context menu.

Visualize the Prover PSL why output

The extension provides a visualizer for the Prover PSL why output. The output file can either be a txt file or an xml file. Both files are created by Prover PSL. For more information about the creation of these files take a look at the Prover PSL help.

Extension Settings

You can configure the extension through Visual Studio's settings interface. Go to "File"->"Preferences"->"Settings". Search for "Prover Studio" to list all available settings. We recommend to configure the settings on the workspace level whenever possible.

Known Issues

No known issues, but see Release notes.

References

Prover Studio demo (HLL features)