diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md index dda873e5..ced3c241 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`) | | `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). 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/scripts/check-verdicts.sh b/scripts/check-verdicts.sh index 37ad0b18..52fc50cc 100755 --- a/scripts/check-verdicts.sh +++ b/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 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 9523d1db..1c296db3 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 , Hypatia.ABI.RsrProfile builddir = "../../build/abi" diff --git a/test/cli_test.exs b/test/cli_test.exs index ffa0d417..38c60911 100644 --- a/test/cli_test.exs +++ b/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 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 6ec4190b..f87e35f1 100644 --- a/verification/PROOF-STATUS.adoc +++ b/verification/PROOF-STATUS.adoc @@ -388,6 +388,50 @@ parse or carries no list passes 3.2.2 with no profile present (`+residualDivergence+`) |OPEN |=== +==== secret-alerts line contract (HYP-01, 2026-11-09) + +An engineering property of a cross-language wire format (PROOF-POLICY §1: +Idris2), so it carries the §5 tokens only and no PWG. +`+scripts/check-verdicts.sh+` (CI: `idris2 --check` job) is the gate. + +[width="100%",cols="28%,14%,42%,16%",options="header",] +|=== +|File |Language |Claim |Status +|`+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 +|=== + ==== actions.lock closure (2026-11-09, standards#963 criterion 5) An engineering property of one wire format (`+actions.lock+`), so Idris2