fix: preserve @ in workflow filenames and record qualified proof receipt

.github/workflows/creusot.yml

@@ -9,10 +9,10 @@
 # can say no, proves a planted TRUE one, and only then runs
 # `cargo creusot prove` in every crate that carries contracts.
 #
-# What it covers here: verification/squabble-creusot. Obligations are
-# **stated, not discharged** — no run has reached Why3 yet (see
-# docs/CREUSOT.adoc). A green on this check means the obligations were
-# discharged on that run, not that they were ever stated before.
+# What it covers here: verification/squabble-creusot. Hosted run 41909189438
+# discharged its obligations at merge checkout f9499a8de0b8c525459a669e2cdbcacf83a49b85
+# after rejecting the false control and proving the true one (docs/CREUSOT.adoc).
+# Each later source still needs its own proof run; this is not a whole-engine proof.
 #
 # Full-SHA pin, DE-ONBOARDED from actions.lock — same rule as rust-ci.yml: the
 # gate scripts are pinned by the caller's own `uses:` SHA, so this line is the

.github/workflows/standards-pipeline.yml

@@ -33,7 +33,7 @@ permissions:
 
 jobs:
   pipeline:
-    # metadatastician/standards @ 8e48b1ca (standards main 2026-10-25; see actions.lock).
+    # metadatastician/standards @ a797d308c0517d4e2d21cc7f1cb08d41f82b1a12 (see actions.lock).
     #
     # NO `secrets:` block, deliberately. ci-pipeline.yml declares
     # `workflow_call.inputs` only, has no `secrets:` block and references no

README.adoc

@@ -217,12 +217,21 @@ just verify-mirror    # stable Rust: the model vs the real engine
 just verify-creusot   # the prover: discharge the obligations
 ----
 
-**Stated, not proved.** No obligation has been discharged, and this repository's
-own `Rust CI` currently ends as a zero-job `startup_failure`, so CI has not
-compiled the workspace either. `.github/workflows/creusot.yml` calls the estate's
-`creusot-gate.yml`, which fails a claim of proof with no contracts behind it and
-reports *no proof performed* rather than a verdict when the prover cannot be
-shown to work. Details and the licence note: `docs/CREUSOT.adoc`.
+**Hosted proof recorded for an exact source revision.** On 2026-11-04,
+https://github.com/hyperpolymath/cicd-squabbler/actions/runs/41909189438/job/126852164109[job 126852164109]
+rejected the planted false contract, proved the true control, then discharged
+the obligations in `verification/squabble-creusot` at merge checkout
+`f9499a8de0b8c525459a669e2cdbcacf83a49b85`. `Proved (13 files)` is the
+prover's file-level result, not a theorem count. The gate's zero trusted-axiom
+field counts only tracked Rust lines containing the literal `#[trusted]`;
+it does not count axioms from dependencies or the prover. That checkout combines
+PR head
+`1fd9db9bb94d9ac8ed54f7a6ef4f8c51ff35a848` with base
+`17284299184fd31a10c7bf382f02262cd0ab308c`. This receipt covers the separate
+contract crate at that revision; later revisions and the operational engine
+need their own validation. The gate still reports *no proof performed* when
+it cannot establish a working prover. Scope, historical environment failures
+and the licence note: `docs/CREUSOT.adoc`.
 
 == Downstream integration contracts (pinned, immutable revisions)
 
@@ -280,7 +289,7 @@ check away, or any override are provably *not* paths to green.
 | `crates/squabble-app`  | The loopback HTTP backend (axum, `127.0.0.1:7741`): serves the shared planner to the boj-server `cicd-squabbler-mcp` cartridge. The GitHub App *webhook* leg (trigger button + octocrab) is still to come — no webhook route is registered.
 | `crates/squabble-forge`| Forge access: GitHub GraphQL via `gh api graphql`, batched, validated against a committed schema snapshot. REST where GraphQL has no equivalent — notably `repos/{o}/{n}` for canonical `full_name` resolution (redirects followed, names compared).
 | `spark/`               | The formal heart. `Gate_Machine` + the proved theorem `green ⇔ (non-empty ∧ all passed)`.
-| `verification/squabble-creusot` | The Rust twin of `spark/`: Creusot contracts for the same invariants, plus a stable-Rust mirror that fails if the engine drifts from them. **Stated, not proved** — no obligation has been discharged yet. See `docs/CREUSOT.adoc`.
+| `verification/squabble-creusot` | Creusot contracts for the scalar invariants, plus a stable-Rust mirror that tests for drift from the engine. A hosted proof discharged the contract crate at merge checkout `f9499a8…` on 2026-11-04; this does not certify later source or the whole engine. Exact receipt and scope: `docs/CREUSOT.adoc`.
 |===
 
 == Verify it yourself

crates/squabble-cli/src/chains.rs

@@ -667,6 +667,42 @@ mod tests {
             .any(|f| f.severity() == Severity::Blocking));
     }
 
+    #[test]
+    fn moved_details_label_only_unconfirmed_consumers() {
+        use squabble_core::chains::{Edge, EdgeKind, Pin};
+
+        let edge = |from: &str, file: &str, pin: &str| Edge {
+            from: RepoId::new(from),
+            file: file.into(),
+            to: RepoId::new("old/tool"),
+            kind: EdgeKind::Action,
+            path: None,
+            pin: Pin::parse(pin),
+            version_hint: None,
+        };
+        let finding = Finding::MovedUpstream {
+            written: RepoId::new("old/tool"),
+            canonical: RepoId::new("new/tool"),
+            consumers: vec![edge(
+                "me/app",
+                "ci.yml",
+                "1111111111111111111111111111111111111111",
+            )],
+            unconfirmed_consumers: vec![edge(
+                "me/shared",
+                "build.yml",
+                "2222222222222222222222222222222222222222",
+            )],
+        };
+        assert_eq!(
+            details(&finding),
+            [
+                "me/app:ci.yml @111111111111",
+                "me/shared:build.yml @222222222222 (upstream revision unconfirmed)",
+            ]
+        );
+    }
+
     #[test]
     fn a_dead_upstream_is_found_by_rest_even_without_follow() {
         let r = collect(