fix(rules): rule precision — WH006/WH013, harvested-registry, npx text, proof suites

lib/cross_repo_learning.ex

@@ -616,8 +616,12 @@ defmodule Hypatia.CrossRepoLearning do
         |> Map.get("languages", %{})
         |> Enum.sort_by(fn {lang, count} ->
           count_score = if is_number(count), do: -count, else: 0
-          prio = Enum.find_index(@language_priority, &(String.downcase(&1) == String.downcase(lang)))
-          {count_score, if(prio, do: prio, else: length(@language_priority)), String.downcase(lang)}
+
+          prio =
+            Enum.find_index(@language_priority, &(String.downcase(&1) == String.downcase(lang)))
+
+          {count_score, if(prio, do: prio, else: length(@language_priority)),
+           String.downcase(lang)}
         end)
         |> List.first({"unknown", 0})
         |> elem(0)

lib/hypatia/scanner_suppression.ex

@@ -59,7 +59,12 @@ defmodule Hypatia.ScannerSuppression do
     "security_errors" => %{
       :any =>
         @training_corpus_paths ++
-          [".github/workflows/integration.yml"]
+          [".github/workflows/integration.yml"],
+      # `harvested-registry/` is a corpus of OTHER projects' manifests kept as
+      # reference material; example credentials are its content, the same
+      # justification as `.audittraining/` (#865). Scoped to `secret_detected`
+      # only — every other security_errors rule still scans it.
+      "secret_detected" => ["harvested-registry/"]
     },
     # ⚠ `benches/` is exempted for code_safety ONLY, deliberately not for
     # security_errors. Cargo's convention puts benchmarks in `benches/`, and a
@@ -454,7 +459,8 @@ defmodule Hypatia.ScannerSuppression do
   # pragmas (`hypatia:ignore RE005 -- <reason>`, `hypatia:ignore zig_ptr_cast`)
   # use the verb form; both are honoured identically.
   defp directive_re,
