Unit 8: the reference witness layer, ASSERT_MY_ANNEX, and bitlisp-commit - #68
Open
EvanWinget wants to merge 17 commits into
Open
Unit 8: the reference witness layer, ASSERT_MY_ANNEX, and bitlisp-commit#68EvanWinget wants to merge 17 commits into
EvanWinget wants to merge 17 commits into
Conversation
The seventh self assert, CONDITIONS.md's ASSERT_MY_ANNEX entry: one 32-byte operand at the generic cost, parsed through the fixed-width rule every 32-byte identity operand shares. The transaction view's BitLisp input gains an optional annex_hash, the BIP341 sha_annex digest of the annex its witness carries, None without one. The assert compares its operand against that field byte-exact, so an input without an annex fails it (unsatisfied_annex_assert). The admission rule of SPEC.md section 3.4: an input carrying an annex hash whose condition list holds no ASSERT_MY_ANNEX is unasserted_annex. It reads the input alone. validate_transaction runs it over every assembled input before any other rule, because a view built without the spend pipeline (every validation vector, the runner's carried inputs) must satisfy the same invariant, and the witness layer will run the same function at its own stage. The runner's tx shape and the compiler's vocabulary mirror gain the field and the name. Invariants: the self assert suite draws the input's own annex hash and annex operands from colliding pools, so environment independence and field equality now cover the assert, and a new property pins that unasserted_annex fires exactly when an annex is present and unasserted. The duplicate suite adds the assert to its idempotent pool.
gap_0x39_invalid pinned bad_condition_opcode while the vocabulary table of CONDITIONS.md section 2 already assigned 0x39 to ASSERT_MY_ANNEX (spec commit d50da1e, condition-record decision 30). The vector was wrong against the spec from that commit and stayed so on purpose until the implementation landed. It is replaced by the assert's parse case and its rejections: 31 and 33 byte operands, an empty operand, a pair operand, arity zero and two. costs.json gains the assert's 200 line, its exact-budget pair, and the annex condition in the all-opcodes sum, whose total rises by 200 to 14,405,400 (COSTS.md section 10, one generic entry more). validation/self-asserts.json pins the assert and the admission rule of SPEC.md section 3.4 in both directions: satisfied, wrong hash, assert without an annex, annex without the assert (with an empty list, with a satisfied assert, and with a failing assert the admission rule precedes), an annex asserted then a later assert failing on its own error, duplicate and contradictory annex asserts, and an annex hash on a plain input, which no rule reads. The annex every case hashes is 0x50 then the ASCII bytes "annex".
Section 3.3 said the nil program's empty condition list is rejected as bad_condition_list and the nil leaf has no valid spend. It contradicted CONDITIONS.md section 1, under which the empty list is a proper list and parses to no conditions, VALIDATION.md rule 5, which says the empty list charges nothing and satisfies any budget, and the corpus, where conditions/costs.json pins the empty list as valid and three validation files carry a valid input whose list is empty. Chialisp agrees: a coin spend producing no conditions is valid. The section now states what the rules give: the nil leaf is spendable by anyone, its spend contributing no condition. The two named programs differ in who chooses the conditions, the spender under the atom 1 and nobody under nil. Found while writing the witness layer's vector for the nil program.
Two consensus modules. commitment.py is the hashing of section 2: the tree hash over a node (moved here from the compiler, which now imports it, since the leaf script is consensus data), BIP340's tagged hash, the TapLeaf hash under a leaf version, the TapBranch fold of a control block's path, the annex digest, and a control block parsed into leaf version, parity, internal key, and path. spend.py is sections 3 and 4: evaluate_spend takes the input as the transaction carries it before evaluation, the witness elements in serialization order, and the budget, and returns the accrued cost with the input carrying its condition list, execution identity, and annex hash. The stages run in the spec's order. The annex is set aside by the BIP341 rule (two or more elements, the last beginning 0x50), then base consensus's own checks run as a precondition: two or more elements, a control block of 33 plus 32m bytes with m at most 128, BitLisp's leaf version, and the internal key tweaked by the revealed leaf's root giving the spent scriptPubKey with the parity bit matching. Those checks precede stage 1 in the spec and a spend failing them never reaches it, so they raise BaseConsensusError, a class outside the error taxonomy, never a code a vector could pin as BitLisp behavior. secp256k1 gains taproot_output_point, the full point, so the parity bit can be read. Stage 1 is widths: four elements, a 32-byte leaf script, the solution, program, and annex each at most MAX_WITNESS_ELEMENT_SIZE = 10,000 bytes, bad_witness. Stage 2 decodes the program and compares its tree hash to the leaf script, leaf_mismatch. Stage 3 decodes the solution. Stage 4 is run, stage 5 parse_conditions on the same budget and then the annex admission rule, the same function validate_transaction runs. The two new codes join CODES beside bad_encoding. Every element decodes under the strict deserializer, so an element with trailing bytes is bad_encoding at its stage, the surplus tolerance being inside the solution node, not around it.
The digest-domain table of section 2.4 named the tag BIP340/challenge with first byte 0x07. BIP340 spells its challenge tag BIP0340/challenge, the string secp_verify and the signature asserts hash under, whose digest begins 0x7b. Neither byte is 0x01 or 0x02, so the domain argument stood either way, but the table pins the tags a validator hashes under and must name them as hashed. Found by the test that computes every row of the table from the tag strings the implementation uses.
A fourth suite, one input's witness through the per-input stages of SPEC.md section 4. A case is the spent scriptPubKey, the witness elements in serialization order, and an explicit budget (section 3.2 is PROVISIONAL until COSTS.md section 9 fixes the function, so each case states its own). Success pins the parsed conditions, the three identity fields read from the control block, the annex hash when there is one, and the cost. A witness base consensus would refuse, or one under another leaf version, is a malformed vector, because the spec gives it no outcome. Four files. witness.json is section 3.1's rules in order and the stage order: the element count with and without an annex, the 0x50-tagged first element that is a solution and not an annex, the leaf script at 0, 31, and 33 bytes, each program and solution decoding failure, leaf_mismatch and what it precedes, the VM error and the parse error each preceding unasserted_annex, and the budget at one below and exactly the total. element-bound.json is rule 4 at and one above MAX_WITNESS_ELEMENT_SIZE for the solution, the program, and the annex, and the bound preceding the stage 2 failures. programs.json is section 3.3's two named programs, the atom 1 and nil, surplus solution data ignored, and section 3.4's annex in both directions at this stage: admitted under its assert, unasserted_annex without it, and the two stage 6 failures (another hash, no annex) passing the input stages as the spec places them. identity.json is sections 2.2 and 2.3: paths of 0, 1, 2, and 128 elements with siblings sorting on both sides of the leaf, two internal keys, both parity bits, cross-checked at generation against the vendored Bitcoin Core tagged hash. Each case states the outcome the spec predicts and the generator checked the implementation against that prediction, so the files pin predicted behavior, not observed.
The commitment scheme's hashing has real oracles and this file uses them. The official BIP341 wallet vectors give every leaf's control block, leaf hash, merkle root, and scriptPubKey under leaf versions 0xc0 and 0xfa: ControlBlock reads all twelve to the published identity, passes the base consensus check against the published output, and rejects a flipped output byte, a flipped parity bit, and a lengthened leaf script. The vendored Bitcoin Core framework is the oracle for the tagged hash over every tag the package uses, the leaf hash under any leaf version, and the annex digest's serialization, including the three-byte compact size a bound-sized annex needs. The tree hash is checked against the VM's sha256tree operator, which the differential harness pins to the consensus wheel. The digest-domain table of SPEC.md section 2.4 is recomputed from the tag strings: every first byte, none 0x01 or 0x02, and the table is exactly the set of tags the package hashes under, so a new tag fails here until the spec's table gains its row. Found the table's BIP340/challenge row wrong, fixed in the spec commit before this. The spend entry's invariants: under the anyone-can-spend program an annex passes the input stages exactly when the solution asserts its hash, the element bound is exact at MAX_WITNESS_ELEMENT_SIZE, the identity is the leaf hash and the path fold whatever the path, the annex split follows BIP341 on its edge cases, and a key-path spend or a foreign leaf version raises BaseConsensusError.
The commitment-hash utility queued 2026-08-14 and moved to this PR when the scheme fixed its output. From a program, as text or as serialized hex, it prints the leaf script (the tree hash), the tapleaf hash under BitLisp's leaf version, the merkle root, the internal key, the control block a spend of the leaf carries, and the taproot scriptPubKey. --sibling names the path elements leaf upward for a leaf that shares its tree, and --internal-key replaces the default, the BIP341 nothing-up-my-sleeve point, so the default output has no key path. The control block is the piece a spender needs and the one no other tool produces. Tests pin its output against the spend suite's identity vectors, which were cross-checked against the Bitcoin Core tagged hash, and its exit 2 paths: a program that does not parse or decode, a sibling that is not hex, a key of the wrong width, a key that does not lift. The eighth console script, listed with the others.
The commitment record gains a section for the reference witness layer: the three choices made in landing it (base consensus's checks run as a precondition outside the taxonomy, the annex rule run once per stage on two paths, the runner's witness form deferred to unit 9), and the two spec corrections the vectors and tests forced (the nil program, the challenge tag). Decision 3's owed vector is the test that recomputes the digest table, described where the vector was promised. The carried list loses the two items this PR delivered. The condition record's C25 row and decision 30 name the files their owed vectors landed in, the VM record's entry 7 the same for the disjointness pin. The glossary gains the control block, a term the spec used without a row. The REPL doc lists bitlisp-commit with the other one-shot commands and shows its output.
taproot_output_key now reads the x coordinate off taproot_output_point, so _apply_tweak had no caller in the consensus path, which the mutation pass showed as a survivor. Removed. Its three boundary tests, the scalar at the group order, the scalar one below it, and the sum at infinity, move onto _tweaked_point and compare points.
The mutation pass moved the compact-size threshold by one and the corpus did not notice: no annex sat on either side of 253 bytes, where BIP341's sha_annex prefix turns three bytes wide. Two cases in spend/programs.json, an annex of 252 bytes under the one-byte prefix and one of 253 under fd plus two little-endian bytes, each asserted by its program (SPEC.md section 3.4).
The seven touched modules, 1,027 mutants. Every survivor in the two new modules falls to the pytest suite. One gap became a vector, one dead function was removed, and one survivor class is new: checks base consensus makes before a spend reaches BitLisp, which the spend suite treats as malformed by design and no vector can kill.
CONDITIONS.md's self assert heading and count still read five conditions at 0x30 to 0x33 and 0x38 while the entry for 0x39, the cost table's "each self assert" row, and the implementation all file ASSERT_MY_ANNEX under the family. Six, with the annex hash named among the facts the family reads. VALIDATION.md's transaction view said an input without a condition list may carry the triple or not. It may carry annexHash or not on the same terms, and no rule reads either: the sentence now says so, the vector annex_on_plain_input_unread having pinned a shape the spec did not name.
Four spellings of BIP340's tagged hash became one, secp256k1's tagged_hash, which the challenge digest, the tweak scalar, the leaf and branch hashes, and the signature-assert digests all call. The digest-domain test now scans that one function's call sites, so a new tag cannot enter the package unseen. tx.py's compact-size prefix was a copy of commitment.py's and imports it instead. The tree hash is the sha256tree operator run with its charges discarded, not a second copy of its walk. conditions.py derives a taproot scriptPubKey through commitment.taproot_script_pubkey, which gives that function its consensus caller. The annex admission rule moves to spend.py, the per-input stage it belongs to, and validate_transaction imports it, so the dependency runs from the later stage to the earlier one. ControlBlock gains build, which derives the parity bit from the output key, and serialize, the inverse of parse, so the forward construction exists in the library once. The tree hash on the leaf_mismatch path is computed once, and TxInput's four optional 32-byte fields share one width check.
The command refused nothing above 128 siblings and printed a control block and scriptPubKey for a leaf base consensus can never spend. It now exits 2 past MERKLE_PATH_MAX_DEPTH. The control block comes from ControlBlock.build and the scriptPubKey from taproot_script_pubkey rather than hand assembly, and the doc says the first byte's low bit is the output key's parity, so d0 and d1 are both expected. The tools package imports the tree hash from the consensus module directly.
The digest-domain completeness test scanned a fixed tuple of four tags, so a new tagged_hash call would have passed it. It now collects every literal tag at a tagged_hash call site plus the signature bindings' tags, and checks the function is defined once. A round-trip property covers ControlBlock.build, serialize, parse, and check together. The lone self assert equality property draws an annex only under an annex assert again, so the five older families reach the equality check on every example rather than a third of them, the admission rule having its own property.
The REPL doc's bitlisp-commit example showed a control block whose first byte the reader would take as constant. It now shows the real output for the atom 1 and says the low bit is the output key's parity. The commitment record states why the digest-domain table is pinned by a test rather than the vector decision 3 first promised, and where the annex rule lives.
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.
The second half of unit 8: the reference witness layer over the commitment scheme PR 67 specified, ASSERT_MY_ANNEX, the element bound, every stage 1 to 3 failure vector, the 0x39 gap vector flipping, and the commitment-hash utility.
What changed
annex_hash. The assert compares against it, and the admission rule (an annex with no assert isunasserted_annex) is one function run at stage 5 by the spend entry and first invalidate_transaction.python/bitlisp/commitment.py: the tree hash (moved from the compiler, which now imports it), BIP340 tagged hash, TapLeaf hash, TapBranch fold,sha_annex, and a parsedControlBlockwith base consensus's check against the spent scriptPubKey.python/bitlisp/spend.py:evaluate_spend(tx_input, witness, max_cost)runs SPEC.md section 4's stages 1 to 5 and returns the cost and the input as the view carries it. Base consensus's checks run first as a precondition and raiseBaseConsensusError, a class outside the error taxonomy, because the spec gives such a spend no outcome.vectors/spend/:witness.json(section 3.1's rules in order and the stage order),element-bound.json(10,000 and 10,001 bytes for the solution, the program, and the annex),programs.json(the atom 1, nil, surplus tolerance, the annex both ways),identity.json(paths of 0, 1, 2, and 128, both sort orders, both parity bits).bitlisp-commit, the eighth console script: leaf script, tapleaf, merkle root, internal key, control block, scriptPubKey from a program.docs/mutation-triage.md.BIP340/challengewith first byte 0x07, and BIP340's tag isBIP0340/challenge, first byte 0x7b.Three implementation choices, steelmanned both ways in the session and ratified by Evan, are recorded in
docs/commitment-record.mdsection 5: base consensus's checks as an out-of-taxonomy precondition, the annex rule run on both paths, and the runner and REPL witness form deferred to unit 9's first PR, where the vault is the first consumer.Spec sections
SPEC.md 2.2 and 2.3 (the leaf hash and the identity read from the control block), 3.1 (the six witness rules), 3.2 (explicit budgets in every vector until COSTS.md section 9 exists), 3.3 (the two named programs), 3.4 (the annex), 4 (the stage table). CONDITIONS.md's ASSERT_MY_ANNEX entry. VALIDATION.md's transaction view (
annexHash). Condition-record decision 30, commitment-record decisions 3, 4, 5, and 12.Reading order
66fd49dconditions: ASSERT_MY_ANNEX and the admission rule (implementation and invariants)5253749vectors: 0x39 flips from gap to ASSERT_MY_ANNEX (the wrong vector's spec citation is in the message)f454598spec: the nil program is spendable by anyone4ca2488spend: the witness layer (commitment.py,spend.py, the two new error codes,taproot_output_point)1422edespec: the challenge tag row843b9a9vectors: the spend suite (runner and four files)43bcbd2tests: the witness layer against its oraclesa177b76tools: bitlisp-commit9ba6c27docs: the records, glossary, and REPL doc6bcbe76secp256k1: the dead x-only tweak helper removed (found by the mutation pass)629b04bvectors: the annex digest's compact-size boundary (found by the mutation pass)7b118c5docs: the mutation pass of 2026-09-06 in the triage recordFold-ins from a max-effort review of the PR head (no consensus defect found, 10 findings, all applied):
d907f8cspec: the self assert family counts six, the view's annex hash on a plain inputbd89255spend: one tagged hash (four spellings became one), one compact size, the tree hash as the operator, the annex rule moved to the per-input stage,ControlBlock.buildandserialize586fdcctools: bitlisp-commit refuses more than 128 siblings, builds the block through the libraryff05ed2tests: the digest-domain completeness check scans every tagged_hash call site, a control block round trip, the lone-assert property back at full density2507c52docs: the parity bit in the bitlisp-commit example, the record's two added rationalesVerify
The spend vectors were generated from predicted outcomes: the generator asserted the implementation against the spec's prediction for each case before writing it, and the identity cases were cross-checked against the vendored Bitcoin Core tagged hash. To re-derive one by hand,
bitlisp-commit "(q)"prints the leaf script, control block, and scriptPubKey that thesingle_leafcase ofspend/identity.jsoncarries.Not in this PR