Skip to content

ASSERT_MY_TAPTREE, the cheap identity assert - #60

Open
EvanWinget wants to merge 6 commits into
mainfrom
identity-assert
Open

ASSERT_MY_TAPTREE, the cheap identity assert#60
EvanWinget wants to merge 6 commits into
mainfrom
identity-assert

Conversation

@EvanWinget

@EvanWinget EvanWinget commented Aug 22, 2026

Copy link
Copy Markdown
Owner

Lands the 2026-08-22 identity-assert amendment (decision by Evan, recorded in the execution plan): spec, implementation, vectors, tests, and the condition-record decision. The vault and singleton rework onto the new assert follows in its own PR, which also decides the fate of ASSERT_MY_TAPROOT.

What changed

  • ASSERT_MY_TAPTREE at 0x38. (0x38 internal_key merkle_root), a sixth self assert at CONDITION_GENERIC_COST (200). It asserts the spending input's execution identity byte-exact: the internal key and merkle root base consensus authenticated from the control block. It proves what ASSERT_MY_TAPROOT proves at 1,300,200 by derivation, with no derivation.
  • The transaction view's identity is a triple. internalKey joins tapleaf and merkleRoot, validator-filled, required together on a condition-carrying input. Rule 3 reads the first two, the self asserts read the last two, no specifier reads the internal key. The view takes the triple as authenticated and derives nothing from it.
  • Operand domains. Both operands exactly 32 bytes. The internal key is width-checked only (the field it is compared against always lifts, so a non-point operand fails as unsatisfied, the signature asserts' treatment of a pubkey). The root is never empty, the one parse-level difference from ASSERT_MY_TAPROOT. Error unsatisfied_taptree_assert.
  • Corpus. Every condition-carrying input in the validation corpus (415) gains internal_key: the NUMS point on the 82 honest vault and singleton instances, chosen by a checkable rule (the scriptPubKey equals the tweak of NUMS by the merkle root), filler elsewhere. Every pinned program, payload, and signature is byte-identical.

Spec sections

CONDITIONS.md self asserts (the family preamble and the 0x38 entry), VALIDATION.md transaction view and invariants, COSTS.md section 10. Decision 28 and divergence row C24 in docs/condition-record.md, with the width-only operand steelmanned both ways.

Read the commits in this order

  1. spec: ASSERT_MY_TAPTREE, the transaction view gains the internal key
  2. conditions: ASSERT_MY_TAPTREE, the internal key on the transaction model
  3. vectors: the corpus gains the internal key, the taptree cases
  4. tests: the internal key on every fixture, taptree coverage
  5. docs: decision 28, divergence C24, glossary and corpus shape
  6. review fold-ins: oracle snapshot restored, identity closure, spec wording, one width rule (the review comment below lists the ten findings)

Verify independently

.venv/bin/pytest python/tests                 # 815 pass
.venv/bin/python tools/run_vectors.py         # 38 files, 1132 cases
PATH=.venv/bin:$PATH ci/lint/lint.sh

The vault and singleton closure tests recompile both puzzles and recompute every pinned program and conditions payload, so the sweep of their instance inputs is checked against source. In the vector diff, every line the sweep touched is an added internal_key line (plus the comma the preceding line gains): git diff main -- vectors/validation | grep '^[-+] ' | grep -v internal_key shows only the merkle_root comma lines outside self-asserts.json. The VM diff harness is untouched (no operator change).

Notes for review

  • The model does not check that an input's scriptPubKey is the tweak of its identity, the stance PR 58 set for the pair. The invariant relating the two asserts is therefore conditional on an honest input, stated as such in VALIDATION.md, and pinned by a hypothesis property over honest-spk inputs and by the taptree_ignores_scriptpubkey vector, which shows a taptree assert satisfied over a P2WPKH filler script.
  • A worked spend: a compiled program emitting one ASSERT_MY_TAPTREE validates at total cost 612. The same spend through ASSERT_MY_TAPROOT costs 1,300,612.
  • The language-level addition makes ASSERT_MY_TAPTREE a reserved name, the same deliberate source-compatibility break as every prior vocabulary addition, pinned by the compiler vocabulary test.
  • The empty merkle root that ASSERT_MY_TAPROOT accepts (no script tree) has no taptree spelling: a BitLisp spend always executes a leaf. That case is unsatisfiable on any BitLisp input already, a point for the 0x37 decision at the rework PR.

The 2026-08-22 amendment, decided by Evan and recorded in the
execution plan. Every puzzle spend so far paid 1,300,200 for
ASSERT_MY_TAPROOT to re-derive a scriptPubKey that base consensus
had already authenticated from the control block.

VALIDATION.md changes:

- The transaction view's execution identity becomes a triple:
  tapleaf, merkleRoot, and internalKey, the 32-byte x-only
  internal key the control block carries. Base consensus
  authenticates all three during every script-path spend. The
  view takes the triple as authenticated and derives nothing from
  it: no rule recomputes the scriptPubKey from the key and root.
  Rule 3's specifiers read tapleaf and merkleRoot, the self assert
  family reads internalKey and merkleRoot, and no specifier reads
  internalKey. Decision 26's decline of internal-key addressing
  stands for counterparts, where the control block proves no
  possession. A self assert over the spending input's own key
  claims no possession: it pins which tweak preimage the coin's
  scriptPubKey was built from.
- Invariants: the lone-self-assert bullet covers multi-operand
  asserts, ASSERT_MY_TAPTREE's outcome is unchanged by the spent
  scriptPubKey, and on an input whose scriptPubKey is the taproot
  output of its identity (every input base consensus admits)
  ASSERT_MY_TAPTREE and ASSERT_MY_TAPROOT over equal operands
  produce identical outcomes, modulo a tweak collision.

CONDITIONS.md changes: ASSERT_MY_TAPTREE at 0x38, the next code
after the taproot assert, 0x34 to 0x36 staying the recorded
decline gap. Two 32-byte atom operands, the internal key
width-checked only (the view's key always lifts, so a non-point
operand never matches and fails as unsatisfied, the same treatment
the signature asserts give a pubkey operand), the merkle root
never empty (the rule 3 operand's domain, the one parse-level
difference from ASSERT_MY_TAPROOT). One condition over both
fields rather than two single-field asserts: the pair is one fact,
the tweak preimage, and mirroring ASSERT_MY_TAPROOT operand for
operand makes a puzzle's adoption an opcode swap. Cost
CONDITION_GENERIC_COST, stage 2, error unsatisfied_taptree_assert.
The family preamble counts six conditions and states the internal
key's content class.

COSTS.md section 10: one sentence stating why the new assert
charges the generic constant alone.
Implements the spec commit. ASSERT_MY_TAPTREE parses as two
width-checked 32-byte atoms, the internal key then the merkle root,
at CONDITION_GENERIC_COST. The internal key is not lifted: the
field it is compared against always lifts, so a non-point operand
fails as unsatisfied, the treatment the signature asserts give a
pubkey operand. The root is never empty, the one parse-level
difference from ASSERT_MY_TAPROOT.

The transaction model's TxInput gains internal_key beside tapleaf
and merkle_root, and the construction rule requires all three on a
condition-carrying input. The model takes the triple as
consensus-authenticated and never re-derives the scriptPubKey.
check_self_asserts compares both operands against the carrying
input's fields, raising the new unsatisfied_taptree_assert with
both demanded and carried values in the message.

Tooling follows: the runner's context loader accepts internal_key
and the target input must carry the triple, the compiler's
condition vocabulary gains the name (a reserved name, the same
deliberate source-compatibility break every prior addition made),
and the vector runner renders the parsed condition as its two
operands with nothing derived.
Mechanical sweep, the spec commit authorizes every change: each of
the 415 condition-carrying inputs in the validation corpus gains
the now-required internal_key. The 82 honest puzzle instances in
the vault and singleton files carry the NUMS point both puzzles
curry, chosen by a checkable rule (the input's scriptPubKey equals
the tweak of NUMS by its merkle root), the family suites and the
two hostile foreign-script inputs carry fixed filler no case reads.
Every pinned program, conditions payload, and signature is
byte-identical to before.

New conditions cases pin the parse surface: both operands at
exactly 32 bytes, the empty root rejected (the one parse-level
difference from ASSERT_MY_TAPROOT), a key that lifts to no curve
point parsing (the width-only decision), arity and pair-operand
rejections. The gap case moves from 0x38 to 0x39. The costs suite
pins the 200 charge, its exact-budget pair, and the all-opcodes
pair re-totaled.

New validation cases pin the semantics: satisfied on an honest
input, each operand mismatching alone, a non-point operand failing
as unsatisfied rather than malformed, the assert ignoring the spent
scriptPubKey (the model takes the identity as authenticated and
derives nothing), agreement with ASSERT_MY_TAPROOT on an honest
input, the covenant recreate pattern, duplication idempotence, and
two inputs each asserting its own identity against a neighbor's.
Every case executed at generation.
Every fixture constructing a condition-carrying input gains the
internal_key the model now requires: fixed filler in the family
suites and tool tests, per-input distinct values in the message
invariants, and the NUMS point on the vault and singleton instance
inputs, the key both puzzles curry.

The self assert invariants now draw the input's execution identity
from a small pool the taptree operands share, so satisfied and
unsatisfied taptree asserts are both dense. AssertMyTaptree joins
the strategy pool, which puts it under the environment-independence
and lone-assert properties, and two properties are new: the
taptree assert's outcome never depends on the spent scriptPubKey,
and on an input whose scriptPubKey is the taproot output of its
own identity the taptree and taproot asserts over equal operands
are satisfied together and fail together.

New coverage elsewhere: the model refuses a condition-carrying
input missing any one of the three identity fields and an internal
key at the wrong width, the corpus loader maps those to context
errors, the runner refuses a target input missing any field, the
cost table pins 200, and the compiler vocabulary table pins the
name at 0x38 with its count.
The condition record gains decision 28 (the cheap identity assert:
the internal key read by self asserts only and why decision 26's
objection does not reach it, the view deriving nothing from the
triple, the width-only operand with both sides steelmanned, the
never-empty root, one condition over both fields as a stated
exception to decision 20, opcode 0x38, the subsumption of
ASSERT_MY_TAPROOT with its fate deferred to the rework PR) and
divergence row C24. The register's rule 2 row names the taproot
assert as the taptree assert's oracle through the agreement
invariant. The comparison doc gains the self-assert row, the
glossary the condition and the widened identity triple, the
vectors README the internal_key input field and the parsed shape.
The execution plan's amendment bullet records what landed and what
the rework PR still owes.
…ding, one width rule

Ten verified findings from the review pass, most severe first.

The implementation commit had reformatted the five vendored Bitcoin
Core oracle files through a formatter pass that omitted the
third-party exclusion, breaking the verbatim guarantee their README
records by sha256. The files are restored to main's blobs, the lint
script's hint now carries the exclusion, and a new provenance check
compares every file the README table lists against its recorded
hash, so the guarantee is enforced rather than assumed.

Nothing checked that an instance vector's identity triple derives
its scriptPubKey, so the honest-key rule the sweep applied was
prose only, and the forthcoming rework removes the taproot assert
that would have caught a mis-set key. Both puzzle suites gain a
closure test: every condition-carrying input's scriptPubKey is the
tweak of its internal key by its merkle root, the leaf equals the
root, and the vault file's two filler inputs are counted so the
exemption cannot widen.

Spec wording: the agreement invariant says the two asserts are
satisfied together and fail together, each with its own error,
rather than "identical outcomes", and the CONDITIONS.md entry
carries the honest-input qualifier. The environment-independence
invariant names the execution identity beside prevout data. Rule 3
no longer calls its two fields the view's execution identity, which
is now a triple. The family preamble states the internal key's
content class directly instead of pointing at a table that has no
row for it. The language reference counts 27 condition names, and
three docstrings that said pair now say triple.

Code: one _fixed_width_atom helper replaces four hand-rolled copies
of the exact-width atom check, so the operands decision 28 says
share a domain share it in code. Vectors pin error codes only, so
the unified messages change no expectation.

Tests: AssertMyTaptree joins the rule 4 duplication pool and its
idempotent set, the runner's render table pins its output, and the
agreement property looks up precomputed tweaks instead of deriving
two per example, which takes the suite from 120 to 102 seconds.
@EvanWinget

Copy link
Copy Markdown
Owner Author

Review pass (code-review skill, high, Fable finders, adversarial verify)

Ten findings survived verification, all folded in commit 5f2b217:

  1. Vendored oracle files reformatted (severe). The implementation commit's formatter pass had reformatted the five Bitcoin Core files under tools/oracle/bitcoincore/ (AST-equal, pure formatting), silently breaking the verbatim guarantee their README records by sha256. Restored to main's blobs (git diff main -- tools/oracle is empty). Root cause was the lint script's printed hint omitting the third-party exclusion, now fixed, and no check comparing the snapshot to the README table, now added as an oracle provenance lint step.
  2. Instance-vector identity unchecked. The "honest NUMS by a checkable rule" claim was prose only, and the rework PR will remove the ASSERT_MY_TAPROOT that currently catches a mis-set key. Both puzzle suites gain a closure test: every condition-carrying input's scriptPubKey is the tweak of its internal key by its merkle root, leaf equals root, the vault file's two filler inputs counted.
  3. "Identical outcomes" was false: the two asserts agree on satisfied/failed, not on error code. Reworded to "satisfied together and fail together, each with its own error", and the CONDITIONS.md sentence gained the honest-input qualifier it lacked.
  4. Environment-independence invariant still said "prevout data alone". Now names the execution identity.
  5. Family preamble cross-referenced rule 3's stability table for a field the table has no row for. States the class directly now.
  6. Rule 3 called its two fields "the execution-identity fields of the transaction view", which is now a triple. Reworded.
  7. Rule 4 property never duplicated a taptree assert (pool and idempotent set), and the runner's render table had no row. Both added.
  8. Stale counts and docstrings: language.md said 26 names, three docstrings said pair. Fixed.
  9. Slow property: the agreement test derived two tweaks per example. Precomputed, suite 120 s to 102 s.
  10. Four copies of the 32-byte width check. One _fixed_width_atom helper now serves the fixed-byte self asserts, the taproot internal key, the rule 3 identity operands, and the taptree operands. Vectors pin codes only, so the unified messages change no expectation.

Dropped after verification: the costs.json all-opcodes re-pin (correct, +200), partial identity on non-condition inputs (pre-existing, no rule reads it), single error code for the conjunction (decision 28).

Final: 815 tests, 1132 vector cases, lint clean including the new provenance check.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant