Report contract for consumers: 0.4.0 frozen, verdict matrix as data, corroboration keys — and the estate's Creusot lane

.github/workflows/creusot-gate.yml

@@ -0,0 +1,96 @@
+# SPDX-License-Identifier: MPL-2.0
+name: Creusot Gate
+
+# Rust deductive verification, as the estate requires it: the Creusot gate in
+# hyperpolymath/cicd-suite, called rather than copied. This file adds no
+# steps of its own, exactly like main-estate-audit.yml — a copy would freeze
+# this repository at whatever cicd-suite commit it happened to hold.
+#
+# Why this file exists at all: the estate audit's own `languages` job runs the
+# Idris2, Zig, proof-runner and BoJ checks, not this one, so before this file
+# nothing in this repository watched for a Creusot claim. The gate's checks are
+# therefore new coverage here, not a duplicate of the audit's.
+#
+# KNOWN LIMIT OF THE PINNED GATE (reviewed, upstream fix required): the pinned
+# script recognises a Creusot dependency by its literal `creusot-std` /
+# `creusot-contracts` key. A crate that renames the dependency
+# (`creusot = { package = "creusot-std" }`) and writes contracts would set
+# `obligations=true` while leaving the selected-crate list empty, so the proof
+# loop could run over nothing and still exit green. That is a gap in the gate,
+# not a pass for this tree, and it cannot be fixed from here without copying
+# the gate (which is what this repository refuses to do). It is recorded so the
+# first aliased dependency arrives with someone looking; the honest fix is a
+# cicd-suite release that resolves the alias and rejects an empty crate list
+# when obligations exist.
+#
+# WHAT THIS GATE DOES, AND WHAT IT DOES NOT CLAIM
+# -----------------------------------------------
+# Three phases, run by the reusable:
+#
+#   detect   does any crate carry a Creusot obligation (a creusot-std /
+#            creusot-contracts dependency, or a #[requires]/#[ensures] and
+#            friends)? does any prose or source header CLAIM Creusot
+#            verification?
+#   theatre  T1: a claim with no obligations behind it is a hard failure —
+#            "verified with Creusot" without contracts is proof theatre.
+#            T2: a creusot-std dependency that annotates nothing is named.
+#            T3: every #[trusted] axiom is listed, because a proof is only as
+#            strong as the set it trusts.
+#   prove    only runs when detect found obligations. It installs Creusot at
+#            a pinned release, proves a planted FALSE contract and REQUIRES
+#            the prover to refuse it, proves a planted TRUE one and requires
+#            success, and only then runs `cargo creusot prove` in every crate
+#            with obligations. A prover that cannot say no is not a prover.
+#
+# MEASURED ON THIS TREE (2026-10-28, cicd-suite bf7dd95 creusot-check):
+#   obligations=false  claims=false  contract_count=0  trusted_count=0
+# so the theatre phase reports, in its own words, "no Creusot obligations and
+# no verification claims in this tree. Nothing was proved and nothing claims
+# to be — this gate is silent, not green-as-assurance."
+#
+# That is the honest state, and it is the state PROOF-PROGRESS.adoc records:
+# Pons has no machine-checked soundness proof. The gate exists here so that
+# the first time anyone claims, in a README, a module header or a doc, that
+# this code has been proved by Creusot — with no contracts behind it — the
+# build goes red (T1) instead of the claim shipping. (The gate reads that
+# claim phrase out of prose lines, so even quoting it here would be a mistake
+# if workflows were scanned; this comment deliberately paraphrases.) It is a guard against theatre today and the
+# wiring for real obligations tomorrow: the day a crate depends on
+# creusot-std, detect flips obligations to true, prove runs, and the tree has
+# to discharge its contracts or fail.
+#
+# A first obligation therefore needs, together: a creusot-std dependency, the
+# nightly pin Creusot is built against (the reusable's `rust_nightly` input),
+# and a crate whose contracts `cargo creusot prove` actually discharges. There
+# is no way to have the third without the toolchain, and no honest way to
+# claim it before it runs.
+#
+# Pin: the same cicd-suite commit main-estate-audit.yml uses (bf7dd95), so the
+# audit's `languages` component and this job run the same gate revision.
+# DE-ONBOARDED from actions.lock deliberately, like the secret-scanner and
+# estate-audit callers: a reusable onboarded cross-repo startup-fails with zero
+# jobs under sha_pinning_required. Do not run a full-directory `gh actions-lock`
+# that re-onboards this file.
+
+on:
+  push:
+    branches: [main]
+  pull_request:
+    branches: [main]
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+permissions:
+  contents: read
+
+jobs:
+  creusot:
+    uses: hyperpolymath/cicd-suite/.github/workflows/creusot-gate.yml@bf7dd95cf49733019343ff485c2f45c6b261839c # cicd-suite main
+    # A creusot-std dependency that annotates nothing is a hollow dependency:
+    # this repository adds one only when it also writes the contract, so the
+    # warning is escalated to a failure. It costs nothing today — there is no
+    # such dependency — and it means the first one cannot arrive alone.
+    with:
+      enforce_hollow: true

