Charge the array index scan its exact lexical items

Merged
VA
2d ago
+145-21

Cause

Breaking commit: #821 be953d15c (Batch filesystem staging and reuse request encoding).

#821 replaced the second serialization pass of canonical encodings with executor::json::arrays::build. That function scans the encoded document to build the decoder's array index. It funded the scan with Inspect { items: document.len() }, one examined item per byte, which is an upper bound. So every canonical encoding of an array-bearing value charged items_examined in proportion to its text, and native fixtures budgeted on items went over:

  • runtime::tests::native::native_policy_approval_keeps_exact_binding_and_paid_utf8_prompt: 657 > 256
  • filesystem::task_runtime::tests::model::native_stock_model_original_lost_ack_uses_native_provider_and_settlement: 65537 > 65536
  • filesystem::task_runtime::tests::settlement::native_stock_tool_lost_ack_reconciles_original_fence_without_redispatch: 65581 / 65588 > 65536
  • acyclic-harness-providers codex_dispatch_tests::stock::codex_stock_execution_counts_locally_without_a_backend_count_route: 65537 > 65536

Fix

The scan re-examines exactly the serializer's lexical items, and the encoder already counted those for this same document (scope.lexical.items).

  • arrays::build now funds exactly that count up front.
  • It rejects a scan that would examine one item more ("scan exceeds its admission").
  • It rejects a scan that ends with a different count ("scan differs from its admission").

No budget or limit is raised. The work is still charged before the scan runs, now at its exact size.

Tests

  • single_pass_properties: the generated property asserts the scan's Inspect equals an independent lexical-item oracle (lexical_items, which counts strings, opened containers and scalar starts) instead of the byte length. The OmitScanCharge negative control remains.
  • New index_scan_examines_exactly_its_admitted_items:
    • Exact funding succeeds.
    • Funding items - 1 fails with "exceeds".
    • Funding items + 1 fails with "differs".
    • The document includes escaped quotes and brackets inside strings.
  • exact_encoding_properties: the canonical {"z":["a","b"],"a":7} receipt drops from 21 to 7 inspected items (CODEC) and from 28 to 14 total items (LEDGER). These are the exact counts: 7 serializer items plus 7 scan items. Every other field is unchanged.
  • Layout-dependent sizes are derived, not hardcoded (from the review). The ledger and peak byte counts depend on the feature set: size_of::<Error>() is 96 with filesystem and 104 with --all-features, and the guard header is 104 vs 112. The table now computes them from the same const APIs the encoder charges: sdk_json_diagnostic_bytes() and the new OwnedBytes::vec_guard_header_bytes::<G>(), which the three internal guard sites now use as well. Every assertion is still an exact equality. A hardcoded size is its own negative control: the old 1,248/1,424 values failed under --features filesystem, measuring 1,160 and 1,328.

Why the merge gate missed it

#821 merged before the build-box PR gate existed. GitHub CI (static.yml and the others) runs no Harness Rust test target, by decision: the merge gate is the build-box PR gate, which runs the full acyclic-harness and acyclic-harness-providers suites (--all-features) against the PR merged onto main before every merge, and fails on any test not already failing on main. That gate runs all four regressions above, so this PR adds no paid GitHub Actions job.

Verification (bb2, head d0f51f4da)

  • cargo test --locked -p acyclic-harness --features filesystem --lib -- executor::json task_runtime::tests runtime::tests::native: 70 passed, 0 failed, 1.18 s.
  • The same filter with --all-features: 70 passed, 0 failed, 1.20 s.
  • codex_stock_execution_counts_locally_without_a_backend_count_route (providers): passed, 0.13 s.
  • The swarm_limits Windows GNU compile failure is pre-existing on main, outside this diff, and owned by co-st-targets.