-    do: ~r/(?:^|[\s#\/\-;])hypatia:\s*(?:allow|ignore)\s+([A-Za-z0-9_\*]+)(?:\/([A-Za-z0-9_\*]+))?/i
+    do:
+      ~r/(?:^|[\s#\/\-;])hypatia:\s*(?:allow|ignore)\s+([A-Za-z0-9_\*]+)(?:\/([A-Za-z0-9_\*]+))?/i
 
   defp directive_matches?(line, rule_module, rule_type) do
     case Regex.run(directive_re(), line) do

lib/rules/cicd_rules.ex

@@ -440,7 +440,7 @@ defmodule Hypatia.Rules.CicdRules do
       id: :npx_in_workflow,
       pattern: ~r/(?:^|[\s;&|])(?:npx|npm[[:space:]]+run)\b/m,
       reason:
-        "npx / `npm run` banned in CI -- use `deno task` or `deno run` instead (npm fully banned 2026-05-25)",
+        "npx / `npm run` banned in CI -- use `bunx` or `bun run` instead (npm banned 2026-05-25; Deno banned 2026-09-22, standards LANGUAGE-POLICY §1.3)",
       applies_to: ["*.yml", "*.yaml", "*.sh", "Justfile", "Mustfile"]
     },
     %{id: :golang_detected, glob: "*.go", reason: "Go banned -- use Rust"},

lib/rules/honest_completion.ex

@@ -63,6 +63,7 @@ defmodule Hypatia.Rules.HonestCompletion do
       has_ci: File.dir?(Path.join(repo_path, ".github/workflows")),
       has_tests_dir:
         File.dir?(Path.join(repo_path, "test")) or File.dir?(Path.join(repo_path, "tests")),
+      has_proof_suite: proof_suite_checked_in_ci?(repo_path),
       # State file location convention varies across the estate:
       # most repos use .machine_readable/STATE.a2ml directly; some
       # (including hypatia) namespace it under a profile dir like
@@ -73,6 +74,26 @@ defmodule Hypatia.Rules.HonestCompletion do
     }
   end
 
+  # A mechanised proof library's test suite IS its proof check: a green
+  # `agda All.agda` / `lake build` / `coqc` / `idris2 --build` is the oracle
+  # (echo-types#271). Both halves are required — proof sources present AND a
+  # workflow that runs the checker — so an unchecked `.agda` file does not
+  # count as tests.
+  @proof_checker_invocation ~r/(?:^|[\s;&|(])(?:agda\s|lake\s+build|lean\s|coqc\s|dune\s+build|idris2\s+(?:--build|--check|-c)\b)/m
+
+  defp proof_suite_checked_in_ci?(repo_path) do
+    count_files(repo_path, ~w(.agda .lagda.md .lean .idr .v)) > 0 and
+      repo_path
+      |> Path.join(".github/workflows/*.{yml,yaml}")
+      |> Path.wildcard()
+      |> Enum.any?(fn wf ->
+        case File.read(wf) do
+          {:ok, text} -> Regex.match?(@proof_checker_invocation, text)
+          _ -> false
+        end
+      end)
+  end
+
   defp state_file_exists?(repo_path) do
     mr = Path.join(repo_path, ".machine_readable")
 
@@ -291,7 +312,8 @@ defmodule Hypatia.Rules.HonestCompletion do
 
     # No tests = big deduction
     findings =
-      if not evidence.has_tests_dir and evidence.test_files == 0 do
+      if not evidence.has_tests_dir and evidence.test_files == 0 and
+           not Map.get(evidence, :has_proof_suite, false) do
         [
           %{
             type: :no_tests,

lib/rules/pin_integrity.ex

@@ -277,7 +277,9 @@ defmodule Hypatia.Rules.PinIntegrity do
       # v3
       # Pinned to v1.2.3 — do not move
 
-  Returns `nil` when the comment makes no version claim.
+  Returns the first matching version without its `v` prefix. A bare major
+  such as `3` is ignored unless prefixed with `v`; dotted versions need no
+  prefix. Returns `nil` when there is no match or the input is not a string.
   """
   @spec claimed_version(String.t()) :: nil | String.t()
   def claimed_version(comment) when is_binary(comment) do
@@ -534,8 +536,15 @@ defmodule Hypatia.Rules.PinIntegrity do
   Relabel a pin's inline comment — but only when the comment **leads** with a
   version claim.
 
-  Both estate shapes are covered:
+  `version` is the replacement without a `v` prefix. The leading claim must
+  end at whitespace or the end of the comment. A rewritten comment has one
+  leading `#`; existing whitespace and trailing prose are preserved. Bare
+  claims with no leading whitespace gain a space after `#`. A `nil` version
+  leaves the comment unchanged.
 
+  With `version` set to `"4.38.0"`, these estate shapes are covered:
+
+      "v3"                                           -> "# v4.38.0"
       "# v3"                                        -> "# v4.38.0"
       "# v4.38.0 (4.38.1 blocked estate-wide; …)"   -> unchanged
 
@@ -554,14 +563,23 @@ defmodule Hypatia.Rules.PinIntegrity do
       if comment == "" or String.starts_with?(comment, "#"), do: comment, else: "# " <> comment
 
     body = String.replace_prefix(comment, "#", "")
+    hashed? = body != comment
 
     case Regex.run(~r/^\s*/, body) do
       [lead] ->
         trimmed = String.slice(body, String.length(lead)..-1//1)
 
+        # pin_sites/1 hands over the comment without its `#`; a bare claim
+        # comes back in the canonical `# vX` shape rather than as `#vX`.
+        # Promoted only after slicing, so the claim's first byte survives.
+        out_lead = if hashed? or lead != "", do: lead, else: " "
+
         case Regex.run(~r/^(v?\d+(?:\.\d+)*)(?:\s|$)/, trimmed) do
-          [_whole, claim] -> "#" <> lead <> String.replace_prefix(trimmed, claim, "v" <> version)
-          _ -> comment
+          [_whole, claim] ->
+            "#" <> out_lead <> String.replace_prefix(trimmed, claim, "v" <> version)
+
+          _ ->
+            comment
         end
 
       _ ->

lib/rules/pr_automerge.ex

@@ -191,8 +191,18 @@ defmodule Hypatia.Rules.PrAutomerge do
   @doc """
   Version deltas for every action this PR re-pins.
 
-  `status` is one of `:ok`, `:unresolved` (no source could place a version on
-  the refs) or `:conflict` (upstream tags and the PR body disagree). `source`
+  Each removed pin is paired with the first added pin for the same action
+  in the same file. Unpaired pins and unchanged refs are omitted. Returns a
+  flat list of maps with `:action`, `:file`, `:from`, `:to`, `:status`,
+  `:source` and `:major?`.
+
+  `resolution` supplies versions keyed by `{action, ref}`, then
+  `{action_base, ref}`, then `ref`, in that order of preference. If either
+  ref is unresolved, a matching claim from `body_claims/1` supplies both
+  versions; without a claim, both are `nil`.
+
+  `status` is one of `:ok`, `:unresolved` (no source supplied both versions)
+  or `:conflict` (resolved versions and the PR body disagree). `source`
   records which source produced the versions that were used, so a reviewer can
   see exactly what the decision rested on.
   """
@@ -383,12 +393,18 @@ defmodule Hypatia.Rules.PrAutomerge do
   @doc """
   Render a decision as the frozen merge-orchestration manifest.
 
-  Conforms to
-  `docs/design/merge-orchestration/schemas/decision-manifest.schema.json`;
-  the two contract invariants hold by construction — any denial sets
-  `safety: "flag"` and records a veto, and a `meta` change level can only
-  reach `arm_auto` through the `MGX-001` pin-only exemption, which the
-  actuator re-proves from the diff.
+  Takes the decision from `classify/2` and PR metadata with atom or string
+  keys. Includes pin deltas, the denylisted-site count and the current UTC
+  timestamp in ISO 8601 format. The author kind is always `"dependabot"`.
+
+  A decision with `safety: "flag"` gets a string-keyed Patch-Bridge veto,
+  plus a hypatia veto when its change level is `"meta"`, and
+  `"clamped_by" => "veto"`. Other safety values produce no vetoes and a
+  `nil` clamp. Safety and change level are copied from the decision;
+  this function does not validate the result against
+  `docs/design/merge-orchestration/schemas/decision-manifest.schema.json`.
+
+  Missing required keys in the decision or its delta maps raise `KeyError`.
   """
   @spec decision_manifest(map(), map()) :: map()
   def decision_manifest(decision, pr) do

lib/rules/rsr_conformance.ex

@@ -392,7 +392,9 @@ defmodule Hypatia.Rules.RsrConformance do
   # while the estate migrates. Hardcoding either name made whichever half had
   # not migrated unscoreable.
   defp present_mr(rel) do
-    fn repo -> if exists?(repo, Path.join(Hypatia.Paths.machine_tree(repo), rel)), do: :pass, else: :fail end
+    fn repo ->
+      if exists?(repo, Path.join(Hypatia.Paths.machine_tree(repo), rel)), do: :pass, else: :fail
+    end
   end
 
   defp absent(rel), do: fn repo -> if exists?(repo, rel), do: :fail, else: :pass end

lib/rules/structural_drift.ex

@@ -1099,7 +1099,8 @@ defmodule Hypatia.Rules.StructuralDrift do
               # its sibling `src/connectors/`). Only a reference that
               # resolves NOWHERE is genuine post-rename drift.
               MapSet.member?(real_basenames, dir) or
-                File.dir?(Path.join([repo_path, Path.dirname(rel), "src", dir]))
+                File.dir?(Path.join([repo_path, Path.dirname(rel), "src", dir])) or
+                not describes_a_local_src_tree?(repo_path, rel)
             end)
             |> Enum.map(fn stale_dir ->
               %{
@@ -1121,6 +1122,18 @@ defmodule Hypatia.Rules.StructuralDrift do
     end
   end
 
+  # A root-relative `src/<dir>/` can only be rename drift of a tree that HAS a
+  # `src/`: the repo root's, or the referencing doc's own directory's. In a
+  # repo with neither (standards: an estate-level repo whose specs and audits
+  # quote OTHER repos' layouts, e.g. the k9 spec's `src/tea/` example), the
+  # reference describes a foreign tree and cannot drift here. This was the
+  # single largest SD022 false-positive class — 34 baselined entries in
+  # standards alone (standards#945).
+  defp describes_a_local_src_tree?(repo_path, rel) do
+    File.dir?(Path.join(repo_path, "src")) or
+      File.dir?(Path.join([repo_path, Path.dirname(rel), "src"]))
+  end
+
   # Drop whole-line comments before matching. A commented-out example is not a
   # live claim about the tree.
   #

lib/rules/workflow_hardening.ex

@@ -267,9 +267,27 @@ defmodule Hypatia.Rules.WorkflowHardening do
   requires `contents: write`.
   """
   def performs_contents_write?(content) when is_binary(content) do
+    content = strip_foreign_pushes(content)
     Enum.any?(@contents_write_operations, &Regex.match?(&1, content))
   end
 
+  # `git push <remote>` where <remote> is a NAMED remote other than `origin`
+  # (`gitlab`, `codeberg`, `backup`, …). `contents: write` governs the job's
+  # GITHUB_TOKEN, i.e. pushes to THIS repository; a mirror push to another
+  # forge authenticates with its own SSH key or token and needs no grant.
+  # Flags before the remote (`--force`, `-u`, `--mirror`) are skipped. A bare
+  # `git push`, `git push origin …` and `git push "$REMOTE"` are all kept —
+  # the last because the remote cannot be known statically (standards#943).
+  @foreign_push ~r/\bgit\s+push\b(?:\s+-[-\w=]*)*\s+(?!origin\b)[A-Za-z][\w.-]*/
+
+  @doc """
+  Remove foreign-remote `git push` invocations, leaving any other operation on
+  the same line (`git push gitlab main && git push origin main`) intact.
+  """
+  def strip_foreign_pushes(content) when is_binary(content) do
+    Regex.replace(@foreign_push, content, "")
+  end
+
   @doc """
   Return true when at least one JOB declares its own `permissions:` block.
   A job-level block replaces the workflow-level one, so its presence means
@@ -602,7 +620,10 @@ defmodule Hypatia.Rules.WorkflowHardening do
 
       job_blocks
       |> Enum.flat_map(fn {job_id, line_no, body} ->
-        if Regex.match?(~r/^\s+timeout-minutes:/m, body) do
+        # A reusable-workflow caller (`job: uses: ./.github/workflows/x.yml`)
+        # cannot carry `timeout-minutes:` — GitHub rejects the key there; the
+        # called workflow's own jobs own their timeouts (standards#943).
+        if Regex.match?(~r/^\s+timeout-minutes:/m, body) or reusable_caller_job?(body) do
           []
         else
           [
@@ -1090,6 +1111,32 @@ defmodule Hypatia.Rules.WorkflowHardening do
     end
   end
 
+  @doc """
+  Return true when a job body (as produced by the job extractor, header line
+  first) has a JOB-LEVEL `uses:` key, i.e. it calls a reusable workflow.
+  Step-level `uses:` sits deeper (`- uses:` or under `- name:`) and is not
+  matched: only a `uses:` at the job's own key indentation counts.
+  """
+  def reusable_caller_job?(body) when is_binary(body) do
+    keys =
+      body
+      |> String.split("\n")
+      |> Enum.drop(1)
+      |> Enum.reject(&(String.trim(&1) == "" or String.starts_with?(String.trim(&1), "#")))
+
+    case keys do
+      [] ->
+        false
+
+      [first | _] ->
+        key_indent = indent_of(first)
+
+        Enum.any?(keys, fn line ->
+          indent_of(line) == key_indent and Regex.match?(~r/^\s*uses:\s*\S/, line)
+        end)
+    end
+  end
+
   # Extract every job definition from the workflow content. Returns
   # `[{job_id, line_no, body}]`. Approximate — assumes 2-space indent
   # under `jobs:`.
@@ -1098,7 +1145,9 @@ defmodule Hypatia.Rules.WorkflowHardening do
     in_jobs? = false
     jobs_indent = nil
 
-    {acc, _, _, _} =
+    # The final job is still in flight when the lines run out; it must be
+    # flushed too, or the last job of every workflow is never checked.
+    {acc, _, _, last} =
       Enum.with_index(lines, 1)
       |> Enum.reduce({[], in_jobs?, jobs_indent, nil}, fn
         {line, _no}, {acc, false, _ji, _current} ->
@@ -1119,14 +1168,14 @@ defmodule Hypatia.Rules.WorkflowHardening do
               {acc, true, nil, current}
           end
 
-        {line, _no}, {acc, true, jobs_indent, current} ->
+        {line, no}, {acc, true, jobs_indent, current} ->
           case Regex.run(~r/^(\s+)([a-zA-Z0-9_-]+):\s*$/, line) do
             [_, ws, job_id] ->
               this_indent = String.length(ws)
 
               if this_indent == jobs_indent do
                 acc2 = flush(acc, current)
-                {acc2, true, jobs_indent, {job_id, current_line_no(current, line), [line]}}
+                {acc2, true, jobs_indent, {job_id, no, [line]}}
               else
                 # Still in current job body
                 {acc, true, jobs_indent, append_line(current, line)}
@@ -1144,12 +1193,9 @@ defmodule Hypatia.Rules.WorkflowHardening do
           end
       end)
 
-    Enum.reverse(acc)
+    acc |> flush(last) |> Enum.reverse()
   end
 
-  defp current_line_no(nil, _line), do: 0
-  defp current_line_no({_id, no, _body}, _line), do: no
-
   defp append_line(nil, _), do: nil
   defp append_line({id, no, body}, line), do: {id, no, [line | body]}
 

scripts/sweeps/estate-pin-integrity.sh

@@ -119,6 +119,8 @@ relabel_comment() {
   local body="${comment#\#}"
   local lead="${body%%[![:space:]]*}"
   local trimmed="${body#"$lead"}"
+  # A bare claim (no `#`, no leading space) normalises to `# vX`, as relabel/2 does.
+  [ "$body" = "$comment" ] && [ -z "$lead" ] && lead=" "
   if printf '%s' "$trimmed" | grep -qE '^v?[0-9]+(\.[0-9]+)*([[:space:]]|$)'; then
     printf '%s%s' "#${lead}" \
       "$(printf '%s' "$trimmed" | sed -E "0,/^v?[0-9]+(\.[0-9]+)*/s//v${version}/")"

test/honest_completion_test.exs

@@ -84,6 +84,29 @@ defmodule Hypatia.Rules.HonestCompletionTest do
       assert Enum.any?(findings, &(&1.type == :no_tests))
     end
 
+    test "a CI-checked proof suite counts as tests (echo-types#271)" do
+      evidence = base_evidence(%{has_tests_dir: false, test_files: 0, has_proof_suite: true})
+      findings = HonestCompletion.generate_findings(%{}, evidence)
+      refute Enum.any?(findings, &(&1.type == :no_tests))
+    end
+
+    test "collect_evidence/1 needs proof sources AND a checker in CI" do
+      root = Path.join(System.tmp_dir!(), "hc_proof_#{System.unique_integer([:positive])}")
+      File.mkdir_p!(Path.join(root, "proofs/agda"))
+      File.write!(Path.join(root, "proofs/agda/All.agda"), "module All where\n")
+      refute HonestCompletion.collect_evidence(root).has_proof_suite
+
+      File.mkdir_p!(Path.join(root, ".github/workflows"))
+
+      File.write!(
+        Path.join(root, ".github/workflows/agda.yml"),
+        "jobs:\n  check:\n    steps:\n      - run: agda --safe proofs/agda/All.agda\n"
+      )
+
+      assert HonestCompletion.collect_evidence(root).has_proof_suite
+      File.rm_rf!(root)
+    end
+
     test "flags high TODO density" do
       claims = %{}
       evidence = base_evidence(%{todo_count: 100, source_files: 50})