/light-client-proof-verification

name: "light-client-proof-verification"
description: "L1 trigger - audits light client and cross-chain proof verification: Merkle proof soundness, ICS-23 subkey handling (Dragonberry class), state root checks, message integrity."

Injectable Skill: Light Client Proof Verification

> **L1 trigger**: `L1_PATTERN=true` AND (`light_client/` OR `ics23/` OR `merkle/` OR `proof/` OR `verify_proof` OR `verify_root` OR `validate_path` OR `merkle_tree` OR `state_root` OR `trie_proof` OR `ibc/` OR `beacon-api-client/` detected in recon subsystem map) > **Inject Into**: `depth-consensus-invariant` or `depth-external` > **Language**: Go and Rust > **Finding prefix**: `[LC-N]` > **Status**: v0.1 draft, Round 4 exemplars pending

Orchestrator Decomposition Guide

• Sections 1, 2: depth-consensus-invariant (proof soundness)
• Section 3: depth-external (cross-chain assumptions)
• Section 4: depth-edge-case (boundary + adversarial inputs)

When This Skill Activates

Recon identifies light-client or cross-chain proof verification code. This skill is the most consequential for cross-chain bridges and IBC-adjacent code because a proof-verification bug can allow forged state to be accepted as canonical — the Dragonberry class.

1. Proof Format Fingerprinting

Identify the exact proof format used:

| Format | Identifier | Notable pitfalls | |---|---|---| | **Merkle-Patricia Trie (MPT)** | Ethereum state proofs, `eth_getProof` | RLP decode edge cases; extension/branch collision | | **IAVL+** | Cosmos SDK `x/store` | Left-right ordering; ICS-23 subkey encoding | | **Sparse Merkle Tree (SMT)** | Aptos, Sui, Celestia | Empty-leaf handling; default hash values | | **Verkle** | Future Ethereum | KZG commitment; opening soundness | | **SSZ proofs** | Ethereum Beacon chain | Generalized index encoding | | **ICS-23** | IBC light clients | Generic proof spec; multiple backends |

Write the format into the finding header.

2. Soundness Checks Per Format

2a. Merkle-Patricia Trie (Ethereum state proof)

• **RLP decode strictness**: does the decoder reject non-canonical RLP encodings? Leading zeros, empty-byte integers, overlong encodings?
• **Hash pre-image check**: the proof path hashes must chain correctly from leaf to root
• **Key encoding**: the MPT key is nibbled (4-bit). Off-by-one in nibble-decoding is a classic bug class.
• **Leaf vs extension vs branch disambiguation**: node type encoded in first byte of value; must be checked before use

Tag: `[MPT:{defect}]`

2b. IAVL+ and ICS-23 (Cosmos)

• **Subkey handling**: an ICS-23 `NonExistenceProof` needs the left+right neighbors. **Dragonberry root cause**: the check did not forbid the subkey from being a prefix of a real key, allowing forgery.
• **Left/right monotonicity**: in a non-existence proof, left key < query < right key must be strictly enforced
• **Leaf-op vs inner-op ordering**: ICS-23 specs the op order; a decoder that accepts reordered ops is vulnerable
• **Root hash binding**: the proof root must match the block's state root, not just any known root

Tag: `[ICS23:{defect}]`

**Known exemplar**: Cosmos SDK Dragonberry (Oct 2022) — [Verichains writeup](https://blog.verichains.io/p/vsa-2022-103-cosmos-sdk-forging-membership). Subkey suffix forgery allowed forged membership proofs. Patched in Cosmos SDK 0.45.9 / 0.46.3.

2c. Sparse Merkle Tree

• **Default hash**: empty leaves hash to a specific value. Is this enforced? Can an attacker supply a different "empty" value?
• **Bit-walk correctness**: key bits index into left/right children. Off-by-one at the last bit is a known bug class.

2d. SSZ / Generalized indices

• **GIndex arithmetic**: the generalized index encodes tree position. Incorrect arithmetic accepts proofs for the wrong leaf.
• **Multi-proof batch**: verify each leaf independently does not skip any intermediate node

2f. Binary Merkle path primitives (`validate_path`, `validate_chunk`)

For custom Merkle helpers, do not stop at "hashes are recomputed." Build a field-by-field proof-soundness table:

| Check | Required invariant | Evidence | |---|---|---| | Leaf binding | The supplied leaf/value hash is compared to the target leaf, not only folded into a path | | | Target offset | `target_offset` / index selects the left-right walk and is range-checked | | | Proof length | number of siblings equals expected tree depth, or the verifier rejects | | | Operator correctness | all acceptance conditions use the intended boolean connective (`&&` vs `||`) | | | Root binding | final computed root equals the trusted root for the same block/header/context | | | Empty/singleton tree | zero-node and one-node cases are explicitly defined | |

Mandatory procedure:

1. Locate every `validate_path`, `verify_path`, `validate_chunk`, `verify_chunk`, `calculate_root`, and `hash_leaf` function. 2. For each verifier, write the exact predicate that returns `true`. 3. Try these adversarial proofs: wrong leaf with valid sibling path, correct leaf with too-short proof, proof for adjacent `target_offset`, empty proof, and a proof where only one side of a compound condition holds. 4. If the verifier accepts any case where the leaf, path length, offset, or root is not bound, emit a finding even if another caller performs a partial check. The primitive itself is load-bearing.

Tag: `[MERKLE-PATH:{leaf|length|offset|operator|root}]`

3. Root Binding

The proof is only as good as the root it verifies against.

1. Where does the verified root come from? Block header? Light-client state? Trusted setup? 2. Is the root **freshness** bounded? A stale root can be used to verify a stale state; a recent root cannot prove historical state 3. For cross-chain proofs: the root is provided by a validator signature (Tendermint) or a fraud-proof challenge (optimistic rollup). What's the trust model? 4. **Replay**: can the same proof be replayed against a different root to deceive a different chain?

Tag: `[ROOT-BIND:{source}:{freshness-bo