feat: provable sum-budget reads — SumBudgetWindow in the GroveDBProof V1 envelope - #800
Merged
QuantumExplorer merged 1 commit intoAug 14, 2026
Conversation
Contributor
|
Important Review skippedAuto reviews are disabled on base/target branches other than the default branch. Please check the settings in the CodeRabbit UI or the ⚙️ Run configurationConfiguration used: defaults Review profile: CHILL Plan: Pro Plus Run ID: You can disable this status message by setting the Use the checkbox below for a quick retry:
Comment |
This was referenced Aug 14, 2026
… V1 envelope
Sum-budget path queries (ReadMode::SumBudget: walk items in key order,
stop when the running net sum reaches the budget) gain a proof form: a
new appended ProofBytes::SumBudgetWindow variant whose payload carries
an ordinary Merk proof over exactly the window of elements the budget
walk scanned, plus the window size and whether the walk exhausted the
ranges.
The verifier executes the window proof with the query's OWN items and
direction (limited to the claimed window on a stop, unlimited on
claimed exhaustion so the proof itself attests the range end), then
REPLAYS the engine's fold arithmetic element by element — saturating
net-budget subtraction, per-match limit, the grove-version global scan
cap with its counted-but-unprocessed tripping element, skip semantics —
and rejects a window that continues past a fired stop, stops short of
one, or misstates exhaustion. The parent binding falls out of the
ordinary combine_hash(H(value), child_root) tree-descent check, and a
plain Merk descent at a sum-budget position is rejected so the shape
can never be silently served as key selection.
Provable fold semantics are pinned to SKIP non-sum elements and SKIP
references — the two behaviors a single-subtree window proof can replay
deterministically (reference targets live outside the window). The
unified trusted read (run_path_query) switches to the same options so
read and verified results agree over any state; the legacy
AggregateSumPathQuery surface keeps its configurable options untouched.
Corrections made while pinning the semantics against the engine:
SumBudgetRead's cap field is renamed max_items_checked -> match_limit
(the engine decrements it per MATCHED result, not per scanned element —
the old name and doc were wrong; wire layout unchanged, stack unmerged),
sum_limit > i64::MAX is now rejected at validation (the engine's budget
arithmetic is signed), and AggregateSumQueryResult gains an
elements_scanned field (the window size the prover needs, and a useful
read-API datum on its own).
Gated on the new proof.sum_budget_in_v1_envelope slot (0 in V1..V3,
1 in V4) on both sides, with the V0-envelope refusal following the
ACOR template. verify_path_query returns the new
VerifiedPathQuery::SumBudget { matches, total, stop } with the
replay-attested SumBudgetStop reason.
Tests: round trips for all four stop conditions (budget — including
negative values giving budget back — match limit, exhaustion, plus
skip-semantics windows with foreign elements); read/verified agreement
across budget configs; forgeries (understated window, both directions
of exhaustion lying, plain-descent substitution); V3-refuses/V4-serves
gates on both sides. Full suites, clippy, verify-only build green.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
QuantumExplorer
force-pushed
the
claude/pathquery-axis-proofs-v1
branch
from
August 14, 2026 01:39
c6b2283 to
6dd6a79
Compare
QuantumExplorer
force-pushed
the
claude/pathquery-sum-budget-proofs
branch
from
August 14, 2026 01:39
4e3eb0d to
2559561
Compare
QuantumExplorer
merged commit Aug 14, 2026
4b42794
into
claude/pathquery-axis-proofs-v1
1 check passed
This was referenced Aug 14, 2026
Merged
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
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.
Context
PR 5 of the unified PathQuery effort (stacked on #799 ← #798 ← #797 ← #795). Sum-budget path queries —
ReadMode::SumBudget: walk items in key order, stop when the running net sum reaches the budget — gain a proof form, completing proof coverage for every read-mode shape.Design
The window is the proof. A new appended
ProofBytes::SumBudgetWindowvariant carries{ exhausted, window_len, merk_proof }: an ordinary Merk proof over exactly the window of elements the budget walk scanned. No new cryptographic machinery — the parent binding falls out of the ordinarycombine_hash(H(value), child_root)tree-descent check, and merk limit-proof semantics already attest "these are the first N elements in walk order".The fold replay is the attestation. The verifier executes the window proof with the query's own items and direction — limited to the claimed window on a stop, unlimited on claimed exhaustion (so the proof itself must prove the range end) — then replays the read engine's exact fold arithmetic element by element: saturating net-budget subtraction (negative sum items give budget back), the per-match limit, and the grove-version global scan cap including its counted-but-unprocessed tripping element. A window that continues past a fired stop, stops short of one, or misstates exhaustion is rejected. A plain Merk descent at a sum-budget position is also rejected, so the shape can never be silently served as key selection.
Provable fold semantics, pinned. The provable shape skips non-sum elements and skips references — the two behaviors a single-subtree window proof can replay deterministically (a reference's target lives outside the window).
run_path_query's trusted read switches to the same options, so read ≡ verified over any state; the legacyAggregateSumPathQuerysurface keeps its configurable options untouched.Engine-truth corrections made while pinning the replay against
element/aggregate_sum_query:SumBudgetRead.max_items_checked→match_limit: the engine decrements this per matched result, not per scanned element — the PR feat: ReadMode vocabulary — PathQuery expresses axis and sum-budget reads #797 name and doc were wrong (wire layout unchanged; the stack is unmerged so no compat concern)sum_limit > i64::MAXnow rejected at validation (the engine's budget arithmetic is signed and errors there anyway)AggregateSumQueryResultgainselements_scanned— the window size the prover needs, and a useful read-API datum in its own rightGating: new
proof.sum_budget_in_v1_envelopeslot (0 in V1–V3, 1 in V4) read by both sides; V0-envelope refusal follows the ACOR template.verify_path_queryreturnsVerifiedPathQuery::SumBudget { matches, total, stop }with the replay-attestedSumBudgetStop(BudgetReached/MatchLimitReached/HardScanCapReached/Exhausted).Tests
🤖 Generated with Claude Code