Skip to content

Commit 5eb28d7

Browse files
docs(policy): correct ephapax Admitted count (3 → 1) + link adoption PR (#221)
## Summary The trusted-base reduction policy's P0 migration table cited **3 Admitteds** in `ephapax/formal/Semantics.v`. The actual count on `main` is **1** — the other two (`step_preserves_type` and `step_output_context_eq`) were discharged via [ephapax#146](hyperpolymath/ephapax#146) (Path 3 at-pre helper landing) before this policy doc was filed. Also adds: - Link to `formal/PRESERVATION-DESIGN.md` (four-layer redesign on branch `proof/l1-region-threading-design`) as the principled closure plan. - Forward link to [ephapax#164](hyperpolymath/ephapax#164) — the P0 migration PR adopting this policy in `ephapax/docs/proof-debt.adoc`. No semantic change to the policy itself — just keeping the migration table accurate as repos adopt the schema. ## Test plan - [x] One-line `.adoc` table cell edit; no build target affected - [x] GPG-signed commit (key `4A03639C…2867091E`, noreply email) - [x] Auto-merge SQUASH enabled 🤖 Generated with [Claude Code](https://claude.com/claude-code)
1 parent 5a78322 commit 5eb28d7

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

docs/TRUSTED-BASE-REDUCTION-POLICY.adoc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -191,7 +191,7 @@ first (rough P0/P1/P2 ordering):
191191
|===
192192
| Priority | Repo | Why this one first
193193

194-
| P0 | `ephapax` | 3 `Admitted`s in `formal/Semantics.v` already have a discharge plan (memory: `project_ephapax_preservation_closure_plan`); annotate while closing.
194+
| P0 | `ephapax` | 1 `Admitted` in `formal/Semantics.v` (`preservation`); was 3 at audit time, 2 discharged via https://github.com/hyperpolymath/ephapax/pull/146[ephapax#146]. Discharge plan in `ROADMAP.adoc` § "Preservation closure plan" + `formal/PRESERVATION-DESIGN.md` (four-layer redesign on branch `proof/l1-region-threading-design`). Migration filed: https://github.com/hyperpolymath/ephapax/pull/164[ephapax#164].
195195
| P0 | `boj-server` | Reference implementation — formalise the existing harness as the canonical example.
196196
| P1 | `absolute-zero` | 72 Coq + 315 Lean markers across 6638 proof files; needs the schema before any single-repo close-out is tractable.
197197
| P1 | `maa-framework` | 134 markers in 25 files (high density); investigate whether vendored or original.

0 commit comments

Comments
 (0)