ARCHITECTURE.adoc

@@ -95,8 +95,9 @@ Components marked *planned* carry the milestone that delivers them; see
 * Inline comment allowances; strings cannot suppress findings
 * Suppressed findings are counted rather than silently erased
 . *Reporter* — *built*
-* Human-readable output with SPECULATIVE visually demoted
-* JSON 0.3.0 envelope with skip, transcode and suppression accounting
+* Human-readable output with SPECULATIVE visually *and* numerically demoted
+* JSON 0.5.0 envelope (0.4.0 frozen and still validatable) with skip, transcode,
+  suppression, demoted-count and corroboration-key accounting
 * SARIF 2.1.0 with invocation notifications and honest artifact offsets
 * Generated catalogue and man page from the live registry/CLI model
 

CHANGELOG.adoc

@@ -3,6 +3,76 @@
 
 == Unreleased — 0.1.0-dev.1
 
+=== Added
+
+* The three things a repinning consumer needs are now published, and each one is
+  a fact the code checks rather than a promise the docs make.
+
+  **The report contract is versioned, and 0.4.0 is frozen.** The envelope moves
+  to 0.5.0 with three appended keys: `findings[].semantic_fingerprint`,
+  `counts.actionable` and `counts.demoted_speculative`. Additive in both
+  directions, and the bump is still taken, because a consumer has to be able to
+  tell whether a report carries the corroboration key at all. `0.4.0` does not
+  disappear: `schemas/scan-0.4.0.json` is byte-pinned by
+  `FROZEN_0_4_0_SCHEMA_BLAKE3` (a test recomputes the digest, so editing the
+  frozen file fails the build instead of a consumer), and `pons
+  validate-report` still accepts a 0.4.0 report — the version *declared inside
+  the document* selects the schema, so a 0.4.0 declaration cannot carry a 0.5.0
+  key. `schemas/index.json` lists every published artifact with its version,
+  status and BLAKE3 digest, and `schemas/README.adoc` states the freeze rule and
+  how to add a version.
+
+  **The severity × evidence matrix is published as data.**
+  `schemas/verdict-matrix-1.0.0.json` carries all twelve (severity, evidence)
+  cells with `sarif_level`, `aggregate_weight`, `counts_toward_verdict`,
+  `gate_eligible`, `count_bucket` and `demotion_suffix`, plus both scales and the
+  corroboration recipe. It is generated from `crates/pons-core/src/verdict.rs`,
+  which is now the single home of the SARIF level and rank tables, the
+  evidence-contract confidence labels and the `--fail-on` rank, so the published
+  document cannot state a different number from the reporter; a drift test fails
+  if the committed file and the code disagree.
+
+  **Every finding carries a semantic fingerprint.**
+  `findings[].semantic_fingerprint` is BLAKE3 over
+  `pons-corroboration-v1`, the root-relative path, the 1-based start line and
+  the evidence class — a *site*, not a finding, so a grid can mark Pons's
+  finding and a panic-attack or Hypatia finding at the same line as one
+  corroborated site instead of double-counting the overlap. It deliberately
+  ignores the rule id, the producer and the severity. The record fingerprint is
+  unchanged and still does the other job (one finding, rule id plus a
+  whitespace-folded anchor). `validate-report` recomputes the key rather than
+  checking its shape, so a producer cannot point a finding at an arbitrary site.
+
+  **`SPECULATIVE` is demoted numerically as well as visually.** The demoted
+  bucket has an aggregate weight of **zero** at every severity, `counts.actionable`
+  excludes it, and `validate-report` rejects a document whose
+  `actionable + demoted_speculative` does not account for `counts.total` — the
+  demotion is a number in the contract, not a convention a reader might miss.
+  The human summary gains a `verdict:` line separating the two. Appendix E's
+  SARIF `rank` of 20 is kept, on purpose and published as a *different* number:
+  a guess stays visible and adds nothing.
+
+* Tests for all of it, including the ones that make the claims non-vacuous: a
+  frozen 0.4.0 report still validates through the binary, a 0.4.0 declaration
+  carrying a 0.5.0 key is rejected, an unknown version is refused rather than
+  validated against the nearest shape, a forged corroboration key is rejected,
+  and the frozen schema digest is recomputed from disk.
+
+=== Added (verification lane)
+
+* The estate's Creusot gate is now called by this repository
+  (`.github/workflows/creusot-gate.yml`) at the same cicd-suite pin as the
+  estate audit, instead of only arriving inside the audit's `languages`
+  component. Nothing is proved by this and nothing claims to be: measured with
+  the gate's own `detect` and `theatre` phases on this tree, `obligations=false
+  claims=false contract_count=0 trusted_count=0`, and the gate's verdict is its
+  own words — "nothing was proved and nothing claims to be". What the lane buys
+  is the negative: a claim that this code is proved, with no contracts behind
+  it, is now a build failure (T1), a `creusot-std` dependency that annotates nothing
+  is a failure here because `enforce_hollow` is set (T2), and every `#[trusted]`
+  axiom must be listed (T3). `PROOF-PROGRESS.adoc` records the state and what a
+  first real obligation requires.
+
 === Fixed
 
 * The shared secret scanner's owner spelling is now recorded where it is

