From 664380d91886112d8bab35103e016bbd7f953644 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 19 Sep 2026 09:12:39 +0000 Subject: [PATCH] refactor(root): move root artefacts to their canonical locations Applies the estate root-shape rollout: files that are not root-level by necessity move to where their tooling and the estate canon expect them, and every reference to them is updated in the same change. * .machine_readable/root-allow.txt * build/guix.scm (from guix.scm) -> build/guix.scm * .github/CONTRIBUTING.md (new) * CONTRIBUTING.adoc (deleted) * GOVERNANCE.adoc Verified with `git apply --check` against current main before committing; no behaviour change intended, the Justfile entry points keep working. --- .github/CONTRIBUTING.md | 91 ++++++++++++++++++++++++++++++++ .machine_readable/root-allow.txt | 1 + CONTRIBUTING.adoc | 84 ----------------------------- GOVERNANCE.adoc | 4 +- guix.scm => build/guix.scm | 2 +- 5 files changed, 95 insertions(+), 87 deletions(-) create mode 100644 .github/CONTRIBUTING.md delete mode 100644 CONTRIBUTING.adoc rename guix.scm => build/guix.scm (95%) diff --git a/.github/CONTRIBUTING.md b/.github/CONTRIBUTING.md new file mode 100644 index 0000000..37c4a83 --- /dev/null +++ b/.github/CONTRIBUTING.md @@ -0,0 +1,91 @@ +# Contributing to echo-types + +Thank you for your interest. Echo-types is a constructive Agda +formalisation; contribution discipline reflects the proof-bearing nature +of the codebase. + +## Sign-off + +All commits require Developer Certificate of Origin sign-off: + + git commit -s -m "feat: ..." + +## Branches + +- `main` — protected; only fast-forward from approved PRs. + +- `feat/` — feature branches, squash-merge. + +- `fix/` — bug-fix branches. + +## Pre-merge checklist + +1. `just` `verify` passes (full Agda type-check pass against + `proofs/agda/All.agda` and the test suites). + +2. CHANGELOG.md updated under `[Unreleased]`. + +3. `.machine_readable/6a2/STATE.a2ml` `last-updated` bumped if the + change is significant. + +4. **Banned constructs.** No new `believe_me`, `assert_total`, + `postulate`, `sorry`, `Admitted`, `unsafeCoerce`, or `Obj.magic` + introduced. Estate-wide policy. + +5. **Guardrails are CI-enforced.** All `.agda` files under + `proofs/agda/**` must declare `{-#` `OPTIONS` `--safe` `--without-K` + `#-}` at the top. `tools/check-guardrails.sh` runs at CI time across + every file (regardless of `All.agda` membership) and fails on: + missing `--safe` / `--without-K`, escape pragmas (`TERMINATING`, + `REWRITE`, `NO_POSITIVITY_CHECK`, etc.), `postulate` in code, or + unsafe primitives (`primTrustMe`, `primEraseEquality`, `trustMe`). + The `Exploratory` classification in + `docs/echo-types/echo-kernel-note.adoc` only excuses `All.agda` + membership — it does NOT excuse the guardrail. If you need + postulates for a demo or earn-back-gate consumer, the file must live + outside `proofs/agda/` (no current non-guarded path exists; widening + the guardrail’s allowlist requires a separate design discussion). + +6. **EI-2 discipline.** Per `.machine_readable/6a2/STATE.a2ml` `§` + `ei-2`, the integration-recipe distinctness investigation is + *terminated negatively* and is not to be reopened. If a change + touches that territory, read `STATE.a2ml` `§` `ei-2` first; the + `forbidden-rebrandings` list is a hard fence. + +7. **Naming traps.** `ModeGraded` (with trailing `d`) is canonical; + never `ModeGrade`. See `STATE.a2ml` `§` `naming-traps`. + +## Reviews + +At least one maintainer review (see MAINTAINERS.adoc). Bridge-module +changes (the cross-system bridges in `proofs/agda/Echo*Bridge*.agda`) +need attention because they fix the load-bearing distinctness story; +flag them for explicit review. + +## Contribution model — Tri-Perimeter Contribution Framework (TPCF) + +echo-types follows the estate-wide **Tri-Perimeter Contribution +Framework (TPCF)** — graduated trust without gatekeeping: + +- **Perimeter 1 — Core Systems (maintainers only).** The proof kernel: + `proofs/agda/Echo.agda`, the identity-claim spine, the bridge modules, + the `All.agda` / `Smoke.agda` wiring, and the guardrail tooling. + Direct commits by maintainers only. + +- **Perimeter 2 — Expert Extensions (trusted contributors).** New proof + modules, decoration instances, and ordinal-track slices. Apply via + issue → review → merge under the relevant `proofs/agda/` path with the + build invariant green. + +- **Perimeter 3 — Community Sandbox (open to all).** Docs (`.adoc`), + tutorial walkthroughs, wiki pages, `.well-known/` content, and spec + proposals. + +### Fork workflow + +External contributors use the standard **fork**-and-pull-request +workflow: fork the repository, branch from `main`, run `just` `validate` +locally (full Agda verify + kernel-guard), and open a PR. Maintainers +(Perimeter 1) may commit directly to feature branches. Every PR must +keep `All.agda` + `Smoke.agda` green under `--safe` `--without-K` and +introduce no banned constructs (see the pre-merge checklist above). diff --git a/.machine_readable/root-allow.txt b/.machine_readable/root-allow.txt index 25e49a4..efa5179 100644 --- a/.machine_readable/root-allow.txt +++ b/.machine_readable/root-allow.txt @@ -1,2 +1,3 @@ .hypatia-ignore CLAUDE.md +build/ # build orchestration: guix.scm relocated here (canon 1.2.1 guix-primary template_ref = "build/") diff --git a/CONTRIBUTING.adoc b/CONTRIBUTING.adoc deleted file mode 100644 index 64426cf..0000000 --- a/CONTRIBUTING.adoc +++ /dev/null @@ -1,84 +0,0 @@ -== Contributing to echo-types - -Thank you for your interest. Echo-types is a constructive Agda -formalisation; contribution discipline reflects the proof-bearing nature -of the codebase. - -=== Sign-off - -All commits require Developer Certificate of Origin sign-off: - -.... -git commit -s -m "feat: ..." -.... - -=== Branches - -* `+main+` — protected; only fast-forward from approved PRs. -* `+feat/+` — feature branches, squash-merge. -* `+fix/+` — bug-fix branches. - -=== Pre-merge checklist - -[arabic] -. `+just verify+` passes (full Agda type-check pass against -`+proofs/agda/All.agda+` and the test suites). -. CHANGELOG.md updated under `+[Unreleased]+`. -. `+.machine_readable/6a2/STATE.a2ml+` `+last-updated+` bumped if the -change is significant. -. *Banned constructs.* No new `+believe_me+`, `+assert_total+`, -`+postulate+`, `+sorry+`, `+Admitted+`, `+unsafeCoerce+`, or -`+Obj.magic+` introduced. Estate-wide policy. -. *Guardrails are CI-enforced.* All `+.agda+` files under -`+proofs/agda/**+` must declare `+{-# OPTIONS --safe --without-K #-}+` -at the top. `+tools/check-guardrails.sh+` runs at CI time across every -file (regardless of `+All.agda+` membership) and fails on: missing -`+--safe+` / `+--without-K+`, escape pragmas (`+TERMINATING+`, -`+REWRITE+`, `+NO_POSITIVITY_CHECK+`, etc.), `+postulate+` in code, or -unsafe primitives (`+primTrustMe+`, `+primEraseEquality+`, `+trustMe+`). -The `+Exploratory+` classification in -`+docs/echo-types/echo-kernel-note.adoc+` only excuses `+All.agda+` -membership — it does NOT excuse the guardrail. If you need postulates -for a demo or earn-back-gate consumer, the file must live outside -`+proofs/agda/+` (no current non-guarded path exists; widening the -guardrail’s allowlist requires a separate design discussion). -. *EI-2 discipline.* Per `+.machine_readable/6a2/STATE.a2ml § ei-2+`, -the integration-recipe distinctness investigation is _terminated -negatively_ and is not to be reopened. If a change touches that -territory, read `+STATE.a2ml § ei-2+` first; the -`+forbidden-rebrandings+` list is a hard fence. -. *Naming traps.* `+ModeGraded+` (with trailing `+d+`) is canonical; -never `+ModeGrade+`. See `+STATE.a2ml § naming-traps+`. - -=== Reviews - -At least one maintainer review (see MAINTAINERS.adoc). Bridge-module -changes (the cross-system bridges in `+proofs/agda/Echo*Bridge*.agda+`) -need attention because they fix the load-bearing distinctness story; -flag them for explicit review. - -=== Contribution model — Tri-Perimeter Contribution Framework (TPCF) - -echo-types follows the estate-wide *Tri-Perimeter Contribution Framework -(TPCF)* — graduated trust without gatekeeping: - -* *Perimeter 1 — Core Systems (maintainers only).* The proof kernel: -`+proofs/agda/Echo.agda+`, the identity-claim spine, the bridge modules, -the `+All.agda+` / `+Smoke.agda+` wiring, and the guardrail tooling. -Direct commits by maintainers only. -* *Perimeter 2 — Expert Extensions (trusted contributors).* New proof -modules, decoration instances, and ordinal-track slices. Apply via issue -→ review → merge under the relevant `+proofs/agda/+` path with the build -invariant green. -* *Perimeter 3 — Community Sandbox (open to all).* Docs (`+.adoc+`), -tutorial walkthroughs, wiki pages, `+.well-known/+` content, and spec -proposals. - -==== Fork workflow - -External contributors use the standard *fork*-and-pull-request workflow: -fork the repository, branch from `+main+`, run `+just validate+` locally -(full Agda verify + kernel-guard), and open a PR. Maintainers (Perimeter -1) may commit directly to feature branches. Every PR must keep -`+All.agda+` + `+Smoke.agda+` green under `+--safe --without-K+` and -introduce no banned constructs (see the pre-merge checklist above). diff --git a/GOVERNANCE.adoc b/GOVERNANCE.adoc index e41020d..5ae0a72 100644 --- a/GOVERNANCE.adoc +++ b/GOVERNANCE.adoc @@ -114,7 +114,7 @@ This repository adheres to hyperpolymath estate-wide policies: * **License**: MPL-2.0 for code, CC-BY-SA-4.0 for prose (per standards/LICENCE-POLICY.adoc) * **Code of Conduct**: Follows hyperpolymath CODE_OF_CONDUCT.md * **Security**: Follows hyperpolymath SECURITY.md -* **Contributing**: Follows hyperpolymath CONTRIBUTING.adoc conventions +* **Contributing**: Follows hyperpolymath .github/CONTRIBUTING.md conventions == Repository-Specific Conventions @@ -148,7 +148,7 @@ Changes to this document require the same process as Significant Changes above. * link:MAINTAINERS.adoc[Maintainers] * link:CODE_OF_CONDUCT.md[Code of Conduct] -* link:CONTRIBUTING.adoc[Contributing Guide] +* link:.github/CONTRIBUTING.md[Contributing Guide] * link:https://github.com/hyperpolymath/standards/blob/main/LICENCE-POLICY.adoc[Estate License Policy] * link:https://github.com/hyperpolymath/standards[rhodium-standard-repositories (TPCF)] diff --git a/guix.scm b/build/guix.scm similarity index 95% rename from guix.scm rename to build/guix.scm index b02aab3..f6dbed6 100644 --- a/guix.scm +++ b/build/guix.scm @@ -1,6 +1,6 @@ ;; SPDX-License-Identifier: MPL-2.0 ;; Guix development environment. -;; Usage: guix shell -D -f guix.scm +;; Usage: guix shell -D -f build/guix.scm (use-modules (guix packages) (guix build-system gnu)