Prototype spec RFC 0008 quantifiers behind an experimental opt-in flag (ADR-0009)

[kikashy]

Material-decision impact: public-surface, documented-claim; review: see the ## Cross-vendor adversarial review comment on this PR

What this adds

A DRAFT-RFC PROTOTYPE of spec RFC 0008's exists/every/uniform, reachable only via judgment-pack experimental evaluate --rfc0008-quantifiers (ADR-0009, opened in this PR per the ADR process). Current-condition-root scoping, structural aggregate-depth-two enforcement, the RFC's pinned truth tables, and a byte-sensitive precharged work-accounting candidate. Containment verified by the cross-vendor review against a separately built main: without the flag, all three operators produce byte-identical refusals; spec validate, MCP, and the conformance runner have no diff. Packs using the operators remain invalid under 0.1.0-draft and every successful evaluation carries an explicit draft-prototype marker.

What it proved

• Two-implementation evidence (with the clean-room Python prototype in judgment-pack-evaluator-experiments): 80 conformance rows, 79 agree; the single divergence is where the limit is drawn — the exact question RFC 0008 declares unresolved. Census equivalence (A6/R3/R5 quantifier twins vs prepared-boolean originals): 9/9 across both implementations.
• The accounting precondition is real: the first candidate model (flat units) was broken by the review's ~1 MiB-pointer attack — tens of gigabytes of processing under budget. The repaired byte-sensitive model carries the attack as a regression (refused in 0.07s, verified unrefused under the old model).
• One RFC gap found: uniform's five clauses omit resolved-but-indeterminate equality; this runtime extends clause 4 and the spec-side amendment is proposed separately.

The record

Cross-vendor review (OpenAI gpt-5.6-sol) follows as a comment: one major (the accounting attack) and four minors, all accepted and implemented in 2f4e064 under the change-after-review exception (each linked per finding). Internal same-vendor verification before the cross-vendor pass: two adversarial verifiers, two blockers + four majors absorbed (disclosed for completeness, not regime-qualifying).

🤖 Generated with Claude Code

[kikashy]

Cross-vendor adversarial review

• Drafting models: Anthropic claude-fable-5 (session: direction, integration, dispositions) and Anthropic claude-opus-5 (implementation workflow: implementer, two internal adversarial verifiers, fixer), 2026-07-27.
• Reviewing model: OpenAI gpt-5.6-sol (vendor: OpenAI) via codex-cli 0.145.0, 2026-07-27.
• Reviewed SHA: 73ec8ff. Context given: full working-tree checkout of this branch, shell access with go toolchain, the spec repository for the authoritative RFC text, instructed to diff and build against main; no MCP servers.
• Runs: one on this PR. No run was discarded. The output below is the reviewing model's complete returned review text; the full session log including tool exploration is preserved locally.

Prompt (verbatim)

Adversarially review the change on this branch of judgment-pack-runtime (`git diff main...HEAD`):
a DRAFT-RFC PROTOTYPE of the specification's RFC 0008 bounded collection quantifiers
(exists/every/uniform) behind a new `--rfc0008-quantifiers` opt-in on `experimental evaluate`,
with ADR-0009 recording the decision. The authoritative semantics are
/home/onword/repo/judgment-pack/judgment-pack-spec/rfcs/0008-bounded-collection-quantifiers.md
(Specification + Conformance) — read them and verify the implementation against the TEXT.

You may build and run: prefix all go commands with GO111MODULE=on (go build ./..., go vet ./...,
go test ./...). Attack, in order:
1. SEMANTIC FIDELITY: current-condition-root threading (restore after each element; empty-pointer
   rules; uniform.at member-relativity); exists/every strong-logic combination with pinned
   empty-array values; uniform's five ordered clauses (a known unequal pair must beat missing data
   even when the FIRST member's at is missing — check the pairwise logic, not just clause order);
   structural depth-two counting through all/any/not wrappers; short-circuit only on dominant
   values, never unknown.
2. THE ACCOUNTING CANDIDATE: is the precharge actually order-independent and complete before any
   predicate runs? Does ragged nesting really cost the sum, never the product? Does preflight's own
   cost stay bounded? Is limit exhaustion an error and never a disposition? Try to construct an
   input where short-circuiting changes whether the limit trips, or where two permutations of the
   same array produce different outcomes of any kind.
