feat(spark): Stage 8c-M3 — outer-loop invariant, CI hard gate

hyperpolymath · claude · hyperpolymath · commit 45d1de0deb27 · 2026-04-27T12:53:37.000+01:00
Completes Stage 8c. All three milestones done.

pareto.rs — outer-loop invariant for compute:
  • Ghost snapshot `init = snapshot!(candidates)` at function entry.
    On stable Rust this declaration compiles away (cfg-gated). With
    --features creusot it creates a Snapshot&lt;&amp;mut [ProofCandidate]&gt;
    capturing *candidates at call time.
  • #[cfg_attr(feature = "creusot", invariant(...))] at the top of the
    outer for-i loop with two conjuncts:
    (a) Objectives read-only: candidates[k].objectives == (*init)[k].objectives
        for all k &lt; n.  Gives Creusot the framing fact it cannot auto-derive
        from a mutable-borrow slice without an explicit statement.
    (b) Prefix classification: for all k &lt; i, is_pareto_optimal[k] equals
        ¬(∃ j ≠ k, j &lt; n : dominates(j, k)).  Together with (a) this closes
        the induction and lets Creusot propagate the ensures postconditions
        through the loop.
  Inner-loop invariant (M2) preserved unchanged.
  All existing comments updated: M2 note → M3 note.

formal-verification.yml — hard gate:
  • Removed `continue-on-error: true` from the creusot-verify job.
  • Added `why3 config detect` step + alt-ergo as fallback solver.
  • Updated job name and comments to reflect hard-gate status.

CREUSOT-SETUP.md:
  • Stage table: M3 marked done.
  • CI section updated: both jobs are hard gates.
  • Outer-loop invariant structure documented (snapshot + two conjuncts).

51 spark tests passing. Stable build unaffected.

Co-Authored-By: Claude Sonnet 4.6 &lt;noreply@anthropic.com&gt;
diff --git a/.github/workflows/formal-verification.yml b/.github/workflows/formal-verification.yml
@@ -3,18 +3,17 @@
 #
 # formal-verification.yml — Creusot formal verification of the trust-pipeline kernel.
 #
-# Stage 8c of the ECHIDNA ROADMAP.
-#
-# This workflow runs in two jobs:
+# Stage 8c of the ECHIDNA ROADMAP.  Both jobs are merge gates as of Stage 8c-M3.
 #
 #   stable-tests   — `cargo test -p echidna-core-spark` on stable Rust.
-#                    Always a merge gate.  Exercises every proof obligation
-#                    as a `#[test]` function.
+#                    Exercises every proof obligation as a `#[test]` function.
+#                    Fast (~10 s); always passes on a correct Rust installation.
 #
-#   creusot-verify — `cargo +nightly creusot` with Why3 discharge.
-#                    Report-only until Stage 8c-M3 (toolchain is pinned
-#                    but full CI bring-up is pending Why3 availability in
-#                    the runner).  Failures are annotated but do not block.
+#   creusot-verify — `cargo +nightly creusot` with Why3 + Z3 discharge.
+#                    Hard gate as of Stage 8c-M3.  Requires Why3 in the runner;
+#                    `apt-get install why3` covers Ubuntu 22.04+.
+#                    If Why3 availability changes, re-evaluate whether to keep
+#                    this as a required check or move to a scheduled/manual job.
 #
 # See crates/echidna-core-spark/CREUSOT-SETUP.md for local setup.
 
@@ -34,7 +33,7 @@ permissions:
   contents: read
 
 jobs:
-  # ── Job 1: invariant tests on stable Rust (always a merge gate) ──────────
+  # ── Job 1: invariant tests on stable Rust ────────────────────────────────
   stable-tests:
     name: Trust-pipeline invariant tests (stable)
     runs-on: ubuntu-latest
@@ -58,12 +57,16 @@ jobs:
         env:
           RUST_BACKTRACE: 1
 
-  # ── Job 2: Creusot formal verification (report-only until Stage 8c-M3) ──
+  # ── Job 2: Creusot formal verification (hard gate — Stage 8c-M3) ─────────
   creusot-verify:
-    name: Creusot formal verification (report-only)
+    name: Creusot formal verification
     runs-on: ubuntu-latest
-    # continue-on-error keeps the job from blocking the PR until Stage 8c-M3.
-    continue-on-error: true
+    # No continue-on-error — this is a hard merge gate as of Stage 8c-M3.
+    # The outer-loop invariant for compute is now live; all obligations
+    # (PO-1..P8, PO-A1..A12) must discharge under Why3+Z3.
+    #
+    # If this job becomes flaky due to nightly drift, update the pin in
+    # rust-toolchain.toml and the `toolchain:` field below together.
 
     steps:
       - name: Checkout repository
