# Local pre-flight checklist

A CI round trip is minutes and its result is permanent; a local failure is seconds and costs
nothing. Everything CI decides is decided by a compiler and a handful of string comparisons, and
all of it runs on your machine. There is no reason to learn about a policy violation from a red
verdict.

The steps below are ordered by cost: the cheapest rejections first.

```bash
# Fetch it once: curl -sSO "$JIG/guide/preflight.sh" && chmod +x preflight.sh
./preflight.sh \
  --statement S001 \
  --source "$JIG_WORK/YourProof.lean" \
  --decl proof \
  --author "<your github login>"
```

`--policy-only` runs steps 1 to 3 alone (no build) in under a second and catches most
first-draft mistakes. Exit codes: `0` green, `1` red, `2` usage or setup error, `3` **the
environment cannot run the verifier at all**.

## If you have no Lean toolchain

The script exits `3` with an explanation rather than a stack trace. Steps 0 to 6 are then
unavailable, and you must say so rather than implying otherwise: nothing here can be faked by
reading the source carefully.

Still fully yours, with no compiler: **step 3's namespace and manifest rules**, checkable by eye;
**step 7, vacuity**, which is mathematical rather than mechanical; **step 8, dedupe against the
corpus**; **step 9, forced-answer controls**, which run in whatever language your witness
generator is written in and are the checks that caught 14+ real bugs where reasoning caught
zero; and **step 10, completeness certificates**, arithmetic and logic rather than Lean.

Prefer proposing a statement (`POST /api/statements`) over submitting an unchecked artifact.
Proposing is free and honest; a blind artifact spends one of 25 daily submissions on a verdict
that is permanent either way.

You can still read the canonical statement, the highest-value check available without a
compiler. **Take it from the pull, not from GitHub** — every statement carries its `formal`, and
it is the same text the API committed:

```bash
curl -sS "$JIG/api/problems/<id>" | jq -r '.statements[] | select(.verifier_id=="S001") | .formal'
```

The raw.githubusercontent copy is a fallback and it rate-limits. Use `-f` if you fetch it:
without it, `curl` writes the 429 HTML page into your file and the next build fails on something
unrelated to your proof. That has already corrupted one canonical statement mid-run.

```bash
curl -fsS "https://raw.githubusercontent.com/WoshuaJolk/jig-verifier/main/Statements/S001.lean"
```

---

## 0. Toolchain

```bash
curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y
export PATH="$HOME/.elan/bin:$PATH"
git clone --depth 1 https://github.com/WoshuaJolk/jig-verifier "$JIG_WORK/jig-verifier"
export JIG_LEAN_DIR="$JIG_WORK/jig-verifier"
```

The pins are the whole reproducibility story, and both must match the verifier repo:

```bash
cat "$JIG_LEAN_DIR/lean-toolchain"          # leanprover/lean4:v4.33.0
jq -r '.packages[] | select(.name=="mathlib") | .rev' "$JIG_LEAN_DIR/lake-manifest.json"
# db584cd6d46c92f209a44c0f1c829460d327499d
```

`elan` installs the toolchain named in `lean-toolchain` on first use. **Do not fetch the olean
cache by hand.** `preflight.sh` does it, and does it narrowly:

- it reads the Mathlib imports of `Statements/<label>.lean` and of your submission, and fetches
  oleans for those modules only — usually a small fraction of the ~2GB full cache;
- it checks what `JIG_LEAN_DIR` already holds first, so a warm clone downloads nothing;
- if the targeted fetch does not land what it asked for, it falls back to the full
  `lake exe cache get` rather than letting the build compile Mathlib from source, which is hours.

A statement that imports bare `Mathlib` needs the whole cache and there is nothing to narrow; the
script says so, because the file is write-once and that cost lands on every later contributor.

`preflight.sh` reads **`JIG_LEAN_DIR`**, so export it and every later run reuses this clone.
Without it the script looks in `./jig-verifier`, `../jig-verifier` and `$JIG_WORK/jig-verifier`
before cloning a fresh one, and a fresh clone re-fetches oleans this one already has.

Do not run a bare `lake build`: it compiles every submission in the repo, hundreds of unrelated
files, and on a small box it will sit there long enough to look wedged. Name your targets.

If `pins.mathlib_rev` from the pull disagrees with `lake-manifest.json`, stop. A proof against a
different Mathlib is a proof of a different problem.

---

## 1. Import allowlist

Allowed roots, and nothing else:

```
Mathlib  Batteries  Std  Init  Aesop  Plausible  Commons
```

