feat(findings): every finding names its support; findings.ncl enforced in CI (HYP-01, PR B)

.claude/CLAUDE.md

@@ -13,7 +13,7 @@ Hypatia is the neurosymbolic CI/CD intelligence layer for the hyperpolymath ecos
 ## Architecture
 
 ```
-Hypatia                       # 133 Elixir modules total
+Hypatia                       # 140 Elixir modules total (`shopt -s globstar; ls lib/**/*.ex | wc -l`)
 ├── Elixir pipeline          # core: pattern analysis, dispatch, learning
 ├── Merge orchestration       # 12 modules — leases, ledger, ticker (largest subsystem)
 ├── Kin subsystem             # 6 modules — contingency, arbiter, gate, watchdog
@@ -122,6 +122,7 @@ OutcomeTracker.record_outcome()         -- Feedback loop
 | `scorecard_ingestor.ex` | Ingests 20 OpenSSF Scorecard checks as local scan patterns |
 | `learning_scheduler.ex` | GenServer: polls outcomes every 5 min, drives feedback loop |
 | `self_diagnostics.ex` | Health monitoring, circuit breaker, auto-recovery |
+| `hypatia/verdict.ex` | HYP-01: every finding names its `support`, `evidence` and a derived `level` (mirror of `Verdict.idr`; contract `schema/findings.ncl`) |
 | `application.ex` | OTP Application supervisor for all GenServers |
 
 ### VCL Query Layer (lib/vcl/)

.github/workflows/escript-soundness.yml

@@ -85,7 +85,7 @@ jobs:
       - name: Install jq
         run: |
           apt-get update -qq
-          apt-get install -y -qq jq git
+          apt-get install -y -qq jq git curl
 
       - name: Fetch source at the exact commit under test
         run: |
@@ -162,3 +162,26 @@ jobs:
             exit 1
           fi
           echo "Consumer-shaped invocation produced $(jq 'length' consumer.json) findings."
+
+      # HYP-01: every finding in CI output names its support. The schema's
+      # self-test runs first, so a schema that accepts everything cannot
+      # pass: it must refuse a pattern finding that claims "sound" (and six
+      # other bad shapes in test/fixtures/findings-schema/). Then the real
+      # consumer-shaped output above must satisfy schema/findings.ncl, whose
+      # LevelDerived contract re-derives every finding's level.
+      - name: Findings carry support, evidence and a derived level
+        working-directory: source
+        env:
+          NICKEL_VERSION: 1.11.0
+          NICKEL_SHA256: d40cd32b8374636fda8939a8e479616c7a1db57acb5ef5a9621e242ed8f5a361
+        run: |
+          set -euo pipefail
+          mkdir -p "$HOME/.local/bin"
+          curl -fsSL -o "$HOME/.local/bin/nickel" \
+            "https://github.com/tweag/nickel/releases/download/${NICKEL_VERSION}/nickel-x86_64-linux"
+          echo "${NICKEL_SHA256}  $HOME/.local/bin/nickel" | sha256sum -c -
+          chmod +x "$HOME/.local/bin/nickel"
+          export NICKEL="$HOME/.local/bin/nickel"
+          "$NICKEL" --version
+          bash scripts/check-findings-schema.sh --self-test
+          bash scripts/check-findings-schema.sh consumer.json

hypatia-cli-bash.sh

@@ -77,6 +77,14 @@ FINDINGS_FILE=""
 FINDING_COUNT=0
 FIRST_FINDING=true
 
+# The level a finding is reported at, derived from its support and evidence
+# (Hypatia.Verdict.level/2; schema/findings.ncl derive_level): sound only for a
+# mechanical re-check that confirms, epi with evidence, belief without.
+VERDICT_LEVEL_JQ='def verdict_level:
+  if .support.kind == "mechanical" and .support.result == "confirms" then "sound"
+  elif (.evidence | length) > 0 then "epi"
+  else "belief" end;'
+
 init_findings() {
     FINDINGS_FILE=$(mktemp /tmp/hypatia-findings-XXXXXX.json)
     echo "[" > "$FINDINGS_FILE"
@@ -94,12 +102,22 @@ emit_finding() {
     [[ "$FIRST_FINDING" == "false" ]] && echo "," >> "$FINDINGS_FILE"
     FIRST_FINDING=false
 
+    # HYP-01: every finding names its support (schema/findings.ncl). A regex
+    # match is `pattern` support with one evidence token; `level` is derived
+    # by the same rule as Hypatia.Verdict.level/2, never written by hand.
     jq -n \
         --arg sev "$sev" --arg type "$type" --arg pattern "$pattern" \
         --arg file "$file" --argjson line "$line" --arg code "$code" \
         --arg cwe "$cwe" --arg fix "$fix" --argjson auto "$([ "$auto_fixable" = "true" ] && echo true || echo false)" \
-        '{severity:$sev, type:$type, pattern:$pattern, file:$file,
-          line:$line, code:$code, cwe:$cwe, fix:$fix, auto_fixable:$auto}' \
+        --arg version "$VERSION" \
+        "${VERDICT_LEVEL_JQ}"'
+        {severity:$sev, type:$type, pattern:$pattern, file:$file,
+          line:$line, code:$code, cwe:$cwe, fix:$fix, auto_fixable:$auto,
+          support:{kind:"pattern"},
+          evidence:[{rule:("bash/" + $pattern), rule_version:$version,
+                     span:{file:$file, start_line:$line, end_line:$line},
+                     observations:1}]}
+        | . + {level: verdict_level}' \
         >> "$FINDINGS_FILE"
 
     ((FINDING_COUNT++)) || true
@@ -923,7 +941,7 @@ scan_directory() {
               findings: $findings}'
     elif [[ "$format" == "github" ]]; then
         jq -r '.[] | select(. != {}) |
-            "::\(.severity) file=\(.file),line=\(.line)::\(.pattern) - \(.fix)"' \
+            "::\(.severity) file=\(.file),line=\(.line)::\(.pattern) - \(.fix) [\(.level): \(.support.kind)]"' \
             "$FINDINGS_FILE"
     else
         # Summary header
@@ -946,7 +964,7 @@ scan_directory() {
 
         # Group by type for readability
         jq -r '.[] | select(. != {}) |
-            "[\(.severity | ascii_upcase)] \(.file):\(.line)  (\(.pattern))\n  \(.fix)\n"' \
+            "[\(.severity | ascii_upcase)] \(.file):\(.line)  (\(.pattern); \(.level): \(.support.kind))\n  \(.fix)\n"' \
             "$FINDINGS_FILE"
     fi
 
@@ -989,7 +1007,7 @@ scan_file() {
         echo "$filtered"
     else
         echo "$filtered" | jq -r '.[] |
-            "[\(.severity | ascii_upcase)] \(.file):\(.line)  (\(.pattern))\n  \(.fix)\n"'
+            "[\(.severity | ascii_upcase)] \(.file):\(.line)  (\(.pattern); \(.level): \(.support.kind))\n  \(.fix)\n"'
     fi
 
     rm -f "$FINDINGS_FILE"
@@ -1064,7 +1082,7 @@ check_staged_files() {
 
     if [[ "$critical" -gt 0 ]]; then
         echo "$filtered" | jq -r '.[] | select(.severity == "critical") |
-            "[\(.severity | ascii_upcase)] \(.file):\(.line)  (\(.pattern))\n  \(.fix)\n"'
+            "[\(.severity | ascii_upcase)] \(.file):\(.line)  (\(.pattern); \(.level): \(.support.kind))\n  \(.fix)\n"'
         log_error "Pre-commit BLOCKED: $critical critical issues in staged files"
         return 1
     elif [[ "$count" -gt 0 ]]; then

lib/hypatia/cli.ex

@@ -293,6 +293,17 @@ defmodule Hypatia.CLI do
         "(#{breakdown}); exit #{exit_code}" <>
         if(config.exit_zero and total > 0, do: " (--exit-zero suppressed exit 1)", else: "")
     )
+
+    # A separate line, so the summary above keeps its shape for any caller
+    # that pattern-matches it. Levels are derived (Hypatia.Verdict), never
+    # stored by a rule.
+    levels = Hypatia.Verdict.level_counts(filtered)
+
+    IO.puts(
+      :stderr,
+      "[hypatia] verdict levels: sound=#{levels["sound"]}, epi=#{levels["epi"]}, " <>
+        "belief=#{levels["belief"]}"
+    )
   end
 
   defp env_flag?(name) do
@@ -311,7 +322,9 @@ defmodule Hypatia.CLI do
   @doc """
   Runs the selected rule modules against `repo_path` and returns normalized
   finding maps. Each map includes `rule_module`, `type`, `severity`, `file`,
-  `reason`, and `action`; line-aware findings may also include `line`.
+  `reason`, and `action`; line-aware findings may also include `line`. Every
+  map also carries the HYP-01 verdict fields `support`, `evidence` and the
+  derived `level` (`Hypatia.Verdict`, `schema/findings.ncl`).
   Findings covered by configured suppressions are excluded.
 
   ## Parameters
@@ -983,6 +996,10 @@ defmodule Hypatia.CLI do
         repo_path: repo_path
       )
     end)
+    # HYP-01: every finding names its support. Same funnel, exactly once, so
+    # no rule module can emit a finding without `support`, `evidence` and a
+    # derived `level` (schema/findings.ncl; Hypatia.Verdict).
+    |> Enum.map(&Hypatia.Verdict.annotate/1)
   end
 
   # ─── Code safety scanning ────────────────────────────────────────────
@@ -1223,7 +1240,7 @@ defmodule Hypatia.CLI do
   defp output(findings, "github") do
     # GitHub Actions annotation format
     Enum.each(findings, fn f ->
-      level =
+      annotation =
         case f.severity do
           "critical" -> "error"
           "high" -> "error"
@@ -1234,7 +1251,7 @@ defmodule Hypatia.CLI do
 
       file = Map.get(f, :file, "")
       reason = Map.get(f, :reason, "")
-      IO.puts("::#{level} file=#{file}::#{reason}")
+      IO.puts("::#{annotation} file=#{file}::#{reason} [#{Hypatia.Verdict.describe(f)}]")
     end)
   end
 
@@ -1251,7 +1268,7 @@ defmodule Hypatia.CLI do
         IO.puts(:stderr, "  [#{String.upcase(severity)}] (#{length(group)} findings)")
 
         Enum.each(group, fn f ->
-          IO.puts(:stderr, "    #{f.file}: #{f.reason}")
+          IO.puts(:stderr, "    #{f.file}: #{f.reason} [#{Hypatia.Verdict.describe(f)}]")
         end)
 
         IO.puts(:stderr, "")

lib/hypatia/sarif.ex

@@ -130,6 +130,23 @@ defmodule Hypatia.SARIF do
         "partialFingerprints" => %{"hypatiaFindingHash/v1" => fingerprint}
       }
 
+      # HYP-01 verdict fields ride in the SARIF property bag (SARIF 2.1.0
+      # §3.8), outside the fingerprint, so annotating a finding never
+      # re-opens an alert code scanning has already triaged.
+      result =
+        case Map.get(finding, :level) || Map.get(finding, "level") do
+          nil ->
+            result
+
+          verdict_level ->
+            support = Map.get(finding, :support) || Map.get(finding, "support") || %{}
+
+            Map.put(result, "properties", %{
+              "hypatia.level" => verdict_level,
+              "hypatia.support" => Map.get(support, :kind) || Map.get(support, "kind")
+            })
+        end
+
       rules =
         Map.put_new(rules, rule_id, %{
           "id" => rule_id,

lib/hypatia/verdict.ex

@@ -0,0 +1,179 @@
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
+defmodule Hypatia.Verdict do
+  @moduledoc """
+  Every finding names its support (HYP-01).
+
+  The JSON mirror of `src/Hypatia/ABI/Verdict.idr`, which is normative, and of
+  `schema/findings.ncl`, the contract CI validates scan output against. Each
+  finding carries three fields:
+
+    * `support` — what its evidence supports:
+      `%{kind: "pattern"}` (a rule matched),
+      `%{kind: "observed", observations: n}` (a fleet count; rules.a2ml's
+      thresholds are belief formation, not soundness), or
+      `%{kind: "mechanical", ...}` (a prover re-check, with both digests);
+    * `evidence` — the tokens the finding was issued on: rule, rule version,
+      span, observation count;
+    * `level` — derived here and nowhere else: `"sound"` only for a
+      mechanical support whose re-check confirms; `"epi"` for any other
+      support with evidence; `"belief"` with no evidence at all.
+
+  Elixir rules carry the tag only. No rule is proved sound, so the honest
+  default for every rule-module finding is `pattern` / `epi`. The only way to
+  `"sound"` is `attach_recheck/3`, which refuses a re-check whose target is
+  not the finding's file or whose target digest does not match the bytes on
+  disk. It cannot re-run the prover; `scripts/recheck-lean-hole.sh` is the
+  pattern for checking the artefact digest against a fresh run.
+  """
+
+  @rule_version Mix.Project.config()[:version]
+
+  @provers ~w(lean4 idris2 agda coq)
+  @results ~w(confirms refutes)
+
+  @type level :: String.t()
+
+  @doc "The rule version stamped on evidence tokens (the hypatia version)."
+  @spec rule_version() :: String.t()
+  def rule_version, do: @rule_version
+
+  @doc """
+  Attach `support`, `evidence` and the derived `level` to a finding.
+
+  An existing `support` or `evidence` is kept; a `level` is always
+  recomputed, so a rule cannot assert one.
+  """
+  @spec annotate(map()) :: map()
+  def annotate(finding) when is_map(finding) do
+    support = Map.get(finding, :support) || %{kind: "pattern"}
+    evidence = Map.get(finding, :evidence) || [token(finding)]
+
+    finding
+    |> Map.put(:support, support)
+    |> Map.put(:evidence, evidence)
+    |> Map.put(:level, level(support, evidence))
+  end
+
+  @doc """
+  The evidence token a rule-module finding offers: the rule that fired, at
+  this hypatia version, over the finding's line (`0` when the finding is
+  file- or repository-level). `observations` is this scan's own single
+  observation; fleet-wide counts belong in an `observed` support.
+  """
+  @spec token(map()) :: map()
+  def token(finding) do
+    line =
+      case Map.get(finding, :line) do
+        n when is_integer(n) and n >= 0 -> n
+        _ -> 0
+      end
+
+    %{
+      rule: "#{Map.get(finding, :rule_module, "unknown")}/#{Map.get(finding, :type, "unknown")}",
+      rule_version: @rule_version,
+      span: %{file: to_string(Map.get(finding, :file, "")), start_line: line, end_line: line},
+      observations: 1
+    }
+  end
+
+  @doc """
+  Derive the level from support and evidence (`Verdict.idr` `level`;
+  `schema/findings.ncl` `derive_level`).
+  """
+  @spec level(map(), list()) :: level()
+  def level(%{kind: "mechanical", result: "confirms"}, _evidence), do: "sound"
+  def level(_support, [_ | _]), do: "epi"
+  def level(_support, []), do: "belief"
+
+  @doc """
+  Replace a finding's support with a prover re-check, if the re-check is
+  about this finding's file and its target digest matches the file under
+  `repo_path`.
+
+  `recheck` has string values for `:prover`, `:prover_version`, `:target`,
+  `:target_sha256`, `:artefact_sha256` and `:result`. A re-check that
+  `"refutes"` is attached as recorded and derives `"epi"`, not `"sound"`.
+  """
+  @spec attach_recheck(map(), map(), String.t()) :: {:ok, map()} | {:error, term()}
+  def attach_recheck(finding, recheck, repo_path) do
+    with :ok <- check_string(:target, recheck[:target]),
+         :ok <- check_string(:prover_version, recheck[:prover_version]),
+         :ok <- check_member(:prover, recheck[:prover], @provers),
+         :ok <- check_member(:result, recheck[:result], @results),
+         :ok <- check_digest(:target_sha256, recheck[:target_sha256]),
+         :ok <- check_digest(:artefact_sha256, recheck[:artefact_sha256]),
+         :ok <- check_same_target(finding, recheck),
+         {:ok, digest} <- file_sha256(Path.join(repo_path, recheck.target)),
+         :ok <- check_target_digest(digest, recheck.target_sha256) do
+      support =
+        recheck
+        |> Map.take([:prover, :prover_version, :target, :target_sha256, :artefact_sha256, :result])
+        |> Map.put(:kind, "mechanical")
+
+      {:ok, finding |> Map.put(:support, support) |> annotate()}
+    end
+  end
+
+  @doc """
+  One-line rendering of a finding's level and support, for text and
+  GitHub-annotation output. Derived from the record, never stored on it.
+  """
+  @spec describe(map()) :: String.t()
+  def describe(finding) do
+    support = Map.get(finding, :support) || %{kind: "pattern"}
+    evidence = Map.get(finding, :evidence) || []
+
+    basis =
+      case support do
+        %{kind: "mechanical"} = s -> "#{s.prover} #{s.prover_version} re-check #{s.result}"
+        %{kind: "observed", observations: n} -> "observed #{n}x"
+        %{kind: kind} -> to_string(kind)
+      end
+
+    "#{level(support, evidence)}: #{basis}"
+  end
+
+  @doc "Count findings by level, every level present (for the scan summary)."
+  @spec level_counts([map()]) :: %{level() => non_neg_integer()}
+  def level_counts(findings) do
+    Enum.reduce(findings, %{"sound" => 0, "epi" => 0, "belief" => 0}, fn f, acc ->
+      Map.update(acc, Map.get(f, :level, "belief"), 1, &(&1 + 1))
+    end)
+  end
+
+  defp check_string(field, value) do
+    if is_binary(value) and value != "", do: :ok, else: {:error, {:invalid, field, value}}
+  end
+
+  defp check_member(field, value, allowed) do
+    if value in allowed, do: :ok, else: {:error, {:invalid, field, value}}
+  end
+
+  defp check_digest(field, value) do
+    if is_binary(value) and value =~ ~r/\A[0-9a-f]{64}\z/,
+      do: :ok,
+      else: {:error, {:invalid, field, value}}
+  end
+
+  defp check_same_target(finding, recheck) do
+    if Path.expand(to_string(Map.get(finding, :file, "")), "/") ==
+         Path.expand(recheck.target, "/"),
+       do: :ok,
+       else: {:error, {:target_mismatch, Map.get(finding, :file), recheck.target}}
+  end
+
+  defp file_sha256(path) do
+    case File.read(path) do
+      {:ok, bytes} -> {:ok, :crypto.hash(:sha256, bytes) |> Base.encode16(case: :lower)}
+      {:error, reason} -> {:error, {:unreadable_target, path, reason}}
+    end
+  end
+
+  defp check_target_digest(actual, recorded) do
+    if actual == recorded,
+      do: :ok,
+      else: {:error, {:target_digest_mismatch, actual, recorded}}
+  end
+end