security: standardize secret scanning on TruffleHog
docs: Add CODEOWNERS, MAINTAINERS, and GOVERNANCE documents
chore: rename k9 directories to self-validating for clarity
Proof-status: refresh after 2026-06-01/02 proof landings Today's PRs that change the proof state: - #270 Print Assumptions audit framework wired across L1 + L3 keystones (closes P10/P32) - #273 is_linear_ty Rust↔Coq bridge truth-table mechanical assertion (P28) - #274 canonical_*_l1_m ported to modality-polymorphic L1 judgment (P43, prerequisite for progress_l1, all 7 axiom-free) - #277 OwnershipKind from_byte/to_byte round-trip — typed-wasm ADR-0002 carrier handshake (P59) - #280 step_pop_disjoint_from_type_l1 stated + EASY cases Qed-closed (P06, HARD cases blocked on §4.8 lambda-rigidity) Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
chore: migrate license from PMPL-1.0-or-later to MPL-2.0
wiki: refresh 22 → 12 preservation count + extended reduction story Mirrors the companion repo PR #122. After PR #116 closed 10 more preservation goals (22 → 12) and PR #121 landed the Phase 1 scaffold (Lemma B stated), updates the wiki to reflect: Home.md — 22 → 12 in proof-status-at-a-glance table; reduction-story bullets extended through PR #114, #116, #121; new pointer to ROADMAP §'Preservation closure plan' as the canonical 12 → 0 path. Proof-status.md — date updated to 2026-05-21; preservation row says '12 open goals'; reduction story now has five passes (was three): added region-invariance lemma (#114), per-case closures (#116), and Phase 1 scaffold (#121); '22 → 0' section replaced with '12 → 0 (canonical closure plan -- see ROADMAP)' summarising the 5-phase plan. What-can-go-wrong.md — '22 open / 910 closed' → '12 open / 910 closed' in the closing paragraph. Comparison-to-other-languages.md — '910 closed, 22 open' → '910 closed, 12 open'. Glossary.md — '22 open / 910 closed' → '12 open / 910 closed' in the preservation entry. One occurrence of '29 → 22 goals' is retained in Home.md as intentional reduction-step history.
wiki: correct Idris2 region-linearity theorem names The 2026-05-20 wiki refresh used the wrong names for two region-linearity theorems: regionSafetyTheorem -> regionSafetyExtract (actual name) noGCTheorem -> noGCExtract (actual name) Also corrected file paths: all four theorems live in `Ephapax/Formal/RegionLinear.idr` (not separate `RegionSafety.idr`/`NoGC.idr`/`NoEscape.idr`/`Orthogonality.idr` files, which don't exist). Files updated: - Home.md (1 occurrence each) - Region-calculus.md (5 occurrences across 2 sections) - Proof-status.md (5-row table — names and paths corrected; line numbers added per-theorem for direct navigation)
wiki: add six topic guides for outside readers Add Linear-and-affine, Region-calculus, Two-phase-compiler, What-can-go-wrong, Comparison-to-other-languages, and Glossary. Each opens with a 1-paragraph what/why/where summary, cross-links the others, and references concrete files in the ephapax repo. Update _Sidebar.md with a "Topic guides" section. Proof-state claims stay consistent with Proof-status.md: preservation is 22 open / 910 closed; the Idris2 frontend is 8/9 files %default total + 1 %default covering.
wiki: refresh for 2026-05-20 state — add Proof-status page + sidebar nav Home.md rewritten as a navigation hub for outside readers: - 'Start here, by audience' table routes new readers to the right quickstart per role. - 'What is Ephapax?' summary positioned for an outside observer. - Proof status at a glance with the preservation reduction story (910 -> 22) and the Idris2 totality campaign outcome. - 'Documentation by topic' indexes every other repo .adoc/.md. - 'Highest-leverage open work' prioritised contribution roadmap. - 'Related projects' updated to include echo-types and corrected links. New Proof-status.md is the canonical 'what's proven / what's open' page with per-lemma table for Coq (Qed list + the 22-goal preservation breakdown) and per-file table for the Idris2 frontend totality campaign. Links every relevant PR (#89-#100 Idris2 + #92/#102/#104/#106 Coq preservation chain). New _Sidebar.md provides persistent navigation across wiki pages.
Create wiki Home page with project overview