diff --git a/CHANGELOG.md b/CHANGELOG.md index 1930ddc..757977e 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -87,6 +87,11 @@ repository still gets a decision, never by following the link; no release carrie - :memo: docs(openspec): amend AUD2-S03 to the shipped pin and log D-153 (SEC-03) - :memo: docs(audit): document the AUD2 gate and correct stale line counts (F4, F6) - :memo: docs(backlog): mark P5-AUD2 complete (S01-S05 landed) +- :memo: docs(e11): record the tier-1 CEL ceiling and narrow E11 (E11-S01) +- :memo: docs(e11): strike set-difference unconditionally; make the graph shape contingent +- :memo: docs(e11): Shape D justifies E11 unconditionally — an encoded adjacency CEL cannot decode (F01) +- :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) ### 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 dedf4a8..3c2e3d1 100644 --- a/docs/decisions/decisions.md +++ b/docs/decisions/decisions.md @@ -159,4 +159,5 @@ project/process decisions. | D-152 | 2026-08-18 | **The 2026-08-18 audit's "Next (risk reduction)" wave is decomposed as its own epic P5-AUD2 (`openspec/specs/p5-aud2-audit-remediation/spec.md`), five stories, spec-first.** Context: `agent-context/PROJECT-AUDIT-2026-08-18.md` closed both P1 conditions the same day and v0.3.0 shipped, leaving a named but untracked wave — exec-transport trio (REL-01/02/07), REL-03 `ErrNotFound` discrimination, SEC-03 cosign identity pin, TEST-02 mutant. Options considered: **(a)** hand-fix them as loose commits (rejected — AGENTS.md rule 4 is spec-first, and REL-01 is now byte-identical across *three* audits precisely because nothing ever tracked it); **(b)** append them to the existing P5-AUD epic (rejected — that epic's exit gate is CLOSED and reopening it would make "AUD complete" a moving claim); **(c)** a new AUD2 epic keyed to this audit **(chosen)**. Three consequences recorded here so they are not re-litigated: **(1)** AUD2 has **no release-condition story** — the audit had exactly two P1s and both are already closed; **(2)** **WG-S01 is deliberately excluded** — it carries the LGTM governance marker, and GOVERNANCE says such stories are surfaced to the maintainer, which an autonomous loop's decide-and-log does not override; **(3)** AUD2's exit gate is a **`task check` stage**, not a `release-exitgate` step, because that job is `pull_request`-skipped (RELSE-08) and wiring the gate there is how AUD-S18's own stale `CHECK_STAGES` pin survived four merges. A 2026-08-10-keyed AUD2 draft exists only in the local stash `leave-aud2-not-this-epic`, was never committed, and is superseded; its still-open items (F3/F5/F7) stay Later-wave. Revert: delete the spec + backlog section; the four findings return to the audit report untracked. | | D-153 | 2026-08-19 | **The cosign signer-identity pin published in `SECURITY.md` was WRONG, not merely missing from `hack/install.sh`: the identity regexp is widened to `^https://github\.com/PlatformRelay/[Aa]ssent/` in both files (AUD2-S03 / SEC-03).** Substance first: `SECURITY.md`'s "Verify a tagged release" instructions pinned `--certificate-identity-regexp '^https://github.com/PlatformRelay/assent/'`, and an adopter who followed them on **v0.2.0 or v0.3.0 got a verification FAILURE on a genuine, correctly signed artifact** — the published recipe has been broken for every release since v0.2.0, and the natural reading of that failure is "this release was tampered with". Cause: the repository was renamed `PlatformRelay/assent` → `PlatformRelay/Assent` between v0.1.0 and v0.2.0; the keyless signing certificate's Subject Alternative Name carries GitHub's canonical casing; cosign compiles `--certificate-identity-regexp` as a Go RE2 pattern and matches it **case-sensitively**. Decoded from the published bundles: v0.3.0 and v0.2.0 sign as `https://github.com/PlatformRelay/Assent/.github/workflows/release.yaml@refs/tags/vX.Y.Z`, v0.1.0 as `https://github.com/PlatformRelay/assent/.github/workflows/release.yaml@refs/heads/main`. All three verify under the new value; independently re-confirmed with real cosign against the real v0.3.0 artifact (`Verified OK` under the new pin, exit 1 "expected SAN value to match regex" under the old). Options considered: **(a)** ship the pin byte-identical to the published-but-broken value and file the breakage as a follow-up (rejected — it would land a green gate asserting a guarantee that fails closed on this project's own releases, D-124's defect one level up); **(b)** case-insensitive `(?i)` (rejected — wider than the defect and it silently accepts casings GitHub never issues); **(c)** an explicit `[Aa]` class in both files, dots escaped (chosen). Not widened otherwise: the `^` anchor and the owner/repo scope stand, so another owner, an `assent-mirror` typosquat, another forge and an unescaped-dot host all still fail. Enforcement, per D-128: **one** published truth — `hack/release/install_cosign_pin_test.sh` extracts the pair from `hack/install.sh` and `SECURITY.md`, requires exactly one distinct value per file, reddens on drift, and (this is the assertion that would have caught the defect) matches the pin against the three **real** SANs above, committed as offline fixtures, plus six negatives. Extends D-110 (bundles beside archives) and D-109; the maintainer-path twin at `hack/release/verify-artifacts.sh:124` is still unpinned and is tracked in the backlog, not fixed here. Revert: restore `'^https://github.com/PlatformRelay/assent/'` in both files — which re-breaks verification of v0.2.0 and every later release, so revert only together with a repo rename back to lowercase. | | D-154 | 2026-08-23 | **Every `hack/**` script that uses a bash 4+ feature declares a PER-SCRIPT version floor via the shared `hack/lib/require-bash.sh`, because one of them was a silent local FAIL-OPEN under stock macOS bash 3.2 (BASH32-F01).** Substance first: `/bin/bash hack/docs/truthlag_pins_test.sh` on macOS printed 20 `PASS` lines, died at its `declare -A ex_s09_prefix_hint=(…)`, never printed its final `OK: all truth-lag pins green` banner — and **exited 0**. Its caller `task docs-gates`, and therefore `task check`, read that as a green gate, and AGENTS.md rule 4 makes a green local `task check` a per-commit precondition; CI is ubuntu/bash 5, so nothing merges through this path, which is precisely why it survived. Mechanism, measured on bash 3.2.57: 3.2 has no associative arrays, so under `set -u` it re-reads `declare -A x=([k]=v)` as an INDEXED array assignment and evaluates the subscript `k` **arithmetically**, hitting "unbound variable"; the shell terminates the script and the exit status is 0. Two theories were disproved en route and are recorded so they are not re-explored: the `trap … EXIT` status-swallow (3.2 propagates 1 through an EXIT trap correctly) and `set -e` (the script runs `set -uo pipefail`). The other two affected scripts fail CLOSED, but only incidentally: `hack/release/verify-artifacts.sh:202`'s literal is EMPTY, so there is no subscript to evaluate and it degrades to `declare: -A: invalid option`, which its `set -e` turns into exit 2 (measured with a `--dist` that reaches line 202 — an unreachable dist exits 1 much earlier); `hack/validate-schemas-stock.sh`'s `mapfile` degrades to "command not found" and it exits 1. Populating an empty literal or dropping `-e` silently converts a closed failure into the open one, so "how this construct happens to degrade" is not a guarantee worth depending on. Options considered: **(a)** one blanket repo-wide floor (rejected — the binding minimum differs per feature: `declare -A` 4.0, `local -n` 4.3, `mapfile -d ''` 4.4; a blanket floor both refuses shells that could run the 4.0 gates and hides which feature actually binds); **(b)** rewrite the three scripts to be 3.2-compatible (rejected — associative arrays and `mapfile` are the right tools here, a rewrite is a large risky change to scripts whose correctness IS the product, and it does nothing about the next gate author); **(c)** copy the existing inline `BASH_VERSINFO` guard from `hack/audit/aud2_exitgate_test.sh:71` into each script (rejected as the *only* measure — it duplicates the explanation three more times and still leaves the next author to rediscover the hazard); **(d) chosen** — a shared `require_bash [.] ` helper, called with each script's own correct floor (4.0 / 4.0 / 4.4), plus a meta-gate. Enforcement, per D-128, is one place: `hack/lint/bash_version_guard_test.sh`, wired as `task check` stage **20** and pinned in `hack/audit/exitgate_test.sh`'s `CHECK_STAGES` in the same commit. It scans every `hack/**/*.sh` for command-position bash 4+ constructs, requires a guard on each, requires the declared floor to be at least the feature's own minimum, and — the assertion that makes the rest non-vacuous — requires the scan to still find all four known feature-using files, so a typo in a detection pattern reds instead of quietly matching nothing. Its own negative control mutates real copies of the three scripts with the guard lines stripped and asserts they are flagged. `hack/audit/aud2_exitgate_test.sh` keeps its inline guard and is accepted by the gate as guarded; adopting the helper there is a follow-up, not this lane. Stated limits: the gate sees only command-position constructs in `hack/**/*.sh` (not `eval`, dynamically built command names, case-modification expansions, or scripts outside `hack/`), and the exit-0 control needs a real bash 3.2 — present on macOS, absent on CI ubuntu, where it SKIPs **loudly** rather than passing silently. Accepted behaviour change: under 3.2, `hack/release/verify-artifacts.sh --help` now refuses instead of printing usage. Revert: delete the guard calls — `task check` then silently stops certifying the docs truth-lag pins for every contributor whose `bash` is 3.2. | +| 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). | diff --git a/docs/planning/open-questions.md b/docs/planning/open-questions.md index b0f47f1..6695ea6 100644 --- a/docs/planning/open-questions.md +++ b/docs/planning/open-questions.md @@ -34,3 +34,5 @@ | OQ-30 | **RESOLVED (D-148, 2026-08-16): (b) — keep the guard skipped on `pull_request`; the real mechanism (merge-direction-dependent ordering hazard) is now recorded in D-125/D-136.** Analysis retained below for the record. Original text: Is a `pull_request`-scoped CHANGELOG drift gate viable now that D-136 skips merge commits? The guard is retained with NO demonstrated reason — its original one is dead and its proposed successor measures false.** D-125 skipped the gate on `pull_request` because `refs/pull/N/merge`'s synthetic merge subject rendered into the generated changelog, so no committed `CHANGELOG.md` could match. **D-136 killed that reason** — that commit is a merge commit and is now skipped. The successor reason drafted in D-136's first version — "the merge ref also carries every commit landed on `main` since the branch forked, so the render is a union the branch's file cannot match, red by construction" — was then measured four ways and **could not be made true**: (1) PR #41's **live** `refs/pull/41/merge` (`491bb2a`, head `49eebb3` into base `7513d79`) rendered with the new `cliff.toml` → `verify-changelog: ok`, **0 diff lines**; (2) the direct counterexample — the same head merged into a `main` that **had** moved (`1d8aa60`, containing PR #40) → `verify-changelog: ok`, **0 diff lines**, i.e. not red with the base moved; (3) a synthetic sandbox where base and lane each add a commit to the **same** cliff group and each regenerate → `CONFLICT (content): Merge conflict in CHANGELOG.md`, so the PR is unmergeable, GitHub mints no merge ref, and the gate never runs. (4) **The strongest one, taken last and re-run rather than transcribed:** GitHub RE-MINTED `refs/pull/41/merge` against the moved base after all of the above. Re-fetched live — `7715bf7`, head `ee5e527` into base `1d8aa60` — and put through the real gate script: **`verify-changelog: ok`, 0 diff lines, 0 merge subjects rendered.** That is not a simulation: it is the exact artifact a `pull_request`-scoped gate would evaluate, with the base moved past the fork point AND after the lane had merged `main` in — the direction the finding below shows is hazardous — and it is green. Measurement (1)'s `491bb2a` at base `7513d79` is its stale predecessor, kept only to show the result did not depend on the base standing still. **Mechanism the dead premise overlooked:** the merge ref's `CHANGELOG.md` is not "the branch's committed file" — it is the three-way MERGE RESULT, which already contains the base's lines, because the file is merged like any other. So base movement ends in clean-and-matching or conflict-and-no-merge-ref. **The third outcome EXISTS, and merge DIRECTION decides it — measured while writing this row.** A clean textual auto-merge whose line order differs from git-cliff's topological order is red with no author error, and it reproduced immediately: merging `origin/main` **into the lane** (lane as first parent) auto-merged `CHANGELOG.md` without conflict and then failed `verify-changelog` on pure ordering — one `docs(compare)` line moved and PR #40's lines landed in a different position. The SAME two commits merged in the **merge-ref direction** (base `1d8aa60` as first parent, measurement (2) above) matched exactly. git-cliff's traversal follows parent order, so first-parent choice changes the render. This does not revive the retired premise — GitHub always mints the merge ref base-first, which is the direction that matched — but it means the clean-and-matching outcome is a property of that direction, measured on two merges, not a proof. It also re-confirms D-125's surviving rule: regenerate after any `git merge origin/main`. **Still untested:** behaviour on `pull_request_target`, on a PR from a fork, and after a force-push that re-mints the merge ref. **Counter-evidence for enabling it:** the only red reproduced on any merge ref was a branch that had not run `task changelog-write` for its own commits — a **true positive the gate exists to catch**, which argues the PR placement may now be correct rather than merely harmless. **Correction, folded in from the PR #41 review because it belongs in the row and not only in a review thread:** that review first read these greens as "the evidence points toward the PR gate being viable", and then took it back as **one measurement short**. The direction finding above supplies a false-positive mechanism it had not considered — a clean textual auto-merge whose line order differs from git-cliff's topological order reds with no author error and no author fix available. Four green measurements are therefore NOT a green light; on today's evidence the gate would not be enabled. **Ruling needed (deliberately not taken here, operator's call):** (a) enable the step on `pull_request` and delete the guard; (b) keep the guard and record the real reason once someone finds one; or (c) keep the guard permanently on cost/noise grounds and say so, rather than on a mechanism. Not to be resolved by deleting the guard on the strength of these three measurements alone — they show the claimed failure did not reproduce, not that no failure exists. | Before any change to the `pull_request` guard on the changelog step in `.github/workflows/verify.yaml`; not a release blocker — the guard is fail-safe (the gate runs locally in `task check` and on push-to-main) | Raised by the PR #41 review (finding CL-02) against D-136's first draft; measurements reproduced independently before recording. Sites now pointing here: `Taskfile.yml` `check:`, `.github/workflows/verify.yaml`, `hack/release/README.md`, `hack/release/changelog_gate_test.sh` §3. See [D-125](../decisions/decisions.md) and [D-136](../decisions/decisions.md) | | OQ-31 | **RESOLVED (D-146, 2026-08-16): (a) — "zero forge writes" stays absolute; the BLOCK is surfaced via a required CI job status reading the already-emitted `DecisionRecord`, not via a forge write.** Analysis retained below for the record. Original text: May the GUARD-1 self-edit BLOCK path write a summary or supersession note, or is "zero forge writes on a self-modifying MR" absolute? If it is absolute, what channel carries the BLOCK to the human reviewer — given that no thread is posted and the exit code is `0`?** Raised by RELI-01 ([D-138](../decisions/decisions.md)) and deliberately left **UNDECIDED**. The tension is real in both directions. **For absolute:** `openspec/specs/p5-aud-audit-remediation/spec.md` pins *"the decision is BLOCK with zero forge writes (GUARD-1 dominance over the gap-degrade)"* as a frozen acceptance criterion, and the guard exists so that an MR editing `.assent/**` cannot make assent vouch for its own policy — any write is a write the MR's own content influenced. **Against absolute:** the only human-visible surface then keeps whatever the previous run said, which today can be `✅ Decision: APPROVE`, so the guard's output is *invisible* to the reviewer it protects, and D-130's compensating control (a REVIEW rerun upserts the summary and adds an unresolved discussion) does not reach this path because no thread is posted. Zero *authority* writes need not mean zero *communication*. **Options, none taken here:** (a) keep it absolute and carry BLOCK on a non-forge channel — a non-zero exit code, or a required CI job status; (b) permit exactly one write, a fixed-text supersession/BLOCK note with no policy-derived content, which cannot be steered by the MR; (c) permit the summary upsert but not the thread. (b) and (c) both **reopen the frozen criterion above and need an openspec change proposal first** — spec before code. Note that (a) changes an exit-code contract wrapper scripts rely on ([`docs/usage/cli.md`](../usage/cli.md)), so it is not the free option it looks like. | Before the RELI-01 fix lands (v0.2.1) | Found by the 2026-08-09 audit's reliability lens; recorded in [D-138](../decisions/decisions.md). Evidence: `cmd/assent/run.go` step-9 GUARD switch, `openspec/specs/p5-aud-audit-remediation/spec.md`, `openspec/specs/p5-e5-provider-host/spec.md` REQ-E5-S08-03 | | OQ-32 | **RESOLVED (D-147, 2026-08-16): (b) — add a host-side secret resolver (process env / file path / hosted store); repo-side config gains only an opaque, host-allowlisted reference name, never a literal credential or URL pairing. ADR amending ADR-0015 §7 required before code.** Analysis retained below for the record. Original text: No provider transport can carry a credential, so NO provider can call Entra ID, Keycloak, or any token-authenticated IdP directly — and nothing says so. Found while designing P5-DEM (D-142). Verified across three surfaces that agree: `CallHTTP` (`internal/provider/transport.go`) sets **only** `Content-Type: application/json` — no header map, no bearer token, no client certificate; the repo-side provider schema (`schemas/policy/v1alpha1/config.schema.json` `$defs/provider`) is `additionalProperties:false` over exactly `{type, url, failure}`, so there is nowhere to put one; and `ScrubEnv`/`ScrubArgv` build the exec child's environment **from scratch** and refuse any name matching `(?i)(TOKEN\|SECRET)` **even when explicitly configured**, so the exec tier cannot carry one either. **This is not a bug — it is ADR-0015 §7 working exactly as designed**, and Spike C's `TestIsolation` proves it against a deliberately hostile provider that exfiltrates its whole environment and stdin. **What has never been written down is the consequence:** Entra ID and Keycloak both require a bearer token on every call, so the only shape that works today is a **broker** — a service holding the IdP credential *itself*, reachable by assent without one (loopback/sidecar, or mTLS terminated outside assent's transport). That is arguably the *correct* architecture: the credential never enters the decision path and a compromised provider's blast radius stays bounded. But it is undocumented, and it **narrows what `docs/vision.md:67` promises** ("pluggable providers: Keycloak, LDAP, GitLab/GitHub groups, ownership files, custom plugins") and what ADR-0004 §1 planned ("OIDC/Keycloak group lookup, LDAP" as builtins — never shipped). `docs/architecture/c4-context.md:19` is currently the **only** place stating the truth: *"Keycloak / LDAP: no builtin — reachable only via the generic HTTP/exec provider transport."* **Ruling needed (deliberately not taken):** **(a)** bless the broker pattern, document it in the provider-author guide, and amend `docs/vision.md:67` + ADR-0004 §1 to stop implying direct IdP calls — **RECOMMENDED**: costs nothing, keeps ADR-0015 §7 and the isolation proof intact, and is what DEM-S02/DEM-S03 are already written against; **(b)** add a narrow repo-side credential channel (header or secret-ref) to the HTTP transport — **reopens a frozen schema AND the trust boundary the hostile-provider isolation proof rests on**, and would need its own ADR; **(c)** state the limitation and add nothing. Note this is **not** merely a docs question under (a): a reader of the vision page today would reasonably budget a Keycloak integration as "configure a builtin" and discover mid-implementation that they must also deploy and operate a broker. **Not to be resolved by quietly adding a header field** — that is option (b) and it is a trust-boundary change. | Before DEM-S02 publishes the provider-author guide (the guide must state one of these answers); **not** a release blocker — the current behaviour is fail-safe, just undocumented | Found designing [P5-DEM](https://github.com/PlatformRelay/assent/blob/main/openspec/specs/p5-dem-demo-repos/spec.md) (judgment call (e)); recorded in [D-142](../decisions/decisions.md). Evidence: `internal/provider/transport.go` `CallHTTP`/`ScrubEnv`/`ScrubArgv`, `schemas/policy/v1alpha1/config.schema.json` `$defs/provider`, `docs/planning/spikes/spike-c-provider.md` § Isolation evidence, ADR-0015 §7, ADR-0004 §1, `docs/vision.md:67`, `docs/architecture/c4-context.md:19` | +| OQ-35 | **`entry` / `oldEntry` bind whole-entry value trees under `assent test` but a bare scalar under `assent run` — do we extend the binding to the run path, or narrow the documented contract?** `docs/planning/predicate-scope.md` describes `entry` as "head-state value tree of the containing `EntryRef`" with no qualifier, and `internal/core/aggregate/evaluate.go` `bindLeafActivation` binds `toCEL(entryOr(ch.Entry, ch.New))` — falling back to the change's **scalar** `new`/`old` when `ch.Entry` is nil. The **only** writer of `EvalChange.Entry` is `internal/adoptertest/entrytree.go` `populateEntries` (called from `adoptertest.go:288`); `internal/evaldecode.BuildEvaluationInput` — the sole production builder, reached from `cmd/assent/evaldecode.go` — never sets it, and `cmd/` contains no reference to `EntryConfig`, `DiffEntries` or `change.Entries` at all (`assent run` calls the document-mode `change.Diff` via `changeSetForGoverned`). **Consequence:** a rule such as `oldEntry.acls.filter(a, !(a in entry.acls)).size() == 0` passes in `assent test` and, in production, hits a no-such-attribute error on a scalar → `predicate.error` → REVIEW. The direction is fail-safe, so this is not urgent and not a release blocker; what it is not is *documented*, and an adopter who validates a pack with `assent test` has no signal that the rule will never fire in `assent run`. **Ruling needed (deliberately not taken):** **(a)** extend entry reconstruction to the `assent run` path so the two agree — the honest fix, but it puts collection-mode entry derivation on the live decision path and needs its own story; **(b)** state the limitation in `predicate-scope.md` and add an `assent lint` hard error for a rule that navigates `entry`/`oldEntry` as an object — cheap, keeps the contract truthful, costs adopters the capability; **(c)** leave as is (rejected on sight — it is a silent test/production divergence). **Not to be resolved by a fixture that only runs under `assent test`** — that is precisely the "test that cannot fail" this repo's reviews keep finding. | **Gates nothing.** D-156 records that both resolutions strike the set-difference shape (extending makes CEL express it; narrowing makes it an input-availability failure a Rego module inherits unchanged), and the graph-relationship shape needs no entry tree — its adjacency arrives as a flat `cardinality: set` fact. What is actually at stake is a silent `assent test` / `assent run` divergence: a pack an adopter validates green can contain a rule that never fires in production. Blocks nothing today. | Found writing [the tier-1 ceiling record](rego-tier-ceiling.md) (E11-S01); recorded in [D-156](../decisions/decisions.md). Evidence: `internal/core/aggregate/evaluate.go` (`bindLeafActivation`, `entryOr`), `internal/adoptertest/entrytree.go`, `internal/evaldecode/evaldecode.go` `BuildEvaluationInput`, `cmd/assent/run.go:293` `changeSetForGoverned`, `docs/planning/predicate-scope.md` | +| 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 and dynamic navigation into it — is a mapping-shaped fact value in-contract or out?** `schemas/provider/v1alpha1/response.schema.json` freezes `declaration.type` to `boolean \| string \| integer \| principal` and `cardinality` to `single \| set`; `value` itself carries **no** JSON-Schema type constraint ("shape governed by declaration.type/cardinality") and `provider.ResolveFactsChecked` cross-checks the *declaration*, never the value. Meanwhile `builtin/repo-file` maps each requested output to a **top-level key** of the resolved file via `readMapping` (`map[string]any` from `yaml.Unmarshal`), so a top-level key holding a mapping is emitted verbatim; `factsToCEL`/`toCEL` bind it as a CEL map; and `internal/lint/facts_ref.go`'s D-051 shape check permits arbitrary navigation *past* `.value` (`selectChainFields` stops the chain at an index), so `facts.registry.topics.value[string(new)].retentionMs` is lint-clean and compiles. **So a keyed cross-manifest join works today under a declaration that cannot describe it.** This is not hypothetical polish: D-156 struck the cross-manifest shape from E11's scope partly on the strength of that spelling, and it is the one leg of that strike resting on an undeclarable value. **Ruling needed (deliberately not taken):** **(a)** add `object` (or `map`) to the declaration `type` enum — an announced additive change to a frozen schema, needs its own openspec change and `API_STABILITY.md` entry, and widens what a hostile provider may inject into the decision path; **(b)** state that a fact value must match its declared scalar/set shape and enforce it host-side in `ResolveFactsChecked` (a mismatch → `invalid`, value dropped) — fail-safe and closes the gap, but it **breaks** the keyed-join spelling above and returns the cross-manifest sub-shape B2 to the ceiling; **(c)** document the status quo as intentional — the declaration describes the *leaf* type and navigation into a container is the author's risk (weakest: it makes the declaration cross-check advisory for exactly the values that carry the most structure). | Not a release blocker — the current behaviour is fail-safe either way (an absent key errors → REVIEW). **Gates nothing in D-156:** it touches only the *second* spelling of cross-manifest sub-shape B2, which is struck on its first spelling (a purpose-built provider) regardless, and the graph-relationship shape needs only a flat `cardinality: set` fact. Relevant to anything that later publishes the provider-author guide (DEM-S02). | Found writing [the tier-1 ceiling record](rego-tier-ceiling.md) (E11-S01); recorded in [D-156](../decisions/decisions.md). Evidence: `schemas/provider/v1alpha1/response.schema.json` (`declaration.type`/`cardinality`, unconstrained `value`), `internal/provider/resolve.go` `ResolveFactsChecked`, `internal/provider/builtin/repo_file.go` (`answerRepoFile`, `readMapping`), `internal/core/aggregate/evaluate.go` `factsToCEL`/`toCEL`, `internal/lint/facts_ref.go` (`checkFactsShape`, `selectChainFields`) | diff --git a/docs/planning/rego-tier-ceiling.md b/docs/planning/rego-tier-ceiling.md new file mode 100644 index 0000000..c65c0db --- /dev/null +++ b/docs/planning/rego-tier-ceiling.md @@ -0,0 +1,614 @@ +# The tier-1 (CEL) ceiling — where `assert` runs out, with concrete rules + +**Owner:** E11-S01 (`openspec/specs/p5-e11-rego-backend/spec.md`). **Authority:** D-141 +(implementation unlock), D-156 (this record). **Satisfies:** REQ-E11-S01-01 (a concrete rule +per named shape, its attempted CEL leaf, and the specific reason it fails) and +REQ-E11-S01-02 (any shape found CEL-expressible is **struck from E11's scope**). + +This document is a **scope-reduction instrument**, not a feature argument. D-017 required +"each ported rule tries CEL first, the backend is built when a concrete rule demonstrably +exceeds the tier-1 ceiling". D-141 lifted that as a *gate*; it did not lift it as a *design +need*. Two of the four shapes `openspec/specs/later-phases.md:284` names turn out not to +justify a second backend, and they are struck here. + +Every claim below is checked against **the CEL surface this repository actually binds** — not +CEL in general. The ceiling is set by what assent *binds*, not by what `cel-go` can parse. + +--- + +## 1. The tier-1 surface, as actually bound + +`internal/core/aggregate/evaluate.go` `newEvalEnv` builds the environment with **eleven +variables and nothing else**: + +```go +cel.NewEnv( + cel.Variable("old", cel.DynType), cel.Variable("new", cel.DynType), + cel.Variable("entry", cel.DynType), cel.Variable("oldEntry", cel.DynType), + cel.Variable("path", cel.StringType), cel.Variable("kind", cel.StringType), + cel.Variable("file", cel.StringType), cel.Variable("env", cel.StringType), + cel.Variable("changes", cel.ListType(cel.DynType)), + cel.Variable("facts", cel.DynType), cel.Variable("mr", cel.DynType), +) +``` + +That matches the frozen predicate-scope table (`docs/planning/predicate-scope.md`) exactly. +**Zero extension libraries and zero custom functions are registered** — no `ext.Bindings`, no +`ext.Math`, no `ext.Lists`, no `ext.Strings`, no optional types. Five further properties bound +the surface, and each is load-bearing below: + +| Property | Where it is fixed | +| --- | --- | +| Combinators are **boolean**, not dataflow: `all`/`any`/`not` combine leaf *truth values*; no value crosses a leaf boundary | `internal/core/aggregate/asserttree.go` (`walkAssertTreeDepth`, depth ceiling 32) | +| One leaf is compiled and evaluated **once, standalone**, under a fixed cost budget of `1_000_000` | `evaluate.go` `celCostBudget`, `evalLeaf` | +| The evaluation unit is **one file** | `change.ChangeSet` is documented "the canonical, order-stable set of changes for **one file**" (`internal/change/diff.go:129`); `assent run` takes exactly one `--subject file:` (`cmd/assent/run.go:266`) and diffs that file alone (`:293`) | +| `facts` may be addressed **only** as a static `facts...value…` dot chain | `internal/lint/facts_ref.go` — `facts['x']` and bare `facts` are `facts-reference-syntax` hard errors; a third segment other than `value` or an envelope escape is `facts-reference-shape` (D-051 Option B) | +| Ordering raw text is refused in **every** spelling (`a < b`, `string(a) < string(b)`, `bytes(a) < bytes(b)`) | `evaluate.go` `textOrderGuard` (D-131, ADR-0013 Amendment 1) | + +### 1.1 Function census — measured, not recalled + +A throwaway probe reconstructed `newEvalEnv` byte-faithfully against the pinned +`github.com/google/cel-go v0.31.0` and compiled each candidate. Results: + +| Compiles | Rejected (`undeclared reference`) | +| --- | --- | +| `size(...)`, `filter`, `map`, `all`, `exists`, `exists_one`, `in`, `has` | `sum(...)` and `.sum()` | +| chained comprehensions — `changes.filter(c, …).all(c, …)` | `math.*` (the `ext.Math` library is not registered) | +| the **value binder** `[expr].all(v, …)` — CEL's standard poor-man's `let`: computes `expr` once and binds it to `v` | `reduce`, `transformList`, `transformMap`, two-var `all(i, x, …)` — every construct that could vary an iteration count | +| nested comprehensions — `changes.all(c, changes.exists(d, …))` | `reduce(...)` — no fold of any kind | +| `oldEntry.acls.filter(a, !(a in entry.acls))` | `lists.*` (`ext.Lists` is not registered) | +| `facts.registry.topics.value[string(new)].retentionMs` | `cel.bind(...)` (`ext.Bindings` is not registered) | +| `string(new) in facts.registry.topics.value` | `.?field` / `orValue` (optional syntax unsupported) | +| `matches`, `startsWith`, `endsWith`, `contains`, `timestamp`, `duration`, `int`, `double`, `+` on strings | `split`, `substring`, `indexOf` — every string **decomposition** function (`ext.Strings` is not registered). Read §1.1's note: this does **not** block working with encoded values | +| | `now`, `rand` — non-determinism is not reachable (rule 7 holds) | + +The string row is worth reading carefully, and **also worth not over-reading** — an earlier +draft of §5 did exactly that. The surface can **test** a string (`matches`, `startsWith`, +`endsWith`, `contains`) but cannot **take it apart**: no `split`, no `substring`, no `indexOf`, +no character indexing. That is a real absence. It is **not**, however, a barrier to working with +encoded values, because `+` on strings and `in` are both stdlib: over a finite in-input +candidate set you can always **rebuild** the string you were going to decode and test membership +instead. §5 shows that construction recovering an edge's far end and detecting a 3-cycle without +any decomposition function. What the absence does cost is spelling *generic* string surgery, +which no shape in this record needs. + +**Reproduction** (deliberately not committed — it would add a dependency edge E11-S03 has not +been authorised to add): copy `newEvalEnv` verbatim into a nested throwaway module pinned to +`cel-go v0.31.0`, call `env.Compile` on each expression above, and print the issue set. The +root `go.mod`/`go.sum` must stay byte-unchanged and `go list ./...` must not enumerate the +probe — the same containment E11-S00 uses. The expression list is exactly the leaves quoted in +§2–§5, plus these five, whose verdicts carry §5: + +```text +REJECTED facts.graph.edges.value.exists(s, s.split("|")[0] == string(new)) undeclared 'split' +REJECTED facts.graph.edges.value.exists(s, split(s, "|")[0] == string(new)) undeclared 'split' +REJECTED facts.graph.edges.value.exists(s, s.substring(0, s.indexOf("|")) == ...) undeclared 'substring' +REJECTED facts.graph.edges.value.exists(s, s.indexOf("|") > 0) undeclared 'indexOf' +REJECTED !transitiveClosure(entry.dependsOn).exists(d, d == entry.name) undeclared 'transitiveClosure' +COMPILES see below +COMPILES facts.graph.nodes.value.filter(m, (string(new) + "|" + m) in facts.graph.edges.value) +``` + +The last two were **evaluated**, not merely compiled, under `cel.CostLimit(1_000_000)` against +`edges: ["orders|billing","billing|ledger","ledger|orders"]` and +`nodes: [orders, billing, ledger, payments]` — yielding `true/true/true/false` and `[billing]` +respectively. Evaluation matters here: a compile-only check would have left §5's claim about +what CEL can *do* with those primitives untested. + +### 1.2 The one property the whole record rests on, measured rather than recalled + +§5's verdict — the only shape-level claim in this document with nothing behind it but itself — +reduces to a single property: **the number of iterations a tier-1 CEL expression performs cannot +be made to depend on the data.** Every expression's maximum path length is a *syntactic* +property, fixed when the rule is authored. Earlier drafts supported this with "CEL is +non-Turing-complete by design", which is a recalled argument in a section headed *measured, not +recalled*. Compiled against `newEvalEnv`: + +```text +REJECTED !transitiveClosure(entry.dependsOn).exists(d, d == entry.name) undeclared 'transitiveClosure' +REJECTED changes.reduce(a, x, a + 1, 0) > 0 undeclared 'reduce' +REJECTED [1,2,3].reduce(a, x, a + x, 0) == 6 undeclared 'reduce' +REJECTED changes.transformList(x, x).size() > 0 undeclared 'transformList' +REJECTED changes.transformMap(k, v, v).size() > 0 undeclared 'transformMap' +REJECTED changes.all(i, x, i >= 0) undeclared 'all' (no two-var form) +REJECTED cel.bind(x, changes, x.size() > 0) undeclared 'cel' +REJECTED range(3).size() == 3 / lists.range(3).size() == 3 undeclared 'range' / 'lists' +REJECTED for (x, changes) { x } reserved identifier: for +``` + +There is no fold, no user-defined function, no self-reference, no loop form, and no generator; +the four comprehension macros iterate exactly one level over one collection and cannot call +themselves. Depth must therefore be written out, and cel-go hard-caps that at a parser recursion +limit of **250** (`expression recursion limit exceeded: 250` at nesting depth 260; depth 200 +still compiles). **That is the ceiling — one property, measured nine ways.** A bounded `k`-hop +check really is an approximation when the data outruns the authored `k`: on a 4-cycle, the `k=3` +form evaluates `false` and the `k=4` form `true`. + +### 1.3 Two ceilings that are *not* expressiveness — and that Rego does not lift + +Three of the verdicts below turn on this distinction, so it is stated once, up front. + +- **Input availability.** A predicate can only reason over what is in `EvaluationInput`. + REQ-E11-S05-01 pins that a Rego module receives **the identical `EvaluationInput`**, and + `later-phases.md` fences the tier at "declared data, **no I/O**". So a rule that fails + because the data it needs is not in the input **fails identically under Rego**. That is not + a tier-1 ceiling; it is an input contract, and adding a second expression language cannot + move it. +- **Declaration vocabulary.** `schemas/provider/v1alpha1/response.schema.json` freezes + `declaration.type` to `boolean | string | integer | principal` and `cardinality` to + `single | set`. There is **no declarable object/map type**. A fact whose value is a mapping + is undeclarable, whichever backend reads it. (See residual OQ-36.) + +### 1.4 On the `assent run` path, almost every binding is a **scalar** + +This is measured, and it decides two of the five verdicts below. `assent run` diffs the +governed file in **document mode** (`changeSetForGoverned` → `change.Diff`), and document-mode +`walkNode` emits a `Change` **only where two scalars differ**: a sequence on either side, or a +map-vs-non-map type flip, returns a reason → the whole ChangeSet is **opaque** → fail-safe +REVIEW (`internal/change/diff.go`, `walkNode` and the `vSequence` leaf marker). Collection mode +(`DiffEntries`, which projects sequence elements) is reached **only** from +`internal/adoptertest`; `cmd/` references it nowhere. + +Consequently, in production: + +| Binding | Shape on the `assent run` path | +| --- | --- | +| `old`, `new` | always a **scalar** (`DecodeCanonical` of a scalar render) | +| `entry`, `oldEntry` | the same scalars — `EvalChange.Entry` is `json:"-"`, in-memory only, and `internal/adoptertest/entrytree.go` `populateEntries` is its **sole writer** (OQ-35) | +| `changes[i].old`, `changes[i].new` | always scalars, for one file | +| `facts.

