Prove StackSignature::compose associativity in Rocq

[avrabe]

Overview

Formally prove in Rocq that StackSignature::compose is associative.

Property

(a.compose(b)).compose(c) == a.compose(b.compose(c))

Implementation

1. Translate StackSignature struct to Rocq
2. Translate compose function to Rocq
3. Write and prove associativity theorem

Depends on

• Add Rocq formal verification support using rules_rocq_rust #45 (Rocq foundation)

Files

• loom-core/src/stack.rs
• proofs/stack/compose_assoc.v (new)