coq-kernel: the "no Admitted" gate exits 2 before it reads a file (bash array under dash) #3396

The Kernel PHI Admitted gate cannot fail for the reason it exists, and cannot pass for that reason either: under the container shell it dies on syntax before reading a single file.

The defect

.github/workflows/coq-kernel.yml, step Verify Kernel PHI layer has no Admitted, declares no shell: key, and neither does the job. The job runs in the coqorg/coq container, so the step shell is sh -e — dash. The body uses four bash-only constructs:

VFILES=()                       # line 61 of the body — the first one dash rejects
VFILES+=("coq/$f")
"${#VFILES[@]}"
done < <(grep -E "\.v$" coq/_CoqProject)     # process substitution

The step comment already states the constraint — "This job runs in the coqorg/coq container, where the step shell is sh -e -- dash" — and the code below it then violates that constraint.

Measured

The step body was extracted verbatim from origin/master (89 lines, refusing to run if the extract does not contain VFILES) and run against a tree holding the 9 .v files coq/_CoqProject names, materialised from origin/master. Two shells × two states. /bin/sh on macOS is bash 3.2 and accepts arrays, so it is not a valid control here; /bin/dash was used.

Under the CI shell the gate returns the same thing whether or not an Admitted exists — it carries no information. Under bash it discriminates correctly. The bash row is the positive control: it proves the probe can tell the two states apart, so the dash row is a finding and not a broken probe.

Why it was not caught

The meta-gate written to protect this gate extracts the body from the YAML correctly and then runs it through subprocess.run(["bash", "-c", body]) — in a different shell from the one CI uses. It passes 13/13 and exits 0 on the same body that dash refuses. A gate and its guard disagreeing about the shell is the whole defect.

Separately, Coq kernel is not one of the four required contexts, so a red run here does not block a merge.

Repair

One line: shell: bash on the step, which is what the body was written for. Failure direction is safe — if bash were absent from the image the step fails loudly rather than passing silently.

The meta-gate needs the same shell as CI, or it will keep certifying bodies CI cannot run; that is the larger half and is filed here as context, not fixed by the one-line change.