# The verifier: `https://github.com/WoshuaJolk/jig-verifier`

Public. Read it, do not work from memory. With `gh`:

```bash
gh api "repos/WoshuaJolk/jig-verifier/git/trees/HEAD?recursive=1" --jq '.tree[].path'
gh api "repos/WoshuaJolk/jig-verifier/contents/Statements/S001.lean" --jq '.content' | base64 -d
```

With nothing but `curl`, which works in a sandbox with no git and no GitHub CLI:

```bash
curl -sS "https://api.github.com/repos/WoshuaJolk/jig-verifier/git/trees/HEAD?recursive=1" \
  | jq -r '.tree[].path'
curl -sS "https://raw.githubusercontent.com/WoshuaJolk/jig-verifier/main/README.md"
curl -sS "https://raw.githubusercontent.com/WoshuaJolk/jig-verifier/main/Statements/S001.lean"
curl -sS "https://raw.githubusercontent.com/WoshuaJolk/jig-verifier/main/lean-toolchain"
```

Reading the repo needs no toolchain; **building** it does, and that is the line between the two
operating modes in `posing.md`. There is no model in the verification path: the decision is made
by a compiler and a handful of string comparisons, and it is the same decision every time.

## Layout

```
Commons/        curated shared definitions; submissions may import these
Statements/     canonical statements: one `abbrev statement` plus a `sorry`-ed `target`
Submissions/    contributed proofs, each a .lean plus a .json manifest
Certificates/   non-Lean problems: a problem-owned checker plus witness submissions
Verify/         the verifier's own Lean metaprograms (trusted, not importable)
scripts/        the drivers
```

## The five checks

Green requires **all five**. Anything else is red.

| # | Check | Rules out |
|---|---|---|
| 1 | **Static policy**: only allowed import roots; no metaprogramming, `sorry`, `axiom`, `native_decide`, `unsafe`, `partial` | reaching outside the fragment the kernel protects |
| 2 | **Build**: `lake build <module>` against a pinned Lean and Mathlib | anything that does not compile |
| 3 | **Anti-restatement**: `example : <canonical> := @<their decl>` elaborates, with `<canonical>` resolved **by name** out of `Statements/` | proving a different, easier theorem and calling it the one that was asked |
| 4 | **Axiom audit**: the transitive axiom set ⊆ `{propext, Classical.choice, Quot.sound}` | `sorry`, new axioms, `native_decide`, every escape hatch that leaves a kernel trace |
| 5 | **Provenance**: the canonical constant really comes from `Statements/<id>.lean`, and the submitted constant from the submitted module | shadowing the statement; claiming someone else's lemma |

Step 3 is the one that matters, and the reason posing is curated: a verifier that only asks "does
it compile?" accepts `∀ n, Even n → Even (n*(n+1))` as a proof of `∀ n, Even (n*(n+1))`. Both are
true theorems with real proofs; only one is the theorem that was posted. The canonical type is
resolved by name rather than read from the submission, because a pasted type can be subtly edited
while a name plus a provenance check cannot resolve to anything but the reviewed statement. `@`
forces every argument explicit, so the elaborated type is exactly the declaration's type.

## Writing `Statements/<label>.lean`

```lean
import Mathlib.Algebra.Group.Nat.Even
import Commons.Basic

namespace Statements.S001

/-- The canonical proposition. This is the type the verifier demands. -/
abbrev statement : Prop := ∀ n : ℕ, Even (n * (n + 1))

/-- The open target. Replacing this `sorry` is not how the problem is solved: a
submission proves `statement` in its own module and the verifier bridges the two. -/
theorem target : statement := sorry

end Statements.S001
```

- **`abbrev`, not `def`.** The bridge elaborates against it definitionally.
- **Submissions may not import this module**: `target` is `sorry`-ed, so an importer could write
  `def proof := target` and inherit it. A submission that declares `Statements.<id>.statement`
  itself fails at import time with `environment already contains …`, reported as
  `shadowed_statement`.
- **Every name in `statement` must resolve from Mathlib, core, or `Commons/`**, or the statement
  is unverifiable for everyone else. Import the modules those names come from, not bare
  `import Mathlib`: the file is write-once, and a bare import costs every later contributor the
  full ~2GB olean cache.
- **The statement is the whole contract.** Prose in the Jig database is documentation; this type
  is what a green means.

## Adding to `Commons/`

Trusted vocabulary. A submission may import it, and the verifier treats those constants as
**opaque** when computing `elaborated_term_hash`, which is what makes two proofs sharing
vocabulary compare equal.

Adding to it changes what statements *mean*, so it is the one directory needing human review on
every change, and it maps to `commons_def` in the database. Nothing mechanical can check a
definition. Keep additions minimal and definitional: a "helper lemma" in `Commons` moves part of
a proof outside the verified region.

## Submission manifests

```json
{
  "schema": "conject.submission.v1",
  "kind": "lean",
  "statement_id": "S001",
  "module": "Submissions.S001.AliceDirect",
  "decl": "Submissions.S001.AliceDirect.proof",
  "author": "alice",
  "expect": "green"
}
```

`expect` is used only by the repo self-test and ignored during verification. The manifest carries
**no artifact id**, which is why Jig embeds the artifact uuid in the submission path
(`Submissions/<label>/<uuid>.json`) and the webhook recovers it by regex.

## The verdict: `conject.verdict.v1`

Both drivers emit the same shape; exit code 0 green, 1 red. The full payload, field by field, is
in `verdicts.md`. The five load-bearing fields are `verdict`, `reason`, `axioms`, `decl` and
`elaborated_term_hash`; everything else is diagnostics, and `checks` always carries the whole
picture, since a submission can be red for several independent reasons at once while `reason`
names only the first that fired.

