feat(echidna-core-spark): add Creusot-annotated pareto module (M3)

Mirrors src/rust/verification/pareto.rs as a parallel verification
artefact in the SPARK kernel crate, executing milestone M3 of
docs/design/SPARK_ADOPTION_PLAN.md.

- pareto.rs: ProofObjective, ProofCandidate, dominates(), compute().
  Identical algorithm to verification/pareto.rs; identical test suite
  plus 14 new property tests in `impl_invariants` mod (PO-P1..PO-P8d)
  matching the corresponding Lean4 theorems in ParetoMaximality.lean.

- lib.rs: register the new pub mod pareto; document in module table.

Build: cargo build -p echidna-core-spark — clean, no warnings.
Tests: cargo test -p echidna-core-spark — 48 passed, 0 failed
       (14 of those are the new pareto invariants).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

crates/echidna-core-spark/src/lib.rs

@@ -47,8 +47,10 @@
 //! |---|---|---|
 //! | (this file) | `confidence.rs` | `TrustLevel` total order, combine monotonicity |
 //! | [`axiom_tracker`] | `axiom_tracker.rs` | `DangerLevel` order, classify monotonicity |
+//! | [`pareto`] | `verification/pareto.rs` | Dominance irreflexivity / antisymmetry / transitivity, frontier soundness + completeness, best-axis preservation (E10) |
 
 pub mod axiom_tracker;
+pub mod pareto;
 
 // ---------------------------------------------------------------------------
 // Creusot prelude — only imported when verifying