feat: provable sum-budget reads — SumBudgetWindow in the GroveDBProof V1 envelope - #807
Merged
Merged
Conversation
… 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>
Contributor
|
Caution Review failedThe pull request is closed. ℹ️ Recent review info⚙️ Run configurationConfiguration used: defaults Review profile: CHILL Plan: Pro Plus Run ID: 📒 Files selected for processing (19)
📝 WalkthroughWalkthroughSum-budget queries now limit matched items, generate terminal Merk window proofs, and verify replayed budget outcomes. Support is enabled from Grove V4. Tests cover round trips, stop conditions, tampering, trusted-read agreement, and version gates. ChangesSum-budget proof support
Estimated code review effort: 4 (Complex) | ~60 minutes Sequence Diagram(s)sequenceDiagram
participant PathQuery
participant ProofGenerator
participant SumBudgetWindowProof
participant ProofVerifier
participant VerifiedPathQuery
PathQuery->>ProofGenerator: submit sum-budget query
ProofGenerator->>SumBudgetWindowProof: build and encode terminal window
SumBudgetWindowProof-->>ProofVerifier: carry window metadata and Merk proof
ProofVerifier->>ProofVerifier: replay budget and stop conditions
ProofVerifier-->>VerifiedPathQuery: return matches, total, and stop
✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
Comment |
Codecov Report❌ Patch coverage is Additional details and impacted files@@ Coverage Diff @@
## develop #807 +/- ##
===========================================
- Coverage 92.23% 92.15% -0.08%
===========================================
Files 267 267
Lines 80895 81285 +390
===========================================
+ Hits 74612 74908 +296
- Misses 6283 6377 +94
🚀 New features to boost your workflow:
|
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.
Re-opens the work from #800, rebased onto
developafter #799 merged.Why a new PR: #800 was merged into #799's branch rather than into develop, and that merge was then reverted — so GitHub shows #800 as
MERGED(unreopenable) while develop contains none of its content. This branch replays the same commit on top of the merged #799.What it adds
Sum-budget path queries were the last shape with no proof form. They now prove through the standard V1 envelope — no new wire family — via
ProofBytes::SumBudgetWindow:limit = Nover the same items.VerifiedPathQuery::SumBudget { matches, total, stop }.Gated on
proof.sum_budget_in_v1_envelope(GROVE_V4+), mirroring the axis-descent gate on both sides.Rebase adaptations
SumBudgetRead.max_items_checked→match_limit: the engine decrements it per matched result, not per scanned element, so the old name described the wrong thing. Renamed with the field.Box<ReadMode>(develop'slarge_enum_variantfix) threaded through the newread_mode_at_pathresolver and the window builder —as_deref()at both sites.read_mode_at_pathis now the shared private resolver;axis_read_at_pathandsum_budget_at_pathare thin wrappers over it, so prover and verifier still cannot disagree about which layers carry read modes.verify_path_query_shape_tests::sum_budget_path_queries_have_no_proof_form_yet(added in feat: axis-ordered reads embedded in the GroveDBProof V1 envelope #799) asserted this shape had no proof form. That is exactly what this PR provides, so it becamesum_budget_verifies_through_the_unified_entry— a positive round trip asserting the proved window equals the trusted read'sresults, withtotal = 12andstop = BudgetReached.Verification
cargo test --workspace --all-features— greencargo clippy --workspace --all-features -- -D warnings— cleancargo build --no-default-features --features verify -p grovedb— cleangrovedb/src/tests/sum_budget_proof_tests.rs(round trips per stop reason, read-vs-proof differentials acrosssum_limit/match_limitcombinations, non-sum-element skip parity, forgery rejections, V4 gates)🤖 Generated with Claude Code
Summary by CodeRabbit
New Features
Improvements
Compatibility