One parsed workflow model (#971); prove RE001's egress decision and the KYAML alias budget

.claude/CLAUDE.md

@@ -13,7 +13,7 @@ Hypatia is the neurosymbolic CI/CD intelligence layer for the hyperpolymath ecos
 ## Architecture
 
 ```
-Hypatia                       # 150 Elixir source files under lib/ (recursive tree count, 2026-11-04)
+Hypatia                       # 155 Elixir source files under lib/ (recursive tree count, 2026-11-09)
 ├── Elixir pipeline          # core: pattern analysis, dispatch, learning
 ├── Merge orchestration       # 12 modules — leases, ledger, ticker (largest subsystem)
 ├── Kin subsystem             # 6 modules — contingency, arbiter, gate, watchdog
@@ -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 |
+| `Egress.idr` | RE001's decision on egress declarations (standards ADR-009): `Clean` is decidable (`decClean`); an audit hardener never passes a block claim; a declaration lists exactly the secrets read; a run-time key is never declared. Mirror: `test/egress_decision_mirror_test.exs` |
 
 **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

.github/workflows/ci.yml

@@ -357,6 +357,9 @@ jobs:
             test/rules/audit_prevention_test.exs \
             test/security_errors_test.exs \
             test/research_extensions_test.exs \
+            test/research_extensions_equivalence_test.exs \
+            test/workflow_test.exs \
+            test/egress_decision_mirror_test.exs \
             test/deed_test.exs \
             test/kyaml_test.exs \
             test/kyaml_conformance_test.exs

CHANGELOG.adoc

@@ -31,6 +31,105 @@ a comment keeps its `run:`. WH014 reads each job's steps through the same
 reader. On the hypatia, echidna and standards trees, WH013, WH014 and RE001
 report exactly what they did before.
 
+==== One parsed workflow model; RE001 and RE002 read it (#971) (2026-11-09)
+
+`Hypatia.Workflow` is #971's model: each workflow is parsed once by
+`Hypatia.Kyaml`, the port of kyq's KYAML reader, into `Workflow`, `Job` and
+`Step` records. Scalars a rule compares (`uses`, `run`, `if`) are their YAML
+values, folded and unquoted; mappings a rule walks (`env`, `with`) keep their
+nodes, so every value keeps its source line. RE001 and RE002 now read the
+model instead of scanning lines (WH013 and WH014 follow, and
+`Hypatia.WorkflowYaml` with them):
+
+* **Layout no longer changes a finding.** Block or flow YAML, plain or quoted
+  keys, literal or folded `run:` blocks and aliases all read the same. A new
+  equivalence harness (`test/research_extensions_equivalence_test.exs`)
+  renders seeded random workflows four ways and requires the same findings
+  from each. Run against the old line-based RE001, it fails on its seventh
+  case.
+* **An unreadable workflow is reported, not guessed at.** A workflow the
+  reader refuses (a `<<` merge key, which GitHub also refuses; aliases past
+  kyq's node budget; any other KYAML error) gets a `:warn` RE001 finding at
+  the error, if it names `secrets`. Its deed declarations are not reported
+  stale.
+* **The three post-merge review threads on #975 are closed by construction,**
+  each with a test that fails on the line reader: `<<: [*defaults]` is
+  refused and reported, not misplaced; text in a `name: |` block beside the
+  hardener is not its input, so an audit hardener no longer passes for a
+  block one; a folded `egress-policy: >-` is read as its value, and a
+  literal block is trimmed as the action's `core.getInput` trims it.
+* **Declared endpoints are checked** against the workflow (`:warn`): a host
+  outside GitHub that a step names literally (a URL or a `git@host:` remote,
+  shell comments aside) must be covered by the job's `:endpoints`, and
+  harden-runner's `allowed-endpoints`, when listed, must agree with them.
+  An allowed entry written with an expression
+  (`${{ secrets.SMTP_HOST }}:465`) names its host only at run time and is not
+  compared, and GitHub's own hosts are outside the comparison on both sides.
+  `Hypatia.Deed.egress_declarations/1` now returns `:endpoints`.
+* **RE002** finds harden-runner the way RE001 does: a real step, the owner in
+  any case, its own `with: egress-policy`. A step with no policy runs
+  harden-runner's default, `audit`, and is now reported. The trigger is a
+  `push` or `release` key of `on:`, not a `push:` anywhere in the file.
+* **Review fixes on #1036**, each with a test that fails without it. The
+  endpoint comparison no longer takes `notgithubusercontent.com` for a
+  GitHub host; reads a URL's scheme in any case (`HTTPS://`); compares a
+  literal IPv4 host (loopback aside; a single-label name such as
+  `localhost` or a service container is still not egress); treats a URL
+  port written as an expression as unknown instead of the scheme's default;
+  reads `git@gitlab.com:123team/x.git` as a remote but
+  `owner@example.com: failed` as prose; ignores a `#` inside shell quotes
+  (`git commit -m "fix #12" && git push …`) when looking for comments;
+  keeps the literal host of an allowed entry whose port is an expression;
+  and holds an allowed entry with no port (every port) to a declaration
+  with none, and a declaration with no port to an allowed entry with none.
+  Hosts are now also read from the job's and the workflow's `env:` (a
+  value is not counted where the job or the step sets the same
+  variable again), but not from a
+  step's `name`, `id` or `if`; database and broker URLs
+  (`postgres://`, `rediss://`, `mongodb+srv://`, AMQP, MQTT, LDAP, SMTP,
+  SFTP) are read at their scheme's default port; and a `#` after a shell
+  control operator (`done;# …`) opens a comment. `scan/2` parses each
+  workflow once for RE001 and RE002. RE002 skips a job whose `if:` admits only events other than
+  `push` and `release`, and reports a workflow the reader refuses if it
+  names harden-runner (the line reader used to find its `audit` there).
+  A job or step read through an alias is reported at the alias again, not
+  at the anchor. On the six repositories above, RE001 and RE002 give the
+  same 6 findings before and after.
+
+The `code_safety/elixir_atom_from_user` description was backwards: it named
+`String.to_existing_atom` as the danger. It now names `String.to_atom`. The
+pattern was always right.
+
+Measured on 2026-11-09 against the main branches of hyperpolymath/hypatia,
+rsr-template-repo, choreographic-types and mathesis, and
+metadatastician/standards and kyq: RE001 and RE002 give the same 6 findings
+as the line reader did. Two defects in the endpoint comparison surfaced only
+there and are fixed with tests: an `allowed-endpoints` entry written with an
+expression crashed it (hypatia's own `push-email-notify.yml`), and a deed
+listing GitHub hosts drew 12 false findings on hypatia.
+
+The decision and the alias budget are proved, and the code is held to the
+proofs (verification/PROOF-STATUS.adoc, "Egress declarations and the KYAML
+reader"):
+
+* `src/Hypatia/ABI/Egress.idr` models RE001's acceptance of a job as a
+  decidable type and proves that an audit hardener never satisfies a block
+  claim, that a declaration lists exactly the secrets read, and that a key
+  computed at run time is never declared. Three expected rejections and a
+  positive control run in `scripts/check-verdicts.sh`.
+  `test/egress_decision_mirror_test.exs` runs RE001 on all 280 cases of a
+  small domain and requires it to agree with the proved decision.
+* `verification/proofs/idris2/KyamlBudget.idr` models `within_budget?/2`
+  and proves that, on a document in which no alias names another alias
+  (which the reader guarantees), it passes exactly the documents whose
+  expanded size is within the limit, in at most 2 · (limit + 1) + 2 calls
+  of `count/3` however far the aliases expand. The bound counts calls, not
+  the work inside one or allocation. `test/kyaml_test.exs` holds the
+  Elixir count to the model on 154 trees at every limit.
+
+The reader as a whole is tested, not proved, and endpoints are not
+modelled; both are recorded as such.
+
 ==== RE001 accepts a deed egress declaration; the job token no longer counts (2026-10-27)
 
 The estate-wide decision on `step-security/harden-runner` (standards ADR-009) is

docs/rules/logtalk-migration.adoc

@@ -583,16 +583,13 @@ evidence, not a standards-gate receipt.
 [[proofing]]
 == Proofing: policy, grades, and exact statuses
 
-Proofing follows hyperpolymath/mathesis'
-`estate-mathematical-architecture` (§§5–6) for grades and
-metadatastician/standards `3-practice/PROOF-POLICY.adoc` for evidence
-discipline; everything else follows the standards repo. In Mathesis'
-ladder, *Grade 3* means the statement is formulated in Agda and
-type-checks under the strict profile; Grade 2 additionally requires
-translation into independent foundational system(s); Grade 1
-additionally requires those witnesses to compile in headless isolated
-CI through verified checker APIs. Statuses are recorded exactly
-(Open / Claimed / AGDA-PENDING / Grade 3 / …), never as a percentage,
+Proofing follows metadatastician/standards `3-practice/PROOF-POLICY.adoc`:
+§5 for status tokens and §8 for Proof Witness Grades (owner ruling
+2026-11-04, which supersedes the ladder of the Mathesis architecture
+brief). `PWG-3` means the Agda proof is checked under the §2.1
+invocation; `PWG-2i` adds one counted Rocq or Lean recheck leg and
+`PWG-2ii` both; `PWG-1` adds a current per-commit receipt for every
+witness. Statuses and grades are recorded exactly, never as a percentage,
 and a checked model never silently becomes a runtime-refinement or
 reconciliation claim.
 
@@ -609,15 +606,15 @@ exactly
 |`verification/proofs/agda/LogtalkMigration.agda`
 (`categoriesAgree`, `severitiesAgree`, `autoFixableAgrees`,
 `fixPresenceAgrees`, `prevention*`, `catchAll*Low`)
-|*Grade 3 — AGDA-VERIFIED.* Receipt recorded in
+|*PROVEN, `PWG-3`.* Receipt recorded in
 `verification/PROOF-STATUS.adoc`: official pinned Agda 2.8.0.2 Linux
 release (builtins only, no stdlib), invocation `agda --safe
 --without-K --cubical-compatible LogtalkMigration.agda`, success in
 Verify Proofs run 41328302925, job 124912804344, at commit 4018290eaa3265b82209e2a45b6917a4bb0a0331;
 source SHA-256
 bbd18e2747c84e2eda7ff5a778a2df7f8960a1ef47b1c253f316b9d97b9902a0.
 The `agda strict-profile check` job fails hard (never skips) on every
-relevant change. No Grade 2/1, Rocq/Lean reconciliation, or Elixir
+relevant change. No `PWG-2i`, `PWG-2ii` or `PWG-1`, Rocq/Lean reconciliation, or Elixir
 runtime-refinement claim is made.
 
 |VeriSimDB connector field preservation
@@ -706,7 +703,7 @@ sibling repositories from this branch):
   coordinated. ✓ (landing: siblings)
 * Repository guard against new active `.lgt` files / Logtalk output
   settings, exact-path shrink-only allowlist, wired into CI. ✓
-* Proofing graded honestly: finite correspondence at Mathesis
-  *Grade 3 / AGDA-VERIFIED* on the recorded strict-profile Agda
+* Proofing graded honestly: finite correspondence PROVEN at
+  `PWG-3` on the recorded strict-profile Agda
   receipt; Idris statement supersession recorded and re-checked; no
   claim inflated beyond its evidence. ✓

docs/rules/migration/echidna-security-learning-issue.md

@@ -33,7 +33,7 @@ Deliberate divergences, all ledgered in Hypatia `docs/rules/logtalk-migration.ad
 - `BranchProtectionID` prevention is `scorecard-enforcer.yml` (long-standing Elixir value), not the Logtalk `branch-protection-enforcer.yml`; `CodeReviewID` gained a prevention mapping with no Logtalk counterpart.
 - Wholly unknown alert ids get severity `:info` in Elixir rather than the Logtalk catch-all `low`; all 18 known ids agree exactly.
 
-Proof status, stated exactly: the finite table correspondence is modelled in Hypatia `verification/proofs/agda/LogtalkMigration.agda` and is **Mathesis Grade 3 / AGDA-VERIFIED** on a strict-profile receipt (Agda 2.8.0.2, `agda --safe --without-K --cubical-compatible`, Hypatia Verify Proofs run 41328302925 at commit 4018290eaa3265b82209e2a45b6917a4bb0a0331; full receipt in Hypatia `verification/PROOF-STATUS.adoc`). Elixir behaviour is pinned by ExUnit tests in the same PR's CI. The Agda model grades the finite table correspondence only — no runtime-refinement or Grade 2/1 claim is being sold here.
+Proof status, stated exactly: the finite table correspondence is modelled in Hypatia `verification/proofs/agda/LogtalkMigration.agda` and is **PROVEN, `PWG-3`** (metadatastician/standards `3-practice/PROOF-POLICY.adoc` §5 and §8) on a strict-profile receipt (Agda 2.8.0.2, `agda --safe --without-K --cubical-compatible`, Hypatia Verify Proofs run 41328302925 at commit 4018290eaa3265b82209e2a45b6917a4bb0a0331; full receipt in Hypatia `verification/PROOF-STATUS.adoc`). Elixir behaviour is pinned by ExUnit tests in the same PR's CI. The Agda model grades the finite table correspondence only — no runtime-refinement, `PWG-2i`, `PWG-2ii` or `PWG-1` claim is being sold here.
 
 ## Requested changes in ECHIDNA
 

lib/hypatia/deed.ex

@@ -87,7 +87,7 @@ defmodule Hypatia.Deed do
   The jobs declared in the repo deed's `(egress …)` clause.
 
   Returns `{:ok, deed_file, jobs}` where each job is
-  `%{workflow: path, job: id, secrets: MapSet, enforcement: name}`, `:none` when
+  `%{workflow: path, job: id, secrets: MapSet, endpoints: [string], enforcement: name}`, `:none` when
   the repo has no deed, or `{:error, deed_file, reason}` when the deed or the clause cannot be
   read. A deed without the clause declares nothing: `{:ok, deed_file, []}`.
   """
@@ -206,7 +206,14 @@ defmodule Hypatia.Deed do
              true <- Enum.all?(endpoints, &valid_endpoint?(&1, secrets)),
              {:symbol, enf} when enf in @enforcement <- by_key["enforcement"],
              true <- reason_ok?(by_key["reason"]) do
-          job = %{workflow: workflow, job: job, secrets: MapSet.new(secrets), enforcement: enf}
+          job = %{
+            workflow: workflow,
+            job: job,
+            secrets: MapSet.new(secrets),
+            endpoints: endpoints,
+            enforcement: enf
+          }
+
           {:cont, {:ok, [job | jobs]}}
         else
           _ ->