PROOF-PROGRESS.adoc

@@ -15,6 +15,35 @@ conformance, not source-derived typestate or a proof of all executions. See
 link:docs/PURPOSE-AND-PROOF.adoc[purpose, comparison, proof status and opportunities]
 for the operator-facing distinction and bounded next steps.
 
+== The Rust deductive-verification lane (Creusot)
+
+This repository now calls the estate's Creusot gate as its own check
+(`.github/workflows/creusot-gate.yml`), at the same cicd-suite pin the estate
+audit uses. Before this, the gate was not run here at all: the pinned estate
+audit's `languages` job runs the Idris2, Zig, proof-runner and BoJ checks, not
+the Creusot one, so nothing was watching for a Creusot claim in this tree.
+
+Measured on this tree with the gate's own `detect` and `theatre` phases
+(2026-10-28): `obligations=false claims=false contract_count=0
+trusted_count=0`. The gate's verdict is therefore, in its own words, *"no
+Creusot obligations and no verification claims in this tree. Nothing was proved
+and nothing claims to be — this gate is silent, not green-as-assurance."*
+
+That silence is the accurate status, not a pass: there is no `creusot-std`
+dependency, no `#[requires]`/`#[ensures]` anywhere, and no claim of Creusot
+verification in this documentation. What the lane now guarantees is the
+negative: a claim of Creusot verification with no contracts behind it (T1) is a
+build failure, a `creusot-std` dependency that annotates nothing (T2) is a
+failure here because `enforce_hollow` is set, and every `#[trusted]` axiom has
+to be listed (T3).
+
+Adding a first real obligation needs three things together — the `creusot-std`
+dependency, the nightly pin Creusot is built against, and a crate whose
+contracts `cargo creusot prove` discharges — and honesty about ordering: with
+no obligation, the `prove` phase does not run, so nothing about this tree is
+proved today. The provenance ledger keeps `Actually-Proven` unreachable
+(`proof_artifacts: []`) so that no test can claim it in the meantime.
+
 == Headline
 
 [cols="2,1,4",options="header"]

README.adoc

@@ -30,7 +30,7 @@ and link:docs/adr/0004-companion-to-panic-attack.adoc[ADR-0004].
 
 *Implementation in progress toward v0.1.0.* Milestones M0–M4 are present: the
 Rust workspace, scanning engine, six native tree-sitter grammars including PHP,
-JSON 0.4.0/SARIF reporters, Python CFG/dataflow and a bounded PHP context-flow
+JSON 0.5.0 (0.4.0 frozen)/SARIF reporters, Python CFG/dataflow and a bounded PHP context-flow
 slice. Thirteen source rules are registered (ten T0, three T1).
 `pons scan <PATH>`, `pons catalogue`, `pons man`, `pons doctor`, `pons trace`,
 `pons wharf-trace` and `pons validate-report` exist;

