The fee reserve: RESERVE_FEE and validation rule 7 - #40
Merged
Merged
Conversation
CONDITIONS.md gains the RESERVE_FEE entry at 0x50, the fees block rename, and the trimmed planned-entries paragraph. The declined entries ASSERT_FEE_LE, ASSERT_OUTPUT_COUNT, and ASSERT_INPUT_COUNT leave the planned list, with the decline rationale recorded in docs/condition-record.md decision 21 in the companion docs commit. VALIDATION.md gains the fee reserve as the fourth condition sort, rule 7 with the fee definition and the summed-reserve comparison, the composition guarantee's reserve sentence, the stage 4 fee extension, rule 2's extended validity enumeration, rule 4's counted-reserve bullet, the pre-registered slot-addition invariant re-scope, and four family invariants. Every sort enumeration in both documents is extended for the fourth sort, including rule 4's constrains-nothing bullet and the one-way implication paragraph, which now states what rule 7 reads. Semantics match Chia's deployed RESERVE_FEE exactly (checked-sum accumulation, fee at least the sum, boundary equality passes), probe-verified against the chia_rs wheel under COST_CONDITIONS. The MAX_MONEY operand bound follows the landed amount-operand convention and diverges from Chia only for operands no fee could satisfy, rejected at parse rather than at the comparison. Ratified by Evan 2026-08-09 (decision 21).
Decision 21 carries the seven ratified parts: the sequencing decision (vocabulary before costing, rule 5 last, decided fresh after decision 19's counted-sort deferral), RESERVE_FEE adopted at 0x50 matching deployed Chia, the fee reserve as the fourth condition sort, the ASSERT_FEE_LE decline with the decomposition proof, the ASSERT_OUTPUT_COUNT and ASSERT_INPUT_COUNT declines with the reserved-tier reintroduction path, the witness-dependent cell declines, and the error and encoding mechanics. Divergence C15 records the operand domain (MAX_MONEY at parse against Chia's below-2^64 at comparison) and the hardened-implementation obligation that a wrapping accumulator would loosen validity. Section 2 gains the fee-reserve probe provenance. The novel-layer register gains the rule 7 row. Two corrections from the adversarial review pass are recorded in place: decision 14's value-protection line no longer lists the fee reserve (its floor is fungible across inputs, so an aggregator can capture a spend's surplus while covering the reserve, pinned by the surplus-capture vector), and decision 20's register forward reference is reworded now that row 7 exists. The comparison doc's fee section flips its rows from planned to normative or declined, and its self-assert section, properties table, and Phase 2 observations catch up with decisions 19 through 21 (they predated the rule 4 and self assert landings). The glossary gains the RESERVE_FEE and fee reserve rows. The execution plan's vocabulary checkbox gains the 2026-08-09 amendment including the sequencing decision. The evaluation doc's obligation 4 gains a dated note recording the universal asserts' decline.
RESERVE_FEE parses at 0x50 with one minimally encoded operand in 0 to MAX_MONEY, the landed amount-operand convention (divergence C15: Chia accepts any canonical uint below 2^64 and fails the comparison instead). check_fee_reserve implements rule 7: the fee, inputs minus outputs, must be at least the exact sum of every reserve of every BitLisp input, one comparison for the whole transaction. Python integers keep the sum exact, so Chia's checked-add overflow error has no counterpart: a reserve stack no fee can reach fails the same comparison with the same insufficient_fee error. Semantics probe-verified against the chia_rs 0.46.0 wheel (provenance in docs/condition-record.md section 2): checked-sum accumulation within and across spends, boundary equality passes, zero reserves legal.
{"opcode", "reserve"} with the reserve as an integer, matching
the landed per-family forms.
Conditions file: operand sanitization from the probe corpus (canonical encodings, MAX_MONEY domain per divergence C15, arity, pair operand), duplicates parsing individually, and the fees-block gap codes pinned invalid. Validation file: the rule 7 probe corpus translated (boundary equality from both sides, within-input and cross-input accumulation, one-short rejections), the counted-not-collapsed k equals 3 case and the sum-not-max separating case, the split metamorphic pair within and across inputs, the fee-theft grafted-output regression case, zero reserve at zero fee, a reserve stack no fee can reach, non-BitLisp value funding the fee, a claim and reserve together, and the covered-merge composition case at the exact boundary. Five cases from the five-agent review: the surplus-capture acceptance vector pinning that the reserve's floor is fungible across inputs and protects no coin's surplus (decision 14 correction), two above-2^32 cases separating exact arithmetic from 32-bit truncation of either comparison side (the recorded high-bytes lesson), and two off-boundary cases separating numeric from lexicographic atom comparison, which every prior valid case sat too close to the boundary to catch.
The spec's four family invariants (operand monotonicity, split, boundary raise-by-one, fee-theft grafted output) plus the carrier-independence property (moving a reserve between inputs), the re-scoped slot-addition invariant with its unconditional input half, the covered-merge composition property, and two deterministic separating cases (sum not max, counted not collapsed). The reserve and fee pools cross 2^32 so the strategies exercise the truncation boundary the vector corpus pins. Teeth verified by mutation: max-semantics, set-collapse, strict-inequality, 32-bit-truncation of either comparison side, and lexicographic atom-compare mutants each die in the vector corpus, the first three in this suite as well.
A transaction violating exactly one condition-layer rule carries that rule's code and vectors pin it. A transaction violating more than one is invalid under each, and any violated rule's code conforms: rejection is the consensus outcome, the code is diagnostic. This states explicitly the freedom the corpus already exercised implicitly, closing the cross-rule precedence flag from the self assert PR. Ratified by Evan 2026-08-09 (decision 22 in docs/condition-record.md).
Complete error enumeration considered and declined on three grounds: fail-fast bounds the work an invalid transaction can extract, the set of all errors is ill-defined because failures gate evaluability in the stage frame's dependency order, and identical-set reporting widens the cross-implementation conformance surface for zero consensus benefit. Full-enumeration diagnostics recorded as Phase 3 and 5 tooling outside the consensus contract.
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.
What this adds
RESERVE_FEE at opcode 0x50, the vocabulary's fee floor, and validation rule 7: the transaction's fee (inputs minus outputs) must be at least the exact sum of every reserve of every BitLisp input, error insufficient_fee. The fee reserve is the fourth condition sort beside claims, asserts, and message records: counted, not idempotent, occurrences sum. Semantics match Chia's deployed RESERVE_FEE exactly, probe-verified (16 probes against the chia_rs 0.46.0 wheel under COST_CONDITIONS, provenance in the condition record's section 2).
The unit also records four declines (decision 21): ASSERT_FEE_LE (transaction-wide form is merge-poison per decision 14, per-input form decomposes into ASSERT_MY_AMOUNT plus claims), ASSERT_OUTPUT_COUNT in both exact and floor forms, ASSERT_INPUT_COUNT mirroring it, and the witness-dependent grid cells (weight, fee rate) as self-referential. The reserved tier is the recorded reintroduction path. The same session ratified the Phase 2 sequencing: AGG_SIG next, rule 5 last so costing prices the complete vocabulary.
A follow-up ratified after the review landed as the final two commits: decision 22 settles the cross-rule error question raised in PR 39 and re-raised by this review's surviving check-reorder mutant. Fail-fast stays, multi-violation error codes are unpinned by design, and full-enumeration diagnostics are recorded as Phase 3 and 5 tooling.
Spec authority
Read the commits in this order
spec:the normative text, self-contained.docs:decision 21, C15, provenance, and the catch-up corrections described below.validation:the implementation, one parse function and one comparison.tools:the pinned JSON form.vectors:14 conditions cases, 21 validation cases.tests:10 hypothesis invariants plus two deterministic separating tests.spec:the decision 22 error-code paragraph.docs:the decision 22 record.Verify independently
Mutation teeth: max-semantics, set-collapse, strict-inequality, 32-bit truncation of either comparison side, and lexicographic atom-compare mutants all die in the vector corpus alone.
The five-agent review, catches folded in pre-PR
Flagged for your judgment