[rearden-grok]

Summary

• Pin Rob1Ham/btc-lean at d390f7932e64a134aec3cca1614bed3276539f2d as a shallow gitlink, third_party/btc-lean, the same mechanism as third_party/bitcoin. The previous pin was c6e8f5e91f30b1c690b4d0320404517120a8b52d. The 726 ids are unchanged (676 proven, 50 obsolete). 169 rows changed a field, including the consensus/policy split and the corrected merkle, median, witness-nonce, and powLimit sentences.
• Each proven rule is still named by a // btc-lean: comment on the statement that implements or tests it, or listed with a reason in docs/btc-lean-gaps.md. Comments that sat on the previous statement were moved onto the line the new sentence describes (upper median, witness nonce bytes, tapscript hashtype and pubkey size, NOP success, annex hash, key-path Schnorr, validation-weight serialization). status: obsolete needs no comment.
• A comment is an index, not a transferred Lean theorem, and not a claim of byte-for-byte agreement with Bitcoin Core. Wallet rows are not included. The Rust edits are comments only. No consensus behavior changes.

Test plan

• The gitlink SHA is d390f7932e64a134aec3cca1614bed3276539f2d.
• Checker reports 726 rules, 610 commented, 66 gaps, 50 obsolete. Gap reasons are non-empty. Commented ids, gap ids, and obsolete ids do not overlap.
• Required checks: qc, test, windows, macos, coverage on the pin bump.

[coreyphillips]

Two independent reviews.

needs changing before merge

• Many btc-lean ids are anchored to statements unrelated to the rule (crates/rbitcoin-consensus/src/block/facts.rs:119). The PR, the changelog and docs/consensus-tests.md all say each id is a comment on the statement that implements or tests the rule. A large share are not. In several cases the real implementing statement has no comment at all. To confirm, I cloned Rob1Ham/btc-lean at d390f79 into a temp copy of the tree and ran the checker. It passes with 726 rules, 610 commented, 66 gaps and 50 obsolete, matching the PR. I then dumped each of the 177 comment blocks next to the row's summary/check text and read the code under each one. Examples where the rule text and the code below disagree: block/facts.rs:119 BIP30 rows (BLK-096 INV-104 TXV-063 ...) on reject_same_block_create (same-block ordering). Real check: reject_bip30_unspent_prior, block/mod.rs:1171, uncommented. block/facts.rs:100 maturity rows (BLK-100 INV-028 TXV-021 TXV-070) on reject_genesis_coinbase_spend. Real check: reject_one_create, block/mod.rs:1197, uncommented. block/facts.rs:133 BLK-097 (91842/91880), INV-109 (prev-hash linkage) on reject_unresolved_spend(missing: bool) block/mod.rs:211 BLK-027/BLK-028 (first/only coinbase) on the bad-cb-length return. Real checks: mod.rs:156-166, uncommented. block/mod.rs:231 BLK-029 (coinbase scriptSig length) on the block stripped-size check block/mod.rs:263 INV-029 (in >= out), INV-032 (cb <= subsidy+fees) on txouttotal-toolarge block/mod.rs:276 BLK-036/TXV-053 (ConnectBlock accurate cost), SWT-024/026/027, TXV-051 (witness sigops) on the CheckBlock legacy-only x4 check (p.sigops is legacy counts). add_sigops, facts.rs:64, uncommented. block/mod.rs:61 SCR-044 "MIN_TRANSACTION_WEIGHT=240" on MIN_TX_WEIGHT = 10 * 4 block/mod.rs:82 TXV-059 (coinbase not script-verified) on the null-prevout check script/p2wsh.rs:45 SCR-135 "P2WPKH exactly 2 witness items" on the P2WSH hash compare script/interpreter.rs:920 SCR-125 (CLTV non-final input) on the CSV arm script/interpreter.rs:1438 INV-050 NULLDUMMY, SCR-041 "50 WU per sig" on check_signature_encoding header.rs:148 BLK-001 (header field order) on the BadVersion return bip34_tests.rs:6 BLK-070 (227931 + hash pin) on a test of OP_N heights 0..16 There are more in the same pattern, in interpreter.rs, scriptnum.rs:54 and tx_precompute.rs:846. The history explains it. These comments were converted from a file-level census table (83f402c), and aad3039 then reduced the checker to "the id appears in some comment", so nothing catches a misplaced id. Because these comments sit in consensus code, a reader who trusts // btc-lean: BLK-096 above reject_same_block_create will look for BIP30 in the wrong function. The presence-only gate also makes it costly to move ids to the right line later. Each id should go on the statement the row describes, or into docs/btc-lean-gaps.md.
• Several consensus rows index unrelated predicates and tests (crates/rbitcoin-consensus/src/block/mod.rs:1255). Several proven IDs point to code that neither implements nor tests their rule. Here, INV-017 through INV-021 and TXV-034 through TXV-039 describe BIP68 relative locks, but is_final_tx only checks absolute locktime. Their test annotations likewise point to sequence_final_ignores_locktime, which never calls the relative-lock predicate. I confirmed this against the pinned YAML and both bodies; the checker still reports 610 commented IDs. Similar mismatches include BLK-100 on the genesis-spend predicate and BIP143/Taproot IDs on core_sighash_all_rows, which exclusively calls legacy_signature_hash. The index needs an audit against the actual implementation and test sites.