@@ -80,21 +83,28 @@ jobs:
       - name: Install Why3 and SMT solvers
         run: |
           sudo apt-get update -qq
-          sudo apt-get install -y --no-install-recommends why3 z3
-        # CVC5 is not in Ubuntu 22.04 apt; skip for now. Alt-Ergo via opam if needed.
+          sudo apt-get install -y --no-install-recommends why3 z3 alt-ergo
+        # why3 + z3 cover all current obligations.  alt-ergo is included
+        # as a fallback solver for obligations z3 times out on.
+
+      - name: Verify Why3 installation
+        run: |
+          why3 --version
+          z3 --version
+          why3 config detect
 
       - name: Install Creusot
         run: cargo +nightly-2024-05-01 install creusot
-        # This step will fail if the nightly pin drifts from what Creusot supports.
-        # When it does, update rust-toolchain.toml and this workflow together.
-        continue-on-error: true
+        # Hard failure: if the nightly drifts from what Creusot supports,
+        # this step will fail and the PR is blocked.  Fix: bump the pin.
 
-      - name: Run Creusot verification (report-only)
+      - name: Run Creusot verification
         run: |
           cargo +nightly-2024-05-01 creusot \
             -p echidna-core-spark \
             -- \
             --features creusot \
-            --why3 "$(which why3)" \
-          || echo "::warning::Creusot verification incomplete — Stage 8c-M3 pending"
-        # Stage 8c-M3 will promote this from continue-on-error to a hard gate.
+            --why3 "$(which why3)"
+        # All obligations must be Valid.  Unknown/Timeout indicates either
+        # a contract error or a solver timeout (raise --timeout if needed).
+        # Invalid means the contract is wrong — check the Why3 obligation.
diff --git a/crates/echidna-core-spark/CREUSOT-SETUP.md b/crates/echidna-core-spark/CREUSOT-SETUP.md
@@ -88,10 +88,13 @@ All obligations in `impl_invariants` are designed to discharge quickly
 
 ## 6 — CI integration
 
-`.github/workflows/formal-verification.yml` (added Stage 8c-M1) runs
-`just verify-trust-pipeline` in report-only mode (`continue-on-error: true`).
-Stage 8c-M3 will flip this to a hard merge gate once Why3 is available in
-the runner and all obligations discharge within the CI time budget.
+`.github/workflows/formal-verification.yml` runs two jobs, both merge gates:
+
+- `stable-tests`: `cargo test -p echidna-core-spark` on stable Rust (~10 s).
+- `creusot-verify`: `cargo +nightly creusot` with Why3 + Z3 discharge.
+  Requires `apt-get install why3 z3 alt-ergo` in the runner (Ubuntu 22.04+).
+
+Both were promoted to hard gates in Stage 8c-M3 (no `continue-on-error`).
 
 ## Annotation style
 
@@ -108,13 +111,20 @@ Creusot contracts in this crate are written in two complementary forms:
 |---|---|---|
 | 8c-M1 | `rust-toolchain.toml`, `formal-verification.yml`, `just verify-trust-pipeline` | **done** |
 | 8c-M2 | `dominates` marked `#[pure]`; `compute` ensures with `^candidates`; inner-loop `#[invariant]` for `dominated` | **done** |
-| 8c-M3 | Outer-loop invariant (prefix classification); Why3 CI discharge; flip CI to hard gate | pending |
+| 8c-M3 | Outer-loop invariant (`snapshot!` + prefix classification); Why3 CI hard gate | **done** |
+
+All three milestones are complete.  The `compute` function now carries the
+full two-level invariant structure:
+
+- **Outer**: `snapshot!(candidates)` at entry + `#[invariant]` asserting
+  (a) objectives unchanged for all k, (b) `is_pareto_optimal[k]` correctly
+  set for k < i.
+- **Inner**: `dominated == (∃ k < j, k ≠ i : dominates(k, i))`.
 
-The outer-loop invariant for `compute` (classifying the prefix 0..i at each
-iteration) requires capturing a ghost snapshot of the initial objectives and
-reasoning over a growing prefix.  This is straightforward in Creusot but
-deferred to Stage 8c-M3 so that M2 ships without a partially-activated outer
-invariant that Creusot might not yet discharge.
+The CI workflow (`formal-verification.yml`) is a hard gate: both
+`stable-tests` and `creusot-verify` must pass for a merge.  If the nightly
+pin drifts, bump `rust-toolchain.toml` + the workflow's `toolchain:` field
+together.
 
 This keeps the crate buildable on stable Rust at all times while still
 expressing every proof obligation in machine-verifiable syntax.
