diff --git a/.github/CONTRIBUTING.md b/.github/CONTRIBUTING.md new file mode 100644 index 0000000..79c398c --- /dev/null +++ b/.github/CONTRIBUTING.md @@ -0,0 +1,249 @@ +# Contributing to epistemic-types + +`epistemic-types` is a small, deliberately honest Agda formalization of +standpoint-indexed modal / epistemic / echo-like type formers. It +favours mathematical honesty over a large API. Contributions are +welcome, but the bar is **everything still type-checks under `--safe` +`--without-K`, with no shortcuts**. + +- **Author:** Jonathan D.A. Jewell (hyperpolymath) + [j.d.a.jewell@open.ac](j.d.a.jewell@open.ac).uk + +- **Version:** 0.1.0 (status: prototype) + +- **Last updated:** 2026-06-15 + +’’’’’ + +## Contribution model — Tri-Perimeter Contribution Framework (TPCF) + +epistemic-types follows the estate-wide **Tri-Perimeter Contribution +Framework (TPCF)** — graduated trust without gatekeeping: + +- **Perimeter 1 — Core Systems (maintainers only).** The proof kernel: + `src/EpistemicTypes/*.agda` (Base, Access, Warrant, ProofTransport, + the EchoBridge/SurrealBridge), the `All.agda` wiring, and build + tooling. + +- **Perimeter 2 — Expert Extensions (trusted contributors).** New + epistemic/standpoint modules, examples, and bridges. Apply via issue → + review → merge, with `just` `check` green. + +- **Perimeter 3 — Community Sandbox (open to all).** Docs (`.adoc`), + `.well-known/`, AI manifests, spec proposals. + +### Fork workflow + +External contributors use the standard **fork**-and-pull-request +workflow: fork the repository, branch from `main`, run `just` `check` +(the full `--safe` `--without-K` type-check) locally, and open a PR. +Proofs are load-bearing — a red `agda` check blocks merge, and no +`postulate` / `believe_me` shortcuts are accepted. + +## Build and check + +The combined proof and rejection gate must stay green: + + just check + +This checks every source module (including `All.agda`) and runs +`tests/check-rejections.sh`. Deliberate rejection fixtures stay outside +the positive `All.agda` import graph. + +Requirements: + +- **Agda 2.6.4.3**. + +- **No Agda standard library.** The build runs with `--no-libraries`; + the only external core imports allowed are from `Agda.Builtin.*` and + `Agda.Primitive`. The optional `tests/integration/CanonicalEcho.agda` + checks correspondence with actual sibling sources through `just` + `check-canonical`; its dependencies stay outside the default core + gate. + +`All.agda` imports every core module, so `just` `check` checks the whole +library. A change is not done until `just` `check` passes with no errors +and no warnings. + +CI checks every source module, semantic rejection controls and pinned +canonical Echo correspondence. Proof and security gates must pass before +merge; see [docs/ci-safety.adoc](docs/ci-safety.adoc). Run the local +checks before opening a PR. + +’’’’’ + +## The honesty rules + +These are non-negotiable. A PR that breaks any of them will not be +merged. + +- **No `postulate`.** Nothing is asserted without proof. If a law holds, + prove it; if it does not, it is not stated as if it did. Where a law + is not derivable but is needed, it appears as an explicit *field* the + caller must supply (see `LawfulModality`, `FactiveModality`, + `BeliefModality`), so the assumption is visible at the type level + rather than smuggled in. + +- **No standard library.** As above: `Agda.Builtin.*` and + `Agda.Primitive` only. + +- **`--safe` `--without-K`.** Every module compiles under `{-#` + `OPTIONS` `--safe` `--without-K` `#-}`. This rules out `postulate`, + unsafe pragmas, axiom K, and `--type-in-type`. Do not weaken these + options. + +- **No too-strong rules.** Keep the interfaces as weak as the proofs + allow. The base form `E` `:` `K` `→` `Set` `ℓ` `→` `Set` `ℓ` is a + plain indexed endofunctor (`map` only) — it is **not** a monad or + comonad, and there is no generic `return`/`reflect`. Do not promote it + to one. If something needs more structure, add a *named* stronger + interface (e.g. `ReturnModality`) that callers opt into, and keep the + base interface untouched. + +- **Add lemmas with proofs, not admits.** New results land as complete + proofs closed with normal Agda terms. No holes (`?`), no admit-shaped + escapes, no `TERMINATING`/`NON_COVERING` pragmas to paper over gaps. + +### Keep the bridges distinct + +The library is careful about what is and is not the same thing. Preserve +these separations when extending: + +- `Echo` `C` `y` carries a specified residue certificate. + `MatchesSource` is compatibility, not unique historical provenance. + `BoundedEcho` measures a residue separately; it is not a retention + index or an epistemic standpoint. + +- A `ReadView` `s` must entail its contents equality. Writes must not + silently refresh cached values; evidence transport needs its stability + proof. + +- In `ProofTransport`, every proof status must entail its explicit + `Meaning` via `proofSound`. Preserve the successful-check witness and + the verifier’s soundness obligation. Public transport needs an + explicit implication between holder meanings; evidence tokens alone + never suffice. `just` `check` must pass both the positive library and + the deliberate type-error regression controls. + +’’’’’ + +## Adding a module or lemma + +1. Put Agda source under `src/EpistemicTypes/` and add the new module + to the `import`/re-export list in `src/EpistemicTypes/All.agda` so + `just` `check` covers it. + +2. Open each module with `{-#` `OPTIONS` `--safe` `--without-K` `#-}`. + +3. Keep modules small and single-purpose, mirroring the existing + layout: `Base`, `Warrant`, `Access`, `EchoBridge`, `SurrealBridge`, + `ProofTransport`, `ProofTransportExample`, `Examples`. + +4. State assumptions as interface fields, not postulates. Add lawful + instances only after the laws are proved or explicitly required as + fields. + +5. Run `just` `check`. + +If a change touches the ProofTransport engineering rendering (the +a2ml/k9 attestation target under `.machine_readable/proof-transport/`), +keep the Agda model and the machine-readable description in step. + +’’’’’ + +## Documentation + +- **AsciiDoc (`.adoc`) is the default** for documentation. Update the + relevant `.adoc` file alongside any behavioural or interface change. + +- Existing docs keep their current names: `README.adoc` and + `explainme.adoc`. Do **not** rename or duplicate them. + +- Machine-readable descriptions live under `.machine_readable/` (a2ml + + Nickel/k9). a2ml files use the canonical TOML-like dialect: + `[section]` headers, `key` `=` `"value"`, arrays `[` `"a",` `"b"` `]`, + inline tables `{` `k` `=` `"v",` `j` `=` `"w"` `}`. + +- Root contribution, conduct, security and changelog documents use + AsciiDoc. Preserve their existing `.adoc` filenames. + +’’’’’ + +## Commits and pull requests + +### Branch naming + + feat/short-description # new module, interface, or lemma + fix/short-description # corrected proof or definition + docs/short-description # .adoc / machine-readable docs + refactor/short-description + +### Conventional Commits + +Commit messages follow [Conventional +Commits](https://www.conventionalcommits.org/): + + (): + + [optional body] + + [optional footer] + +Typical scopes match the modules: `base`, `warrant`, `access`, `echo`, +`surreal`, `proof-transport`, `docs`. + +### Signed commits + +All commits must be **signed**. Use the existing SSH/GPG signing key; do +not create new keys. Verify with: + + git log --show-signature + +Unsigned commits will be asked to be re-signed before merge. + +### Before you open a PR + +1. `just` `check` passes — no errors, no warnings. + +2. No `postulate`, no library imports, no `?`/admits, no weakened + pragmas. + +3. The honesty rules above still hold (weak base interface, distinct + bridges, no proof-smuggling in transport). + +4. Relevant `.adoc` and `.machine_readable/` files updated. + +5. Commits are conventional and signed. + +Keep PRs small and focused — one idea, one proof obligation, easy to +check. + +’’’’’ + +## Licence note + +The licence is owner-managed. Do **not** add `LICENSE`, +`SPDX-License-Identifier` headers, or copyright header lines in a PR. +The repo is currently SPDX-free and stays consistent; licensing is +handled separately by the owner. + +’’’’’ + +## Ecosystem siblings + +`epistemic-types` sits alongside (and should stay coherent with) these +estate repos: + +- **echo-types** — Agda loss-with-residue formalism; `EchoBridge` + composes with it. Audit it before duplicating echo machinery here. + +- **ephapax** — sibling formal language (four-layer redesign with echo + obligations). + +- **standards** — estate RSR/standards, k9-svc, and a2ml tooling. + +- **a2ml / k9** — machine-readable + contractile tooling; the + engineering target for `ProofTransport`. + +When a contribution overlaps a sibling (especially echo-types), prefer +reusing or extending it upstream over re-deriving it locally. diff --git a/CONTRIBUTING.adoc b/CONTRIBUTING.adoc deleted file mode 100644 index cdf52c4..0000000 --- a/CONTRIBUTING.adoc +++ /dev/null @@ -1,234 +0,0 @@ -== Contributing to epistemic-types - -`epistemic-types` is a small, deliberately honest Agda formalization of -standpoint-indexed modal / epistemic / echo-like type formers. It -favours mathematical honesty over a large API. Contributions are -welcome, but the bar is *everything still type-checks under -`--safe --without-K`, with no shortcuts*. - -* *Author:* Jonathan D.A. Jewell (hyperpolymath) j.d.a.jewell@open.ac.uk -* *Version:* 0.1.0 (status: prototype) -* *Last updated:* 2026-06-15 - -''''' - -[[contribution-model--tri-perimeter-contribution-framework-tpcf]] -=== Contribution model — Tri-Perimeter Contribution Framework (TPCF) - -epistemic-types follows the estate-wide *Tri-Perimeter Contribution -Framework (TPCF)* — graduated trust without gatekeeping: - -* *Perimeter 1 — Core Systems (maintainers only).* The proof kernel: -`src/EpistemicTypes/++*++.agda` (Base, Access, Warrant, ProofTransport, -the EchoBridge/SurrealBridge), the `All.agda` wiring, and build tooling. -* *Perimeter 2 — Expert Extensions (trusted contributors).* New -epistemic/standpoint modules, examples, and bridges. Apply via issue → -review → merge, with `just check` green. -* *Perimeter 3 — Community Sandbox (open to all).* Docs (`.adoc`), -`.well-known/`, AI manifests, spec proposals. - -==== Fork workflow - -External contributors use the standard *fork*-and-pull-request workflow: -fork the repository, branch from `main`, run `just check` (the full -`--safe --without-K` type-check) locally, and open a PR. Proofs are -load-bearing — a red `agda` check blocks merge, and no `postulate` / -`believe++_++me` shortcuts are accepted. - -=== Build and check - -The combined proof and rejection gate must stay green: - -.... -just check -.... - -This checks every source module (including `All.agda`) and runs -`tests/check-rejections.sh`. Deliberate rejection fixtures stay outside -the positive `All.agda` import graph. - -Requirements: - -* *Agda 2.6.4.3*. -* *No Agda standard library.* The build runs with `--no-libraries`; the -only external core imports allowed are from `Agda.Builtin.++*++` and -`Agda.Primitive`. The optional `tests/integration/CanonicalEcho.agda` -checks correspondence with actual sibling sources through -`just check-canonical`; its dependencies stay outside the default core -gate. - -`All.agda` imports every core module, so `just check` checks the whole -library. A change is not done until `just check` passes with no errors -and no warnings. - -CI checks every source module, semantic rejection controls and pinned canonical -Echo correspondence. Proof and security gates must pass before merge; see -link:docs/ci-safety.adoc[]. Run the local checks before opening a PR. - -''''' - -=== The honesty rules - -These are non-negotiable. A PR that breaks any of them will not be -merged. - -* *No `postulate`.* Nothing is asserted without proof. If a law holds, -prove it; if it does not, it is not stated as if it did. Where a law is -not derivable but is needed, it appears as an explicit _field_ the -caller must supply (see `LawfulModality`, `FactiveModality`, -`BeliefModality`), so the assumption is visible at the type level rather -than smuggled in. -* *No standard library.* As above: `Agda.Builtin.++*++` and -`Agda.Primitive` only. -* *`--safe --without-K`.* Every module compiles under -`++{++-++#++ OPTIONS --safe --without-K ++#++-}`. This rules out -`postulate`, unsafe pragmas, axiom K, and `--type-in-type`. Do not -weaken these options. -* *No too-strong rules.* Keep the interfaces as weak as the proofs -allow. The base form `E : K → Set ℓ → Set ℓ` is a plain indexed -endofunctor (`map` only) — it is *not* a monad or comonad, and there is -no generic `return`/`reflect`. Do not promote it to one. If something -needs more structure, add a _named_ stronger interface (e.g. -`ReturnModality`) that callers opt into, and keep the base interface -untouched. -* *Add lemmas with proofs, not admits.* New results land as complete -proofs closed with normal Agda terms. No holes (`?`), no admit-shaped -escapes, no `TERMINATING`/`NON++_++COVERING` pragmas to paper over gaps. - -==== Keep the bridges distinct - -The library is careful about what is and is not the same thing. Preserve -these separations when extending: - -* `Echo C y` carries a specified residue certificate. `MatchesSource` is -compatibility, not unique historical provenance. `BoundedEcho` measures -a residue separately; it is not a retention index or an epistemic -standpoint. -* A `ReadView s` must entail its contents equality. Writes must not -silently refresh cached values; evidence transport needs its stability -proof. -* In `ProofTransport`, every proof status must entail its explicit -`Meaning` via `proofSound`. Preserve the successful-check witness and -the verifier's soundness obligation. Public transport needs an explicit -implication between holder meanings; evidence tokens alone never -suffice. `just check` must pass both the positive library and the -deliberate type-error regression controls. - -''''' - -=== Adding a module or lemma - -[arabic] -. Put Agda source under `src/EpistemicTypes/` and add the new module to -the `import`/re-export list in `src/EpistemicTypes/All.agda` so -`just check` covers it. -. Open each module with -`++{++-++#++ OPTIONS --safe --without-K ++#++-}`. -. Keep modules small and single-purpose, mirroring the existing layout: -`Base`, `Warrant`, `Access`, `EchoBridge`, `SurrealBridge`, -`ProofTransport`, `ProofTransportExample`, `Examples`. -. State assumptions as interface fields, not postulates. Add lawful -instances only after the laws are proved or explicitly required as -fields. -. Run `just check`. - -If a change touches the ProofTransport engineering rendering (the -a2ml/k9 attestation target under -`.machine++_++readable/proof-transport/`), keep the Agda model and the -machine-readable description in step. - -''''' - -=== Documentation - -* *AsciiDoc (`.adoc`) is the default* for documentation. Update the -relevant `.adoc` file alongside any behavioural or interface change. -* Existing docs keep their current names: `README.adoc` and -`explainme.adoc`. Do *not* rename or duplicate them. -* Machine-readable descriptions live under `.machine++_++readable/` -(a2ml {plus} Nickel/k9). a2ml files use the canonical TOML-like dialect: -`++[++section++]++` headers, `key = "value"`, arrays -`++[++ "a", "b" ++]++`, inline tables `++{++ k = "v", j = "w" }`. -* Root contribution, conduct, security and changelog documents use AsciiDoc. - Preserve their existing `.adoc` filenames. - -''''' - -=== Commits and pull requests - -==== Branch naming - -.... -feat/short-description # new module, interface, or lemma -fix/short-description # corrected proof or definition -docs/short-description # .adoc / machine-readable docs -refactor/short-description -.... - -==== Conventional Commits - -Commit messages follow https://www.conventionalcommits.org/[Conventional -Commits]: - -.... -(): - -[optional body] - -[optional footer] -.... - -Typical scopes match the modules: `base`, `warrant`, `access`, `echo`, -`surreal`, `proof-transport`, `docs`. - -==== Signed commits - -All commits must be *signed*. Use the existing SSH/GPG signing key; do -not create new keys. Verify with: - -.... -git log --show-signature -.... - -Unsigned commits will be asked to be re-signed before merge. - -==== Before you open a PR - -[arabic] -. `just check` passes — no errors, no warnings. -. No `postulate`, no library imports, no `?`/admits, no weakened -pragmas. -. The honesty rules above still hold (weak base interface, distinct -bridges, no proof-smuggling in transport). -. Relevant `.adoc` and `.machine++_++readable/` files updated. -. Commits are conventional and signed. - -Keep PRs small and focused — one idea, one proof obligation, easy to -check. - -''''' - -=== Licence note - -The licence is owner-managed. Do *not* add `LICENSE`, -`SPDX-License-Identifier` headers, or copyright header lines in a PR. -The repo is currently SPDX-free and stays consistent; licensing is -handled separately by the owner. - -''''' - -=== Ecosystem siblings - -`epistemic-types` sits alongside (and should stay coherent with) these -estate repos: - -* *echo-types* — Agda loss-with-residue formalism; `EchoBridge` composes -with it. Audit it before duplicating echo machinery here. -* *ephapax* — sibling formal language (four-layer redesign with echo -obligations). -* *standards* — estate RSR/standards, k9-svc, and a2ml tooling. -* *a2ml / k9* — machine-readable {plus} contractile tooling; the -engineering target for `ProofTransport`. - -When a contribution overlaps a sibling (especially echo-types), prefer -reusing or extending it upstream over re-deriving it locally. diff --git a/guix.scm b/build/guix.scm similarity index 95% rename from guix.scm rename to build/guix.scm index 9e575f6..bbf41df 100644 --- a/guix.scm +++ b/build/guix.scm @@ -2,7 +2,7 @@ ;; Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) ;; ;; Guix development environment for epistemic-types. Replaces flake.nix (Guix-only policy). -;; Usage: guix shell -D -f guix.scm +;; Usage: guix shell -D -f build/guix.scm (use-modules (guix packages) (guix build-system gnu)