ci/json-ratchet.kyaml

@@ -25,6 +25,7 @@
     },
     {
       paths: [
+        "crates/pons-core/tests/golden/report-0.4.0.json",
         "crates/pons-core/tests/golden/report.json",
         "crates/pons-core/tests/golden/report.sarif.json",
       ],
@@ -144,9 +145,12 @@
     {
       paths: [
         "schemas/evidence-1.0.0.json",
+        "schemas/index.json",
         "schemas/scan-0.4.0.json",
+        "schemas/scan-0.5.0.json",
+        "schemas/verdict-matrix-1.0.0.json",
       ],
-      reason: "The published report schemas. They are the human-readable contract for Pons's machine-readable output and are reviewed line by line; a canonical rendering of a 755-line schema is not reviewable.",
+      reason: "The published contract artifacts: the report schemas, the frozen 0.4.0 schema, the version index that attests each of them by BLAKE3, and the severity x evidence matrix. They are the human-readable contract for Pons's machine-readable output and are reviewed line by line; a canonical rendering of a 755-line schema is not reviewable, and canonicalising a document whose field order is part of its published guarantee would change the contract rather than enforce it.",
     },
   ],
 }

ci/yaml-ratchet.kyaml

@@ -28,6 +28,7 @@
     {
       paths: [
         ".github/workflows/codeql.yml",
+        ".github/workflows/creusot-gate.yml",
         ".github/workflows/deed-conformance.yml",
         ".github/workflows/format-policy.yml",
         ".github/workflows/k9-conformance.yml",

crates/pons-cli/src/main.rs

@@ -93,11 +93,11 @@ enum FailOn {
 }
 
 impl FailOn {
-    fn rank(self) -> u8 {
+    fn severity(self) -> Severity {
         match self {
-            FailOn::Info => 0,
-            FailOn::Warn => 1,
-            FailOn::Error => 2,
+            FailOn::Info => Severity::Info,
+            FailOn::Warn => Severity::Warn,
+            FailOn::Error => Severity::Error,
         }
     }
 }
@@ -126,14 +126,6 @@ impl Language {
     }
 }
 
-fn severity_rank(s: Severity) -> u8 {
-    match s {
-        Severity::Info => 0,
-        Severity::Warn => 1,
-        Severity::Error => 2,
-    }
-}
-
 /// Run the CLI, treating a propagated broken pipe as success and other
 /// operational errors as exit status 2.
 fn main() -> ExitCode {
@@ -312,8 +304,11 @@ fn doctor() -> String {
 /// `no_speculative` removes speculative findings and counts them as suppressed;
 /// `explain` adds evidence and tier annotations only in human output.
 ///
-/// Returns 2 if `fail_on_skips` is set and any input was skipped, otherwise 1
-/// if a remaining non-speculative finding meets `fail_on`, or 0.
+/// Each entry in `required_languages` must have at least one inventory entry,
+/// with every matching entry analysed completely.
+/// Returns 2 if no files were analysed, a coverage requirement failed, or
+/// `fail_on_skips` is set and any input was skipped; otherwise 1 if a remaining
+/// non-speculative finding meets `fail_on`, or 0.
 ///
 /// Missing paths, a forced grammar for a directory, unknown selected rules,
 /// configuration and discovery errors, and rendering or stdout errors propagate.
@@ -450,8 +445,12 @@ fn run_scan(
         || (fail_on_skips && !report.skipped.is_empty());
     let finding_threshold = fail_on.is_some_and(|threshold| {
         report.findings.iter().any(|f| {
-            f.evidence() != EvidenceClass::Speculative
-                && severity_rank(f.severity()) >= threshold.rank()
+            pons_core::verdict::counts_toward_verdict(f.evidence())
+                // One rank table, shared with the published verdict matrix
+                // (schemas/verdict-matrix-1.0.0.json), so a consumer reading
+                // the data and the binary get the same gate.
+                && pons_core::verdict::fail_on_rank(f.severity())
+                    >= pons_core::verdict::fail_on_rank(threshold.severity())
         })
     });
     report.exit_code = Some(if coverage_failed {