build: add container, scripts, and documentation for verifying and constructing proofs on an HPC cluster

[cfm]

Here's another option for verifying and reconstructing proofs. Tagging you, @felixlinker, in case you want to include these instructions in the CCS artifact.

[felixlinker]

Heya! Thanks for that :) We should definitely include it, but I don't think it's necessary for the review. I'll spare us the extra zenodo version for now. There'll be probably some changes to the artifact due to the review, and then we can batch everything together for a new version!

[cfm]

Confirmed that verify.sbatch completes successfully:

[cfmyers@klone-login01 securedrop-protocol-models]$ sacct -u cfmyers --units=G   --format=JobID%15,JobName%14,Elapsed,UserCPU,SystemCPU,TotalCPU,MaxRSS,State
          JobID        JobName    Elapsed    UserCPU  SystemCPU   TotalCPU     MaxRSS      State 
--------------- -------------- ---------- ---------- ---------- ---------- ---------- ---------- 
     36142958_0 verify-secure+   00:29:17   01:09:44  05:12.537   01:14:56             COMPLETED 
36142958_0.bat+          batch   00:29:17   01:09:44  05:12.537   01:14:56    104.92G  COMPLETED 
36142958_0.ext+         extern   00:29:17   00:00:00   00:00:00   00:00:00             COMPLETED 
     36142958_1 verify-secure+   01:41:07   03:15:21  22:18.723   03:37:40             COMPLETED 
36142958_1.bat+          batch   01:41:07   03:15:21  22:18.723   03:37:40    165.12G  COMPLETED 
36142958_1.ext+         extern   01:41:07   00:00:00   00:00:00   00:00:00             COMPLETED 
     36142958_2 verify-secure+   01:02:32   02:16:02  14:15.359   02:30:18             COMPLETED 
36142958_2.bat+          batch   01:02:32   02:16:02  14:15.359   02:30:18    124.67G  COMPLETED 
36142958_2.ext+         extern   01:02:32   00:00:00   00:00:00   00:00:00             COMPLETED 
     36142958_3 verify-secure+   00:36:52   01:19:47  06:40.811   01:26:28             COMPLETED 
36142958_3.bat+          batch   00:36:52   01:19:47  06:40.811   01:26:28    110.39G  COMPLETED 
36142958_3.ext+         extern   00:36:52   00:00:00   00:00:00   00:00:00             COMPLETED 
     36142958_4 verify-secure+   00:31:12   01:13:13  05:39.088   01:18:52             COMPLETED 
36142958_4.bat+          batch   00:31:12   01:13:13  05:39.088   01:18:52    112.44G  COMPLETED 
36142958_4.ext+         extern   00:31:12   00:00:00   00:00:00   00:00:00             COMPLETED

[Copilot]

Pull request overview

Adds an HPC-friendly workflow for constructing and verifying Tamarin proofs by introducing an Apptainer container definition, Slurm batch scripts, and accompanying documentation. This fits the repo’s goal of making the SecureDrop protocol model proofs reproducible across environments, especially on clusters.

Changes:

• Document running well-formedness checks and proof verification on Slurm via Apptainer.
• Add Slurm batch scripts to verify/reconstruct all proofs using a job array.
• Fix Makefile log target dependency to depend on the corresponding .spthy file instead of all proofs.

Reviewed changes

Copilot reviewed 5 out of 5 changed files in this pull request and generated 1 comment.

Show a summary per file

File	Description
README.md	Adds HPC/Slurm + Apptainer usage instructions and references the new batch scripts.
Makefile	Narrows proof/%.log dependency to the matching proof/%.spthy.
hpc/verify.sbatch	Adds Slurm array job to verify proofs inside the Apptainer container.
hpc/prove.sbatch	Adds Slurm array job to reconstruct proofs inside the Apptainer container.
hpc/tamarin.def	Defines the Apptainer image used to run Tamarin/Maude in a reproducible environment.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[Copilot]

Pull request overview

Copilot reviewed 7 out of 7 changed files in this pull request and generated no new comments.

Suppressed comments (6)

README.md:86

• Same as above: using bash -c inside the container can fail if bash isn’t present. sh -c is sufficient for ulimit + make and avoids an unnecessary dependency.

    ```bash
    salloc --nodes=1 --ntasks=1 --cpus-per-task=10 --mem=192G --time=12:00:00 apptainer exec tamarin.sif bash -c 'ulimit -Sn $(ulimit -Hn); make proof/Auto_.log'
    ```

Makefile:15

• .SECONDARY: with no prerequisites disables intermediate-file cleanup for all targets in this Makefile, not just proof .spthy files. If the intent is only to keep generated proof/%.spthy from being deleted when building proof/%.log, scope .SECONDARY to that pattern to avoid retaining unrelated intermediates in future expansions of the Makefile.

# Keep make from deleting a freshly constructed proof as an intermediate file.
.SECONDARY:

README.md:24

• The container build is pinned to x86_64 (--platform=linux/amd64 in hpc/Dockerfile, and the setup script downloads x86_64/Linux64 binaries). The README should call out the architecture requirement so ARM users don’t hit confusing build/run failures.

A containerized environment is also available, for example via Docker:

```bash
docker build --tag tamarin hpc
docker run --rm --volume "$PWD:/workspace" tamarin --version

README.md:80

• These examples run apptainer exec … bash -c …, but the container image is built from Debian slim and hpc/setup.sh doesn’t explicitly install bash. To avoid failures on minimal images, use sh -c (POSIX) here.

This issue also appears on line 84 of the same file.

    ```bash
    salloc --nodes 1 --ntasks 1 --mem=10G --time=1:00:00 apptainer exec tamarin.sif bash -c 'ulimit -Sn $(ulimit -Hn); make well-formed'
    ```

hpc/verify.sbatch:27

• This runs bash -c inside the Apptainer image, but hpc/setup.sh doesn’t install bash explicitly. Using sh -c makes the job script work even if the image only provides /bin/sh (common for slim bases).

apptainer exec "$SIF" bash -c \
    "ulimit -Sn \$(ulimit -Hn); make N_THREADS=${SLURM_CPUS_PER_TASK} \
    -W proof/${PREFIX}.spthy \
    proof/${PREFIX}.log"

hpc/prove.sbatch:27

• This runs bash -c inside the Apptainer image, but hpc/setup.sh doesn’t install bash explicitly. Switching to sh -c avoids a hard dependency on bash being present in the image.

apptainer exec "$SIF" bash -c \
    "ulimit -Sn \$(ulimit -Hn); make N_THREADS=${SLURM_CPUS_PER_TASK} \
    -B \
    proof/${PREFIX}.spthy"

[cfm]

I've tacked on a Dockerfile for local use. Feel free to merge if you're happy with this, @felixlinker, or I can do so first thing tomorrow.