Add hard-gated Creusot verification for proof-critical Rust kernels

[hyperpolymath]

Estate-policy gap

Ephapax is implemented substantially in Rust, but the repository currently has no Creusot integration, contracts, setup documentation, or hard verification workflow. A bounded audit of the checkout found no creusot/crueset material. Estate-wide GitHub code search found the established hard-gated Creusot pattern in hyperpolymath/echidna, not in Ephapax.

Existing Coq bridge round-trip tests, property tests, type-system tests, and typed-Wasm verification seams are valuable, but they do not establish that Creusot proof obligations have been generated and discharged.

Required outcome

• Identify the proof-critical Rust kernel(s) and state their safety/correctness contracts.
• Add Creusot-compatible contracts and loop/data invariants to those kernels.
• Pin a compatible Rust nightly, Creusot version, Why3 version, and solver set.
• Provide reproducible local setup and verification documentation.
• Add a CI job that fails on invalid, unknown, timed-out, or undisposed obligations; do not use continue-on-error.
• Include a deliberately broken contract/implementation positive control while commissioning the gate, proving that CI can fail for a false obligation.
• Define how Creusot obligations relate to Ephapax's existing Coq, ownership-carrier, typed-Wasm, and test evidence without claiming that one automatically proves another.
• Record the exact proved boundary and explicitly list unproved compiler phases.

Completion language

Keep these states distinct in documentation and reviews: contracts written, tool configured, workflow wired, obligations generated, obligations discharged, and proof boundary published. None implies the next.

This issue records the Rust/Creusot estate-policy requirement; it is not satisfied by adding an empty workflow or proof scaffold.