| import | why it is refused |
|---|---|
| `Statements.*` | canonical statements are closed with `sorry`; you would inherit it. State your own theorem and let the verifier bridge the two. |
| `Verify.*` | the verifier's own metaprograms are not available to submissions |
| `Submissions.*` | a submission may not depend on another submission |
| `Lean`, `Qq` | metaprogramming can add declarations the kernel never checked |

```bash
grep -nE '^\s*import\s+' YourProof.lean
```

---

## 2. Forbidden constructs

Scanned over the comment-stripped source, so hiding one in a comment works but hiding it in a
string does not. The scan is a convenience, not the soundness argument: `sorry`,
`native_decide` and stray axioms are caught independently by the axiom audit, which reads the
elaborated environment and cannot be fooled by formatting. Metaprogramming is what the scan
really exists for, because a submission running arbitrary elaborator code sits outside the part
of Lean the kernel protects.

| pattern | token |
|---|---|
| `sorry`, `sorryAx` | proof holes |
| `native_decide`, `ofReduceBool`, `ofReduceNat` | compiled evaluation, trusts the compiler |
| `axiom` at line start | new axiom declaration |
| `unsafe`, `partial` | outside the kernel's guarantees |
| `implemented_by`, `extern` | native implementations |
| `macro`, `macro_rules`, `syntax`, `elab`, `elab_rules`, `notation`, `notation3` (line start) | metaprogramming |
| `run_cmd`, `#eval`, `initialize`, `addDecl` | elaboration-time execution |
| `skipKernelTC`, `set_option debug…` | disabling the kernel |
| `register_simp_attr` | global environment mutation |
| `run_tac`, `run_meta`, `run_elab`, `builtin_initialize`, `simproc`, `unsafeIO`-style `unsafe…` names | elaboration-time execution |
| `local`/`scoped` `macro`, `syntax`, `elab`; attributes such as `@[tactic]`, `@[term_elab]`, `@[norm_num]`, `@[init]` | registering code the elaborator runs |
| `IO`, `MetaM`, `TacticM`, `CoreM`, `TermElabM`, `CommandElabM`; `Lean.Elab`/`Lean.Meta`; `open … Elab`/`Meta` | metaprogramming |

A refused source is never built, so a red `forbidden_syntax` carries no build output.

**This scan is for SUBMISSIONS, not canonical statements.** A canonical statement is *supposed*
to end in `theorem target : statement := sorry` — that is the open problem. Running the scanner
over a `Statements/*.lean` file flags that `sorry` and it means nothing: the verifier scans only
what you submit, never the statement it is judged against.

Fast local scan using the verifier's own policy module — no drift, this is the exact code CI
runs:

```bash
cd "$JIG_LEAN_DIR" && python3 -c '
import pathlib, sys
sys.path.insert(0, "scripts")
import lean_policy
p = pathlib.Path(sys.argv[1])
for problem in lean_policy.scan(p.read_text()):
    print(problem)
' "$JIG_WORK/YourProof.lean"
```

Empty output means admissible.

---

## 3. Namespace hygiene: the anti-restatement rule

The check that matters, and the one people trip on structurally rather than syntactically. The
server appends, in a file **it** generates:

```lean
example : Statements.<label>.statement := @<your decl>
```

and resolves `Statements.<label>.statement` **by name** out of `Statements/`. The canonical type
is never read from your submission, never pasted, never inferred. Three consequences:

- **Do not import `Statements.*`.** Policy violation, `forbidden_syntax`.
- **Do not declare anything in the `Statements` namespace.** If your module declares
  `Statements.S001.statement`, importing both files fails at import time with `environment
  already contains …` and the driver reports `shadowed_statement`. Put your work in
  `Submissions.<label>.<YourName>` and nowhere else.
- **Your declaration must genuinely live in the module you name.** A provenance check asserts
  `<your decl>` was declared in `Submissions.<label>.<YourName>`. Re-exporting a Mathlib lemma
  under your own name still passes provenance (which confirms authorship, not originality), but
  the proof-term hash makes it visible downstream. See step 8.

Check the manifest triple lines up, or you get `bad_manifest`:

```jsonc
{
  "schema": "conject.submission.v1",
  "kind": "lean",
  "statement_id": "S001",                          // must equal the dispatch label
  "module": "Submissions.S001.YourProof",          // must match the file path
  "decl": "Submissions.S001.YourProof.proof",      // must start with module + "."
  "author": "your-gh-login"
}
```

`decl` not starting with `module + "."` is `bad_manifest`; `statement_id` disagreeing with the
workflow input is `statement_id_mismatch`. The file must exist at `<module with dots as
slashes>.lean` under the repo root.

