Repository navigation
Exact native live-object limits and lighter standing-order scratch reads - #791
Conversation
This change combines two reviewed lines of work on current main and re-pins the layout probe for the grown identifier table. The history is one commit so that the documentation revert check judges the net change together with this message. Scratch search routes: - Reuse bounded scratch search routes for standing-order reads - Avoid unnecessary local-route I/O for nonlocal ID lookups Native live-object limits: - Add live-object policy regression rows - Pin live-object population rows in CI - Strengthen live-object policy boundary controls - Make native live-object limits exact and unbounded by default - Carry typed I/O failures from native Store status errors - Pin native Store I/O outcomes and clarify policy documentation - Regenerate allocation site inventory for exact live-object limits - Register checked live-object field assignments - Clarify open allocation inventory accounting - Account for the checked live-object field in the source gate test - Use neutral wording in policy tests Integration: - Use a neutral label in six source-bound notes - Pin the adapter and host sizes measured on the integrated tree - Move the adapter member offset pins with the grown layout Test update carried by this commit: since the scratch search route work, the resident id table answers a lookup of a resident row from its directory and no longer reads its disk index for it. The two cases of tests/test_p2cx_sc412.cpp that counted that read (budget and default) now also look up an absent key, so the disk tree is read through the read cache although a resident row is answered from its directory. No threshold changes. Documentation sentences replaced or removed by this change, named so the documentation revert check can match each to the commit that introduced it: - 0c8e1a8: in docs/ci.md the two sentences that pinned 90 slow-test names now state the 94 pinned slow-test names and how they are counted. - 39fc78c: in docs/pages/memory-management.md, docs/pages/run-failure-codes.md and docs/pages/scratch-tables.md the sentences that said the labels keep the existing message text and limits, and that a generic store live-object cap applies, now describe the exact live-object limit policy: the former default of 1,048,576 is 0 (unbounded) and finite-limit refusals omit the approved-maximum clause. Co-Authored-By: Claude Sonnet 5.5 <[email protected]>
There was a problem hiding this comment.
Graphify reviewed this change.
No issues found by static checks — no coupling regressions or blocking issues in the code graph. That is not the same as safe to merge: see what was not checked.
Not checked: tests were not run; formal verification proved 0 of 2 changed function(s) (2 not verified).
Formal verification. PR-changed functions: 0/2 verified (0 proven, 0 may-equivalent, 0 distinguished) · 2 not verified (2 unsupported).
Not verified on this run: scratch\_object\_limit\_message (unsupported), create (unsupported).
Graphify review — findings
Changes the internal native Store live-object limit so it defaults to 0 (unbounded) instead of the old 1,048,576 cap. Any positive uint64, including UINT64_MAX, is treated as a finite limit and signed negative input is refused before conversion. Finite cohort refusals still report scratch_capacity_exceeded with resource=cohort but drop the "approved maximum" text, and physical backing failures stay separate. Only native embedders and tests set this parameter, and strategies must be recompiled against the new headers to get the unbounded default. Shape layout and the native layout stamp are unchanged, so an old plugin's explicit 1,048,576 stays finite on a new engine, while a new plugin's 0 selects the old cap on an old engine. Bumps the unreviewed ceiling in ci/cr150-source-bounds.yaml to 1410 and rewrites the affected bound notes for the new default.
Review partial — this diff was larger than one review pass covers, so later files were not reviewed; some findings may be missing.
Analysis details — impact, health, verification
Impact & health
Graphify review
Impact — 3396 functions depend on the 3014 functions this change touches.
Health — this change adds coupling hotspots:
- worse:
put_ok()— 22 callers, 4 callees - worse:
check_rollback_only()— 9 callers, 8 callees - worse:
expected_ordered_digest()— 11 callers, 3 callees - worse:
erase_ok()— 9 callers, 3 callees - new:
verify_retained()— 3 callers, 8 callees - worse:
expected_state_digest()— 8 callers, 3 callees - new:
handle_route_read_growth()— 1 callers, 22 callees - new:
check_finite_boundary()— 2 callers, 11 callees - …and 8 more — each is listed as a finding
Verification — 3396 functions in the blast radius were not formally verified this run (proofs are advisory here).
Gate & verification
graphify gate
PASS — objectively clean (no health regressions, tests not run — proofs not run this pass (advisory)). Grounded, not self-assessed.
Advisory (not blocking):
- verification_scope: 3336 function(s) in the blast radius were not formally verified this run
Formal verification
Could not verify: Could not verify scratch\_object\_limit\_message.
The verifier did not have enough to check scratch\_object\_limit\_message, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: unsupported: signature arity changed (3 -> 2 positional params)
Could not verify: Could not verify create.
The verifier did not have enough to check create, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: unsupported: member function — receiver/self (`this`) not synthesizable from the simple-type literal pools — abstaining rather than guessing a receiver
· 11 grounded finding(s) anchored inline below; 5 more finding(s) on lines outside this diff (see the check run).
| return UINT64_C(0xd38a91e65b7402cf) ^ ((index + 1) * UINT64_C(0x9e3779b97f4a7c15)); | ||
| } | ||
|
|
||
| void write_marker(Store& store, Id id, std::uint64_t index, std::uint64_t requested) { |
There was a problem hiding this comment.
write_marker()
high coupling complexity (Ca·Ce = 12).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| require(store.write(id, 0, &value, sizeof(value)) == sizeof(value), "short marker write"); | ||
| } | ||
|
|
||
| void verify_retained(Observation& observation) { |
There was a problem hiding this comment.
verify_retained()
fans out to 8 callees (efferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| observation.readback_complete = true; | ||
| } | ||
|
|
||
| void populate(Observation& observation, std::vector<Id>& ids) { |
There was a problem hiding this comment.
populate()
fans out to 11 callees (efferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| observation.report("population_verified"); | ||
| } | ||
|
|
||
| void expect_refusal(Observation& observation, std::vector<Id>& ids) { |
There was a problem hiding this comment.
expect_refusal()
fans out to 7 callees (efferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| require(ids.size() == ids_before, "refusal changed retained IDs"); | ||
| } | ||
|
|
||
| Id check_finite_boundary(Observation& observation, std::vector<Id>& ids) { |
There was a problem hiding this comment.
check_finite_boundary()
fans out to 11 callees (efferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| verify(*s, model, 512, numeric_probes(), 1, true, "after forced eviction"); | ||
| } | ||
|
|
||
| bool ordered_search_growth() { |
There was a problem hiding this comment.
ordered_search_growth()
fans out to 18 callees (efferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| return flat; | ||
| } | ||
|
|
||
| bool interleaved_range_growth() { |
There was a problem hiding this comment.
interleaved_range_growth()
fans out to 20 callees (efferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| return flat; | ||
| } | ||
|
|
||
| bool interleaved_interior_growth() { |
There was a problem hiding this comment.
interleaved_interior_growth()
fans out to 19 callees (efferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| return flat; | ||
| } | ||
|
|
||
| bool handle_route_read_growth() { |
There was a problem hiding this comment.
handle_route_read_growth()
fans out to 22 callees (efferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| return bounded; | ||
| } | ||
|
|
||
| void ordered_search_error_controls() { |
There was a problem hiding this comment.
ordered_search_error_controls()
fans out to 19 callees (efferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
This pull request is one commit on top of the current
main(e1d29cb9). It carries two reviewed engine changes and replaces #790, which held the same changes as a chain of commits.Live-object limits
Standing-order scratch reads
Tests and layout
Strategy modules built against 1.10.x must be rebuilt against these headers (already stated in the changelog).
Verification
Part of #621.
🤖 Generated with Claude Code