Skip to content

Commit c48fbde

Browse files
docs: record 2026-06-24 governance/CI/Hypatia work + track Hypatia handoff (#319)
## Summary Housekeeping pass to bring the living docs current with this session's **non-proof** infrastructure work, and to version-control the outstanding Hypatia triage. **No `.v` files touched; no proof-state change.** ## Changes - **`CHANGELOG.md`** — new `### Governance, CI & security-scan infrastructure (2026-06-24)` entry under `[Unreleased]`: govdocs (#314), `standards` pin remediation (#315, now `d135b05…` via #316), the Hypatia gate getting unblocked and surfacing **37 pre-existing findings** (5 critical / 7 high / 25 medium), and the closure of stale PRs #310/#311. - **`docs/governance/HYPATIA-HANDOFF.md`** (new) — a tracked record of the **OPEN** Hypatia triage: how it surfaced, why the engine can't run in the remote sandbox (Hex registry blocked by egress policy), reproduction steps, disposition rules (incl. the `CLAUDE.md` fences), and the drafted `standards` visibility patch. Honestly framed as **not yet fixed**. - **`.machine_readable/6a2/STATE.a2ml`** — bumped `updated:`; appended a clearly-delimited `INFRA (…non-proof track)` clause to `last_action`. The Phase-D proof narrative is left intact. - **`docs/wikis/Home.md`** — linked the new governance docs (`GOVERNANCE.adoc` / `MAINTAINERS.adoc` / `CODEOWNERS`). ## Deliberately NOT touched `STATUS.adoc`, `ROADMAP.adoc`, `formal/PROOF-STATUS.a2ml`, `formal/PRESERVATION-DESIGN.md`, `formal/PRESERVATION-HANDOFF.md`, `CLAUDE.md`, `0-AI-MANIFEST.a2ml` — these are proof-cadence-owned / fenced; adding CI/governance content would muddle the proof narrative, and they carry no incorrect information without it. Happy to add infra notes there too if you'd prefer. ## Honesty notes - The 37 findings are **pre-existing repo debt**, surfaced (not caused) by fixing the broken pin; they are **not fixed** here — triage is handed off. - The `standards` visibility patch is **drafted, not applied**. - `#316/#317/#318` (further pin bump, licence pass, push-email workflow) landed on `main` *after* my #315 and are **not** attributed to this session — only referenced where factually relevant. 🤖 Generated with [Claude Code](https://claude.com/claude-code) --- _Generated by [Claude Code](https://claude.ai/code/session_019g8rX8vRZ2HemGKagi6a71)_ Co-authored-by: Claude <noreply@anthropic.com>
1 parent c8fb5cf commit c48fbde

4 files changed

Lines changed: 125 additions & 2 deletions

File tree

.machine_readable/6a2/STATE.a2ml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,8 +7,8 @@
77
@state(version="2.0"):
88
phase: "implementation"
99
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."
10-
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."
11-
updated: 2026-06-02T13:30:00Z
10+
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."
11+
updated: 2026-06-24T18:13:15Z
1212

1313
@directive(source="owner", date="2026-05-27", canonical="CLAUDE.md"):
1414
# Captured durable directive — preservation work is the four-layer redesign,

CHANGELOG.md

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,30 @@ All notable changes to Ephapax are documented here.
77

88
## [Unreleased]
99

10+
### Governance, CI & security-scan infrastructure (2026-06-24)
11+
12+
- **Governance model formalised** (PR #314): added `.github/CODEOWNERS`
13+
(review routing, sole-maintainer model), `GOVERNANCE.adoc`, and
14+
`MAINTAINERS.adoc`. Salvaged from the closed estate-standardization
15+
branch onto a clean base; prose headers normalised to `CC-BY-SA-4.0`.
16+
- **`standards` reusable-workflow pins remediated** (PR #315): re-pinned
17+
`governance.yml` / `hypatia-scan.yml` / `scorecard.yml` away from
18+
`5a93d9d57cc0` — a ref that is **not** an ancestor of `standards` HEAD,
19+
which broke `governance / Check Workflow Staleness` and made the Hypatia
20+
reusable workflow reference a dead `actions/cache` SHA — to a published
21+
HEAD. Subsequently bumped to the current `d135b05…` (PR #316).
22+
- **Hypatia neurosymbolic scan unblocked** — with the pin fixed, the
23+
`scan / Hypatia Neurosymbolic Analysis` gate now runs to completion
24+
instead of dying at "Prepare all required actions". It reports **37
25+
pre-existing findings** (5 critical, 7 high, 25 medium) — repo debt the
26+
broken pin had been masking, **not** introduced here. Triage + fix is
27+
**handed off** (see `docs/governance/HYPATIA-HANDOFF.md`); a visibility
28+
patch for `standards`' `hypatia-scan-reusable.yml` (publish findings on
29+
failure rather than aborting opaquely under `bash -e`) is **drafted but
30+
not yet applied**.
31+
- **Stale PRs closed**: #310 (disjoint history; reintroduced fenced legacy
32+
preservation work) and #311 (superseded — features already on `main`).
33+
1034
### Proof + stdlib wave (2026-06-01 → 2026-06-02)
1135

1236
- **P43 — canonical-forms L1 modality-polymorphic** (PR #274): port

docs/governance/HYPATIA-HANDOFF.md

Lines changed: 98 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,98 @@
1+
<!-- SPDX-License-Identifier: CC-BY-SA-4.0 -->
2+
<!-- Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> -->
3+
<!-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> -->
4+
5+
# Hypatia findings — outstanding triage handoff (2026-06-24)
6+
7+
> **Status: OPEN.** The Hypatia neurosymbolic gate is now active and reports
8+
> **37 pre-existing findings (5 critical, 7 high, 25 medium)** on ephapax.
9+
> They are **not** fixed — triage + fix is the work below. These are
10+
> pre-existing repo debt that a broken CI pin had been masking, **not**
11+
> introduced by the change that unmasked them.
12+
13+
## How this surfaced
14+
15+
The `scan / Hypatia Neurosymbolic Analysis` gate used to die at "Prepare all
16+
required actions" because the three `hyperpolymath/standards` reusable
17+
workflows were pinned to `5a93d9d57cc0`, a ref that is **not** an ancestor of
18+
`standards` HEAD; that broken pin also transitively referenced a dead
19+
`actions/cache` SHA. PR #315 re-pinned to a published HEAD (later bumped to
20+
`d135b05…` in #316), which let the scan actually run — and report the 37
21+
findings that were previously invisible.
22+
23+
> **Two milestones are not one:** "the workflow now *runs*" and "the workflow
24+
> now *passes*" are different. Fixing the pin achieved the first; the second
25+
> is this document.
26+
27+
## Why this is handed off (cannot be run in the remote sandbox)
28+
29+
The engine is an Elixir escript in `github.com/hyperpolymath/hypatia`. Building
30+
it needs `mix deps.get`, which fetches from **`repo.hex.pm`** — and the remote
31+
session's egress policy returns `403` for the Hex registry (npm/PyPI/crates/Go
32+
are allowed; Hex is not). So the engine must be run on a host where Hex is
33+
reachable (a local machine, or a CI runner), **or** the environment's network
34+
policy must be widened to allow `repo.hex.pm` + `builds.hex.pm`.
35+
36+
## Task 1 — produce the exact findings
37+
38+
```bash
39+
git clone https://github.com/hyperpolymath/hypatia.git ~/hypatia
40+
cd ~/hypatia
41+
mix local.hex --force && mix local.rebar --force
42+
mix deps.get
43+
mix escript.build
44+
# Run with NO GITHUB_TOKEN to match CI (CI had none, so the dependabot /
45+
# secret-scanning / code-scanning alert rules emit nothing — the 37 are
46+
# file-based rules):
47+
HYPATIA_FORMAT=json ./hypatia-cli.sh scan /path/to/ephapax > hypatia-findings.json
48+
jq '[.[].severity] | group_by(.) | map({(.[0]): length}) | add' hypatia-findings.json
49+
```
50+
51+
- Rules are pure functions in `lib/rules/*.ex`; `scan` runs `@all_rule_modules`.
52+
- With no token the 37 are file-based — most likely from `honest_completion`,
53+
`proof_obligation`, `disambiguation_rules`, `code_safety`, `root_hygiene`,
54+
`supply_chain`, `structural_drift`, `workflow_audit`, `workflow_hardening`,
55+
`cicd_rules`, `scorecard_compliance`. (A local token may surface MORE than
56+
37 — run without one to reproduce the gate's set.)
57+
- Severities depend on the pinned `standards` reusable-workflow version
58+
(currently `d135b05…`); the 5/7/25 split was observed on the first
59+
unblocked run and may shift slightly with the engine version.
60+
61+
## Task 2 — triage + fix
62+
63+
1. Group by rule × severity. Fix order: **5 critical → 7 high → 25 medium**.
64+
2. Per finding: true positive → fix in code/docs; false positive / accepted →
65+
add a justified `rule:path` line to `.hypatia-ignore` (matched `grep -qxF`),
66+
or enter it in `.hypatia-baseline.json` (schema in `standards`
67+
`.machine_readable/hypatia-baseline.schema.json`).
68+
3. **Proof / claim findings** (`honest_completion`, `proof_obligation`): fix by
69+
making *claims* honest (docs/metadata), **never** by editing or force-closing
70+
the fenced legacy proofs. Per `CLAUDE.md`: do not touch
71+
`formal/Semantics.v` `Theorem preservation` (provably false; deliberately
72+
`Admitted`), `formal/Typing.v`, or `formal/Counterexample.v`.
73+
4. **`disambiguation_rules`** findings: ensure the ephapax-vs-AffineScript
74+
disambiguation markers are present per `CLAUDE.md`.
75+
5. Re-run the scan until `critical = 0` (ideally total within policy). Open a
76+
PR with a triage table: *finding → disposition → fix*.
77+
78+
## Task 3 — make the gate non-opaque (in `hyperpolymath/standards`)
79+
80+
The gate fails **opaquely**: in `standards`'
81+
`.github/workflows/hypatia-scan-reusable.yml` the scan runs under `bash -e`,
82+
and `hypatia-cli.sh scan` **exits 1 when findings exist**, so the step aborts
83+
*before* the (already-present) `upload-artifact` step and the "warn but don't
84+
fail" critical-check ever run. Net effect: a hard job failure emitting only a
85+
severity count, no detail.
86+
87+
**Fix (in `standards`):** wrap the scan in `set +e` + capture the rc; **always**
88+
upload `hypatia-findings.json` (`if: always()`); write a findings table to
89+
`$GITHUB_STEP_SUMMARY`; enforce the gate in a final dedicated step. Pin
90+
`actions/upload-artifact` by SHA (same supply-chain lesson as PR #315). A full
91+
suggested patch was drafted in-session (not yet applied).
92+
93+
## Guardrails (from `CLAUDE.md`)
94+
95+
- This is `hyperpolymath/ephapax` (not AffineScript). Signed commits.
96+
- Code/config = `MPL-2.0`; prose (`.md`/`.adoc`) = `CC-BY-SA-4.0`.
97+
- Never touch the fenced legacy preservation proof or `Typing.v` /
98+
`Counterexample.v`. Fix proof/claim findings by aligning claims to reality.

docs/wikis/Home.md

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -77,6 +77,7 @@ The four layers and their current state:
7777

7878
## Governance
7979

80+
- **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)
8081
- **Licence**: MPL-2.0
8182
- **Machine-readable state**: [`.machine_readable/6a2/`](https://github.com/hyperpolymath/ephapax/tree/main/.machine_readable/6a2/)
8283
- **Contractiles**: 6-verb governance in [`.machine_readable/contractiles/`](https://github.com/hyperpolymath/ephapax/tree/main/.machine_readable/contractiles/)

0 commit comments

Comments
 (0)