Phase 2 opening: condition encoding, transaction view, matching rule 1 - #20
Merged
Merged
Conversation
CONDITIONS.md section 1 makes the encoding normative: proper-list shape, one-byte opcodes, the three-tier code space (assigned, invalid, reserved 0x80 to 0xff), strict arity and minimal integer encodings for assigned conditions, and the family-block layout with intra-block gaps invalid. Every condition-layer error code is named at the rule that raises it, so the spec stays self-contained. Section 2 opens the vocabulary with CREATE_COIN (0x01): full script bytes plus amount, matched injectively under MATCHING.md rule 1. Chia's puzzle-hash argument and optional memo argument are both deliberately diverged from, rationale in the curation note and in the condition record landing later in this PR. Decisions ratified by Evan, 2026-07-29.
MATCHING.md gains its normative core. The transaction view fixes what matching can see, enumerates the base-rule subset the model enforces (including no duplicate outpoints), and states that no rule beyond base consensus applies, in particular no output scriptPubKey size bound. Rule 1 states injective multiset output matching as multiset containment, with the equality-only matching predicate as binding normative text, so any future relaxation must amend visible prose. Rule 6 fixes the reserved-condition tier: declared cost counting against the spend total under rule 5's accounting, a floor of 500, arguments after the cost unconstrained forever, and the non-consensus policy note discouraging unassigned use. The invariants section is rewritten while being made normative, and every change to the Phase 0 stub text is flagged here for review: 1. Direction correction: the stub said removing a condition never turns an invalid transaction valid, which is false under rule 1 (removing one of two over-claims restores validity). The true monotonicity is the reverse and is now stated in both halves: removing a condition never invalidates, adding one never validates. 2. Value conservation moves from a suite-enforced invariant to a model precondition, since matching never sees a transaction that violates it. 3. The output-removal bullet narrows to the exactly-covered form, because removing a slot whose content still has surplus slots leaves every claim satisfied under multiset semantics. The metamorphic bullet narrows identically. Decisions ratified by Evan, 2026-07-29.
docs/condition-record.md is the Phase 2 counterpart of the VM record: the divergence-from-Chia table (C1 script bytes, C2 memo decline, C3 duplicate claims allowed, C4 the three-tier code space against Chia's ignore-with-cost-table behavior, verified in chia_rs source), reference provenance (CHIP-0025, CHIP-0049, the bllsh reading of 2026-07-29), the design decision record for everything ratified in the 2026-07-29 design session, and the novel-layer register naming the oracle substitute for each matching rule. CLAUDE.md ground rule 3 now names both records. docs/README.md gains the pointer.
bllsh was read on 2026-07-29 for the CREATE_COIN_TAPROOT decision (the D-CC2 entry in docs/condition-record.md). The fetch script now clones it so the checkout is reproducible.
Implements CONDITIONS.md section 1 and the CREATE_COIN entry, and the shape rules of MATCHING.md rule 6: proper-list structure, one-byte opcodes in three tiers, strict arity and minimal integer encodings for CREATE_COIN, and the reserved tier with its declared cost and floor. Six new error codes, one per distinct rejection reason, so every error path can be pinned by its own vector. The errors module docstring now states the split evidence standard: oracle parity for VM codes, the named spec rule for condition and matching codes.
The transaction model carries exactly what MATCHING.md's transaction view names and enforces the base-rule subset it represents (value conservation, ranges, no duplicate outpoints) at construction, so matching never sees a transaction Bitcoin base consensus would reject. It deliberately enforces nothing base consensus does not: output scriptPubKeys carry no size bound, since the 10,000-byte rule is CREATE_COIN's claim-argument rule, not a slot rule. Model misuse is ValueError, never a spend failure. Rule 1 is multiset containment by counting: claims from all BitLisp inputs jointly, slots from the outputs, reject when any content is claimed more times than slots carry it. The equality-only matching predicate that makes counting sufficient is normative in the spec. The package exports for the whole condition layer land here, with the modules they name, so every commit imports standalone.
Both runners keep the vm suite's discipline: closed case keys on every object including output entries, closed expect shapes, unknown error codes rejected, duplicate case names rejected. The per-suite loop is factored into one helper and the vm suite now uses it too. The conditions runner parses a serialized condition-list node and pins either the parsed form or the error code. The matching runner builds the transaction model from JSON. A condition-list parse failure is a case outcome (an invalid spend), but a conditions field that does not deserialize is a malformed vector, because the matching stage receives already-materialized evaluation results and a serialization failure is not a possible outcome there. A model ValueError is likewise a malformed vector, since the model only represents transactions Bitcoin base rules accept.
vectors/conditions/encoding.json pins CONDITIONS.md section 1 and MATCHING.md rule 6: 35 cases covering every rejection rule (structure, opcode tiers, CREATE_COIN arity and argument strictness, reserved declared-cost rules) plus the acceptance boundaries (zero amount, MAX_MONEY, the 10,000-byte script, the cost floor, shapeless reserved arguments). vectors/matching/create-coin.json pins MATCHING.md rule 1 with the duplicate-CREATE_COIN theft case as vector #1, the honest batching counterpart, batching-wallet shapes at three inputs, mixed transactions with non-BitLisp inputs and unmatched outputs, the C3 divergence cases (duplicate claims from one input), metamorphic neighbors (amount off by one, script byte flip), and the oversized-unclaimed-slot case pinning that output slots carry no size bound. vectors/README.md documents both case shapes.
One property per invariant the spec names, over a small content pool chosen for dense claim and slot collisions: the containment statement restated independently, reorder invariance across inputs, outputs, and condition lists, monotonicity in both directions (removing a claim never invalidates, adding one never validates), the unmatchable-claim rejection, the exactly-claimed-output removal and mutation metamorphics, and the generalized theft property (k identical claims never fit k minus one identical slots). Model preconditions (value conservation, duplicate outpoints, empty sides, amount ranges) are pinned as ValueError, distinct from spend invalidity.
EvanWinget
force-pushed
the
matching-rule1
branch
from
July 30, 2026 03:54
790dbfe to
2d8ead8
Compare
Two open items from the opening PR's review are now decided by Evan (2026-07-29). Curation notes stay in spec/CONDITIONS.md, resolving the conflict between the Phase 0 stub's plan and the spec-purity rule, with the exception recorded in ground rule 1. The reserved cost floor stays at 500 per the CHIP-0049 precedent, revisited when matching rule 5 lands.
The containment property restates the matcher's own counting, so it pins the implementation against drift but cannot judge the algorithm. The new property implements rule 1's other formulation, a naive backtracking search for an injective claim-to-slot assignment, and asserts the two formulations never disagree. If counting is ever the wrong reduction of injective matching, this is the test that says so.
A cold-reader exercise on the rule 1 vectors (Evan, 2026-07-29) surfaced the natural misreading: CREATE_COIN's amount taken as the spending input's value, pulling value conservation into matching where it does not belong. The entry now states what the amount is not: no debit from the input, no per-input value tracking, and conservation stays with Bitcoin's base rules transaction-wide.
EvanWinget
added a commit
that referenced
this pull request
Jul 31, 2026
Records the 2026-07-31 decisions by Evan carried into the CREATE_COIN_TAPROOT PR: the empty-root sentinel for key-path-only outputs (separate opcode and outright decline both considered and declined), the two rejection branches unreachable by any constructible vector and pinned by contrived-scalar unit tests instead (a recorded exception to the every-error-path-is-a-vector rule), and the BIP341 wallet test vectors as the vendored tweak-derivation oracle. Also ticks the Phase 2 tx-model checkbox in the execution plan, housekeeping owed since PR #20 landed python/bitlisp/tx.py.
EvanWinget
added a commit
that referenced
this pull request
Jul 31, 2026
Records the 2026-07-31 decisions by Evan carried into the CREATE_COIN_TAPROOT PR: the empty-root sentinel for key-path-only outputs (separate opcode and outright decline both considered and declined), the two rejection branches unreachable by any constructible vector and pinned by contrived-scalar unit tests instead (a recorded exception to the every-error-path-is-a-vector rule), and the BIP341 wallet test vectors as the vendored tweak-derivation oracle. Also ticks the Phase 2 tx-model checkbox in the execution plan, housekeeping owed since PR #20 landed python/bitlisp/tx.py.
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
1 participant
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 is
The opening Phase 2 PR, the thin vertical slice ratified in the 2026-07-29 design session: the condition-list encoding, the CREATE_COIN entry, the transaction view, matching rule 1 (injective multiset output matching), and matching rule 6 (reserved conditions), with the duplicate-CREATE_COIN theft case as regression vector #1 and the first hypothesis invariants. CREATE_COIN_TAPROOT was ratified in the same session and lands as its own PR right after this one.
A five-agent review pass (independent reviewers plus per-issue confidence scoring) ran before this revision and its findings are folded into the commits: the spec's error-code cross-reference was made self-contained, the transaction model no longer enforces a scriptPubKey size bound base consensus lacks (with a vector pinning the oversized-slot case), the spec's base-rule enumeration now includes duplicate-outpoint rejection, the matching runner closes output-entry keys and rejects non-deserializing condition hex as malformed vectors, the invariant suite covers both monotonicity directions, and every commit imports standalone for bisectability.
Spec sections
Read the commits in this order
Flagged for review: changes to pre-existing stub text
The Phase 0 stub's invariants said removing a condition never turns an invalid transaction valid. Under rule 1 that is false: removing one of two over-claims restores validity. The true property is the reverse monotonicity and the spec now states both halves. Two further stub rewrites (value conservation as model precondition, the output-removal and metamorphic bullets narrowed to the exactly-covered form) are enumerated in commit 2's message. If any of the three reads wrong to you, that is a spec conversation before merge.
Open design question, resolved during review
CONDITIONS.md's curation notes carry rationale prose, which the Phase 0 stub explicitly planned but the newer spec-purity rule (spec states behavior only, rationale in docs/) arguably forbids. Two recorded decisions conflict. Resolved by Evan during review: curation notes stay in the spec, the exception is recorded in CLAUDE.md ground rule 1 and the condition record, final commit. The reserved cost floor of 500 was ratified in the same pass.
Verify independently
The diff harness run confirms the VM intersection is untouched by this PR. The two new suites have no external oracle by design, which is why the invariant suite and the adversarial corpus land in the same PR as the rule they pin (ground rule 4).