3. CONTAINMENT: with the flag absent, is the extended grammar truly unreachable — packs using the
   ops fail exactly as on main? Is `spec validate`, the MCP surface, and the conformance runner
   untouched (diff them)? Do the JSON and human draft-prototype markers state only true things in
   every flag/pack combination?
4. THE PUBLIC SURFACE: flag help text, CHANGELOG entry, ADR-0009 (accurate context? honest
   consequences? correctly indexed?), README/architecture updates — do any overstate what a
   draft-RFC prototype is or imply conformance?
5. TESTS: find a Conformance row of the RFC with no covering test, or a test whose name claims
   more than its assertions check.

Severity (blocker/major/minor), exact text/file:line, concrete fix. If sound, say so plainly — do
not invent findings.

Output (complete, unedited)

Not sound as-is: no blocker-severity finding, but one major accounting defect and four minor issues.

Findings

1. Major — the work budget does not bound actual work.
   unitPointer and scalar values cost one unit, fact never resolves or sizes its selected runtime value during preflight, and valueUnits charges every scalar as one. Yet pointer resolution scans/splits/unescapes the complete path, while numeric equality and decimal ordering parse complete tokens.

   Concrete attack: a valid depth-two exists over 30,000 {} elements whose inner aggregate has a valid approximately 1 MiB unresolved path charges only 2 + 30,000×2 = 60,002, below the 100,000 budget. Preflight nevertheless scans that path roughly 30,000 times—about 30 GiB of processing—and evaluation repeats it because every inner result is unknown. Long numeric/decimal operands similarly get reparsed per element while costing one scalar unit.

   Fix: make pointer charges byte/token-sensitive and reserve them before resolution; charge scalar byte lengths and numeric parsing complexity; include selected fact values in preflight or cache compiled pointers and parsed numeric operands. Add long-pointer and long-number regressions proving refusal occurs before the expensive operation.

2. Minor — uniform defines a result for a case the RFC’s five clauses omit.
   The authoritative clauses cover known inequality, missing at, and known equality, but not two resolved values whose equality is indeterminate (RFC lines 307–320). The implementation treats any indeterminate comparison as clause-4 unknown (quantifier.go), and tests label that behavior conformance (quantifier_test.go).

   Fix: amend RFC clause 4 to explicitly include indeterminate equality—after known inequality so clause 3 still dominates—then retain these tests. Until then, ADR-0009 should not claim the Specification is implemented “exactly.”

3. Minor — the required R5 equivalence row is missing.
   The RFC explicitly requires distinct A6, R3, and R5 re-encodings (RFC line 596). The test claims R3/R5 coverage, but loads only an A6 pair and an R3 /modification/... pair (rfc0008_test.go). ADR-0009 consequently overstates that all three run as committed tests (ADR-0009).

   Fix: add separate prepared/quantifier R5 fixtures using /request/allNewItemsAvailable, with matching dispositions and published-schema acceptance/rejection assertions.

4. Minor — public surface documentation contains two literal inaccuracies.
   The changelog says “Three diagnostic codes” but lists four distinct codes: GRAMMAR, DEPTH, SHAPE, and WORK-LIMIT (CHANGELOG.md). It and the flag help also say every result carries draftPrototype; handled grammar/work-limit errors use the operational-error envelope and carry no such member.

   Fix: say “four diagnostic codes” and “every successful evaluation payload.” Apply the same successful-result qualification to ADR-0009 and flag help, or add the marker to operational errors.

5. Minor — accounting documentation falsely claims duplication invariance.
   The code says charge is identical under permutation “or duplication” (quantifier.go); the test repeats the claim but tests only permutations (quantifier_test.go). Duplicating an element necessarily adds its where charge and may cross the limit. Only the condition value is duplicate-invariant while both inputs remain within limits.

   Fix: restrict the accounting claim to permutation invariance. Add a test showing duplication increases charge while preserving the logical result when both cases fit the budget.

Confirmed sound

The current-root threading, empty-pointer behavior, strong three-valued combinations, pinned empty arrays, dominant-only short-circuiting, structural depth through wrappers, and uniform’s known-unequal-pair-over-missing behavior are correct—including when the first member is missing.

Containment is also sound. Validation, MCP, and conformance-runner packages have no diff. Against a separately built main, all three operators without the flag produced byte-identical JSON and human refusals; an ordinary Core evaluation was also identical. ADR indexing/status and the README/architecture no-conformance posture are accurate apart from the wording above.

