
# These instructions are slightly outdated, from before merging into AIComposer.

# For macOS users

1. Clone https://github.com/Certora/VeriSafe project, and this specific pull request: https://github.com/Certora/VeriSafe/pull/12
2. Clone https://github.com/Certora/CexAnalyzer
3. Install docker desktop and make sure it’s enabled
4. Get a Claude API key, set it as `ANTHROPIC_API_KEY` in your environment
5. Taken from VeriSafe, adapted for macOS:

> You will need to build the local RAG database used for CVL manual searches by the LLM.
> Instructions are as follows:
> 1. cd into `verisafe/scripts/`
> 2. run `docker compose create && docker compose start`. This will initalize a local postgres database. NB: no attempt has been made to ensure this database is secure; caveat emptor
> 3. Run the base script `./gen_docs_zsh.sh`; if it completes without error, you should have `cvl_manual.html` in your directory
> 4. Create a new python virtual environment for the RAG build process by running `python3 -m venv somepath` where `somepath` is some path on your filesystem
> 5. Run `source somepath/bin/activate`.
> 6. Run `pip3 install -r ./rag_build_requirements.txt` 
> 7. Run `python3 ./ragbuild.py cvl_manual.html`.
> 8. Run the command `deactivate`
> 9. (Optional) cleanup `somepath`


1. From CexAnalyzer, `pip install -r requirements.txt`
2. Clone this repo https://github.com/Certora/ScrappyViolationAnalyzerCLI
3. From ScrappyViolationAnalyzerCLI, `pip install -r requirements.txt`
4. `export CEXANALYZER_PATH=/path/to/CexAnalyzer/main.py`
5. Run with  `python3 AutoCVL/analyze_violations.py PROVER_URL RULE_NAME OPTIONAL_METHOD_NAME`
    1. You may also run with `--all` instead of `RULE_NAME` etc..., but it’s VERY expensive so avoid that if you can.
6. Follow the output of the analyzer.

# For Linux users

Same, with 2 main differences:

1. checkout the main branch of VeriSafe instead of the PR
2. run `gen_docs.sh` instead of `gen_docs_zsh.sh` 

# Troubleshooting

- If you cannot fetch the zipOutput (i.e. failure in certora_wget.py), try to login to [prover.certora.com](http://prover.certora.com) using Firefox browser. Other browsers, and non-macOS environments, were not tested!
- The analysis can take some time, so be patient. It’s faster than Prover though :)
- Docker issues - good luck
