Metadata-Version: 2.1
Name: proof_frog
Version: 0.1.1
Summary: A tool for verifying game-hopping proofs
Author-email: Ross Evans <rpevans@uwaterloo.ca>
Requires-Python: >=3.11
Description-Content-Type: text/markdown
Requires-Dist: antlr4-python3-runtime >= 4.13
Requires-Dist: colorama >= 0.4
Requires-Dist: z3-solver >= 4.12
Requires-Dist: sympy >= 1.12
Project-URL: Documentation, https://prooffrog.github.io
Project-URL: Source, https://github.com/ProofFrog/ProofFrog

# ProofFrog
A work in progress

## Installation:

```
pip3 install -r requirements.txt
pip3 install -r requirements-dev.txt
```

## Commands:

To use the proof engine: `python3 proof_frog prove [proof_file]`. As of right now, the only proofs working are 'examples/Proofs/SymEnc/OTUC=>OTS.proof' and 'examples/Proofs/SymEnc/CPA$=>CPA.proof'.

You can also parse any type of file (scheme, proof, game, or primitive) using `python3 proof_frog parse [file]`. It will read the file, transform it into an internal AST representation, stringify the representation, and print it back out to the screen.

The bash files `testParsing.sh` ensures that the ANTLR grammar can parse each file in the examples folder. `testAST.sh` parses each file with proof_frog, strips the whitespace, and diffs it with the original file to ensure that the AST output matches the file input.