GO111MODULE=on go build ./..., go vet ./..., uncached go test -count=1 ./..., and git diff --check main...HEAD all passed.

---

Dispositions

#	Finding	Disposition	Implemented by
1	Major — the work budget did not bound actual work (flat units vs byte-shaped processing; the ~1 MiB-pointer attack)	Accept	Byte-sensitive charging: pointers charge 1+len(path) to compile (reserved before the scan, compiled form cached per authored path) plus per-resolution token bytes; scalars charge token length. Both reviewer regressions added; the pointer attack is refused in 0.07s and was verified unrefused (and 8.8s without the cache) under the old model. (2f4e064)
2	Minor — uniform defines a result for a case the RFC's five clauses omit (resolved-but-indeterminate equality)	Accept in this repo's half	Behavior kept as the proposed reading; tests renamed amendment-* and documented as pinning a proposal, not conformance; ADR-0009's "exactly" removed. The RFC clause-4 amendment is proposed in the spec repository separately. (2f4e064)
3	Minor — required R5 equivalence row missing	Accept	Distinct R5 prepared/quantifier fixture pairs over /request/allNewItemsAvailable, five rows, schema acceptance/rejection assertions; ADR-0009 corrected. (2f4e064)
4	Minor — CHANGELOG counted three of four diagnostic codes; draftPrototype overclaimed to every result	Accept	"Four diagnostic codes"; marker qualified to every successful evaluation payload in CHANGELOG, flag help, ADR-0009, README. (2f4e064)
5	Minor — duplication-invariance overclaim on the charge	Accept	Claim restricted to permutation invariance of the charge; new test pins that duplication raises the charge and preserves the condition value within limits. (2f4e064)

All 2f4e064 changes implement dispositioned findings of this review and are covered by the change-after-review exception; the cross-implementation matrix in the sibling repository was re-run in full against the repaired model (same 79/80 result).

[kikashy]

Cross-vendor adversarial review — run 2 (verification of the post-spec-review repairs)

• Reviewing model: OpenAI gpt-5.6-sol (vendor: OpenAI) via codex-cli 0.145.0, 2026-07-27.
• Reviewed SHA: d3e6a8c (determinate numeric equality; third accounting candidate). Context given: full working-tree checkout, go toolchain, diff against main; no MCP servers.
• Runs on this PR: two (run 1 above, this run). No run was discarded.

Prompt (verbatim)

This is a VERIFICATION pass on this branch's newest commit. You (a prior run from your vendor)
reviewed an earlier SHA of this runtime branch (one major: budget did not bound actual work; four
minors) and, separately, a spec-side review reproduced a live prototype disagreement on numeric
equality (1e999999999 vs 2e999999999). The newest commit responds to both: jsonEqual became total
(normalized sign/significand/exponent comparison, big.Rat indeterminable arm deleted — note this
also changes the non-quantifier experimental path, CHANGELOG'd), uniform reduced to exactly the
RFC's five clauses, and the accounting moved to its third candidate (preflight resolves fact
pointers; selected runtime values priced, in: per candidate; evidence-requirement ids priced).

Scope narrowly: `git diff main...HEAD` with attention to the newest commit; run
GO111MODULE=on go build ./... && go vet ./... && go test -count=1 ./... yourself. Check ONLY:
1. Is normalized-token numeric equality correct? Attack the normal form: -0 vs 0, 0e999999999,
   trailing/leading zeros, 1e-2 vs 0.01, exponent-sign forms (1E+3), values differing only beyond
   the significand (10e999999998 vs 1e999999999), and asymmetry/transitivity. Is ordering
   (greater-than family) genuinely untouched?
2. Does the third accounting candidate still hold the settled intents: order-independent,
   charge-before-evaluate, ragged sums, refusal before expensive work — now that preflight resolves
   fact pointers (does THAT resolution do unpriced work for a long pointer... or is it covered by
   the compiled-pointer reserve)? Try to construct remaining unpriced work.
3. Any regression to containment (validation/mcp/conformance untouched; flag-off behavior identical
   to main) or any doc/CHANGELOG/ADR statement the new code falsifies.
Do not re-litigate dispositioned design choices. Findings with severity and exact fixes, or state
plainly that the repairs converge.

Output (complete, unedited)

The repairs do not fully converge: one major and two minor findings remain.

