usage: con-ron [--verified|--trusted] [--jobs=<n>] [--no-mark-persistent]
               [--progress[=<stride>]] [--pins FILE|--no-pins]
               FILE.ndjson
       con-ron --help

  --verified        the default, and the mode the main theorem is about: if
                    the declaration fold accepts a stream in this mode, the
                    environment holds no constant whose type is False
                    (ConLeche.no_proof_of_False, and DESIGN.md §1's
                    conron.no_proof_of_False for the port).
  --trusted         the unverified mode: the SAME checker bodies at the mode
                    with the certification-only work switched off.  An accept
                    in this mode is outside the theorem.
  --jobs=<n>        the check phase's worker count: <n> workers claim records
                    one at a time off a shared counter, and --jobs=1 runs the
                    plain loop with no counter and no result table.  The
                    verdict, and the declaration a rejection names, are the
                    same at every <n>: the results are walked in RECORD order,
                    so the first failing record in fold order is the one
                    reported.  Each worker reserves 1 GiB of address space for
                    its stack, so a run under `ulimit -v` needs 3x the
                    checker's resident set plus a gigabyte per worker; the
                    DEFAULT is one worker per hardware thread capped at 16 for
                    that reason (con-leche's uncapped default aborts on a
                    96-thread machine).  0 or a non-numeral is a usage error,
                    as in con-leche.
  --no-mark-persistent
                    ACCEPTED AND A NO-OP: the mark it turns off is a
                    Lean-runtime reference-counting device
                    (Runtime.markPersistent), and this program's counts are
                    std::sync::Arc counts -- atomic by type, in every lane,
                    with no runtime mark to clear.  A run that passes it says
                    so on stderr.
  --progress[=<stride>]
                    opt-in progress heartbeat on STDERR, one line shape per
                    phase:
                      con-ron: parse done: <N> fold records ... t=<s>s
                      con-ron: install <i>/<N> <decl> t=<s>s
                      con-ron: install done: <N>/<N> ..., <M> checks pending t=<s>s
                      con-ron: check <done>/<M> <kind> <name> t=<s>s
                      con-ron: check done: <M>/<M> t=<s>s
                      con-ron: done: parse <p>s, install <i>s, check <c>s, <n> workers
                    An install line is printed BEFORE every <stride>-th
                    declaration is installed (<i> is its FOLD position, which
                    the stream's record index sits near but not at a fixed
                    offset above), so a run that dies in the install phase
                    names the declaration it died in on its last line.  A
                    check line is printed AFTER every <stride>-th COMPLETED
                    check.  On a failure the phase's closing line says so
                    ('install failed at', 'check failed at') and the summary
                    still prints.  Bare --progress is stride 1; a stride that
                    is not a decimal numeral, or 0, is a usage error.
  --pins FILE       con-ron's own, FOR TESTING: read the pin list from a
                    `con-ron-pins/1` dump instead of the core's own embedded
                    text (task #43), through the UNVERIFIED reader.
  --no-pins         con-ron's own, FOR TESTING: the empty pin list, the pin
                    loop's `[]` arm, under which a Nat.div/Nat.mod stream
                    declines.  Neither flag is needed for a normal run: the
                    pins are con-leche's `natOpPinSets`, embedded in the
                    verified core and decoded by it.
  --help            print this text on STDOUT and exit 0, in any argument
                    position; no input is read.

exit codes: 0 accepted, 1 rejected, 2 declined, 3 usage/malformed/internal.
An out-of-memory condition is NEITHER: con-leche's exit 1 for it is the Lean
runtime's own panic, and this program instead aborts the way Rust aborts on a
failed allocation ('memory allocation of <n> bytes failed', SIGABRT, which a
shell reports as 134).  A panic is exit 3.

environment (con-leche's):
  CON_LECHE_INMODEL=0          turn the in-process modeller off; a mutual or
                               nested block is then pushed bare and the FOLD
                               declines it, having found no route
  CON_LECHE_INMODEL_CENSUS=1   report every mutual/nested block's outcome
                               after the parse and stop (exit 2)
  CON_LECHE_PROJREC_TRACE      name each rewritten projection function
  CON_LECHE_VERBOSE            print the environment's constant count

RETIRED FLAGS.  --set-model, --set-model=p, --set-model=r, --no-model,
--tt-model, --yolo, --infer-only, --pre, --core, --core=<c>, --install-only,
--check-range and --check-range=<r> are never silent aliases: each is
rejected with a message naming what stands in its place, and the run exits 3
without reading the input, so a verdict's provenance is readable off the
invocation.

NOT PORTED: CON_LECHE_ROUTE_TRACE, the install-route audit (it reads the
recognisers on the environment the step sees, which is a second dispatch of
the fold, not a print); CON_LECHE_INMODEL_DUMP, the debug splice of the
generated records into a copy of the input — it is written through
con-leche's annotated-NDJSON writer (`Frontend/ExportWrite.lean`), an output
path this checker does not have.