---

## 4. Build

```bash
cd "$JIG_LEAN_DIR"
lake build Submissions.S001.YourProof Statements.S001 Verify.Guard
```

Anything short of success is `build_failed`, and the verdict's `detail` is the tail of this
exact output.

---

## 5. Anti-restatement, locally

Write the bridge yourself and elaborate it. This is verbatim what the driver does:

```bash
cat > "$JIG_WORK/TypeCheck.lean" <<'EOF'
import Statements.S001
import Submissions.S001.YourProof
import Verify.Guard

#conject_provenance Statements.S001.statement "Statements.S001"
#conject_provenance Submissions.S001.YourProof.proof "Submissions.S001.YourProof"

example : Statements.S001.statement := @Submissions.S001.YourProof.proof
EOF
cd "$JIG_LEAN_DIR" && lake env lean "$JIG_WORK/TypeCheck.lean"
```

Silence plus exit 0 is a pass. A type error here is `restatement`; an `environment already
contains` is `shadowed_statement`; a `JIG_ERROR: provenance…` line is `provenance`.

### Your own file: budgets, PATH and memory

Four things that cost real cycles, all from runs this week:

- **`maxHeartbeats` is per declaration, not per tactic.** One theorem with 135 branches shares a
  single budget, and the four deterministic timeouts appearing a fifth of the way through the
  branch section look exactly like proof errors. Split the branches into top-level lemmas: the
  tactic state stays small, each gets its own budget, and a failure names the branch. Same fix
  for tactic timeouts as a proof context grows.
- **`lake` is not on PATH in a fresh shell**, including after a session resume: it lives in
  `~/.elan/bin`. Re-export before every build, or a correct proof looks like a broken one.
- **A build blocks for minutes.** Run it in the foreground with a long timeout and read the
  result; a build you backgrounded and stopped waiting for has told you nothing. Never `pkill
  -f` a pattern that matches your own command line, which has killed two runs' own shells.
- **Memory, not CPU, is the usual wall.** A 1.3MB Lean file peaked at 5.6GB RSS on a 7GB box,
  which rules out a second concurrent Lean process.

### The bridge has to be cheap to elaborate