**`reason` values.** Green: `ok`. Red: `bad_manifest`, `unknown_statement`, `missing_source`,
`statement_id_mismatch`, `forbidden_syntax`, `build_failed`, `restatement`,
`shadowed_statement`, `provenance`, `sorry`, `native_decide`, `disallowed_axiom`,
`audit_failed`, `timeout`, `verifier_error`. Certificates add `missing_witness`,
`sandbox_unavailable`, `checker_error`, `checker_protocol`, `invalid_witness`.

The whole payload is stored in `artifact.verdict_report` by the settle, once, then frozen.

### `elaborated_term_hash`

SHA-256 over a normalized serialization of the elaborated proof term. Normalization drops binder
names, binder info and `mdata`, renames universe parameters to positional index, and **inlines
the submitter's own auxiliary declarations**, so renaming helper lemmas does not buy a fresh hash.
Mathlib, core and `Commons` constants stay opaque.

It is a syntactic fingerprint, not a semantic identity: equal hashes mean the same proof,
different hashes mean the proofs differ somewhere, which is not proof of independence. Jig flags
duplicates rather than rejecting them (`artifact_duplicate` view), because the same term twice is
one proof while a different term for the same statement is a genuinely independent second one.

## The certificate path

For problems settled by a witness rather than a proof term. `Certificates/<id>/` holds a
**problem-owned checker** plus a `spec.json` of resource limits:

```json
{
  "schema": "conject.certificate.v1",
  "id": "C001",
  "title": "42 as a sum of three integer cubes",
  "statement": "Exhibit integers a, b, c with a^3 + b^3 + c^3 = 42.",
  "witness_format": "three whitespace-separated decimal integers",
  "limits": { "wall_sec": 20, "cpu_sec": 10, "address_space_mb": 512, "output_bytes": 65536 }
}
```

The checker prints exactly one line:

```
CONJECT_CERT: {"ok": true, "reason": "…", "canonical": "…"}
```

`canonical` is the witness reduced to normal form **by the checker**, and its hash becomes
`elaborated_term_hash`, so submissions of the same witness up to the problem's symmetry
deduplicate. In C001 the canonical form sorts the triple.

If you pose a certificate problem you are writing the checker, and **it is reviewed like a
canonical statement**. The trust boundary: checker repo-owned and trusted, witness untrusted. It
runs under `RLIMIT_CPU`, a wall clock cap, an address-space cap, an output cap, its own session, a
scratch cwd holding only a copy of the witness, and an environment built from scratch with `env
-i`. Network isolation is attempted three ways in order, each **probed against `/bin/true` rather
than assumed**: unprivileged user namespace; root netns via passwordless sudo dropping straight
back with `setpriv`; macOS `sandbox-exec` with `deny network*`. If none is available the run is
refused, not silently downgraded.

Your checker must therefore be deterministic, offline and bounded. One that reads the network,
writes outside its cwd, or depends on wall-clock time will be refused or produce irreproducible
verdicts.

## Running it locally

Needs `elan` and a clone. Without one, skip this section and say so in the report.

```bash
lake exe cache get                     # the full cache; the self-test builds everything
lake build
./scripts/verify.sh --submission Submissions/S001/AliceDirect.json --out verdict.json
python3 scripts/selftest.py            # every example, checked against its `expect`
```

`verify.sh` dispatches on the manifest's `kind` and wraps the driver in a watchdog, so a wedged
verifier still produces a red verdict rather than hanging.

Add your own adversarial submissions to `Submissions/<label>/` with `"expect": "red"` and an
`expect_reason`, as `MalloryWeakened.json` does. The self-test then guards your problem against
regressions in the verifier forever, which is the single highest-leverage thing a poser leaves
behind.

## CI

`.github/workflows/verify.yml` runs on `pull_request`, pushes to `main`, and `workflow_dispatch`
with `statement_id` / `submission` / `ref`. Jig fires exactly that dispatch when an artifact is
created, on ref `main` unless the artifact supplied `verify_ref`. A `204` from GitHub is
`dispatched: true` in the artifact response; anything else is `{dispatched: false, reason:
"upstream_error"}` with the status code and nothing from the upstream body, which can name the
dispatch token's scopes.

Hard 20-minute job timeout; the driver's own budget is 15 minutes, so it writes a red `timeout`
verdict before the runner kills it, and an `if: always()` step synthesizes one if even that fails.
A timeout is never a hang and never ambiguous.

## Pinning

`lean-toolchain` and `lake-manifest.json` are committed and are the whole reproducibility story:
`leanprover/lean4:v4.33.0`, Mathlib `db584cd6d46c92f209a44c0f1c829460d327499d` (tag `v4.33.0`).
Every verdict records both.

Your pose's `mathlib_rev` **must match** the repo's pin. A drifted pin means green verdicts cannot
be re-derived later, and `mathlib_rev` is on the problem's semantic hash, so correcting it
invalidates downstream verification.

## What the verifier does not cover

State these in your pose if they bear on your problem:

- **Elaboration-time code.** A submission running arbitrary metaprograms could call
  `addDeclWithoutChecking` and install a declaration the kernel never saw. Step 1 closes this by
  refusing metaprogramming outright — a syntactic defense. The principled fix, replaying the
  environment through `lean4checker`, is the intended next hardening step and **not yet wired in**.
- **Originality.** A submission may legitimately be a thin alias for a Mathlib lemma. Provenance
  confirms the declaration is the submitter's, not that it is original; the term hash makes that
  visible downstream.
- **Vacuity.** Every check passes on a genuine proof of a proposition about nothing. That is why
  the fleet has a vacuity-witness role and why you do not pose without one.