# How provreq Is Installed in This Repo
Qrusty's requirements are managed with [provreq](https://github.com/greeng3/provablerequirements)
(the "Provable Requirements" tool). This document describes how the provreq toolchain is provisioned
in the dev container and how to run it. For what the requirements _are_ and the day-to-day workflow,
see the "Requirements (provreq)" section of the top-level [README](../README.md).
## Where it comes from
Everything below lives in [`.devcontainer/Dockerfile`](../.devcontainer/Dockerfile). Rebuild the dev
container ("Dev Containers: Rebuild Container" in VS Code) to pick up changes.
### Base image — the verification toolchain
```dockerfile
FROM ghcr.io/greeng3/provreq-devcontainer:latest
```
The base is provreq's own prebuilt dev-container image, itself built on
`greeng340or/rust-dev-ubuntu` (qrusty's previous base). It bakes in the pieces provreq needs so we
don't build them here:
- the verification engines `provreq check`/`verify` drive — **Kani, TLC, Prusti, Creusot**;
- **Doorstop** (for viewing the archived heritage), `uv`, `yamllint`;
- **glab** (v1.107.0) and **gh** — so the GitLab CLI survives a container rebuild;
- the cargo gate tools: `cargo-audit`, `cargo-outdated`, `cargo-llvm-cov`, `taplo`.
Because it is inherited, `glab` and every engine are present in a fresh container with no extra work.
### The provreq CLI + UI
provreq is installed **from source with its frontend built**, so the web UI is embedded in the
binary:
```dockerfile
ARG PROVREQ_TAG=v0.0.31
RUN git clone --depth 1 --branch "$PROVREQ_TAG" \
https://github.com/greeng3/provablerequirements /tmp/provreq-src \
&& npm --prefix /tmp/provreq-src/web ci \
&& npm --prefix /tmp/provreq-src/web run build \
&& RUSTFLAGS= cargo install --path /tmp/provreq-src --locked \
&& rm -rf /tmp/provreq-src
```
Why build from a clone instead of `cargo install --git … provreq`: provreq embeds its web UI from
`web/dist` at compile time (via `rust-embed`). A plain `cargo install --git` compiles only the Rust
backend and never runs the frontend build, so `provreq serve` then reports **"The provreq UI has not
been built"**. Building `web/dist` first and then `cargo install --path .` from that same tree
embeds the real UI. `RUSTFLAGS` is cleared for this step because the base image sets
`-C target-feature=+crt-static`, which a dev-tool binary has no reason to link against.
The version is pinned by the `PROVREQ_TAG` build arg. **To upgrade provreq:** bump `PROVREQ_TAG` in
the Dockerfile and rebuild the container.
### The System config (`PROVREQ_SYSTEM_CONFIG`)
`provreq serve` needs an operator-level **System config** — separate from the per-project marker
[`requirements/provreq.json`](../requirements/provreq.json). It names which project slugs belong to
this system and holds the LLM provider block you add in the UI.
`.devcontainer/devcontainer.json` points `PROVREQ_SYSTEM_CONFIG` at
**`/workspace/.provreq/system.json`** — on the persistent workspace mount. As of provreq **v0.0.13**
the UI bootstraps this file on your first "add provider", so nothing seeds it at image-build time.
As of **v0.0.14** this is the single LLM config source: the CLI (e.g. `provreq triage`) reads the
same file the UI writes, so a provider added in the UI is available to CLI commands too.
Two things that matter here:
- **It lives on `/workspace`, not container HOME.** Earlier (v0.0.12) it sat under
`/root/.config/provreq/`, which a container rebuild wipes — so every rebuild silently dropped the
LLM you had added. Putting it on the bind-mounted workspace makes the provider config **survive a
rebuild**.
- **It holds your API keys, so it is gitignored.** v0.0.13's UI writes the provider key into this
file, which is why `.provreq/` is in [`.gitignore`](../.gitignore) — it must never be committed.
(It is on the writable workspace mount, not the read-only `/etc/secrets`, because the UI edits it
in place.)
### The WebDriver grid (`WEBDRIVER_URL`)
provreq's category-3 (UI) verification drives a **W3C WebDriver grid** — it probes
`GET <WEBDRIVER_URL>/status` and reports the `Selenium (WebDriver)` engine `available` only when a
grid answers. `.devcontainer/devcontainer.json` sets:
```json
"WEBDRIVER_URL": "http://host.docker.internal:4444"
```
That address reaches a Selenium grid published on the host's `:4444` (e.g. a `selenium-chrome`
container). `host.docker.internal` is used deliberately — `localhost` and container names don't
resolve on the default Docker bridge, and the grid's container IP changes across restarts. If no
grid is running there, provreq simply reports the engine `MISSING`; start a grid and it flips to
`available` (no provreq restart needed for a fresh `provreq engines`).
> The heavy-tier **MonPoly** engine (category 2b) is not installed here: provreq treats the heavy
> tier as image-provided, so it belongs in the `provreq-devcontainer` base image, not this repo's
> Dockerfile.
## Running it
### Web UI
```bash
provreq serve # serves the UI on http://127.0.0.1:17869 (loopback; VS Code forwards it)
```
`serve` binds loopback only by design (provreq is single-operator: one subject, this machine, no
auth). Port **17869** is listed in `.devcontainer/devcontainer.json` `forwardPorts`, so VS Code
republishes it to the host automatically — open <http://localhost:17869/>. It serves the project in
the current directory, so run it from the repo root where `requirements/` lives.
As of provreq **v0.0.20** the UI covers the full workflow — reviewing requirements, **triage**, and
**formalization** — that earlier versions exposed only on the CLI.
### CLI + Make targets
```bash
make check-requirements # provreq check — artifacts load, no duplicate uuids, no orphan tags
make traceability # provreq report — per requirement: implemented / verified + last verdict
make traceability-report # regenerate docs/traceability_report.md
make kani # category-1 mechanical proofs (Kani) over qrusty_core
```
`check-requirements` also runs as step 5/9 of `make pre-merge`. `scripts/validate_dependencies.sh`
(`make validate-deps`) reports whether `provreq` is on `PATH`.
#### `make kani` — category-1 mechanical proofs (#113)
The category-1 proofs (PER-0002's queue-key scheme — prefix construction and range-exactness) live in
the pure, C-free `qrusty_core` crate so Kani can codegen them without the umbrella crate's rocksdb FFI.
Run them with:
```bash
make kani # cargo kani -p qrusty_core → VERIFICATION SUCCESSFUL
```
The target runs Kani under an **isolated empty `CARGO_HOME`** and a **cleared `RUSTFLAGS`**. The base
image ships `~/.cargo/config.toml` with a forced `[build] target` (equal to the native triple) plus a
crt-static `RUSTFLAGS`; the forced target has historically malformed cargo-kani's internal
`rustc --print` probe (`error: failed to run rustc to learn about target-specific information`). The
isolated `CARGO_HOME` drops that forced target — safe here because `qrusty_core` is std-only, so there
is no registry cache to lose. **Do not** copy this empty-cache pattern to the asserted (`cargo test`)
verify route: that builds rocksdb and needs the real cache.
The upstream fix (dropping/scoping the forced `[build] target` in the base image so even a bare
`cargo kani` works everywhere) belongs in `greeng3/provreq-devcontainer`; this target is the
repo-owned bypass so cat-1 proving is a no-ceremony workflow here regardless.
### Doorstop heritage viewer
The pre-provreq Doorstop tree is archived read-only under `docs/doorstop-heritage/`. It can still be
browsed with `doorstop-server` on port **17867**:
```bash
bash .devcontainer/start-doorstop.sh
```
## On-disk layout
| `requirements/` | The provreq project — `provreq.json` marker + `artifacts/<prefix>/*.md`. |
| `ProvableRequirements/` | The provreq companion tree (triage, drafts, verdicts, `provreq.yml`). |
| `docs/doorstop-heritage/` | The archived pre-provreq Doorstop tree (read-only). |
| `docs/traceability_report.md` | Generated by `provreq report` (kept in provreq's own text shape). |
The provreq-managed trees and the generated report are excluded from this repo's
prettier / markdownlint / yamllint runs (`.prettierignore`, `.yamllint.yml`, and the `lint-md`
exclusions) — their shape is provreq's to decide, not the formatter's.