Earlier (bb1, before the review)

  • cargo test --locked -p acyclic-harness --all-features --lib -- executor::json task_runtime::tests runtime::tests::native: 70 passed, 0 failed.
  • cargo test --locked -p acyclic-harness-providers -- codex_stock_execution_counts_locally_without_a_backend_count_route: passed. Item counts go from open=844, lease=256, run=64436 (failing) to open=430, admission=0, lease=199, run=50919.
  • Bisect: these tests pass at d6e6422ca (parent of #821) and fail at be953d15c.

Companion #821 fixes: #995 (encoder slack double-retained) and #996 (trace event typing).

Guarantee

Class: F/H, the array index scan's work funded by an upper bound (document bytes) instead of its exact size (lexical items). Structural fix: arrays::build is funded with the encoder's exact lexical item count for the same document. It rejects a scan that would examine more ("exceeds its admission") or that ends with a different count ("differs from its admission"), so over- and under-funding both fail at runtime, not just in tests.
Proof: single_pass_properties checks scan Inspect against an independent lexical-item oracle over generated documents, and keeps its OmitScanCharge negative control. Its ByteScanCharge control restores document-byte funding at the real scan charge callback and must fail the same exact assertion. The shrinking digest property independently counts the value tree and checks exact original-native-ledger items. index_scan_examines_exactly_its_admitted_items covers exact funding, items-1 (exceeds) and items+1 (differs), with escaped quotes and brackets inside strings. exact_encoding_properties pins the exact receipt counts, deriving the layout-dependent byte sizes from the encoder's own const APIs so the same exact assertions hold under --features filesystem and --all-features (both run).
Entry points: arrays::build is reached only through serialization::build_buffered, which passes its own scope.lexical.items. Its callers are canonical_json_bytes_bounded (including store::history::canonical_bytes_with_work) and canonical_digest_with_work (through observed canonical_json_digest). The byte encoder is covered by single_pass_properties and exact codec/native-ledger receipts. The digest property now counts containers, keys and values independently from the value tree and checks the original native ledger's exact items_examined, including the scan only when an array is present.
Gaps: none for the class this PR closes (index-scan item accounting).

Separately tracked (not claimed here): GREEN-budget's aggregate proofs (guarantee matrix rows G03/G05/G13/G14/G40: generated whole stock-turn, recursive-child and approval histories, aggregate reservation/credit transfer, exact-limit mutation proofs). The coordinator scoped these out of this PR into their own item. This PR does not claim GREEN-budget is closed.

🤖 Generated with Claude Code

Review fixes

  • (Round 1 added a GitHub Actions json-accounting job under the required SDK Static status; round 2 reverted it. See Round 2 below.)
  • The scan property now rejects restored byte-based funding explicitly. Digest accounting has an independent shrinking tree-count oracle, and both scan entry points are enumerated above.

Review validation

  • cargo test --locked -p acyclic-harness -p acyclic-harness-providers --features acyclic-harness/filesystem --lib -- executor::json task_runtime::tests runtime::tests::native codex_dispatch_tests::stock: 70 Harness tests passed in 1.69 s; 2 provider tests passed in 0.22 s. This includes the byte-funding control and the digest tree-count property. Compilation: 6m 46s; build-slot total wall time 837.1 s, including 386 s queued. The final commit differs from the tested Rust tree only in the workflow aggregation.
  • Focused rustfmt --edition 2024 --check: passed, 11.3 s build-slot wall time.
  • Windows GNU: cargo check --locked -p acyclic-harness -p acyclic-stream --lib --tests --features acyclic-harness/filesystem --target x86_64-pc-windows-gnu reached Harness library/test checking, then failed with the unchanged E0432 SwarmClient/grpc import in harness-fuzz/support/swarm_limits.rs:2. 638.3 s total, including 426 s queued. This is the earlier pre-existing failure, owned by co-st-targets and fixed separately on main in merged #975; it adds no candidate-specific blocker. No second check or alternate feature build was run.

Round 2 (Claude review-and-fix)

  • Reverted the round-1 static.yml change. It made the required SDK Static status wait for a cold compile of Harness and providers on a GitHub-hosted runner, with a 20-minute timeout. That goes against the decision to gate merges on the build box rather than paid CI. Hitting the timeout would also have blocked every PR in the repo. The build-box PR gate already runs these tests as part of the full suites before every merge, so the revert does not weaken CI relative to main, and static.yml is again identical to main.
  • Negative control for the digest tree-count oracle, run against production. arrays::build was mutated back to Inspect { items: document.len() } (uncommitted) and executor::json::tests::digest_properties was run: observed_digest_preserves_identity_without_an_encoded_copy failed and shrank to value = Array [], with items_examined 3 vs oracle 2 (tests.rs:145). The other 5 digest properties passed in 1.01 s; the build took 7m 04s on bb2. Production was then restored. The Rust tree at head matches the tree round 1 tested (70 + 2 passed).
  • The Guarantee now claims only the index-scan item-accounting class. GREEN-budget's aggregate proofs are listed as a separately tracked item.