📝 docs(e11): record the tier-1 CEL ceiling (E11-S01) - #88
Merged
Conversation
Adds docs/planning/rego-tier-ceiling.md — the artifact D-017's per-rule
evidence gate was protecting and D-141 lifted as a gate, not as a design
need. It is a scope-reduction instrument: of the four shapes later-phases.md
names, two are struck outright and a third in part.
Measured against the surface this repo actually binds (newEvalEnv's eleven
frozen 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.
Exceeds tier 1, and therefore justifies E11:
- folds/aggregates: sum/reduce/math.*/lists.* are undeclared references;
size() is the only aggregate, so counting is expressible and summing is not
- graph reasoning over data already in EvaluationInput: no recursion,
fixpoint or fold; bounded unrolling answers a different rule
Struck, with the CEL that does the job:
- registry membership, keyed attribute lookup, set difference, and the
"named intermediate" half of multi-pass
- same-changeset cross-file reasoning is struck on a different ground: the
blocker is input availability, not expressiveness. The evaluation unit is
one file and REQ-E11-S05-01 pins the identical EvaluationInput, so a Rego
module fails that rule identically
Also records that the one committed illustration of the escape hatch,
examples/policies/rego/bounded_change.rego, is entirely tier-1 expressible.
Binds S05 (do not widen the input), S07 (fold result + cycle witness, not a
cross-manifest reference), S11 and S12. Judgment call (d) is untouched: this
lane writes no Go, adds no dependency and touches no schema.
Residuals raised, not decided: OQ-35 (entry/oldEntry bind whole-entry trees
only under assent test) and OQ-36 (no declarable object type for a fact value).
…ape contingent Applies the record's own input-availability test to the two shapes it had exempted from it. Set-difference: struck unconditionally. Both resolutions of OQ-35 strike it — extending the entry binding to `assent run` makes CEL express it; narrowing the contract makes it an input-availability failure, and REQ-E11-S05-01 hands a Rego module that identical input, so Rego fails identically. The previous conditional would have left S05/S07 waiting on an answer that cannot change the verdict. Graph relationship: verdict unchanged (CEL has no recursion wherever the data sits), but building on it is now explicitly contingent on OQ-35 or OQ-36. New §1.3 measures why: on the `assent run` path document-mode walkNode emits a Change only where two SCALARS differ — a sequence makes the ChangeSet opaque -> REVIEW — and DiffEntries is reached only from internal/adoptertest. So old/new/entry/oldEntry and every changes[i].old/.new bind scalars, and the only value-tree-shaped binding left is facts.<p>.<n>.value, which is flat under `cardinality: set` and undeclarable if richer. An adjacency has no in-contract home today. Headline, now stated in all four places: on today's input contract the fold/aggregate shape is E11's ONLY unconditional justification. Synced across the record, the epic spec, the backlog row, D-156's rejected option (b), and both OQ rows so a grep for drift finds none.
…ency CEL cannot decode (F01)
Review F01 was right and the premise it attacked was false. The record claimed
"a mapping-valued fact, which an adjacency needs, is undeclarable" and turned
the graph shape into a contingency on OQ-35/OQ-36. An adjacency needs no such
thing.
Verified end to end in-tree: `edges: {type: string, cardinality: set}` is a
legal declaration; fact.value carries no JSON-Schema type constraint and
ResolveFactsChecked cross-checks the declaration, never the value; outputs are
operator-authored per provider; the http transport is live on the plain
`assent run` path with no --checkout; and a set fact binds as a CEL list. So
["orders|billing", "billing|ledger"] is an in-contract adjacency inside
EvaluationInput today.
Tier-1 CEL cannot use it, for two independent reasons — and the second is
sharper than the first. Measured, not recalled:
REJECTED ...exists(s, s.split("|")[0] == string(new)) undeclared 'split'
REJECTED ...exists(s, s.substring(0, s.indexOf("|")) ...) undeclared 'substring'
REJECTED ...exists(s, s.indexOf("|") > 0) undeclared 'indexOf'
COMPILES ...exists(s, s.startsWith(string(new) + "|")) one hop, prefix only
ext.Strings is unregistered, so the surface can TEST a string but never take it
apart: an edge's far end is unrecoverable, which kills even a bounded two-hop
check that the no-recursion argument alone would permit. Rego does both with
pure builtins (split, recursive rules, graph.reachable).
An input that is in contract and available today, that CEL provably cannot
decode and Rego consumes trivially, is the cleanest tier-2 justification in the
record — and exactly the per-rule evidence D-017's gate demanded. E11 now has
TWO unconditional justifications; the operator recommendation to defer S02-S13
on a contingency is withdrawn.
F02: §5 had conflated a provider-supplied catalog (B1/B2, struck as working and
shipped) with B3, which is specifically same-changeset cross-file DIFFS. That
conflation is what hid F01. F03: one evidentiary standard now applies —
awkward-but-working spellings count whether they strike a shape or preserve one.
Also records the binding this creates where S04 will read it: split and
graph.reachable MUST NOT be denied by the capability allowlist. Orthogonal to
judgment call (d), which stays untouched and blocking.
Sweep: F04 marks each downstream consequence with how it is held (S05 by
REQ-E11-S05-03's schemas/decision pin, S12 by REQ-E11-S12-01, S07 by nothing —
said plainly). F05 tracks the ADR-0002 "cross-entry checks" correction as a
standalone residual so a published ADR cannot stay wrong if E11 never proceeds.
F06 corrects the sanitization claim: --exclude-standard means the gitignored
probe is NOT scanned. F07 states that B1's corpus citation is an identity fact,
not a cross-manifest registry read. Probe expressions now land in the artifact.
… was false (F-01)
Review F-01 refuted §5's reason 2 by execution, and I reproduced it before
editing. Over a finite in-input candidate set, decode is replaceable by
encode-and-compare. Compiled AND evaluated under the real cel.CostLimit(1e6):
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))
over edges ["orders|billing","billing|ledger","ledger|orders"] and nodes
[orders,billing,ledger,payments] => true/true/true/false. Correct 3-cycle
detection with no split, no substring, no indexOf. The far end recovers as a
value too: nodes.filter(m, ("orders"+"|"+m) in edges) => [billing].
Both primitives (+ on strings, `in`) were already in this record's own §1.1
census, so the claim was internally inconsistent as well as false. The cost
rebuttal is closed by my own §2: this record refuses scale as an expressiveness
argument.
Shape D's VERDICT is unchanged and E11 still has two unconditional
justifications — reason 1 was always sufficient and is independently verified
(transitiveClosure -> undeclared reference). The honest claim is narrower: a
bounded k-hop check IS expressible; UNBOUNDED reachability is not. Rego answers
it at any depth with graph.reachable. Fixed in all seven places it had spread:
the record §1.1/§5/§6 (x2), D-156, spec.md justification block, S01 verdict
table, S04 floor, and the backlog row.
This is F03 with the sign flipped — draft 1 rejected a working spelling to
narrow Shape D, draft 2 rejected one that would have narrowed it. Both drafts
are now recorded in §5 and D-156 with the common cause named, and the
"one standard is applied throughout" claim is corrected rather than repeated.
F-02: "Held by a gate: REQ-E11-S04-02's golden" was itself an invented
enforcement path, inside the fix meant to remove those. That golden detects
DRIFT, not OMISSION — an author who never adds graph.reachable commits a golden
without it and it is green forever. Relabelled "Held by review" in the record,
the spec's S04 floor, and D-156, with the drift/omission distinction spelled
out. Only S05 still claims a gate; that one is real.
F-04: the S04 floor keeps its operative MUST but is re-argued onto what holds —
graph.reachable closes what CEL cannot close, split rebuilds the adjacency from
the encoded pairs, both pure and deterministic.
F-03: S12's "Held by a gate" softened — REQ-E11-S12-01's Test list omits
docs/adr/0002-*, so nothing fails today if the line survives.
F-05: states plainly that no provider in the corpus ships an encoded adjacency;
deliverability is the same contract inference used to strike B1.
F-06: the ADR-0002 residual moves out of the Phase-3 freeze table to a new E11
residual table as E11-R01.
F-07: no action — CHANGELOG is generated from commit subjects and rule 2 forbids
the rewrite that would fix the ordering.
…one (F3-01)
Review F3-01 was right and I reproduced it before editing. The census had
omitted the surface's only value binder, [expr].all(v, ...) — CEL's standard
poor-man's let. Binding each BFS frontier once per level makes cost additive
across levels, not exponential in k. Measured under the real
cel.CostLimit(1_000_000) with newEvalEnv verbatim:
ring |N|=50 deg5 |E|=250 frontier k=10 89,551
frontier k=20 235,297
frontier k=50 686,317 (all correct)
ring |N|=200 deg5 |E|=1000 frontier k=10 462,618; k=20 EXCEEDED
without the binder: naive nesting exceeds the budget at k=4 on |N|=50
Roughly linear in k. And at |N|=50, k=50 >= |N|, so CEL is not approximating
there at all — it decides reachability exactly, in 69% of budget. The sentence
"exhausts the cost budget on any real graph" foreclosed a question a reader
sizing this epic is entitled to ask, with an assertion measurement refutes.
Deleted, not replaced. This is the fourth instance of the pattern I diagnosed
myself — reaching for a second reason when one sufficient reason was in hand —
so no new supporting argument was added. Reason 1 stands alone and now carries
the verdict by itself.
F3-02: reason 1 restated positively and measured rather than recalled, in a new
§1.2. The property is that a CEL expression's iteration count cannot be made
data-dependent: reduce / transformList / transformMap / two-var all / range /
lists.range / cel.bind all undeclared, `for` a reserved identifier, no fold, no
self-reference, no generator — so depth is SYNTACTIC, hard-capped by cel-go's
parser recursion limit of 250 (verified: depth 200 compiles, 260 does not). And
a fixed k really is an approximation when data outruns it: on a 4-cycle the k=3
form is false, the k=4 form true. One property, measured nine ways.
Census gains the [expr].all(v, ...) binder row. §2/A2 corrected: the binder
removes the evaluation-cost half of the residual, leaving legibility only — A2
is struck MORE firmly than before.
F3-04: the B1 symmetry is epistemic, not evidential — B1 has a shipped mechanism
and infers only the set's source; Shape D infers the whole delivery.
F3-05: graph.reachable carries the justification; split is a pure convenience.
F3-03: no action, as directed.
Subsections renumbered 1.2->1.3, 1.3->1.4 with all cross-references retargeted.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Records what the tier-1 CEL surface cannot express, measured against
newEvalEnv's eleven frozen predicate-scope variables and zero extension libraries.Strikes cross-manifest membership, keyed lookup, set difference, and the named-intermediate half of multi-pass from E11's justification.
Leaves two unconditional justifications for a second backend:
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.Docs/spec-only: zero Go, zero schema, zero dependency change.
Four independent review rounds, a different reviewer each round; the final round returned APPROVE with no P0/P1.