From 9b80032bad8bdcf563a4f0cd21b078e1050ba5a2 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 12:54:30 +0000 Subject: [PATCH 1/3] fix(secret-alerts): give each finding its HYP-01 verdict fields `hypatia secret-alerts` (from #969) printed the SSA findings as the rule module built them: no `support`, `evidence` or derived `level`. HYP-01 requires every finding to name all three, and the scan path already adds them through Hypatia.Verdict.annotate/1. The secret-alerts line was the one output that skipped it. Each finding now goes through Verdict.annotate/1. The fields the sweep workflow reads (rule, severity, reason, detail) are unchanged. `rule_module`/`type` are added so the evidence token names the rule, e.g. `secret_scanning_alerts/SSA001`. Test: a finding on the secret-alerts line carries support `pattern`, level `epi` and that evidence token. It fails without the fix. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01P4yFkxW5Heb8p2YW7ZYs9F --- lib/hypatia/cli.ex | 12 +++++++++++- test/cli_test.exs | 24 ++++++++++++++++++++++++ 2 files changed, 35 insertions(+), 1 deletion(-) diff --git a/lib/hypatia/cli.ex b/lib/hypatia/cli.ex index 1322f7da..004be994 100644 --- a/lib/hypatia/cli.ex +++ b/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 diff --git a/test/cli_test.exs b/test/cli_test.exs index ffa0d417..cd9ef52e 100644 --- a/test/cli_test.exs +++ b/test/cli_test.exs @@ -42,6 +42,30 @@ 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} + } + + sweep = fn _, _ -> {:ok, %{findings: [finding], total: 1, by_severity: %{critical: 1}}} end + + assert {line, 0} = Hypatia.CLI.secret_alerts_output("acme", "demo", sweep) + assert {:ok, %{"findings" => [decoded]}} = Jason.decode(line) + + assert %{ + "rule" => "SSA001", + "detail" => %{"alert_number" => 1}, + "support" => %{"kind" => "pattern"}, + "level" => "epi", + "evidence" => [%{"rule" => "secret_scanning_alerts/SSA001"}] + } = decoded + 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 From 44e63ef57e036f5b9feab87d78bb5fd796efc1be Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:23:28 +0000 Subject: [PATCH 2/3] =?UTF-8?q?proof(abi):=20Idris2=20contract=20for=20the?= =?UTF-8?q?=20secret-alerts=20line=20(PROOF-POLICY=20=C2=A71)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `hypatia secret-alerts` prints one JSON line and an exit code, and the private secret-scanning sweep reads both from bash/jq. PROOF-POLICY §1 assigns cross-language wire contracts to Idris2, so this adds Hypatia.ABI.SecretAlerts (%default total, no escape hatches). It proves: - exit 0 exactly for status ok and 3 for error, with the status recoverable from the code (exitZeroIsOk, errorExitsThree, statusOfExitRoundTrip); no other code reads as ok (nonZeroNotOk), so a crash or usage error is never a clean read; - an error line is always Unread, never Clean, and a Clean line exits 0 (errorIsUnread, errorNeverClean, unreadIsError, cleanExitsZero); - `total` is the number of findings by construction (a length-indexed vector; totalIsLength); - every finding is a pattern-supported HYP-01 verdict and is never reported "sound" (findingNeverSound, via patternNeverSoundLevel). It does not prove that the Elixir producer emits this shape. The ExUnit tests check that on sample data (TESTED), and §2.1 says a model is not a refinement proof. The check-verdicts gate covers the module: escape-hatch scan, one positive control (SecretAlertsLines) and three expected rejections (error read as Clean, total disagreeing with findings, empty error reason). Each is refused at `invalid` with its stated diagnostic. verification/PROOF-STATUS rows and the CLAUDE.md ABI table are updated. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01P4yFkxW5Heb8p2YW7ZYs9F --- .claude/CLAUDE.md | 1 + scripts/check-verdicts.sh | 2 +- src/Hypatia/ABI/SecretAlerts.idr | 209 ++++++++++++++++++++ src/abi/hypatia-abi.ipkg | 1 + tests/accept/SecretAlertsLines.idr | 50 +++++ tests/reject/SecretAlertsEmptyReason.idr | 20 ++ tests/reject/SecretAlertsErrorIsClean.idr | 24 +++ tests/reject/SecretAlertsTotalDisagrees.idr | 28 +++ verification/PROOF-STATUS.adoc | 34 ++++ 9 files changed, 368 insertions(+), 1 deletion(-) create mode 100644 src/Hypatia/ABI/SecretAlerts.idr create mode 100644 tests/accept/SecretAlertsLines.idr create mode 100644 tests/reject/SecretAlertsEmptyReason.idr create mode 100644 tests/reject/SecretAlertsErrorIsClean.idr create mode 100644 tests/reject/SecretAlertsTotalDisagrees.idr diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md index 62980ffc..5926aa1c 100644 --- a/.claude/CLAUDE.md +++ b/.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`) | **Build system:** `src/abi/hypatia-abi.ipkg` (compile), `verify/hypatia-verify.ipkg` (proofs), `pack.toml` (Pack package manager). The ipkg sets `sourcedir = ".."`, so **`src/Hypatia/ABI/` is what compiles** — that is the diff --git a/scripts/check-verdicts.sh b/scripts/check-verdicts.sh index ba896bcd..1f478da0 100755 --- a/scripts/check-verdicts.sh +++ b/scripts/check-verdicts.sh @@ -40,7 +40,7 @@ mkdir -p "$logs" 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; do +for module in src/Hypatia/ABI/Verdict.idr src/Hypatia/ABI/Retraction.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 diff --git a/src/Hypatia/ABI/SecretAlerts.idr b/src/Hypatia/ABI/SecretAlerts.idr new file mode 100644 index 00000000..8333cb12 --- /dev/null +++ b/src/Hypatia/ABI/SecretAlerts.idr @@ -0,0 +1,209 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- 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) diff --git a/src/abi/hypatia-abi.ipkg b/src/abi/hypatia-abi.ipkg index 7a8964a9..8b3bfa70 100644 --- a/src/abi/hypatia-abi.ipkg +++ b/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 builddir = "../../build/abi" diff --git a/tests/accept/SecretAlertsLines.idr b/tests/accept/SecretAlertsLines.idr new file mode 100644 index 00000000..e5d28063 --- /dev/null +++ b/tests/accept/SecretAlertsLines.idr @@ -0,0 +1,50 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- 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 diff --git a/tests/reject/SecretAlertsEmptyReason.idr b/tests/reject/SecretAlertsEmptyReason.idr new file mode 100644 index 00000000..49db78c4 --- /dev/null +++ b/tests/reject/SecretAlertsEmptyReason.idr @@ -0,0 +1,20 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- 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) diff --git a/tests/reject/SecretAlertsErrorIsClean.idr b/tests/reject/SecretAlertsErrorIsClean.idr new file mode 100644 index 00000000..7c7b7e53 --- /dev/null +++ b/tests/reject/SecretAlertsErrorIsClean.idr @@ -0,0 +1,24 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- EXPECTED REJECTION (secret-alerts line contract). scripts/check-verdicts.sh +-- passes only if Idris2 refuses this module, and only at `invalid`. +-- +-- Must fail: a line that could not read the alerts is Unread, never Clean. +-- A sweep must not count "could not look" as "no alerts". +-- +-- EXPECT: Mismatch between: Clean and Unread. + +module SecretAlertsErrorIsClean + +import Data.List +import Hypatia.ABI.SecretAlerts + +%default total + +errLine : AlertLine Error +errLine = ErrLine "acme" "demo" "HTTP 403" + (MkNonEmptyString IsNonEmpty) + +invalid : outcome SecretAlertsErrorIsClean.errLine = Clean +invalid = Refl diff --git a/tests/reject/SecretAlertsTotalDisagrees.idr b/tests/reject/SecretAlertsTotalDisagrees.idr new file mode 100644 index 00000000..4a813057 --- /dev/null +++ b/tests/reject/SecretAlertsTotalDisagrees.idr @@ -0,0 +1,28 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- EXPECTED REJECTION (secret-alerts line contract). scripts/check-verdicts.sh +-- passes only if Idris2 refuses this module, and only at `invalid`. +-- +-- Must fail: an ok line's `total` is the number of findings. A line +-- claiming two findings while carrying one does not typecheck. +-- +-- EXPECT: Mismatch between: 0 and 1. + +module SecretAlertsTotalDisagrees + +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 + +invalid : AlertLine Ok +invalid = OkLine "acme" "demo" 2 [SecretAlertsTotalDisagrees.finding] diff --git a/verification/PROOF-STATUS.adoc b/verification/PROOF-STATUS.adoc index ea95851c..fbcedaa0 100644 --- a/verification/PROOF-STATUS.adoc +++ b/verification/PROOF-STATUS.adoc @@ -286,6 +286,40 @@ untouched-finding negative control and two mutants killed |TESTED a scan or dispatch path. It is not, like the rest of the safety systems (CLAUDE.md Known Gap 2) |OPEN +|`+src/Hypatia/ABI/SecretAlerts.idr+` |Idris2 |The `hypatia +secret-alerts` line contract, a cross-language wire format read by the +bash/jq secret-scanning sweep. The exit code is 0 exactly for an ok line and +3 for an error line (`+exitZeroIsOk+`, `+errorExitsThree+`, +`+statusOfExitRoundTrip+`); no non-zero code reads as ok +(`+nonZeroNotOk+`); an error line is always Unread and never Clean +(`+errorIsUnread+`, `+errorNeverClean+`, `+unreadIsError+`); a Clean line +exits 0 (`+cleanExitsZero+`); `total` is the number of findings by +construction (`+totalIsLength+`); no finding is reported "sound" +(`+findingNeverSound+`) |PROVEN + +|`+tests/accept/SecretAlertsLines.idr+` |Idris2 |Positive control: an ok +line with one pattern-supported finding and an error line are accepted, +classify as WithAlerts / Unread, and exit 0 / 3 (`+okHasAlerts+`, +`+errUnread+`, `+findingIsEpi+`) |TESTED + +|`+tests/reject/SecretAlertsErrorIsClean.idr+` |Idris2 |Expected +rejection: an error line read as Clean is refused at `+invalid+` |TESTED + +|`+tests/reject/SecretAlertsTotalDisagrees.idr+` |Idris2 |Expected +rejection: an ok line whose `total` disagrees with its findings is refused +at `+invalid+` |TESTED + +|`+tests/reject/SecretAlertsEmptyReason.idr+` |Idris2 |Expected +rejection: an error line with an empty reason is refused at `+invalid+` +|TESTED + +|Producer, lib/hypatia/cli.ex `secret_alerts_output/3` |Elixir |The +Elixir producer emits the contract's shape: ok with findings and exit 0, +error and exit 3, and every finding annotated with its HYP-01 verdict +fields. Checked on sample data by test/cli_test.exs ("secret-alerts"), not +proved; the Idris2 module is a model of the interface, not a refinement +proof of the producer (PROOF-POLICY §2.1) |TESTED + |Derived workflow steps, lib/dispatch_manifest.ex |Elixir |Every dispatch-manifest step names the verdict it derives from, and a factless step refuses the whole manifest before anything is written: From 35311cee9315c0ff3ef9199c3db573ae8b5b7cd3 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 10 Nov 2026 15:45:08 +0000 Subject: [PATCH 3/3] test(secret-alerts): every finding is annotated and keeps its own fields CodeRabbit review of #1024 (both Trivial): the fixture had one finding, so a regression that annotated only the first would pass, and dropping severity, reason or action went unnoticed. Two findings now, each checked. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0136P7ZnmBahbhfkFEP6ark4 --- test/cli_test.exs | 43 +++++++++++++++++++++++++++++++++---------- 1 file changed, 33 insertions(+), 10 deletions(-) diff --git a/test/cli_test.exs b/test/cli_test.exs index cd9ef52e..38c60911 100644 --- a/test/cli_test.exs +++ b/test/cli_test.exs @@ -52,18 +52,41 @@ defmodule Hypatia.CLITest do detail: %{alert_number: 1} } - sweep = fn _, _ -> {:ok, %{findings: [finding], total: 1, by_severity: %{critical: 1}}} end + 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" => [decoded]}} = Jason.decode(line) - - assert %{ - "rule" => "SSA001", - "detail" => %{"alert_number" => 1}, - "support" => %{"kind" => "pattern"}, - "level" => "epi", - "evidence" => [%{"rule" => "secret_scanning_alerts/SSA001"}] - } = decoded + 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