..value` | a scalar, or a **flat list of scalars** under `cardinality: set`. A nested/mapping value is undeclarable (§1.2, OQ-36) | +| `mr.labels` | a flat list of strings | + +So the only *navigable value tree* a production rule can reach is a fact value, and the frozen +declaration cannot describe a nested one. Under `assent test` the picture is different — which +is the whole of OQ-35. + +**But "flat list of scalars" is not the same as "carries no structure", and the difference +decides Shape D (§5).** A `{type: string, cardinality: set}` output is fully in contract, and a +provider may put whatever it likes in each string — including an encoded edge, e.g. +`edges: ["orders|billing", "billing|ledger"]`. Every link is verified in-tree: the declaration +is legal (`schemas/provider/v1alpha1/response.schema.json`); `fact.value` carries **no** +JSON-Schema type constraint and `provider.ResolveFactsChecked` cross-checks the *declaration*, +never the value (`internal/provider/resolve.go`); outputs are operator-authored per provider +(`internal/provider/config.go`, `Outputs map[string]Declaration`); the `http` transport is live +on the plain `assent run` path with **no `--checkout`** (`cmd/assent/provider_host.go`, +`providerCallFor`); and a set fact binds as a CEL list, which ships green today. **So an +adjacency is available inside `EvaluationInput` right now — no `--checkout`, no OQ-35, no +OQ-36.** + +--- + +## 2. Shape A — multi-pass + +### A1 · Fold/aggregate over a collection — **EXCEEDS TIER 1** + +**Rule (generic).** *Bulk-change budget:* across one manifest, the **total** increase in +`partitions` contributed by a single merge request may not exceed 64; any single change is +fine, the sum is what is governed. + +**Attempted CEL leaf.** + +```cel +changes + .filter(c, c.kind == "modify" && string(c.path).endsWith("/partitions")) + .map(c, int(c.new) - int(c.old)) + .sum() <= 64 +``` + +**Why it fails.** `sum` is an `undeclared reference`. So is `reduce`, `math.sum`, and every +`lists.*` helper — none of `ext.Math`, `ext.Lists` or `ext.TwoVarComprehensions` is registered +by `newEvalEnv`, and registering one would widen the frozen predicate scope, which E11's +non-goals fence explicitly. CEL's four collection macros (`all`, `exists`, `exists_one`, +`filter`/`map`) are **boolean or shape-preserving**; none of them folds a list into a scalar. +`size()` is the *only* aggregate in the surface, so **counting is expressible and summing is +not**: `size(changes.filter(c, c.kind == "add")) <= 3` compiles and is the idiom the corpus +already uses. Every other aggregate a budget rule needs — sum, min, max, average, product — +has no spelling. + +**Why Rego lifts it.** `sum`, `max`, `min`, `count` and `product` are OPA builtins over data +already in the input; no I/O and no extra data are required. This shape is therefore a genuine +tier-2 justification and it is the **strongest** one in this record. + +**Scale note, not an expressiveness note.** Where a fold *can* be hand-simulated (see A2), the +`1_000_000` cost budget bounds how far. A cost overrun is an `evalLeaf` error → `predicate.error` +→ REVIEW, so it degrades safely; it is a scale ceiling, and it is not offered here as an +expressiveness argument. + +### A2 · A named intermediate reused across checks — **STRUCK** + +**Rule (generic).** *Compute the set of newly added ACL entries once, then assert three things +about it* (all are prod-scoped; none names a wildcard principal; none exceeds the per-MR count). + +**Attempted CEL leaf.** + +```cel +cel.bind(added, changes.filter(c, c.kind == "add"), + size(added) <= 5 && added.all(c, !c.new.contains("*"))) +``` + +**Verdict: STRUCK — CEL expresses this, by inlining.** `cel.bind` is an `undeclared +reference` (`ext.Bindings` is not registered) and the assert tree cannot carry the value +either: `all`/`any`/`not` combine leaf *booleans*, so no derived collection crosses a leaf +boundary. But both are **rewrites, not walls** — `changes.filter(c, c.kind == "add")` is a +pure, deterministic sub-expression, and re-deriving it inside each leaf is semantically +identical: + +```cel +size(changes.filter(c, c.kind == "add")) <= 5 +changes.filter(c, c.kind == "add").all(c, !string(c.new).contains("*")) +``` + +Chained and nested comprehensions both compile (§1.1) — and the surface additionally has a value +binder, `[expr].all(v, …)`, which computes the sub-expression **once** and reuses it: + +```cel +[changes.filter(c, c.kind == "add")].all(added, + added.size() <= 5 && added.all(c, !string(c.new).contains("*"))) +``` + +That compiles, and it removes the re-derivation entirely. So the residual is **legibility, not +expressiveness and not evaluation cost** — the binder answers the cost half — and legibility is +not a licence to add a second backend. A hostile reviewer will point out that a chained +comprehension *is* a second pass; that reviewer is right, and this record concedes it. **This +shape is struck more firmly than the first draft struck it**, which is exactly why only A1 +survives from multi-pass. + +--- + +## 3. Shape B — cross-manifest reference — **STRUCK, all three sub-shapes** + +This is the shape `DEM-S05` (judgment call (f), D-142) was nominated to probe. It splits into +three sub-shapes with different reasons and the **same verdict**: none of them justifies E11. + +### B1 · Membership in a registry — **STRUCK (CEL-expressible, already in the corpus)** + +**Rule (generic).** An ACL entry may only reference a topic that appears in the topic registry. + +**CEL leaf that does the job.** + +```cel +string(new) in facts.registry.topics.value +``` + +A `cardinality: set`, `type: string` output is exactly a list of names; `factsToCEL` binds a +resolved fact's `value` through `toCEL`, so it arrives as a CEL list and `in` is a standard +operator. **The *idiom* is shipped and green** — +`examples/packs/service-catalog/.assent/packs/catalog/rules/ownership.yaml:21` uses +`entry.owner in facts.author.groups.value` in the dogfood packs. Stated precisely, because the +distinction matters: that instance is an **identity** fact (the author's groups), not a +cross-manifest registry read. What the corpus proves is that a set-valued fact binds as a CEL +list and `in` decides membership over it; that the *source* of such a set can be another +manifest follows from the provider contract — any provider may return a set — not from that +example. The nearest shipped cross-manifest instance is the **keyed** form in B2. + +### B2 · Keyed attribute lookup — **STRUCK (CEL-expressible, two ways)** + +**Rule (generic).** The team requesting an ACL must own the referenced topic. + +Two spellings work today: + +```cel +# (i) a purpose-built provider returns the joined attribute directly +entry.team == facts.resource_owner.owner.value + +# (ii) index into a registry fact by a key taken from the change +facts.registry.topics.value[string(new)].retentionMs > 0 +``` + +(i) is shipped: `internal/provider/builtin/resource_owner.go` keys the lookup by the governed +entry identity and returns one `type: string, cardinality: single` fact — +`examples/archetypes/referenced-resource-ownership/` exercises it in both polarities. +(ii) compiles, and it is **lint-clean**: `internal/lint/facts_ref.go`'s D-051 shape check +permits `facts.

