CRUX verb correspondence (#3739 amendment): every leaf of the derived apr surface maps to its llama.cpp/ollama counterpart or comparator: none + reason #3774

Child of #3739, for its scope amendments. 17:19Z (issuecomment-5764587628), verbatim: "Every derived verb has a CRUX mapping entry in one committed correspondence file: its llama.cpp counterpart and/or its ollama counterpart, with argument mapping. ... Or the entry is comparator: none with a reason. A derived verb with NO entry is a SHACL violation. Absence is never "no comparator"." 19:03Z adds "the correspondence file gains an hf column", and 19:04Z adds a llamafile column.

Schema, agreed with aprender-97 (#3715 / #3745 S2, the shape side that reads this file):

• evidence/crux/verb-correspondence.yaml, not contracts/, because pv walks contracts/ as provable contracts.
• Every entry states EVERY engine explicitly, as a mapping or {none: "<reason>"}, so "hf omitted" can never read the same as "hf forgotten". aprender-97, verbatim: "make absence explicit PER ENGINE rather than only per verb ... a missing engine key is a violation on the shape side".

done_when

• evidence/crux/verb-correspondence.yaml (schema: crux-verb-correspondence/v1) has exactly one entry per LEAF key of the surface apr surface --json emits (P0: release cells are hand-coded, not DERIVED from apr's interface — the gate cannot see a verb, flag or input shape nobody typed into a list (run --prompt --chat, serve, code all leaked) #3745 S1, apr-cli-surface/v1), hidden and foreign leaves included, with aliases counted as the same verb. It carries surface: {source, sha256} binding it to the emitted surface it was derived from.
• Every entry has comparators with ALL FOUR engine keys (llama.cpp: {binary, args}, ollama: {subcommand, args}, hf: {api, args}, llamafile: {binary, args}), each either that mapping or {none: <non-empty reason>}. An entry with at least one mapping has judged_by ∈ golden | greedy_tokens | task.
• Measured at authoring and recorded, each with a negative control that fails:
  • every mapped llama.cpp binary exists in the pinned build (d1d3c3396) and every mapped flag appears in its --help;
  • every ollama subcommand and flag appears in ollama --help (0.33.2);
  • every mapped apr flag is an arg of that verb in the surface.
• Out of scope, each with its owner:
  • the hf and llamafile mappings are declared here but verified against their pins by the engine worker's rows, since the pins don't exist yet;
  • the SHACL reading is aprender-97's S2;
  • the cells for newly mapped verbs are later CRUX inference dogfood, every release: the SAME GGUF + SAME prompts through apr, llama.cpp and ollama, per verb (run / chat / serve / code) on lambda and gx10 — apr must be right wherever a competitor is right #3739 slices.

Added 2026-09-21 ~19:30Z: the judge side and the driver hook

The cop assigned these to #3774, verbatim: "You own the correspondence file columns (hf and llamafile) and the judge side (#3774)". The engine drivers themselves are the engine worker's (infra-3c, PMAT-3778). Row contract v1 is #3739 (comment), with its correction at issuecomment-5766162965.

• scripts/lib/crux_inference_judge.py treats hf and llamafile as comparators: RED when either is right and apr is wrong. Their gen rows are read in the contract's JSON ({"text": …}); output that isn't that JSON, or has no text, is no answer.
• tok rows (raw-text ids, carrying input) and tmpl rows (chat rendering) are byte-equal or RED, with the first differing index or byte named.
  • An engine row with no apr row beside it is RED.
  • A row the reference engine refused is UNJUDGED, and the run declines.
  • greedy rows are REPORTED: the first divergence, plus the logit cosine there from .npy, read with the stdlib.
• scripts/crux_inference_dogfood.sh exports CRUX_MANIFEST and CRUX_WORK, resolves scripts/crux_engine_<hf|llamafile>.{sh,py}, and records its probe output verbatim in the receipt. Inside each cell's GPU lock it calls gen with the pin's sampling; llamafile gets --interface server. A missing script, a failing probe, or a gen that appends no row becomes a refused row naming why.
• scripts/check_crux_inference_judge.sh covers each rule with a row, and a mutant of each rule turns the table RED.

Added 2026-09-21 ~21:15Z: three things the engine integration forced

• The GPU lock goes through gpu-q (the cop, verbatim: "Make the script prefer gpu-q: GPUQ_WAIT=<bound> gpu-q --prio ${CRUX_GPU_PRIO:-5} -- … when gpu-q --caps lists wait … falling back to your bounded flock with "may have jumped the queue" recorded").
  • Each cell (one prompt, every engine) is written as one script and runs as ONE gpu-q command.
  • ollama's unload wait runs inside the cell.
  • Exit 75 means every engine of that cell is a refused row.
  • harness.gpu_lock records which path ran.
• evidence/crux/hf-sources.yaml maps each GGUF (by sha256) to the HF source weights at a PINNED revision. The GGUF side's provenance is the repo's LFS sha256 equalling the file's. The driver passes --source-repo/--source-revision/--dtype to the hf engine, and a GGUF with no entry is a refused hf row naming the gap.
• A degenerate answer is no answer, from any engine: 8 or more non-space characters, 90% or more of them one character. On the integration run a broken HF load emitted ! × 64, and the golden greeting pattern "!" scored it correct (apr qa golden_output: the greeting case's "!" pattern scores degenerate output ("!!!!", token id 0) as correct #3782 is the Rust gate's copy of that hole).