worth doing, does not block

• Census script headers describe the earlier markdown design (scripts/btc-lean-census.sh:2). scripts/btc-lean-census.sh says it checks the "cited line" and "Does not need the third_party/btc-lean checkout". Run without the submodule, it exits 1 with third_party/btc-lean/spec/db/rules.yaml is not checked out. I ran it in this worktree to confirm. scripts/btc-lean-census.test.sh says the self-test rejects "a drifted line", but no line-drift check exists after aad3039. These comments describe what 83f402c did and will mislead someone running the script locally.
• Checker counts untracked .rs files, including nested worktrees (scripts/btc-lean-census.py:91). comment_ids uses root.rglob("*.rs") and only filters out target/ after the walk. Untracked copies count as coverage, so a local run can pass or fail because of files git does not track. I confirmed it in a temp copy of the tree: adding .spar-worktrees/other/src/a.rs with // btc-lean: INV-119 made the checker report INV-119: gap row also has a // btc-lean: comment. The main checkout here has .spar-worktrees/review-991 and review-1064 under it. The walk also traverses all of target/. Enumerating with git ls-files '*.rs' avoids both problems. CI is unaffected.
• Unsupported Taproot policy checks are counted as covered (crates/rbitcoin-consensus/src/block/mod.rs:847). TPR-021 and TPR-027 are counted as covered although their optional Taproot policy checks are absent. ScriptVerifyFlags has neither corresponding flag, and the other annotated site only tests P2WPKH LOW_S and STRICTENC. Likewise, SCR-154 and TPR-062 describe DISCOURAGE_OP_SUCCESS, but is_op_success only classifies opcodes and execution unconditionally accepts them. These rows belong in the gap ledger unless a relevant test site exists.
• BLK-128 is listed as missing despite existing witness autofill (docs/btc-lean-gaps.md:147). The gap ledger incorrectly says coinbase witness autofill is absent. fill_witness_reserved_value in crates/rbitcoin-rpc/src/methods/mine.rs:907 performs exactly this operation, and submit_received_block calls it before validation. With SegWit active, a commitment present, and an empty coinbase witness, it inserts one 32-byte zero item. BLK-128 should index that implementation instead of remaining a gap.

nits

• Gaps file states the input MoneyRange gap twice and contradicts BLK-103 (docs/btc-lean-gaps.md:119). "MAX_MONEY does not cap an input sum or the block fee" (INV-025 ... BLK-091) and "MoneyRange on every input fold" (TXV-069) describe the same missing cap in two sections. BLK-103 ("Σin ≥ Σout, both in MoneyRange") is commented on fee_from_values, but the gaps file says that function does not apply MoneyRange.