This repository contains the artifacts for the paper David Baelde, Antoine Dallon, Stéphanie Delaune, Charlie Jacomme, Adrien Koutsos: Robust Logical Foundations for Mechanizing Post-Quantum Cryptography in Squirrel CCS 2026## OrganizationThe artifacts include:- `artifact-appendix.pdf`: the artifact appendix of the paper;- `case-studies/`: the Squirrel developments (see `case-studies/README.md` for more details);- `squirrel/`: our post-quantum extension of Squirrel;- `docker/`: configuration and script to build the Docker image;- `squirrel.tar`: pre-built Docker image.## HTML FilesThe `case-studies/html/` sub-directory contains HTML versions of theSquirrel developments that can be consulted from a web browser,without installing Squirrel.## Reproduction with DockerProvided that docker is[installed](https://docs.docker.com/engine/install), the followinginstructions allow to reproduce our results:1 - Load the docker image `squirrel.tar` using `docker load --input squirrel.tar`. Alternatively, the docker image may be built from scratch by running `./docker/build.sh`.2 - Once the docker image is loaded, run `docker run -it sp/squirrel-prover:latest bash`.3 - Run all our examples by executing `make` in the `case-studies/` directory.## Reproduction from Sources1 - Build Squirrel. First build the squirrel prover, whose source code is in `squirrel/`. See `squirrel/README.md` for dependencies and build instructions. Note that building with SMT support is mandatory for some of our examples. These developments were checked using CVC5 (version 1.0.8) and Z3 (version 4.13.2). 2 - Add Squirrel to the PATH. `export PATH=$PATH:/path/to/squirrel`3 - Run examples. To run all our examples, execute `make` in the `case-studies/` directory.