Rocq proofs for CopyLayout and recursive pointer fixup adapters

[avrabe]

Context

The v0.2.0 list adapter implementation introduced:

• CopyLayout enum in resolver.rs — distinguishes Bulk { byte_multiplier } from Elements { element_size, inner_pointers }
• emit_inner_pointer_fixup() in adapter/fact.rs — generates wasm loops for recursive inner pointer fixup
• Canonical ABI sizing methods in parser.rs — canonical_abi_align, canonical_abi_size_unpadded, canonical_abi_element_size

These are correctness-critical code paths that would benefit from formal verification.

Proof targets

• canonical_abi_element_size matches the Component Model spec's elem_size definition
• CopyLayout construction is consistent with type structure (every pointer pair gets a layout)
• byte_multiplier correctly computes total byte size from element count
• Recursive fixup loop terminates (bounded by type nesting depth)
• Inner pointer offsets within elements are correctly computed with alignment

Files

• meld-core/src/parser.rs — ABI sizing functions
• meld-core/src/resolver.rs — CopyLayout enum and construction
• meld-core/src/adapter/fact.rs — emit_inner_pointer_fixup
• Proofs would go in proofs/adapter/ and proofs/parser/