Add prebuilt Rocq toolchain image for run-experiment's rocq-image

[alpaylan]

Why

run-experiment.yml's rocq-image input runs the job inside a prebuilt container to skip the ~30‑min from‑source Coq/QuickChick build — but nothing ever built that image. Experiment repos defaulting rocq-image to ghcr.io/alpaylan/etna-quickchick:programmable-pbt fail immediately with manifest unknown (example run). This PR adds the missing half.

What

• docker/rocq.Dockerfile — reproduces the from‑source path exactly: AFL‑instrumented OCaml 5.2.1 switch (ocaml-variants.5.2.1+options + ocaml-option-afl) + Coq (Rocq 9.1.1) + QuickChick (alpaylan/QuickChick#programmable-pbt) + the deps its opam file declares (mathcomp‑ssreflect, simple‑io, ext‑lib, …). The opam switch paths are baked into the image ENV so each Actions step's non‑login shell finds coqc/dune without opam env.
  • Needs libgmp-dev in the apt layer: a bare container has no setup-ocaml to auto‑install opam depexts, so Coq's zarith → conf-gmp → libgmp-dev must be present (this was the first thing the local build caught).
  • etna is not baked in — run-experiment.yml installs it fresh per run (latest release), so a copy here would only go stale and tie the image to etna's release‑arch matrix.
• .github/workflows/build-rocq-image.yml — workflow_dispatch (+ push on Dockerfile change) that builds and pushes to ghcr.io/<owner>/etna-quickchick.
• run-experiment.yml — gate the "Setup OCaml for Coq" and "Install Coq + QuickChick + ExtLib" steps on inputs.rocq-image == '', so supplying an image actually uses it instead of rebuilding the toolchain inside it.

Validation

Built the image locally (arm64) and confirmed in a fresh non‑login shell:

```
$ docker run --rm etna-quickchick:local-test sh -c 'coqc /tmp/t.v' # imports QuickChick + mathcomp.ssreflect
=== QUICKCHICK + SSREFLECT LOAD OK ===
```

After merge (one‑time)

1. Run Build Rocq toolchain image (Actions → workflow_dispatch) to populate the registry.
2. Set the etna-quickchick package visibility to Public so experiment repos under the same owner can pull it.
3. Re‑run the experiment workflow — it now boots straight into the prebuilt toolchain.

🤖 Generated with Claude Code