Findings

• Major — uniform still admits unpriced repeated numeric normalization.
  uniform repeatedly compares the original representative, and numbersEqual normalizes both tokens on every comparison. Preflight charges each selected value only once (quantifier.go:385).

  Adversarial case: one 80,001-byte 1000…0 followed by 999 copies of the equivalent 1e80000. Both permutations charge exactly 90,009 under the 100,000 budget and the full engine admits them, but one benchmark iteration took approximately:

  • Long token last: 0.162 ms
  • Long token first: 92.3 ms

  Thus actual work is O(long-token × members) while charge is O(long-token + members). This falsifies the “one pass” accounting claim in ADR-0009:75.

  Exact fix: normalize each resolved at value once into a reusable equality representation and retain the representative’s normalized form throughout the pass. Avoid a cache keyed by the long token itself, since repeatedly hashing that key recreates the scan. Alternatively, reserve the order-independent worst-case representative reread, such as sum(value sizes) + (resolvedCount-2)*max(value size).

• Minor — empty JSON-pointer tokens are not charged per resolution step.
  Resolution loops once per token (condition.go:256), but chargePointer charges only 1 + compiled.bytes. A valid pointer containing 100 empty reference tokens ("////…") therefore charges one unit on each cached resolution while executing 100 map traversals. The initial raw-pointer scan is correctly reserved before compilation; this is specifically a repeated-resolution gap. Carrier depth limits the amplification, hence minor severity.

  Exact fix: charge at least max(1, len(compiled.tokens))*unitPointerStep + compiled.bytes, then update the pointer-cost fixtures and prose.

• Minor — ADR containment statement is stale.
  ADR-0009:100 says “the evaluator without the flag” does not change, but numeric equality changes unconditionally. The CHANGELOG correctly acknowledges this. Remove that phrase or qualify it with the §7.4 equality exception.

Verified

• Numeric normalization is correct for all requested cases, including signed zero, huge-exponent zero, fractional/exponent equivalence, trailing zeros, E+, 10e999999998 == 1e999999999, huge unequal values, symmetry, and transitivity.
• Ordered comparison is byte-for-byte unchanged from main.
• The five-clause uniform semantics are correct.
• Fact-selected values, in candidates, evidence IDs, ragged sums, sibling addition, order-independent charge totals, and charge-before-predicate behavior otherwise hold.
• No files under validation, MCP, or conformance changed. A representative flag-off evaluation was byte-identical to main, apart from the intentional numeric-equality behavior.
• git diff --check passes and the worktree is clean.
• With module mode applied to the full sequence, go build ./..., go vet ./..., and go test -count=1 ./... all pass.

---

Dispositions — run 2

#	Finding	Disposition	Implemented by
1	Major — uniform admits unpriced repeated numeric normalization (92.3ms vs 0.162ms permutation asymmetry under identical charge)	Accept, both fixes	An order-independent (n-1) x max(valueUnits) reread term prices the pass; values are canonicalized once so comparisons hit the identical-token short-circuit (measured 0.6/0.8ms on the reviewer's case); the adversarial case (80,001-byte token + 999 x 1e80000) is refused identically in both permutations. ADR's "one pass" claim replaced. (aecba37)
2	Minor — empty pointer tokens charged one unit per resolution	Accept	Per-resolution cost is now max(1, tokens) x step + bytes; a 100-empty-token pointer over 1,000 elements is refused while the one-token pointer evaluates. (aecba37)
3	Minor — ADR containment phrase stale (numeric equality changes unconditionally)	Accept	Qualified with the §7.4 numeric-equality exception, matching the CHANGELOG. (aecba37)

Context: the d3e6a8c changes this run reviewed were themselves prompted by the spec-side review on spec PR #19 (determinacy replacing the indeterminate arm; selected-value pricing) — outside this PR's own change-after-review exception, hence this fresh run. The aecba37 fixes implement run 2's dispositioned findings recorded here and are covered by the exception. The cross-implementation matrix was re-run after aecba37: 81/82 rows agree (the two new determinacy rows J15/J16 among the agreements), 9/9 census equivalence, the only divergence remaining the deliberately unpinned L3. The accounting model is now its fourth candidate; every predecessor was retired by a demonstrated, now-regression-tested pricing attack — which is the acceptance-precondition evidence RFC 0008 asked for, recorded in spec PR #19.