From 38b44477795fb4ec727bde4f86d78641b6c19b54 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 24 Jun 2026 18:14:58 +0000 Subject: [PATCH] docs: record 2026-06-24 governance/CI/Hypatia work; track Hypatia handoff MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Reflects this session's non-proof infrastructure work in the living docs (no .v files touched, no proof-state change): - CHANGELOG.md: new "Governance, CI & security-scan infrastructure (2026-06-24)" entry — govdocs (#314), standards pin remediation (#315, now d135b05 via #316), Hypatia gate unblocked + 37 pre-existing findings handed off, stale PRs #310/#311 closed. - docs/governance/HYPATIA-HANDOFF.md: tracked record of the OPEN Hypatia triage (37 findings: 5 crit / 7 high / 25 med), reproduction steps, disposition rules, and the standards visibility patch — explicitly not-yet-fixed. - .machine_readable/6a2/STATE.a2ml: bump `updated`; append a delimited INFRA clause to last_action (proof narrative left intact). - docs/wikis/Home.md: link the new governance docs. Proof-roadmap docs (STATUS.adoc, ROADMAP.adoc, PROOF-STATUS.a2ml, PRESERVATION-*) deliberately left untouched — proof-cadence-owned. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_019g8rX8vRZ2HemGKagi6a71 --- .machine_readable/6a2/STATE.a2ml | 4 +- CHANGELOG.md | 24 ++++++++ docs/governance/HYPATIA-HANDOFF.md | 98 ++++++++++++++++++++++++++++++ docs/wikis/Home.md | 1 + 4 files changed, 125 insertions(+), 2 deletions(-) create mode 100644 docs/governance/HYPATIA-HANDOFF.md diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 4332be46..42348534 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -7,8 +7,8 @@ @state(version="2.0"): phase: "implementation" next_action: "Phase D slice 4 Phase 3b Stages 2-4 (#240/#241/#242): Stage 1 (both 1a + 1b) complete. Stages 2-4 sequenced per the owner-approved 4-stage plan: Stage 2 (#240) ELam annotation extension — independent of Stage 1, ships when prioritised; Stage 3 (#241) CPS + relaxed Phase 3b — blocked on Stage 2; Stage 4 (#242) compound non-linear + unconditional preservation_l2 — blocked on Stage 3. Stage 4's destination collapses Stage 1b's three preconditions (P1 = tfuneff_lambda_free, P2 = regions_introduced_by ⊆ R_in_v, P3 = expr_closed_below 0 v) once typing-derived closure invariants land. Anti-patterns to refuse (per CLAUDE.md owner directive): no `Admitted`; no touching `Semantics.v` / `Typing.v` / `Counterexample.v`; no closure of residual `Semantics_L1.v` admits — strictly NEW infrastructure orthogonal to legacy. Coqc 8.18.0 is the only authority." -last_action: "Proof + stdlib wave 2026-06-01 → 02 landed (13 PRs): canonical-forms L1 modality-polymorphic (#274, P43, 7 lemmas axiom-free, prerequisite for progress_l1/P42); Print Assumptions audit framework across L1 + L3 keystones (#270, closes P10/P32); step_pop_disjoint_from_type_l1 stated + EASY cases Qed-closed (#280, P06, HARD cases blocked on #240/#241/#242); Rust↔Coq is_linear_ty truth-table mechanical assertion (#273, P28); OwnershipKind from_byte/to_byte round-trip (#277, P59, typed-wasm ADR-0002 carrier handshake); 4 stdlib DB-theory additions — Transactions as linear scopes (#275, D04), Allen's interval algebra (#272, D11), MessageHandle as linear typestate (#279, D17), monoidal aggregates (#281, D18); doc truth-restore + banned-preservation framing buried (#263); cluster-D L3/L4 status meander (#278); Track C panic-attack triage (#271); coq-build noble apt CI fix (#282, unblocks ~5 PRs); R5b standards SHA bump (#276). Plus CHANGELOG sync (#283). Build oracle clean across all 12 .v files. Print Assumptions: canonical_*_l1_m + most new lemmas zero-axiom; expected residuals (preservation_l1, region_liveness_at_split_l1_gen, region_shrink_preserves_typing_l1_gen_m) tracked. Stages 2-4 (#240/#241/#242) still un-touched. Wiki Proof-status.md refreshed 2026-06-02." -updated: 2026-06-02T13:30:00Z +last_action: "Proof + stdlib wave 2026-06-01 → 02 landed (13 PRs): canonical-forms L1 modality-polymorphic (#274, P43, 7 lemmas axiom-free, prerequisite for progress_l1/P42); Print Assumptions audit framework across L1 + L3 keystones (#270, closes P10/P32); step_pop_disjoint_from_type_l1 stated + EASY cases Qed-closed (#280, P06, HARD cases blocked on #240/#241/#242); Rust↔Coq is_linear_ty truth-table mechanical assertion (#273, P28); OwnershipKind from_byte/to_byte round-trip (#277, P59, typed-wasm ADR-0002 carrier handshake); 4 stdlib DB-theory additions — Transactions as linear scopes (#275, D04), Allen's interval algebra (#272, D11), MessageHandle as linear typestate (#279, D17), monoidal aggregates (#281, D18); doc truth-restore + banned-preservation framing buried (#263); cluster-D L3/L4 status meander (#278); Track C panic-attack triage (#271); coq-build noble apt CI fix (#282, unblocks ~5 PRs); R5b standards SHA bump (#276). Plus CHANGELOG sync (#283). Build oracle clean across all 12 .v files. Print Assumptions: canonical_*_l1_m + most new lemmas zero-axiom; expected residuals (preservation_l1, region_liveness_at_split_l1_gen, region_shrink_preserves_typing_l1_gen_m) tracked. Stages 2-4 (#240/#241/#242) still un-touched. Wiki Proof-status.md refreshed 2026-06-02. | INFRA (2026-06-24, non-proof track): governance docs landed (#314 — CODEOWNERS/GOVERNANCE.adoc/MAINTAINERS.adoc); standards reusable-workflow pins remediated (#315) and current at d135b05 (#316); Hypatia neurosymbolic gate now active and reporting 37 pre-existing findings (5 crit / 7 high / 25 med) — triage handed off (docs/governance/HYPATIA-HANDOFF.md), standards visibility patch drafted-not-applied. No .v files touched; no proof-state change." +updated: 2026-06-24T18:13:15Z @directive(source="owner", date="2026-05-27", canonical="CLAUDE.md"): # Captured durable directive — preservation work is the four-layer redesign, diff --git a/CHANGELOG.md b/CHANGELOG.md index 3fdfa995..4c82233b 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,6 +7,30 @@ All notable changes to Ephapax are documented here. ## [Unreleased] +### Governance, CI & security-scan infrastructure (2026-06-24) + +- **Governance model formalised** (PR #314): added `.github/CODEOWNERS` + (review routing, sole-maintainer model), `GOVERNANCE.adoc`, and + `MAINTAINERS.adoc`. Salvaged from the closed estate-standardization + branch onto a clean base; prose headers normalised to `CC-BY-SA-4.0`. +- **`standards` reusable-workflow pins remediated** (PR #315): re-pinned + `governance.yml` / `hypatia-scan.yml` / `scorecard.yml` away from + `5a93d9d57cc0` — a ref that is **not** an ancestor of `standards` HEAD, + which broke `governance / Check Workflow Staleness` and made the Hypatia + reusable workflow reference a dead `actions/cache` SHA — to a published + HEAD. Subsequently bumped to the current `d135b05…` (PR #316). +- **Hypatia neurosymbolic scan unblocked** — with the pin fixed, the + `scan / Hypatia Neurosymbolic Analysis` gate now runs to completion + instead of dying at "Prepare all required actions". It reports **37 + pre-existing findings** (5 critical, 7 high, 25 medium) — repo debt the + broken pin had been masking, **not** introduced here. Triage + fix is + **handed off** (see `docs/governance/HYPATIA-HANDOFF.md`); a visibility + patch for `standards`' `hypatia-scan-reusable.yml` (publish findings on + failure rather than aborting opaquely under `bash -e`) is **drafted but + not yet applied**. +- **Stale PRs closed**: #310 (disjoint history; reintroduced fenced legacy + preservation work) and #311 (superseded — features already on `main`). + ### Proof + stdlib wave (2026-06-01 → 2026-06-02) - **P43 — canonical-forms L1 modality-polymorphic** (PR #274): port diff --git a/docs/governance/HYPATIA-HANDOFF.md b/docs/governance/HYPATIA-HANDOFF.md new file mode 100644 index 00000000..1765a7da --- /dev/null +++ b/docs/governance/HYPATIA-HANDOFF.md @@ -0,0 +1,98 @@ + + + + +# Hypatia findings — outstanding triage handoff (2026-06-24) + +> **Status: OPEN.** The Hypatia neurosymbolic gate is now active and reports +> **37 pre-existing findings (5 critical, 7 high, 25 medium)** on ephapax. +> They are **not** fixed — triage + fix is the work below. These are +> pre-existing repo debt that a broken CI pin had been masking, **not** +> introduced by the change that unmasked them. + +## How this surfaced + +The `scan / Hypatia Neurosymbolic Analysis` gate used to die at "Prepare all +required actions" because the three `hyperpolymath/standards` reusable +workflows were pinned to `5a93d9d57cc0`, a ref that is **not** an ancestor of +`standards` HEAD; that broken pin also transitively referenced a dead +`actions/cache` SHA. PR #315 re-pinned to a published HEAD (later bumped to +`d135b05…` in #316), which let the scan actually run — and report the 37 +findings that were previously invisible. + +> **Two milestones are not one:** "the workflow now *runs*" and "the workflow +> now *passes*" are different. Fixing the pin achieved the first; the second +> is this document. + +## Why this is handed off (cannot be run in the remote sandbox) + +The engine is an Elixir escript in `github.com/hyperpolymath/hypatia`. Building +it needs `mix deps.get`, which fetches from **`repo.hex.pm`** — and the remote +session's egress policy returns `403` for the Hex registry (npm/PyPI/crates/Go +are allowed; Hex is not). So the engine must be run on a host where Hex is +reachable (a local machine, or a CI runner), **or** the environment's network +policy must be widened to allow `repo.hex.pm` + `builds.hex.pm`. + +## Task 1 — produce the exact findings + +```bash +git clone https://github.com/hyperpolymath/hypatia.git ~/hypatia +cd ~/hypatia +mix local.hex --force && mix local.rebar --force +mix deps.get +mix escript.build +# Run with NO GITHUB_TOKEN to match CI (CI had none, so the dependabot / +# secret-scanning / code-scanning alert rules emit nothing — the 37 are +# file-based rules): +HYPATIA_FORMAT=json ./hypatia-cli.sh scan /path/to/ephapax > hypatia-findings.json +jq '[.[].severity] | group_by(.) | map({(.[0]): length}) | add' hypatia-findings.json +``` + +- Rules are pure functions in `lib/rules/*.ex`; `scan` runs `@all_rule_modules`. +- With no token the 37 are file-based — most likely from `honest_completion`, + `proof_obligation`, `disambiguation_rules`, `code_safety`, `root_hygiene`, + `supply_chain`, `structural_drift`, `workflow_audit`, `workflow_hardening`, + `cicd_rules`, `scorecard_compliance`. (A local token may surface MORE than + 37 — run without one to reproduce the gate's set.) +- Severities depend on the pinned `standards` reusable-workflow version + (currently `d135b05…`); the 5/7/25 split was observed on the first + unblocked run and may shift slightly with the engine version. + +## Task 2 — triage + fix + +1. Group by rule × severity. Fix order: **5 critical → 7 high → 25 medium**. +2. Per finding: true positive → fix in code/docs; false positive / accepted → + add a justified `rule:path` line to `.hypatia-ignore` (matched `grep -qxF`), + or enter it in `.hypatia-baseline.json` (schema in `standards` + `.machine_readable/hypatia-baseline.schema.json`). +3. **Proof / claim findings** (`honest_completion`, `proof_obligation`): fix by + making *claims* honest (docs/metadata), **never** by editing or force-closing + the fenced legacy proofs. Per `CLAUDE.md`: do not touch + `formal/Semantics.v` `Theorem preservation` (provably false; deliberately + `Admitted`), `formal/Typing.v`, or `formal/Counterexample.v`. +4. **`disambiguation_rules`** findings: ensure the ephapax-vs-AffineScript + disambiguation markers are present per `CLAUDE.md`. +5. Re-run the scan until `critical = 0` (ideally total within policy). Open a + PR with a triage table: *finding → disposition → fix*. + +## Task 3 — make the gate non-opaque (in `hyperpolymath/standards`) + +The gate fails **opaquely**: in `standards`' +`.github/workflows/hypatia-scan-reusable.yml` the scan runs under `bash -e`, +and `hypatia-cli.sh scan` **exits 1 when findings exist**, so the step aborts +*before* the (already-present) `upload-artifact` step and the "warn but don't +fail" critical-check ever run. Net effect: a hard job failure emitting only a +severity count, no detail. + +**Fix (in `standards`):** wrap the scan in `set +e` + capture the rc; **always** +upload `hypatia-findings.json` (`if: always()`); write a findings table to +`$GITHUB_STEP_SUMMARY`; enforce the gate in a final dedicated step. Pin +`actions/upload-artifact` by SHA (same supply-chain lesson as PR #315). A full +suggested patch was drafted in-session (not yet applied). + +## Guardrails (from `CLAUDE.md`) + +- This is `hyperpolymath/ephapax` (not AffineScript). Signed commits. +- Code/config = `MPL-2.0`; prose (`.md`/`.adoc`) = `CC-BY-SA-4.0`. +- Never touch the fenced legacy preservation proof or `Typing.v` / + `Counterexample.v`. Fix proof/claim findings by aligning claims to reality. diff --git a/docs/wikis/Home.md b/docs/wikis/Home.md index cba6d5b5..28a32688 100644 --- a/docs/wikis/Home.md +++ b/docs/wikis/Home.md @@ -77,6 +77,7 @@ The four layers and their current state: ## Governance +- **Governance model**: sole-maintainer — [GOVERNANCE.adoc](https://github.com/hyperpolymath/ephapax/blob/main/GOVERNANCE.adoc), [MAINTAINERS.adoc](https://github.com/hyperpolymath/ephapax/blob/main/MAINTAINERS.adoc), [CODEOWNERS](https://github.com/hyperpolymath/ephapax/blob/main/.github/CODEOWNERS) - **Licence**: MPL-2.0 - **Machine-readable state**: [`.machine_readable/6a2/`](https://github.com/hyperpolymath/ephapax/tree/main/.machine_readable/6a2/) - **Contractiles**: 6-verb governance in [`.machine_readable/contractiles/`](https://github.com/hyperpolymath/ephapax/tree/main/.machine_readable/contractiles/)