..value` plus arbitrary deeper navigation, and `selectChainFields` stops +the chain at the index, so a *dynamic* index past `.value` is accepted. Only an index on +`facts` itself (`facts[x]`) is a hard error. + +**Two residuals, recorded honestly, neither of which Rego fixes.** (a) Spelling (ii) relies on +a fact whose value is a **mapping**, and the frozen provider declaration has no object type +(§1.3) — the value is undeclarable, so this is a contract gap, raised as **OQ-36**, not a +backend argument. (b) The generic `builtin/repo-file` cannot supply an arbitrary registry: it +resolves a **basename** by walking up from the change anchor and maps each output to a +**top-level key** of that one file (`repo_file.go` `findMostSpecific` / `answerRepoFile`) — no +glob, no directory enumeration. So a join over "every manifest under `topics/**`" needs a +provider written for it, which is a **domain-aware join** — declined permanently by D-017 and +fenced out of E11's non-goals. Rego is on the wrong side of that fence too. + +### B3 · Same-changeset cross-file reasoning — **STRUCK from E11's justification** + +**Rule (generic).** An ACL referencing a topic that the *same* merge request deletes must not +evaluate as "topic present". + +**Attempted CEL leaf.** There is nothing to write. `changes` binds +`in.ChangeSet.Changes` (`bindLeafActivation`), and that ChangeSet is one file's: +`change.ChangeSet` is documented "for one file"; `assent run` strips one `--subject +file:` and calls `changeSetForGoverned(governed, base, head)` on it alone; the +changed-file fold propagates only `classify.ClassAssentPolicy` and opacity, never a second +file's changes; `adoptertest.Case` is singular (`File string; Base, Head []byte`). No single +evaluation can contain both files, and there is no cross-subject aggregation at the run seam. +`REQ-DEM-S05-04` already records this finding independently. + +**Why this is struck rather than escalated.** The blocker is **input availability**, not +expressiveness (§1.3). REQ-E11-S05-01 pins the Rego module to the *identical* +`EvaluationInput`, and the tier is fenced to "declared data, no I/O" — so a Rego module +evaluating this rule sees exactly the same single-file changeset and fails in exactly the same +way. **Adding the Rego tier does not make this rule writable.** The only mechanism that +resolves it today is a provider fact read from the checkout tree +(`cmd/assent/provider_host.go` `checkoutFS`), which is available to both tiers equally and is +gated on `--checkout` (DEM-S14, infra-gated). + +> **Accuracy note for a downstream lane.** `REQ-DEM-S05-04` describes that tree as the +> "merged-result checkout". The code reads `/head` when present, and `checkout.go:44` +> documents `head/` as "the MERGE-REQUEST HEAD: content under judgment". Head and merge result +> are not the same tree. Fixing that sentence is DEM's, not E11-S01's — flagged, not edited. + +**Consequence for E11's documentation (binds S12).** E11 must not be described anywhere as +delivering cross-manifest reasoning. It does not, and REQ-E11-S12-01 forbids claiming a +capability this record struck. + +--- + +## 4. Shape C — set difference — **STRUCK as an expressiveness claim; blocked on a binding-parity defect** + +**Rule (generic).** No ACL entry may be removed from a prod entry without an explicit +`allow-removal` label on the merge request. + +**CEL leaf that expresses it.** + +```cel +oldEntry.acls.filter(a, !(a in entry.acls)).size() == 0 || "allow-removal" in mr.labels +``` + +It compiles (§1.1) and the semantics are right: `filter` + `in` + `size` is set difference, and +symmetric difference, subset and disjointness follow the same way (`oldEntry.acls.all(a, a in +entry.acls)` for subset, `entry.deps.all(d, oldEntry.deps.exists(o, o == d))` for containment). +**CEL expresses set difference over a bounded collection, so this shape is struck.** + +**The residual, which is a defect and not a ceiling.** The leaf above needs `entry`/`oldEntry` +to be **whole-entry value trees**. They are — but only under `assent test`: + +- `bindLeafActivation` binds `toCEL(entryOr(ch.Entry, ch.New))`, falling back to the scalar + `new`/`old` when `ch.Entry` is nil; +- the **only** writer of `ch.Entry` is `internal/adoptertest/entrytree.go` `populateEntries`, + called from `adoptertest.go:288`; +- `internal/evaldecode.BuildEvaluationInput` — the sole production builder, used by + `cmd/assent/evaldecode.go` — never sets it, and `cmd/` contains **no** reference to + `EntryConfig`, `DiffEntries` or `change.Entries` at all. + +So on the `assent run` path `entry` binds a **scalar**, `entry.acls` is a no-such-attribute +error → `predicate.error` → REVIEW. The same rule passes in `assent test` and degrades to +REVIEW in production. That asymmetry is fail-safe, so it is not urgent, but it is real and it +is **not E11-S01's to decide** — raised as **OQ-35**. + +**Why the strike is nonetheless unconditional.** Apply the §1.3 test to both resolutions of +OQ-35 and they converge: + +- if OQ-35 is resolved by **extending** the entry binding to `assent run`, the leaf above works + in production and the shape is struck because **CEL expresses it**; +- if OQ-35 is resolved by **narrowing** the documented contract to the scalar binding, the + shape fails for **input availability** — there is no entry tree in `EvaluationInput` — and + REQ-E11-S05-01 hands a Rego module that identical input, so **Rego fails identically**. + +Either way the shape does not justify a second backend, so it is struck outright and nothing +downstream is left waiting on OQ-35. What OQ-35 *does* decide is whether the shape is writable +at all, which is a test/production-parity question, not a backend question. + +--- + +## 5. Shape D — graph relationship — **EXCEEDS TIER 1, unconditionally** + +**Rule (generic).** A service manifest may not declare a dependency that is **transitively** +reachable back to itself — no dependency cycles at any depth. + +**The input is available today.** A provider declares +`edges: {type: string, cardinality: set}` and returns the adjacency as encoded pairs: + +```yaml +edges: ["orders|billing", "billing|ledger", "ledger|orders"] +``` + +That declaration is in contract, the `http` transport that serves it runs on the plain +`assent run` path with no `--checkout`, and the value binds as a CEL list — every link verified +in §1.4. **No OQ-35, no OQ-36, no `--checkout`, no schema change.** + +**Attempted CEL leaf.** + +```cel +!transitiveClosure(entry.dependsOn).exists(d, d == entry.name) +``` + +**Why it fails.** `transitiveClosure` is an `undeclared reference` and nothing replaces it. CEL +is deliberately non-Turing-complete: **no recursion, no fixpoint, no user-defined function, no +`while`, no fold** (§1.2, measured nine ways) — the four comprehension macros iterate exactly one level over one +collection, and a comprehension cannot call itself. **Unbounded reachability therefore has no +spelling at tier 1**, and neither does any question that depends on it: shortest path, +ancestor-of, strongly-connected component, topological order. + +**What *is* expressible, stated precisely, because an earlier draft of this record got it +wrong.** A cycle check to a **fixed** depth `k` is writable, and it does *not* need the string +decomposition CEL lacks. Over a finite in-input candidate set, **decode is replaceable by +encode-and-compare** — rebuild the edge string and test membership: + +```cel +# a 3-cycle through the subject, using only `+`, `in` and nested exists() +facts.graph.nodes.value.exists(m, facts.graph.nodes.value.exists(n, + (string(new) + "|" + m) in facts.graph.edges.value && + (m + "|" + n) in facts.graph.edges.value && + (n + "|" + string(new)) in facts.graph.edges.value)) +``` + +Compiled **and evaluated** under the real `1_000_000` cost limit against +`edges: ["orders|billing","billing|ledger","ledger|orders"]` and +`nodes: [orders, billing, ledger, payments]`, that returns `true / true / true / false` — correct +3-cycle detection with no `split`, no `substring`, no `indexOf`. The far end of an edge is +recoverable as a *value* the same way: +`nodes.filter(m, (string(new) + "|" + m) in edges)` → `[billing]`. Both primitives (`+` on +strings, `in`) were already in this record's own §1.1 census, so this was always derivable from +the table above. + +**So the ceiling is `k` itself, not decoding — and `k` reaches further than an earlier draft of +this record claimed.** That draft asserted the cost grew as `O(|N|^(k-1)·|E|)` and "exhausts the +cost budget on any real graph". **Measured, that is the wrong complexity class and the wrong +conclusion.** Binding each BFS frontier once per level with `[expr].all(v, …)` (§1.1) makes the +cost *additive across levels* rather than multiplicative, and under the real +`cel.CostLimit(1_000_000)`: + +```text +ring |N|=50 deg 5 |E|=250 frontier k=10 cost= 89,551 k=20 cost=235,297 k=50 cost=686,317 (all correct) +ring |N|=200 deg 5 |E|=1000 frontier k=10 cost=462,618 k=20 EXCEEDED +without the frontier binder naive nesting exceeds the budget at k=4 on the |N|=50 graph +``` + +Cost grows roughly linearly in `k` at fixed `|N|`. At `|N|=50` a check to `k=50` fits in 69% of +budget — and since `k ≥ |N|`, CEL there is **not approximating at all: it decides reachability +exactly.** Many governed catalogs are well under 50 entries. The practical `k` collapses around +`|N|≈200`. + +**This is recorded because it is the honest envelope, not because it is a second reason.** It is +not offered as an expressiveness argument — §2 refuses scale in that role and the same refusal +applies here. It changes nothing about the verdict, and a reader entitled to ask "would CEL +suffice for *our* graph?" is entitled to the measurement rather than an assertion that +forecloses the question. The one claim that carries the verdict is unchanged and narrow: **a +bounded `k`-hop check is expressible; unbounded reachability is not.** + +**Why Rego lifts it.** Recursive rule definitions over `input` are the canonical Rego idiom and +`graph.reachable` answers the closure directly, at any depth, without unrolling; `split` turns +the encoded pairs back into an adjacency so the recursion has something to walk. All are pure, +deterministic, and need no I/O and no data beyond the input already bound. + +**This is the cleanest tier-2 justification in the record, and it is unconditional.** An input +that is in contract and available today, over which tier-1 CEL can answer only a fixed-depth +approximation while Rego answers the actual question, is precisely the evidence D-017's per-rule +gate was asking for. It needs no answer from OQ-35 or OQ-36. + +> **Caveat, stated because this record makes the same distinction for B1 (§3).** No provider in +> the corpus delivers an encoded adjacency today. That the shape is **declarable and +> deliverable** follows from the provider contract — any provider may return a +> `{type: string, cardinality: set}` output, and every link is verified in §1.4 — not from a +> shipped example. **The same epistemic standard as B1, but not the same evidential weight:** +> B1 has a shipped mechanism (`ownership.yaml:21`) and infers only the *source* of the set, +> whereas Shape D infers the whole delivery. That is why "unconditional" is qualified throughout +> as *on today's shipped input contract*, and why the cheapest thing that would close the gap is +> one `assent test` fixture carrying a stubbed `edges` fact. + +**Two things this record got wrong before, recorded so the corrections are auditable.** + +1. *Draft 1* claimed "a mapping-valued fact, which an adjacency needs, is undeclarable" and + downgraded this shape to a contingency on OQ-35/OQ-36. An adjacency needs no mapping — a set + of encoded strings carries one inside the frozen declaration. The error came from conflating + a *provider-supplied catalog* (shapes B1/B2, struck here as working and shipped) with **B3, + which is specifically same-changeset cross-file *diffs***. +2. *Draft 2* replaced that with a second "independent reason" — that CEL cannot decode an edge, + and that this kills even a bounded two-hop check. **Refuted by execution** (above): + encode-and-compare needs no decoding. Both errors are the same failure with the sign flipped + — an **asymmetric evidentiary standard**, accepting awkward-but-working spellings when they + *struck* a shape (A2's re-derivation, B2's dynamic index) and rejecting one when it would + have *narrowed* a shape this record wanted to keep. The verdict was right both times; the + argument was not. One standard now applies in both directions, and Shape D stands on + reason 1 alone. + +**Binds E11-S04 (the capability sandbox), which is not written yet.** `graph.reachable` is pure +and deterministic and **must not be denied** by the allowlist: it is what closes the graph at +any depth, and it alone carries this shape's justification. `split` should be allowed alongside +it — it is equally pure and it is the convenient way to rebuild the adjacency from the encoded +pairs — but it is a convenience, not the justification. A denylist drafted from "deny anything unfamiliar" would +strike out this shape's own justification. Recorded in the S04 section of the epic spec, not +only here. + +--- + +## 6. Verdict summary and the resulting scope + +| Shape | Verdict | Reason | +| --- | --- | --- | +| A1 fold/aggregate over a collection | **EXCEEDS — justifies E11** | no `sum`/`reduce`/`math.*`/`lists.*`; `size()` is the only aggregate | +| A2 named intermediate across checks | **STRUCK** | no `cel.bind` and no value flow across leaves, but inlining is semantically identical | +| B1 registry membership | **STRUCK** | `x in facts.

..value` over a `set` fact; already shipped in the corpus | +| B2 keyed attribute lookup | **STRUCK** | purpose-built provider, or `facts.

..value[key]` (compiles, lint-clean); residual OQ-36 | +| B3 same-changeset cross-file | **STRUCK from E11** | input availability, not expressiveness — the evaluation unit is one file and S05 pins the identical input, so Rego fails identically | +| C set difference | **STRUCK — unconditionally** | `oldEntry.x.filter(a, !(a in entry.x))` expresses it if the entry tree is bound; if it is not, the failure is input availability and Rego fails identically. Both resolutions of OQ-35 strike it | +| D graph relationship | **EXCEEDS — justifies E11, unconditionally** | no recursion, fixpoint, fold or user-defined function ⇒ **unbounded** reachability has no spelling. A *bounded* `k`-hop check **is** expressible via encode-and-compare (verified by evaluation, §5) — the ceiling is `k`, not decoding. The adjacency is in contract and available today as a `{type: string, cardinality: set}` fact — no OQ-35, no OQ-36, no `--checkout` | + +**What E11 is now justified to build:** a tier-2 backend for **folds/aggregates over the +in-input collections** and **recursive/graph reasoning over an adjacency the input already +carries**. Both justifications are **unconditional** on today's shipped input contract; neither +waits on OQ-35 or OQ-36. Nothing else in this record supports the epic. + +**The single strongest piece of evidence** is Shape D: an input that is declarable and +deliverable today, over which tier-1 CEL can express only a check to some **fixed, syntactically +written depth `k`** — because the iteration count of a CEL expression cannot be made +data-dependent (§1.2) — while Rego answers the **actual**, unbounded question with +`graph.reachable`. That gap is exactly the per-rule evidence D-017's gate existed to demand. +Note the claim is about **expressiveness only**: on a small enough graph a large enough `k` is +both affordable and *complete* (§5 measures where), so this is not an argument that CEL is too +slow — it is an argument that CEL cannot write the rule that holds at any size. + +**What E11 is no longer justified to claim:** cross-manifest reasoning of any kind, set +operations over entry trees, and "reuse a computed intermediate". Two of the four shapes +`later-phases.md` names are struck outright and a third is struck in part. + +**Consequences for downstream stories** (recorded here; the epic spec carries the same text): + +Each is marked with **how it is held** — because a consequence with no mechanism is a comment, +not a constraint, and saying so is cheaper than pretending otherwise. + +- **S05** (input binding) need not carry cross-manifest data and must not be widened to fetch + any — widening the input is a *different* decision from adding a backend, and E11's non-goals + fence it. **Held by a gate:** `evaluation-input.schema.json` lives under + `schemas/decision/v1alpha1/`, and REQ-E11-S05-03 pins + `git diff --exit-code -- schemas/decision/`, so a widening reddens. +- **S04** (capability sandbox) **must not deny `graph.reachable`** — it is pure, deterministic, + and the thing that closes the graph at any depth, which is Shape D's entire justification. + `split` belongs in the same allowlist as an equally pure convenience for rebuilding the + adjacency, but it is not what carries the shape. A denylist drafted from "deny anything unfamiliar" would + strike out the epic's own strongest evidence. **Held by review — not by a gate, and the + distinction is the point.** REQ-E11-S04-02's committed `allowed-builtins.golden` detects + **drift**: it fires when the allowed set *changes*, so the sandbox cannot silently *widen*. + It does **not** detect **omission** — an S04 author who simply never adds `graph.reachable` + commits a golden without it and the test is green forever. S04 must therefore carry this floor + as a reviewed acceptance criterion or write the pin itself. (This says nothing about judgment + call (d); *where* the evaluator lives is untouched here.) +- **S07** (violation shape) must support a **fold result** (a computed scalar with the + contributing elements named) and a **path/cycle witness**, not a cross-manifest reference. + **Held by nothing — stated plainly.** There is no schema or gate over the violation shape at + the time of writing; S07 must either carry this as a reviewed acceptance criterion or create + the pin itself. +- **S12** (docs truth) must not describe Rego as enabling cross-entry or cross-manifest checks. + ADR-0002 §"`rego`" currently calls it an "escape hatch for **cross-entry checks**"; per this + record that phrase is inaccurate for the shipped input contract. **Held partly.** + REQ-E11-S12-01's normative text is broad enough to cover it, but its `Test:` list omits + `docs/adr/0002-*` — the actual wrong file — and its `Verify: task check` has no pin over the + phrase today, so the gate would not fail if the line survived. **And S12 is story 12 of 14**: + if E11 never proceeds, a published ADR stays wrong indefinitely. The correction is therefore + also tracked as a standalone backlog residual, independent of this epic — that residual, not + REQ-E11-S12-01, is what actually keeps it from being lost. + +**Corroborating observation.** The single committed illustration of the escape hatch, +`examples/policies/rego/bounded_change.rego`, is **entirely tier-1 expressible** — both of its +`violations` rules are per-change predicates over `input.changes` and `input.facts`, and +`examples/policies/declarative/bounded-change.yaml` is the same rule already authored in the +envelope. When S11 unquarantines it, it should be labelled as a *shape* illustration, not as +evidence that the tier is needed. + +--- + +## 7. Residuals raised, not decided + +**Neither gates any verdict in this record, and neither blocks E11.** Both are +test/production-parity and contract-hygiene questions surfaced while measuring the surface; +they are recorded so the measurement is reproducible, not as conditions on the scope decision. + +| Ref | Question | +| --- | --- | +| **OQ-35** | `entry`/`oldEntry` bind whole-entry trees only under `assent test` (and only there is collection-mode diffing reached at all); `assent run` falls back to the scalar. Extend the binding to the run path, or narrow the documented contract? Shape C is struck either way (§4) and Shape D needs no entry tree (§5). What is at stake is a silent `assent test` / `assent run` divergence an adopter cannot see. | +| **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 and dynamic navigation into it. Is a mapping-shaped fact value in-contract? Touches B2's *second* spelling only — B2 is struck on its first spelling regardless, and Shape D needs only a flat `cardinality: set` fact. | + +Neither is the escalated judgment call (d) (rule-7 mechanism, (d1) vs (d2)); that question is +untouched by this record, which writes no Go and adds no dependency. + +**D-002 / rule 1.** Every rule in this document is a generated generic equivalent — topics, +ACLs, partitions, service dependencies. No employer, internal system, tenant, cluster or +hostname appears in any form. `bash hack/check-sanitization.sh` covers this file: it scans +`git ls-files --cached --others --exclude-standard`, so a new **untracked** file is in scope. +Note the `--exclude-standard` — a **gitignored** path is *not* scanned, which is why the +throwaway CEL probe of §1.1 is deliberately not committed and is **not** covered by that gate. +Its expressions are reproduced inline above, where the gate does see them. diff --git a/openspec/specs/backlog.md b/openspec/specs/backlog.md index 370deb4..925e455 100644 --- a/openspec/specs/backlog.md +++ b/openspec/specs/backlog.md @@ -591,7 +591,7 @@ LGTM** (published contract + the decision path itself). Independent of E10; may | ID | Story | Execution | Depends on | Gate contribution | | --- | --- | --- | --- | --- | | E11-S00 | ⚠️ **SPIKE, do first**: does OPA expose a deterministic (non-wall-clock) eval budget? Nested throwaway module — root `go.mod` unchanged | **[autonomous · spike]** | none | if not, S06 stalls the epic *after* S02+S03 commit | -| E11-S01 | Record the tier-1 (CEL) ceiling with concrete exceeding rules | **[autonomous]** | none | **do first** — a CEL-expressible shape is struck from scope | +| E11-S01 | ✅ **DONE (D-156)** — tier-1 (CEL) ceiling recorded: `docs/planning/rego-tier-ceiling.md` | **[autonomous]** | none | **E11 NARROWED**: cross-manifest + set-difference **struck** (both unconditional). **Two justifications survive, both unconditional**: fold/aggregate, and graph reasoning — a CEL expression's iteration count cannot be data-dependent (depth is syntactic, capped at cel-go's 250), so **unbounded** reachability has no spelling. A bounded `k`-hop check *is* writable and on a small graph is affordable and even complete — the ceiling is expressive, not performance. Cross-manifest is an *input* limit S05's identical `EvaluationInput` does not lift. Sets an S04 allowlist floor (`graph.reachable`, plus `split` as a convenience) held by **review**, not by REQ-E11-S04-02's drift-only golden. Residuals OQ-35/OQ-36 gate nothing | | E11-S02 | ⚠️ Additive `rego:` leaf in the policy schema (announced, no `apiVersion` bump) | **[autonomous · engine-grade · LGTM]** | **S00**, S01 | drift guard scoped; both polarities tested | | E11-S03 | 🔴 Module loading from the **target ref**; compile failure is a lint hard error — **blocked on the operator's rule-7 answer (d1/d2)**: this story adds OPA to `go.mod` inside the guarded tree | **[autonomous · engine-grade · LGTM]** | S02 + operator | no second, laxer load path; transitive purity guard under (d1) | | E11-S04 | 🔴 OPA capability sandbox — **blocked on the operator's rule-7 *mechanism* answer (d1 vs d2)**; "accept and pin" settled only the supply-chain half | **[autonomous · engine-grade · LGTM]** | S03 + operator | both purity gates are non-transitive; see D-141 | @@ -605,6 +605,13 @@ LGTM** (published contract + the decision path itself). Independent of E10; may | E11-S12 | Docs & maturity truth; retire ADR-0002's "pluggable half unbuilt" line | **[autonomous]** | S11 | nothing still calls Rego locked | | E11-S13 | Exit gate | **[autonomous]** | S00–S12 | **the E11 exit gate** | +**E11 residual, tracked independently of the epic** — because it corrects a *published* ADR and +must not wait on 14 stories that may never run: + +| ID | Item | Status | Needs operator | Notes | +| --- | --- | --- | --- | --- | +| **E11-R01** | ADR-0002's `rego` bullet calls the tier an "escape hatch for **cross-entry checks**" — inaccurate for the shipped input contract: E11-S01 / D-156 strikes cross-manifest, and the tier's real justification is folds + unbounded graph reachability | **OPEN** | no (agent lane) | E11-S12 owns it under REQ-E11-S12-01, but that is **story 12 of 14** and the REQ's `Test:` list omits `docs/adr/0002-*`, so nothing fails today if the line survives. Fix is one sentence in `docs/adr/0002-policy-frontends-rego-declarative.md`; evidence in `docs/planning/rego-tier-ceiling.md` §3/§6 | + ## Phase 5 — EX complex in-tree examples / adopter tests / docs truth Full INVEST stories in [p5-ex-complex-examples/spec.md](p5-ex-complex-examples/spec.md). diff --git a/openspec/specs/p5-e11-rego-backend/spec.md b/openspec/specs/p5-e11-rego-backend/spec.md index febc74a..5a3894a 100644 --- a/openspec/specs/p5-e11-rego-backend/spec.md +++ b/openspec/specs/p5-e11-rego-backend/spec.md @@ -61,6 +61,28 @@ second tier real. the loader tier alongside CEL compilation; module *evaluation* is pure computation and may live in core only once S04's sandbox makes that true by construction. +**Justification, post-S01 (D-156) — read this before adding anything to the epic.** S01 has +landed and **narrowed E11**: `docs/planning/rego-tier-ceiling.md` strikes **cross-manifest** +and **set-difference** from the four named shapes and strikes the named-intermediate half of +**multi-pass**. What remains, and the only thing E11 may be justified or documented as +delivering, is: **folds/aggregates over the in-input collections** (CEL has `size()` and no +other aggregate) and **recursive/graph reasoning over an adjacency the input already carries**. +**Both are unconditional on today's shipped input contract** — neither waits on any open +question. The strongest single piece of evidence is the graph shape: a +`{type: string, cardinality: set}` fact carrying encoded edges is fully in contract and +deliverable over the `http` transport on the plain `assent run` path, and over it tier-1 CEL can +express only a check to some **fixed depth `k` written into the rule text** — because the +iteration count of a CEL expression cannot be made data-dependent: `reduce`, `transformList`, +`transformMap`, two-var `all`, `range` and `cel.bind` are all `undeclared reference`, `for` is a +reserved identifier, and depth must therefore be spelled out against cel-go's parser recursion +cap of 250. **Unbounded reachability has no spelling at all.** Rego answers the actual question +at any depth with `graph.reachable`. The claim is about **expressiveness only** — on a small +graph a large `k` is both affordable and complete (measured in the record's §5), so this is not +an argument that CEL is too slow. +Cross-manifest reasoning is an *input-availability* limit, not a tier-1 expressiveness limit — +REQ-E11-S05-01 pins the identical input, so the Rego tier fails on it identically. See the +E11-S01 section for the verdict table and the binding consequences for S05/S07/S11/S12. + **Scope**: (S00) the deterministic-budget feasibility spike, in a nested throwaway module so it adds no dependency; (S01) the tier-1 ceiling, recorded with concrete exceeding rules; (S02) additive `rego:` leaf in the policy schema; (S03) module loading + compile-time errors; (S04) OPA @@ -271,7 +293,43 @@ human dependency. - Verify: manual review - Level: L0 -### E11-S01 — Record the tier-1 ceiling with concrete exceeding rules `[autonomous]` +### E11-S01 — Record the tier-1 ceiling with concrete exceeding rules `[autonomous]` — ✅ **DONE (D-156)** + +**Outcome — E11's scope is NARROWED. Read `docs/planning/rego-tier-ceiling.md` before S05, +S07 or S12.** Of the four shapes `later-phases.md` names, **two are struck outright, one is +struck in part, and one and a half survive**: + +| Shape | Verdict | Reason (measured against `newEvalEnv`, not CEL in general) | +| --- | --- | --- | +| multi-pass — **fold/aggregate** over a collection | **EXCEEDS — justifies E11** | `sum`/`reduce`/`math.*`/`lists.*` are all `undeclared reference`; `size()` is the only aggregate in the surface, so counting is expressible and summing is not | +| multi-pass — **named intermediate** across checks | **STRUCK** | no `cel.bind` and the assert tree combines booleans, not values — but re-deriving the sub-expression inside each leaf is semantically identical and compiles | +| cross-manifest | **STRUCK (all three sub-shapes)** | membership is `x in facts.

..value`; keyed lookup is a purpose-built provider or `facts.

..value[key]` (compiles, lint-clean); **same-changeset cross-file is an input-availability limit, not an expressiveness one** — the evaluation unit is one file and REQ-E11-S05-01 pins the *identical* `EvaluationInput`, so a Rego module fails identically | +| set-difference | **STRUCK — unconditionally** | `oldEntry.x.filter(a, !(a in entry.x))` expresses it when the entry tree is bound; when it is not (`adoptertest` is the sole writer of `EvalChange.Entry`, so `assent run` binds a scalar) the failure is input availability and Rego fails identically. **Both resolutions of OQ-35 strike it**, so nothing downstream waits on that answer | +| graph-relationship | **EXCEEDS — justifies E11, unconditionally** | **The iteration count of a CEL expression cannot be made data-dependent** — no recursion, fold, user-defined function or loop form (`reduce`/`transformList`/`transformMap`/two-var `all`/`range`/`cel.bind` all undeclared, `for` reserved), so depth is a *syntactic* property capped by cel-go's 250 recursion limit ⇒ **unbounded reachability has no spelling**. A *bounded* `k`-hop check **is** expressible (encode-and-compare over a finite candidate set, verified by evaluation) and on a small graph a large `k` is affordable and even complete — so the ceiling is expressive, not performance. Rego answers it at any depth with `graph.reachable`. Adjacency is **in contract and available today** as a `{type: string, cardinality: set}` fact over the `http` transport — no `--checkout`, no OQ-35, no OQ-36, no schema change. **Caveat:** no provider in the corpus ships one yet — same epistemic standard as B1, less evidential weight (B1 has a shipped mechanism and infers only the set's source) | + +**The headline, stated plainly so no later story over- or under-claims it: E11 has two +unconditional justifications on today's shipped input contract — the fold/aggregate shape and +the graph shape — and neither waits on an open question.** OQ-35 and OQ-36 are recorded +residuals of the measurement, not conditions on this scope decision. + +**Binds E11-S04, whose denylist is not written yet:** `split` and `graph.reachable` are pure and +deterministic and **must not be denied** by the capability set. They are precisely what carries +the graph shape's justification, and a denylist drafted from "deny anything unfamiliar" would +strike out the epic's own strongest evidence. Recorded again in the S04 section. This says +nothing about judgment call (d) — *where* the evaluator lives is untouched. + +**Binding consequences for later stories:** +- **S05** must **not** be widened to carry cross-manifest data. Widening the input is a + different decision from adding a backend, and E11's non-goals fence it. +- **S07**'s violation shape must support a **fold result** (a computed scalar naming its + contributing elements) and a **path/cycle witness** — not a cross-manifest reference. +- **S12** must not describe Rego as enabling cross-entry or cross-manifest checks. ADR-0002's + `rego` bullet currently calls it an "escape hatch for **cross-entry checks**"; that phrase is + inaccurate for the shipped input contract and correcting it is S12's, under REQ-E11-S12-01. +- **S11**: the committed illustration `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 in the envelope). When + the quarantine lifts it must be labelled a *shape* illustration, never evidence of need. - **Goal**: a written, reviewable statement of what CEL *cannot* express, grounded in real rules — the artifact D-017's evidence gate was protecting. @@ -292,7 +350,12 @@ human dependency. - Level: L0 - **REQ-E11-S01-02** — Given a shape might in fact be CEL-expressible, when the document is reviewed, then any shape found expressible in CEL is **struck from E11's scope** and - recorded — the epic narrows rather than building an unjustified tier. + recorded — the epic narrows rather than building an unjustified tier. **Satisfied by the + verdict table at the head of this section (D-156):** cross-manifest and set-difference are + struck, the named-intermediate half of multi-pass is struck, and only the fold/aggregate and + in-input graph shapes remain as justification. A shape struck because the *data* is absent + (cross-manifest sub-shape B3) is struck from E11 too, on the separate ground that Rego + receives the identical input and therefore fails identically. - Test: `docs/planning/rego-tier-ceiling.md`, `openspec/specs/p5-e11-rego-backend/spec.md` - Verify: manual review - Level: L0 @@ -409,6 +472,21 @@ human dependency. fails to **compile**, not at runtime; and the rule-7 boundary question is closed by an ADR amendment + decision row rather than by a green-but-non-transitive purity walk. +- ⚠️ **ALLOWLIST FLOOR, set by E11-S01 / D-156 — `graph.reachable` MUST be allowed**, and + `split` alongside it. Both are pure and deterministic (no clock, randomness or I/O). + **`graph.reachable` is the one that carries the epic's strongest justification**: it closes + the graph at any depth, which tier-1 CEL cannot do at all — a CEL expression's iteration count + cannot be data-dependent, so only a fixed, syntactically written depth is expressible + (`docs/planning/rego-tier-ceiling.md` §1.2, §5). `split` is the convenient way to rebuild the + adjacency from the encoded `"a|b"` pairs the input carries — equally pure, but a convenience, + not the justification. A denylist drafted from "deny anything unfamiliar" would strike out the reason E11 + exists. **This floor is held by REVIEW, not by a gate:** REQ-E11-S04-02's golden detects a + **change** to the allowed set, so the sandbox cannot silently *widen* — it cannot detect an + **omission**, and a golden written without `graph.reachable` is green forever. S04 must carry + this as a reviewed acceptance criterion or write the pin itself. **It says nothing about + judgment call (d)** — *which* builtins are callable is orthogonal to *where* the evaluator + lives and *which gate* enforces rule 7; (d1) vs (d2) is untouched and still blocking. + - **REQ-E11-S04-01** — Given rule 7 and D-013, when a module calls `http.send`, `net.lookup_ip_addr`, `time.now_ns`, `rand.intn`, or `opa.runtime`, then compilation **fails** with a message naming the denied builtin — one test case per denied builtin, each asserting failure.