secret-alerts: HYP-01 verdict fields + Idris2 line contract (PROOF-POLICY §1)

.claude/CLAUDE.md

@@ -177,6 +177,7 @@ Training pipeline reads outcomes/*.jsonl for ESN (confidence time series) and pa
 | `RuleEngine.idr` | Rule-evaluation types |
 | `Verdict.idr` | Verdict records (HYP-01): support = Pattern / Observed n / Mechanical re-check; `Sound` only from a confirming re-check. Gate: `scripts/check-verdicts.sh` (+ `tests/reject/`, `tests/accept/`) |
 | `Retraction.idr` | Quarantine as retraction (HYP-01): a token survives iff its support thins into what remains; a finding survives through one of its tokens. Transcribed from residual-evidence-types `Revision.agda` @ 97244f5 |
+| `SecretAlerts.idr` | The `hypatia secret-alerts` line contract read by the bash/jq secret-scanning sweep: exit 0 iff ok, 3 iff error; an error line is never "clean"; `total` = number of findings; no finding is "sound". Gate: `scripts/check-verdicts.sh` (`tests/accept/SecretAlertsLines.idr`, `tests/reject/SecretAlerts*.idr`) |
 | `RsrProfile.idr` | RSR capability-profile resolution (engineering model of `lib/rules/rsr_conformance.ex`): deed precedence, fail-closed duplicate/list-less clauses, a2ml fallback, and when criterion 3.2.2 agrees with the scorecard's `profile_present` (and the one case it does not). Gate: `scripts/check-verdicts.sh` (+ `tests/reject/`, `tests/accept/`) |
 
 **Build system:** `src/abi/hypatia-abi.ipkg` (compile), `verify/hypatia-verify.ipkg` (proofs), `pack.toml` (Pack package manager).

lib/hypatia/cli.ex

@@ -323,7 +323,7 @@ defmodule Hypatia.CLI do
             status: "ok",
             total: result.total,
             by_severity: result.by_severity,
-            findings: result.findings
+            findings: Enum.map(result.findings, &annotate_secret_alert/1)
           })
 
         {line, 0}
@@ -333,6 +333,16 @@ defmodule Hypatia.CLI do
     end
   end
 
+  # Every finding names its support, evidence and derived level (HYP-01),
+  # as the scan path does. The rule fields the sweep reads are kept as they
+  # are; `rule_module`/`type` give the evidence token its rule name.
+  defp annotate_secret_alert(finding) do
+    finding
+    |> Map.put(:rule_module, "secret_scanning_alerts")
+    |> Map.put(:type, finding.rule)
+    |> Hypatia.Verdict.annotate()
+  end
+
   # ─── Diagnostic summary ──────────────────────────────────────────────
   #
   # Always emit a single-line summary on stderr after a scan/report so CI

scripts/check-verdicts.sh

@@ -47,7 +47,7 @@ export IDRIS2_PATH="$PWD/build/abi/ttc${IDRIS2_PATH:+:$IDRIS2_PATH}"
 
 # 2. No escape hatch in the modules the rejections are about.
 for module in src/Hypatia/ABI/Verdict.idr src/Hypatia/ABI/Retraction.idr \
-              src/Hypatia/ABI/RsrProfile.idr; do
+              src/Hypatia/ABI/RsrProfile.idr src/Hypatia/ABI/SecretAlerts.idr; do
   if grep -nE 'believe_me|assert_total|assert_smaller|idris_crash|postulate|sorry|admit|native_decide|Admitted|unsafeCoerce|Obj\.magic' \
        "$module"; then
     echo "ERROR: escape-hatch marker in $module" >&2

src/Hypatia/ABI/SecretAlerts.idr

@@ -0,0 +1,209 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+-- Hypatia ABI — the `hypatia secret-alerts` line contract
+--
+-- `hypatia secret-alerts --owner O --repo R` prints one JSON line and exits.
+-- A bash/jq consumer (the private estate secret-scanning sweep) reads the line
+-- and the exit code, so the pair is a cross-language wire contract: PROOF-POLICY
+-- §1 assigns it to Idris2.  The Elixir producer is
+-- `Hypatia.CLI.secret_alerts_output/3`; test/cli_test.exs ("secret-alerts")
+-- exercises it.
+--
+-- The contract:
+--   * status "ok": the alerts were read.  The line carries `total` and the
+--     findings; `total` is the number of findings; exit code 0.
+--   * status "error": the alerts could not be read (refused token, secret
+--     scanning disabled, timeout, pagination cap).  The line carries a
+--     non-empty reason; exit code 3.
+--   * A sweep classifies a line as Clean (ok, no findings), WithAlerts (ok,
+--     at least one finding) or Unread (error).  "Could not look" is never
+--     "clean".
+--   * Every finding is a pattern-supported HYP-01 verdict, so it is never
+--     reported at level "sound".
+--
+-- What is proved here (%default total, no proof-bypass primitives):
+--   * the exit code is 0 exactly for status Ok, and 3 for Error
+--     (`exitZeroIsOk`, `errorExitsThree`), and the status can be recovered
+--     from the exit code (`statusOfExitRoundTrip`);
+--   * no exit code other than 0 reads as Ok (`nonZeroNotOk`), so a crash
+--     (exit 1) or a usage error (exit 2) is never taken for a clean read;
+--   * an error line is always Unread, and a Clean line has exit 0
+--     (`errorIsUnread`, `cleanExitsZero`, `unreadIsError`);
+--   * `total` equals the number of findings by construction (the findings
+--     are a vector indexed by `total`; `totalIsLength`);
+--   * every finding is pattern-supported and never "sound"
+--     (`findingNeverSound`).
+--
+-- What is NOT proved here:
+--   * that the Elixir producer emits exactly this shape: the ExUnit tests
+--     check it on sample data (TESTED), and this module does not prove
+--     runtime refinement (PROOF-POLICY §2.1: a model does not prove the
+--     implementation);
+--   * anything about GitHub's API: pagination, rate limits and token scope
+--     are the producer's job.
+
+module Hypatia.ABI.SecretAlerts
+
+import Data.List
+import Data.Vect
+import Hypatia.ABI.Verdict
+
+%default total
+
+------------------------------------------------------------------------
+-- Section 1: Status and exit code
+------------------------------------------------------------------------
+
+||| Whether the alerts were read.
+public export
+data Status = Ok | Error
+
+public export
+Uninhabited (Ok = Error) where
+  uninhabited Refl impossible
+
+public export
+Uninhabited (Error = Ok) where
+  uninhabited Refl impossible
+
+||| The process exit code for each status.
+public export
+exitCode : Status -> Nat
+exitCode Ok    = 0
+exitCode Error = 3
+
+||| Read a status back from an exit code.  Any code but 0 and 3 (a crash,
+||| a usage error) is not a status line at all.
+public export
+statusOfExit : Nat -> Maybe Status
+statusOfExit 0 = Just Ok
+statusOfExit 3 = Just Error
+statusOfExit _ = Nothing
+
+||| The exit code determines the status.
+public export
+statusOfExitRoundTrip : (s : Status) -> statusOfExit (exitCode s) = Just s
+statusOfExitRoundTrip Ok    = Refl
+statusOfExitRoundTrip Error = Refl
+
+||| Exit 0 means Ok.
+public export
+exitZeroIsOk : (s : Status) -> exitCode s = 0 -> s = Ok
+exitZeroIsOk Ok    Refl = Refl
+exitZeroIsOk Error prf  = absurd prf
+
+||| An error exits 3, never 0.
+public export
+errorExitsThree : exitCode Error = 3
+errorExitsThree = Refl
+
+||| No non-zero exit code reads as Ok.
+public export
+nonZeroNotOk : (n : Nat) -> Not (n = 0) -> Not (statusOfExit n = Just Ok)
+nonZeroNotOk 0 nz _ = nz Refl
+nonZeroNotOk 1 _ prf = absurd prf
+nonZeroNotOk 2 _ prf = absurd prf
+nonZeroNotOk 3 _ prf = absurd (justInjective prf)
+  where
+    justInjective : Just Error = Just Ok -> Error = Ok
+    justInjective Refl impossible
+nonZeroNotOk (S (S (S (S k)))) _ prf = absurd prf
+
+------------------------------------------------------------------------
+-- Section 2: The line
+------------------------------------------------------------------------
+
+||| A secret-scanning finding: a pattern-supported verdict (rule SSA001 to
+||| SSA004).  The rule cannot assert a level; it is derived (HYP-01).
+public export
+record SecretFinding where
+  constructor MkSecretFinding
+  verdict   : Verdict
+  isPattern : support verdict = Pattern
+
+||| A non-empty string, for an error reason.
+public export
+data NonEmptyString : String -> Type where
+  MkNonEmptyString : {0 s : String} -> NonEmpty (unpack s) -> NonEmptyString s
+
+||| One output line, indexed by its status.  An Ok line's findings are a
+||| vector of length `count` (the wire `total`), so it cannot disagree with them.
+public export
+data AlertLine : Status -> Type where
+  OkLine  : (owner, repo : String) -> (count : Nat)
+         -> (findings : Vect count SecretFinding) -> AlertLine Ok
+  ErrLine : (owner, repo : String) -> (reason : String)
+         -> NonEmptyString reason -> AlertLine Error
+
+||| The exit code a line is printed with.
+public export
+exitOf : {s : Status} -> AlertLine s -> Nat
+exitOf {s} _ = exitCode s
+
+||| `total` is the number of findings.
+public export
+totalIsLength : (owner, repo : String) -> (n : Nat) -> (fs : Vect n SecretFinding)
+             -> length fs = n
+totalIsLength _ _ n fs = lengthCorrect fs
+
+------------------------------------------------------------------------
+-- Section 3: How a sweep reads a line
+------------------------------------------------------------------------
+
+||| The three outcomes a sweep distinguishes.
+public export
+data Outcome = Clean | WithAlerts | Unread
+
+public export
+Uninhabited (Unread = Clean) where
+  uninhabited Refl impossible
+
+||| Classify a line.
+public export
+outcome : AlertLine s -> Outcome
+outcome (OkLine _ _ 0 _)     = Clean
+outcome (OkLine _ _ (S _) _) = WithAlerts
+outcome (ErrLine _ _ _ _)    = Unread
+
+||| An error line is always Unread: "could not look" is never "clean".
+public export
+errorIsUnread : (l : AlertLine Error) -> outcome l = Unread
+errorIsUnread (ErrLine _ _ _ _) = Refl
+
+||| An error line is never Clean.
+public export
+errorNeverClean : (l : AlertLine Error) -> Not (outcome l = Clean)
+errorNeverClean l prf = absurd (trans (sym (errorIsUnread l)) prf)
+
+||| A Clean line was printed with exit code 0.
+public export
+cleanExitsZero : {s : Status} -> (l : AlertLine s) -> outcome l = Clean -> exitOf l = 0
+cleanExitsZero (OkLine _ _ 0 _)     Refl = Refl
+cleanExitsZero (OkLine _ _ (S _) _) prf  = absurd prf
+  where
+    Uninhabited (WithAlerts = Clean) where
+      uninhabited Refl impossible
+cleanExitsZero (ErrLine _ _ _ _)    prf  = absurd prf
+
+||| An Unread line has status Error.
+public export
+unreadIsError : {s : Status} -> (l : AlertLine s) -> outcome l = Unread -> s = Error
+unreadIsError (OkLine _ _ 0 _)     prf = absurd prf
+  where
+    Uninhabited (Clean = Unread) where
+      uninhabited Refl impossible
+unreadIsError (OkLine _ _ (S _) _) prf = absurd prf
+  where
+    Uninhabited (WithAlerts = Unread) where
+      uninhabited Refl impossible
+unreadIsError (ErrLine _ _ _ _)    Refl = Refl
+
+------------------------------------------------------------------------
+-- Section 4: Findings are never "sound"
+------------------------------------------------------------------------
+
+||| No secret-scanning finding is reported at level "sound".
+public export
+findingNeverSound : (f : SecretFinding) -> Not (level (verdict f) = LvSound)
+findingNeverSound f = patternNeverSoundLevel (verdict f) (isPattern f)

src/abi/hypatia-abi.ipkg

@@ -24,6 +24,7 @@ modules = Hypatia.ABI.Types
         , Hypatia.ABI.RuleEngine
         , Hypatia.ABI.Verdict
         , Hypatia.ABI.Retraction
+        , Hypatia.ABI.SecretAlerts
         , Hypatia.ABI.RsrProfile
 
 builddir = "../../build/abi"

test/cli_test.exs

@@ -42,6 +42,53 @@ defmodule Hypatia.CLITest do
       assert {:ok, %{"status" => "ok", "repo" => "demo", "total" => 0}} = Jason.decode(line)
     end
 
+    test "each finding names its support, evidence and derived level (HYP-01)" do
+      finding = %{
+        rule: "SSA001",
+        file: "github_personal_access_token",
+        severity: :critical,
+        reason: "open alert",
+        action: :escalate,
+        detail: %{alert_number: 1}
+      }
+
+      stale = %{
+        finding
+        | rule: "SSA002",
+          severity: :high,
+          reason: "stale alert",
+          action: :report,
+          detail: %{alert_number: 2}
+      }
+
+      sweep = fn _, _ ->
+        {:ok, %{findings: [finding, stale], total: 2, by_severity: %{critical: 1, high: 1}}}
+      end
+
+      assert {line, 0} = Hypatia.CLI.secret_alerts_output("acme", "demo", sweep)
+      assert {:ok, %{"findings" => [first, second]}} = Jason.decode(line)
+
+      # Every finding is annotated, not only the first, and the rule's own
+      # fields (severity, reason, action) survive the annotation.
+      for {decoded, rule, n, severity, reason, action} <- [
+            {first, "SSA001", 1, "critical", "open alert", "escalate"},
+            {second, "SSA002", 2, "high", "stale alert", "report"}
+          ] do
+        assert %{
+                 "rule" => ^rule,
+                 "detail" => %{"alert_number" => ^n},
+                 "severity" => ^severity,
+                 "reason" => ^reason,
+                 "action" => ^action,
+                 "support" => %{"kind" => "pattern"},
+                 "level" => "epi",
+                 "evidence" => [%{"rule" => evidence_rule}]
+               } = decoded
+
+        assert evidence_rule == "secret_scanning_alerts/" <> rule
+      end
+    end
+
     test "a failed fetch is reported as an error with exit 3, never as clean" do
       sweep = fn _, _ -> {:error, "GitHub API 404: Secret scanning is disabled"} end
 

tests/accept/SecretAlertsLines.idr

@@ -0,0 +1,50 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+-- POSITIVE CONTROL (secret-alerts line contract).  The counterparts of
+-- tests/reject/SecretAlerts*.idr: a well-formed ok line with one
+-- pattern-supported finding, and a well-formed error line, are accepted;
+-- they classify as WithAlerts (exit 0) and Unread (exit 3); the finding is
+-- never "sound".  test/cli_test.exs ("secret-alerts") checks the Elixir
+-- producer on the same shapes.
+
+module SecretAlertsLines
+
+import Data.List
+import Data.Vect
+import Hypatia.ABI.Verdict
+import Hypatia.ABI.SecretAlerts
+
+%default total
+
+token : EvidenceToken
+token = MkEvidenceToken "secret_scanning_alerts" "SSA001" "0.1.0"
+          (MkSpan "github_personal_access_token" 0 0) 1
+
+finding : SecretFinding
+finding = MkSecretFinding (MkVerdict "open secret-scanning alert" [token] Pattern) Refl
+
+okLine : AlertLine Ok
+okLine = OkLine "acme" "demo" 1 [finding]
+
+errLine : AlertLine Error
+errLine = ErrLine "acme" "demo" "HTTP 404"
+            (MkNonEmptyString IsNonEmpty)
+
+okHasAlerts : outcome SecretAlertsLines.okLine = WithAlerts
+okHasAlerts = Refl
+
+okExits0 : exitOf SecretAlertsLines.okLine = 0
+okExits0 = Refl
+
+errUnread : outcome SecretAlertsLines.errLine = Unread
+errUnread = Refl
+
+errExits3 : exitOf SecretAlertsLines.errLine = 3
+errExits3 = Refl
+
+findingIsEpi : level (verdict SecretAlertsLines.finding) = LvEpi
+findingIsEpi = Refl
+
+findingNotSound : Not (level (verdict SecretAlertsLines.finding) = LvSound)
+findingNotSound = findingNeverSound SecretAlertsLines.finding

tests/reject/SecretAlertsEmptyReason.idr

@@ -0,0 +1,20 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+-- EXPECTED REJECTION (secret-alerts line contract).  scripts/check-verdicts.sh
+-- passes only if Idris2 refuses this module, and only at `invalid`.
+--
+-- Must fail: an error line names why the alerts could not be read.  An
+-- empty reason does not typecheck.
+--
+-- EXPECT: Mismatch between: ?x :: ?xs and [].
+
+module SecretAlertsEmptyReason
+
+import Data.List
+import Hypatia.ABI.SecretAlerts
+
+%default total
+
+invalid : AlertLine Error
+invalid = ErrLine "acme" "demo" "" (MkNonEmptyString IsNonEmpty)