From e733b64906e6d951ecb7c5f1402817832942fad6 Mon Sep 17 00:00:00 2001 From: Konrad Heimel Date: Sun, 23 Aug 2026 21:09:12 +0200 Subject: [PATCH 1/4] :lock: fix(release): grade EVERY cosign invocation, not just some (UNIV-COSIGN, D-160) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit hack/release/install_cosign_pin_test.sh asserted an EXISTENTIAL property where the guarantee it publishes is UNIVERSAL. Every individual assertion was sound and the conjunction still certified nothing: a second, UNPINNED `cosign verify-blob` appended to any of the three graded files ran the gate to exit 0 — measured before the fix, hack/install.sh rc=0, SECURITY.md rc=0, hack/release/verify-artifacts.sh rc=0. Mechanism: `has_flag` grepped the whole folded extraction so a pinned sibling satisfied it; `one_value`'s `sort -u` collapsed the agreeing values so the D-153 drift comparison saw a consistent file; section 0 PRINTED the invocation count and asserted nothing about it; and 4b/5d's stub-log checks were positive-only greps, the same shape at runtime. SECURITY.md was worse than the other two — it fed only the drift comparison and had no invocation-level grading at all. This is the AUD2-S05 quorum defect one layer out: not a wrong assertion, a wrong quantifier. The property is now universal: every `cosign verify-blob` invocation in every graded file carries --certificate-oidc-issuer, --certificate-identity-regexp and --bundle, each with SECURITY.md's published value. Presence alone is not a pin — `--certificate-identity-regexp ''` carries the flag, matches every Fulcio identity ever issued, and slips past `sort -u` because an empty capture is not a line — so each invocation's own value is compared (WRONG-VALUE, distinct from UNPINNED). Classification fails CLOSED: an occurrence that is neither at command position nor a backticked prose mention is reported UNCLASSIFIABLE, never skipped. "Exactly one invocation per file", the remedy recorded when the finding was filed, was rejected as FALSE on this tree: SECURITY.md legitimately publishes two, one over the archive and one over checksums.txt. Anti-vacuity: sections 2b/2c run eight mutants against each of the three files plus a prose-exemption control, chosen for BRANCH coverage of the new predicate rather than variety of shape — second-unpinned (must red, name the file, quote the call, and produce exactly the two UNPINNED lines so pinned siblings are provably unflagged), second-pinned (must stay green AND raise the extractor's invocation count), off-command-position appended fully pinned so only the classifier can redden it, no-candidates, fold-broken (asserted NOT to also report UNPINNED, since conflating the two sends the maintainer to the wrong file), no-invocations, empty identity regexp, foreign issuer. The runtime twin has its own vacuity control. hack/install.sh, SECURITY.md and hack/release/verify-artifacts.sh are byte-unchanged: all four of their invocations were already pinned. This closes a hole in the checker, not in the checked. The stage was already wired into `task check` and pinned in CHECK_STAGES, so no wiring changed. --- CHANGELOG.md | 1 + docs/decisions/decisions.md | 1 + hack/release/install_cosign_pin_test.sh | 446 ++++++++++++++++++++++-- openspec/specs/backlog.md | 1 + 4 files changed, 411 insertions(+), 38 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 9c7d86a..e46ee7d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -119,6 +119,7 @@ repository still gets a decision, never by following the link; no release carrie - :lock: fix(provider): bound exec stdout, set WaitDelay, capture stderr - :lock: fix(release): pin cosign signer identity on the maintainer verify path (AUD2-F01) - :lock: fix(hack): refuse to run gate scripts under a too-old bash (BASH32-F01) +- :lock: fix(release): grade EVERY cosign invocation, not just some (UNIV-COSIGN, D-160) ### Testing - :white_check_mark: test(cmd): assert the REL-03 error wrap as one contiguous substring diff --git a/docs/decisions/decisions.md b/docs/decisions/decisions.md index 97393f1..99dc226 100644 --- a/docs/decisions/decisions.md +++ b/docs/decisions/decisions.md @@ -162,3 +162,4 @@ project/process decisions. | D-156 | 2026-08-23 | **The tier-1 (CEL) ceiling is recorded (`docs/planning/rego-tier-ceiling.md`, E11-S01 / REQ-E11-S01-01+02) and it NARROWS E11: two of the four named shapes are struck outright and a third in part.** Substance first: of multi-pass / cross-manifest / set-difference / graph-relationship (`openspec/specs/later-phases.md:284`), **cross-manifest and set-difference are struck, the "named intermediate" half of multi-pass is struck, and only fold/aggregate-over-a-collection and in-input graph reasoning survive as justification for a second backend.** Measured against the surface this repo actually binds — `internal/core/aggregate/evaluate.go` `newEvalEnv`, eleven frozen predicate-scope variables, **zero extension libraries** — reproduced in a nested throwaway module pinned to the repo's `cel-go v0.31.0` (root `go.mod`/`go.sum` byte-unchanged; nothing added to the dependency graph, which judgment call (d) has not authorised). **What exceeds tier 1: (1) folds.** `sum`, `reduce`, `math.*` and `lists.*` are all `undeclared reference`; `size()` is the only aggregate in the surface, so a rule counting matched changes is expressible and a rule summing a numeric delta across them is not. **(2) Graph reasoning** — the iteration count of a CEL expression cannot be made data-dependent, so depth is syntactic and **unbounded** reachability has no spelling; a bounded `k`-hop form *is* writable and answers a fixed-depth question, not the rule (detailed below, with the refutations of two sharper claims this row previously made). **What is struck, with the CEL that does the job:** registry membership — `string(new) in facts.registry.topics.value` over a `cardinality: set` fact, already shipped green at `examples/packs/service-catalog/.assent/packs/catalog/rules/ownership.yaml:21`; keyed attribute lookup — either a purpose-built provider (`builtin/resource-owner`, exercised in both polarities by `examples/archetypes/referenced-resource-ownership/`) or `facts.

..value[key].field`, which compiles and is lint-clean because `internal/lint/facts_ref.go`'s D-051 shape check permits arbitrary navigation past `.value` and only forbids indexing `facts` itself; set difference — `oldEntry.acls.filter(a, !(a in entry.acls)).size() == 0`; named intermediates — no `cel.bind`, but re-deriving the sub-expression inside each leaf is semantically identical and compiles. **The sharpest finding is a distinction, not a rule:** same-changeset **cross-file** reasoning fails for **input availability**, not expressiveness — the evaluation unit is one file (`change.ChangeSet` is documented "for one file", `internal/change/diff.go:129`; `assent run` strips one `--subject file:`, `cmd/assent/run.go:266`, and diffs it alone, `:293`) and **REQ-E11-S05-01 pins the Rego module to the identical `EvaluationInput`** with the tier fenced to "declared data, no I/O". **A Rego module therefore fails that rule identically, so it is struck from E11's justification too** — the fix is an input decision, which E11's non-goals fence, not a backend decision. Corroborating: the one committed illustration of the escape hatch, `examples/policies/rego/bounded_change.rego`, is **entirely tier-1 expressible** — both `violations` rules are per-change predicates and `examples/policies/declarative/bounded-change.yaml` is the same rule already in the envelope. **The strongest single piece of evidence, and the one that sizes the epic, is the graph shape.** On the `assent run` path document-mode `walkNode` emits a Change **only where two scalars differ** — a sequence on either side makes the whole ChangeSet **opaque → REVIEW** before any rule runs (`internal/change/diff.go`) — and collection-mode `DiffEntries` is reached only from `internal/adoptertest`, so `old`/`new`/`entry`/`oldEntry` and every `changes[i].old`/`.new` bind **scalars**. That does **not** starve a graph rule, because a flat `set` fact still carries structure: `edges: {type: string, cardinality: set}` returning `["orders|billing","billing|ledger"]` is a **fully declarable, in-contract adjacency inside `EvaluationInput` today** — the declaration is legal (`schemas/provider/v1alpha1/response.schema.json`), `fact.value` carries no JSON-Schema type constraint and `ResolveFactsChecked` cross-checks the *declaration* not the value (`internal/provider/resolve.go`), outputs are operator-authored (`internal/provider/config.go`), the `http` transport is live on the plain run path with **no `--checkout`** (`cmd/assent/provider_host.go` `providerCallFor`), and a set fact binds as a CEL list. Tier-1 CEL nonetheless cannot answer the actual question over it: **CEL has no recursion, fixpoint, fold or user-defined function, so unbounded reachability has no spelling** (`transitiveClosure` → `undeclared reference`; the four comprehension macros iterate one level and cannot call themselves). **Stated precisely, because two drafts of this record overreached and both were caught by independent review:** a *bounded* `k`-hop check **is** expressible and does **not** need the string decomposition CEL lacks — over a finite in-input candidate set (a `nodes` set fact, the same construction as `edges`), decode is replaceable by **encode-and-compare**: `nodes.value.exists(m, nodes.value.exists(n, (string(new)+"|"+m) in edges.value && (m+"|"+n) in edges.value && (n+"|"+string(new)) in edges.value))` compiles **and evaluates** under the real `cel.CostLimit(1_000_000)` to `true/true/true/false` over the fixture above, and `nodes.value.filter(m, (string(new)+"|"+m) in edges.value)` recovers an edge's far end as `[billing]`. Both primitives (`+` on strings, `in`) were already in this record's own function census, so the claim that decoding was a second independent barrier was internally inconsistent as well as false. **The real ceiling is `k`, and a third draft got its cost wrong too** — it claimed `O(|N|^(k-1)·|E|)` "exhausts the cost budget on any real graph". Wrong complexity class and wrong conclusion, because the census had omitted the surface's only value binder, `[expr].all(v, …)`: binding each BFS frontier once per level makes cost additive across levels, and measured under the real `cel.CostLimit(1_000_000)` a ring `|N|=50, deg 5` costs 89,551 at `k=10`, 235,297 at `k=20` and 686,317 at `k=50` — roughly linear in `k`, and at `k=50 ≥ |N|` CEL is **not approximating at all, it decides reachability exactly**, in 69% of budget. The practical `k` collapses around `|N|≈200` (`k=10` at 46% of budget, `k=20` exceeds). Recorded because a reader sizing this epic is entitled to ask "would CEL suffice for *our* graph?" and the previous sentence foreclosed that question with an assertion measurement refutes; it is **not** offered as a second reason. **What carries the verdict is one property, now measured rather than recalled: the iteration count of a tier-1 CEL expression cannot be made data-dependent.** `reduce`, `transformList`, `transformMap`, two-var `all(i,x,…)`, `range`/`lists.range` and `cel.bind` are all `undeclared reference`; `for` is a `reserved identifier`; there is no fold, self-reference or generator; so depth is a **syntactic** property, hard-capped by cel-go's parser recursion limit of 250 (`expression recursion limit exceeded: 250` at depth 260, depth 200 still compiles). That a fixed `k` really is an approximation when the data outruns it is measured too: on a 4-cycle the `k=3` form evaluates `false` and the `k=4` form `true`. **Rego answers the unbounded question with `graph.reachable` — pure and deterministic — and that single gap is the whole justification.** **An input that is in contract and available today, over which CEL can only approximate and Rego decides, is exactly the per-rule evidence D-017's gate demanded — so E11 has TWO unconditional justifications (folds and graphs), neither waiting on any open question.** Deliverability caveat, stated because this row makes the same distinction for sub-shape B1: **no provider in the corpus ships an encoded adjacency today** — that one *can* follows from the provider contract, the same inference used to strike B1, not from a shipped example. Options considered: **(a)** record all four shapes as exceeding, the reading D-141's unlock invites (rejected — three are demonstrably expressible and an unfalsifiable ceiling claim is the defect this story exists to prevent); **(b)** strike set-difference **conditionally**, so that a narrowing answer to OQ-35 would return it to the ceiling (rejected on the second pass — both resolutions strike it: extending the entry binding makes CEL express it, narrowing makes it an input-availability failure that REQ-E11-S05-01 hands to Rego unchanged, so a conditional would have left a downstream story waiting on an answer that cannot change the verdict); **(c)** strike cross-manifest and set-difference **unconditionally**, strike half of multi-pass, keep folds and in-input graphs **both unconditionally** **(chosen)**. **Two rejected drafts are recorded because the same failure produced both, with the sign flipped, and only independent review caught either.** Draft 1 made the graph shape *contingent* on OQ-35/OQ-36 on the premise that "an adjacency needs a mapping-valued fact" — it does not; a set of encoded strings carries one inside the frozen declaration — which came from conflating a *provider-supplied catalog* (sub-shapes B1/B2, struck here as working and shipped) with **B3, which is specifically same-changeset cross-file *diffs***. It would have advised the operator to defer a 14-story epic on a premise that does not hold. Draft 2 replaced that with a second "independent reason" — that CEL cannot decode an edge, killing even a bounded two-hop check — **refuted by execution** (the encode-and-compare leaf above). Draft 3 replaced *that* with the exponential-cost claim above — **refuted by measurement**. The common cause across all three is one habit: **reaching for a second independent reason when one sufficient reason was already in hand**, and then applying an **asymmetric evidentiary standard** to protect it — accepting awkward-but-working spellings when they *struck* a shape (A2's re-derivation, B2's dynamic index) and rejecting them when they would have *narrowed* one this record wanted to keep. The verdict was right in all four drafts; the supporting argument was wrong in three. It now rests on one measured property and no supporting argument at all, which is the form it should have taken first. The correction to A2 runs the same way: the value binder `[expr].all(v, …)` removes the evaluation-cost half of A2's residual, so **A2 is struck more firmly than the first draft struck it**. Binds later stories: **S05** must not be widened to carry cross-manifest data; **S07**'s violation shape must support a fold result and a path/cycle witness, not a cross-manifest reference; **S12** must correct ADR-0002's `rego` bullet, which calls the tier an "escape hatch for **cross-entry checks**" — inaccurate for the shipped input contract; **S11** must label the unquarantined example a shape illustration, never evidence of need. **Binds E11-S04, whose denylist is not yet written: `graph.reachable` MUST be allowed**, with `split` alongside it — both pure and deterministic. `graph.reachable` is the one that carries the justification (it closes the graph at any depth); `split` is a convenience for rebuilding the adjacency. A capability set drafted from "deny anything unfamiliar" would strike out the epic's own strongest justification. Recorded in the S04 section of the epic spec, not only S01's. **That floor is held by REVIEW, not by a gate, and this row says so rather than inventing an enforcement path:** REQ-E11-S04-02's committed golden detects a *change* to the allowed set (so the sandbox cannot silently widen) and cannot detect an *omission* — a golden written without `graph.reachable` stays green forever. It says nothing about judgment call (d), since *which* builtins are callable is orthogonal to *where* the evaluator lives. Two residuals raised, neither decided, **neither gating any verdict here**, and neither the escalated rule-7 (d1)/(d2) question: **OQ-35** (the `entry`/`oldEntry` binding asymmetry — a silent `assent test` / `assent run` divergence; set-difference is struck either way and the graph shape needs no entry tree) and **OQ-36** (the frozen provider declaration has no object/map type, yet the authoring surface and `builtin/repo-file` together permit a mapping-valued fact). Also flagged, not edited (out of lane): `REQ-DEM-S05-04` calls the provider-visible tree the "merged-result checkout"; the code reads `/head`, documented at `cmd/assent/checkout.go:44` as "the MERGE-REQUEST HEAD". This lane writes no Go, adds no dependency and touches no schema. Revert: delete `docs/planning/rego-tier-ceiling.md` and the D-156 narrowing text from the E11 spec — which restores an epic justified by four shapes, three of which this record shows are not real. | | D-158 | 2026-08-23 | **CI-TOOLCHAIN — `verify` was red on every PR from a golangci-lint/Go skew; the remedy is to bump `GOLANGCI_LINT_VERSION` v2.12.2 → v2.13.1 and KEEP `go-version: stable`.** Symptom: PR #85, a six-file Markdown diff with **zero Go bytes**, failed `verify` with `/opt/hostedtoolcache/go/1.27.0/x64/src/crypto/internal/randutil/randutil.go:11:2: could not import math/rand/v2 (… method must have no type parameters) (typecheck)` — the failing path is inside the **Go toolchain's own source tree**, so no author change can fix it and re-running cannot clear it. `Analyze (go)`, `Analyze (actions)` and `CodeQL` all passed on the same run: the tree compiles clean under Go 1.27, only the linter chokes. **Mechanism**: golangci-lint typechecks the standard library with the `go/types` it was **compiled with**, not the `go` on `PATH`. GitHub's `stable` rolled 1.26 → 1.27.0 between this repo's last green `main` run (2026-08-19) and 2026-08-23; the v2.12.2 release binary is built with go1.26.x and cannot read the 1.27 stdlib. **Reproduced locally, not reasoned** (Go 1.27.0 SDK on `PATH`, `GOTOOLCHAIN=local`, whole tree): v2.12.2 → **panic** in `pkg/goanalysis/runner_loadingpackage.go:335` inside `go/types.(*Checker).Files`, exit 2; official v2.13.1 asset (`built with go1.27.0`) → **0 issues**, exit 0; `golangci-lint config verify` → exit 0, so the v2 config schema in `.golangci.yml` needs no migration; v2.13.1 also → **0 issues** against local Go 1.26.6, so the bump is safe for contributors who have not moved; and `go install …@v2.13.1` under Go 1.27.0 → 0 issues, which is the **`release-exitgate`** path (that job builds the binary rather than using the action, and `if: github.event_name != 'pull_request'` / RELSE-08 means no PR ever exercises it). **Diagnosis heuristic worth keeping**: golangci-lint's `go.mod` carries the comment *"the minimum Go version must always be latest-1"*, so its `go` directive is a machine-readable "supports Go 1.N+1" signal — v2.12.2 says `go 1.25.0` (supports ≤1.26), v2.13.1 says `go 1.26.0` (supports ≤1.27), and upstream commit `42a0530` in v2.13.0 is literally "go1.27 support". **Options considered.** (A) *bump the linter* — CHOSEN: treats the root cause, is a **one-line** diff because the version is single-sourced at workflow scope (D-128), fixes BOTH exposed sites (the `golangci-lint-action` in `verify` and the `go install` in `release-exitgate`) at once, and the risk it carried — new findings from a newer linter blocking every merge, since `golangci-lint` runs inside `task lint` inside `task check` — was **measured at zero** on the whole tree under both Go versions. (B) *pin `go-version: 1.26.x`* — REJECTED as the primary: it needs two pins (`verify.yaml:56` and `:171`), leaves the class of bug live, undercuts the stated reason `stable` is there (`# govulncheck needs it`, with `setup-go` exporting `GOTOOLCHAIN=local` so a pinned toolchain can fail to `go run` a tool whose module requires a newer Go — unverified, and moot under (A)), and trades a loud recurrence for **silent indefinite drift onto an unsupported Go** in a repo whose posture is govulncheck + cosign + SLSA + Scorecard. (C) *both* — REJECTED as gold-plating: (A) alone is measured green, and a second simultaneous remedy would make a still-red PR ambiguous. **Per-file sweep of `go-version: stable`, stated rather than silently skipped:** `verify.yaml:56` and `:171` were the only exposed sites and are fixed by the env bump without touching either line; `schemas.yml:57` (runs `go test` + ajv, no linter), `vulncheck.yaml:30` (govulncheck only — `stable` is actively *desirable* there) and `codeql.yaml:45` (CodeQL, which passed on 1.27.0) carry no golangci-lint and are NOT exposed; `release.yaml` uses `go-version-file: go.mod` and is unaffected. `hack/lint/workflow_pins_test.sh` asserts `TASK_VERSION`, action SHA pins and step wiring but **not** `go-version` or `GOLANGCI_LINT_VERSION`; it passes on this change. **Revert is (B), not bare v2.12.2** — reverting the env line alone restores a known-red state: revert = `GOLANGCI_LINT_VERSION` back to `v2.12.2` **and** pin `verify.yaml:56` + `:171` to `go-version: 1.26.x`. **Residual risk, stated plainly:** when `stable` rolls to Go 1.28, v2.13.1 breaks identically. The repo finds out because `verify` reds on **every** PR including zero-Go diffs — loud and immediate, with the signature recorded in `verify.yaml`'s env comment and the fix being one env line. Nothing detects it *earlier*: dependabot's `github-actions` ecosystem updates `uses:` refs, not `env:` literals (backlog `CI-TOOLCHAIN-F01`). Accepted on purpose over (B)'s failure mode. Note also the pre-existing local/CI linter skew — `Taskfile.yml`'s `lint` task is bare `golangci-lint run ./...` against whatever binary a contributor has installed, so this pin has never governed local `task check`; deliberately not changed here (that file was owned by a concurrent lane). | | D-159 | 2026-08-23 | **ORPHAN — `release-verify-test` was a gate invoked by nothing (D-124 again), and it is wired into `task check` in its three OFFLINE modes, not its default `all`.** Finding: `Taskfile.yml` defined `release-verify-test` — the **only** test of `hack/release/verify-artifacts.sh` — and no caller existed anywhere: not `check:`, not `CHECK_STAGES` in `hack/audit/exitgate_test.sh`, not `.github/workflows/**`, not the push-only `release-exitgate`. That script is not incidental: **`SECURITY.md:61` publishes it as the procedure release consumers run** to check artifact checksums, the stamped `assent version` and cosign signatures, and D-153/AUD2-F01 had just proved that published verification instructions rot silently. Measured before fixing, as the lane required: the gate was **green**, so this is a wiring defect only — nothing was being papered over. **Why not the `all` default.** `verify_test.sh` with no argument adds `test_snapshot_pass`, which shells out to `task release-snapshot`: `go install github.com/goreleaser/goreleaser/v2@…` on any machine without it (**network**, in a gate that runs before every commit), a `before: hooks: go mod tidy` that **rewrites `go.mod`/`go.sum` in the middle of `task check`**, `--clean` on the developer's `dist/`, and a five-target cross-compile (10s here with warm caches and goreleaser already installed; minutes cold). A flaky or network-bound stage is worse than a missing one, so `check:` runs `negative`, `cosign-skip-when-absent` and `readme` — REQ-E9-S12-02/03/04, all offline, together well under a second. **Consequence, stated precisely: REQ-E9-S12-01 (the real snapshot→verify round trip) is not gated per-commit in `task check`; it runs in push-only CI via `hack/release/exitgate_test.sh:33-34` (the `release-exitgate` job, `if: github.event_name != 'pull_request'`) — automated but not PR-visible, i.e. the RELSE-08 blind spot.** Those two lines are literally `task release-snapshot` then `task release-verify`, which is the `Verify:` string the spec gives the requirement (`openspec/specs/p5-e9-distribution/spec.md:441-442`), so nothing here needs a new gate built — an earlier draft of this row claimed the requirement was covered by no automation at all, which was false, and acting on it would have meant a future lane duplicating `exitgate_test.sh:33-34`. What this lane declines to do is move that L1 round trip into a per-commit gate: it cannot be, for the network/`go mod tidy`/`--clean` reasons above. Narrowing the RELSE-08 exposure for this requirement is a separate question from D-159. **Pinning.** `CHECK_STAGES` goes 20 → 21 in the same commit as the `check:` line (the AUD-S18/RELSE-08 lockstep), and `STAGE_BODY_PINS` pins the body **per mode** rather than by the bare script path — a single `bash hack/release/verify_test.sh` pin would stay green if two modes were dropped *and* if the stage were reverted to the unrunnable-in-check default. Three mutation controls prove it: deleting the `check:` line reds `check_check_wiring` by stage name, gutting one of the three modes reds `check_stage_bodies` while the other two still run, and the same deletion applied to the real tree reds the real gate at rc=1. **Also fixed, minimally, because wiring made it matter:** `verify_test.sh` wrote its captured stdout/stderr to fixed `/tmp/verify-{tamper,nosig}.{out,err}` and then **grepped** them; harmless while nothing ran it, but this repo runs several lane worktrees whose `task check` invocations overlap, and a concurrent run truncating `/tmp/verify-nosig.err` at open would fail the other run's `skip.*cosign` grep spuriously. Scratch files now live in each run's own `mktemp -d` (invisible to `verify-artifacts.sh`, which globs only `*.tar.gz`/`*.zip`) and are removed by the existing `RETURN` trap. | +| D-160 | 2026-08-23 | **UNIV-COSIGN — the cosign signer-pin gate asserted an EXISTENTIAL property where the guarantee it publishes is UNIVERSAL, so it certified nothing about a file's second `cosign verify-blob`; `hack/release/install_cosign_pin_test.sh` now grades EVERY invocation in ALL THREE published files, statically and at runtime.** Substance first, and measured before anything was written: a scratch copy of each graded file with a **second, unpinned** `cosign verify-blob` appended to its real invocation ran the gate to **exit 0** — `hack/install.sh` rc=0, `SECURITY.md` rc=0, `hack/release/verify-artifacts.sh` rc=0, the last of these being the shape a reviewer had already demonstrated on an earlier lane. **Every individual assertion in that gate was sound.** `has_flag` grepped the whole folded extraction, so a pinned sibling satisfied it; `one_value`'s `sort -u` collapsed two agreeing values to one, so the D-153 drift comparison saw a consistent file; section 0 **printed** the extracted invocation count and asserted nothing about it; and 4b/5d's stub-log checks were positive-only greps, i.e. the same existential shape at runtime, where a second unpinned call leaves the pinned call's log line intact. The conjunction of sound existential assertions is still an existential assertion. **This is the AUD2-S05 quorum defect one layer out: not a wrong assertion, a wrong quantifier**, and it predates both AUD2-S03 and AUD2-F01. **`SECURITY.md` was worse than the other two** — it fed only the drift comparison and had **no invocation-level grading at all**, so an unpinned recipe published to adopters was invisible to the gate that exists to police the recipe. **Property chosen: "every `cosign verify-blob` invocation in every graded file carries `--certificate-oidc-issuer`, `--certificate-identity-regexp` and `--bundle`, EACH WITH SECURITY.md's published value".** The value half is not decoration: `--certificate-identity-regexp ''` carries the flag and matches every Fulcio identity ever issued, and `one_value`'s `sort -u` does not catch it either, because an empty capture is not a line and the file still reports exactly one distinct value — a presence-only universal check would be the same defect one level down, so each invocation's own extracted value is compared against the published pair (reported `WRONG-VALUE[...]`, distinct from `UNPINNED[...]`). Options considered: **(a)** the remedy recorded when the finding was filed — assert the extracted invocation count is **exactly 1** per file (**rejected, and it is not a preference but a fact: it is FALSE on this tree.** `SECURITY.md` legitimately publishes **two** — one over the archive, one over `checksums.txt`, which is what covers the SBOMs listed inside it — so that assertion reds `main` on the day it lands, and the natural repair is to weaken it again); **(b)** universal quantification over invocations **(chosen)** — strictly stronger than (a) where (a) is true, and it keeps holding when a file legitimately grows a third correctly-pinned call. **Enforcement, per D-128, is one predicate**: `pin_violations ` prints one line per problem and nothing when the file is clean, so callers grade its OUTPUT and the identical function is asserted empty against the tree and non-empty against a mutant with no `set -e` games; `assert_all_pinned` is the thin failing wrapper; `log_unpinned_lines` is its runtime twin over the stub-cosign argv log. **Classification is fail-CLOSED, which is the part that carries the guarantee.** The candidate extractor is deliberately left un-narrowed (every non-comment line mentioning `cosign verify-blob`, continuations folded), because anything the *denominator* drops is a hole. A candidate is an invocation when the folded text begins with `cosign verify-blob`; the ONE waved-through non-invocation shape is a markdown inline-code mention (`` `cosign verify-blob` ``, which is how `SECURITY.md`'s capability table names it); **anything else — `foo && cosign verify-blob …`, a here-doc line, an un-backticked prose sentence — is reported UNCLASSIFIABLE rather than skipped**, because "this gate cannot tell whether that call is pinned" must never read as "that call is fine". Accepted cost, stated rather than discovered later: a *correctly pinned* invocation written off command position also reds. That is the intended direction of error for a security gate over three files carrying four invocations in one canonical style, and the message names the fix. **Anti-vacuity, because a lane whose entire deliverable is "make a gate stricter" is maximally exposed** (this repo's #1 review finding is an assertion that cannot fail — D-124, AUD-S18): section 2b runs **eight** mutants against **each** of the three files and 2c runs a ninth, and they were chosen for **branch** coverage of the new predicate rather than for variety of shape — (a) a second **unpinned** invocation must red, name the file, quote the offending command, and produce **exactly two** violations so the pinned siblings are provably not flagged; (b) a second **correctly pinned** invocation must stay green **and** must raise the extractor's invocation count by one, without which (b)'s green could mean "the extractor never saw it"; (c) an occurrence off command position, appended **fully pinned on purpose** so the only thing that can redden it is the classifier itself; (d) every invocation deleted → `NO-CANDIDATES`; (e) the continuation fold broken → `FOLD-BROKEN`, asserted **not** to also report `UNPINNED`, because conflating "the extractor truncated this" with "the pin is missing" sends the next maintainer to the wrong file; (f) every invocation displaced off command position → `NO-INVOCATIONS`; (g) a second invocation carrying both flags with an **empty** identity regexp → `WRONG-VALUE`, the hostile shape a presence-only check waves through; (h) a second invocation carrying both flags with a **foreign OIDC issuer** → `WRONG-VALUE` on the issuer half; and 2c strips the backticks from `SECURITY.md`'s prose mention and requires the same row to fail closed, proving the exemption keys on the backticks and is not a blanket bypass. The runtime twin has its own vacuity control (an unpinned line appended to a copy of the stub log must be seen). **One real defect was caught by this section during the lane and is recorded because it is a trap for the next author**: `log_unpinned_lines` was first written with `awk -v id="identity_re=${sec_identity}"`, and **awk processes escape sequences in a `-v` assignment**, so the pin's `github\.com` arrived as `github.com` and matched nothing; the values now reach awk through `ENVIRON`. **Stated limit, same posture as D-154's**: the denominator is the literal string `cosign verify-blob`, so an invocation spelled through a variable (`"$COSIGN" verify-blob …`), built by `eval`, or assembled from fragments is invisible to this gate. Widening the trigger to bare `verify-blob` was considered and **rejected** — it buys one hypothetical no file uses, and turns any future `SECURITY.md` sentence saying "verify-blob" outside backticks into a red gate, whose repair would be to loosen the classifier. **Nothing outside the gate changed**: `hack/install.sh`, `SECURITY.md` and `hack/release/verify-artifacts.sh` are byte-unchanged, and all four of their invocations were already pinned — this row closes a hole in the *checker*, not in the checked. The stage `release-install-cosign-pin-test` was already wired into `task check` and pinned in `hack/audit/exitgate_test.sh`'s `CHECK_STAGES`, so no wiring changed either. Revert: restore `has_flag`, drop the per-invocation value comparison, and restore the two positive-only stub-log greps — which returns the gate to certifying that *some* cosign call in each file is pinned, a property that is compatible with an unpinned one sitting beside it. | diff --git a/hack/release/install_cosign_pin_test.sh b/hack/release/install_cosign_pin_test.sh index 7eb61a3..c4c9e0e 100755 --- a/hack/release/install_cosign_pin_test.sh +++ b/hack/release/install_cosign_pin_test.sh @@ -44,6 +44,32 @@ # decoded from the REAL published bundles are committed here as test data and # every one of them must verify. # +# UNIV-COSIGN / D-160 — EXISTENTIAL WHERE IT HAD TO BE UNIVERSAL. Until D-160 +# every flag assertion here asked "does SOME cosign invocation in this file carry +# the pin?". Each one was individually sound and the conjunction still certified +# nothing: a reviewer added a SECOND, UNPINNED `cosign verify-blob` to +# hack/release/verify-artifacts.sh and this gate exited 0. `has_flag` grepped the +# whole folded extraction so a pinned sibling satisfied it; `one_value`'s `sort -u` +# collapsed the agreeing values so the drift gate saw one; section 0 PRINTED the +# invocation count and asserted nothing about it; and 4b/5d's stub-log checks were +# positive-only greps, the same shape at runtime. Measured before the fix on +# scratch copies of all three graded files, each with a second unpinned call: +# rc=0, rc=0, rc=0. SECURITY.md was worse than the other two — it had no +# invocation-level grading at all, only the drift comparison. +# +# The property is now UNIVERSAL — EVERY `cosign verify-blob` invocation in EVERY +# graded file carries both pins, EACH WITH SECURITY.md's published value — +# enforced by pin_violations (sections 1, 2, 2b, 2c) and by log_unpinned_lines at +# runtime (4b, 5d). The value half is not decoration: `--certificate-identity- +# regexp ''` carries the flag and matches every Fulcio identity ever issued, and +# `one_value`'s `sort -u` misses it too because an empty capture is not a line. +# A presence-only universal check would be the same defect one level down. +# "Exactly one invocation per +# file", the cheaper remedy, was rejected as FALSE on this tree: SECURITY.md +# legitimately publishes two, one over the archive and one over checksums.txt. +# This is the AUD2-S05 quorum bug one layer out: not a wrong assertion, a wrong +# quantifier. +# # ANTI-VACUITY DISCIPLINE (this repo has a documented history of gates that # cannot fail — D-124, AUD-S18). Every assertion here is a FUNCTION over a file # or a fixture, run twice: once against the real tree (must be GREEN) and once @@ -81,10 +107,20 @@ fail() { # --------------------------------------------------------------- helpers -- -# cosign_invocation — the `cosign verify-blob …` command with its -# backslash continuations folded onto one line. Comment lines are skipped so a -# flag mentioned only in prose can never satisfy an assertion. -cosign_invocation() { +# cosign_candidates — EVERY `cosign verify-blob …` occurrence in the file, +# one per output line, with backslash continuations folded onto that line. +# Comment lines are skipped so a flag mentioned only in prose can never satisfy an +# assertion. +# +# This is the DENOMINATOR of the universal check below (UNIV-COSIGN, D-160), so it +# is deliberately left un-narrowed: anything it drops is a hole. Occurrences that +# are not really invocations (SECURITY.md's table says "`cosign verify-blob` with +# bundle") are classified out — and ACCOUNTED FOR — by pin_violations, never +# filtered away here. +# +# It was already emitting one line per occurrence before D-160; what was missing +# was any caller that looked at more than the first one. +cosign_candidates() { awk ' /^[[:space:]]*#/ { next } !inv && /cosign verify-blob/ { inv = 1 } @@ -98,13 +134,21 @@ cosign_invocation() { ' "$1" } +# cosign_invocations — the candidates that are actual commands, i.e. those +# whose folded text BEGINS with `cosign verify-blob` (leading whitespace already +# stripped by the fold). +cosign_invocations() { + cosign_candidates "$1" | grep '^cosign verify-blob' || true +} + # extract_issuer — every distinct --certificate-oidc-issuer value. extract_issuer() { sed -nE "s/.*--certificate-oidc-issuer[[:space:]]+['\"]?([^'\"[:space:]]+)['\"]?.*/\1/p" "$1" | sort -u } # extract_identity — every distinct --certificate-identity-regexp value. -# The value is single-quoted in both files (a shell regexp must be); an unquoted +# The value is single-quoted in all three graded files (a shell regexp must be); +# an unquoted # value extracts as nothing and trips the positive controls rather than passing. extract_identity() { sed -nE "s/.*--certificate-identity-regexp[[:space:]]+'([^']*)'.*/\1/p" "$1" | sort -u @@ -126,9 +170,125 @@ one_value() { printf '%s' "$out" } -# has_flag — the flag appears inside the cosign invocation. -has_flag() { - cosign_invocation "$1" | grep -qF -- "$2" +# pin_violations — UNIV-COSIGN (D-160). Prints one line per problem, and +# NOTHING AT ALL when every `cosign verify-blob` invocation in carries the +# D-153 signer pin. Callers grade the OUTPUT rather than an exit status, so the +# identical function is asserted empty against the real tree and non-empty against +# a mutant, with no `set -e` games in between. +# +# WHY THIS REPLACED has_flag. Until D-160 the flag assertions were `has_flag`, +# which grepped the WHOLE folded extraction: "SOME invocation is pinned". Every +# individual assertion was sound and the conjunction still certified nothing — +# a reviewer added a second, UNPINNED `cosign verify-blob` to +# hack/release/verify-artifacts.sh and this gate exited 0. `one_value`'s `sort -u` +# collapsed the agreeing values, the drift gate saw one value per file, and §0 +# printed the invocation count without ever asserting anything about it. The +# property needed is UNIVERSAL — *every* invocation is pinned — and the same hole +# was open on all three graded files, not just the one that was probed. +# +# WHY NOT "EXACTLY ONE INVOCATION PER FILE", the cheaper remedy: SECURITY.md +# legitimately publishes TWO — one over the archive, one over checksums.txt (which +# is what covers the SBOMs listed inside it) — so that assertion is false on the +# tree as it stands. Universal is also strictly stronger: it keeps holding when a +# file grows a third, correctly pinned call. +# +# FAIL-CLOSED CLASSIFICATION. A candidate that is not at command position is only +# waved through when it is a markdown inline-code mention (backticked). Anything +# else — `foo && cosign verify-blob …`, a here-doc line, an un-backticked prose +# sentence — is reported UNCLASSIFIABLE rather than skipped, because "this gate +# cannot tell whether that call is pinned" must not read as "that call is fine". +# +# STATED LIMIT, deliberately not closed here (same posture as D-154): the +# denominator is the literal string `cosign verify-blob`. An invocation spelled +# through a variable (`"$COSIGN" verify-blob …`), built by `eval`, or assembled +# from fragments is invisible to this gate. Widening the trigger to bare +# `verify-blob` was considered and rejected — it would turn any future prose +# sentence in SECURITY.md that says "verify-blob" outside backticks into a red +# gate, and the next lane's remedy for that would be to loosen the classifier. +pin_violations() { + local file="$1" rel cand line flag n_cand n_inv=0 inv_iss inv_id + rel="${file#"$ROOT"/}" + # The comparison is against SECURITY.md's published pair, so this must not run + # before section 0 extracted it — otherwise every value check below compares + # against the empty string and passes. + [[ -n "${sec_issuer:-}" && -n "${sec_identity:-}" ]] \ + || fail "pin_violations was called before SECURITY.md's published issuer/identity pair was extracted — every value comparison in it would be vacuous" + cand="$(cosign_candidates "$file")" + n_cand="$(printf '%s' "$cand" | grep -c . || true)" + if [[ "$n_cand" -eq 0 ]]; then + printf 'NO-CANDIDATES: %s carries no `cosign verify-blob` occurrence at all — the call is gone, or the extraction pattern broke; either way every pin assertion over this file would be vacuous\n' "$rel" + return 0 + fi + while IFS= read -r line; do + [[ -n "$line" ]] || continue + if [[ "$line" != 'cosign verify-blob'* ]]; then + # Not at command position. The ONE accepted non-invocation shape is a + # markdown inline-code mention, e.g. SECURITY.md's capability table. + if [[ "$line" == *'`cosign verify-blob`'* ]]; then + continue + fi + printf 'UNCLASSIFIABLE: %s has a `cosign verify-blob` occurrence that is neither at command position nor a backticked prose mention, so this gate cannot decide whether it is pinned — failing closed: %s\n' "$rel" "$line" + continue + fi + n_inv=$((n_inv + 1)) + if [[ "$line" != *--bundle* ]]; then + # --bundle is present in every real invocation across all three files, so + # its absence means the backslash-continuation fold did NOT join this + # command's flag lines. Reported separately from UNPINNED because the + # remedy is different: fix the extractor, do not go looking for a missing + # pin in a file that has one. + printf 'FOLD-BROKEN: %s has a `cosign verify-blob` command that folded WITHOUT --bundle — the continuation fold is truncating this invocation, so its pin verdict below cannot be trusted: %s\n' "$rel" "$line" + continue + fi + for flag in --certificate-oidc-issuer --certificate-identity-regexp; do + [[ "$line" == *"$flag"* ]] \ + || printf 'UNPINNED[%s]: %s has a `cosign verify-blob` invocation without %s — keyless verification there accepts a signer this project never authorised: %s\n' "$flag" "$rel" "$flag" "$line" + done + # PRESENCE IS NOT A PIN. `--certificate-identity-regexp ''` carries the flag + # and matches every Fulcio identity ever issued, so a check that stops at "the + # flag is there" is the same defect D-160 closes, one level down. Each + # invocation's OWN value is therefore compared against SECURITY.md's published + # pair — which also means a second invocation can no longer drift from the + # first behind `one_value`'s `sort -u`. + inv_iss="$(printf '%s\n' "$line" | extract_issuer /dev/stdin)" + inv_id="$(printf '%s\n' "$line" | extract_identity /dev/stdin)" + if [[ "$line" == *--certificate-oidc-issuer* && "$inv_iss" != "$sec_issuer" ]]; then + printf 'WRONG-VALUE[--certificate-oidc-issuer]: %s has a `cosign verify-blob` invocation pinning issuer=%s, but SECURITY.md publishes %s — the flag is present and the guarantee is not: %s\n' "$rel" "${inv_iss:-}" "$sec_issuer" "$line" + fi + if [[ "$line" == *--certificate-identity-regexp* && "$inv_id" != "$sec_identity" ]]; then + printf 'WRONG-VALUE[--certificate-identity-regexp]: %s has a `cosign verify-blob` invocation pinning identity=%s, but SECURITY.md publishes %s — the flag is present and the guarantee is not (an empty regexp matches every Fulcio identity): %s\n' "$rel" "${inv_id:-}" "$sec_identity" "$line" + fi + done <<<"$cand" + [[ "$n_inv" -ge 1 ]] \ + || printf 'NO-INVOCATIONS: %s mentions `cosign verify-blob` but not once at command position — nothing was actually graded\n' "$rel" +} + +# assert_all_pinned

..value[key].field`, which compiles and is lint-clean because `internal/lint/facts_ref.go`'s D-051 shape check permits arbitrary navigation past `.value` and only forbids indexing `facts` itself; set difference — `oldEntry.acls.filter(a, !(a in entry.acls)).size() == 0`; named intermediates — no `cel.bind`, but re-deriving the sub-expression inside each leaf is semantically identical and compiles. **The sharpest finding is a distinction, not a rule:** same-changeset **cross-file** reasoning fails for **input availability**, not expressiveness — the evaluation unit is one file (`change.ChangeSet` is documented "for one file", `internal/change/diff.go:129`; `assent run` strips one `--subject file:`, `cmd/assent/run.go:266`, and diffs it alone, `:293`) and **REQ-E11-S05-01 pins the Rego module to the identical `EvaluationInput`** with the tier fenced to "declared data, no I/O". **A Rego module therefore fails that rule identically, so it is struck from E11's justification too** — the fix is an input decision, which E11's non-goals fence, not a backend decision. Corroborating: the one committed illustration of the escape hatch, `examples/policies/rego/bounded_change.rego`, is **entirely tier-1 expressible** — both `violations` rules are per-change predicates and `examples/policies/declarative/bounded-change.yaml` is the same rule already in the envelope. **The strongest single piece of evidence, and the one that sizes the epic, is the graph shape.** On the `assent run` path document-mode `walkNode` emits a Change **only where two scalars differ** — a sequence on either side makes the whole ChangeSet **opaque → REVIEW** before any rule runs (`internal/change/diff.go`) — and collection-mode `DiffEntries` is reached only from `internal/adoptertest`, so `old`/`new`/`entry`/`oldEntry` and every `changes[i].old`/`.new` bind **scalars**. That does **not** starve a graph rule, because a flat `set` fact still carries structure: `edges: {type: string, cardinality: set}` returning `["orders|billing","billing|ledger"]` is a **fully declarable, in-contract adjacency inside `EvaluationInput` today** — the declaration is legal (`schemas/provider/v1alpha1/response.schema.json`), `fact.value` carries no JSON-Schema type constraint and `ResolveFactsChecked` cross-checks the *declaration* not the value (`internal/provider/resolve.go`), outputs are operator-authored (`internal/provider/config.go`), the `http` transport is live on the plain run path with **no `--checkout`** (`cmd/assent/provider_host.go` `providerCallFor`), and a set fact binds as a CEL list. Tier-1 CEL nonetheless cannot answer the actual question over it: **CEL has no recursion, fixpoint, fold or user-defined function, so unbounded reachability has no spelling** (`transitiveClosure` → `undeclared reference`; the four comprehension macros iterate one level and cannot call themselves). **Stated precisely, because two drafts of this record overreached and both were caught by independent review:** a *bounded* `k`-hop check **is** expressible and does **not** need the string decomposition CEL lacks — over a finite in-input candidate set (a `nodes` set fact, the same construction as `edges`), decode is replaceable by **encode-and-compare**: `nodes.value.exists(m, nodes.value.exists(n, (string(new)+"|"+m) in edges.value && (m+"|"+n) in edges.value && (n+"|"+string(new)) in edges.value))` compiles **and evaluates** under the real `cel.CostLimit(1_000_000)` to `true/true/true/false` over the fixture above, and `nodes.value.filter(m, (string(new)+"|"+m) in edges.value)` recovers an edge's far end as `[billing]`. Both primitives (`+` on strings, `in`) were already in this record's own function census, so the claim that decoding was a second independent barrier was internally inconsistent as well as false. **The real ceiling is `k`, and a third draft got its cost wrong too** — it claimed `O(|N|^(k-1)·|E|)` "exhausts the cost budget on any real graph". Wrong complexity class and wrong conclusion, because the census had omitted the surface's only value binder, `[expr].all(v, …)`: binding each BFS frontier once per level makes cost additive across levels, and measured under the real `cel.CostLimit(1_000_000)` a ring `|N|=50, deg 5` costs 89,551 at `k=10`, 235,297 at `k=20` and 686,317 at `k=50` — roughly linear in `k`, and at `k=50 ≥ |N|` CEL is **not approximating at all, it decides reachability exactly**, in 69% of budget. The practical `k` collapses around `|N|≈200` (`k=10` at 46% of budget, `k=20` exceeds). Recorded because a reader sizing this epic is entitled to ask "would CEL suffice for *our* graph?" and the previous sentence foreclosed that question with an assertion measurement refutes; it is **not** offered as a second reason. **What carries the verdict is one property, now measured rather than recalled: the iteration count of a tier-1 CEL expression cannot be made data-dependent.** `reduce`, `transformList`, `transformMap`, two-var `all(i,x,…)`, `range`/`lists.range` and `cel.bind` are all `undeclared reference`; `for` is a `reserved identifier`; there is no fold, self-reference or generator; so depth is a **syntactic** property, hard-capped by cel-go's parser recursion limit of 250 (`expression recursion limit exceeded: 250` at depth 260, depth 200 still compiles). That a fixed `k` really is an approximation when the data outruns it is measured too: on a 4-cycle the `k=3` form evaluates `false` and the `k=4` form `true`. **Rego answers the unbounded question with `graph.reachable` — pure and deterministic — and that single gap is the whole justification.** **An input that is in contract and available today, over which CEL can only approximate and Rego decides, is exactly the per-rule evidence D-017's gate demanded — so E11 has TWO unconditional justifications (folds and graphs), neither waiting on any open question.** Deliverability caveat, stated because this row makes the same distinction for sub-shape B1: **no provider in the corpus ships an encoded adjacency today** — that one *can* follows from the provider contract, the same inference used to strike B1, not from a shipped example. Options considered: **(a)** record all four shapes as exceeding, the reading D-141's unlock invites (rejected — three are demonstrably expressible and an unfalsifiable ceiling claim is the defect this story exists to prevent); **(b)** strike set-difference **conditionally**, so that a narrowing answer to OQ-35 would return it to the ceiling (rejected on the second pass — both resolutions strike it: extending the entry binding makes CEL express it, narrowing makes it an input-availability failure that REQ-E11-S05-01 hands to Rego unchanged, so a conditional would have left a downstream story waiting on an answer that cannot change the verdict); **(c)** strike cross-manifest and set-difference **unconditionally**, strike half of multi-pass, keep folds and in-input graphs **both unconditionally** **(chosen)**. **Two rejected drafts are recorded because the same failure produced both, with the sign flipped, and only independent review caught either.** Draft 1 made the graph shape *contingent* on OQ-35/OQ-36 on the premise that "an adjacency needs a mapping-valued fact" — it does not; a set of encoded strings carries one inside the frozen declaration — which came from conflating a *provider-supplied catalog* (sub-shapes B1/B2, struck here as working and shipped) with **B3, which is specifically same-changeset cross-file *diffs***. It would have advised the operator to defer a 14-story epic on a premise that does not hold. Draft 2 replaced that with a second "independent reason" — that CEL cannot decode an edge, killing even a bounded two-hop check — **refuted by execution** (the encode-and-compare leaf above). Draft 3 replaced *that* with the exponential-cost claim above — **refuted by measurement**. The common cause across all three is one habit: **reaching for a second independent reason when one sufficient reason was already in hand**, and then applying an **asymmetric evidentiary standard** to protect it — accepting awkward-but-working spellings when they *struck* a shape (A2's re-derivation, B2's dynamic index) and rejecting them when they would have *narrowed* one this record wanted to keep. The verdict was right in all four drafts; the supporting argument was wrong in three. It now rests on one measured property and no supporting argument at all, which is the form it should have taken first. The correction to A2 runs the same way: the value binder `[expr].all(v, …)` removes the evaluation-cost half of A2's residual, so **A2 is struck more firmly than the first draft struck it**. Binds later stories: **S05** must not be widened to carry cross-manifest data; **S07**'s violation shape must support a fold result and a path/cycle witness, not a cross-manifest reference; **S12** must correct ADR-0002's `rego` bullet, which calls the tier an "escape hatch for **cross-entry checks**" — inaccurate for the shipped input contract; **S11** must label the unquarantined example a shape illustration, never evidence of need. **Binds E11-S04, whose denylist is not yet written: `graph.reachable` MUST be allowed**, with `split` alongside it — both pure and deterministic. `graph.reachable` is the one that carries the justification (it closes the graph at any depth); `split` is a convenience for rebuilding the adjacency. A capability set drafted from "deny anything unfamiliar" would strike out the epic's own strongest justification. Recorded in the S04 section of the epic spec, not only S01's. **That floor is held by REVIEW, not by a gate, and this row says so rather than inventing an enforcement path:** REQ-E11-S04-02's committed golden detects a *change* to the allowed set (so the sandbox cannot silently widen) and cannot detect an *omission* — a golden written without `graph.reachable` stays green forever. It says nothing about judgment call (d), since *which* builtins are callable is orthogonal to *where* the evaluator lives. Two residuals raised, neither decided, **neither gating any verdict here**, and neither the escalated rule-7 (d1)/(d2) question: **OQ-35** (the `entry`/`oldEntry` binding asymmetry — a silent `assent test` / `assent run` divergence; set-difference is struck either way and the graph shape needs no entry tree) and **OQ-36** (the frozen provider declaration has no object/map type, yet the authoring surface and `builtin/repo-file` together permit a mapping-valued fact). Also flagged, not edited (out of lane): `REQ-DEM-S05-04` calls the provider-visible tree the "merged-result checkout"; the code reads `/head`, documented at `cmd/assent/checkout.go:44` as "the MERGE-REQUEST HEAD". This lane writes no Go, adds no dependency and touches no schema. Revert: delete `docs/planning/rego-tier-ceiling.md` and the D-156 narrowing text from the E11 spec — which restores an epic justified by four shapes, three of which this record shows are not real. | | D-158 | 2026-08-23 | **CI-TOOLCHAIN — `verify` was red on every PR from a golangci-lint/Go skew; the remedy is to bump `GOLANGCI_LINT_VERSION` v2.12.2 → v2.13.1 and KEEP `go-version: stable`.** Symptom: PR #85, a six-file Markdown diff with **zero Go bytes**, failed `verify` with `/opt/hostedtoolcache/go/1.27.0/x64/src/crypto/internal/randutil/randutil.go:11:2: could not import math/rand/v2 (… method must have no type parameters) (typecheck)` — the failing path is inside the **Go toolchain's own source tree**, so no author change can fix it and re-running cannot clear it. `Analyze (go)`, `Analyze (actions)` and `CodeQL` all passed on the same run: the tree compiles clean under Go 1.27, only the linter chokes. **Mechanism**: golangci-lint typechecks the standard library with the `go/types` it was **compiled with**, not the `go` on `PATH`. GitHub's `stable` rolled 1.26 → 1.27.0 between this repo's last green `main` run (2026-08-19) and 2026-08-23; the v2.12.2 release binary is built with go1.26.x and cannot read the 1.27 stdlib. **Reproduced locally, not reasoned** (Go 1.27.0 SDK on `PATH`, `GOTOOLCHAIN=local`, whole tree): v2.12.2 → **panic** in `pkg/goanalysis/runner_loadingpackage.go:335` inside `go/types.(*Checker).Files`, exit 2; official v2.13.1 asset (`built with go1.27.0`) → **0 issues**, exit 0; `golangci-lint config verify` → exit 0, so the v2 config schema in `.golangci.yml` needs no migration; v2.13.1 also → **0 issues** against local Go 1.26.6, so the bump is safe for contributors who have not moved; and `go install …@v2.13.1` under Go 1.27.0 → 0 issues, which is the **`release-exitgate`** path (that job builds the binary rather than using the action, and `if: github.event_name != 'pull_request'` / RELSE-08 means no PR ever exercises it). **Diagnosis heuristic worth keeping**: golangci-lint's `go.mod` carries the comment *"the minimum Go version must always be latest-1"*, so its `go` directive is a machine-readable "supports Go 1.N+1" signal — v2.12.2 says `go 1.25.0` (supports ≤1.26), v2.13.1 says `go 1.26.0` (supports ≤1.27), and upstream commit `42a0530` in v2.13.0 is literally "go1.27 support". **Options considered.** (A) *bump the linter* — CHOSEN: treats the root cause, is a **one-line** diff because the version is single-sourced at workflow scope (D-128), fixes BOTH exposed sites (the `golangci-lint-action` in `verify` and the `go install` in `release-exitgate`) at once, and the risk it carried — new findings from a newer linter blocking every merge, since `golangci-lint` runs inside `task lint` inside `task check` — was **measured at zero** on the whole tree under both Go versions. (B) *pin `go-version: 1.26.x`* — REJECTED as the primary: it needs two pins (`verify.yaml:56` and `:171`), leaves the class of bug live, undercuts the stated reason `stable` is there (`# govulncheck needs it`, with `setup-go` exporting `GOTOOLCHAIN=local` so a pinned toolchain can fail to `go run` a tool whose module requires a newer Go — unverified, and moot under (A)), and trades a loud recurrence for **silent indefinite drift onto an unsupported Go** in a repo whose posture is govulncheck + cosign + SLSA + Scorecard. (C) *both* — REJECTED as gold-plating: (A) alone is measured green, and a second simultaneous remedy would make a still-red PR ambiguous. **Per-file sweep of `go-version: stable`, stated rather than silently skipped:** `verify.yaml:56` and `:171` were the only exposed sites and are fixed by the env bump without touching either line; `schemas.yml:57` (runs `go test` + ajv, no linter), `vulncheck.yaml:30` (govulncheck only — `stable` is actively *desirable* there) and `codeql.yaml:45` (CodeQL, which passed on 1.27.0) carry no golangci-lint and are NOT exposed; `release.yaml` uses `go-version-file: go.mod` and is unaffected. `hack/lint/workflow_pins_test.sh` asserts `TASK_VERSION`, action SHA pins and step wiring but **not** `go-version` or `GOLANGCI_LINT_VERSION`; it passes on this change. **Revert is (B), not bare v2.12.2** — reverting the env line alone restores a known-red state: revert = `GOLANGCI_LINT_VERSION` back to `v2.12.2` **and** pin `verify.yaml:56` + `:171` to `go-version: 1.26.x`. **Residual risk, stated plainly:** when `stable` rolls to Go 1.28, v2.13.1 breaks identically. The repo finds out because `verify` reds on **every** PR including zero-Go diffs — loud and immediate, with the signature recorded in `verify.yaml`'s env comment and the fix being one env line. Nothing detects it *earlier*: dependabot's `github-actions` ecosystem updates `uses:` refs, not `env:` literals (backlog `CI-TOOLCHAIN-F01`). Accepted on purpose over (B)'s failure mode. Note also the pre-existing local/CI linter skew — `Taskfile.yml`'s `lint` task is bare `golangci-lint run ./...` against whatever binary a contributor has installed, so this pin has never governed local `task check`; deliberately not changed here (that file was owned by a concurrent lane). | | D-159 | 2026-08-23 | **ORPHAN — `release-verify-test` was a gate invoked by nothing (D-124 again), and it is wired into `task check` in its three OFFLINE modes, not its default `all`.** Finding: `Taskfile.yml` defined `release-verify-test` — the **only** test of `hack/release/verify-artifacts.sh` — and no caller existed anywhere: not `check:`, not `CHECK_STAGES` in `hack/audit/exitgate_test.sh`, not `.github/workflows/**`, not the push-only `release-exitgate`. That script is not incidental: **`SECURITY.md:61` publishes it as the procedure release consumers run** to check artifact checksums, the stamped `assent version` and cosign signatures, and D-153/AUD2-F01 had just proved that published verification instructions rot silently. Measured before fixing, as the lane required: the gate was **green**, so this is a wiring defect only — nothing was being papered over. **Why not the `all` default.** `verify_test.sh` with no argument adds `test_snapshot_pass`, which shells out to `task release-snapshot`: `go install github.com/goreleaser/goreleaser/v2@…` on any machine without it (**network**, in a gate that runs before every commit), a `before: hooks: go mod tidy` that **rewrites `go.mod`/`go.sum` in the middle of `task check`**, `--clean` on the developer's `dist/`, and a five-target cross-compile (10s here with warm caches and goreleaser already installed; minutes cold). A flaky or network-bound stage is worse than a missing one, so `check:` runs `negative`, `cosign-skip-when-absent` and `readme` — REQ-E9-S12-02/03/04, all offline, together well under a second. **Consequence, stated precisely: REQ-E9-S12-01 (the real snapshot→verify round trip) is not gated per-commit in `task check`; it runs in push-only CI via `hack/release/exitgate_test.sh:33-34` (the `release-exitgate` job, `if: github.event_name != 'pull_request'`) — automated but not PR-visible, i.e. the RELSE-08 blind spot.** Those two lines are literally `task release-snapshot` then `task release-verify`, which is the `Verify:` string the spec gives the requirement (`openspec/specs/p5-e9-distribution/spec.md:441-442`), so nothing here needs a new gate built — an earlier draft of this row claimed the requirement was covered by no automation at all, which was false, and acting on it would have meant a future lane duplicating `exitgate_test.sh:33-34`. What this lane declines to do is move that L1 round trip into a per-commit gate: it cannot be, for the network/`go mod tidy`/`--clean` reasons above. Narrowing the RELSE-08 exposure for this requirement is a separate question from D-159. **Pinning.** `CHECK_STAGES` goes 20 → 21 in the same commit as the `check:` line (the AUD-S18/RELSE-08 lockstep), and `STAGE_BODY_PINS` pins the body **per mode** rather than by the bare script path — a single `bash hack/release/verify_test.sh` pin would stay green if two modes were dropped *and* if the stage were reverted to the unrunnable-in-check default. Three mutation controls prove it: deleting the `check:` line reds `check_check_wiring` by stage name, gutting one of the three modes reds `check_stage_bodies` while the other two still run, and the same deletion applied to the real tree reds the real gate at rc=1. **Also fixed, minimally, because wiring made it matter:** `verify_test.sh` wrote its captured stdout/stderr to fixed `/tmp/verify-{tamper,nosig}.{out,err}` and then **grepped** them; harmless while nothing ran it, but this repo runs several lane worktrees whose `task check` invocations overlap, and a concurrent run truncating `/tmp/verify-nosig.err` at open would fail the other run's `skip.*cosign` grep spuriously. Scratch files now live in each run's own `mktemp -d` (invisible to `verify-artifacts.sh`, which globs only `*.tar.gz`/`*.zip`) and are removed by the existing `RETURN` trap. | -| D-160 | 2026-08-23 | **UNIV-COSIGN — the cosign signer-pin gate asserted an EXISTENTIAL property where the guarantee it publishes is UNIVERSAL, so it certified nothing about a file's second `cosign verify-blob`; `hack/release/install_cosign_pin_test.sh` now grades EVERY invocation in ALL THREE published files, statically and at runtime.** Substance first, and measured before anything was written: a scratch copy of each graded file with a **second, unpinned** `cosign verify-blob` appended to its real invocation ran the gate to **exit 0** — `hack/install.sh` rc=0, `SECURITY.md` rc=0, `hack/release/verify-artifacts.sh` rc=0, the last of these being the shape a reviewer had already demonstrated on an earlier lane. **Every individual assertion in that gate was sound.** `has_flag` grepped the whole folded extraction, so a pinned sibling satisfied it; `one_value`'s `sort -u` collapsed two agreeing values to one, so the D-153 drift comparison saw a consistent file; section 0 **printed** the extracted invocation count and asserted nothing about it; and 4b/5d's stub-log checks were positive-only greps, i.e. the same existential shape at runtime, where a second unpinned call leaves the pinned call's log line intact. The conjunction of sound existential assertions is still an existential assertion. **This is the AUD2-S05 quorum defect one layer out: not a wrong assertion, a wrong quantifier**, and it predates both AUD2-S03 and AUD2-F01. **`SECURITY.md` was worse than the other two** — it fed only the drift comparison and had **no invocation-level grading at all**, so an unpinned recipe published to adopters was invisible to the gate that exists to police the recipe. **Property chosen: "every `cosign verify-blob` invocation in every graded file carries `--certificate-oidc-issuer`, `--certificate-identity-regexp` and `--bundle`, EACH WITH SECURITY.md's published value".** The value half is not decoration: `--certificate-identity-regexp ''` carries the flag and matches every Fulcio identity ever issued, and `one_value`'s `sort -u` does not catch it either, because an empty capture is not a line and the file still reports exactly one distinct value — a presence-only universal check would be the same defect one level down, so each invocation's own extracted value is compared against the published pair (reported `WRONG-VALUE[...]`, distinct from `UNPINNED[...]`). Options considered: **(a)** the remedy recorded when the finding was filed — assert the extracted invocation count is **exactly 1** per file (**rejected, and it is not a preference but a fact: it is FALSE on this tree.** `SECURITY.md` legitimately publishes **two** — one over the archive, one over `checksums.txt`, which is what covers the SBOMs listed inside it — so that assertion reds `main` on the day it lands, and the natural repair is to weaken it again); **(b)** universal quantification over invocations **(chosen)** — strictly stronger than (a) where (a) is true, and it keeps holding when a file legitimately grows a third correctly-pinned call. **Enforcement, per D-128, is one predicate**: `pin_violations ` prints one line per problem and nothing when the file is clean, so callers grade its OUTPUT and the identical function is asserted empty against the tree and non-empty against a mutant with no `set -e` games; `assert_all_pinned` is the thin failing wrapper; `log_unpinned_lines` is its runtime twin over the stub-cosign argv log. **Classification is fail-CLOSED, which is the part that carries the guarantee.** The candidate extractor is deliberately left un-narrowed (every non-comment line mentioning `cosign verify-blob`, continuations folded), because anything the *denominator* drops is a hole. A candidate is an invocation when the folded text begins with `cosign verify-blob`; the ONE waved-through non-invocation shape is a markdown inline-code mention (`` `cosign verify-blob` ``, which is how `SECURITY.md`'s capability table names it); **anything else — `foo && cosign verify-blob …`, a here-doc line, an un-backticked prose sentence — is reported UNCLASSIFIABLE rather than skipped**, because "this gate cannot tell whether that call is pinned" must never read as "that call is fine". Accepted cost, stated rather than discovered later: a *correctly pinned* invocation written off command position also reds. That is the intended direction of error for a security gate over three files carrying four invocations in one canonical style, and the message names the fix. **Anti-vacuity, because a lane whose entire deliverable is "make a gate stricter" is maximally exposed** (this repo's #1 review finding is an assertion that cannot fail — D-124, AUD-S18): section 2b runs **eight** mutants against **each** of the three files and 2c runs a ninth, and they were chosen for **branch** coverage of the new predicate rather than for variety of shape — (a) a second **unpinned** invocation must red, name the file, quote the offending command, and produce **exactly two** violations so the pinned siblings are provably not flagged; (b) a second **correctly pinned** invocation must stay green **and** must raise the extractor's invocation count by one, without which (b)'s green could mean "the extractor never saw it"; (c) an occurrence off command position, appended **fully pinned on purpose** so the only thing that can redden it is the classifier itself; (d) every invocation deleted → `NO-CANDIDATES`; (e) the continuation fold broken → `FOLD-BROKEN`, asserted **not** to also report `UNPINNED`, because conflating "the extractor truncated this" with "the pin is missing" sends the next maintainer to the wrong file; (f) every invocation displaced off command position → `NO-INVOCATIONS`; (g) a second invocation carrying both flags with an **empty** identity regexp → `WRONG-VALUE`, the hostile shape a presence-only check waves through; (h) a second invocation carrying both flags with a **foreign OIDC issuer** → `WRONG-VALUE` on the issuer half; and 2c strips the backticks from `SECURITY.md`'s prose mention and requires the same row to fail closed, proving the exemption keys on the backticks and is not a blanket bypass. The runtime twin has its own vacuity control (an unpinned line appended to a copy of the stub log must be seen). **One real defect was caught by this section during the lane and is recorded because it is a trap for the next author**: `log_unpinned_lines` was first written with `awk -v id="identity_re=${sec_identity}"`, and **awk processes escape sequences in a `-v` assignment**, so the pin's `github\.com` arrived as `github.com` and matched nothing; the values now reach awk through `ENVIRON`. **Stated limit, same posture as D-154's**: the denominator is the literal string `cosign verify-blob`, so an invocation spelled through a variable (`"$COSIGN" verify-blob …`), built by `eval`, or assembled from fragments is invisible to this gate. Widening the trigger to bare `verify-blob` was considered and **rejected** — it buys one hypothetical no file uses, and turns any future `SECURITY.md` sentence saying "verify-blob" outside backticks into a red gate, whose repair would be to loosen the classifier. **Nothing outside the gate changed**: `hack/install.sh`, `SECURITY.md` and `hack/release/verify-artifacts.sh` are byte-unchanged, and all four of their invocations were already pinned — this row closes a hole in the *checker*, not in the checked. The stage `release-install-cosign-pin-test` was already wired into `task check` and pinned in `hack/audit/exitgate_test.sh`'s `CHECK_STAGES`, so no wiring changed either. Revert: restore `has_flag`, drop the per-invocation value comparison, and restore the two positive-only stub-log greps — which returns the gate to certifying that *some* cosign call in each file is pinned, a property that is compatible with an unpinned one sitting beside it. | +| D-160 | 2026-08-23 | **UNIV-COSIGN — the cosign signer-pin gate asserted an EXISTENTIAL property where the guarantee it publishes is UNIVERSAL, so it certified nothing about a file's second `cosign verify-blob`; `hack/release/install_cosign_pin_test.sh` now grades EVERY invocation in ALL THREE published files, statically and at runtime.** Substance first, and measured before anything was written: a scratch copy of each graded file with a **second, unpinned** `cosign verify-blob` spliced IN-BODY next to its real invocation (the splice shape matters — see UC-04 below) ran the gate to **exit 0** — `hack/install.sh` rc=0, `SECURITY.md` rc=0, `hack/release/verify-artifacts.sh` rc=0, the last of these being the shape a reviewer had already demonstrated on an earlier lane. **Every individual assertion in that gate was sound.** `has_flag` grepped the whole folded extraction, so a pinned sibling satisfied it; `one_value`'s `sort -u` collapsed two agreeing values to one, so the D-153 drift comparison saw a consistent file; section 0 **printed** the extracted invocation count and asserted nothing about it; and 4b/5d's stub-log checks were positive-only greps, i.e. the same existential shape at runtime, where a second unpinned call leaves the pinned call's log line intact. The conjunction of sound existential assertions is still an existential assertion. **This is the AUD2-S05 quorum defect one layer out: not a wrong assertion, a wrong quantifier**, and it predates both AUD2-S03 and AUD2-F01. **`SECURITY.md` was worse than the other two** — it fed only the drift comparison and had **no invocation-level grading at all**, so an unpinned recipe published to adopters was invisible to the gate that exists to police the recipe. **Property chosen: "every `cosign verify-blob` invocation in every graded file carries `--certificate-oidc-issuer`, `--certificate-identity-regexp` and `--bundle`, EACH WITH SECURITY.md's published value".** The value half is not decoration: `--certificate-identity-regexp ''` carries the flag and matches every Fulcio identity ever issued, and `one_value`'s `sort -u` does not catch it either, because an empty capture is not a line and the file still reports exactly one distinct value — a presence-only universal check would be the same defect one level down, so each invocation's own extracted value is compared against the published pair (reported `WRONG-VALUE[...]`, distinct from `UNPINNED[...]`). Options considered: **(a)** the remedy recorded when the finding was filed — assert the extracted invocation count is **exactly 1** per file (**REJECTED AS FACTUALLY WRONG — do not implement it in a later lane; it would red `main` on the day it lands.** `SECURITY.md` legitimately publishes **two** — one over the archive, one over `checksums.txt`, which is what covers the SBOMs listed inside it — so that assertion reds `main` on the day it lands, and the natural repair is to weaken it again); **(b)** universal quantification over invocations **(chosen)** — strictly stronger than (a) where (a) is true, and it keeps holding when a file legitimately grows a third correctly-pinned call. **Enforcement, per D-128, is one predicate**: `pin_violations ` prints one line per problem and nothing when the file is clean, so callers grade its OUTPUT and the identical function is asserted empty against the tree and non-empty against a mutant with no `set -e` games; `assert_all_pinned` is the thin failing wrapper; `log_unpinned_lines` is its runtime twin over the stub-cosign argv log. **Classification is fail-CLOSED, which is the part that carries the guarantee.** The candidate extractor is deliberately left un-narrowed (every non-comment line mentioning `cosign verify-blob`, continuations folded), because anything the *denominator* drops is a hole. A candidate is an invocation when the folded text begins with `cosign verify-blob`; the ONE waved-through non-invocation shape is a markdown inline-code mention (`` `cosign verify-blob` ``, which is how `SECURITY.md`'s capability table names it); **anything else — `foo && cosign verify-blob …`, a here-doc line, an un-backticked prose sentence — is reported UNCLASSIFIABLE rather than skipped**, because "this gate cannot tell whether that call is pinned" must never read as "that call is fine". Accepted cost, stated rather than discovered later: a *correctly pinned* invocation written off command position also reds. That is the intended direction of error for a security gate over three files carrying four invocations in one canonical style, and the message names the fix. **Anti-vacuity, because a lane whose entire deliverable is "make a gate stricter" is maximally exposed** (this repo's #1 review finding is an assertion that cannot fail — D-124, AUD-S18): section 2b runs **eight** mutants against **each** of the three files and 2c runs a ninth, and they were chosen for **branch** coverage of the new predicate rather than for variety of shape — (a) a second **unpinned** invocation must red, name the file, quote the offending command, and produce **exactly two** violations so the pinned siblings are provably not flagged; (b) a second **correctly pinned** invocation must stay green **and** must raise the extractor's invocation count by one, without which (b)'s green could mean "the extractor never saw it"; (c) an occurrence off command position, appended **fully pinned on purpose** so the only thing that can redden it is the classifier itself; (d) every invocation deleted → `NO-CANDIDATES`; (e) the continuation fold broken → `FOLD-BROKEN`, asserted **not** to also report `UNPINNED`, because conflating "the extractor truncated this" with "the pin is missing" sends the next maintainer to the wrong file; (f) every invocation displaced off command position → `NO-INVOCATIONS`; (g) a second invocation carrying both flags with an **empty** identity regexp → `WRONG-VALUE`, the hostile shape a presence-only check waves through; (h) a second invocation carrying both flags with a **foreign OIDC issuer** → `WRONG-VALUE` on the issuer half; and 2c strips the backticks from `SECURITY.md`'s prose mention and requires the same row to fail closed, proving the exemption keys on the backticks and is not a blanket bypass. The runtime twin has its own vacuity control (an unpinned line appended to a copy of the stub log must be seen). **One real defect was caught by this section during the lane and is recorded because it is a trap for the next author**: `log_unpinned_lines` was first written with `awk -v id="identity_re=${sec_identity}"`, and **awk processes escape sequences in a `-v` assignment**, so the pin's `github\.com` arrived as `github.com` and matched nothing; the values now reach awk through `ENVIRON`. **Stated limit, same posture as D-154's**: the denominator is the literal string `cosign verify-blob`, so an invocation spelled through a variable (`"$COSIGN" verify-blob …`), built by `eval`, or assembled from fragments is invisible to this gate. Widening the trigger to bare `verify-blob` was considered and **rejected** — it buys one hypothetical no file uses, and turns any future `SECURITY.md` sentence saying "verify-blob" outside backticks into a red gate, whose repair would be to loosen the classifier. **Nothing outside the gate changed**: `hack/install.sh`, `SECURITY.md` and `hack/release/verify-artifacts.sh` are byte-unchanged, and all four of their invocations were already pinned — this row closes a hole in the *checker*, not in the checked. The stage `release-install-cosign-pin-test` was already wired into `task check` and pinned in `hack/audit/exitgate_test.sh`'s `CHECK_STAGES`, so no wiring changed either. **SECOND ROUND — the first version of this fix REPRODUCED the very defect it closes, one level down, and independent review caught it before merge.** `has_flag` grepped the whole FILE; the replacement grepped the whole LINE. Both are existential; only the scope shrank. **UC-01**: one folded line was graded as at most ONE invocation, so `cosign verify-blob --bundle a.json a && cosign verify-blob --bundle EVIL.json evil` began with `cosign verify-blob` (not UNCLASSIFIABLE), carried `--bundle` (not FOLD-BROKEN), carried both flag strings (not UNPINNED) and yielded the published values (not WRONG-VALUE) — **green**, in same-line, `;`-separated and backslash-folded forms, on all three graded files. Worse, the **full gate exited 0** for `SECURITY.md`: the two shell scripts were incidentally caught by the runtime twin (`log_unpinned_lines` at §5d), but **SECURITY.md is a document and has no runtime twin**, so the hole was unmitigated precisely on the file this row calls "the copy-paste recipe adopters run by hand" — D-153's exact incident class — while the gate printed "EVERY cosign verify-blob invocation ... is pinned", false as printed. The stated-limit paragraph did not cover it: it enumerated `$COSIGN`, `eval` and fragments, not `&&` chaining, and **leading** `&&` was explicitly handled (mutant (c) → UNCLASSIFIABLE), so the operator had been considered and only one side handled. Closed by grading per **OCCURRENCE** (`occurrence_count` + a new `MULTI-OCCURRENCE` violation that fails closed on any line carrying two calls) rather than per line; counting inside an already-triggered line uses the shorter `verify-blob`, so a second call spelled `cosign verify-blob` or `"$COSIGN" verify-blob` and chained onto a pinned one is caught too, which the literal file-level trigger would miss. **UC-02**: `extract_issuer`/`extract_identity` anchor on a greedy `.*`, so the LAST value on a line wins — a hostile `--certificate-identity-regexp ''` placed FIRST was masked by a correct value placed second, **the extraction direction favoured the attacker**. Closed by `flag_value_tokens`, which returns EVERY value of every flag on the occurrence; each must equal the published one, so a repeated flag with an empty value first now reds. **UC-03 (P2, the erosion path)**: a CORRECTLY pinned call written with **double quotes** was refused as `WRONG-VALUE ... identity= ... (an empty regexp matches every Fulcio identity)` — a true refusal with a **false reason**, and the repair a maintainer reaches for on that message is widening the extractor. Both quote styles are now accepted (double quotes are correct shell for this value: it contains no `$` and no backtick), and a **bare** value is diagnosed as `UNQUOTED-VALUE`, a QUOTING defect, never as a wrong or empty one — a gate that misdiagnoses erodes faster than one that refuses. **UC-04**: this row's "rc=0, rc=0, rc=0" reproduction figure is **splice-shape-sensitive** and is stated as measured: it holds for a second unpinned call spliced **in-body** next to the real one. An EOF-appended mutant reds the two shell scripts for an unrelated runtime reason, so the figure should not be read as holding for any second unpinned call. The same sensitivity is why the UC-03 double-quoted mutant reds the two scripts through the full gate (the spliced call actually RUNS and its fixture bundle is absent) while `SECURITY.md`, having no runtime, is the clean end-to-end proof at rc=0. The classifier's fail-closed posture on off-command-position occurrences was independently adjudicated KEEP, since §2c proves the prose exemption keys on the backticks and cannot be widened silently. **The lesson, recorded because it is the whole point of the lane:** a fix for an existential-where-universal defect is itself maximally exposed to the same defect at the next scope down — file, then line, then occurrence — and the only thing that caught it was a reviewer building the chained-call mutant that neither the 20-row external matrix nor the 25 in-gate mutants contained. Revert: restore `has_flag`, drop the per-occurrence grading and the per-invocation value comparison, and restore the two positive-only stub-log greps — which returns the gate to certifying that *some* cosign call in each file is pinned, a property that is compatible with an unpinned one sitting beside it. | diff --git a/hack/release/install_cosign_pin_test.sh b/hack/release/install_cosign_pin_test.sh index c4c9e0e..0456af4 100755 --- a/hack/release/install_cosign_pin_test.sh +++ b/hack/release/install_cosign_pin_test.sh @@ -70,6 +70,31 @@ # This is the AUD2-S05 quorum bug one layer out: not a wrong assertion, a wrong # quantifier. # +# SECOND ROUND (UC-01..UC-04) — THE FIRST D-160 FIX REPRODUCED THE DEFECT IT WAS +# WRITTEN TO CLOSE, one level down, and independent review caught it. has_flag +# grepped the whole FILE; the replacement grepped the whole LINE. Both are +# existential; only the scope shrank. One folded line was graded as at most ONE +# invocation, so +# +# cosign verify-blob --bundle a.json a && cosign verify-blob --bundle EVIL.json evil +# +# started with `cosign verify-blob` (not UNCLASSIFIABLE), carried --bundle (not +# FOLD-BROKEN), carried both flag strings (not UNPINNED) and yielded the published +# values (not WRONG-VALUE): GREEN, in same-line, `;`-separated and backslash-folded +# forms, on all three graded files — and the FULL gate exited 0 on SECURITY.md, +# which has no runtime twin because it is a document. The gate printed "EVERY +# cosign verify-blob invocation ... is pinned", which was false as printed. +# Closed by grading per OCCURRENCE (occurrence_count + MULTI-OCCURRENCE), not per +# line. UC-02: extract_issuer/extract_identity anchor on a greedy `.*`, so the LAST +# value on a line won and a hostile `--certificate-identity-regexp ''` placed FIRST +# was masked by a correct value placed second — the extraction direction favoured +# the attacker. Closed by grading EVERY value of every flag (flag_value_tokens). +# UC-03: a CORRECTLY pinned call written with double quotes was refused as +# "identity= ... an empty regexp matches every Fulcio identity" — +# a true refusal with a false reason, and the repair a maintainer reaches for is +# widening the extractor. Both quote styles are now accepted and a BARE value is +# diagnosed as a QUOTING defect (UNQUOTED-VALUE), never as a wrong or empty value. +# # ANTI-VACUITY DISCIPLINE (this repo has a documented history of gates that # cannot fail — D-124, AUD-S18). Every assertion here is a FUNCTION over a file # or a fixture, run twice: once against the real tree (must be GREEN) and once @@ -147,11 +172,77 @@ extract_issuer() { } # extract_identity — every distinct --certificate-identity-regexp value. -# The value is single-quoted in all three graded files (a shell regexp must be); -# an unquoted -# value extracts as nothing and trips the positive controls rather than passing. +# BOTH quote styles are accepted (UC-03). The value is single-quoted in all three +# graded files and it must be quoted somehow — a BARE regexp is glob-expanded and +# word-split by the shell, so `[Aa]ssent` would silently become something else — +# but double quotes are an equally correct spelling for this particular value (it +# contains no $ and no backtick). A gate that reds on a CORRECTLY pinned, +# double-quoted call while blaming "an empty regexp that matches every Fulcio +# identity" teaches the next maintainer to widen the extractor, which is how a +# pin gate erodes. A bare value still extracts as nothing here, and pin_violations +# names QUOTE STYLE as the cause instead of misdiagnosing it as a wrong value. extract_identity() { - sed -nE "s/.*--certificate-identity-regexp[[:space:]]+'([^']*)'.*/\1/p" "$1" | sort -u + sed -nE "s/.*--certificate-identity-regexp[[:space:]]+'([^']*)'.*/\1/p;s/.*--certificate-identity-regexp[[:space:]]+\"([^\"]*)\".*/\1/p" "$1" | sort -u +} + +# --------------------------- UC-01 / UC-02: per-OCCURRENCE grading ---------- +# +# THE DEFECT THIS BLOCK EXISTS TO CLOSE, stated plainly because it is the same +# defect D-160 was opened to fix, reproduced one level down. The first D-160 fix +# replaced has_flag — which grepped the whole FILE, so a pinned sibling anywhere +# satisfied it — with a check that grepped the whole LINE. That is still an +# existential test, just with a smaller scope: one folded line was graded as at +# most ONE invocation, so +# +# cosign verify-blob --bundle a.json a && cosign verify-blob --bundle EVIL.json evil +# +# started with `cosign verify-blob` (not UNCLASSIFIABLE), contained --bundle (not +# FOLD-BROKEN), contained both flag strings (not UNPINNED) and yielded the +# published values (not WRONG-VALUE). Green. Confirmed in same-line, `;`-separated +# and backslash-folded forms, on all three graded files. The universal property +# is per OCCURRENCE, not per line. +# +# occurrence_count — how many verify-blob calls sit on one folded line. +# The line-level TRIGGER stays the literal `cosign verify-blob` (see +# cosign_candidates) because widening it to bare `verify-blob` reds on prose; but +# COUNTING inside an already-triggered line uses the shorter `verify-blob`, so a +# second call spelled `cosign verify-blob` or `"$COSIGN" verify-blob` and chained +# onto a pinned one is still SEEN and still fails closed. +occurrence_count() { + # WHOLE WORDS, not substrings. A substring count reds on a perfectly good + # invocation whose BUNDLE is named `verify-blob-test.sigstore.json` — a + # false positive on a plausible filename, sitting on the branch that carries the + # whole UC-01 fix, so the repair a maintainer would reach for is loosening this + # very function. awk's default field splitting also folds runs of whitespace, so + # `cosign verify-blob` and `"$COSIGN" verify-blob` still count as occurrences. + # Residual, stated: a bundle named exactly `verify-blob` (no extension) counts as + # an occurrence and fails closed. No file does that, and closed is the safe way + # to be wrong. + printf '%s' "$1" | awk '{ for (i = 1; i <= NF; i++) if ($i == "verify-blob") n++ } END { print n + 0 }' +} + +# flag_value_tokens — reads one folded line on stdin and prints the RAW +# value token following EVERY occurrence of (quotes included), one per line. +# +# "Every", not "the last one", is the point (UC-02). extract_issuer and +# extract_identity anchor on a greedy `.*`, so on a line carrying two values the +# LAST one wins — and a hostile `--certificate-identity-regexp ''` placed FIRST is +# masked by a correct value placed second. The extraction direction favoured the +# attacker. Here every value is returned and every one has to match. +flag_value_tokens() { + local flag="$1" + grep -oE -- "$flag[[:space:]]+('[^']*'|\"[^\"]*\"|[^[:space:]]+)" \ + | sed -E "s/^$flag[[:space:]]+//" || true +} + +# unquote — prints "quotedvalue" or "barevalue". +unquote() { + local raw="$1" n=${#1} + case "$raw" in + \'*\') printf 'quoted\t%s\n' "${raw:1:n-2}" ;; + \"*\") printf 'quoted\t%s\n' "${raw:1:n-2}" ;; + *) printf 'bare\t%s\n' "$raw" ;; + esac } # one_value

..value[key].field`, which compiles and is lint-clean because `internal/lint/facts_ref.go`'s D-051 shape check permits arbitrary navigation past `.value` and only forbids indexing `facts` itself; set difference — `oldEntry.acls.filter(a, !(a in entry.acls)).size() == 0`; named intermediates — no `cel.bind`, but re-deriving the sub-expression inside each leaf is semantically identical and compiles. **The sharpest finding is a distinction, not a rule:** same-changeset **cross-file** reasoning fails for **input availability**, not expressiveness — the evaluation unit is one file (`change.ChangeSet` is documented "for one file", `internal/change/diff.go:129`; `assent run` strips one `--subject file:`, `cmd/assent/run.go:266`, and diffs it alone, `:293`) and **REQ-E11-S05-01 pins the Rego module to the identical `EvaluationInput`** with the tier fenced to "declared data, no I/O". **A Rego module therefore fails that rule identically, so it is struck from E11's justification too** — the fix is an input decision, which E11's non-goals fence, not a backend decision. Corroborating: the one committed illustration of the escape hatch, `examples/policies/rego/bounded_change.rego`, is **entirely tier-1 expressible** — both `violations` rules are per-change predicates and `examples/policies/declarative/bounded-change.yaml` is the same rule already in the envelope. **The strongest single piece of evidence, and the one that sizes the epic, is the graph shape.** On the `assent run` path document-mode `walkNode` emits a Change **only where two scalars differ** — a sequence on either side makes the whole ChangeSet **opaque → REVIEW** before any rule runs (`internal/change/diff.go`) — and collection-mode `DiffEntries` is reached only from `internal/adoptertest`, so `old`/`new`/`entry`/`oldEntry` and every `changes[i].old`/`.new` bind **scalars**. That does **not** starve a graph rule, because a flat `set` fact still carries structure: `edges: {type: string, cardinality: set}` returning `["orders|billing","billing|ledger"]` is a **fully declarable, in-contract adjacency inside `EvaluationInput` today** — the declaration is legal (`schemas/provider/v1alpha1/response.schema.json`), `fact.value` carries no JSON-Schema type constraint and `ResolveFactsChecked` cross-checks the *declaration* not the value (`internal/provider/resolve.go`), outputs are operator-authored (`internal/provider/config.go`), the `http` transport is live on the plain run path with **no `--checkout`** (`cmd/assent/provider_host.go` `providerCallFor`), and a set fact binds as a CEL list. Tier-1 CEL nonetheless cannot answer the actual question over it: **CEL has no recursion, fixpoint, fold or user-defined function, so unbounded reachability has no spelling** (`transitiveClosure` → `undeclared reference`; the four comprehension macros iterate one level and cannot call themselves). **Stated precisely, because two drafts of this record overreached and both were caught by independent review:** a *bounded* `k`-hop check **is** expressible and does **not** need the string decomposition CEL lacks — over a finite in-input candidate set (a `nodes` set fact, the same construction as `edges`), decode is replaceable by **encode-and-compare**: `nodes.value.exists(m, nodes.value.exists(n, (string(new)+"|"+m) in edges.value && (m+"|"+n) in edges.value && (n+"|"+string(new)) in edges.value))` compiles **and evaluates** under the real `cel.CostLimit(1_000_000)` to `true/true/true/false` over the fixture above, and `nodes.value.filter(m, (string(new)+"|"+m) in edges.value)` recovers an edge's far end as `[billing]`. Both primitives (`+` on strings, `in`) were already in this record's own function census, so the claim that decoding was a second independent barrier was internally inconsistent as well as false. **The real ceiling is `k`, and a third draft got its cost wrong too** — it claimed `O(|N|^(k-1)·|E|)` "exhausts the cost budget on any real graph". Wrong complexity class and wrong conclusion, because the census had omitted the surface's only value binder, `[expr].all(v, …)`: binding each BFS frontier once per level makes cost additive across levels, and measured under the real `cel.CostLimit(1_000_000)` a ring `|N|=50, deg 5` costs 89,551 at `k=10`, 235,297 at `k=20` and 686,317 at `k=50` — roughly linear in `k`, and at `k=50 ≥ |N|` CEL is **not approximating at all, it decides reachability exactly**, in 69% of budget. The practical `k` collapses around `|N|≈200` (`k=10` at 46% of budget, `k=20` exceeds). Recorded because a reader sizing this epic is entitled to ask "would CEL suffice for *our* graph?" and the previous sentence foreclosed that question with an assertion measurement refutes; it is **not** offered as a second reason. **What carries the verdict is one property, now measured rather than recalled: the iteration count of a tier-1 CEL expression cannot be made data-dependent.** `reduce`, `transformList`, `transformMap`, two-var `all(i,x,…)`, `range`/`lists.range` and `cel.bind` are all `undeclared reference`; `for` is a `reserved identifier`; there is no fold, self-reference or generator; so depth is a **syntactic** property, hard-capped by cel-go's parser recursion limit of 250 (`expression recursion limit exceeded: 250` at depth 260, depth 200 still compiles). That a fixed `k` really is an approximation when the data outruns it is measured too: on a 4-cycle the `k=3` form evaluates `false` and the `k=4` form `true`. **Rego answers the unbounded question with `graph.reachable` — pure and deterministic — and that single gap is the whole justification.** **An input that is in contract and available today, over which CEL can only approximate and Rego decides, is exactly the per-rule evidence D-017's gate demanded — so E11 has TWO unconditional justifications (folds and graphs), neither waiting on any open question.** Deliverability caveat, stated because this row makes the same distinction for sub-shape B1: **no provider in the corpus ships an encoded adjacency today** — that one *can* follows from the provider contract, the same inference used to strike B1, not from a shipped example. Options considered: **(a)** record all four shapes as exceeding, the reading D-141's unlock invites (rejected — three are demonstrably expressible and an unfalsifiable ceiling claim is the defect this story exists to prevent); **(b)** strike set-difference **conditionally**, so that a narrowing answer to OQ-35 would return it to the ceiling (rejected on the second pass — both resolutions strike it: extending the entry binding makes CEL express it, narrowing makes it an input-availability failure that REQ-E11-S05-01 hands to Rego unchanged, so a conditional would have left a downstream story waiting on an answer that cannot change the verdict); **(c)** strike cross-manifest and set-difference **unconditionally**, strike half of multi-pass, keep folds and in-input graphs **both unconditionally** **(chosen)**. **Two rejected drafts are recorded because the same failure produced both, with the sign flipped, and only independent review caught either.** Draft 1 made the graph shape *contingent* on OQ-35/OQ-36 on the premise that "an adjacency needs a mapping-valued fact" — it does not; a set of encoded strings carries one inside the frozen declaration — which came from conflating a *provider-supplied catalog* (sub-shapes B1/B2, struck here as working and shipped) with **B3, which is specifically same-changeset cross-file *diffs***. It would have advised the operator to defer a 14-story epic on a premise that does not hold. Draft 2 replaced that with a second "independent reason" — that CEL cannot decode an edge, killing even a bounded two-hop check — **refuted by execution** (the encode-and-compare leaf above). Draft 3 replaced *that* with the exponential-cost claim above — **refuted by measurement**. The common cause across all three is one habit: **reaching for a second independent reason when one sufficient reason was already in hand**, and then applying an **asymmetric evidentiary standard** to protect it — accepting awkward-but-working spellings when they *struck* a shape (A2's re-derivation, B2's dynamic index) and rejecting them when they would have *narrowed* one this record wanted to keep. The verdict was right in all four drafts; the supporting argument was wrong in three. It now rests on one measured property and no supporting argument at all, which is the form it should have taken first. The correction to A2 runs the same way: the value binder `[expr].all(v, …)` removes the evaluation-cost half of A2's residual, so **A2 is struck more firmly than the first draft struck it**. Binds later stories: **S05** must not be widened to carry cross-manifest data; **S07**'s violation shape must support a fold result and a path/cycle witness, not a cross-manifest reference; **S12** must correct ADR-0002's `rego` bullet, which calls the tier an "escape hatch for **cross-entry checks**" — inaccurate for the shipped input contract; **S11** must label the unquarantined example a shape illustration, never evidence of need. **Binds E11-S04, whose denylist is not yet written: `graph.reachable` MUST be allowed**, with `split` alongside it — both pure and deterministic. `graph.reachable` is the one that carries the justification (it closes the graph at any depth); `split` is a convenience for rebuilding the adjacency. A capability set drafted from "deny anything unfamiliar" would strike out the epic's own strongest justification. Recorded in the S04 section of the epic spec, not only S01's. **That floor is held by REVIEW, not by a gate, and this row says so rather than inventing an enforcement path:** REQ-E11-S04-02's committed golden detects a *change* to the allowed set (so the sandbox cannot silently widen) and cannot detect an *omission* — a golden written without `graph.reachable` stays green forever. It says nothing about judgment call (d), since *which* builtins are callable is orthogonal to *where* the evaluator lives. Two residuals raised, neither decided, **neither gating any verdict here**, and neither the escalated rule-7 (d1)/(d2) question: **OQ-35** (the `entry`/`oldEntry` binding asymmetry — a silent `assent test` / `assent run` divergence; set-difference is struck either way and the graph shape needs no entry tree) and **OQ-36** (the frozen provider declaration has no object/map type, yet the authoring surface and `builtin/repo-file` together permit a mapping-valued fact). Also flagged, not edited (out of lane): `REQ-DEM-S05-04` calls the provider-visible tree the "merged-result checkout"; the code reads `/head`, documented at `cmd/assent/checkout.go:44` as "the MERGE-REQUEST HEAD". This lane writes no Go, adds no dependency and touches no schema. Revert: delete `docs/planning/rego-tier-ceiling.md` and the D-156 narrowing text from the E11 spec — which restores an epic justified by four shapes, three of which this record shows are not real. | | D-158 | 2026-08-23 | **CI-TOOLCHAIN — `verify` was red on every PR from a golangci-lint/Go skew; the remedy is to bump `GOLANGCI_LINT_VERSION` v2.12.2 → v2.13.1 and KEEP `go-version: stable`.** Symptom: PR #85, a six-file Markdown diff with **zero Go bytes**, failed `verify` with `/opt/hostedtoolcache/go/1.27.0/x64/src/crypto/internal/randutil/randutil.go:11:2: could not import math/rand/v2 (… method must have no type parameters) (typecheck)` — the failing path is inside the **Go toolchain's own source tree**, so no author change can fix it and re-running cannot clear it. `Analyze (go)`, `Analyze (actions)` and `CodeQL` all passed on the same run: the tree compiles clean under Go 1.27, only the linter chokes. **Mechanism**: golangci-lint typechecks the standard library with the `go/types` it was **compiled with**, not the `go` on `PATH`. GitHub's `stable` rolled 1.26 → 1.27.0 between this repo's last green `main` run (2026-08-19) and 2026-08-23; the v2.12.2 release binary is built with go1.26.x and cannot read the 1.27 stdlib. **Reproduced locally, not reasoned** (Go 1.27.0 SDK on `PATH`, `GOTOOLCHAIN=local`, whole tree): v2.12.2 → **panic** in `pkg/goanalysis/runner_loadingpackage.go:335` inside `go/types.(*Checker).Files`, exit 2; official v2.13.1 asset (`built with go1.27.0`) → **0 issues**, exit 0; `golangci-lint config verify` → exit 0, so the v2 config schema in `.golangci.yml` needs no migration; v2.13.1 also → **0 issues** against local Go 1.26.6, so the bump is safe for contributors who have not moved; and `go install …@v2.13.1` under Go 1.27.0 → 0 issues, which is the **`release-exitgate`** path (that job builds the binary rather than using the action, and `if: github.event_name != 'pull_request'` / RELSE-08 means no PR ever exercises it). **Diagnosis heuristic worth keeping**: golangci-lint's `go.mod` carries the comment *"the minimum Go version must always be latest-1"*, so its `go` directive is a machine-readable "supports Go 1.N+1" signal — v2.12.2 says `go 1.25.0` (supports ≤1.26), v2.13.1 says `go 1.26.0` (supports ≤1.27), and upstream commit `42a0530` in v2.13.0 is literally "go1.27 support". **Options considered.** (A) *bump the linter* — CHOSEN: treats the root cause, is a **one-line** diff because the version is single-sourced at workflow scope (D-128), fixes BOTH exposed sites (the `golangci-lint-action` in `verify` and the `go install` in `release-exitgate`) at once, and the risk it carried — new findings from a newer linter blocking every merge, since `golangci-lint` runs inside `task lint` inside `task check` — was **measured at zero** on the whole tree under both Go versions. (B) *pin `go-version: 1.26.x`* — REJECTED as the primary: it needs two pins (`verify.yaml:56` and `:171`), leaves the class of bug live, undercuts the stated reason `stable` is there (`# govulncheck needs it`, with `setup-go` exporting `GOTOOLCHAIN=local` so a pinned toolchain can fail to `go run` a tool whose module requires a newer Go — unverified, and moot under (A)), and trades a loud recurrence for **silent indefinite drift onto an unsupported Go** in a repo whose posture is govulncheck + cosign + SLSA + Scorecard. (C) *both* — REJECTED as gold-plating: (A) alone is measured green, and a second simultaneous remedy would make a still-red PR ambiguous. **Per-file sweep of `go-version: stable`, stated rather than silently skipped:** `verify.yaml:56` and `:171` were the only exposed sites and are fixed by the env bump without touching either line; `schemas.yml:57` (runs `go test` + ajv, no linter), `vulncheck.yaml:30` (govulncheck only — `stable` is actively *desirable* there) and `codeql.yaml:45` (CodeQL, which passed on 1.27.0) carry no golangci-lint and are NOT exposed; `release.yaml` uses `go-version-file: go.mod` and is unaffected. `hack/lint/workflow_pins_test.sh` asserts `TASK_VERSION`, action SHA pins and step wiring but **not** `go-version` or `GOLANGCI_LINT_VERSION`; it passes on this change. **Revert is (B), not bare v2.12.2** — reverting the env line alone restores a known-red state: revert = `GOLANGCI_LINT_VERSION` back to `v2.12.2` **and** pin `verify.yaml:56` + `:171` to `go-version: 1.26.x`. **Residual risk, stated plainly:** when `stable` rolls to Go 1.28, v2.13.1 breaks identically. The repo finds out because `verify` reds on **every** PR including zero-Go diffs — loud and immediate, with the signature recorded in `verify.yaml`'s env comment and the fix being one env line. Nothing detects it *earlier*: dependabot's `github-actions` ecosystem updates `uses:` refs, not `env:` literals (backlog `CI-TOOLCHAIN-F01`). Accepted on purpose over (B)'s failure mode. Note also the pre-existing local/CI linter skew — `Taskfile.yml`'s `lint` task is bare `golangci-lint run ./...` against whatever binary a contributor has installed, so this pin has never governed local `task check`; deliberately not changed here (that file was owned by a concurrent lane). | | D-159 | 2026-08-23 | **ORPHAN — `release-verify-test` was a gate invoked by nothing (D-124 again), and it is wired into `task check` in its three OFFLINE modes, not its default `all`.** Finding: `Taskfile.yml` defined `release-verify-test` — the **only** test of `hack/release/verify-artifacts.sh` — and no caller existed anywhere: not `check:`, not `CHECK_STAGES` in `hack/audit/exitgate_test.sh`, not `.github/workflows/**`, not the push-only `release-exitgate`. That script is not incidental: **`SECURITY.md:61` publishes it as the procedure release consumers run** to check artifact checksums, the stamped `assent version` and cosign signatures, and D-153/AUD2-F01 had just proved that published verification instructions rot silently. Measured before fixing, as the lane required: the gate was **green**, so this is a wiring defect only — nothing was being papered over. **Why not the `all` default.** `verify_test.sh` with no argument adds `test_snapshot_pass`, which shells out to `task release-snapshot`: `go install github.com/goreleaser/goreleaser/v2@…` on any machine without it (**network**, in a gate that runs before every commit), a `before: hooks: go mod tidy` that **rewrites `go.mod`/`go.sum` in the middle of `task check`**, `--clean` on the developer's `dist/`, and a five-target cross-compile (10s here with warm caches and goreleaser already installed; minutes cold). A flaky or network-bound stage is worse than a missing one, so `check:` runs `negative`, `cosign-skip-when-absent` and `readme` — REQ-E9-S12-02/03/04, all offline, together well under a second. **Consequence, stated precisely: REQ-E9-S12-01 (the real snapshot→verify round trip) is not gated per-commit in `task check`; it runs in push-only CI via `hack/release/exitgate_test.sh:33-34` (the `release-exitgate` job, `if: github.event_name != 'pull_request'`) — automated but not PR-visible, i.e. the RELSE-08 blind spot.** Those two lines are literally `task release-snapshot` then `task release-verify`, which is the `Verify:` string the spec gives the requirement (`openspec/specs/p5-e9-distribution/spec.md:441-442`), so nothing here needs a new gate built — an earlier draft of this row claimed the requirement was covered by no automation at all, which was false, and acting on it would have meant a future lane duplicating `exitgate_test.sh:33-34`. What this lane declines to do is move that L1 round trip into a per-commit gate: it cannot be, for the network/`go mod tidy`/`--clean` reasons above. Narrowing the RELSE-08 exposure for this requirement is a separate question from D-159. **Pinning.** `CHECK_STAGES` goes 20 → 21 in the same commit as the `check:` line (the AUD-S18/RELSE-08 lockstep), and `STAGE_BODY_PINS` pins the body **per mode** rather than by the bare script path — a single `bash hack/release/verify_test.sh` pin would stay green if two modes were dropped *and* if the stage were reverted to the unrunnable-in-check default. Three mutation controls prove it: deleting the `check:` line reds `check_check_wiring` by stage name, gutting one of the three modes reds `check_stage_bodies` while the other two still run, and the same deletion applied to the real tree reds the real gate at rc=1. **Also fixed, minimally, because wiring made it matter:** `verify_test.sh` wrote its captured stdout/stderr to fixed `/tmp/verify-{tamper,nosig}.{out,err}` and then **grepped** them; harmless while nothing ran it, but this repo runs several lane worktrees whose `task check` invocations overlap, and a concurrent run truncating `/tmp/verify-nosig.err` at open would fail the other run's `skip.*cosign` grep spuriously. Scratch files now live in each run's own `mktemp -d` (invisible to `verify-artifacts.sh`, which globs only `*.tar.gz`/`*.zip`) and are removed by the existing `RETURN` trap. | -| D-160 | 2026-08-23 | **UNIV-COSIGN — the cosign signer-pin gate asserted an EXISTENTIAL property where the guarantee it publishes is UNIVERSAL, so it certified nothing about a file's second `cosign verify-blob`; `hack/release/install_cosign_pin_test.sh` now grades EVERY invocation in ALL THREE published files, statically and at runtime.** Substance first, and measured before anything was written: a scratch copy of each graded file with a **second, unpinned** `cosign verify-blob` spliced IN-BODY next to its real invocation (the splice shape matters — see UC-04 below) ran the gate to **exit 0** — `hack/install.sh` rc=0, `SECURITY.md` rc=0, `hack/release/verify-artifacts.sh` rc=0, the last of these being the shape a reviewer had already demonstrated on an earlier lane. **Every individual assertion in that gate was sound.** `has_flag` grepped the whole folded extraction, so a pinned sibling satisfied it; `one_value`'s `sort -u` collapsed two agreeing values to one, so the D-153 drift comparison saw a consistent file; section 0 **printed** the extracted invocation count and asserted nothing about it; and 4b/5d's stub-log checks were positive-only greps, i.e. the same existential shape at runtime, where a second unpinned call leaves the pinned call's log line intact. The conjunction of sound existential assertions is still an existential assertion. **This is the AUD2-S05 quorum defect one layer out: not a wrong assertion, a wrong quantifier**, and it predates both AUD2-S03 and AUD2-F01. **`SECURITY.md` was worse than the other two** — it fed only the drift comparison and had **no invocation-level grading at all**, so an unpinned recipe published to adopters was invisible to the gate that exists to police the recipe. **Property chosen: "every `cosign verify-blob` invocation in every graded file carries `--certificate-oidc-issuer`, `--certificate-identity-regexp` and `--bundle`, EACH WITH SECURITY.md's published value".** The value half is not decoration: `--certificate-identity-regexp ''` carries the flag and matches every Fulcio identity ever issued, and `one_value`'s `sort -u` does not catch it either, because an empty capture is not a line and the file still reports exactly one distinct value — a presence-only universal check would be the same defect one level down, so each invocation's own extracted value is compared against the published pair (reported `WRONG-VALUE[...]`, distinct from `UNPINNED[...]`). Options considered: **(a)** the remedy recorded when the finding was filed — assert the extracted invocation count is **exactly 1** per file (**REJECTED AS FACTUALLY WRONG — do not implement it in a later lane; it would red `main` on the day it lands.** `SECURITY.md` legitimately publishes **two** — one over the archive, one over `checksums.txt`, which is what covers the SBOMs listed inside it — so that assertion reds `main` on the day it lands, and the natural repair is to weaken it again); **(b)** universal quantification over invocations **(chosen)** — strictly stronger than (a) where (a) is true, and it keeps holding when a file legitimately grows a third correctly-pinned call. **Enforcement, per D-128, is one predicate**: `pin_violations ` prints one line per problem and nothing when the file is clean, so callers grade its OUTPUT and the identical function is asserted empty against the tree and non-empty against a mutant with no `set -e` games; `assert_all_pinned` is the thin failing wrapper; `log_unpinned_lines` is its runtime twin over the stub-cosign argv log. **Classification is fail-CLOSED, which is the part that carries the guarantee.** The candidate extractor is deliberately left un-narrowed (every non-comment line mentioning `cosign verify-blob`, continuations folded), because anything the *denominator* drops is a hole. A candidate is an invocation when the folded text begins with `cosign verify-blob`; the ONE waved-through non-invocation shape is a markdown inline-code mention (`` `cosign verify-blob` ``, which is how `SECURITY.md`'s capability table names it); **anything else — `foo && cosign verify-blob …`, a here-doc line, an un-backticked prose sentence — is reported UNCLASSIFIABLE rather than skipped**, because "this gate cannot tell whether that call is pinned" must never read as "that call is fine". Accepted cost, stated rather than discovered later: a *correctly pinned* invocation written off command position also reds. That is the intended direction of error for a security gate over three files carrying four invocations in one canonical style, and the message names the fix. **Anti-vacuity, because a lane whose entire deliverable is "make a gate stricter" is maximally exposed** (this repo's #1 review finding is an assertion that cannot fail — D-124, AUD-S18): section 2b runs **eight** mutants against **each** of the three files and 2c runs a ninth, and they were chosen for **branch** coverage of the new predicate rather than for variety of shape — (a) a second **unpinned** invocation must red, name the file, quote the offending command, and produce **exactly two** violations so the pinned siblings are provably not flagged; (b) a second **correctly pinned** invocation must stay green **and** must raise the extractor's invocation count by one, without which (b)'s green could mean "the extractor never saw it"; (c) an occurrence off command position, appended **fully pinned on purpose** so the only thing that can redden it is the classifier itself; (d) every invocation deleted → `NO-CANDIDATES`; (e) the continuation fold broken → `FOLD-BROKEN`, asserted **not** to also report `UNPINNED`, because conflating "the extractor truncated this" with "the pin is missing" sends the next maintainer to the wrong file; (f) every invocation displaced off command position → `NO-INVOCATIONS`; (g) a second invocation carrying both flags with an **empty** identity regexp → `WRONG-VALUE`, the hostile shape a presence-only check waves through; (h) a second invocation carrying both flags with a **foreign OIDC issuer** → `WRONG-VALUE` on the issuer half; and 2c strips the backticks from `SECURITY.md`'s prose mention and requires the same row to fail closed, proving the exemption keys on the backticks and is not a blanket bypass. The runtime twin has its own vacuity control (an unpinned line appended to a copy of the stub log must be seen). **One real defect was caught by this section during the lane and is recorded because it is a trap for the next author**: `log_unpinned_lines` was first written with `awk -v id="identity_re=${sec_identity}"`, and **awk processes escape sequences in a `-v` assignment**, so the pin's `github\.com` arrived as `github.com` and matched nothing; the values now reach awk through `ENVIRON`. **Stated limit, same posture as D-154's**: the denominator is the literal string `cosign verify-blob`, so an invocation spelled through a variable (`"$COSIGN" verify-blob …`), built by `eval`, or assembled from fragments is invisible to this gate. Widening the trigger to bare `verify-blob` was considered and **rejected** — it buys one hypothetical no file uses, and turns any future `SECURITY.md` sentence saying "verify-blob" outside backticks into a red gate, whose repair would be to loosen the classifier. **Nothing outside the gate changed**: `hack/install.sh`, `SECURITY.md` and `hack/release/verify-artifacts.sh` are byte-unchanged, and all four of their invocations were already pinned — this row closes a hole in the *checker*, not in the checked. The stage `release-install-cosign-pin-test` was already wired into `task check` and pinned in `hack/audit/exitgate_test.sh`'s `CHECK_STAGES`, so no wiring changed either. **SECOND ROUND — the first version of this fix REPRODUCED the very defect it closes, one level down, and independent review caught it before merge.** `has_flag` grepped the whole FILE; the replacement grepped the whole LINE. Both are existential; only the scope shrank. **UC-01**: one folded line was graded as at most ONE invocation, so `cosign verify-blob --bundle a.json a && cosign verify-blob --bundle EVIL.json evil` began with `cosign verify-blob` (not UNCLASSIFIABLE), carried `--bundle` (not FOLD-BROKEN), carried both flag strings (not UNPINNED) and yielded the published values (not WRONG-VALUE) — **green**, in same-line, `;`-separated and backslash-folded forms, on all three graded files. Worse, the **full gate exited 0** for `SECURITY.md`: the two shell scripts were incidentally caught by the runtime twin (`log_unpinned_lines` at §5d), but **SECURITY.md is a document and has no runtime twin**, so the hole was unmitigated precisely on the file this row calls "the copy-paste recipe adopters run by hand" — D-153's exact incident class — while the gate printed "EVERY cosign verify-blob invocation ... is pinned", false as printed. The stated-limit paragraph did not cover it: it enumerated `$COSIGN`, `eval` and fragments, not `&&` chaining, and **leading** `&&` was explicitly handled (mutant (c) → UNCLASSIFIABLE), so the operator had been considered and only one side handled. Closed by grading per **OCCURRENCE** (`occurrence_count` + a new `MULTI-OCCURRENCE` violation that fails closed on any line carrying two calls) rather than per line; counting inside an already-triggered line uses the shorter `verify-blob`, so a second call spelled `cosign verify-blob` or `"$COSIGN" verify-blob` and chained onto a pinned one is caught too, which the literal file-level trigger would miss. **UC-02**: `extract_issuer`/`extract_identity` anchor on a greedy `.*`, so the LAST value on a line wins — a hostile `--certificate-identity-regexp ''` placed FIRST was masked by a correct value placed second, **the extraction direction favoured the attacker**. Closed by `flag_value_tokens`, which returns EVERY value of every flag on the occurrence; each must equal the published one, so a repeated flag with an empty value first now reds. **UC-03 (P2, the erosion path)**: a CORRECTLY pinned call written with **double quotes** was refused as `WRONG-VALUE ... identity= ... (an empty regexp matches every Fulcio identity)` — a true refusal with a **false reason**, and the repair a maintainer reaches for on that message is widening the extractor. Both quote styles are now accepted (double quotes are correct shell for this value: it contains no `$` and no backtick), and a **bare** value is diagnosed as `UNQUOTED-VALUE`, a QUOTING defect, never as a wrong or empty one — a gate that misdiagnoses erodes faster than one that refuses. **UC-04**: this row's "rc=0, rc=0, rc=0" reproduction figure is **splice-shape-sensitive** and is stated as measured: it holds for a second unpinned call spliced **in-body** next to the real one. An EOF-appended mutant reds the two shell scripts for an unrelated runtime reason, so the figure should not be read as holding for any second unpinned call. The same sensitivity is why the UC-03 double-quoted mutant reds the two scripts through the full gate (the spliced call actually RUNS and its fixture bundle is absent) while `SECURITY.md`, having no runtime, is the clean end-to-end proof at rc=0. The classifier's fail-closed posture on off-command-position occurrences was independently adjudicated KEEP, since §2c proves the prose exemption keys on the backticks and cannot be widened silently. **The lesson, recorded because it is the whole point of the lane:** a fix for an existential-where-universal defect is itself maximally exposed to the same defect at the next scope down — file, then line, then occurrence — and the only thing that caught it was a reviewer building the chained-call mutant that neither the 20-row external matrix nor the 25 in-gate mutants contained. Revert: restore `has_flag`, drop the per-occurrence grading and the per-invocation value comparison, and restore the two positive-only stub-log greps — which returns the gate to certifying that *some* cosign call in each file is pinned, a property that is compatible with an unpinned one sitting beside it. | +| D-160 | 2026-08-23 | **UNIV-COSIGN — the cosign signer-pin gate asserted an EXISTENTIAL property where the guarantee it publishes is UNIVERSAL, so it certified nothing about a file's second `cosign verify-blob`; `hack/release/install_cosign_pin_test.sh` now grades EVERY invocation in ALL THREE published files, statically and at runtime.** Substance first, and measured before anything was written: a scratch copy of each graded file with a **second, unpinned** `cosign verify-blob` spliced IN-BODY next to its real invocation (the splice shape matters — see UC-04 below) ran the gate to **exit 0** — `hack/install.sh` rc=0, `SECURITY.md` rc=0, `hack/release/verify-artifacts.sh` rc=0, the last of these being the shape a reviewer had already demonstrated on an earlier lane. **Every individual assertion in that gate was sound.** `has_flag` grepped the whole folded extraction, so a pinned sibling satisfied it; `one_value`'s `sort -u` collapsed two agreeing values to one, so the D-153 drift comparison saw a consistent file; section 0 **printed** the extracted invocation count and asserted nothing about it; and 4b/5d's stub-log checks were positive-only greps, i.e. the same existential shape at runtime, where a second unpinned call leaves the pinned call's log line intact. The conjunction of sound existential assertions is still an existential assertion. **This is the AUD2-S05 quorum defect one layer out: not a wrong assertion, a wrong quantifier**, and it predates both AUD2-S03 and AUD2-F01. **`SECURITY.md` was worse than the other two** — it fed only the drift comparison and had **no invocation-level grading at all**, so an unpinned recipe published to adopters was invisible to the gate that exists to police the recipe. **Property chosen: "every `cosign verify-blob` invocation in every graded file carries `--certificate-oidc-issuer`, `--certificate-identity-regexp` and `--bundle`, EACH WITH SECURITY.md's published value".** The value half is not decoration: `--certificate-identity-regexp ''` carries the flag and matches every Fulcio identity ever issued, and `one_value`'s `sort -u` does not catch it either, because an empty capture is not a line and the file still reports exactly one distinct value — a presence-only universal check would be the same defect one level down, so each invocation's own extracted value is compared against the published pair (reported `WRONG-VALUE[...]`, distinct from `UNPINNED[...]`). Options considered: **(a)** the remedy recorded when the finding was filed — assert the extracted invocation count is **exactly 1** per file (**REJECTED AS FACTUALLY WRONG — do not implement it in a later lane; it would red `main` on the day it lands.** `SECURITY.md` legitimately publishes **two** — one over the archive, one over `checksums.txt`, which is what covers the SBOMs listed inside it — so that assertion reds `main` on the day it lands, and the natural repair is to weaken it again); **(b)** universal quantification over invocations **(chosen)** — strictly stronger than (a) where (a) is true, and it keeps holding when a file legitimately grows a third correctly-pinned call. **Enforcement, per D-128, is one predicate**: `pin_violations ` prints one line per problem and nothing when the file is clean, so callers grade its OUTPUT and the identical function is asserted empty against the tree and non-empty against a mutant with no `set -e` games; `assert_all_pinned` is the thin failing wrapper; `log_unpinned_lines` is its runtime twin over the stub-cosign argv log. **Classification is fail-CLOSED, which is the part that carries the guarantee.** The candidate extractor is deliberately left un-narrowed (every non-comment line mentioning `cosign verify-blob`, continuations folded), because anything the *denominator* drops is a hole. A candidate is an invocation when the folded text begins with `cosign verify-blob`; the ONE waved-through non-invocation shape is a markdown inline-code mention (`` `cosign verify-blob` ``, which is how `SECURITY.md`'s capability table names it); **anything else — `foo && cosign verify-blob …`, a here-doc line, an un-backticked prose sentence — is reported UNCLASSIFIABLE rather than skipped**, because "this gate cannot tell whether that call is pinned" must never read as "that call is fine". Accepted cost, stated rather than discovered later: a *correctly pinned* invocation written off command position also reds. That is the intended direction of error for a security gate over three files carrying four invocations in one canonical style, and the message names the fix. **Anti-vacuity, because a lane whose entire deliverable is "make a gate stricter" is maximally exposed** (this repo's #1 review finding is an assertion that cannot fail — D-124, AUD-S18): section 2b runs **eight** mutants against **each** of the three files and 2c runs a ninth, and they were chosen for **branch** coverage of the new predicate rather than for variety of shape — (a) a second **unpinned** invocation must red, name the file, quote the offending command, and produce **exactly two** violations so the pinned siblings are provably not flagged; (b) a second **correctly pinned** invocation must stay green **and** must raise the extractor's invocation count by one, without which (b)'s green could mean "the extractor never saw it"; (c) an occurrence off command position, appended **fully pinned on purpose** so the only thing that can redden it is the classifier itself; (d) every invocation deleted → `NO-CANDIDATES`; (e) the continuation fold broken → `FOLD-BROKEN`, asserted **not** to also report `UNPINNED`, because conflating "the extractor truncated this" with "the pin is missing" sends the next maintainer to the wrong file; (f) every invocation displaced off command position → `NO-INVOCATIONS`; (g) a second invocation carrying both flags with an **empty** identity regexp → `WRONG-VALUE`, the hostile shape a presence-only check waves through; (h) a second invocation carrying both flags with a **foreign OIDC issuer** → `WRONG-VALUE` on the issuer half; and 2c strips the backticks from `SECURITY.md`'s prose mention and requires the same row to fail closed, proving the exemption keys on the backticks and is not a blanket bypass. The runtime twin has its own vacuity control (an unpinned line appended to a copy of the stub log must be seen). **One real defect was caught by this section during the lane and is recorded because it is a trap for the next author**: `log_unpinned_lines` was first written with `awk -v id="identity_re=${sec_identity}"`, and **awk processes escape sequences in a `-v` assignment**, so the pin's `github\.com` arrived as `github.com` and matched nothing; the values now reach awk through `ENVIRON`. **Stated limit, same posture as D-154's**: the denominator is the literal string `cosign verify-blob`, so an invocation spelled through a variable (`"$COSIGN" verify-blob …`), built by `eval`, or assembled from fragments is invisible to this gate. Widening the trigger to bare `verify-blob` was considered and **rejected** — it buys one hypothetical no file uses, and turns any future `SECURITY.md` sentence saying "verify-blob" outside backticks into a red gate, whose repair would be to loosen the classifier. **Nothing outside the gate changed**: `hack/install.sh`, `SECURITY.md` and `hack/release/verify-artifacts.sh` are byte-unchanged, and all four of their invocations were already pinned — this row closes a hole in the *checker*, not in the checked. The stage `release-install-cosign-pin-test` was already wired into `task check` and pinned in `hack/audit/exitgate_test.sh`'s `CHECK_STAGES`, so no wiring changed either. **SECOND ROUND — the first version of this fix REPRODUCED the very defect it closes, one level down, and independent review caught it before merge.** `has_flag` grepped the whole FILE; the replacement grepped the whole LINE. Both are existential; only the scope shrank. **UC-01**: one folded line was graded as at most ONE invocation, so `cosign verify-blob --bundle a.json a && cosign verify-blob --bundle EVIL.json evil` began with `cosign verify-blob` (not UNCLASSIFIABLE), carried `--bundle` (not FOLD-BROKEN), carried both flag strings (not UNPINNED) and yielded the published values (not WRONG-VALUE) — **green**, in same-line, `;`-separated and backslash-folded forms, on all three graded files. Worse, the **full gate exited 0** for `SECURITY.md`: the two shell scripts were incidentally caught by the runtime twin (`log_unpinned_lines` at §5d), but **SECURITY.md is a document and has no runtime twin**, so the hole was unmitigated precisely on the file this row calls "the copy-paste recipe adopters run by hand" — D-153's exact incident class — while the gate printed "EVERY cosign verify-blob invocation ... is pinned", false as printed. The stated-limit paragraph did not cover it: it enumerated `$COSIGN`, `eval` and fragments, not `&&` chaining, and **leading** `&&` was explicitly handled (mutant (c) → UNCLASSIFIABLE), so the operator had been considered and only one side handled. Closed by grading per **OCCURRENCE** (`occurrence_count` + a new `MULTI-OCCURRENCE` violation that fails closed on any line carrying two calls) rather than per line; counting inside an already-triggered line uses the shorter `verify-blob`, so a second call spelled `cosign verify-blob` or `"$COSIGN" verify-blob` and chained onto a pinned one is caught too, which the literal file-level trigger would miss. **UC-02**: `extract_issuer`/`extract_identity` anchor on a greedy `.*`, so the LAST value on a line wins — a hostile `--certificate-identity-regexp ''` placed FIRST was masked by a correct value placed second, **the extraction direction favoured the attacker**. Closed by `flag_value_tokens`, which returns EVERY value of every flag on the occurrence; each must equal the published one, so a repeated flag with an empty value first now reds. **UC-03 (P2, the erosion path)**: a CORRECTLY pinned call written with **double quotes** was refused as `WRONG-VALUE ... identity= ... (an empty regexp matches every Fulcio identity)` — a true refusal with a **false reason**, and the repair a maintainer reaches for on that message is widening the extractor. Both quote styles are now accepted (double quotes are correct shell for this value: it contains no `$` and no backtick), and a **bare** value is diagnosed as `UNQUOTED-VALUE`, a QUOTING defect, never as a wrong or empty one — a gate that misdiagnoses erodes faster than one that refuses. **UC-04**: this row's "rc=0, rc=0, rc=0" reproduction figure is **splice-shape-sensitive** and is stated as measured: it holds for a second unpinned call spliced **in-body** next to the real one. An EOF-appended mutant reds the two shell scripts for an unrelated runtime reason, so the figure should not be read as holding for any second unpinned call. The same sensitivity is why the UC-03 double-quoted mutant reds the two scripts through the full gate (the spliced call actually RUNS and its fixture bundle is absent) while `SECURITY.md`, having no runtime, is the clean end-to-end proof at rc=0. The classifier's fail-closed posture on off-command-position occurrences was independently adjudicated KEEP, since §2c proves the prose exemption keys on the backticks and cannot be widened silently. **The lesson, recorded because it is the whole point of the lane:** a fix for an existential-where-universal defect is itself maximally exposed to the same defect at the next scope down — file, then line, then occurrence — and the only thing that caught it was a reviewer building the chained-call mutant that neither the 20-row external matrix nor the 25 in-gate mutants contained. **THIRD ROUND (UC-05..UC-09), and the reason this row now reads the way it does.** **UC-05**: `occurrence_count` compared whitespace-delimited fields to `verify-blob`, found one, and concluded **singularity** — when all it had established is that it did not find a second. `cosign "verify-blob"`, `cosign 'verify-blob'` and `cosign verify-blob""` are the same command to the shell, and each hid a chained unpinned call from the count. Measured against the round-2 gate on **all three** files at whole-gate level: **rc=0, rc=0, rc=0** — worse than first reported, because `A && B` short-circuits and `set -e` does **not** fire on a non-final member of an AND-list, so even the two shell scripts' runtime twin missed it. Closed by stripping shell quotes before the field compare, which is **a spelling patch, not a terminator, and is labelled as one in the code**. A structural terminator was sought and **ruled out with evidence**: refusing any graded line carrying a command separator would red the REAL files, since `hack/install.sh` and `hack/release/verify-artifacts.sh` both legitimately end their genuine invocation with an or-else `die` tail. **No structural terminator exists for this gate**, so completeness is not available and must not be claimed. **UC-07 is therefore the durable fix, and it is a change of posture rather than of logic.** The `PASS:` banner was printed unconditionally and asserted "EVERY cosign verify-blob OCCURRENCE ... is pinned" plus "a second unpinned call reddens whether it sits on its own line or is chained onto a pinned one" — a **universal claim bound to no assertion**. Under UC-05 that banner did not merely overstate: on a green run it printed something **false**, which is strictly worse than printing nothing, and it is this repo's #1 defect class (an assertion that cannot fail) wearing a different hat. The banner now reports **OBSERVED** counts per file (occurrences found, classified-and-graded, prose-exempt, refused), lists **ASSERTED** properties each of which is shown to fail on a mutant, and states the **NOT ASSERTED** residual in the same breath: this gate finds calls by a literal string and counts quote-stripped words, so a call spelled through a variable, `eval`, or fragments is not seen and not graded, and the counts are what was classified — **not a proof that nothing else exists**. When a fifth spelling turns up, the gate is then **incomplete rather than wrong**, and incomplete is recoverable. **UC-06**: a TRAILING comment mentioning `verify-blob` fired `MULTI-OCCURRENCE: … has 2 verify-blob calls chained on ONE line` — fail-closed but **false as printed**, since `cosign_candidates` only drops lines whose FIRST non-space character is `#`. That is the UC-03 misdiagnosis shape recurring **inside the UC-01 fix**. The message now says TOKENS, names both possible causes, and names the correct repair; excluding trailing comments was rejected as it needs quote-aware parsing, which is the machinery that produced UC-01/02/03. **UC-08**: `shellcheck` SC1087 ×2 (error severity) on `flag_value_tokens` — `"$flag[[:space:]]…"` parses as an array subscript; `${flag}` silences it. Cosmetic: no shellcheck gate exists in this repo. **UC-09**: two stage-count figures reported during this lane ("25", then "28") were **both wrong** and neither came from a committed file — they counted `task: [` lines in a run LOG, which includes nested task invocations. Measured: the Taskfile `check:` block has **21** `- task:` entries and `CHECK_STAGES` has **21** stage names; they agree, and both files are byte-identical to `origin/main`. There is no stage-count mismatch and this lane could not have caused one. **THE PATTERN, recorded because it is the lane's most transferable output:** four P1s, three of them the same scope error at successively finer scopes — file (`has_flag`), line (round 1), then occurrence-spelling (round 2) — each found by review and none by the author's own mutant matrix, because each matrix was built from the shape the previous round had just learned. The general lesson is not "add another spelling": it is that **when a gate's denominator cannot be made provably complete, the gate must report what it classified instead of asserting what exists.** That is now enforced where it is hardest to ignore, in the banner the gate prints on every green run. Revert: restore `has_flag`, drop the per-occurrence grading and the per-invocation value comparison, and restore the two positive-only stub-log greps — which returns the gate to certifying that *some* cosign call in each file is pinned, a property that is compatible with an unpinned one sitting beside it. | diff --git a/hack/release/install_cosign_pin_test.sh b/hack/release/install_cosign_pin_test.sh index 0456af4..06bf4c9 100755 --- a/hack/release/install_cosign_pin_test.sh +++ b/hack/release/install_cosign_pin_test.sh @@ -215,10 +215,34 @@ occurrence_count() { # whole UC-01 fix, so the repair a maintainer would reach for is loosening this # very function. awk's default field splitting also folds runs of whitespace, so # `cosign verify-blob` and `"$COSIGN" verify-blob` still count as occurrences. + # + # UC-05: SHELL QUOTES ARE STRIPPED BEFORE THE COMPARE. A bare field compare finds + # one whole-word token and concludes SINGULARITY, when all it established is that + # it did not find a second one — absence of evidence read as evidence of absence. + # `cosign "verify-blob"`, `cosign 'verify-blob'` and `cosign verify-blob""` are + # all the same command to the shell, and each hid a chained unpinned call from + # the count. Measured: without the strip, all three returned 1 and the full gate + # exited 0 on SECURITY.md. + # + # This is a SPELLING PATCH, not a terminator, and it is labelled as one on + # purpose. It closes three known spellings; it does not prove a fourth does not + # exist. A structural terminator was considered and ruled out with evidence: + # refusing any graded line that carries a command separator would red the REAL + # files, because hack/install.sh and hack/release/verify-artifacts.sh both end + # their genuine invocation with `|| die "cosign verification failed…"`. Since the + # count cannot be made complete, the PASS banner is written to report what was + # classified rather than to claim that nothing else exists (UC-07). + # # Residual, stated: a bundle named exactly `verify-blob` (no extension) counts as # an occurrence and fails closed. No file does that, and closed is the safe way # to be wrong. - printf '%s' "$1" | awk '{ for (i = 1; i <= NF; i++) if ($i == "verify-blob") n++ } END { print n + 0 }' + printf '%s' "$1" | awk '{ + for (i = 1; i <= NF; i++) { + tok = $i + gsub(/["\047]/, "", tok) + if (tok == "verify-blob") n++ + } + } END { print n + 0 }' } # flag_value_tokens — reads one folded line on stdin and prints the RAW @@ -231,8 +255,8 @@ occurrence_count() { # attacker. Here every value is returned and every one has to match. flag_value_tokens() { local flag="$1" - grep -oE -- "$flag[[:space:]]+('[^']*'|\"[^\"]*\"|[^[:space:]]+)" \ - | sed -E "s/^$flag[[:space:]]+//" || true + grep -oE -- "${flag}[[:space:]]+('[^']*'|\"[^\"]*\"|[^[:space:]]+)" \ + | sed -E "s/^${flag}[[:space:]]+//" || true } # unquote — prints "quotedvalue" or "barevalue". @@ -328,7 +352,13 @@ pin_violations() { n_occ="$(occurrence_count "$line")" if [[ "$n_occ" -gt 1 ]]; then n_inv=$((n_inv + n_occ)) - printf 'MULTI-OCCURRENCE: %s has %s `verify-blob` calls chained on ONE line, and this gate grades a line as one invocation — so a pinned first call would vouch for an unpinned second. Put each cosign call on its own line: %s\n' "$rel" "$n_occ" "$line" + # UC-06: say TOKENS, not "calls chained". cosign_candidates only drops a line + # whose FIRST non-space character is `#`, so a TRAILING comment mentioning + # verify-blob lands here too. Refusing it is right (this gate cannot grade a + # line it cannot resolve to one call); describing it as a chained call is not, + # and a message that misdiagnoses is what gets the counter loosened — the + # UC-03 failure recurring inside the UC-01 fix. + printf 'MULTI-OCCURRENCE: %s has %s `verify-blob` TOKENS on ONE line, and this gate grades a line as exactly one invocation, so it refuses rather than guess which one to grade — a pinned first call must not vouch for an unpinned second. Cause is either a second call chained onto this one, or `verify-blob` appearing in a TRAILING COMMENT on this line. Put each cosign call on its own line, and keep `verify-blob` out of trailing comments there: %s\n' "$rel" "$n_occ" "$line" continue fi n_inv=$((n_inv + 1)) @@ -684,7 +714,7 @@ for target in "${GRADED[@]}"; do # the second call spelled so the literal trigger would miss it. occurrence_count # deliberately counts the shorter 'verify-blob' INSIDE an already-triggered # line, so these are seen even though the file-level trigger would not match. - for spelling in '"$COSIGN" verify-blob' 'cosign verify-blob'; do + for spelling in '"$COSIGN" verify-blob' 'cosign verify-blob' 'cosign "verify-blob"' "cosign 'verify-blob'" 'cosign verify-blob""'; do m="$WORK/univ.${label}.chained-spelling-$(printf '%s' "$spelling" | od -An -tx1 | tr -d ' \n')" append_raw "$src" "$m" "cosign verify-blob $PINS_OK --bundle $PROBE_BUNDLE $PROBE_ARTIFACT && $spelling --bundle evil-$PROBE_BUNDLE evil-$PROBE_ARTIFACT" v="$(pin_violations "$m")" @@ -1245,4 +1275,50 @@ grep -qE "^[[:space:]]+${STAGE}\$" "$AUDIT_GATE" \ || fail "'$STAGE' is not in CHECK_STAGES in hack/audit/exitgate_test.sh — the release exit gate would not grade it (AUD-S18)" echo "OK: $STAGE is pinned in CHECK_STAGES" -echo "PASS: install_cosign_pin_test.sh — SEC-03 closed on BOTH paths (REQ-AUD2-S03-01..05 + AUD2-F01 + UNIV-COSIGN/D-160 + UC-01..UC-03): EVERY cosign verify-blob OCCURRENCE in hack/install.sh, SECURITY.md and hack/release/verify-artifacts.sh pins issuer=${inst_issuer} identity=${inst_identity}, byte-identical across the three, with EVERY value of every flag compared (not just the last on a line); a second unpinned call reddens whether it sits on its own line or is chained onto a pinned one with && / ; / |, and a second correctly-pinned one does not; a foreign-signed bundle fails closed with nothing installed and fails the maintainer check too; all four pins proved load-bearing by mutation; the gate is wired into task check" +# ------------------------------------------------------ 7. the PASS banner -- +# +# UC-07 — THE BANNER STATES ONLY WHAT WAS ASSERTED, AND REPORTS WHAT WAS SEEN. +# +# The previous banner was printed unconditionally and asserted "EVERY cosign +# verify-blob OCCURRENCE ... is pinned" plus "a second unpinned call reddens +# whether it sits on its own line or is chained onto a pinned one" — a UNIVERSAL +# claim bound to NO assertion. When UC-05's quoted spelling slipped past the +# occurrence count, that banner did not merely overstate: it printed something +# FALSE, on a green run, which is strictly worse than printing nothing. This +# repo's #1 defect class is an assertion that cannot fail; a claim that is not +# bound to an assertion is the same defect wearing a different hat. +# +# So the claim is now bound to the evidence and the residual travels in the same +# breath as the claim. Four rounds of review on this one gate have each found a +# spelling or a scope the previous round did not cover; the honest posture is that +# a fifth exists and has not been found yet. A gate that says "I classified and +# graded 4 occurrences, I refuse to guess about anything I could not classify, and +# here is what I cannot see at all" stays TRUE when that fifth spelling turns up. +# It is then INCOMPLETE rather than WRONG, and incomplete is recoverable. +# +# The counts below are exact at this point in the run: reaching here means +# pin_violations was EMPTY for all three files, so there were no MULTI-OCCURRENCE +# and no UNCLASSIFIABLE candidates, and therefore candidates = graded + prose. +echo "PASS: install_cosign_pin_test.sh — REQ-AUD2-S03-01..05 + AUD2-F01 + UNIV-COSIGN (D-160, UC-01..UC-08)" +echo " OBSERVED (counts, not proofs of absence):" +for target in "${GRADED[@]}"; do + label="${target%%:*}" + n_c="$(grep -c . <"$WORK/cand.$label" | tr -d ' ')" + n_i="$(grep -c . <"$WORK/inv.$label" | tr -d ' ')" + echo " ${label}: ${n_c} \`cosign verify-blob\` occurrence(s) found — ${n_i} classified as invocations and GRADED, $((n_c - n_i)) exempted as backticked prose, 0 refused as unclassifiable" +done +echo " ASSERTED, and each shown to FAIL on a mutant carrying the defect it exists to catch:" +echo " * every GRADED occurrence carries --certificate-oidc-issuer, --certificate-identity-regexp and --bundle," +echo " with EVERY value it supplies for those flags equal to SECURITY.md's published pair" +echo " (issuer=${inst_issuer}, identity=${inst_identity}) — not merely the last value on the line;" +echo " * hack/install.sh, SECURITY.md and hack/release/verify-artifacts.sh publish that pair byte-identically;" +echo " * the pinned regexp accepts all ${#REAL_SANS_ACCEPT[@]} REAL published release identities and rejects all ${#REAL_SANS_REJECT[@]} negatives;" +echo " * a foreign-signed bundle fails closed on the adopter path with nothing installed, and fails the maintainer path too;" +echo " * on the mutants section 2b builds, a second UNPINNED call reddens both on its own line and chained onto a" +echo " pinned one with && / ; / | (in the spellings 2b enumerates), while a second CORRECTLY pinned call does not." +echo " NOT ASSERTED — the residual, stated here rather than somewhere a reader will not look:" +echo " This gate finds calls by the literal string 'cosign verify-blob' and counts them as whitespace-delimited" +echo " words with shell quotes stripped. A call spelled through a variable, built by eval, or assembled from" +echo " fragments is NOT SEEN and therefore NOT GRADED. The counts above are what was classified — they are NOT" +echo " a proof that no other invocation exists in these files. Any line carrying more than one verify-blob token" +echo " is REFUSED (MULTI-OCCURRENCE), never graded on its first call." diff --git a/openspec/specs/backlog.md b/openspec/specs/backlog.md index fc8b5f5..5d6a39e 100644 --- a/openspec/specs/backlog.md +++ b/openspec/specs/backlog.md @@ -753,7 +753,7 @@ that claim). | ORPHAN | **DONE (D-159)** — `Taskfile.yml`'s `release-verify-test`, the only test of `hack/release/verify-artifacts.sh` (the procedure **`SECURITY.md:61` publishes to release consumers**), was invoked by nothing: absent from `check:`, from `CHECK_STAGES`, and from every workflow — D-124's "a gate invoked by nothing is not a gate", one epic on from AUD2-F01's published-instructions-rot finding. It was **green**, so the defect was wiring only. Now the 14th of 21 `check:` stages, in its three **offline** modes (`negative`, `cosign-skip-when-absent`, `readme` = REQ-E9-S12-02/03/04); the `all` default is deliberately NOT wired — it shells out to `task release-snapshot`, i.e. a networked `go install goreleaser`, a `go mod tidy` before-hook that rewrites tracked files mid-check, and `--clean` on `dist/`. **Not a gap to fill: REQ-E9-S12-01 (snapshot → verify round trip) is already automated** — `hack/release/exitgate_test.sh:33-34` runs exactly `task release-snapshot` then `task release-verify`, the spec's own `Verify:` string, in the `release-exitgate` job. It is push-only (`if: github.event_name != 'pull_request'`), so the exposure is **RELSE-08 visibility, not absence**; do NOT open a lane to build a gate that exists. `CHECK_STAGES` 20 → 21 in the same commit; body pinned **per mode** so dropping two modes or reverting to the bare default reds | **[autonomous]** | — | not owned by any in-flight lane; `Taskfile.yml` + `hack/audit/exitgate_test.sh` are the one `CHECK_STAGES` slot, which only one lane may hold at a time | | CI-TOOLCHAIN-F01 | The linter/toolchain coupling has **no early detector**: dependabot's `github-actions` ecosystem updates `uses:` refs, not `env:` literals, so `GOLANGCI_LINT_VERSION` rots silently until the next Go minor reds every PR at once (~6-monthly). Candidate: a text gate comparing the pinned linter release's go.mod `go 1.N` directive against the toolchain CI resolves, or an updater that watches the literal | **[autonomous]** | D-158 | deliberately out of scope of the fix lane: three lanes were parked behind it, and a new gate belongs with `hack/lint/**`, which was owned by a concurrent lane | | BASH32-F01 | **DONE** — three `hack/**` gate scripts used bash 4+ features with no version guard; under stock macOS `/bin/bash` 3.2 `hack/docs/truthlag_pins_test.sh` died at its `declare -A`, skipped its final `OK:` banner and **exited 0**, so `task docs-gates` (and `task check`) read a gate that certified almost nothing as green. Fixed by a shared, per-script-parameterised `hack/lib/require-bash.sh` floor (4.0 / 4.0 / 4.4), enforced by a new `hack/lint/bash_version_guard_test.sh` wired as `task check` stage 20 (D-154) | **[autonomous]** | — | found *by* the AUD2 wave's macOS runs, not by any audit: CI is ubuntu/bash 5, so the hole is LOCAL-only and no CI lane could have surfaced it | -| UNIV-COSIGN | **DONE (D-160)** — `hack/release/install_cosign_pin_test.sh` graded the D-153 signer pin **existentially** ("*some* `cosign verify-blob` in this file is pinned") where the published guarantee is **universal**, so a **second, unpinned** invocation passed: measured before the fix on scratch copies of all three graded files, rc=**0**/**0**/**0**. `has_flag` grepped the whole folded extraction so a pinned sibling satisfied it, `one_value`'s `sort -u` collapsed the agreeing values, §0 printed the invocation count without asserting it, and 4b/5d's stub-log greps were positive-only — the same shape at runtime. `SECURITY.md` had **no invocation-level grading at all**, only the drift comparison. Closed by one predicate (`pin_violations`) applied to **every** invocation in **all three** files plus its runtime twin, with fail-CLOSED classification of anything it cannot place, mutation-proven by eight mutants per file chosen for **branch** coverage (second-unpinned / second-pinned / off-command-position / no-candidates / fold-broken / no-invocations / empty-identity-regexp / foreign-issuer) plus a prose-exemption control. The check compares each invocation's **value** against SECURITY.md's published pair, not just flag presence: `--certificate-identity-regexp ''` carries the flag, matches every Fulcio identity, and slips past `one_value`'s `sort -u` because an empty capture is not a line. **CORRECTION TO THE RECORDED REMEDY — do not implement it:** the filed remedy "assert the extracted invocation count is exactly 1 per graded file" is **factually wrong and would red `main` on landing**, because `SECURITY.md` legitimately publishes **two** invocations (`SECURITY.md:86` over the archive and `:93` over `checksums.txt`, which is what covers the SBOMs listed inside it). The property is universal, not a count. **Second round (UC-01..UC-04), caught by independent review:** the first fix reproduced the same existential defect one scope down — per **line** instead of per **file** — so an unpinned call CHAINED onto a pinned one (`&&`, `;`, a pipe, or backslash-folded) passed, and the **full gate exited 0** on `SECURITY.md`, which has no runtime twin. Closed by per-**occurrence** grading (`MULTI-OCCURRENCE`), by comparing **every** value of every flag rather than the greedy-last (an empty regexp placed first was masked by a correct one placed second), and by diagnosing quote style separately (`UNQUOTED-VALUE`) so a correctly pinned double-quoted call is accepted instead of being refused with a false "empty regexp" reason | **[autonomous]** | AUD2-F01, D-153 (the pinned value) | demonstrated by a reviewer *on* the AUD2-F01 lane and out of its scope — F01 added a third graded file to a gate whose quantifier was already wrong, so fixing the quantifier is a change to the checker, not to any checked file (all three are byte-unchanged) | +| UNIV-COSIGN | **DONE (D-160)** — `hack/release/install_cosign_pin_test.sh` graded the D-153 signer pin **existentially** ("*some* `cosign verify-blob` in this file is pinned") where the published guarantee is **universal**, so a **second, unpinned** invocation passed: measured before the fix on scratch copies of all three graded files, rc=**0**/**0**/**0**. `has_flag` grepped the whole folded extraction so a pinned sibling satisfied it, `one_value`'s `sort -u` collapsed the agreeing values, §0 printed the invocation count without asserting it, and 4b/5d's stub-log greps were positive-only — the same shape at runtime. `SECURITY.md` had **no invocation-level grading at all**, only the drift comparison. Closed by one predicate (`pin_violations`) applied to **every** invocation in **all three** files plus its runtime twin, with fail-CLOSED classification of anything it cannot place, mutation-proven by eight mutants per file chosen for **branch** coverage (second-unpinned / second-pinned / off-command-position / no-candidates / fold-broken / no-invocations / empty-identity-regexp / foreign-issuer) plus a prose-exemption control. The check compares each invocation's **value** against SECURITY.md's published pair, not just flag presence: `--certificate-identity-regexp ''` carries the flag, matches every Fulcio identity, and slips past `one_value`'s `sort -u` because an empty capture is not a line. **CORRECTION TO THE RECORDED REMEDY — do not implement it:** the filed remedy "assert the extracted invocation count is exactly 1 per graded file" is **factually wrong and would red `main` on landing**, because `SECURITY.md` legitimately publishes **two** invocations (`SECURITY.md:86` over the archive and `:93` over `checksums.txt`, which is what covers the SBOMs listed inside it). The property is universal, not a count. **Second round (UC-01..UC-04), caught by independent review:** the first fix reproduced the same existential defect one scope down — per **line** instead of per **file** — so an unpinned call CHAINED onto a pinned one (`&&`, `;`, a pipe, or backslash-folded) passed, and the **full gate exited 0** on `SECURITY.md`, which has no runtime twin. Closed by per-**occurrence** grading (`MULTI-OCCURRENCE`), by comparing **every** value of every flag rather than the greedy-last (an empty regexp placed first was masked by a correct one placed second), and by diagnosing quote style separately (`UNQUOTED-VALUE`) so a correctly pinned double-quoted call is accepted instead of being refused with a false "empty regexp" reason. **Third round (UC-05..UC-09):** `occurrence_count` read *absence of a second token* as *proof of singularity*, so `cosign "verify-blob"` / `cosign 'verify-blob'` / `cosign verify-blob""` hid a chained unpinned call — **rc=0 on all three files at whole-gate level** against the round-2 gate (`A && B` short-circuits, so `set -e` never fires and even the runtime twin missed it). Fixed by stripping shell quotes before the compare, **explicitly a spelling patch, not a terminator**: a structural terminator was ruled out with evidence, because both scripts legitimately end their real invocation with an or-else `die` tail, so separator-based refusal would red the real files. Since completeness is unavailable, **the `PASS:` banner no longer claims it** — it now reports OBSERVED counts per file, lists only ASSERTED properties (each mutation-proven), and states the NOT-ASSERTED residual in the same breath, so an unknown fifth spelling leaves the gate *incomplete* rather than *wrong*. Also: MULTI-OCCURRENCE now says TOKENS and names trailing comments as a cause (it was false as printed), and SC1087 silenced | **[autonomous]** | AUD2-F01, D-153 (the pinned value) | demonstrated by a reviewer *on* the AUD2-F01 lane and out of its scope — F01 added a third graded file to a gate whose quantifier was already wrong, so fixing the quantifier is a change to the checker, not to any checked file (all three are byte-unchanged) | Sizing, from the S03 implementer's reading of the call site: `verify_cosign()` (`hack/release/verify-artifacts.sh:118–125`) has the byte-identical unpinned From 7757ab3e1c322622c5684acca99deeed580f88d2 Mon Sep 17 00:00:00 2001 From: Konrad Heimel Date: Sun, 23 Aug 2026 23:22:06 +0200 Subject: [PATCH 4/4] :memo: docs(release): correct the residual the gate documents (R3-01) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit TEXT ONLY. Zero non-comment, non-echo lines changed: no predicate, no occurrence_count, no exemption logic, no parsing added. R3-01 (P1). The paragraph 68f7b9d added to make the gate honest contained a sentence that is false: "Any line carrying more than one verify-blob token is REFUSED (MULTI-OCCURRENCE), never graded on its first call." A candidate line that is NOT at command position but contains the backtick-delimited `cosign verify-blob` span is exempted BEFORE occurrence_count runs, so the refusal never reaches it. Measured, spliced into SECURITY.md:57: See `cosign verify-blob`: cosign verify-blob --bundle A.json a && cosign verify-blob --bundle EVIL.json evil occurrence_count = 2 by the definition the banner states two sentences earlier; pin_violations EMPTY; whole gate rc=0 — while printing that sentence, and while reporting the line among those "exempted as backticked prose" when one of the two is a live command. That last part is the UC-06 "false as printed" species this lane itself grades as a defect. Four corrections, at every site that carried the claim: 1. The refusal sentence is scoped to lines AT COMMAND POSITION, and says explicitly that it does not reach a line exempted under residual (1). 2. The exemption is disclosed as residual (1), ahead of the variable/eval/ fragment spellings, because it is the residual that is actually REACHABLE: it keys on the backtick-delimited substring occurring ANYWHERE on the line, not on the line being prose. The unreachable spellings are demoted to (2), with the "not present in these files today" claim verified by grep. 3. OBSERVED no longer calls an exempted line "prose". The branch a line took is a fact; "prose" was an inference, and R3-01 is where that inference is wrong. It now reads "NOT GRADED (exempted because the line contains a backticked mention; such a line may still carry live calls)". 4. The same falsified claim is corrected in the D-160 row, in pin_violations' own header comment, and in the 2c framing comment — 2c grades the backticks-vs-words axis only, and now says so instead of claiming the hatch is narrow outright. Narrowing the exemption is NOT attempted: it needs quote- and markdown-aware parsing, the machinery that produced UC-01/02/03. One claim in my own new text was caught and corrected before commit: "reproduced in a shell script too" was ambiguous enough to read as whole-gate rc=0. Measured both ways — the STATIC defect does reproduce there (candidates=2, invocations=1, pin_violations empty), but the whole gate reds at 4b for an unrelated runtime reason, so the end-to-end green is specific to the document, which has no runtime twin. D-160 now states both halves. --- CHANGELOG.md | 1 + docs/decisions/decisions.md | 2 +- hack/release/install_cosign_pin_test.sh | 60 ++++++++++++++++++------- openspec/specs/backlog.md | 2 +- 4 files changed, 47 insertions(+), 18 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index f608fa0..e638c8d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -93,6 +93,7 @@ repository still gets a decision, never by following the link; no release carrie - :memo: docs(e11): Shape D rests on no-recursion alone — the decode barrier was false (F-01) - :memo: docs(e11): delete the false cost claim; reason 1 carries Shape D alone (F3-01) - :memo: docs(ci): D-159 recorded a residual that does not exist (ORPH-01..04) +- :memo: docs(release): correct the residual the gate documents (R3-01) ### Features - :sparkles: feat(audit): measure REL-03/REL-07 by real mutation run, not by name diff --git a/docs/decisions/decisions.md b/docs/decisions/decisions.md index 4de25c4..8d6de3b 100644 --- a/docs/decisions/decisions.md +++ b/docs/decisions/decisions.md @@ -162,4 +162,4 @@ project/process decisions. | D-156 | 2026-08-23 | **The tier-1 (CEL) ceiling is recorded (`docs/planning/rego-tier-ceiling.md`, E11-S01 / REQ-E11-S01-01+02) and it NARROWS E11: two of the four named shapes are struck outright and a third in part.** Substance first: of multi-pass / cross-manifest / set-difference / graph-relationship (`openspec/specs/later-phases.md:284`), **cross-manifest and set-difference are struck, the "named intermediate" half of multi-pass is struck, and only fold/aggregate-over-a-collection and in-input graph reasoning survive as justification for a second backend.** Measured against the surface this repo actually binds — `internal/core/aggregate/evaluate.go` `newEvalEnv`, eleven frozen predicate-scope variables, **zero extension libraries** — reproduced in a nested throwaway module pinned to the repo's `cel-go v0.31.0` (root `go.mod`/`go.sum` byte-unchanged; nothing added to the dependency graph, which judgment call (d) has not authorised). **What exceeds tier 1: (1) folds.** `sum`, `reduce`, `math.*` and `lists.*` are all `undeclared reference`; `size()` is the only aggregate in the surface, so a rule counting matched changes is expressible and a rule summing a numeric delta across them is not. **(2) Graph reasoning** — the iteration count of a CEL expression cannot be made data-dependent, so depth is syntactic and **unbounded** reachability has no spelling; a bounded `k`-hop form *is* writable and answers a fixed-depth question, not the rule (detailed below, with the refutations of two sharper claims this row previously made). **What is struck, with the CEL that does the job:** registry membership — `string(new) in facts.registry.topics.value` over a `cardinality: set` fact, already shipped green at `examples/packs/service-catalog/.assent/packs/catalog/rules/ownership.yaml:21`; keyed attribute lookup — either a purpose-built provider (`builtin/resource-owner`, exercised in both polarities by `examples/archetypes/referenced-resource-ownership/`) or `facts.

..value[key].field`, which compiles and is lint-clean because `internal/lint/facts_ref.go`'s D-051 shape check permits arbitrary navigation past `.value` and only forbids indexing `facts` itself; set difference — `oldEntry.acls.filter(a, !(a in entry.acls)).size() == 0`; named intermediates — no `cel.bind`, but re-deriving the sub-expression inside each leaf is semantically identical and compiles. **The sharpest finding is a distinction, not a rule:** same-changeset **cross-file** reasoning fails for **input availability**, not expressiveness — the evaluation unit is one file (`change.ChangeSet` is documented "for one file", `internal/change/diff.go:129`; `assent run` strips one `--subject file:`, `cmd/assent/run.go:266`, and diffs it alone, `:293`) and **REQ-E11-S05-01 pins the Rego module to the identical `EvaluationInput`** with the tier fenced to "declared data, no I/O". **A Rego module therefore fails that rule identically, so it is struck from E11's justification too** — the fix is an input decision, which E11's non-goals fence, not a backend decision. Corroborating: the one committed illustration of the escape hatch, `examples/policies/rego/bounded_change.rego`, is **entirely tier-1 expressible** — both `violations` rules are per-change predicates and `examples/policies/declarative/bounded-change.yaml` is the same rule already in the envelope. **The strongest single piece of evidence, and the one that sizes the epic, is the graph shape.** On the `assent run` path document-mode `walkNode` emits a Change **only where two scalars differ** — a sequence on either side makes the whole ChangeSet **opaque → REVIEW** before any rule runs (`internal/change/diff.go`) — and collection-mode `DiffEntries` is reached only from `internal/adoptertest`, so `old`/`new`/`entry`/`oldEntry` and every `changes[i].old`/`.new` bind **scalars**. That does **not** starve a graph rule, because a flat `set` fact still carries structure: `edges: {type: string, cardinality: set}` returning `["orders|billing","billing|ledger"]` is a **fully declarable, in-contract adjacency inside `EvaluationInput` today** — the declaration is legal (`schemas/provider/v1alpha1/response.schema.json`), `fact.value` carries no JSON-Schema type constraint and `ResolveFactsChecked` cross-checks the *declaration* not the value (`internal/provider/resolve.go`), outputs are operator-authored (`internal/provider/config.go`), the `http` transport is live on the plain run path with **no `--checkout`** (`cmd/assent/provider_host.go` `providerCallFor`), and a set fact binds as a CEL list. Tier-1 CEL nonetheless cannot answer the actual question over it: **CEL has no recursion, fixpoint, fold or user-defined function, so unbounded reachability has no spelling** (`transitiveClosure` → `undeclared reference`; the four comprehension macros iterate one level and cannot call themselves). **Stated precisely, because two drafts of this record overreached and both were caught by independent review:** a *bounded* `k`-hop check **is** expressible and does **not** need the string decomposition CEL lacks — over a finite in-input candidate set (a `nodes` set fact, the same construction as `edges`), decode is replaceable by **encode-and-compare**: `nodes.value.exists(m, nodes.value.exists(n, (string(new)+"|"+m) in edges.value && (m+"|"+n) in edges.value && (n+"|"+string(new)) in edges.value))` compiles **and evaluates** under the real `cel.CostLimit(1_000_000)` to `true/true/true/false` over the fixture above, and `nodes.value.filter(m, (string(new)+"|"+m) in edges.value)` recovers an edge's far end as `[billing]`. Both primitives (`+` on strings, `in`) were already in this record's own function census, so the claim that decoding was a second independent barrier was internally inconsistent as well as false. **The real ceiling is `k`, and a third draft got its cost wrong too** — it claimed `O(|N|^(k-1)·|E|)` "exhausts the cost budget on any real graph". Wrong complexity class and wrong conclusion, because the census had omitted the surface's only value binder, `[expr].all(v, …)`: binding each BFS frontier once per level makes cost additive across levels, and measured under the real `cel.CostLimit(1_000_000)` a ring `|N|=50, deg 5` costs 89,551 at `k=10`, 235,297 at `k=20` and 686,317 at `k=50` — roughly linear in `k`, and at `k=50 ≥ |N|` CEL is **not approximating at all, it decides reachability exactly**, in 69% of budget. The practical `k` collapses around `|N|≈200` (`k=10` at 46% of budget, `k=20` exceeds). Recorded because a reader sizing this epic is entitled to ask "would CEL suffice for *our* graph?" and the previous sentence foreclosed that question with an assertion measurement refutes; it is **not** offered as a second reason. **What carries the verdict is one property, now measured rather than recalled: the iteration count of a tier-1 CEL expression cannot be made data-dependent.** `reduce`, `transformList`, `transformMap`, two-var `all(i,x,…)`, `range`/`lists.range` and `cel.bind` are all `undeclared reference`; `for` is a `reserved identifier`; there is no fold, self-reference or generator; so depth is a **syntactic** property, hard-capped by cel-go's parser recursion limit of 250 (`expression recursion limit exceeded: 250` at depth 260, depth 200 still compiles). That a fixed `k` really is an approximation when the data outruns it is measured too: on a 4-cycle the `k=3` form evaluates `false` and the `k=4` form `true`. **Rego answers the unbounded question with `graph.reachable` — pure and deterministic — and that single gap is the whole justification.** **An input that is in contract and available today, over which CEL can only approximate and Rego decides, is exactly the per-rule evidence D-017's gate demanded — so E11 has TWO unconditional justifications (folds and graphs), neither waiting on any open question.** Deliverability caveat, stated because this row makes the same distinction for sub-shape B1: **no provider in the corpus ships an encoded adjacency today** — that one *can* follows from the provider contract, the same inference used to strike B1, not from a shipped example. Options considered: **(a)** record all four shapes as exceeding, the reading D-141's unlock invites (rejected — three are demonstrably expressible and an unfalsifiable ceiling claim is the defect this story exists to prevent); **(b)** strike set-difference **conditionally**, so that a narrowing answer to OQ-35 would return it to the ceiling (rejected on the second pass — both resolutions strike it: extending the entry binding makes CEL express it, narrowing makes it an input-availability failure that REQ-E11-S05-01 hands to Rego unchanged, so a conditional would have left a downstream story waiting on an answer that cannot change the verdict); **(c)** strike cross-manifest and set-difference **unconditionally**, strike half of multi-pass, keep folds and in-input graphs **both unconditionally** **(chosen)**. **Two rejected drafts are recorded because the same failure produced both, with the sign flipped, and only independent review caught either.** Draft 1 made the graph shape *contingent* on OQ-35/OQ-36 on the premise that "an adjacency needs a mapping-valued fact" — it does not; a set of encoded strings carries one inside the frozen declaration — which came from conflating a *provider-supplied catalog* (sub-shapes B1/B2, struck here as working and shipped) with **B3, which is specifically same-changeset cross-file *diffs***. It would have advised the operator to defer a 14-story epic on a premise that does not hold. Draft 2 replaced that with a second "independent reason" — that CEL cannot decode an edge, killing even a bounded two-hop check — **refuted by execution** (the encode-and-compare leaf above). Draft 3 replaced *that* with the exponential-cost claim above — **refuted by measurement**. The common cause across all three is one habit: **reaching for a second independent reason when one sufficient reason was already in hand**, and then applying an **asymmetric evidentiary standard** to protect it — accepting awkward-but-working spellings when they *struck* a shape (A2's re-derivation, B2's dynamic index) and rejecting them when they would have *narrowed* one this record wanted to keep. The verdict was right in all four drafts; the supporting argument was wrong in three. It now rests on one measured property and no supporting argument at all, which is the form it should have taken first. The correction to A2 runs the same way: the value binder `[expr].all(v, …)` removes the evaluation-cost half of A2's residual, so **A2 is struck more firmly than the first draft struck it**. Binds later stories: **S05** must not be widened to carry cross-manifest data; **S07**'s violation shape must support a fold result and a path/cycle witness, not a cross-manifest reference; **S12** must correct ADR-0002's `rego` bullet, which calls the tier an "escape hatch for **cross-entry checks**" — inaccurate for the shipped input contract; **S11** must label the unquarantined example a shape illustration, never evidence of need. **Binds E11-S04, whose denylist is not yet written: `graph.reachable` MUST be allowed**, with `split` alongside it — both pure and deterministic. `graph.reachable` is the one that carries the justification (it closes the graph at any depth); `split` is a convenience for rebuilding the adjacency. A capability set drafted from "deny anything unfamiliar" would strike out the epic's own strongest justification. Recorded in the S04 section of the epic spec, not only S01's. **That floor is held by REVIEW, not by a gate, and this row says so rather than inventing an enforcement path:** REQ-E11-S04-02's committed golden detects a *change* to the allowed set (so the sandbox cannot silently widen) and cannot detect an *omission* — a golden written without `graph.reachable` stays green forever. It says nothing about judgment call (d), since *which* builtins are callable is orthogonal to *where* the evaluator lives. Two residuals raised, neither decided, **neither gating any verdict here**, and neither the escalated rule-7 (d1)/(d2) question: **OQ-35** (the `entry`/`oldEntry` binding asymmetry — a silent `assent test` / `assent run` divergence; set-difference is struck either way and the graph shape needs no entry tree) and **OQ-36** (the frozen provider declaration has no object/map type, yet the authoring surface and `builtin/repo-file` together permit a mapping-valued fact). Also flagged, not edited (out of lane): `REQ-DEM-S05-04` calls the provider-visible tree the "merged-result checkout"; the code reads `/head`, documented at `cmd/assent/checkout.go:44` as "the MERGE-REQUEST HEAD". This lane writes no Go, adds no dependency and touches no schema. Revert: delete `docs/planning/rego-tier-ceiling.md` and the D-156 narrowing text from the E11 spec — which restores an epic justified by four shapes, three of which this record shows are not real. | | D-158 | 2026-08-23 | **CI-TOOLCHAIN — `verify` was red on every PR from a golangci-lint/Go skew; the remedy is to bump `GOLANGCI_LINT_VERSION` v2.12.2 → v2.13.1 and KEEP `go-version: stable`.** Symptom: PR #85, a six-file Markdown diff with **zero Go bytes**, failed `verify` with `/opt/hostedtoolcache/go/1.27.0/x64/src/crypto/internal/randutil/randutil.go:11:2: could not import math/rand/v2 (… method must have no type parameters) (typecheck)` — the failing path is inside the **Go toolchain's own source tree**, so no author change can fix it and re-running cannot clear it. `Analyze (go)`, `Analyze (actions)` and `CodeQL` all passed on the same run: the tree compiles clean under Go 1.27, only the linter chokes. **Mechanism**: golangci-lint typechecks the standard library with the `go/types` it was **compiled with**, not the `go` on `PATH`. GitHub's `stable` rolled 1.26 → 1.27.0 between this repo's last green `main` run (2026-08-19) and 2026-08-23; the v2.12.2 release binary is built with go1.26.x and cannot read the 1.27 stdlib. **Reproduced locally, not reasoned** (Go 1.27.0 SDK on `PATH`, `GOTOOLCHAIN=local`, whole tree): v2.12.2 → **panic** in `pkg/goanalysis/runner_loadingpackage.go:335` inside `go/types.(*Checker).Files`, exit 2; official v2.13.1 asset (`built with go1.27.0`) → **0 issues**, exit 0; `golangci-lint config verify` → exit 0, so the v2 config schema in `.golangci.yml` needs no migration; v2.13.1 also → **0 issues** against local Go 1.26.6, so the bump is safe for contributors who have not moved; and `go install …@v2.13.1` under Go 1.27.0 → 0 issues, which is the **`release-exitgate`** path (that job builds the binary rather than using the action, and `if: github.event_name != 'pull_request'` / RELSE-08 means no PR ever exercises it). **Diagnosis heuristic worth keeping**: golangci-lint's `go.mod` carries the comment *"the minimum Go version must always be latest-1"*, so its `go` directive is a machine-readable "supports Go 1.N+1" signal — v2.12.2 says `go 1.25.0` (supports ≤1.26), v2.13.1 says `go 1.26.0` (supports ≤1.27), and upstream commit `42a0530` in v2.13.0 is literally "go1.27 support". **Options considered.** (A) *bump the linter* — CHOSEN: treats the root cause, is a **one-line** diff because the version is single-sourced at workflow scope (D-128), fixes BOTH exposed sites (the `golangci-lint-action` in `verify` and the `go install` in `release-exitgate`) at once, and the risk it carried — new findings from a newer linter blocking every merge, since `golangci-lint` runs inside `task lint` inside `task check` — was **measured at zero** on the whole tree under both Go versions. (B) *pin `go-version: 1.26.x`* — REJECTED as the primary: it needs two pins (`verify.yaml:56` and `:171`), leaves the class of bug live, undercuts the stated reason `stable` is there (`# govulncheck needs it`, with `setup-go` exporting `GOTOOLCHAIN=local` so a pinned toolchain can fail to `go run` a tool whose module requires a newer Go — unverified, and moot under (A)), and trades a loud recurrence for **silent indefinite drift onto an unsupported Go** in a repo whose posture is govulncheck + cosign + SLSA + Scorecard. (C) *both* — REJECTED as gold-plating: (A) alone is measured green, and a second simultaneous remedy would make a still-red PR ambiguous. **Per-file sweep of `go-version: stable`, stated rather than silently skipped:** `verify.yaml:56` and `:171` were the only exposed sites and are fixed by the env bump without touching either line; `schemas.yml:57` (runs `go test` + ajv, no linter), `vulncheck.yaml:30` (govulncheck only — `stable` is actively *desirable* there) and `codeql.yaml:45` (CodeQL, which passed on 1.27.0) carry no golangci-lint and are NOT exposed; `release.yaml` uses `go-version-file: go.mod` and is unaffected. `hack/lint/workflow_pins_test.sh` asserts `TASK_VERSION`, action SHA pins and step wiring but **not** `go-version` or `GOLANGCI_LINT_VERSION`; it passes on this change. **Revert is (B), not bare v2.12.2** — reverting the env line alone restores a known-red state: revert = `GOLANGCI_LINT_VERSION` back to `v2.12.2` **and** pin `verify.yaml:56` + `:171` to `go-version: 1.26.x`. **Residual risk, stated plainly:** when `stable` rolls to Go 1.28, v2.13.1 breaks identically. The repo finds out because `verify` reds on **every** PR including zero-Go diffs — loud and immediate, with the signature recorded in `verify.yaml`'s env comment and the fix being one env line. Nothing detects it *earlier*: dependabot's `github-actions` ecosystem updates `uses:` refs, not `env:` literals (backlog `CI-TOOLCHAIN-F01`). Accepted on purpose over (B)'s failure mode. Note also the pre-existing local/CI linter skew — `Taskfile.yml`'s `lint` task is bare `golangci-lint run ./...` against whatever binary a contributor has installed, so this pin has never governed local `task check`; deliberately not changed here (that file was owned by a concurrent lane). | | D-159 | 2026-08-23 | **ORPHAN — `release-verify-test` was a gate invoked by nothing (D-124 again), and it is wired into `task check` in its three OFFLINE modes, not its default `all`.** Finding: `Taskfile.yml` defined `release-verify-test` — the **only** test of `hack/release/verify-artifacts.sh` — and no caller existed anywhere: not `check:`, not `CHECK_STAGES` in `hack/audit/exitgate_test.sh`, not `.github/workflows/**`, not the push-only `release-exitgate`. That script is not incidental: **`SECURITY.md:61` publishes it as the procedure release consumers run** to check artifact checksums, the stamped `assent version` and cosign signatures, and D-153/AUD2-F01 had just proved that published verification instructions rot silently. Measured before fixing, as the lane required: the gate was **green**, so this is a wiring defect only — nothing was being papered over. **Why not the `all` default.** `verify_test.sh` with no argument adds `test_snapshot_pass`, which shells out to `task release-snapshot`: `go install github.com/goreleaser/goreleaser/v2@…` on any machine without it (**network**, in a gate that runs before every commit), a `before: hooks: go mod tidy` that **rewrites `go.mod`/`go.sum` in the middle of `task check`**, `--clean` on the developer's `dist/`, and a five-target cross-compile (10s here with warm caches and goreleaser already installed; minutes cold). A flaky or network-bound stage is worse than a missing one, so `check:` runs `negative`, `cosign-skip-when-absent` and `readme` — REQ-E9-S12-02/03/04, all offline, together well under a second. **Consequence, stated precisely: REQ-E9-S12-01 (the real snapshot→verify round trip) is not gated per-commit in `task check`; it runs in push-only CI via `hack/release/exitgate_test.sh:33-34` (the `release-exitgate` job, `if: github.event_name != 'pull_request'`) — automated but not PR-visible, i.e. the RELSE-08 blind spot.** Those two lines are literally `task release-snapshot` then `task release-verify`, which is the `Verify:` string the spec gives the requirement (`openspec/specs/p5-e9-distribution/spec.md:441-442`), so nothing here needs a new gate built — an earlier draft of this row claimed the requirement was covered by no automation at all, which was false, and acting on it would have meant a future lane duplicating `exitgate_test.sh:33-34`. What this lane declines to do is move that L1 round trip into a per-commit gate: it cannot be, for the network/`go mod tidy`/`--clean` reasons above. Narrowing the RELSE-08 exposure for this requirement is a separate question from D-159. **Pinning.** `CHECK_STAGES` goes 20 → 21 in the same commit as the `check:` line (the AUD-S18/RELSE-08 lockstep), and `STAGE_BODY_PINS` pins the body **per mode** rather than by the bare script path — a single `bash hack/release/verify_test.sh` pin would stay green if two modes were dropped *and* if the stage were reverted to the unrunnable-in-check default. Three mutation controls prove it: deleting the `check:` line reds `check_check_wiring` by stage name, gutting one of the three modes reds `check_stage_bodies` while the other two still run, and the same deletion applied to the real tree reds the real gate at rc=1. **Also fixed, minimally, because wiring made it matter:** `verify_test.sh` wrote its captured stdout/stderr to fixed `/tmp/verify-{tamper,nosig}.{out,err}` and then **grepped** them; harmless while nothing ran it, but this repo runs several lane worktrees whose `task check` invocations overlap, and a concurrent run truncating `/tmp/verify-nosig.err` at open would fail the other run's `skip.*cosign` grep spuriously. Scratch files now live in each run's own `mktemp -d` (invisible to `verify-artifacts.sh`, which globs only `*.tar.gz`/`*.zip`) and are removed by the existing `RETURN` trap. | -| D-160 | 2026-08-23 | **UNIV-COSIGN — the cosign signer-pin gate asserted an EXISTENTIAL property where the guarantee it publishes is UNIVERSAL, so it certified nothing about a file's second `cosign verify-blob`; `hack/release/install_cosign_pin_test.sh` now grades EVERY invocation in ALL THREE published files, statically and at runtime.** Substance first, and measured before anything was written: a scratch copy of each graded file with a **second, unpinned** `cosign verify-blob` spliced IN-BODY next to its real invocation (the splice shape matters — see UC-04 below) ran the gate to **exit 0** — `hack/install.sh` rc=0, `SECURITY.md` rc=0, `hack/release/verify-artifacts.sh` rc=0, the last of these being the shape a reviewer had already demonstrated on an earlier lane. **Every individual assertion in that gate was sound.** `has_flag` grepped the whole folded extraction, so a pinned sibling satisfied it; `one_value`'s `sort -u` collapsed two agreeing values to one, so the D-153 drift comparison saw a consistent file; section 0 **printed** the extracted invocation count and asserted nothing about it; and 4b/5d's stub-log checks were positive-only greps, i.e. the same existential shape at runtime, where a second unpinned call leaves the pinned call's log line intact. The conjunction of sound existential assertions is still an existential assertion. **This is the AUD2-S05 quorum defect one layer out: not a wrong assertion, a wrong quantifier**, and it predates both AUD2-S03 and AUD2-F01. **`SECURITY.md` was worse than the other two** — it fed only the drift comparison and had **no invocation-level grading at all**, so an unpinned recipe published to adopters was invisible to the gate that exists to police the recipe. **Property chosen: "every `cosign verify-blob` invocation in every graded file carries `--certificate-oidc-issuer`, `--certificate-identity-regexp` and `--bundle`, EACH WITH SECURITY.md's published value".** The value half is not decoration: `--certificate-identity-regexp ''` carries the flag and matches every Fulcio identity ever issued, and `one_value`'s `sort -u` does not catch it either, because an empty capture is not a line and the file still reports exactly one distinct value — a presence-only universal check would be the same defect one level down, so each invocation's own extracted value is compared against the published pair (reported `WRONG-VALUE[...]`, distinct from `UNPINNED[...]`). Options considered: **(a)** the remedy recorded when the finding was filed — assert the extracted invocation count is **exactly 1** per file (**REJECTED AS FACTUALLY WRONG — do not implement it in a later lane; it would red `main` on the day it lands.** `SECURITY.md` legitimately publishes **two** — one over the archive, one over `checksums.txt`, which is what covers the SBOMs listed inside it — so that assertion reds `main` on the day it lands, and the natural repair is to weaken it again); **(b)** universal quantification over invocations **(chosen)** — strictly stronger than (a) where (a) is true, and it keeps holding when a file legitimately grows a third correctly-pinned call. **Enforcement, per D-128, is one predicate**: `pin_violations ` prints one line per problem and nothing when the file is clean, so callers grade its OUTPUT and the identical function is asserted empty against the tree and non-empty against a mutant with no `set -e` games; `assert_all_pinned` is the thin failing wrapper; `log_unpinned_lines` is its runtime twin over the stub-cosign argv log. **Classification is fail-CLOSED, which is the part that carries the guarantee.** The candidate extractor is deliberately left un-narrowed (every non-comment line mentioning `cosign verify-blob`, continuations folded), because anything the *denominator* drops is a hole. A candidate is an invocation when the folded text begins with `cosign verify-blob`; the ONE waved-through non-invocation shape is a markdown inline-code mention (`` `cosign verify-blob` ``, which is how `SECURITY.md`'s capability table names it); **anything else — `foo && cosign verify-blob …`, a here-doc line, an un-backticked prose sentence — is reported UNCLASSIFIABLE rather than skipped**, because "this gate cannot tell whether that call is pinned" must never read as "that call is fine". Accepted cost, stated rather than discovered later: a *correctly pinned* invocation written off command position also reds. That is the intended direction of error for a security gate over three files carrying four invocations in one canonical style, and the message names the fix. **Anti-vacuity, because a lane whose entire deliverable is "make a gate stricter" is maximally exposed** (this repo's #1 review finding is an assertion that cannot fail — D-124, AUD-S18): section 2b runs **eight** mutants against **each** of the three files and 2c runs a ninth, and they were chosen for **branch** coverage of the new predicate rather than for variety of shape — (a) a second **unpinned** invocation must red, name the file, quote the offending command, and produce **exactly two** violations so the pinned siblings are provably not flagged; (b) a second **correctly pinned** invocation must stay green **and** must raise the extractor's invocation count by one, without which (b)'s green could mean "the extractor never saw it"; (c) an occurrence off command position, appended **fully pinned on purpose** so the only thing that can redden it is the classifier itself; (d) every invocation deleted → `NO-CANDIDATES`; (e) the continuation fold broken → `FOLD-BROKEN`, asserted **not** to also report `UNPINNED`, because conflating "the extractor truncated this" with "the pin is missing" sends the next maintainer to the wrong file; (f) every invocation displaced off command position → `NO-INVOCATIONS`; (g) a second invocation carrying both flags with an **empty** identity regexp → `WRONG-VALUE`, the hostile shape a presence-only check waves through; (h) a second invocation carrying both flags with a **foreign OIDC issuer** → `WRONG-VALUE` on the issuer half; and 2c strips the backticks from `SECURITY.md`'s prose mention and requires the same row to fail closed, proving the exemption keys on the backticks and is not a blanket bypass. The runtime twin has its own vacuity control (an unpinned line appended to a copy of the stub log must be seen). **One real defect was caught by this section during the lane and is recorded because it is a trap for the next author**: `log_unpinned_lines` was first written with `awk -v id="identity_re=${sec_identity}"`, and **awk processes escape sequences in a `-v` assignment**, so the pin's `github\.com` arrived as `github.com` and matched nothing; the values now reach awk through `ENVIRON`. **Stated limit, same posture as D-154's**: the denominator is the literal string `cosign verify-blob`, so an invocation spelled through a variable (`"$COSIGN" verify-blob …`), built by `eval`, or assembled from fragments is invisible to this gate. Widening the trigger to bare `verify-blob` was considered and **rejected** — it buys one hypothetical no file uses, and turns any future `SECURITY.md` sentence saying "verify-blob" outside backticks into a red gate, whose repair would be to loosen the classifier. **Nothing outside the gate changed**: `hack/install.sh`, `SECURITY.md` and `hack/release/verify-artifacts.sh` are byte-unchanged, and all four of their invocations were already pinned — this row closes a hole in the *checker*, not in the checked. The stage `release-install-cosign-pin-test` was already wired into `task check` and pinned in `hack/audit/exitgate_test.sh`'s `CHECK_STAGES`, so no wiring changed either. **SECOND ROUND — the first version of this fix REPRODUCED the very defect it closes, one level down, and independent review caught it before merge.** `has_flag` grepped the whole FILE; the replacement grepped the whole LINE. Both are existential; only the scope shrank. **UC-01**: one folded line was graded as at most ONE invocation, so `cosign verify-blob --bundle a.json a && cosign verify-blob --bundle EVIL.json evil` began with `cosign verify-blob` (not UNCLASSIFIABLE), carried `--bundle` (not FOLD-BROKEN), carried both flag strings (not UNPINNED) and yielded the published values (not WRONG-VALUE) — **green**, in same-line, `;`-separated and backslash-folded forms, on all three graded files. Worse, the **full gate exited 0** for `SECURITY.md`: the two shell scripts were incidentally caught by the runtime twin (`log_unpinned_lines` at §5d), but **SECURITY.md is a document and has no runtime twin**, so the hole was unmitigated precisely on the file this row calls "the copy-paste recipe adopters run by hand" — D-153's exact incident class — while the gate printed "EVERY cosign verify-blob invocation ... is pinned", false as printed. The stated-limit paragraph did not cover it: it enumerated `$COSIGN`, `eval` and fragments, not `&&` chaining, and **leading** `&&` was explicitly handled (mutant (c) → UNCLASSIFIABLE), so the operator had been considered and only one side handled. Closed by grading per **OCCURRENCE** (`occurrence_count` + a new `MULTI-OCCURRENCE` violation that fails closed on any line carrying two calls) rather than per line; counting inside an already-triggered line uses the shorter `verify-blob`, so a second call spelled `cosign verify-blob` or `"$COSIGN" verify-blob` and chained onto a pinned one is caught too, which the literal file-level trigger would miss. **UC-02**: `extract_issuer`/`extract_identity` anchor on a greedy `.*`, so the LAST value on a line wins — a hostile `--certificate-identity-regexp ''` placed FIRST was masked by a correct value placed second, **the extraction direction favoured the attacker**. Closed by `flag_value_tokens`, which returns EVERY value of every flag on the occurrence; each must equal the published one, so a repeated flag with an empty value first now reds. **UC-03 (P2, the erosion path)**: a CORRECTLY pinned call written with **double quotes** was refused as `WRONG-VALUE ... identity= ... (an empty regexp matches every Fulcio identity)` — a true refusal with a **false reason**, and the repair a maintainer reaches for on that message is widening the extractor. Both quote styles are now accepted (double quotes are correct shell for this value: it contains no `$` and no backtick), and a **bare** value is diagnosed as `UNQUOTED-VALUE`, a QUOTING defect, never as a wrong or empty one — a gate that misdiagnoses erodes faster than one that refuses. **UC-04**: this row's "rc=0, rc=0, rc=0" reproduction figure is **splice-shape-sensitive** and is stated as measured: it holds for a second unpinned call spliced **in-body** next to the real one. An EOF-appended mutant reds the two shell scripts for an unrelated runtime reason, so the figure should not be read as holding for any second unpinned call. The same sensitivity is why the UC-03 double-quoted mutant reds the two scripts through the full gate (the spliced call actually RUNS and its fixture bundle is absent) while `SECURITY.md`, having no runtime, is the clean end-to-end proof at rc=0. The classifier's fail-closed posture on off-command-position occurrences was independently adjudicated KEEP, since §2c proves the prose exemption keys on the backticks and cannot be widened silently. **The lesson, recorded because it is the whole point of the lane:** a fix for an existential-where-universal defect is itself maximally exposed to the same defect at the next scope down — file, then line, then occurrence — and the only thing that caught it was a reviewer building the chained-call mutant that neither the 20-row external matrix nor the 25 in-gate mutants contained. **THIRD ROUND (UC-05..UC-09), and the reason this row now reads the way it does.** **UC-05**: `occurrence_count` compared whitespace-delimited fields to `verify-blob`, found one, and concluded **singularity** — when all it had established is that it did not find a second. `cosign "verify-blob"`, `cosign 'verify-blob'` and `cosign verify-blob""` are the same command to the shell, and each hid a chained unpinned call from the count. Measured against the round-2 gate on **all three** files at whole-gate level: **rc=0, rc=0, rc=0** — worse than first reported, because `A && B` short-circuits and `set -e` does **not** fire on a non-final member of an AND-list, so even the two shell scripts' runtime twin missed it. Closed by stripping shell quotes before the field compare, which is **a spelling patch, not a terminator, and is labelled as one in the code**. A structural terminator was sought and **ruled out with evidence**: refusing any graded line carrying a command separator would red the REAL files, since `hack/install.sh` and `hack/release/verify-artifacts.sh` both legitimately end their genuine invocation with an or-else `die` tail. **No structural terminator exists for this gate**, so completeness is not available and must not be claimed. **UC-07 is therefore the durable fix, and it is a change of posture rather than of logic.** The `PASS:` banner was printed unconditionally and asserted "EVERY cosign verify-blob OCCURRENCE ... is pinned" plus "a second unpinned call reddens whether it sits on its own line or is chained onto a pinned one" — a **universal claim bound to no assertion**. Under UC-05 that banner did not merely overstate: on a green run it printed something **false**, which is strictly worse than printing nothing, and it is this repo's #1 defect class (an assertion that cannot fail) wearing a different hat. The banner now reports **OBSERVED** counts per file (occurrences found, classified-and-graded, prose-exempt, refused), lists **ASSERTED** properties each of which is shown to fail on a mutant, and states the **NOT ASSERTED** residual in the same breath: this gate finds calls by a literal string and counts quote-stripped words, so a call spelled through a variable, `eval`, or fragments is not seen and not graded, and the counts are what was classified — **not a proof that nothing else exists**. When a fifth spelling turns up, the gate is then **incomplete rather than wrong**, and incomplete is recoverable. **UC-06**: a TRAILING comment mentioning `verify-blob` fired `MULTI-OCCURRENCE: … has 2 verify-blob calls chained on ONE line` — fail-closed but **false as printed**, since `cosign_candidates` only drops lines whose FIRST non-space character is `#`. That is the UC-03 misdiagnosis shape recurring **inside the UC-01 fix**. The message now says TOKENS, names both possible causes, and names the correct repair; excluding trailing comments was rejected as it needs quote-aware parsing, which is the machinery that produced UC-01/02/03. **UC-08**: `shellcheck` SC1087 ×2 (error severity) on `flag_value_tokens` — `"$flag[[:space:]]…"` parses as an array subscript; `${flag}` silences it. Cosmetic: no shellcheck gate exists in this repo. **UC-09**: two stage-count figures reported during this lane ("25", then "28") were **both wrong** and neither came from a committed file — they counted `task: [` lines in a run LOG, which includes nested task invocations. Measured: the Taskfile `check:` block has **21** `- task:` entries and `CHECK_STAGES` has **21** stage names; they agree, and both files are byte-identical to `origin/main`. There is no stage-count mismatch and this lane could not have caused one. **THE PATTERN, recorded because it is the lane's most transferable output:** four P1s, three of them the same scope error at successively finer scopes — file (`has_flag`), line (round 1), then occurrence-spelling (round 2) — each found by review and none by the author's own mutant matrix, because each matrix was built from the shape the previous round had just learned. The general lesson is not "add another spelling": it is that **when a gate's denominator cannot be made provably complete, the gate must report what it classified instead of asserting what exists.** That is now enforced where it is hardest to ignore, in the banner the gate prints on every green run. Revert: restore `has_flag`, drop the per-occurrence grading and the per-invocation value comparison, and restore the two positive-only stub-log greps — which returns the gate to certifying that *some* cosign call in each file is pinned, a property that is compatible with an unpinned one sitting beside it. | +| D-160 | 2026-08-23 | **UNIV-COSIGN — the cosign signer-pin gate asserted an EXISTENTIAL property where the guarantee it publishes is UNIVERSAL, so it certified nothing about a file's second `cosign verify-blob`; `hack/release/install_cosign_pin_test.sh` now grades EVERY invocation in ALL THREE published files, statically and at runtime.** Substance first, and measured before anything was written: a scratch copy of each graded file with a **second, unpinned** `cosign verify-blob` spliced IN-BODY next to its real invocation (the splice shape matters — see UC-04 below) ran the gate to **exit 0** — `hack/install.sh` rc=0, `SECURITY.md` rc=0, `hack/release/verify-artifacts.sh` rc=0, the last of these being the shape a reviewer had already demonstrated on an earlier lane. **Every individual assertion in that gate was sound.** `has_flag` grepped the whole folded extraction, so a pinned sibling satisfied it; `one_value`'s `sort -u` collapsed two agreeing values to one, so the D-153 drift comparison saw a consistent file; section 0 **printed** the extracted invocation count and asserted nothing about it; and 4b/5d's stub-log checks were positive-only greps, i.e. the same existential shape at runtime, where a second unpinned call leaves the pinned call's log line intact. The conjunction of sound existential assertions is still an existential assertion. **This is the AUD2-S05 quorum defect one layer out: not a wrong assertion, a wrong quantifier**, and it predates both AUD2-S03 and AUD2-F01. **`SECURITY.md` was worse than the other two** — it fed only the drift comparison and had **no invocation-level grading at all**, so an unpinned recipe published to adopters was invisible to the gate that exists to police the recipe. **Property chosen: "every `cosign verify-blob` invocation in every graded file carries `--certificate-oidc-issuer`, `--certificate-identity-regexp` and `--bundle`, EACH WITH SECURITY.md's published value".** The value half is not decoration: `--certificate-identity-regexp ''` carries the flag and matches every Fulcio identity ever issued, and `one_value`'s `sort -u` does not catch it either, because an empty capture is not a line and the file still reports exactly one distinct value — a presence-only universal check would be the same defect one level down, so each invocation's own extracted value is compared against the published pair (reported `WRONG-VALUE[...]`, distinct from `UNPINNED[...]`). Options considered: **(a)** the remedy recorded when the finding was filed — assert the extracted invocation count is **exactly 1** per file (**REJECTED AS FACTUALLY WRONG — do not implement it in a later lane; it would red `main` on the day it lands.** `SECURITY.md` legitimately publishes **two** — one over the archive, one over `checksums.txt`, which is what covers the SBOMs listed inside it — so that assertion reds `main` on the day it lands, and the natural repair is to weaken it again); **(b)** universal quantification over invocations **(chosen)** — strictly stronger than (a) where (a) is true, and it keeps holding when a file legitimately grows a third correctly-pinned call. **Enforcement, per D-128, is one predicate**: `pin_violations ` prints one line per problem and nothing when the file is clean, so callers grade its OUTPUT and the identical function is asserted empty against the tree and non-empty against a mutant with no `set -e` games; `assert_all_pinned` is the thin failing wrapper; `log_unpinned_lines` is its runtime twin over the stub-cosign argv log. **Classification is fail-CLOSED, which is the part that carries the guarantee.** The candidate extractor is deliberately left un-narrowed (every non-comment line mentioning `cosign verify-blob`, continuations folded), because anything the *denominator* drops is a hole. A candidate is an invocation when the folded text begins with `cosign verify-blob`; the ONE waved-through non-invocation shape is a markdown inline-code mention (`` `cosign verify-blob` ``, which is how `SECURITY.md`'s capability table names it); **on a line carrying NO backticked mention, anything else — `foo && cosign verify-blob …`, a here-doc line, an un-backticked prose sentence — is reported UNCLASSIFIABLE rather than skipped**, because "this gate cannot tell whether that call is pinned" must never read as "that call is fine". **That scoping is not cosmetic, and the unscoped version of this sentence was FALSE (R3-01, caught by review on the round that added the honest banner).** The exemption tests whether the substring `` `cosign verify-blob` `` appears **anywhere on the line**, not whether the line is prose, and it is tested BEFORE the command-position and multi-token checks. So a line carrying a backticked mention AND one or more LIVE calls is exempted, neither graded nor refused: measured by splicing ``See `cosign verify-blob`: cosign verify-blob --bundle A.json a && cosign verify-blob --bundle EVIL.json evil`` into `SECURITY.md` — `occurrence_count` = 2 by the definition the banner itself states, `pin_violations` EMPTY, **whole gate rc=0**, while the banner reported that line among those "exempted as backticked prose". The **static** defect is not markdown-specific — splicing a live unpinned call with a trailing backticked mention into `hack/install.sh` gives candidates=2, invocations=1, `pin_violations` EMPTY — but the **whole-gate green is** markdown-specific, and the distinction is stated because a looser sentence here would itself be falsifiable: in that shell script the run reds at §4b for an unrelated RUNTIME reason (the spliced call executes and its bundle is absent), whereas `SECURITY.md` is a document with no runtime twin, which is why rc=0 survives there. Measured both ways rather than inferred from either. **Narrowing the exemption needs quote- and markdown-aware parsing — the machinery that produced UC-01/02/03 — so it is deliberately NOT patched here.** It is instead disclosed as residual (1) in the PASS banner, ahead of the variable/`eval`/fragment spellings, because it is the residual that is actually REACHABLE in these three files while those are not present in any of them. The banner also no longer labels an exempted line "prose": the branch it took is a fact, "prose" was an inference, and R3-01 is the case where that inference is wrong. **This is UC-07 doing its job on its own author:** the claim was falsifiable, it was checked, and the gate is now incomplete-and-honest rather than complete-and-wrong. Accepted cost, stated rather than discovered later: a *correctly pinned* invocation written off command position also reds. That is the intended direction of error for a security gate over three files carrying four invocations in one canonical style, and the message names the fix. **Anti-vacuity, because a lane whose entire deliverable is "make a gate stricter" is maximally exposed** (this repo's #1 review finding is an assertion that cannot fail — D-124, AUD-S18): section 2b runs **eight** mutants against **each** of the three files and 2c runs a ninth, and they were chosen for **branch** coverage of the new predicate rather than for variety of shape — (a) a second **unpinned** invocation must red, name the file, quote the offending command, and produce **exactly two** violations so the pinned siblings are provably not flagged; (b) a second **correctly pinned** invocation must stay green **and** must raise the extractor's invocation count by one, without which (b)'s green could mean "the extractor never saw it"; (c) an occurrence off command position, appended **fully pinned on purpose** so the only thing that can redden it is the classifier itself; (d) every invocation deleted → `NO-CANDIDATES`; (e) the continuation fold broken → `FOLD-BROKEN`, asserted **not** to also report `UNPINNED`, because conflating "the extractor truncated this" with "the pin is missing" sends the next maintainer to the wrong file; (f) every invocation displaced off command position → `NO-INVOCATIONS`; (g) a second invocation carrying both flags with an **empty** identity regexp → `WRONG-VALUE`, the hostile shape a presence-only check waves through; (h) a second invocation carrying both flags with a **foreign OIDC issuer** → `WRONG-VALUE` on the issuer half; and 2c strips the backticks from `SECURITY.md`'s prose mention and requires the same row to fail closed, proving the exemption keys on the backticks and is not a blanket bypass. The runtime twin has its own vacuity control (an unpinned line appended to a copy of the stub log must be seen). **One real defect was caught by this section during the lane and is recorded because it is a trap for the next author**: `log_unpinned_lines` was first written with `awk -v id="identity_re=${sec_identity}"`, and **awk processes escape sequences in a `-v` assignment**, so the pin's `github\.com` arrived as `github.com` and matched nothing; the values now reach awk through `ENVIRON`. **Stated limit, same posture as D-154's**: the denominator is the literal string `cosign verify-blob`, so an invocation spelled through a variable (`"$COSIGN" verify-blob …`), built by `eval`, or assembled from fragments is invisible to this gate. Widening the trigger to bare `verify-blob` was considered and **rejected** — it buys one hypothetical no file uses, and turns any future `SECURITY.md` sentence saying "verify-blob" outside backticks into a red gate, whose repair would be to loosen the classifier. **Nothing outside the gate changed**: `hack/install.sh`, `SECURITY.md` and `hack/release/verify-artifacts.sh` are byte-unchanged, and all four of their invocations were already pinned — this row closes a hole in the *checker*, not in the checked. The stage `release-install-cosign-pin-test` was already wired into `task check` and pinned in `hack/audit/exitgate_test.sh`'s `CHECK_STAGES`, so no wiring changed either. **SECOND ROUND — the first version of this fix REPRODUCED the very defect it closes, one level down, and independent review caught it before merge.** `has_flag` grepped the whole FILE; the replacement grepped the whole LINE. Both are existential; only the scope shrank. **UC-01**: one folded line was graded as at most ONE invocation, so `cosign verify-blob --bundle a.json a && cosign verify-blob --bundle EVIL.json evil` began with `cosign verify-blob` (not UNCLASSIFIABLE), carried `--bundle` (not FOLD-BROKEN), carried both flag strings (not UNPINNED) and yielded the published values (not WRONG-VALUE) — **green**, in same-line, `;`-separated and backslash-folded forms, on all three graded files. Worse, the **full gate exited 0** for `SECURITY.md`: the two shell scripts were incidentally caught by the runtime twin (`log_unpinned_lines` at §5d), but **SECURITY.md is a document and has no runtime twin**, so the hole was unmitigated precisely on the file this row calls "the copy-paste recipe adopters run by hand" — D-153's exact incident class — while the gate printed "EVERY cosign verify-blob invocation ... is pinned", false as printed. The stated-limit paragraph did not cover it: it enumerated `$COSIGN`, `eval` and fragments, not `&&` chaining, and **leading** `&&` was explicitly handled (mutant (c) → UNCLASSIFIABLE), so the operator had been considered and only one side handled. Closed by grading per **OCCURRENCE** (`occurrence_count` + a new `MULTI-OCCURRENCE` violation that fails closed on any line carrying two calls) rather than per line; counting inside an already-triggered line uses the shorter `verify-blob`, so a second call spelled `cosign verify-blob` or `"$COSIGN" verify-blob` and chained onto a pinned one is caught too, which the literal file-level trigger would miss. **UC-02**: `extract_issuer`/`extract_identity` anchor on a greedy `.*`, so the LAST value on a line wins — a hostile `--certificate-identity-regexp ''` placed FIRST was masked by a correct value placed second, **the extraction direction favoured the attacker**. Closed by `flag_value_tokens`, which returns EVERY value of every flag on the occurrence; each must equal the published one, so a repeated flag with an empty value first now reds. **UC-03 (P2, the erosion path)**: a CORRECTLY pinned call written with **double quotes** was refused as `WRONG-VALUE ... identity= ... (an empty regexp matches every Fulcio identity)` — a true refusal with a **false reason**, and the repair a maintainer reaches for on that message is widening the extractor. Both quote styles are now accepted (double quotes are correct shell for this value: it contains no `$` and no backtick), and a **bare** value is diagnosed as `UNQUOTED-VALUE`, a QUOTING defect, never as a wrong or empty one — a gate that misdiagnoses erodes faster than one that refuses. **UC-04**: this row's "rc=0, rc=0, rc=0" reproduction figure is **splice-shape-sensitive** and is stated as measured: it holds for a second unpinned call spliced **in-body** next to the real one. An EOF-appended mutant reds the two shell scripts for an unrelated runtime reason, so the figure should not be read as holding for any second unpinned call. The same sensitivity is why the UC-03 double-quoted mutant reds the two scripts through the full gate (the spliced call actually RUNS and its fixture bundle is absent) while `SECURITY.md`, having no runtime, is the clean end-to-end proof at rc=0. The classifier's fail-closed posture on off-command-position occurrences was independently adjudicated KEEP, since §2c proves the prose exemption keys on the backticks and cannot be widened silently. **The lesson, recorded because it is the whole point of the lane:** a fix for an existential-where-universal defect is itself maximally exposed to the same defect at the next scope down — file, then line, then occurrence — and the only thing that caught it was a reviewer building the chained-call mutant that neither the 20-row external matrix nor the 25 in-gate mutants contained. **THIRD ROUND (UC-05..UC-09), and the reason this row now reads the way it does.** **UC-05**: `occurrence_count` compared whitespace-delimited fields to `verify-blob`, found one, and concluded **singularity** — when all it had established is that it did not find a second. `cosign "verify-blob"`, `cosign 'verify-blob'` and `cosign verify-blob""` are the same command to the shell, and each hid a chained unpinned call from the count. Measured against the round-2 gate on **all three** files at whole-gate level: **rc=0, rc=0, rc=0** — worse than first reported, because `A && B` short-circuits and `set -e` does **not** fire on a non-final member of an AND-list, so even the two shell scripts' runtime twin missed it. Closed by stripping shell quotes before the field compare, which is **a spelling patch, not a terminator, and is labelled as one in the code**. A structural terminator was sought and **ruled out with evidence**: refusing any graded line carrying a command separator would red the REAL files, since `hack/install.sh` and `hack/release/verify-artifacts.sh` both legitimately end their genuine invocation with an or-else `die` tail. **No structural terminator exists for this gate**, so completeness is not available and must not be claimed. **UC-07 is therefore the durable fix, and it is a change of posture rather than of logic.** The `PASS:` banner was printed unconditionally and asserted "EVERY cosign verify-blob OCCURRENCE ... is pinned" plus "a second unpinned call reddens whether it sits on its own line or is chained onto a pinned one" — a **universal claim bound to no assertion**. Under UC-05 that banner did not merely overstate: on a green run it printed something **false**, which is strictly worse than printing nothing, and it is this repo's #1 defect class (an assertion that cannot fail) wearing a different hat. The banner now reports **OBSERVED** counts per file (occurrences found, classified-and-graded, prose-exempt, refused), lists **ASSERTED** properties each of which is shown to fail on a mutant, and states the **NOT ASSERTED** residual in the same breath: this gate finds calls by a literal string and counts quote-stripped words, so a call spelled through a variable, `eval`, or fragments is not seen and not graded, and the counts are what was classified — **not a proof that nothing else exists**. When a fifth spelling turns up, the gate is then **incomplete rather than wrong**, and incomplete is recoverable. **UC-06**: a TRAILING comment mentioning `verify-blob` fired `MULTI-OCCURRENCE: … has 2 verify-blob calls chained on ONE line` — fail-closed but **false as printed**, since `cosign_candidates` only drops lines whose FIRST non-space character is `#`. That is the UC-03 misdiagnosis shape recurring **inside the UC-01 fix**. The message now says TOKENS, names both possible causes, and names the correct repair; excluding trailing comments was rejected as it needs quote-aware parsing, which is the machinery that produced UC-01/02/03. **UC-08**: `shellcheck` SC1087 ×2 (error severity) on `flag_value_tokens` — `"$flag[[:space:]]…"` parses as an array subscript; `${flag}` silences it. Cosmetic: no shellcheck gate exists in this repo. **UC-09**: two stage-count figures reported during this lane ("25", then "28") were **both wrong** and neither came from a committed file — they counted `task: [` lines in a run LOG, which includes nested task invocations. Measured: the Taskfile `check:` block has **21** `- task:` entries and `CHECK_STAGES` has **21** stage names; they agree, and both files are byte-identical to `origin/main`. There is no stage-count mismatch and this lane could not have caused one. **THE PATTERN, recorded because it is the lane's most transferable output:** four P1s, three of them the same scope error at successively finer scopes — file (`has_flag`), line (round 1), then occurrence-spelling (round 2) — each found by review and none by the author's own mutant matrix, because each matrix was built from the shape the previous round had just learned. The general lesson is not "add another spelling": it is that **when a gate's denominator cannot be made provably complete, the gate must report what it classified instead of asserting what exists.** That is now enforced where it is hardest to ignore, in the banner the gate prints on every green run. Revert: restore `has_flag`, drop the per-occurrence grading and the per-invocation value comparison, and restore the two positive-only stub-log greps — which returns the gate to certifying that *some* cosign call in each file is pinned, a property that is compatible with an unpinned one sitting beside it. | diff --git a/hack/release/install_cosign_pin_test.sh b/hack/release/install_cosign_pin_test.sh index 06bf4c9..1ff9ed3 100755 --- a/hack/release/install_cosign_pin_test.sh +++ b/hack/release/install_cosign_pin_test.sh @@ -307,11 +307,20 @@ one_value() { # tree as it stands. Universal is also strictly stronger: it keeps holding when a # file grows a third, correctly pinned call. # -# FAIL-CLOSED CLASSIFICATION. A candidate that is not at command position is only -# waved through when it is a markdown inline-code mention (backticked). Anything -# else — `foo && cosign verify-blob …`, a here-doc line, an un-backticked prose -# sentence — is reported UNCLASSIFIABLE rather than skipped, because "this gate -# cannot tell whether that call is pinned" must not read as "that call is fine". +# CLASSIFICATION, AND WHERE IT IS *NOT* FAIL-CLOSED (R3-01 — read this before +# trusting the exemption). A candidate that is not at command position is waved +# through when the substring `cosign verify-blob` appears ANYWHERE ON THE LINE. +# The test is that substring, not "the line is prose", and it runs BEFORE the +# multi-token refusal below. So a line carrying a backticked mention AND one or +# more LIVE calls is skipped, not graded and not refused — measured, with the full +# gate green. On a line with NO backticked mention, anything not at command +# position — `foo && cosign verify-blob …`, a here-doc line, an un-backticked +# prose sentence — IS reported UNCLASSIFIABLE rather than skipped, because "this +# gate cannot tell whether that call is pinned" must not read as "that call is +# fine". That principle holds for those lines and is DEFEATED on a line that +# carries a backticked mention; narrowing the exemption needs quote/markdown-aware +# parsing, which is the machinery that produced UC-01/02/03, so it is recorded as +# a stated residual and surfaced in the PASS banner rather than patched blind. # # STATED LIMIT, deliberately not closed here (same posture as D-154): the # denominator is the literal string `cosign verify-blob`. An invocation spelled @@ -788,11 +797,16 @@ for target in "${GRADED[@]}"; do echo "OK: $label — an unquoted regexp is named as a QUOTING defect, not a wrong value (UC-03)" done -# The prose escape hatch is NARROW: it is the backticks that make SECURITY.md's -# capability-table row a prose mention, not the words. Strip them and the same -# row must fail closed — otherwise "prose" is a blanket bypass an unpinned call -# could be written into. -echo "== 2c. UNIV-COSIGN: the backticked-prose exemption is not a blanket bypass ==" +# The exemption is narrow IN ONE DIMENSION, and 2c grades exactly that one: it is +# the BACKTICKS that exempt SECURITY.md's capability-table row, not the words. +# Strip them and the same row must fail closed, so the exemption cannot be widened +# to "any line mentioning cosign verify-blob" without this section reddening. +# +# IT IS NOT NARROW IN THE OTHER DIMENSION, and this section does NOT claim it is +# (R3-01): the substring is looked for ANYWHERE on the line, so a line carrying a +# backticked mention AND live calls is exempted. 2c grades the backticks-vs-words +# axis; the same-line axis is an open residual, disclosed in the PASS banner. +echo "== 2c. UNIV-COSIGN: the exemption keys on the BACKTICKS, not on the words ==" grep -qF -- '`cosign verify-blob`' "$SECURITY" \ || fail "SECURITY.md no longer contains a backticked \`cosign verify-blob\` prose mention — 2c grades an exemption that is no longer exercised, so it is decorative (re-point it at whatever prose mention exists, or delete the exemption)" prose_mutant="$WORK/SECURITY.prose-declassified.md" @@ -1305,7 +1319,10 @@ for target in "${GRADED[@]}"; do label="${target%%:*}" n_c="$(grep -c . <"$WORK/cand.$label" | tr -d ' ')" n_i="$(grep -c . <"$WORK/inv.$label" | tr -d ' ')" - echo " ${label}: ${n_c} \`cosign verify-blob\` occurrence(s) found — ${n_i} classified as invocations and GRADED, $((n_c - n_i)) exempted as backticked prose, 0 refused as unclassifiable" + # "exempted" is a fact about which branch the line took; calling it "prose" is an + # INFERENCE, and R3-01 shows it is the wrong one — an exempted line may still + # carry live calls. Report the branch, not the guess about what the line is. + echo " ${label}: ${n_c} \`cosign verify-blob\` occurrence(s) found — ${n_i} classified as invocations and GRADED, $((n_c - n_i)) NOT GRADED (exempted because the line contains a backticked \`cosign verify-blob\` mention; such a line may still carry live calls — see residual (1)), 0 refused as unclassifiable" done echo " ASSERTED, and each shown to FAIL on a mutant carrying the defect it exists to catch:" echo " * every GRADED occurrence carries --certificate-oidc-issuer, --certificate-identity-regexp and --bundle," @@ -1317,8 +1334,19 @@ echo " * a foreign-signed bundle fails closed on the adopter path with nothin echo " * on the mutants section 2b builds, a second UNPINNED call reddens both on its own line and chained onto a" echo " pinned one with && / ; / | (in the spellings 2b enumerates), while a second CORRECTLY pinned call does not." echo " NOT ASSERTED — the residual, stated here rather than somewhere a reader will not look:" -echo " This gate finds calls by the literal string 'cosign verify-blob' and counts them as whitespace-delimited" -echo " words with shell quotes stripped. A call spelled through a variable, built by eval, or assembled from" -echo " fragments is NOT SEEN and therefore NOT GRADED. The counts above are what was classified — they are NOT" -echo " a proof that no other invocation exists in these files. Any line carrying more than one verify-blob token" -echo " is REFUSED (MULTI-OCCURRENCE), never graded on its first call." +echo " (1) THE BACKTICKED-MENTION EXEMPTION IS THE RESIDUAL THAT IS ACTUALLY REACHABLE. A candidate line that is" +echo " NOT at command position is exempted whenever the BACKTICK-DELIMITED substring (a backtick, then" +echo " cosign verify-blob, then a backtick) occurs ANYWHERE ON THE LINE. The test is that substring, NOT" +echo " that the line is prose, and it runs BEFORE the multi-token refusal in (3) and before the" +echo " UNCLASSIFIABLE fallback. So a line carrying BOTH such a mention AND one or more LIVE calls is" +echo " exempted and NOT GRADED, and neither of those two checks ever runs on it. Measured (R3-01), on" +echo " SECURITY.md and on a shell script; on the document the whole gate stays green, which is how it" +echo " was missed." +echo " (2) This gate finds calls by the literal string 'cosign verify-blob' and counts them as whitespace-delimited" +echo " words with shell quotes stripped. A call spelled through a variable, built by eval, or assembled from" +echo " fragments is NOT SEEN and therefore NOT GRADED. No such spelling is present in these three files today," +echo " which makes this the LESS reachable residual of the two." +echo " (3) The counts above are what was classified — they are NOT a proof that no other invocation exists in" +echo " these files. A line AT COMMAND POSITION carrying more than one verify-blob token is REFUSED" +echo " (MULTI-OCCURRENCE), never graded on its first call; that refusal does NOT reach a line exempted" +echo " under (1), because the exemption is tested first." diff --git a/openspec/specs/backlog.md b/openspec/specs/backlog.md index 5d6a39e..39d74b7 100644 --- a/openspec/specs/backlog.md +++ b/openspec/specs/backlog.md @@ -753,7 +753,7 @@ that claim). | ORPHAN | **DONE (D-159)** — `Taskfile.yml`'s `release-verify-test`, the only test of `hack/release/verify-artifacts.sh` (the procedure **`SECURITY.md:61` publishes to release consumers**), was invoked by nothing: absent from `check:`, from `CHECK_STAGES`, and from every workflow — D-124's "a gate invoked by nothing is not a gate", one epic on from AUD2-F01's published-instructions-rot finding. It was **green**, so the defect was wiring only. Now the 14th of 21 `check:` stages, in its three **offline** modes (`negative`, `cosign-skip-when-absent`, `readme` = REQ-E9-S12-02/03/04); the `all` default is deliberately NOT wired — it shells out to `task release-snapshot`, i.e. a networked `go install goreleaser`, a `go mod tidy` before-hook that rewrites tracked files mid-check, and `--clean` on `dist/`. **Not a gap to fill: REQ-E9-S12-01 (snapshot → verify round trip) is already automated** — `hack/release/exitgate_test.sh:33-34` runs exactly `task release-snapshot` then `task release-verify`, the spec's own `Verify:` string, in the `release-exitgate` job. It is push-only (`if: github.event_name != 'pull_request'`), so the exposure is **RELSE-08 visibility, not absence**; do NOT open a lane to build a gate that exists. `CHECK_STAGES` 20 → 21 in the same commit; body pinned **per mode** so dropping two modes or reverting to the bare default reds | **[autonomous]** | — | not owned by any in-flight lane; `Taskfile.yml` + `hack/audit/exitgate_test.sh` are the one `CHECK_STAGES` slot, which only one lane may hold at a time | | CI-TOOLCHAIN-F01 | The linter/toolchain coupling has **no early detector**: dependabot's `github-actions` ecosystem updates `uses:` refs, not `env:` literals, so `GOLANGCI_LINT_VERSION` rots silently until the next Go minor reds every PR at once (~6-monthly). Candidate: a text gate comparing the pinned linter release's go.mod `go 1.N` directive against the toolchain CI resolves, or an updater that watches the literal | **[autonomous]** | D-158 | deliberately out of scope of the fix lane: three lanes were parked behind it, and a new gate belongs with `hack/lint/**`, which was owned by a concurrent lane | | BASH32-F01 | **DONE** — three `hack/**` gate scripts used bash 4+ features with no version guard; under stock macOS `/bin/bash` 3.2 `hack/docs/truthlag_pins_test.sh` died at its `declare -A`, skipped its final `OK:` banner and **exited 0**, so `task docs-gates` (and `task check`) read a gate that certified almost nothing as green. Fixed by a shared, per-script-parameterised `hack/lib/require-bash.sh` floor (4.0 / 4.0 / 4.4), enforced by a new `hack/lint/bash_version_guard_test.sh` wired as `task check` stage 20 (D-154) | **[autonomous]** | — | found *by* the AUD2 wave's macOS runs, not by any audit: CI is ubuntu/bash 5, so the hole is LOCAL-only and no CI lane could have surfaced it | -| UNIV-COSIGN | **DONE (D-160)** — `hack/release/install_cosign_pin_test.sh` graded the D-153 signer pin **existentially** ("*some* `cosign verify-blob` in this file is pinned") where the published guarantee is **universal**, so a **second, unpinned** invocation passed: measured before the fix on scratch copies of all three graded files, rc=**0**/**0**/**0**. `has_flag` grepped the whole folded extraction so a pinned sibling satisfied it, `one_value`'s `sort -u` collapsed the agreeing values, §0 printed the invocation count without asserting it, and 4b/5d's stub-log greps were positive-only — the same shape at runtime. `SECURITY.md` had **no invocation-level grading at all**, only the drift comparison. Closed by one predicate (`pin_violations`) applied to **every** invocation in **all three** files plus its runtime twin, with fail-CLOSED classification of anything it cannot place, mutation-proven by eight mutants per file chosen for **branch** coverage (second-unpinned / second-pinned / off-command-position / no-candidates / fold-broken / no-invocations / empty-identity-regexp / foreign-issuer) plus a prose-exemption control. The check compares each invocation's **value** against SECURITY.md's published pair, not just flag presence: `--certificate-identity-regexp ''` carries the flag, matches every Fulcio identity, and slips past `one_value`'s `sort -u` because an empty capture is not a line. **CORRECTION TO THE RECORDED REMEDY — do not implement it:** the filed remedy "assert the extracted invocation count is exactly 1 per graded file" is **factually wrong and would red `main` on landing**, because `SECURITY.md` legitimately publishes **two** invocations (`SECURITY.md:86` over the archive and `:93` over `checksums.txt`, which is what covers the SBOMs listed inside it). The property is universal, not a count. **Second round (UC-01..UC-04), caught by independent review:** the first fix reproduced the same existential defect one scope down — per **line** instead of per **file** — so an unpinned call CHAINED onto a pinned one (`&&`, `;`, a pipe, or backslash-folded) passed, and the **full gate exited 0** on `SECURITY.md`, which has no runtime twin. Closed by per-**occurrence** grading (`MULTI-OCCURRENCE`), by comparing **every** value of every flag rather than the greedy-last (an empty regexp placed first was masked by a correct one placed second), and by diagnosing quote style separately (`UNQUOTED-VALUE`) so a correctly pinned double-quoted call is accepted instead of being refused with a false "empty regexp" reason. **Third round (UC-05..UC-09):** `occurrence_count` read *absence of a second token* as *proof of singularity*, so `cosign "verify-blob"` / `cosign 'verify-blob'` / `cosign verify-blob""` hid a chained unpinned call — **rc=0 on all three files at whole-gate level** against the round-2 gate (`A && B` short-circuits, so `set -e` never fires and even the runtime twin missed it). Fixed by stripping shell quotes before the compare, **explicitly a spelling patch, not a terminator**: a structural terminator was ruled out with evidence, because both scripts legitimately end their real invocation with an or-else `die` tail, so separator-based refusal would red the real files. Since completeness is unavailable, **the `PASS:` banner no longer claims it** — it now reports OBSERVED counts per file, lists only ASSERTED properties (each mutation-proven), and states the NOT-ASSERTED residual in the same breath, so an unknown fifth spelling leaves the gate *incomplete* rather than *wrong*. Also: MULTI-OCCURRENCE now says TOKENS and names trailing comments as a cause (it was false as printed), and SC1087 silenced | **[autonomous]** | AUD2-F01, D-153 (the pinned value) | demonstrated by a reviewer *on* the AUD2-F01 lane and out of its scope — F01 added a third graded file to a gate whose quantifier was already wrong, so fixing the quantifier is a change to the checker, not to any checked file (all three are byte-unchanged) | +| UNIV-COSIGN | **DONE (D-160)** — `hack/release/install_cosign_pin_test.sh` graded the D-153 signer pin **existentially** ("*some* `cosign verify-blob` in this file is pinned") where the published guarantee is **universal**, so a **second, unpinned** invocation passed: measured before the fix on scratch copies of all three graded files, rc=**0**/**0**/**0**. `has_flag` grepped the whole folded extraction so a pinned sibling satisfied it, `one_value`'s `sort -u` collapsed the agreeing values, §0 printed the invocation count without asserting it, and 4b/5d's stub-log greps were positive-only — the same shape at runtime. `SECURITY.md` had **no invocation-level grading at all**, only the drift comparison. Closed by one predicate (`pin_violations`) applied to **every** invocation in **all three** files plus its runtime twin, with fail-CLOSED classification of anything it cannot place, mutation-proven by eight mutants per file chosen for **branch** coverage (second-unpinned / second-pinned / off-command-position / no-candidates / fold-broken / no-invocations / empty-identity-regexp / foreign-issuer) plus a prose-exemption control. The check compares each invocation's **value** against SECURITY.md's published pair, not just flag presence: `--certificate-identity-regexp ''` carries the flag, matches every Fulcio identity, and slips past `one_value`'s `sort -u` because an empty capture is not a line. **CORRECTION TO THE RECORDED REMEDY — do not implement it:** the filed remedy "assert the extracted invocation count is exactly 1 per graded file" is **factually wrong and would red `main` on landing**, because `SECURITY.md` legitimately publishes **two** invocations (`SECURITY.md:86` over the archive and `:93` over `checksums.txt`, which is what covers the SBOMs listed inside it). The property is universal, not a count. **Second round (UC-01..UC-04), caught by independent review:** the first fix reproduced the same existential defect one scope down — per **line** instead of per **file** — so an unpinned call CHAINED onto a pinned one (`&&`, `;`, a pipe, or backslash-folded) passed, and the **full gate exited 0** on `SECURITY.md`, which has no runtime twin. Closed by per-**occurrence** grading (`MULTI-OCCURRENCE`), by comparing **every** value of every flag rather than the greedy-last (an empty regexp placed first was masked by a correct one placed second), and by diagnosing quote style separately (`UNQUOTED-VALUE`) so a correctly pinned double-quoted call is accepted instead of being refused with a false "empty regexp" reason. **Third round (UC-05..UC-09):** `occurrence_count` read *absence of a second token* as *proof of singularity*, so `cosign "verify-blob"` / `cosign 'verify-blob'` / `cosign verify-blob""` hid a chained unpinned call — **rc=0 on all three files at whole-gate level** against the round-2 gate (`A && B` short-circuits, so `set -e` never fires and even the runtime twin missed it). Fixed by stripping shell quotes before the compare, **explicitly a spelling patch, not a terminator**: a structural terminator was ruled out with evidence, because both scripts legitimately end their real invocation with an or-else `die` tail, so separator-based refusal would red the real files. Since completeness is unavailable, **the `PASS:` banner no longer claims it** — it now reports OBSERVED counts per file, lists only ASSERTED properties (each mutation-proven), and states the NOT-ASSERTED residual in the same breath, so an unknown fifth spelling leaves the gate *incomplete* rather than *wrong*. **R3-01, found by review in the very paragraph that added that banner:** the backticked-mention exemption keys on the substring appearing **anywhere on the line** and is tested first, so a line carrying a backticked mention AND live calls is exempted — `pin_violations` empty, whole gate rc=0. Not patched (narrowing it needs the markdown/quote parsing that produced UC-01/02/03); **disclosed as the FIRST and most reachable residual in the banner**, with exempted lines no longer described as "prose". Also: MULTI-OCCURRENCE now says TOKENS and names trailing comments as a cause (it was false as printed), and SC1087 silenced | **[autonomous]** | AUD2-F01, D-153 (the pinned value) | demonstrated by a reviewer *on* the AUD2-F01 lane and out of its scope — F01 added a third graded file to a gate whose quantifier was already wrong, so fixing the quantifier is a change to the checker, not to any checked file (all three are byte-unchanged) | Sizing, from the S03 implementer's reading of the call site: `verify_cosign()` (`hack/release/verify-artifacts.sh:118–125`) has the byte-identical unpinned