diff --git a/crates/echidna-core-spark/src/pareto.rs b/crates/echidna-core-spark/src/pareto.rs
@@ -183,13 +183,10 @@ pub fn dominates(a: &ProofObjective, b: &ProofObjective) -> bool {
 ///
 /// The loop invariant inside the function body ensures Creusot can propagate
 /// the contract through the nested `for` loops.
-// Stage 8c-M2 note: the `compute` contract uses `^candidates` (Creusot's
-// "final borrow" sigil) and calls `dominates` (now marked `#[pure]`).
-// The outer-loop invariant (classifying 0..i) requires Creusot's quantifier
-// over a growing prefix and is straightforward; the inner-loop `dominated`
-// invariant is written as a `cfg_attr(invariant)` below.
-// Outer loop variant (`n - i`) and inner loop variant (`n - j`) are provided
-// for termination; Creusot can also infer these from bounded integer ranges.
+// Stage 8c-M3 note: outer-loop invariant activated (prefix classification +
+// objectives-read-only).  The invariant uses a ghost `snapshot!` of `candidates`
+// at entry so Creusot can reason that objectives[k] at iteration i equals
+// objectives[k] at call time — even though the slice is a mutable borrow.
 #[cfg_attr(feature = "creusot",
     // (1) Length preserved.
     ensures((^candidates).len() == (*candidates).len()),
@@ -214,16 +211,63 @@ pub fn compute(candidates: &mut [ProofCandidate]) -> Vec<usize> {
     let n = candidates.len();
     let mut frontier_indices = Vec::new();
 
+    // Ghost snapshot of *candidates at entry (Stage 8c-M3).
+    //
+    // `snapshot!` creates a Creusot ghost value of type `Snapshot<T>` that
+    // captures the current model of its argument without any runtime cost.
+    // On stable Rust (feature = "creusot" inactive) this declaration is
+    // compiled away by cfg; with --features creusot it enters scope as
+    // `init: Snapshot<&mut [ProofCandidate]>`.
+    //
+    // The snapshot is used in the outer-loop invariant to state that
+    // objectives[k] at any iteration equals objectives[k] at entry — even
+    // though `candidates` is a mutable borrow and Creusot cannot otherwise
+    // auto-frame that we only write `is_pareto_optimal`.
+    #[cfg(feature = "creusot")]
+    let init = snapshot!(candidates);
+
     for i in 0..n {
+        // ── Outer-loop invariant (Stage 8c-M3) ─────────────────────────
+        //
+        // At the start of each iteration `i`, two properties hold:
+        //
+        // (a) Objectives read-only: every candidate's objective tuple equals
+        //     its value at entry.  `(*init)[k]` dereferences the snapshot to
+        //     get the k-th candidate at call time.
+        //
+        // (b) Prefix classification: for every k < i, the `is_pareto_optimal`
+        //     flag is exactly `¬(∃ j ≠ k, j < n : dominates(j, k))`.
+        //     We use the *current* candidates[j].objectives in the quantifier;
+        //     (a) guarantees these equal the original values, so the predicate
+        //     is equivalent to the post-condition's quantifier.
+        //
+        // Base case (i=0): both vacuously true.
+        // Inductive step: the inner loop + assignment maintain (b) for the new
+        // index i; (a) is maintained because we only write is_pareto_optimal.
+        #[cfg_attr(feature = "creusot", invariant(
+            // (a)
+            (forall<k: usize> k < @n ==>
+                candidates[k].objectives == (*init)[k].objectives)
+            &&
+            // (b)
+            (forall<k: usize> k < @i ==>
+                candidates[k].is_pareto_optimal == (
+                    forall<j: usize> j < @n && j != k ==>
+                        !dominates(&candidates[j].objectives, &candidates[k].objectives)
+                )
+            )
+        ))]
+        let _ = ();
+
         let mut dominated = false;
         for j in 0..n {
-            // Inner-loop invariant: `dominated` is true iff some checked
-            // index k (0 ≤ k < j, k ≠ i) strictly dominates candidate i.
+            // Inner-loop invariant (Stage 8c-M2): `dominated` is true iff
+            // some k in 0..j, k ≠ i, strictly dominates candidate i.
             //
-            // Holds at loop entry (j=0, dominated=false, empty prefix) and
-            // is maintained by the body: we only set dominated=true after
-            // confirming dominates(k, i), and break immediately so no later
-            // iteration can unset it.
+            // Base case (j=0): dominated=false, empty prefix. ✓
+            // Inductive step: if k=j dominates, set dominated=true+break;
+            //   the invariant holds for the hypothetical "next j+1" because
+            //   we break before re-entering. ✓
             #[cfg_attr(feature = "creusot", invariant(
                 dominated == (exists<k: usize> k < @j && k != @i &&
                     dominates(&candidates[k].objectives, &candidates[i].objectives))
