Now also featured on JetBrains Marketplace!
- Description
- Current Features
- Roadmap
- ProofFrog Library Installation
- Parser Differences
- Plugin Development
- Gallery
ProofFrog is a work-in-progress tool for verifying cryptographic game-hopping proofs.
All security properties in ProofFrog are written via pairs of indistinguishable games.
This plugin aims to provide syntax highlighting, annotations, code completion, and other features
for the ProofFrog Domain Specific Language, which is described in detail in the thesis paper.
This plugin is compatible with all JetBrains IDE-s and if you are doing active cryptography R&D,
we wholeheartedly recommend you to use their CLion IDE, which since May 7, 2025 has become
Free for Non-Commercial Use.
ProofFrog has multiple example files which can be used together with this plugin to see the library in action.
- Syntax validation
- Syntax highlighting
- Color settings menu
- Comment with Line Comment action
- Automatic setup of ProofFrog Python library
- Project explorer context menu
- Editor context menu
- Run configurations
- Ctrl+Click of import statement file paths
If you want these goals to get done, then please ⭐ Star this repository to indicate your need for
this software. You can also participate in the discussions
to propose other features for the ProofFrog
plugin or make a pull request against this repository with your implemented changes.
- General reference contributor
- Completion contributor
- Go To Symbol contributor
- Find usages provider
- Folding builder
When you first install the plugin into a JetBrains IDE, it will try to locate a Python virtual environment with
the proof_frog library installed. If it fails to do so, you will be prompted
with a confirmation popup asking if
you want the plugin to download and install it for you.
If you choose Yes, the plugin first downloads the latest release of Astral UV package manager into the plugin
directory, then uses it to download a Python version, then uses it to create a private Python virtual environment
into the plugin directory and finally installs proof_frog from the Python Package Index into the venv.
If you choose No, you can still enable the context-menu actions and run configurations of the plugin by manually
creating a Python virtual environment named either venv or .venv at the top level of your project directory and
installing proof_frog into it. Once you have done that, the plugin will detect and use your manual proof_frog
library installation when you restart the IDE.
The manual installation solution is also useful for developing the proof_frog library itself in PyCharm, because
you can install the library into the venv in editable mode and then use the plugin actions to test the modified library.
There is a minor difference in how this plugin parses ProofFrog code compared to the ProofFrog library itself.
Namely, this plugin does not and will not allow the keyword in as class field names, so you might get parsing
errors when opening some ProofFrog example files which contain Int in = in; or requires F.in == F.out;.
This syntax is forbidden because literally all real programming languages forbid the usage of reserved keywords
as identifiers, and it does not make sense to deviate from this standard.
This plugin must be developed with IntelliJ IDEA IDE (Community or Ultimate).
Development of this plugin requires the Grammar-Kit and Plugin DevKit plugins from the IDE marketplace.
Do once per IDE:
In the top navbar, go to Help -> Edit Custom Properties... and insert
idea.is.internal=true into the idea.properties file, if it's not there yet.
To modify the syntax rules of this plugin, modify the ProofFrog.bnf and ProofFrog.flex files in
sources root directory at src/main/java/io/github/aabmets/prooffroglang.
Then in ProofFrog.bnf context menu select Generate Parser Code and in ProofFrog.flex context menu
select Run JFlex Generator, then use the generated PSI elements in any number of ProofFrog source files
to implement the plugin behavior.