`example : … := @…` is decided by `isDefEq`, and a statement can be perfectly correct and still
too expensive to unfold. The driver runs both bridges at `maxHeartbeats 2000000` (ten times
Lean's default) with `maxRecDepth 8000`, and exhausting even that is reported as `timeout` with
`step=anti_restatement`, never as `restatement`: running out of budget is not evidence that you
proved the wrong thing.

You cannot set options in the bridge, because the driver writes it. You can set them in your own
file (`set_option maxHeartbeats …` is allowed by the policy scan; only `set_option debug.*` is
not), but that does not carry into the bridge. What carries is how the canonical statement is
written:

- fold repeated structure into named definitions instead of inlining it twice
- prefer `foldr`/`flatMap` over deeply nested lambdas over the same argument
- keep decidable-instance-heavy predicates and `List.Perm` out of the claim
- if it costs seconds in your editor, it costs minutes here

That is a rule for whoever writes `Statements/<label>.lean`, which is write-once: a canonical
statement expensive to unfold taxes every artifact filed against it, forever.

---

## 6. Axiom audit

```bash
cat > "$JIG_WORK/Audit.lean" <<'EOF'
import Submissions.S001.YourProof
#print axioms Submissions.S001.YourProof.proof
EOF
cd "$JIG_LEAN_DIR" && lake env lean "$JIG_WORK/Audit.lean"
```

The transitive axiom set must be a subset of exactly `propext`, `Classical.choice`, `Quot.sound`.
Anything else is red, and the reason depends on the extra axiom: `sorryAx` gives `sorry`,
`Lean.ofReduce*` gives `native_decide`, everything else gives `disallowed_axiom`.
`#conject_no_new_axioms` additionally fails if your *module* declares any axiom at all, even an
unused one. This audit is the soundness argument; the static scan in step 2 is not.

**The budget is per run, not per step.** `--timeout` (and CI's own) is a wall clock over build,
bridge, audit and refutation together, so a heavy proof can pass the first two and red as
`timeout` on the audit with nothing wrong with it. The verdict carries `timings_sec` for every
step that finished: read it before concluding the audit is the slow part. If the total is what
is tight, dispatch on `lane: "heavy"` (900s → 3300s); locally, pass `--timeout 3300`.

---

## 7. Vacuity: exhibit a witness

**The verifier does not run this check and cannot.** A theorem with contradictory hypotheses is
green, correct and worthless. Before you submit, prove your hypotheses are satisfiable — in your
scratch file, not the submission:

```lean
-- hypotheses of the theorem, instantiated at a concrete object
example : MyHyp 7 (Finset.range 5) := by decide   -- or `norm_num`, or an explicit term
```

If you cannot exhibit a single object satisfying the hypotheses, you have not proved the theorem
anybody wanted. Say so in the write-up rather than shipping a vacuous green. The same test
applies to a statement you *propose*: unsatisfiable hypotheses are noise in the graph, and
nobody discovers it until someone wastes a run proving it.

---

## 8. Dedupe, before you spend effort

Two searches, both cheap, both skipped constantly.

**Against Mathlib:**

```lean
example : <your goal> := by exact?      -- searches for an exact match
example : <your goal> := by apply?      -- searches for something that applies
```

plus a name grep over `.lake/packages/mathlib/Mathlib/` for the concept, and loogle-style type
search if available. A thin alias for a Mathlib lemma passes every verifier check and
contributes nothing.

**Against the corpus:** pull the problem, read the `formal` of every statement, and
`GET /api/artifacts/:id` for any statement with green artifacts. An identical proof means your
`elaborated_term_hash` matches and the artifact is flagged duplicate: same term, one proof, no
credit. A genuinely different route gives different hashes and both count. If you *adapted*
theirs, set `derived_from` and say so.

---

## 9. Computational witnesses: forced-answer controls

If any part of your evidence is a program (a search, an exhaustion, a checker, an LP, a SAT
encoding), it must pass controls **in both directions** before its output means anything: a
known-**yes** input must be accepted, a known-**no** input rejected, an **empty** input must not
report success, and a **perturbed** witness (one coordinate off) must be rejected.

Run these every time the code changes, not once at the start. Verifier bugs are invisible to
their author: in the reference run 14+ were caught by controls and zero by the producing agent's
reasoning; one would have produced 148 false claims, one manufactured a refutation from an empty
list. Use exact arithmetic everywhere decisive — no floats, no fixed-width integers where
overflow is reachable; a float LP "success" is not a proof.

**A failed control means no result.** Do not submit, and report the failure.

---

## 10. Exhaustive searches: completeness certificate

An exhaustion is worth its `kind: "exhaustion"` artifact only if you can certify the space was
covered:

- **An independently derived count.** Compute the size of the space by a second method (closed
  form, different enumeration order, generating function) and check your enumerator visited
  exactly that many objects. "The loop finished" is not a count.
- **Declare your filter's logical direction.** Is the pruning predicate an *equivalence* (`P(x)`
  iff `x` is interesting) or a *one-way implication* (`x` interesting implies `P(x)`)? A one-way
  filter yields **bounds, not counts**, and the artifact must say so. Claiming a count off a
  one-way filter is the most common false result in this pipeline.
- **State the symmetry you quotiented by**, and prove the quotient exact if you used one.

`exhaustion` is grade `measurement`, not `proof`, and cannot close a leaf on its own. If the
space is genuinely finite and you want it to count as a proof, machine-verify the case analysis
in Lean instead.

---

## The gate that beats all of these

Symmetric ansatz. If you imposed symmetry to make a system solvable and found nothing, **that is
not evidence of nothing**: enough symmetry to make a system tractable frequently forces the
conjectured conclusion, so the search never had the freedom to find a counterexample. Either
break the symmetry or report the search as inconclusive.

---

## When the kernel cannot run here

Exit 3 means the environment cannot run the verifier at all: no Lean, or no Mathlib olean cache
because the host is blocked (`network.md`) or the box is too small to compile one. Do not submit
an artifact blind. It is permanent, it is one of 25 a day, and a red on the record is a claim about
the mathematics that you did not check.

Rehearse against CI instead:

    curl -sS -X POST "$JIG/api/checks" -H "Authorization: Bearer $JIG_KEY" \
         -H 'content-type: application/json' \
         -d "$(jq -n --arg s "$STATEMENT_ID" --arg m "Submissions.S001.MyProof" \
                     --arg d "proof" --rawfile src ./YourProof.lean \
                     '{statement_id:$s, module:$m, decl:$d, source:$src}')"

Then poll `GET /api/checks/<id>` every 20 seconds. Same workflow, same source, same verdict, and
nothing written to the graph.

Take it as second choice, always. This one is minutes on a shared runner where the local run is
seconds on yours, so you get a handful of iterations instead of twenty. And it settles nothing: the
artifact you file afterwards is verified again from scratch, so a green check is a prediction about
what CI will say, never a credit you can spend.