diff --git a/.devcontainer/README.adoc b/.devcontainer/README.adoc index a540001..2935dc8 100644 --- a/.devcontainer/README.adoc +++ b/.devcontainer/README.adoc @@ -6,9 +6,10 @@ `.devcontainer/Containerfile` builds a Debian 13 image pinned to the same base digest as the repository's Proof Safety workflow, and installs the same Agda (`agda-bin=2.6.4.3-1+b2`) plus `bash`, `git`, `just`, `make` and `ripgrep` -(`tests/check-rejections.sh` needs `rg`). `devcontainer.json` runs `just check` -once, after creation, so a fresh container either reproduces the positive and -expected-rejection proof gates or reports the failing gate. +(`tests/check-policy.sh` and `tests/check-rejections.sh` need `rg`). +`devcontainer.json` runs `just check` once after creation, so a fresh container +reproduces the policy guard, all 22 positive modules and all 13 +expected-rejection controls, or reports the failing gate. == Usage diff --git a/.github/CONTRIBUTING.md b/.github/CONTRIBUTING.md index 5612fac..d78e8c3 100644 --- a/.github/CONTRIBUTING.md +++ b/.github/CONTRIBUTING.md @@ -3,15 +3,15 @@ `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**. +welcome, but the bar is **everything still passes the canonical +`--safe --without-K --cubical-compatible` profile, with no shortcuts**. - **Author:** Jonathan D.A. Jewell (hyperpolymath) - [j.d.a.jewell@open.ac](j.d.a.jewell@open.ac).uk + [j.d.a.jewell@open.ac.uk](mailto:j.d.a.jewell@open.ac.uk) - **Version:** 0.1.0 (status: prototype) -- **Last updated:** 2026-06-15 +- **Last updated:** 2026-11-01 ’’’’’ @@ -21,8 +21,8 @@ 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 + all 22 modules recursively under `src/EpistemicTypes/` (core, + applications, and Kripke semantics), the `All.agda` wiring, and proof tooling. - **Perimeter 2 — Expert Extensions (trusted contributors).** New @@ -35,9 +35,9 @@ Framework (TPCF)** — graduated trust without gatekeeping: ### 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 +workflow: fork the repository, branch from `main`, run `just check` +(the policy gate, all positive modules, and all expected rejections) 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 @@ -46,9 +46,10 @@ 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. +This runs `tests/check-policy.sh`, checks all 22 source modules recursively, +and validates all 13 expected-rejection fixtures. Deliberate rejection +fixtures stay outside the positive `All.agda` import graph; coverage does not +depend on `All.agda` alone. Requirements: @@ -61,9 +62,10 @@ Requirements: `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. +`All.agda` imports the full graph, but the gate also checks every source file +independently so an omitted aggregate import cannot hide a module. A change is +not done until `just check` passes with no errors and no warnings outside the +single documented `UnsupportedIndexedMatch` transport-computation category. CI checks every source module, semantic rejection controls and pinned canonical Echo correspondence. Proof and security gates must pass before @@ -84,13 +86,14 @@ merged. `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. +- **No standard library in core source.** As above: `Agda.Builtin.*`, + `Agda.Primitive`, and local modules only. The optional pinned integration is + a separate boundary. -- **`--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. +- **Complete strict profile.** Every first-party module starts with + `{-# OPTIONS --safe --without-K --cubical-compatible --exact-split + --no-sized-types --no-guardedness #-}`. The command line repeats the first + three canonical flags. Do not weaken or partially restate this profile. - **No too-strong rules.** Keep the interfaces as weak as the proofs allow. The base form `E` `:` `K` `→` `Set` `ℓ` `→` `Set` `ℓ` is a @@ -129,15 +132,15 @@ these separations when extending: ## 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. +1. Put Agda source under `src/EpistemicTypes/` and wire it into + `src/EpistemicTypes/All.agda` where the full graph requires it. The + recursive gate will detect the new module; update the explicit 22-module + policy/metadata inventory in the same change rather than bypassing it. -2. Open each module with `{-#` `OPTIONS` `--safe` `--without-K` `#-}`. +2. Open each module with the exact complete strict `OPTIONS` line shown above. -3. Keep modules small and single-purpose, mirroring the existing - layout: `Base`, `Warrant`, `Access`, `EchoBridge`, `SurrealBridge`, - `ProofTransport`, `ProofTransportExample`, `Examples`. +3. Keep modules small and single-purpose, following the existing core, + `Applications/`, and `Kripke/` layout. 4. State assumptions as interface fields, not postulates. Add lawful instances only after the laws are proved or explicitly required as @@ -156,8 +159,9 @@ keep the Agda model and the machine-readable description in step. - **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. +- Preserve exact current names and roles: `README.adoc` is the overview, + `explainme.adoc` the concise narrative, and `EXPLAINME.adoc` the detailed + claims/evidence ledger. - Machine-readable descriptions live under `.machine_readable/` (a2ml + Nickel/k9). a2ml files use the canonical TOML-like dialect: @@ -230,10 +234,9 @@ 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. +The licence and existing SPDX declarations are owner-managed. Do **not** add, +remove, or alter licence files, SPDX identifiers, or copyright lines without +explicit owner instruction. ’’’’’ @@ -242,8 +245,9 @@ handled separately by the owner. `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. +- **echo-types** — canonical proof-relevant Echo sibling. The optional pin + checks representation and one-way lowering; Echo is not a resource instance. + Audit it before duplicating Echo machinery here. - **ephapax** — sibling formal language (four-layer redesign with echo obligations). diff --git a/.github/workflows/agda.yml b/.github/workflows/agda.yml index 8c814f0..34505f0 100644 --- a/.github/workflows/agda.yml +++ b/.github/workflows/agda.yml @@ -38,9 +38,22 @@ jobs: with: persist-credentials: false - name: Verify toolchain and proof constructions + shell: bash run: | test "$(agda --version)" = 'Agda version 2.6.4.3' - bash scripts/check.sh + set +e + output=$(bash scripts/check.sh 2>&1) + status=$? + set -e + printf '%s\n' "$output" + if [ "$status" -ne 0 ]; then + annotation=$(tail -n 20 <<< "$output") + annotation=${annotation//'%'/'%25'} + annotation=${annotation//$'\r'/'%0D'} + annotation=${annotation//$'\n'/'%0A'} + printf '::error title=Canonical proof gate::%s\n' "$annotation" + exit "$status" + fi echo: name: Canonical Echo correspondence @@ -65,7 +78,7 @@ jobs: - name: Prove representation round trips and lowering agreement run: | test "$(agda --version)" = 'Agda version 2.6.4.3' - agda --no-libraries --safe --without-K --double-check --ignore-interfaces \ + agda --no-libraries --safe --without-K --cubical-compatible --double-check --ignore-interfaces \ -W error -W noUnsupportedIndexedMatch -i src -i tests/integration \ -i .ci-deps/echo-types/proofs/agda -i /usr/share/agda-stdlib/src \ tests/integration/CanonicalEcho.agda diff --git a/.machine_readable/descriptiles/0-AI-MANIFEST.a2ml b/.machine_readable/descriptiles/0-AI-MANIFEST.a2ml index 68c00e5..3f4ca3c 100644 --- a/.machine_readable/descriptiles/0-AI-MANIFEST.a2ml +++ b/.machine_readable/descriptiles/0-AI-MANIFEST.a2ml @@ -6,13 +6,13 @@ project = "epistemic-types" repo = "hyperpolymath/epistemic-types" version = "0.1.0" status = "prototype" -last-updated = "2026-06-15" +last-updated = "2026-11-01" author = "Jonathan D.A. Jewell (hyperpolymath) " [purpose] summary = "Agda prototypes for standpoint-indexed modal, epistemic, and echo-like type formers." stance = "Favours mathematical honesty over a large API." -detail = "A small, deliberately honest Agda formalization. Constructive; compiles under {-# OPTIONS --safe --without-K #-}. No postulates. No Agda standard library (built with 'agda --no-libraries', using only Agda.Builtin.* / Agda.Primitive)." +detail = "A small, deliberately honest Agda formalization. All first-party modules declare --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness. Core source has no postulates, escape hatches or standard-library imports." core-form = "E : K -> Set ℓ -> Set ℓ. E κ A reads 'A is epistemically available at standpoint κ'." base-interface = "A plain indexed endofunctor (map only) — NOT a monad/comonad; no generic return/reflect." @@ -26,7 +26,7 @@ echo_distinction = "Echo values have explicit retention certificates; resource b no_collapse = "Do not collapse Echo C y and E κ A. Their composition is meaningful, but they are not the same modality." [typecheck] -command = "bash tests/check-proofs.sh && bash tests/check-rejections.sh" +command = "bash tests/check-policy.sh && bash tests/check-proofs.sh && bash tests/check-rejections.sh" just-target = "just check" agda-version = "2.6.4.3" @@ -36,6 +36,6 @@ agda-version = "2.6.4.3" present = ["0-AI-MANIFEST.a2ml", "AGENTIC.a2ml", "ECOSYSTEM.a2ml", "META.a2ml", "NEUROSYM.a2ml", "PLAYBOOK.a2ml", "README.adoc", "STATE.a2ml"] [invariants] -single-source-of-truth = "This directory is authoritative; no duplicate metadata in the root directory." +single-source-of-truth = "This directory is authoritative; the root 0-AI-MANIFEST.a2ml is a universal pointer and must agree with it." no-stale-metadata = true ci = "Proof and security workflows configured; see docs/ci-safety.adoc." diff --git a/.machine_readable/descriptiles/AGENTIC.a2ml b/.machine_readable/descriptiles/AGENTIC.a2ml index 857991a..26858c2 100644 --- a/.machine_readable/descriptiles/AGENTIC.a2ml +++ b/.machine_readable/descriptiles/AGENTIC.a2ml @@ -7,7 +7,7 @@ repository = "hyperpolymath/epistemic-types" author = "Jonathan D.A. Jewell (hyperpolymath) " version = "0.1.0" status = "prototype" -last-updated = "2026-06-15" +last-updated = "2026-11-01" [agent-permissions] can-edit-source = true # Agda modules under src/EpistemicTypes/ @@ -16,15 +16,17 @@ can-edit-machine-readable = true # .machine_readable/ (descriptiles, proof-tran can-edit-build = true # Justfile, epistemic-types.agda-lib, .gitignore can-create-files = true can-edit-license = false # LICENSE / SPDX are owner-manual — agents MUST NOT touch -can-add-spdx-headers = false # repo is intentionally SPDX-free; keep it consistent +can-add-spdx-headers = false # licensing declarations remain owner-managed [agent-constraints] # What AI agents must NOT do in this repository: # Honesty discipline (the whole point of the library): # - Never add a postulate. There are zero postulates and that is load-bearing. -# - Never weaken the pragma: keep {-# OPTIONS --safe --without-K #-} everywhere. -# - Never import an Agda standard library. Build stays `agda --no-libraries`; -# only Agda.Builtin.* and Agda.Primitive are permitted. +# - Never weaken the full strict pragma: --safe --without-K --cubical-compatible +# --exact-split --no-sized-types --no-guardedness. +# - Never import an Agda standard library into core source. Build stays +# `agda --no-libraries`; only Agda.Builtin.*, Agda.Primitive and local modules +# are permitted. The separately pinned CanonicalEcho integration is the exception. # - Never introduce a too-strong rule. The base interface E : K -> Set ℓ -> Set ℓ # is a plain indexed endofunctor (map only). Do NOT add a generic return, # reflect, join, or extract that is not justified by an explicit field or proof. @@ -55,10 +57,10 @@ release-claim-requires-hard-pass = true [verification] # The single source of truth for "does it hold". command = "just check" -underlying = "bash tests/check-proofs.sh && bash tests/check-rejections.sh" +underlying = "bash tests/check-policy.sh && bash tests/check-proofs.sh && bash tests/check-rejections.sh" agda-version = "2.6.4.3" -entrypoint = "src/EpistemicTypes/All.agda" -expected = "type-checks clean, no postulates, no warnings" +entrypoint = "scripts/check.sh (recursive source gate; All.agda is the aggregate module)" +expected = "22 source modules accepted, 13 intended rejections, strict profile/import/escape-hatch policy and planted-postulate control pass" [automation-hooks] # on-enter: Read 0-AI-MANIFEST.a2ml, then STATE.a2ml. diff --git a/.machine_readable/descriptiles/ECOSYSTEM.a2ml b/.machine_readable/descriptiles/ECOSYSTEM.a2ml index 24f4c52..10af825 100644 --- a/.machine_readable/descriptiles/ECOSYSTEM.a2ml +++ b/.machine_readable/descriptiles/ECOSYSTEM.a2ml @@ -5,7 +5,7 @@ project = "epistemic-types" ecosystem = "hyperpolymath" version = "0.1.0" status = "prototype" -last-updated = "2026-06-15" +last-updated = "2026-11-01" [position] type = "formal-methods-library" @@ -13,11 +13,11 @@ purpose = "A small, deliberately honest Agda formalization of standpoint-indexed [stack] language = "Agda 2.6.4.3" -options = "--safe --without-K" -libraries = "none — built with 'agda --no-libraries' against Agda.Builtin.* and Agda.Primitive only" +options = "--safe --without-K --cubical-compatible; source also declares --exact-split --no-sized-types --no-guardedness" +libraries = "core: none — --no-libraries against Agda.Builtin.*, Agda.Primitive and local modules; optional CanonicalEcho integration has pinned external source/stdlib" machine-readable = "a2ml + Nickel/k9" docs = "AsciiDoc" -check = "just check == agda --no-libraries -i src src/EpistemicTypes/All.agda" +check = "just check == policy inventory/negative control + all 22 source modules + all 13 expected rejections" notes = "Single-tool Agda library. The core has no runtime dependencies; CI uses a pinned Debian verification container." [core] @@ -32,7 +32,10 @@ modules = [ "EpistemicTypes.Examples", "EpistemicTypes.ProofTransport — standpoint-indexed proof transport across trust boundaries", "EpistemicTypes.ProofTransportExample — a K9-SVC / A2ML attestation scenario", - "EpistemicTypes.All — re-export aggregator" + "EpistemicTypes.ReadConsistency and ContinuityExamples — pure store history, freshness and continuity witnesses", + "EpistemicTypes.Applications.* — six modules for the RapidNJ bound, integer instance and skip warrants", + "EpistemicTypes.Kripke.* — five modules for indexed Box/frame correspondences, non-factive belief, residual candidates and dependence", + "EpistemicTypes.All — full-graph import; public re-export is deliberately narrower" ] [proof-transport] @@ -43,8 +46,11 @@ no-smuggling = "proofNeedsChecker: no checker-free Proof -> Proof transport is e [related-projects] projects = [ - { name = "echo-types", relationship = "sibling-formalism", notes = "Agda loss-with-residue (min-plus graded) formalism. EpistemicTypes.EchoBridge's 'Echo C y' composes with it; kept deliberately distinct from the epistemic E κ A modality (no collapse)." }, + { name = "echo-types", relationship = "sibling-formalism", notes = "Agda proof-relevant fibre/residue formalism. Canonical Echo can be lowered one-way into separately measured resource evidence, but Echo is not a resource instance. The local bridge checks representation/lowering at a pin and does not collapse Echo into E κ A." }, { name = "ephapax", relationship = "sibling-formal-language", notes = "Sibling formal language; its four-layer redesign carries echo obligations. Echo / standpoint vocabulary is shared at the conceptual level, not via a code dependency." }, + { name = "choreographic-types", relationship = "external-proof-consumer", notes = "Imports the warrant interface and proves scoped finite binary/plain-merge K-CUT results, including asynchronous variants. Data-dependent warrants and generalized fragments remain open; not a local dependency." }, + { name = "residual-evidence-types", relationship = "research-neighbour", notes = "Operated in production; its mathematical/API maturity remains early research with no stable API despite checked composition/revision/finite-checker progress. The local dependence result is a mirror, not an imported identity." }, + { name = "secret-types", relationship = "standalone-boundary", notes = "Owns confidentiality labels and generic TINI. No Secret API or IFC theorem belongs here; termination-sensitive noninterference and declassification remain open there." }, { name = "standards", relationship = "estate-foundation", notes = "Estate RSR / standards repo plus k9-svc and a2ml tooling. Supplies the descriptiles layout and the contractile / k9 rendering conventions this repo's .machine_readable mirrors." }, { name = "a2ml + k9", relationship = "rendering-target", notes = "Machine-readable a2ml + Nickel/k9 contractile tooling. The engineering rendering target for ProofTransport: the standpoint-indexed proof-transport core is rendered to a2ml/k9 under .machine_readable/proof-transport/." } ] diff --git a/.machine_readable/descriptiles/META.a2ml b/.machine_readable/descriptiles/META.a2ml index 6e97d15..3343c5e 100644 --- a/.machine_readable/descriptiles/META.a2ml +++ b/.machine_readable/descriptiles/META.a2ml @@ -3,7 +3,7 @@ [metadata] version = "0.1.0" -last-updated = "2026-10-04" +last-updated = "2026-11-01" [project-info] name = "epistemic-types" @@ -20,7 +20,7 @@ summary = "A small, deliberately honest Agda formalization of standpoint-indexed adrs = [ { id = "ADR-001", title = "No postulates: laws are record fields when not derivable", status = "accepted", date = "2026-06-15" }, { id = "ADR-002", title = "Separate FactiveModality from BeliefModality; no generic reflect/return", status = "accepted", date = "2026-06-15" }, - { id = "ADR-003", title = "Compile under --safe --without-K", status = "accepted", date = "2026-06-15" }, + { id = "ADR-003", title = "Compile under the strict canonical Agda profile", status = "accepted", date = "2026-06-15", updated = "2026-11-01" }, { id = "ADR-004", title = "No Agda standard library; build with agda --no-libraries", status = "accepted", date = "2026-06-15" }, { id = "ADR-005", title = "Keep certified residues and resource bounds distinct from epistemic standpoints", status = "accepted", date = "2026-06-15" }, { id = "ADR-006", title = "ProofTransport: no smuggling by construction", status = "accepted", date = "2026-06-15" }, @@ -42,18 +42,18 @@ decision = "The base interface `E : K -> Set ℓ -> Set ℓ` is a plain indexed consequence = "No monad/comonad structure is assumed. Factive extraction is available exactly where factivity has been declared, and nowhere else." [architecture-decisions.ADR-003] -title = "Compile under --safe --without-K" +title = "Compile under the strict canonical Agda profile" status = "accepted" -context = "`--safe` rejects postulates and unsafe pragmas; `--without-K` keeps the development compatible with proof-relevant / HoTT-friendly foundations." -decision = "Every module carries `{-# OPTIONS --safe --without-K #-}` and the aggregate `All.agda` type-checks under those options." -consequence = "Reinforces ADR-001 mechanically (no `--safe`-violating escape hatches) and constrains pattern matching to be K-free." +context = "`--safe` rejects postulates and unsafe pragmas; `--without-K` preserves proof relevance; `--cubical-compatible` is the estate canonical theory profile." +decision = "Every first-party module declares `--safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness`. The command line explicitly repeats the canonical first three flags, and the recursive gate checks every source module rather than trusting only the aggregate." +consequence = "Reinforces ADR-001 mechanically, keeps pattern matching K-free, and makes profile drift and omitted modules gate failures. tests/check-policy.sh supplies the planted-postulate negative control." [architecture-decisions.ADR-004] title = "No Agda standard library; build with agda --no-libraries" status = "accepted" -context = "Depending on `agda-stdlib` adds a large surface and a version-pinning burden for a deliberately small prototype." -decision = "Build with `agda --no-libraries`, using only `Agda.Builtin.*` and `Agda.Primitive`. No third-party Agda library is imported." -consequence = "The project is self-contained and reproducible with just an Agda binary, at the cost of re-deriving small primitives in-tree." +context = "Depending on `agda-stdlib` would add a large surface to the deliberately small core; the optional canonical-Echo witness is a separate integration boundary." +decision = "Build core source with `agda --no-libraries`, using only `Agda.Builtin.*`, `Agda.Primitive`, and local modules. The integration job explicitly pins sibling source and stdlib inputs." +consequence = "The core remains self-contained and reproducible with just an Agda binary; external correspondence cannot be mistaken for a core import." [architecture-decisions.ADR-005] title = "Keep certified residues and resource bounds distinct from epistemic standpoints" @@ -74,7 +74,7 @@ title = "Secret types and information-flow control are specified outside this re status = "accepted" context = "Issue #29 preserved a secret-types research note here; issue #32 then proposed an in-repository security model. On 2026-10-04 the owner ruled that hyperpolymath/secret-types is the standalone home, with D153 (a secret type is a value whose flow is constrained by a confidentiality label with explicit declassification, registered in the type-family map on that boundary) and D154 (reuse an existing lattice, two-point first then general; prove noninterference; declassify only at explicit audited points)." decision = "This repository adds no Secret API and no information-flow implementation. docs/secret-types.adoc is retained as the boundary/history note; the specification itself (canonical text in hyperpolymath/secret-types docs/secret-types.adoc; placement in docs/decisions/0004-standalone-repo-and-scope.adoc, PR #4 d1122d8), lattice reuse, the noninterference theorem, and audited declassification belong to hyperpolymath/secret-types." -consequence = "The epistemic core keeps its scope: no confidentiality claim attaches to BeliefModality, Echo grades, or Access. epistemic-types#29 stays closed. Issue #32 was closed on 2026-10-05 as delivered here - no transfer and no duplicate; do not reopen it. Its successor guard is epistemic-types#39. The standalone repository is no longer specification-only: at ccdcb3ec42792337a9ab6047e1f99de9d20a4f96 (2026-10-19) TINI at the two-point lattice and over a Lattice record are PROVEN and its proof gate is green; declassification is not yet implemented. See docs/secret-types.adoc section Status update 2026-10-25." +consequence = "The epistemic core keeps its scope: no confidentiality claim attaches to BeliefModality, Echo retention, measured resource bounds, or Access. epistemic-types#29 stays closed. Issue #32 was closed on 2026-10-05 as delivered here - no transfer and no duplicate; do not reopen it. Its successor guard is epistemic-types#39. Source-reviewed at standalone secret-types f581f8295bdee854f76291ab884a16cc8114dc6f on 2026-11-01: generic TINI over a Lattice record/down-closed observer and the two-point instance are PROVEN in its ledger; termination-sensitive noninterference and declassification remain OPEN. No theorem is imported here." [development-practices] build-tool = "just" @@ -90,10 +90,10 @@ posture = "Mathematical honesty over API size. The library is small on purpose: base-interface = "`E : K -> Set ℓ -> Set ℓ`, read `E κ A` = 'A is epistemically available at standpoint κ'. The base is a plain indexed endofunctor (map only) — not a monad or comonad — so no return/reflect is assumed for free." factivity = "Factive knowledge and non-factive belief are distinct interfaces (FactiveModality vs BeliefModality), preventing belief from being read as knowledge." access = "`Access` adds a preorder over standpoints and an `AccessibleModality` whose `increase` transports availability along the preorder." -echo = "`EchoBridge` supplies a min-plus-graded loss/residue modality `Echo C y`, kept structurally distinct from epistemic availability; the two compose but never collapse (see ADR-005)." +echo = "`EchoBridge` supplies certified residue `Echo C y`; `BoundedEcho` separately adds a measured upper bound. Neither is identified with epistemic availability or made a resource instance (see ADR-005)." surreal = "`SurrealBridge` offers an abstract `SurrealAccess` carrier with a `GradedSurrealModality` and a finite-birthday tower `daySurrealAccess`, as instances of the abstract access interface rather than a full surreal-number library." proof-transport = "`ProofTransport` formalizes standpoint-indexed proof transport across trust boundaries with statuses Data/Code/Claimed/Receipt/Proof/ProofUnder and modes Public/Designated/IssuerMediated/EnvironmentMediated/OpaqueReceipt; no-smuggling is by construction (see ADR-006)." -modules = "Base, Warrant, Access, EchoBridge, SurrealBridge, Examples, ProofTransport, ProofTransportExample, with All re-exporting the development." +modules = "22 Agda source modules: map-only core and examples, proof transport, store/continuity, certified Echo and finite-day resource adapter, six application modules, and five scoped Kripke modules. All imports the full graph; the recursive gate checks every file." [ecosystem] # Real sibling projects in the estate. diff --git a/.machine_readable/descriptiles/NEUROSYM.a2ml b/.machine_readable/descriptiles/NEUROSYM.a2ml index b3de403..50cdd06 100644 --- a/.machine_readable/descriptiles/NEUROSYM.a2ml +++ b/.machine_readable/descriptiles/NEUROSYM.a2ml @@ -1,55 +1,53 @@ # NEUROSYM.a2ml — Neurosymbolic integration metadata -# Hypatia scanning + symbolic-rule configuration for epistemic-types. -# This is a small Agda formal-methods prototype, checked by `just check` -# (== `agda --no-libraries -i src src/EpistemicTypes/All.agda`, Agda 2.6.4.3). -# Rules below are right-sized to that single-tool library; honesty over breadth. +# Hypatia scanning boundary plus repository-owned Agda policy rules. +# Hypatia's active rule engine is Elixir under its lib/rules/ tree. This +# repository does not vendor those rules and does not claim an enabled Hypatia +# scan; its blocking proof authority remains Agda via scripts/check.sh. [metadata] project = "epistemic-types" version = "0.1.0" status = "prototype" -last-updated = "2026-06-15" +last-updated = "2026-11-01" author = "Jonathan D.A. Jewell (hyperpolymath) " [hypatia-config] scan-enabled = false scan-depth = "standard" # quick | standard | deep -report-format = "logtalk" +report-format = "json" # Hypatia CLI/AssailReport exchange format +rule-engine = "Hypatia Elixir rules (upstream lib/rules); no rules vendored here" scan-paths = [ "src/EpistemicTypes" ] file-globs = [ "*.agda" ] [symbolic-rules] -# Custom symbolic rules for this repository. -# Agda has no `believe_me`/`unsafeCoerce`; the honest analogues to flag are -# escape hatches and library coupling that would weaken the constructive, -# `--safe --without-K`, no-postulate, no-stdlib discipline of this repo. +# Repository-local syntactic guards. These are input policy for an optional +# Hypatia scan; tests/check-policy.sh and the Agda kernel are authoritative. rules = [ - { name = "no-postulate", pattern = "postulate", severity = "critical", note = "This repo postulates nothing. Any `postulate` is a silent axiom; laws must be fields or proofs." }, - { name = "no-terminating-pragma", pattern = "\\{-# TERMINATING #-\\}", severity = "critical", note = "Bypasses the termination checker; breaks the constructive honesty guarantee." }, - { name = "no-non-terminating-pragma", pattern = "\\{-# NON_TERMINATING #-\\}", severity = "critical", note = "Same escape hatch as TERMINATING; not used here and must not appear." }, - { name = "no-primTrustMe", pattern = "primTrustMe", severity = "critical", note = "Unsound equality witness; equivalent in spirit to believe_me. Must never appear." }, - { name = "no-trustMe", pattern = "trustMe", severity = "critical", note = "Library-level wrapper over primTrustMe; same prohibition." }, - { name = "no-no-positivity-check", pattern = "\\{-# NO_POSITIVITY_CHECK #-\\}", severity = "critical", note = "Disables the positivity checker; would admit non-strictly-positive (unsound) data." }, - { name = "no-no-termination-check", pattern = "\\{-# NO_TERMINATION_CHECK #-\\}", severity = "critical", note = "Legacy termination bypass; forbidden for the same reason as TERMINATING." }, - { name = "no-stdlib-import", pattern = "open import (Data|Relation|Function|Algebra|Category|Codata|Effect|Foreign|IO|Reflection|Tactic|Agda\\.Builtin\\.Reflection)\\b", severity = "high", note = "Repo builds with `agda --no-libraries`; only `Agda.Builtin.*` and `Agda.Primitive` are permitted. A standard-library import would not type-check under `just check` and breaks the self-contained guarantee." }, - { name = "no-unsafe-options", pattern = "\\{-# OPTIONS[^#]*--type-in-type", severity = "critical", note = "`--type-in-type` is inconsistent; the repo target is `--safe --without-K`." }, - { name = "echo-not-collapsed", pattern = "Echo .* = .* E ", severity = "medium", note = "Heuristic: Echo C y (certified residue and separately measured bounds) and E kappa A (epistemic availability) are distinct modalities. Their composition is meaningful; their identification is a modelling error. Manual review on hit." } + { name = "no-postulate", pattern = "postulate", severity = "critical", note = "Positive proof sources postulate nothing. Laws must be fields or proofs." }, + { name = "no-terminating-pragma", pattern = "\\{-# TERMINATING #-\\}", severity = "critical", note = "Termination-checker bypass; forbidden." }, + { name = "no-non-terminating-pragma", pattern = "\\{-# NON_TERMINATING #-\\}", severity = "critical", note = "Termination-checker bypass; forbidden." }, + { name = "no-primTrustMe", pattern = "primTrustMe", severity = "critical", note = "Unsound equality witness; forbidden." }, + { name = "no-trustMe", pattern = "trustMe", severity = "critical", note = "Library wrapper over primTrustMe; forbidden." }, + { name = "no-no-positivity-check", pattern = "\\{-# NO_POSITIVITY_CHECK #-\\}", severity = "critical", note = "Positivity-checker bypass; forbidden." }, + { name = "no-no-termination-check", pattern = "\\{-# NO_TERMINATION_CHECK #-\\}", severity = "critical", note = "Legacy termination-checker bypass; forbidden." }, + { name = "no-stdlib-import", pattern = "open import (Data|Relation|Function|Algebra|Category|Codata|Effect|Foreign|IO|Reflection|Tactic|Agda\\.Builtin\\.Reflection)\\b", severity = "high", note = "Core source is checked with --no-libraries; only Agda builtins/primitive and local modules are permitted." }, + { name = "no-unsafe-options", pattern = "\\{-# OPTIONS[^#]*--type-in-type", severity = "critical", note = "The source profile is --safe --without-K --cubical-compatible; type-in-type is forbidden." }, + { name = "echo-not-collapsed", pattern = "Echo .* = .* E ", severity = "medium", note = "Heuristic manual-review hit: Echo residue, measured resource bounds, and epistemic availability are distinct." } ] [symbolic-rules.notes] -# These are syntactic flags, not a proof of soundness. The real guarantee is -# that `just check` succeeds under {-# OPTIONS --safe --without-K #-} with no -# postulates and no libraries. Hypatia hits are advisory; `--safe` is the floor. -checker-of-record = "agda --no-libraries -i src src/EpistemicTypes/All.agda" -safe-flags = "--safe --without-K" +checker-of-record = "bash scripts/check.sh" +canonical-agda-profile = "--safe --without-K --cubical-compatible" +source-hardening = "--exact-split --no-sized-types --no-guardedness" +warning-boundary = "All warnings are errors except Agda 2.6.4.3's UnsupportedIndexedMatch category, narrowly disabled for Kripke.Belief's indexed relation elimination and the pinned external integration; no Cubical transport computation is claimed there." +trust-boundary = "Hypatia findings are advisory here. Agda proof gates and exact expected-rejection diagnostics block proof regressions." [neural-config] -# Neural pattern detection is not configured for this prototype. -# A formal Agda library is better served by the deterministic symbolic rules -# above and by the type-checker than by learned pattern matching. enabled = false +note = "No learned pattern model is configured for this formal library." [ci] -# CI checks core proofs, semantic rejections, pinned Echo correspondence and workflow/secret security. -# See AUDIT.adoc. Verification is local via `just check`. -enabled = false +hypatia-scan-enabled = false +proof-ci-enabled = true +proof-entry-point = "bash scripts/check.sh" +note = "Proof, rejection, canonical Echo, governance, CodeQL and secret-scanning workflows exist; see docs/ci-safety.adoc. No Hypatia scan result is claimed." diff --git a/.machine_readable/descriptiles/PLAYBOOK.a2ml b/.machine_readable/descriptiles/PLAYBOOK.a2ml index 56d4f9b..52b2847 100644 --- a/.machine_readable/descriptiles/PLAYBOOK.a2ml +++ b/.machine_readable/descriptiles/PLAYBOOK.a2ml @@ -5,7 +5,7 @@ [metadata] version = "0.1.0" status = "prototype" -last-updated = "2026-06-15" +last-updated = "2026-11-01" repo = "hyperpolymath/epistemic-types" single-tool = "agda" @@ -13,27 +13,27 @@ single-tool = "agda" method = "library (no deploy)" target = "library" notes = "Constructive Agda formalization consumed by reading and re-checking the source. Nothing is built into an artifact, served, or shipped. Downstream use = import the modules and typecheck." -ci = "not enabled (see AUDIT.adoc)" +ci = "Proof and security CI enabled; see docs/ci-safety.adoc" [gate] # The single source of truth for 'is the library healthy?'. command = "just check" -expands-to = "agda --no-libraries -i src src/EpistemicTypes/All.agda" +expands-to = "tests/check-policy.sh; tests/check-proofs.sh over all 22 source modules; tests/check-rejections.sh over all 13 fixtures" agda-version = "2.6.4.3" -options = "--safe --without-K" -dependencies = "none (only Agda.Builtin.* / Agda.Primitive; no standard library; no postulates)" -green-means = "All.agda re-exports every module and the whole library typechecks." +options = "--safe --without-K --cubical-compatible; source hardening --exact-split --no-sized-types --no-guardedness" +dependencies = "core: Agda builtins/primitive and local modules only; optional canonical integration pins Echo source and stdlib" +green-means = "Policy guard passes, every source module checks, and every enumerated malformed construction fails for its intended reason." [incident-response] # 'Incident' here = the library stopped typechecking. steps = [ "1. Read .machine_readable/descriptiles/STATE.a2ml for current status, assumptions, and the module list.", - "2. Run `just check` to reproduce the failure (same as `agda --no-libraries -i src src/EpistemicTypes/All.agda`).", - "3. Read the Agda error: it names the failing module under src/EpistemicTypes/ and the offending goal or type.", - "4. Open and inspect that failing module; fix the definition or the field standing in for a not-yet-derived law.", - "5. Re-run `just check` until green; the whole library must typecheck via All.agda." + "2. Run `just check` to reproduce the same policy, positive-proof and expected-rejection gates as core CI.", + "3. Identify whether the policy inventory, a positive module, or an intended rejection failed; missing tools/imports are failures, not evidence.", + "4. Fix the source or status record without weakening flags, widening the map-only API, or turning an assumption into a theorem.", + "5. Re-run `just check` until all three gates are green; update PROOF-STATUS.adoc when proof scope changes." ] -honesty-rule = "Never silence a failure with a postulate or by weakening --safe/--without-K. Laws appear as explicit fields when they are not derivable." +honesty-rule = "Never silence a failure with a postulate or by weakening --safe/--without-K/--cubical-compatible. Laws appear as explicit fields when they are not derivable." boundary-rule = "Do not collapse Echo C y (certified residue and separately measured bounds) into E κ A (standpoint/warrant/access). Their composition is meaningful; they are not the same modality." [release-process] @@ -43,17 +43,18 @@ steps = [ "3. Update CHANGELOG.adoc with the changes for this version.", "4. Tag the release at the green commit." ] -preconditions = "`just check` is green; no postulates introduced; --safe --without-K still hold." +preconditions = "`just check` and the pinned integration gate are green at the release revision; no postulates; canonical strict profile still holds." [maintenance-operations] gate = "`just check`" description = "`just check` is the maintenance gate. Any change to src/EpistemicTypes/** is only complete once `just check` is green again." routine = [ "After editing any module, run `just check`.", - "When adding a module, re-export it from EpistemicTypes.All so the gate covers it.", - "Keep modules small and typecheck frequently (incremental, one module at a time)." + "When adding a module, update the source graph, policy inventory, STATE module list and current counts; recursive checking does not depend on public re-export.", + "Keep modules small and typecheck frequently (incremental, one module at a time).", + "Keep PROOF-STATUS and PROOF-NEEDS aligned with exact theorem scope and external trust boundaries." ] -no-build-system = "There is no separate build, lint, test, container, or security pipeline beyond the typechecker; the proof obligation IS the test." +no-runtime = "There is no deployed service. Proof, rejection, policy, canonical correspondence, governance, CodeQL and secret-scanning gates are separate and must not be conflated." [ecosystem] # Sibling repos this library relates to (no automated coupling). diff --git a/.machine_readable/descriptiles/STATE.a2ml b/.machine_readable/descriptiles/STATE.a2ml index 574218e..cbcdfa8 100644 --- a/.machine_readable/descriptiles/STATE.a2ml +++ b/.machine_readable/descriptiles/STATE.a2ml @@ -1,7 +1,7 @@ [metadata] project = "epistemic-types" version = "0.1.0" -last-updated = "2026-10-05" +last-updated = "2026-11-01" status = "prototype" # prototype | active | paused | archived [project-context] @@ -16,20 +16,22 @@ phase = "design" # design | implementation | testing | maintenance | a maturity = "experimental" # experimental | alpha | beta | production | lts [constraints] -discipline = "Constructive. Compiles under {-# OPTIONS --safe --without-K #-}. No postulates. No Agda standard library (built with 'agda --no-libraries'; only Agda.Builtin.* / Agda.Primitive)." +discipline = "Constructive. Every first-party module declares --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness. No postulates or proof escape hatches. Core source uses no Agda standard library (agda --no-libraries; only Agda.Builtin.*, Agda.Primitive and local modules)." honesty-rule = "Laws appear as explicit fields when not derivable; lawful instances are added only after proving or explicitly assuming the laws. No smuggling." [boundaries] -secret-types = "Owner decision 2026-10-04: hyperpolymath/secret-types is the standalone home for secret types (D153: label-constrained flow with explicit declassification and type-family-map registration; D154: reuse an existing lattice two-point-first, prove noninterference, declassify only at explicit audited points). This repository adds no Secret API and no information-flow implementation; docs/secret-types.adoc is retained as the boundary/history note. epistemic-types#29 is resolved and stays closed. epistemic-types#32 was closed on 2026-10-05 as delivered here, with no transfer (none required); do not reopen it, transfer it, or duplicate it - the successor guard is epistemic-types#39. The standalone repository is no longer specification-only: at ccdcb3ec42792337a9ab6047e1f99de9d20a4f96 (2026-10-19) its proof gate is green, TINI at the two-point lattice and over a Lattice record are PROVEN, and declassification is not yet implemented. Pointers: docs/secret-types.adoc section Status update 2026-10-25, and docs/secret-types-transition-review-2026-10-05.adoc kept as history." +secret-types = "Owner decision 2026-10-04: hyperpolymath/secret-types is the standalone production home for secret types (D153/D154). This repository adds no Secret API, IFC implementation or confidentiality theorem; docs/secret-types.adoc is the boundary/history note. epistemic-types#29 stays closed; #32 was closed on 2026-10-05 as delivered here with no transfer; do not reopen/duplicate it (successor guard #39). Source-reviewed at secret-types f581f8295bdee854f76291ab884a16cc8114dc6f on 2026-11-01: generic TINI over a Lattice record/down-closed observers and the two-point instance are PROVEN in its ledger; termination-sensitive noninterference and declassification remain OPEN. No theorem is imported here." [build] checker = "Agda 2.6.4.3 (CI-matched)" command = "just check" entry-point = "scripts/check.sh — local agda when present, else 'guix shell -D -f build/guix.scm -- bash scripts/check.sh'" -expands-to = "bash tests/check-proofs.sh && bash tests/check-rejections.sh" +expands-to = "bash tests/check-policy.sh && bash tests/check-proofs.sh && bash tests/check-rejections.sh" dev-container = ".devcontainer/ — Debian 13 pinned to the same base image digest as CI, agda-bin=2.6.4.3-1+b2; postCreateCommand runs 'just check'" ci-entry-point = ".github/workflows/agda.yml asserts 'Agda version 2.6.4.3', then runs 'bash scripts/check.sh'" -aggregator = "src/EpistemicTypes/All.agda re-exports every module." +warning-policy = "-W error with only noUnsupportedIndexedMatch disabled: locally for Kripke.Belief's indexed relation elimination and at the pinned external integration boundary. No Cubical transport computation is claimed for those functions." +proof-status = "AGDA-VERIFIED; Mathesis Grade 3. Proof Safety run 41326349568 passed both core/rejection/policy and pinned integration jobs at checked revision bf9c75a38794d744ce466574e6323062e7d22533. Rocq/Lean/bridge legs remain open." +aggregator = "src/EpistemicTypes/All.agda imports the full source graph; the recursive gate separately checks every source file, including modules not publicly re-exported." [modules] # Agda modules under src/EpistemicTypes/. @@ -46,6 +48,11 @@ list = [ "EpistemicTypes.ContinuityExamples", "EpistemicTypes.EchoBridge", "EpistemicTypes.Examples", + "EpistemicTypes.Kripke.Belief", + "EpistemicTypes.Kripke.Dependence", + "EpistemicTypes.Kripke.Frame", + "EpistemicTypes.Kripke.Indexed", + "EpistemicTypes.Kripke.Residual", "EpistemicTypes.ProofTransport", "EpistemicTypes.ProofTransportExample", "EpistemicTypes.ReadConsistency", @@ -68,14 +75,19 @@ applications-sorted-row = "Rows as entries (index, distance, row sum), the All p applications-qcriterion = "Q and qBound over any OrderedGroup, the bound lemma qBound-≤-Q, the row lemma qBound-≤-suffix, claim weakening, and prefix/suffix composition." applications-rapidnj-skip = "Checkable (the exactness seam), scan state, skip evidence, the generated warrant and soundness map, the factive modality, the belief-only reading, and the declared-not-assumed cross-iteration obligation." applications-rapidnj-examples = "Executable integer check, refutation of an over-eager comparison, a worked four-taxon scan, and the runtime status mirror (Factive / Belief / Collapsed / SansFibre)." +kripke-indexed = "World-indexed modality/factivity/access records and the one-world reduction to the base Modality." +kripke-frame = "Frame and Box; constructive reflexive iff T, transitive iff 4, Euclidean implies 5, serial implies D. Converse 5/D are not claimed." +kripke-belief = "Two-world non-reflexive model with a warrant for a proposition false at the current world and a proof that no soundness map exists for that evidence." +kripke-residual = "Residual candidates as a Box and a three-world presence-without-identification witness." +kripke-dependence = "Local faithful mirror showing candidate-equivalent contexts can differ in proper dependence; identity with residual-evidence-types' owning record remains unproved." [route-to-mvp] milestones = [ { name = "Base indexed-endofunctor interface (E, Modality and law-fields)", completion = 100 }, { name = "Warrant / Access / EchoBridge / SurrealBridge formers", completion = 100 }, { name = "ProofTransport core (View, statuses, modes, transmit/verify)", completion = 100 }, - { name = "Concrete Kripke-style semantics", completion = 0 }, - { name = "Evidence-state and observation-rule examples", completion = 0 }, + { name = "Scoped constructive Kripke semantics and frame correspondences", completion = 100 }, + { name = "Residual-candidate and presence-without-identification examples", completion = 100 }, { name = "Richer day-bounded surreal fragments as SurrealAccess instances", completion = 0 }, { name = "Applications layer: RapidNJ Q-criterion bound and skip warrants", completion = 100 }, { name = "Rational (ℚ) instance and the common-denominator rescaling transport", completion = 0 }, @@ -84,8 +96,8 @@ milestones = [ [roadmap] items = [ - "Add concrete Kripke-style semantics.", - "Add evidence-state and observation-rule examples.", + "Extend the scoped Kripke fragment only with exact theorem statements; converse 5/D require explicit classical assumptions.", + "Re-prove the dependence mirror against residual-evidence-types' owning record before claiming correspondence.", "Add richer day-bounded surreal fragments as instances of the abstract SurrealAccess interface.", "Add lawful instances only after proving or explicitly assuming laws.", "Extend the echo bridge without importing a full graded comonad.", @@ -94,17 +106,17 @@ items = [ ] [progress-summary] -note = "Prototype. The base interface and all seventeen modules typecheck under 'just check' (Agda 2.6.4.3, --safe --without-K, --no-libraries, no postulates), against twelve rejection fixtures. The endofunctor/Modality formers, Warrant, Access transport, EchoBridge residue, SurrealBridge tower, ProofTransport, its K9-SVC/A2ML attestation example, and the applications layer (RapidNJ Q-criterion bound, generated skip warrants, discharged integer instance) are in place. Remaining work is semantics, lawful instances, and the rational/rescaling obligation — see [roadmap]." +note = "Prototype. Authoritative inventory: 22 source modules and 13 expected-rejection fixtures. The map-only core, explicit warrant/factivity boundary, proof transport, store consistency, certified Echo residue with separate measured bounds, finite-day surreal adapter, RapidNJ integer certificate, and scoped constructive Kripke semantics are implemented. The 2026-11-01 canonical profile is --safe --without-K --cubical-compatible; hosted receipt status and Mathesis grade are in PROOF-STATUS.adoc. Open work includes data-dependent warrant soundness, residual owning-record correspondence, lawful instances, rational/rescaling and update obligations, independent Rocq/Lean legs, and runtime refinement." [blockers-and-issues] # No active blockers. [critical-next-actions] actions = [ - "Add concrete Kripke-style semantics for the standpoint-indexed formers.", - "Add evidence-state and observation-rule worked examples.", + "Obtain and record the hosted Agda receipt for the explicit 2026-11-01 canonical profile.", + "Inventory exact propositions before any Rocq/Lean recheck; do not infer correspondence from names.", "Prove or explicitly assume modality laws before exposing lawful instances.", - "Extend the echo bridge without importing a full graded comonad.", + "Discharge data-dependent warrant, rational/rescaling, row-update, and cross-iteration obligations without widening the base API.", ] [ci] @@ -116,6 +128,9 @@ part-of = ["RSR Framework", "echo / epistemic formal-methods siblings"] siblings = [ { name = "echo-types", relation = "Agda loss-with-residue formalism; EchoBridge composes with it." }, { name = "ephapax", relation = "Sibling formal language; four-layer redesign carries echo obligations." }, + { name = "choreographic-types", relation = "External consumer of Warrant with scoped K-CUT proofs; no universal/local proof import." }, + { name = "residual-evidence-types", relation = "Production-operated early research neighbour with no stable API; local dependence mirror only." }, + { name = "secret-types", relation = "Standalone production home for confidentiality/TINI; no local Secret API or theorem." }, { name = "standards", relation = "Estate RSR/standards + k9-svc + a2ml tooling." }, { name = "a2ml + k9", relation = "Machine-readable + contractile tooling; the engineering target for ProofTransport (see .machine_readable/proof-transport/)." }, ] diff --git a/0-AI-MANIFEST.a2ml b/0-AI-MANIFEST.a2ml index 3d9f0ba..ecc7ace 100644 --- a/0-AI-MANIFEST.a2ml +++ b/0-AI-MANIFEST.a2ml @@ -4,7 +4,7 @@ title = "epistemic-types — universal AI agent entry point" version = "0.1.0" format = "a2ml" status = "prototype" -last-updated = "2026-10-04" +last-updated = "2026-11-01" [project] name = "epistemic-types" @@ -30,18 +30,19 @@ proof-transport-readme = ".machine_readable/proof-transport/README.adoc" readme = "README.adoc" explainme = "explainme.adoc" audit = "AUDIT.adoc" -format = "AsciiDoc (.adoc) is the default; existing lowercase doc filenames are canonical and are not renamed." +format = "AsciiDoc (.adoc) is the default. README.adoc is the overview, explainme.adoc the concise narrative, and EXPLAINME.adoc the detailed claim/evidence ledger; treat their exact casing as canonical." [invariants] -scm-files-location = ".machine_readable/ ONLY — a2ml and scm/Nickel/k9 files never live at repo root" +machine-readable-location = "Project specifications live under .machine_readable/. The root 0-AI-MANIFEST.a2ml universal pointer and coordination.k9 session entry point are the explicit operational exceptions." license = "MPL-2.0" build = "just check" -build-expansion = "bash scripts/check.sh → bash tests/check-proofs.sh && bash tests/check-rejections.sh" -agda-options = "{-# OPTIONS --safe --without-K #-} ; no postulates; no Agda standard library (only Agda.Builtin.* / Agda.Primitive)" +build-expansion = "bash scripts/check.sh → policy gate + all 22 source modules + all 13 expected rejections" +agda-options = "--safe --without-K --cubical-compatible plus source hardening --exact-split --no-sized-types --no-guardedness; -W error with UnsupportedIndexedMatch disabled only alongside an exact 23-source-span audit; no postulates; core imports only builtins/primitive/local modules" agda-version = "2.6.4.3" echo-distinction = "Do not collapse Echo C y and E κ A. Echo retains certified residues; epistemic types are standpoint/warrant/access modalities. Their composition is meaningful; they are not the same modality." ci = "Proof and security workflows configured; required merge checks are described in docs/ci-safety.adoc" -secret-types = "Owner decision 2026-10-04: hyperpolymath/secret-types is the standalone home for secret types (D153/D154). Do not add a Secret API or information-flow implementation here; docs/secret-types.adoc is the boundary/history note. epistemic-types#29 stays closed. Issue #32 was closed on 2026-10-05 as delivered here (no transfer); do not reopen, transfer, or duplicate it - the successor guard is #39. The standalone repository now carries a proved noninterference theorem (ccdcb3ec42792337a9ab6047e1f99de9d20a4f96, 2026-10-19); see docs/secret-types.adoc section Status update 2026-10-25." +proof-status = "AGDA-VERIFIED; Mathesis Grade 3. Canonical Proof Safety receipt 41326349568 at checked revision bf9c75a38794d744ce466574e6323062e7d22533. Independent Rocq/Lean/bridge legs remain open." +secret-types = "Owner decision 2026-10-04: hyperpolymath/secret-types is the standalone production home (D153/D154). Do not add a Secret API, IFC implementation or confidentiality theorem here. #29 stays closed; #32 closed on 2026-10-05 with no transfer and must not be reopened/duplicated (guard #39). Source-reviewed at standalone f581f8295bdee854f76291ab884a16cc8114dc6f on 2026-11-01: generic TINI and its two-point instance are PROVEN; termination-sensitive noninterference and declassification remain OPEN. No theorem is imported here." [first-run] dev-container = ".devcontainer/ — Debian 13 pinned to the same base image digest as CI, agda-bin=2.6.4.3-1+b2; postCreateCommand runs 'just check'." @@ -54,10 +55,21 @@ aggregator = "src/EpistemicTypes/All.agda" modules = [ "EpistemicTypes.Access", "EpistemicTypes.All", + "EpistemicTypes.Applications.IntegerModel", + "EpistemicTypes.Applications.OrderedGroup", + "EpistemicTypes.Applications.QCriterion", + "EpistemicTypes.Applications.RapidNJExamples", + "EpistemicTypes.Applications.RapidNJSkip", + "EpistemicTypes.Applications.SortedRow", "EpistemicTypes.Base", "EpistemicTypes.ContinuityExamples", "EpistemicTypes.EchoBridge", "EpistemicTypes.Examples", + "EpistemicTypes.Kripke.Belief", + "EpistemicTypes.Kripke.Dependence", + "EpistemicTypes.Kripke.Frame", + "EpistemicTypes.Kripke.Indexed", + "EpistemicTypes.Kripke.Residual", "EpistemicTypes.ProofTransport", "EpistemicTypes.ProofTransportExample", "EpistemicTypes.ReadConsistency", @@ -74,6 +86,9 @@ SurrealBridge = "SurrealAccess carrier plus GradedSurrealModality plus daySurrea Examples = "Worked instances of the abstract interfaces." ProofTransport = "Standpoint-indexed proof transport across trust boundaries." ProofTransportExample = "Sound Boolean certificate checks; valid acceptance, bad payload/artefact rejection, false-claim and holder-boundary impossibility." +Applications = "Six-module RapidNJ Q-criterion/skip-warrant layer with discharged integer instance and explicit rational/update obligations." +Kripke = "Five-module scoped constructive semantics: indexed Box/frame correspondences, non-factive model, residual candidates and dependence mirror." +ReadConsistency = "Pure store histories, current reads, cache staleness and explicit fact stability." [proof-transport] thesis = "Proofhood is standpoint-indexed. Transmission across a trust boundary moves bytes (von Neumann), not proofhood (Curry-Howard); a receiver recovers proofhood only with its OWN checker plus evidence." @@ -97,14 +112,14 @@ step-3 = "Read .machine_readable/descriptiles/META.a2ml for architecture and des step-4 = "Read .machine_readable/descriptiles/ECOSYSTEM.a2ml for ecosystem position and sibling repos." step-5 = "Read .machine_readable/descriptiles/AGENTIC.a2ml, NEUROSYM.a2ml, and PLAYBOOK.a2ml for agent guidance." step-6 = "Read README.adoc and explainme.adoc for the human-facing overview." -step-7 = "Run 'just check' (→ scripts/check.sh: local Agda or the Guix environment, or the dev container) to check every source module and semantic rejection fixture before and after changes." +step-7 = "Run 'just check' (→ scripts/check.sh: local Agda or Guix/dev container) to enforce policy, check all 22 source modules and validate all 13 expected rejections before and after changes." [policy] rules = [ "Preserve mathematical honesty: do not introduce postulates; laws appear as fields when not derivable.", - "Keep the build dependency-free: no Agda standard library; only Agda.Builtin.* / Agda.Primitive.", + "Keep core source dependency-free: no Agda standard library; only Agda.Builtin.*, Agda.Primitive and local modules. Keep the optional canonical integration pinned and separate.", "Keep modules small and type-check frequently with 'just check'.", - "Keep a2ml / Nickel / k9 files under .machine_readable/ only.", + "Keep project a2ml/Nickel/k9 specifications under .machine_readable/; retain only the universal 0-AI-MANIFEST.a2ml pointer and coordination.k9 session entry point at the root.", "License and SPDX changes are owner-manual; do not add LICENSE files or SPDX headers.", "Maintain owner-authorized proof and security CI; do not bypass failing checks.", "Secret types and information-flow control stay outside this repository (D153/D154; canonical specification in hyperpolymath/secret-types). Issue #32 is closed (2026-10-05, delivered here; no transfer): do not reopen, transfer, or duplicate it, and use the successor guard #39 for pointer updates (docs/secret-types.adoc section Status update 2026-10-25).", @@ -112,8 +127,11 @@ rules = [ [ecosystem] siblings = [ - { name = "echo-types", relation = "Agda loss-with-residue formalism; EpistemicTypes.EchoBridge composes with it." }, + { name = "echo-types", relation = "Canonical proof-relevant Echo sibling; optional pin checks representation and one-way lowering. Echo is not a resource instance." }, { name = "ephapax", relation = "Sibling formal language; four-layer redesign with echo obligations." }, + { name = "choreographic-types", relation = "External Warrant consumer with scoped K-CUT proofs; not a local proof import." }, + { name = "residual-evidence-types", relation = "Production-operated early research with no stable API; local mirror only." }, + { name = "secret-types", relation = "Standalone production confidentiality/TINI project; no local Secret API." }, { name = "standards", relation = "Estate RSR/standards plus k9-svc and a2ml tooling." }, { name = "a2ml", relation = "Machine-readable dialect; ProofTransport's engineering rendering target." }, { name = "k9", relation = "Contractile tooling; proof-transport.k9.ncl is a Kennel-leash datum for it." }, diff --git a/AFFIRMATION.adoc b/AFFIRMATION.adoc index 433d2d1..b032cb1 100644 --- a/AFFIRMATION.adoc +++ b/AFFIRMATION.adoc @@ -3,13 +3,17 @@ = AFFIRMATION — epistemic-types, as of 2026-06-16 :toc: macro -NOTE: The dated historical affirmation below is superseded in scope by the -2026-09-07 repairs. Proof transport now entails its explicit Meaning; -ReadConsistency now models store histories with contents agreement; Echo now -uses certified residues, source compatibility, migration laws, and separate -measured bounds. Neither these proofs nor the earlier affirmation establishes -external-store or runtime refinement. Current evidence and limitations are in -`PROOF-STATUS.adoc` and `docs/continuity-foundations.adoc`. +NOTE: This is a frozen 2026-06-16 receipt, not current inventory. Later work +supersedes its ten-module count, licence/CI observations, and statement that +Kripke semantics is absent. The current tree has 22 source modules, 13 +expected-rejection fixtures, and a scoped constructive Kripke semantics. The +2026-09-07 repairs also made proof transport entail explicit `Meaning`, tied +reads to store histories, and replaced unconstrained Echo tokens with certified +residues, migration laws, and separate measured bounds. Do not silently read +those later facts back into the historical attestation. Current evidence, +Mathesis grade, and limitations are in `PROOF-STATUS.adoc`, `PROOF-NEEDS.adoc`, +`docs/kripke-status-2026-10-12.adoc`, and +`docs/continuity-foundations.adoc`. :toclevels: 2 _the No-Bullshit file: what we affirm was true and checkable at this moment_ diff --git a/AUDIT.adoc b/AUDIT.adoc index 355eeb9..e1054f9 100644 --- a/AUDIT.adoc +++ b/AUDIT.adoc @@ -1,5 +1,5 @@ = epistemic-types: proof and repository safeguards -:revdate: 2026-09-07 +:revdate: 2026-11-01 :toc: == Current scope @@ -18,11 +18,18 @@ The owner authorized proof/security CI and protected-main enforcement on billing incident are superseded. Existing GitHub workflows already run; their current proof coverage is extended by this change. -* Every module under `src/EpistemicTypes/` -- seventeen at the time of writing, - including the applications layer -- is checked with Agda 2.6.4.3, safe mode, - without-K, internal double checking and warnings as errors. Each source - module is checked. -* Twelve deliberate rejection fixtures must fail for their intended type mismatch. +* Every one of the 22 modules under `src/EpistemicTypes/` -- core, + applications, and Kripke -- is checked with Agda 2.6.4.3 under explicit + `--safe --without-K --cubical-compatible`, internal double checking and + warnings as errors. The `UnsupportedIndexedMatch` category is accepted only + at the 23 exact source spans in `tests/check-proofs.sh`; no Cubical + transport-computation claim is made for those eliminations. +* Thirteen deliberate rejection fixtures must fail for their intended type + mismatch. +* The policy gate enforces exact source/rejection/integration path manifests, + exactly one complete strict pragma per module, the standalone import + boundary, zero escape hatches, fail-closed searches, and a planted-postulate + negative control. * Canonical Echo residue correspondence is checked against pinned sibling source. * CodeQL analyzes Actions workflows, and the shared scanner checks secrets. * Main receives changes through PRs with required proof/security checks. Signed diff --git a/CITATION.cff b/CITATION.cff index 4e89eb7..04366cf 100644 --- a/CITATION.cff +++ b/CITATION.cff @@ -2,7 +2,7 @@ cff-version: 1.2.0 message: "If you use this software, please cite it as below." type: software title: "Epistemic Types" -abstract: "Constructive Agda prototype for standpoint-indexed epistemic modalities, separating knowledge (factive) from belief and warrant. Provides a tropical-graded bridge from standpoint access to echo-type residues, and a compositional proof-transport calculus with a no-smuggling guarantee across trust boundaries." +abstract: "Constructive Agda prototype for standpoint-indexed epistemic modalities, separating factive knowledge from belief and warrant. It provides certified Echo residues with separately measured resource bounds, a finite-day access adapter, scoped constructive Kripke semantics, and proof transport sound relative to an explicit claim meaning across trust boundaries." authors: - family-names: "Jewell" given-names: "Jonathan D.A." diff --git a/CODE_OF_CONDUCT.adoc b/CODE_OF_CONDUCT.adoc index 556f73f..c9b64a1 100644 --- a/CODE_OF_CONDUCT.adoc +++ b/CODE_OF_CONDUCT.adoc @@ -45,8 +45,9 @@ successes affected by our mistakes - Learning from the experience and avoiding repetition - Respecting others’ time and attention - Staying on topic in project spaces - Following project conventions (this is a -`+--safe --without-K+` Agda library with no postulates and no standard -library; corrections and proofs should preserve that discipline) +`+--safe --without-K --cubical-compatible+` Agda library with no postulates +and no standard-library imports in core source; corrections and proofs should +preserve the complete strict profile) *Accessibility* - Using plain language and avoiding unnecessary jargon - Providing alt text for images and transcripts for audio/video - Being diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index 84946b8..d8d6a1b 100644 --- a/EXPLAINME.adoc +++ b/EXPLAINME.adoc @@ -30,10 +30,12 @@ A warrant records the type of evidence for a claim without assuming the evidence ____ How this is implemented:: -`link:src/EpistemicTypes/Warrant.agda[]` defines `Warrant κ A` (type of evidence tokens), `Epi κ A` (token + warrant), and `SoundWarrant` (separate interface adding `soundness : Epi κ A → A`). +`link:src/EpistemicTypes/Warrant.agda[]` defines `Warrant K κ A` (type of +evidence tokens), `Epi K κ A` (token + warrant), and `SoundWarrant` (separate +interface adding `sound : Warrant.Evidence warrant → A`). Caveat:: -`SoundWarrant` is an optional interface. Nothing in the core forces warrants to be sound. This is the right default for security/attestation use cases where the receiver must verify locally, but it means `Epi κ A` cannot be used as a drop-in replacement for `A` without assuming `SoundWarrant`. +`SoundWarrant` is an optional interface. Nothing in the core forces warrants to be sound. This is the right default for security/attestation use cases where the receiver must verify locally, but it means `Epi K κ A` cannot be used as a drop-in replacement for `A` without a `SoundWarrant` for the concrete warrant. === Accessibility is a preorder with transport @@ -147,7 +149,11 @@ row-insertion update and cross-iteration bound reuse. [CAUTION] ==== -**No Kripke semantics.** The prototype defines the syntactic/type-theoretic interfaces for modalities but does not model them against a Kripke frame semantics. This is the largest open theoretical gap. +**Kripke scope is deliberately limited.** `src/EpistemicTypes/Kripke/` now +implements world-indexed `Box`, constructive T/4 correspondences, forward 5/D, +a non-factive model, a residual-candidate frame, and a dependence mirror. It is +not a complete epistemic logic; converse 5/D, data-dependent warrant soundness, +and the cross-repository dependence correspondence remain open. ==== [CAUTION] @@ -185,6 +191,21 @@ row-insertion update and cross-iteration bound reuse. | `src/EpistemicTypes/Access.agda` | Preorder accessibility + transport +| `src/EpistemicTypes/Kripke/Indexed.agda` +| World-indexed modalities and the one-world reduction + +| `src/EpistemicTypes/Kripke/Frame.agda` +| `Box`; T and 4 in both constructive directions; Euclidean-to-5 and serial-to-D + +| `src/EpistemicTypes/Kripke/Belief.agda` +| Concrete non-factive `Warrant` and refutation of its soundness map + +| `src/EpistemicTypes/Kripke/Residual.agda` +| Residual-candidate `Box` and presence without identification + +| `src/EpistemicTypes/Kripke/Dependence.agda` +| Candidate-equivalent contexts whose proper dependence differs, in the local mirror + | `src/EpistemicTypes/SurrealBridge.agda` | BoundedEcho resource-bound weakening, with GradedSurrealModality as an explicit interface and finite daySurrealAccess @@ -193,4 +214,76 @@ row-insertion update and cross-iteration bound reuse. | `src/EpistemicTypes/ProofTransportExample.agda` | Sound Boolean verification, false-claim rejection, and holder-boundary counterexample + +| `tests/check-policy.sh` +| Inventory/profile/import/escape-hatch guards and the generated `--safe` negative control + +| `tests/check-rejections.sh` +| Exact manifest and intended diagnostics for all 13 expected rejections +|=== + +[[proof-ledger]] +== Proof Ledger + +The detailed theorem inventory is link:PROOF-STATUS.adoc[]. These rows group +that inventory by trust boundary rather than pretending that one successful +command proves an external implementation. + +[cols="2,1,2,2,2", options="header"] +|=== +| Obligation | Status | Checker (version, flags) | Where | Trust boundary + +| Map-only modal/warrant/access separation +| proven +| Agda 2.6.4.3, `--safe --without-K --cubical-compatible`, builtins only +| `src/EpistemicTypes/{Base,Warrant,Access,Examples}.agda` +| Records prove only their stated fields; concrete law instances remain separate + +| Proof-transport semantic soundness +| proven +| Agda 2.6.4.3, `--safe --without-K --cubical-compatible`, builtins only +| `src/EpistemicTypes/ProofTransport*.agda` +| Relative to the supplied `Meaning`, checker, and acceptance-soundness proof + +| Store/retention/resource model +| proven +| Agda 2.6.4.3, `--safe --without-K --cubical-compatible`, builtins only +| `ReadConsistency.agda`, `EchoBridge.agda`, `SurrealBridge.agda` +| No external store, scheduler, physical measure, or runtime refinement + +| RapidNJ integer certificate +| proven +| Agda 2.6.4.3, `--safe --without-K --cubical-compatible`, builtins only +| `src/EpistemicTypes/Applications/` +| Rational/rescaling, insertion, and cross-iteration obligations remain open + +| Scoped constructive Kripke semantics +| proven +| Agda 2.6.4.3, `--safe --without-K --cubical-compatible`, builtins only +| `src/EpistemicTypes/Kripke/` +| Not completeness; no converse 5/D or data-dependent global warrant soundness + +| Residual dependence correspondence to the owning sibling record +| argued +| — +| `Kripke/Dependence.agda`, `docs/kripke-status-2026-10-12.adoc` +| The local mirror is checked; identity with the sibling's current record is not + +| Semantic rejection controls +| tested-only +| Agda 2.6.4.3; expected exit 42 and per-fixture diagnostic +| `tests/check-rejections.sh`, `tests/reject/` +| Rejection tests do not replace positive theorems + +| Pinned canonical Echo representation/lowering correspondence +| tested-only +| Agda 2.6.4.3 + stdlib 2.1 + pinned Echo source +| `tests/integration/CanonicalEcho.agda` +| Pinned source correspondence only; no full sibling or runtime equivalence + +| Rocq and Lean theorem rechecks and statement bridges +| open +| — +| `PROOF-NEEDS.adoc` +| Required for Mathesis Grade 2 or reconciliation; none claimed |=== diff --git a/GOVERNANCE.adoc b/GOVERNANCE.adoc index a992736..459e2e3 100644 --- a/GOVERNANCE.adoc +++ b/GOVERNANCE.adoc @@ -1,4 +1,5 @@ = Governance Model +:revdate: 2026-11-01 :toc: preamble This document describes how `epistemic-types` (`hyperpolymath/epistemic-types`) @@ -16,9 +17,9 @@ model is intentionally lightweight and matches the size of the project. * Proposals, issues, and pull requests are welcome and are reviewed on technical merit. * Decisions are recorded in the open, through GitHub issues, pull requests, - and `CHANGELOG.md`. + and `CHANGELOG.adoc`. -The project's stewardship bias is the same one stated in `readme.adoc`: it +The project's stewardship bias is the same one stated in `README.adoc`: it **favours mathematical honesty over a large API**. Governance exists mainly to protect that bias. @@ -30,8 +31,10 @@ protect that bias. | **Honesty over surface area** | A change that adds convenience but hides an unproved assumption is declined. - Postulates and a dependence on the Agda standard library are out of scope by - design (the build runs `agda --no-libraries` under `--safe --without-K`). + Postulates and a standard-library dependency in core source are out of scope + by design (the core gate runs `agda --no-libraries` under + `--safe --without-K --cubical-compatible`). The optional canonical-Echo + integration is pinned and checked separately. | **Stewardship, not gatekeeping** | The maintainer has the final say but prefers to merge well-scoped, honest @@ -42,7 +45,7 @@ protect that bias. them. | **Transparency** -| Significant decisions are documented in the issue, PR, or `CHANGELOG.md`. +| Significant decisions are documented in the issue, PR, or `CHANGELOG.adoc`. | **Open contribution** | Anyone may fork and open a pull request. @@ -94,7 +97,8 @@ checked locally, never assumed. === Routine decisions -* Documentation fixes (in `readme.adoc`, `explainme.adoc`, or the other docs) +* Documentation fixes (in `README.adoc`, `explainme.adoc`, `EXPLAINME.adoc`, + or the other docs) * Small proof clarifications that keep the same statements * Typos, comment fixes, formatting @@ -112,7 +116,7 @@ checked locally, never assumed. . Open an issue describing the change and the mathematics it commits to. . Discuss; the maintainer checks it against the "honesty over API" bias and - against what `readme.adoc` lists as *intentionally unformalized*. + against what `README.adoc` lists as *intentionally unformalized*. . The maintainer decides and records the rationale in the issue or PR. === Structural decisions @@ -122,8 +126,8 @@ checked locally, never assumed. * Ownership transfer **Process:** the maintainer decides, and the decision is recorded in -`CHANGELOG.md`. Licence and SPDX matters are handled manually by the owner and -are out of scope for automated changes. +`CHANGELOG.adoc`. Licence and SPDX declarations are owner-managed and must not +be changed without explicit owner instruction. == Contribution lifecycle @@ -133,12 +137,13 @@ are out of scope for automated changes. | **Idea** | Open an issue. Worth checking the *roadmap* and *what remains intentionally - unformalized* sections of `readme.adoc` first — some omissions are deliberate. + unformalized* sections of `README.adoc` first — some omissions are deliberate. | **Development** -| Fork, implement, and make it type-check: `just check` - (i.e. `agda --no-libraries -i src src/EpistemicTypes/All.agda`, Agda 2.8.0). - No postulates; no Agda standard library. +| Fork, implement, and run `just check` under the CI-matched Agda 2.6.4.3. + The gate enforces policy, checks all 22 source modules under explicit + `--safe --without-K --cubical-compatible`, and validates all 13 expected + rejections. No postulates; no Agda standard library in core source. | **Review** | Open a PR. The maintainer reviews on a best-effort basis (this is a personal @@ -148,8 +153,8 @@ are out of scope for automated changes. | The maintainer merges or requests changes. | **Release** -| The maintainer tags and updates `CHANGELOG.md`. There is no automated release - pipeline. +| The maintainer tags and updates `CHANGELOG.adoc`. There is no automated + release pipeline. |=== == Conflict resolution @@ -161,13 +166,12 @@ are out of scope for automated changes. == Project policies -* **Licence:** the repository is the owner's sole work and is classified - MPL-2.0 at the estate level. The working tree is currently SPDX-free by - choice; licence files and SPDX headers are added manually by the owner and - are not part of automated changes. See `AUDIT.adoc`. -* **Code of conduct:** see `CODE_OF_CONDUCT.md`. -* **Security:** see `SECURITY.md`. -* **Contributing:** see `CONTRIBUTING.md`. +* **Licence:** MPL-2.0 for code and CC-BY-SA-4.0 where marked for documentation. + The checked-in licence and SPDX declarations are owner-managed. See + `AUDIT.adoc`. +* **Code of conduct:** see `CODE_OF_CONDUCT.adoc`. +* **Security:** see `SECURITY.adoc`. +* **Contributing:** see `.github/CONTRIBUTING.md`. == Repository conventions @@ -179,15 +183,16 @@ are out of scope for automated changes. | `just check` is the single source of truth. A change that does not type-check is not merged. -| **No postulates, no stdlib** -| The formalization stays constructive and self-contained - (`Agda.Builtin.*` / `Agda.Primitive` only). +| **No postulates, no core stdlib** +| The core formalisation stays constructive and standalone + (`Agda.Builtin.*`, `Agda.Primitive`, and local modules only). The optional + sibling integration is kept outside that core boundary. | **Docs** -| AsciiDoc (`.adoc`) is the default. Existing docs keep their lowercase names - (`readme.adoc`, `explainme.adoc`). Only `CONTRIBUTING.md`, - `CODE_OF_CONDUCT.md`, `SECURITY.md`, and `CHANGELOG.md` are Markdown, for - GitHub community-health recognition. +| AsciiDoc (`.adoc`) is the default. `README.adoc` is the project overview; + `explainme.adoc` is the concise narrative; `EXPLAINME.adoc` is the detailed + claim/evidence ledger. The contributing guide remains Markdown under + `.github/`. | **Machine-readable** | `a2ml` + Nickel/`k9` artefacts live under `.machine_readable/`, including the @@ -195,32 +200,35 @@ are out of scope for automated changes. `.machine_readable/proof-transport/`. | **CI/CD** -| Not enabled. There are no GitHub Actions workflows or status badges; see - `AUDIT.adoc` for the reasons. +| Proof and security workflows are enabled. The `Proof Safety` workflow pins + Agda 2.6.4.3 and runs the canonical gate; branch-protection expectations are + recorded in `AUDIT.adoc` and `docs/ci-safety.adoc`. |=== == Ecosystem position `epistemic-types` is a sibling, not a dependency, of the related estate -formalizations. The `EchoBridge` module is written so it can compose with -`echo-types` (the loss-with-residue formalism) without importing it; `ephapax` -shares the echo-obligation framing; the `a2ml`/`k9` tooling in `standards` is -the engineering target for `ProofTransport`. Governance of those repositories -is separate and lives in their own `GOVERNANCE` documents. +formalizations. `EchoBridge` owns a local certified-residue model, while the +optional pinned integration checks representation and one-way lowering against +`echo-types`; Echo is not a resource instance. `ephapax` shares the +Echo-obligation framing; the `a2ml`/`k9` tooling in `standards` is the +engineering target for `ProofTransport`. Governance and proof responsibilities +of sibling repositories remain separate. == Governance evolution If the project grows, this model may change — for example by adding a co-maintainer or a trusted reviewer (see *graduated trust* above). Any such -change is itself a structural decision and is recorded in `CHANGELOG.md`. +change is itself a structural decision and is recorded in `CHANGELOG.adoc`. == See also -* link:readme.adoc[readme] — what the prototype is and how to type-check it -* link:explainme.adoc[explainme] — the longer-form explanation +* link:README.adoc[README] — what the prototype is and how to type-check it +* link:explainme.adoc[explainme] — concise narrative explanation +* link:EXPLAINME.adoc[EXPLAINME] — detailed claims and evidence ledger * link:.github/CONTRIBUTING.md[Contributing] -* link:CODE_OF_CONDUCT.md[Code of Conduct] -* link:SECURITY.md[Security policy] +* link:CODE_OF_CONDUCT.adoc[Code of Conduct] +* link:SECURITY.adoc[Security policy] * link:AUDIT.adoc[Audit] — build, CI, and licence status == Changelog diff --git a/Justfile b/Justfile index ceb8e7a..0e043c4 100644 --- a/Justfile +++ b/Justfile @@ -3,6 +3,9 @@ check: bash scripts/check.sh # Individual gates (also invoked by scripts/check.sh and by CI). +check-policy: + bash tests/check-policy.sh + check-proofs: bash tests/check-proofs.sh @@ -11,7 +14,7 @@ check-rejections: # Optional integration gate: actual echo-types checkout and stdlib source. check-canonical echo_root stdlib_src: - agda --no-libraries --safe --without-K --double-check --ignore-interfaces -W error -W noUnsupportedIndexedMatch -i src -i tests/integration -i '{{echo_root}}/proofs/agda' -i '{{stdlib_src}}' tests/integration/CanonicalEcho.agda + agda --no-libraries --safe --without-K --cubical-compatible --double-check --ignore-interfaces -W error -W noUnsupportedIndexedMatch -i src -i tests/integration -i '{{echo_root}}/proofs/agda' -i '{{stdlib_src}}' tests/integration/CanonicalEcho.agda # Build/test/validate include positive proofs and semantic rejection controls. build: check diff --git a/MAINTAINERS.adoc b/MAINTAINERS.adoc index 9176f99..8b70c66 100644 --- a/MAINTAINERS.adoc +++ b/MAINTAINERS.adoc @@ -1,4 +1,5 @@ = Maintainers +:revdate: 2026-11-01 :toc: preamble Maintainers of `epistemic-types` — a small Agda formalization of @@ -23,18 +24,23 @@ lead maintainer. * *Core interface* (`Base`, `Warrant`, `Access`) — the indexed endofunctor `E : K -> Set ℓ -> Set ℓ` and its lawful / factive / belief / return variants; keeping the base interface honestly `map`-only. -* *Echo + Surreal bridges* (`EchoBridge`, `SurrealBridge`) — the min-plus - graded loss/residue `Echo r A`, kept distinct from `E κ A`, and the - graded surreal access tower. Cross-checked against sibling `echo-types`. +* *Echo + finite-day resource bridge* (`EchoBridge`, `SurrealBridge`) — + certified residue `Echo C y`, separately measured `BoundedEcho`, and the + finite-day access tower, all kept distinct from `E κ A`. The optional + representation/lowering integration is pinned to sibling `echo-types`. +* *Kripke semantics* (`Kripke/*`) — preserve the exact constructive T/4/5/D + scope, non-factive countermodel, residual frame, and local dependence mirror; + do not upgrade external warrant results into global local soundness. * *Proof transport* (`ProofTransport`, `ProofTransportExample`) — the standpoint-indexed transport of attestations across trust boundaries (statuses, transmit/verify, no-smuggling), plus its a2ml/k9 engineering rendering under `.machine_readable/proof-transport/`. -* *Build + honesty invariants* — that `just check` stays green - (`agda --no-libraries -i src src/EpistemicTypes/All.agda`, Agda 2.8.0), - under `--safe --without-K`, with no postulates and no standard library. -* *Documentation* — `readme.adoc`, `explainme.adoc`, and the machine-readable - 6a2 / contractile descriptors. +* *Build + honesty invariants* — that `just check` stays green under Agda + 2.6.4.3 and explicit `--safe --without-K --cubical-compatible`: policy + guard, all 22 source modules, all 13 intended rejections, no postulates, and + no standard-library import in core source. +* *Documentation* — `README.adoc`, `explainme.adoc`, `EXPLAINME.adoc`, and the + machine-readable a2ml / contractile descriptors. == Contribution Process @@ -44,7 +50,7 @@ Contributions are welcome via: 2. *Pull Requests* — submit changes for review. Every change must keep `just check` green and preserve the honesty -invariants (no postulates, no stdlib, `--safe --without-K`). All +invariants (no postulates, no core stdlib, canonical strict Agda profile). All contributions are reviewed by the lead maintainer. == Decision Making @@ -61,8 +67,9 @@ maintainer at mailto:j.d.a.jewell@open.ac.uk[j.d.a.jewell@open.ac.uk]. == See Also -* link:readme.adoc[Readme] -* link:explainme.adoc[Explainme] +* link:README.adoc[README] +* link:explainme.adoc[Concise explanation] +* link:EXPLAINME.adoc[Claims and evidence ledger] * link:.github/CONTRIBUTING.md[Contributing Guide] -* link:CODE_OF_CONDUCT.md[Code of Conduct] -* link:AUDIT.adoc[Audit] — CI is not enabled; see the audit for rationale. +* link:CODE_OF_CONDUCT.adoc[Code of Conduct] +* link:AUDIT.adoc[Audit] — proof/security CI and repository safeguards. diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc new file mode 100644 index 0000000..a4c9310 --- /dev/null +++ b/PROOF-NEEDS.adoc @@ -0,0 +1,103 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += epistemic-types — proof needs +:revdate: 2026-11-01 +:toc: + +This queue records only obligations that remain relevant to this repository. +It does not widen the map-only API, merge independent type families, or import +sibling research merely to make a status table look complete. Completed +results and exact limits are in link:PROOF-STATUS.adoc[]. + +== P0 — current verification profile + +[cols="1,3,1",options="header"] +|=== +| ID | Obligation | Status +| P0-1 | Run all 22 source modules with Agda 2.6.4.3 under explicit +`--safe --without-K --cubical-compatible`, double checking, no libraries, no +interfaces, and warnings as errors except the exact-location-audited +`UnsupportedIndexedMatch` transport-computation manifest | CLOSED — run +`41326349568`, revision `bf9c75a`; exact 23-span audit added on 2026-11-01 and +awaiting its final-head hosted receipt +| P0-2 | Run all 13 rejection fixtures and require the intended type mismatch, +Agda exit 42, and no import/tool failure | CLOSED — run `41326349568` +| P0-3 | Run the proof-policy inventory, banned-construct/import checks, and the +planted-postulate negative control | CLOSED — run `41326349568` +| P0-4 | Recheck pinned canonical Echo correspondence under the explicit profile +| CLOSED — run `41326349568` +|=== + +Closing P0 establishes Mathesis Grade 3 for the checked Agda revision. It does +not establish independent cross-prover agreement. + +== P1 — theorem-level independent rechecks + +The estate theory policy requires theorem-by-theorem Rocq and Lean legs. These +must start from exact propositions, not matching filenames or theorem names. + +[cols="1,3,1",options="header"] +|=== +| ID | Obligation | Status +| P1-1 | Assign stable theorem IDs and record exact Agda propositions, +premises, universes, source revision, Agda version, and imports | OPEN +| P1-2 | Re-prove or transport each selected theorem into Rocq without Mathlib +or unrecorded axioms; record route and checker receipt | OPEN / NOT-INVENTORIED +| P1-3 | Re-prove or transport each selected theorem into Lean without Mathlib +or unrecorded axioms; record route and checker receipt | OPEN / NOT-INVENTORIED +| P1-4 | Check proposition correspondence, including equality, universe, +modality, totality, and assumption translations | BRIDGE-PENDING +| P1-5 | Record every residual assumption and quarantine any mismatch rather +than weakening the Agda statement | OPEN +|=== + +No Grade 2i, Grade 2ii, Grade 1, or `RECONCILED` claim is made until the +applicable rows close. + +== P2 — local mathematical obligations + +[cols="1,3,1",options="header"] +|=== +| ID | Obligation | Status +| P2-1 | Soundness for data-dependent warrants, with the evidence-to-claim map +proved for each concrete source of evidence | OPEN +| P2-2 | Re-prove the dependence result against residual-evidence-types' owning +record if an external identity/correspondence is to be claimed | OPEN +| P2-3 | Rational `OrderedGroup`/order instance or a common-denominator +rescaling theorem connecting rational RapidNJ input to the checked integer +certificate | OPEN +| P2-4 | Row-insertion preservation and cross-iteration reuse of the RapidNJ +skip bound | OPEN +| P2-5 | Any desired converse of modal 5 or D, with its classical assumptions +made explicit | OPEN +| P2-6 | Any law-bearing modality instance beyond the existing concrete +examples; laws must be proved or remain explicit fields | OPEN +|=== + +== P3 — correspondence and implementation obligations + +[cols="1,3,1",options="header"] +|=== +| ID | Obligation | Status +| P3-1 | Authoritative external-store refinement for `ReadConsistency` | OPEN +| P3-2 | Runtime refinement for proof transport, including the checker, +artefact, holder, and trust-boundary semantics | OPEN +| P3-3 | Scheduler/resource interpretation for measured Echo bounds | OPEN +| P3-4 | Any full Conway-surreal or physical-cost interpretation | OPEN +| P3-5 | Full graded-comonad/graded-loss correspondence | OPEN +|=== + +None of P3 follows from a model typecheck. Echo retention, epistemic +availability, and resource accounting stay separate unless an explicit bridge +is proved. + +== Explicit non-obligations + +The following are not scheduled work for this repository: + +* generic `bind` or `extract` for `E`; +* identifying Echo with a resource instance; +* confidentiality labels or noninterference (owned by standalone + `hyperpolymath/secret-types`); +* stabilising residual-evidence-types' API from here; +* extending choreographic-types' K-CUT fragment from this repository; +* claiming that externally reported proofs are local rechecks. diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc index e766da1..9b2a7de 100644 --- a/PROOF-STATUS.adoc +++ b/PROOF-STATUS.adoc @@ -1,112 +1,259 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 -= epistemic-types — Proof Status += epistemic-types — proof status +:revdate: 2026-11-01 :toc: +:sectnums: [abstract] -Verification status of the epistemic-types Agda formalisation. The whole library -**type-checks under `--safe`** with **zero postulates** and is fully -self-contained (`--no-libraries`: it imports only `Agda.Builtin.*` / -`Agda.Primitive`). This records a reproduced `agda` run, not a "looks fine" reading. - -== Applications layer — 2026-09-27 - -`src/EpistemicTypes/Applications/` adds the first worked application: the -per-row Q-criterion bound used by RapidNJ when searching for the -neighbour-joining minimum. Five modules and one example module pass the same -gate (`--safe --without-K --no-libraries --double-check -W error`, no -postulates): - -* `QCriterion.qBound-≤-Q` proves the row bound over an arbitrary - `OrderedGroup`, using only reflexivity, transitivity, monotone addition, - antitone negation and `Nat`-indexed scaling -- no ring law, no multiplication - or division of carrier elements. -* `RapidNJSkip` generates a warrant from a skip certificate (sorted-row - invariant, running-maximum invariant, accepted exact check) and proves - `skip-known`: the skipped quadrant's entries cannot beat the incumbent. The - soundness map is `FactiveModality.reflect = sound-epi`; without it the same - run is belief (`no-receipt-reflection`). -* `IntegerModel` discharges the arithmetic budget for the integers, and - `RapidNJExamples` turns `dec-≤ℤ` into a `Checkable`, runs a worked four-taxon - scan by computation, and refutes an over-eager comparison - (`no-always-true`). -* One new rejection fixture (`UncheckedSkip`) refuses a recorded check that the - numbers do not meet. - -Not claimed: any rational (ℚ) instance, the rescaling transport from a rational -matrix to its common-denominator integer form, the row-insertion update that -maintains the invariants, and cross-iteration bound reuse. These are stated as -obligations in link:docs/applications/rapidnj-q-criterion.adoc[]. - -== Current continuity-foundations correction — 2026-09-07 - -`ReadView` now entails equality with the indexed store contents. Cached-read -freshness is tied to a particular store history; every write invalidates old -freshness, and synchronization reads current contents in the model. - -`Echo` now carries a specified residue certificate. Source compatibility, recovery, -and migration have explicit obligations. The collision theorem refutes every -migration requiring a distinction discarded by the retained pair. Resource -bounds require measure inequalities; arbitrary grade retagging is removed. - -The eleven-module core and eleven deliberate rejection fixtures (the counts at -that date; `just check` now reports seventeen modules and twelve fixtures) pass -with Agda 2.6.4.3 under `--safe --without-K --no-libraries`, without warnings. -The additional canonical Echo integration proves both representation round -trips and agreement of lowering; its standard-library dependencies emit Cubical -compatibility warnings. See link:docs/continuity-foundations.adoc[] for commands, -scope, and remaining runtime and combined-language obligations. - -== Earlier semantic proof-transport correction — 2026-09-07 - -The token-only proof-status construction has been replaced. `proofSound` -derives an explicit `Meaning holder artifact claim` from every proof status. -The verifier supplies a Boolean check and a proof of acceptance soundness; -proof construction requires its successful-check equality. No global soundness -axiom is added. - -Reproduced with Agda 2.6.4.3: `just check` passes the full 10-module library -and four semantic rejection controls. Examples prove legitimate acceptance -and rejection of bad payloads, altered artefacts, false claims, opaque modes, -and missing checking resources. Holder-dependent transfer is explicitly -qualified. The older `proofNeedsChecker` theorem remains a weaker structural -projection; its former semantic interpretation was unsupported. - -At that stage ReadConsistency/store coherence and EchoBridge/index constraints -were still open; the later correction above addresses their model-level gaps. -External-store and runtime correspondence remain open. - -== Earlier reproduced baseline - -* Command: `agda --safe -i src src/EpistemicTypes/All.agda` → **exit 0**. -* All **10/10** modules declare `{-# OPTIONS --safe #-}`; **zero `postulate`**, - zero `believe_me`/`primTrustMe`. -* Agda used here: **2.6.3** (the repo's `CONTRIBUTING.md` targets 2.8.0; the - development uses only `Agda.Builtin`/`Agda.Primitive`, so it checks under both). - -Modules (`src/EpistemicTypes/`): `Base`, `Access`, `Warrant`, `ReadConsistency`, -`ProofTransport` (+ `ProofTransportExample`), `EchoBridge`, `SurrealBridge`, -`Examples`, `All`. - -Reproduce: -[source,sh] +This is the current, source-anchored verification record for the Agda +formalisation. The authoritative positive tree contains *22 source modules* and +the negative-control manifest contains *13 expected-rejection fixtures*. The +source is constructive, builtins-only, map-only at its base interface, and has +no postulates or proof escape hatches. Exact theorem scope and trust boundaries +are recorded below; historical snapshots remain in `AFFIRMATION.adoc` and are +not current inventory. + +== Status vocabulary + +This document uses the estate proof-policy vocabulary: + +* `PROVEN` — accepted by the named kernel under its safe profile, with no proof + escape hatch; +* `TESTED` — a bounded, sampled, integration, or expected-rejection control; +* `ASSUMED` — an explicit premise or an externally reported correspondence not + rechecked by this repository; +* `OPEN` — not discharged. + +The separate cross-prover labels `AGDA-PENDING`, `AGDA-VERIFIED`, +`COQ-CHECKED`, `LEAN-CHECKED`, `BRIDGE-PENDING`, and `RECONCILED` describe +verification legs; they do not strengthen the proof-policy status. + +== Verification profile and current receipt + +The policy entry point is `scripts/check.sh`. It runs: + +[source,shell] ---- -just check # = agda --no-libraries -i src src/EpistemicTypes/All.agda -# or, enforcing --safe explicitly: -agda --safe -i src src/EpistemicTypes/All.agda +bash tests/check-policy.sh +bash tests/check-proofs.sh +bash tests/check-rejections.sh ---- -== Honest scope +Every first-party Agda entry point is invoked with the canonical theory profile +`--safe --without-K --cubical-compatible --exact-split --no-sized-types +--no-guardedness`. Positive source checks use `--no-libraries --double-check +--ignore-interfaces -W error`. Agda 2.6.4.3's +`UnsupportedIndexedMatch` category is disabled in that strict pass only because +its 23 existing warning spans are checked separately against the exact manifest +in `tests/check-proofs.sh`. A new, moved, or stale location fails the gate. The +safe proofs check, but no Cubical transport-computation claim is made for those +indexed eliminations, including `Kripke.Belief.believed`. The policy gate also +compares all 22 source modules, 13 rejection fixtures, and the integration +witness with exact path manifests; rejects additional `OPTIONS` pragmas, proof +escape hatches, and non-core imports; and verifies a generated negative +control: `--safe` must reject a planted postulate with Agda's expected +diagnostic and exit code. + +The most recent hosted receipt before adoption of the explicit +`--cubical-compatible` CLI requirement is Proof Safety run +https://github.com/hyperpolymath/epistemic-types/actions/runs/40445723481[40445723481] +at source commit `5422cd5bf1418c44321bf0f77e894737a451d8f5` (Agda 2.6.4.3), where both +`Proof core and rejection controls` and `Canonical Echo correspondence` passed. +Because that command did not spell out the new CLI flag, it is retained as +historical evidence, not as the receipt for the 2026-11-01 profile. + +The fresh canonical-profile receipt is Proof Safety run +https://github.com/hyperpolymath/epistemic-types/actions/runs/41326349568[41326349568] +at checked revision `bf9c75a38794d744ce466574e6323062e7d22533` on 2026-11-01. +Both `Proof core and rejection controls` and `Canonical Echo correspondence` +passed with Agda 2.6.4.3. The core job ran the policy preflight, all 22 source +modules, and all 13 intended rejections; the separate integration job checked +the pinned Echo witness. + +Current profile status: `AGDA-VERIFIED`; the checked revision is *Mathesis +Grade 3*. The immediately following status/metadata receipt update changes no +Agda source, fixture, gate, option, or dependency pin and is itself rerun by the +same PR workflow. No missing tool, import failure, or unexpected rejection +counts as a pass. + +== Local proof ledger + +All `PROVEN` rows below describe the Agda model only. They are covered by the +canonical hosted receipt above; they do not thereby establish an external +runtime or an unlisted mathematical correspondence. + +[cols="1,4,1,3",options="header"] +|=== +| ID | Exact scope | Status | Source + +| L-1 +| Map-only standpoint modality; lawful, factive, belief, return, and + accessibility capabilities remain separate records. No generic `bind` or + `extract` exists. +| PROVEN +| `Base.agda`, `Access.agda` + +| L-2 +| Warrant evidence does not imply its claim. Extraction requires the separate + `SoundWarrant.sound` field; concrete contradiction witnesses refute generic + reflection for belief and warrant. +| PROVEN +| `Warrant.agda`, `Examples.agda` + +| L-3 +| Proof transport derives `Meaning holder artifact claim` only from an accepted + sound checker. Transmission moves bytes to a receipt, not proofhood; public + transfer and designated-holder transfer have distinct premises. +| PROVEN +| `ProofTransport.agda`, `ProofTransportExample.agda` + +| L-4 +| Pure finite store histories tie reads to indexed contents; writes stale old + caches; synchronisation restores model-level freshness; fact transport needs + an explicit stability proof. +| PROVEN +| `ReadConsistency.agda`, `ContinuityExamples.agda` + +| L-5 +| Echo residue certificates, source compatibility, recovery, migration, + collision obstruction, and measured upper bounds are separate. Echo is not a + resource instance and the epistemic modality is not collapsed into Echo. +| PROVEN +| `EchoBridge.agda`, `ContinuityExamples.agda` + +| L-6 +| The finite-day `SurrealAccess` instance supports bound weakening and preserves + residue data. It is not the Conway proper class and proves no physical-cost + statement. +| PROVEN +| `SurrealBridge.agda` + +| L-7 +| The order-generic RapidNJ Q-criterion row bound and generated skip warrant are + proved over `OrderedGroup`; the integer instance and worked scan discharge + that scope. +| PROVEN +| `Applications/*.agda` + +| K-1 +| World-indexed modalities and the one-world reduction `toModality`; this is a + construction, not a formal impossibility theorem about every alternative + encoding in the unindexed API. +| PROVEN +| `Kripke/Indexed.agda` + +| K-2 +| `Frame`, `Box`, and its map action. +| PROVEN +| `Kripke/Frame.agda` + +| K-3 +| Constructively: reflexive iff the `Box` T/factivity map exists; transitive iff + the `Box` 4/positive-introspection map exists; Euclidean implies 5; serial + implies D. +| PROVEN +| `Kripke/Frame.agda:T`, `T⁻¹`, `Four`, `Four⁻¹`, `Five`, `D` + +| K-4 +| Converse 5 and converse D. +| OPEN +| No declaration; classical reasoning would be required + +| K-5 +| A non-reflexive two-world frame carries a `Box` witness and an + epistemic-types `Warrant` for a proposition false at the current world; no + soundness map for that evidence exists. +| PROVEN +| `Kripke/Belief.agda` + +| K-6 +| Residual candidates are represented as a `Box`; a three-world witness proves + presence without identification. +| PROVEN +| `Kripke/Residual.agda` + +| K-7 +| Two contexts can have pointwise-equivalent candidate interpretations while + proper dependence differs, in the local faithful mirror. +| PROVEN +| `Kripke/Dependence.agda` + +| K-8 +| The local dependence mirror is propositionally identical to + residual-evidence-types' current owning record. +| ASSUMED +| Documentary comparison only; no imported owning definition + +| C-1 +| Every one of the 13 intended-invalid constructions is rejected for its + enumerated semantic type mismatch. This is negative-control evidence, not a + positive theorem. +| TESTED +| `tests/check-rejections.sh`, `tests/reject/*.agda` + +| C-2 +| The local residue representation round-trips to pinned canonical Echo and + lowering agrees at the pinned source revision. This is source-level + correspondence only, not a full graded-comonad or runtime theorem. +| TESTED +| `tests/integration/CanonicalEcho.agda`; Echo pin + `46cd1a32d4dcf1020f01dd1aab41f816742da10e` +|=== + +== External pinned evidence, not local closure + +Choreographic-types reports machine-checked K-CUT results for its explicitly +finite, binary-choice, plain-merge fragment, including K-CUT-LOSS, the +directional K-CUT-WARRANT bound, transport, and asynchronous variants. It also +reports `SoundWarrant` for warrants determined by that type-level frame. +Data-dependent warrants, recursion, full merge, and the wider asynchronous +forms remain open there. The previously recorded pinned E-6 receipt remains +external evidence; this repository does not generalise it into global warrant +soundness and does not count it as a locally rechecked theorem. + +The current cross-repository status statements in +`docs/what-epistemic-is.adoc` are documentary pointers. They are not imports, +build dependencies, or independent proof legs for this repository. + +== Mathesis grade and independent proof legs + +Mathesis Grade 3 means that the Agda source checks under the strict profile at a +recorded revision, without an independent foundational translation. Hosted run +`41326349568` closes that requirement for checked revision `bf9c75a`; this +proof corpus is *Mathesis Grade 3*. + +No theorem in this repository currently has a theorem-by-theorem Rocq or Lean +leg with an exact statement comparison: + +[cols="2,1,3",options="header"] +|=== +| Leg | Status | Consequence +| Agda canonical profile | AGDA-VERIFIED | Grade 3 receipt: run `41326349568`, revision `bf9c75a` +| Rocq/Coq | OPEN / NOT-INVENTORIED | No Grade 2i/2ii credit +| Lean | OPEN / NOT-INVENTORIED | No Grade 2i/2ii credit +| Proposition/semantics bridge | BRIDGE-PENDING | No claim of reconciliation +| Runtime refinement | OPEN | Model theorems do not verify an implementation +|=== + +The standards corpus has no repository-specific `epistemic-types` T3 stub. Its +current theory mapping therefore governs: Agda is the source of truth, with +Rocq and Lean rechecks as open future obligations. A repository-tier label is +not inferred from the Mathesis grade. -* Status: **prototype (v0.1.0)** — a deliberately small, honest formalisation of - standpoint-indexed modal / epistemic / echo-like type formers. -* `EchoBridge` and `SurrealBridge` remain self-contained. The optional integration - test imports canonical Echo sources and proves a residue correspondence; no - full surreal-number library or combined-runtime verification is claimed. -* The library is self-contained by design (`--no-libraries`); it does not depend - on the standard library. +== Explicit open obligations -== Licence +* Complete epistemic logic beyond the implemented constructive frame fragment, + including any desired classical converses for 5 and D. +* Soundness for data-dependent warrants; no global extraction rule is assumed. +* Re-proof the dependence result against residual-evidence-types' owning + definitions if that external correspondence is to be claimed. +* Rational input or a proved common-denominator rescaling transport for the + RapidNJ application; row insertion and cross-iteration bound reuse. +* Law-bearing instances where records currently expose laws as caller-supplied + fields; no generic monad/comonad commitment. +* Full Conway-surreal semantics, full graded-loss/comonad semantics, external + store/scheduler/attestation/runtime refinement, and physical guarantees. +* The theorem-level Rocq and Lean inventory, independent checks, and explicit + proposition bridges needed for Mathesis Grade 2 or stronger. -* **`LICENSE` present (MPL-2.0).** Previously flagged here as missing; the owner - has since added a REUSE-style `LICENSE` + `LICENSES/{MPL-2.0,CC-BY-SA-4.0}.txt`, - matching the estate sole-owner policy. +See `PROOF-NEEDS.adoc` for the executable next-proof queue. diff --git a/README.adoc b/README.adoc index 7d3f06f..e3ed0d5 100644 --- a/README.adoc +++ b/README.adoc @@ -52,9 +52,10 @@ Monadic (`bind`) and comonadic (`extract`) structure are *not* provided by defau A warrant records the *type of evidence* for a claim without assuming the evidence is valid: -* `Warrant κ A` — the type of evidence tokens for `A` from standpoint `κ`. -* `Epi κ A` — an evidence token paired with its warrant type. -* `SoundWarrant` — a separate interface adding a soundness map (`evidence → A`). Not assumed by default. +* `Warrant K κ A` — the type of evidence tokens for `A` from standpoint `κ`. +* `Epi K κ A` — an evidence token paired with its warrant type. +* `SoundWarrant` — a separate interface adding a soundness map from that + warrant's `Evidence` to `A`. Not assumed by default. This separates "I have a receipt for A" from "A is true." @@ -161,8 +162,8 @@ interface is a breaking correction documented in link:docs/proof-transport.adoc[ | Standard | `EpistemicTypes.Base` -| Knowledge (factivity) vs. Belief distinction -| Standard (modal logic S5 vs. KD45) +| Knowledge (factivity) vs. non-factive belief distinction +| Standard distinction; this minimal API does not claim S5 or KD45 | `EpistemicTypes.Base` | Warrant types without assumed soundness @@ -190,7 +191,7 @@ interface is a breaking correction documented in link:docs/proof-transport.adoc[ [NOTE] ==== -2026-10-12: Kripke semantics, the frame-condition correspondences, a non-factive model (`Warrant ≠ SoundWarrant` witnessed), the residual-evidence frame and the dependence test now live under `src/EpistemicTypes/Kripke/`; see link:docs/kripke-status-2026-10-12.adoc[]. Global warrant soundness for type-determined warrants is proved externally in choreographic-types, at the recorded revision `d8536184366f4ac4567aa066c5dbcb9220e3607a` with a successful CI type-check, and is not re-checked here (E-6). Soundness for data-dependent warrants remains an assumption. +2026-10-12: Kripke semantics, the frame-condition correspondences, a non-factive model (`Warrant ≠ SoundWarrant` witnessed), the residual-evidence frame and the dependence test now live under `src/EpistemicTypes/Kripke/`; see link:docs/kripke-status-2026-10-12.adoc[]. Choreographic-types externally proves soundness for type-determined warrants in its finite binary/plain-merge fragment at the recorded revision `d8536184366f4ac4567aa066c5dbcb9220e3607a`, with a successful CI type-check; that result is not re-checked or generalised here (E-6). Soundness for data-dependent warrants remains open and is not assumed by this repository. ==== [CAUTION] @@ -223,7 +224,7 @@ This is a prototype, not a complete epistemic logic. The following are **intenti [source,bash] ---- -just check # positive proofs and expected rejection controls +just check # policy guard + 22 positive modules + 13 expected rejections ---- `just check` calls `scripts/check.sh`: it uses a local `agda` when one is on @@ -245,12 +246,24 @@ To check a single module or the aggregate directly: [source,bash] ---- -agda --no-libraries -i src src/EpistemicTypes/All.agda +agda --no-libraries --safe --without-K --cubical-compatible \ + --double-check --ignore-interfaces \ + -W error -W noUnsupportedIndexedMatch \ + -i src src/EpistemicTypes/All.agda ---- +Agda 2.6.4.3's `UnsupportedIndexedMatch` category is disabled in the strict +pass, then rerun without warnings-as-errors and compared with the exact 23-span +manifest in `tests/check-proofs.sh`. A warning at a new location, or a stale +manifest entry, fails the gate. The proofs check in safe mode; the repository +does not claim that those indexed eliminations compute when applied to Cubical +transports. All other warnings remain errors. + == Documentation -* link:EXPLAINME.adoc[EXPLAINME] — claim-by-claim receipts and known gaps +* link:EXPLAINME.adoc[EXPLAINME] — claim-by-claim receipts and proof ledger +* link:PROOF-STATUS.adoc[Proof status] / link:PROOF-NEEDS.adoc[proof needs] — current verification grade, trust boundaries, and open proof legs +* link:docs/kripke-status-2026-10-12.adoc[Kripke status] — exact constructive frame scope and warrant boundary * link:docs/continuity-foundations.adoc[Continuity foundations] — store coherence, retained information, bounds, and next obligations * link:docs/proof-transport.adoc[Proof transport] — semantic verification across boundaries * link:docs/applications/rapidnj-q-criterion.adoc[Applications: the RapidNJ Q-criterion] — the bound, the skip warrant, the exact-arithmetic obligation diff --git a/SECURITY.adoc b/SECURITY.adoc index f06be9f..a554a94 100644 --- a/SECURITY.adoc +++ b/SECURITY.adoc @@ -1,6 +1,6 @@ == Security Policy -_Last updated: 2026-06-15 — version 0.1.0 (prototype)_ +_Last updated: 2026-11-01 — version 0.1.0 (prototype)_ === Scope and threat model @@ -12,10 +12,12 @@ formers. It is a single-tool, library-only project: only "`execution`" is Agda type-checking the source. * *No network, no secrets, no I/O.* The library reads no input and writes no output beyond what the type-checker reports. -* *No dependencies.* It compiles under -`+{-# OPTIONS --safe --without-K #-}+` with *no postulates* and *no Agda +* *No core dependencies.* The source library compiles under +`+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}+` with *no postulates* and *no Agda standard library* (built with `+agda --no-libraries+`, using only -`+Agda.Builtin.*+` / `+Agda.Primitive+`). +`+Agda.Builtin.*+`, `+Agda.Primitive+`, and local modules). The separately +pinned canonical-Echo integration check imports sibling source and the Agda +standard library; it is not part of the standalone core. Because there is no runtime surface, the meaningful "`attack surface`" is the *proofs and machine-readable specifications themselves*. A @@ -25,14 +27,14 @@ example: * a proof that type-checks but encodes a false or misleading claim; * an unintended use of a postulate, `+--type-in-type+`, an `+unsafe+` pragma, or some other escape hatch that would weaken the -`+--safe --without-K+` guarantee; +`+--safe --without-K --cubical-compatible+` guarantee; * a flaw in the `+ProofTransport+` discipline that lets an attestation claim more than it should — e.g. something that lets a receiver-bound (designated) proof be treated as portable, or a receipt-only artifact be treated as a certifying proof, contrary to the `+proofNeedsChecker+` -"`no-smuggling`" invariant. The same applies to the `+EchoBridge+` -graded loss/residue accounting and the `+SurrealBridge+` birthday-tower -carriers. +"`no-smuggling`" invariant. The same applies to `+EchoBridge+` residue +certificates and separately measured bounds, and to the finite-day +`+SurrealBridge+` carriers. * a divergence between the Agda formalization and its engineering rendering in `+.machine_readable/proof-transport/+` (a2ml / Nickel-k9) that would let the machine-readable spec be read as guaranteeing @@ -70,14 +72,16 @@ withdraw a claim_ rather than ship a patch to running software, the resolution may take the form of a documentation correction, a proof revision, or an honest note that a stated property does not hold. -There is no automated CI on this repository (see `+AUDIT.adoc+`), so -verification is manual: the canonical check is +Proof and security CI are enabled (see `AUDIT.adoc` and +`docs/ci-safety.adoc`). The canonical local/CI proof entry point is: -.... -just check # == agda --no-libraries -i src src/EpistemicTypes/All.agda -.... +[source,shell] +---- +just check # policy guard + 22 source modules + 13 expected rejections +---- -with *Agda 2.8.0*. +CI pins *Agda 2.6.4.3* and explicitly invokes +`--safe --without-K --cubical-compatible`. === Supported versions @@ -101,9 +105,9 @@ report responsibly and avoid privacy violations or destructive testing. === Related projects Findings here may also be relevant to sibling formal-methods work in the -estate — in particular `+echo-types+` (the loss-with-residue formalism -that `+EchoBridge+` composes with), `+ephapax+` (sibling formal language -with echo obligations), and the `+standards+` / `+a2ml+` / `+k9+` +estate — in particular `+echo-types+` (the proof-relevant Echo source used by +the pinned representation/one-way-lowering check), `+ephapax+` (sibling formal +language with echo obligations), and the `+standards+` / `+a2ml+` / `+k9+` tooling that `+ProofTransport+`’s machine-readable rendering targets. Where appropriate, a report against one may be cross-referenced to the others. diff --git a/build/guix.scm b/build/guix.scm index ba23992..ece1146 100644 --- a/build/guix.scm +++ b/build/guix.scm @@ -19,7 +19,7 @@ ;; `scripts/check.sh` falls back to this environment when no Agda is on PATH. ;; The Agda in Guix may differ from the version CI pins (2.6.4.3); the script ;; reports the version it uses. ripgrep and findutils are required by -;; tests/check-rejections.sh and tests/check-proofs.sh. +;; tests/check-policy.sh, tests/check-rejections.sh and tests/check-proofs.sh. (package (name "epistemic-types") (version "0.1.0") diff --git a/coordination.k9 b/coordination.k9 index 2be88c6..6064238 100644 --- a/coordination.k9 +++ b/coordination.k9 @@ -57,7 +57,7 @@ repo: owner: "Jonathan D.A. Jewell (hyperpolymath) " version: "0.1.0" status: "prototype" - last_updated: "2026-06-15" + last_updated: "2026-11-01" kind: "single-tool Agda library" # Paths the session machinery must treat as load-bearing. Changes under these @@ -66,9 +66,13 @@ protected_paths: - path: "src/" role: "Agda sources (the formalization)" - path: "src/EpistemicTypes/All.agda" - role: "re-export aggregator; the check entry point" + role: "full-graph aggregate; recursive gate checks every source file independently" - path: ".machine_readable/" role: "a2ml + Nickel/k9 machine-readable surface (descriptiles/, proof-transport/)" + - path: "tests/" + role: "proof-policy gate, 13 expected rejections and pinned integration witness" + - path: "PROOF-STATUS.adoc" + role: "current proof ledger and Mathesis grade boundary" - path: "Justfile" role: "canonical build recipe" - path: "epistemic-types.agda-lib" @@ -79,16 +83,16 @@ invariants: - id: "build-green" statement: "The library typechecks: `just check` succeeds." command: "just check" - expands_to: "bash tests/check-proofs.sh && bash tests/check-rejections.sh" + expands_to: "bash tests/check-policy.sh && bash tests/check-proofs.sh && bash tests/check-rejections.sh" tool: "Agda 2.6.4.3" - id: "no-postulates" - statement: "No postulates. Compiles under {-# OPTIONS --safe --without-K #-}; constructive throughout." + statement: "No postulates or escape hatches. Every first-party module declares --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness." - id: "no-stdlib" - statement: "No Agda standard library. Built with `agda --no-libraries`; only Agda.Builtin.* and Agda.Primitive are imported." + statement: "Core source has no Agda standard library: --no-libraries with only Agda.Builtin.*, Agda.Primitive and local imports. Pinned CanonicalEcho integration stays separate." - id: "licence-owner-manual" - statement: "Licence/SPDX are owner-manual. The tree is intentionally SPDX-free; do not add LICENSE, SPDX headers, or copyright lines in any automated pass. Classification (owner sole repo => MPL-2.0) is flagged separately for the owner." + statement: "Licence/SPDX declarations are present and owner-managed; do not alter them without owner instruction." - id: "honesty-over-api" - statement: "Favour mathematical honesty over a large API. The base E : K -> Set ℓ -> Set ℓ is a plain indexed endofunctor (map only) — not a monad/comonad; no generic return/reflect. Echo r A is kept distinct from E κ A." + statement: "Favour mathematical honesty over a large API. Base E is map-only with no generic bind/extract. Certified Echo C y, separately measured bounds, and E κ A remain distinct; Echo is not a resource instance." # CI and merge gates are explicitly authorized by the owner (2026-09-07). ci: @@ -99,9 +103,15 @@ ci: ecosystem: siblings: - name: "echo-types" - relationship: "EchoBridge (min-plus graded loss/residue) composes with echo-types' loss-with-residue formalism." + relationship: "Pinned representation/lowering correspondence only; Echo remains distinct from E κ A and is not a resource instance." - name: "ephapax" relationship: "Sibling formal language; four-layer redesign carries echo obligations." + - name: "choreographic-types" + relationship: "External Warrant consumer with scoped finite binary/plain-merge K-CUT results; no universal theorem imported here." + - name: "residual-evidence-types" + relationship: "Production-operated early research with no stable API; local dependence result is a mirror." + - name: "secret-types" + relationship: "Standalone production home for confidentiality and generic TINI; no local Secret API or theorem." - name: "standards" relationship: "Estate RSR/standards + k9-svc + a2ml tooling; source of truth for session-management." - name: "a2ml + k9" diff --git a/docs/README.adoc b/docs/README.adoc index 444eb03..f0e71e2 100644 --- a/docs/README.adoc +++ b/docs/README.adoc @@ -1,6 +1,6 @@ = Documentation Index — epistemic-types Jonathan D.A. Jewell (hyperpolymath) -v0.1.0, 2026-06-15: prototype +v0.1.0, 2026-11-01: prototype `epistemic-types` is a small, deliberately honest Agda formalization of standpoint-indexed modal / epistemic / echo-like type formers. It favours @@ -29,6 +29,15 @@ authority. `FactiveModality.reflect`, and the exact-arithmetic (ℚ) obligation stated rather than assumed. +| `PROOF-STATUS.adoc` / `PROOF-NEEDS.adoc` (repo root) +| Current proof ledger, Mathesis grade boundary, exact checker profile, and the + open Agda/Rocq/Lean/correspondence obligations. Historical counts in + `AFFIRMATION.adoc` do not override these files. + +| `docs/kripke-status-2026-10-12.adoc` +| The implemented constructive Kripke fragment, exact frame-condition theorem + scope, non-factive model, residual reading, and external-warrant boundary. + | `docs/proof-transport.adoc` | Focused walkthrough of `EpistemicTypes.ProofTransport`: how `transmit` downgrades a sender's `Proof` to a receiver's `Receipt`, how `verify` upgrades @@ -41,9 +50,10 @@ authority. two-level information-flow proposal (label order, attacker and observation boundary, noninterference target), and the reason no `Secret` API or security theorem exists in this repository. Issue #32 was closed on 2026-10-05 as - delivered here (no transfer; successor guard #39), and the note's 2026-10-25 - status update records the standalone repository's proved noninterference - theorem. + delivered here (no transfer; successor guard #39). The boundary note records + the 2026-11-01 source review: generic and two-point termination-insensitive + noninterference are proved there; termination-sensitive noninterference and + declassification remain open. | `docs/secret-types-transition-review-2026-10-05.adoc` | Cross-reference review of the Secret Types transition: the evidence and @@ -81,11 +91,14 @@ The Agda modules remain authoritative; these files restate them as data. == Source modules (authority) -The core lives in `src/EpistemicTypes/`. `All.agda` checks `Base`, `Warrant`, +The source lives in `src/EpistemicTypes/`. `All.agda` checks `Base`, `Warrant`, `Access`, `ReadConsistency`, `EchoBridge`, `SurrealBridge`, `ContinuityExamples`, -`Examples`, `ProofTransport`, and `ProofTransportExample`. Some imports are not -publicly re-exported to avoid helper-name collisions. Every core module uses -`--safe --without-K` and builtins only. Local checks use Agda 2.6.4.3. +`Examples`, `ProofTransport`, `ProofTransportExample`, and all five +`Kripke/` modules. Some imports are not publicly re-exported to avoid +helper-name collisions. Every source module declares +`--safe --without-K --cubical-compatible --exact-split --no-sized-types +--no-guardedness` and imports only builtins or local modules. CI pins Agda +2.6.4.3. The applications layer lives beside the core in `src/EpistemicTypes/Applications/`: `OrderedGroup` (the arithmetic budget), `IntegerModel` (the discharged @@ -99,7 +112,8 @@ link:applications/rapidnj-q-criterion.adoc[]. == Notes * `Echo C y`, `BoundedEcho C measure budget y`, and `E κ A` have separate roles. -* `just check` runs the proof graph (seventeen modules, including the - applications layer) and twelve semantic rejection fixtures. +* `just check` enforces the policy profile, checks all 22 source modules + (including applications and Kripke), and validates 13 semantic rejection + fixtures. * `just check-canonical` separately checks correspondence against actual sibling Echo sources; it requires an explicit standard-library source path. diff --git a/docs/applications/rapidnj-q-criterion.adoc b/docs/applications/rapidnj-q-criterion.adoc index c253eaf..ea8d17b 100644 --- a/docs/applications/rapidnj-q-criterion.adoc +++ b/docs/applications/rapidnj-q-criterion.adoc @@ -229,7 +229,8 @@ exact comparison decides it. == What is proved, and what is not -Proved (all machine-checked under `--safe --without-K`, no postulates): +Proved (machine-checked with Agda 2.6.4.3 under the repository's strict +`--safe --without-K --cubical-compatible` profile, with no postulates): * `qBound-≤-Q`, `qBound-≤-suffix`, `noBetter-weaken`, `noBetter-append`; * `skipWarrant` / `skipSoundWarrant` construction and `skip-known`, diff --git a/docs/ci-safety.adoc b/docs/ci-safety.adoc index 897df7d..b09eeb4 100644 --- a/docs/ci-safety.adoc +++ b/docs/ci-safety.adoc @@ -9,18 +9,30 @@ The owner explicitly authorized maintaining these CI and merge safeguards on `Proof core and rejection controls` checks every file under `src/EpistemicTypes/`, including a file accidentally omitted from `All.agda`. -It uses Agda 2.6.4.3 with `--safe --without-K --double-check ---ignore-interfaces -W error --no-libraries`. It also runs all enumerated -false-claim controls (twelve at the time of writing). The rejection runner requires Agda's type-error exit code -and the intended semantic diagnostic; import and environment failures do not pass. +It uses Agda 2.6.4.3 with explicit +`--safe --without-K --cubical-compatible --exact-split --no-sized-types +--no-guardedness --double-check --ignore-interfaces -W error --no-libraries`. +The strict pass disables `UnsupportedIndexedMatch`, then a second pass requires +that category to occur at exactly the 23 reviewed spans listed in +`tests/check-proofs.sh`; a new, moved, or stale warning fails. The proofs remain +safe, but those indexed eliminations are not claimed to compute when applied to +Cubical transports. The policy preflight compares exactly 22 source paths, 13 +rejection paths and one integration path with authoritative manifests; requires +every first-party module to contain exactly one complete strict pragma; scans +the positive proof tree for escape hatches and non-core imports; and requires +`--safe` to reject a generated postulate. Search-tool errors fail closed. The +rejection runner then requires every fixture's type-error exit code and intended +semantic diagnostic. Import and environment failures do not pass. `Canonical Echo correspondence` imports the actual `echo-types` source pinned to `46cd1a32d4dcf1020f01dd1aab41f816742da10e`. It checks both residue-conversion round trips and agreement of lowering. Its standard library is Debian's Agda stdlib -2.1-4. Only `UnsupportedIndexedMatch`, the already-reviewed warning about Cubical -transport compatibility, is suppressed for this integration. Safe mode, -without-K, internal double checking and all other warnings-as-errors remain. -The claim is ordinary Agda correspondence, not Cubical computation compatibility. +2.1-4. The same warning category is disabled because the reviewed external +Echo/stdlib sources also emit it. Safe mode, without-K, cubical-compatible +mode, internal double checking and all other warnings-as-errors remain. The +claim is the named pinned-source +correspondence, not full Cubical computation compatibility of those external +dependencies. The Debian 13 container is pinned by digest; the Agda packages are pinned by version and installed through authenticated Debian repositories. There are no diff --git a/docs/continuity-foundations.adoc b/docs/continuity-foundations.adoc index 35a730b..ff8a1e7 100644 --- a/docs/continuity-foundations.adoc +++ b/docs/continuity-foundations.adoc @@ -142,23 +142,28 @@ migration. The canonical retention axis remains distinct from resource grades. [source,sh] ---- just check -agda --no-libraries --safe --without-K --ignore-interfaces -i src src/EpistemicTypes/All.agda +agda --no-libraries --safe --without-K --cubical-compatible --ignore-interfaces -i src src/EpistemicTypes/All.agda just check-canonical /path/to/echo-types /path/to/agda-stdlib/src ---- -The core, examples and applications layer have been checked with Agda 2.6.4.3. -`just check` covers every source module under `src/EpistemicTypes/` (seventeen -at the time of writing) and every semantic rejection fixture (twelve): the four -proof-transport controls plus `StaleSample`, `FakeFreshness`, `ForkedHistory`, -`ForgedResidue`, `MismatchedSource`, `UnderstatedBound`, `InventedMigration`, and -`UncheckedSkip`. -An unrelated import or tool failure fails the rejection gate. - -The optional canonical integration also checks successfully with the locally -available standard library 2.1. Its dependencies emit `UnsupportedIndexedMatch` -compatibility warnings about Cubical transports; this run establishes ordinary -`--without-K` checking, not Cubical computation compatibility. The core build -has no standard-library dependency and emits no warnings. +The source tree has been checked with Agda 2.6.4.3. `just check` covers every +source module under `src/EpistemicTypes/` (22: core, applications, and Kripke) +and every semantic rejection fixture (13): the four proof-transport controls, +`StaleSample`, `FakeFreshness`, `ForkedHistory`, `ForgedResidue`, +`MismatchedSource`, `UnderstatedBound`, `InventedMigration`, `UncheckedSkip`, +and `BeliefIsKnowledge`. An unrelated import or tool failure fails the +rejection gate. The current 2026-11-01 aggregate receipt status is recorded in +link:../PROOF-STATUS.adoc[]. + +The optional canonical integration uses standard library 2.1 and pinned Echo +source. It now invokes `--cubical-compatible` explicitly, while suppressing the +reviewed `UnsupportedIndexedMatch` warning emitted by those external +dependencies. The run establishes the stated representation/lowering +correspondence at those pins; it does not establish full Cubical computation +compatibility for the dependencies. The core build has no standard-library +dependency. Its strict pass disables the same warning category, but a second +pass requires the exact 23-span core manifest in `tests/check-proofs.sh`; all +other warnings are errors and location drift fails. == Next obligations @@ -172,5 +177,6 @@ an acceptance checker with a soundness proof. These remain separate work. The core, deliberate rejection controls and pinned canonical Echo correspondence are CI gates; see link:ci-safety.adoc[]. Only the documented Cubical transport -compatibility warning is suppressed for the integration. The core remains -warning-free with no standard-library dependency. +compatibility warning category is disabled: locally for `Kripke.Belief` and at +the pinned external integration boundary. The core remains standalone; no +other warning is suppressed. diff --git a/docs/kripke-status-2026-10-12.adoc b/docs/kripke-status-2026-10-12.adoc index 5fd088d..c0e767f 100644 --- a/docs/kripke-status-2026-10-12.adoc +++ b/docs/kripke-status-2026-10-12.adoc @@ -1,35 +1,96 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 -= Kripke semantics and warrant soundness — status 2026-10-12 += Kripke semantics and warrant soundness — 2026-10-12 result, current scope +:revdate: 2026-11-01 +:toc: -The modules under `src/EpistemicTypes/Kripke/` formalise Kripke semantics -and the results below. Complete epistemic logic and soundness for -data-dependent warrants remain outstanding; E-6 records the external -verification for type-determined warrants. +This document preserves the Kripke milestone first recorded on 2026-10-12 while +stating its current exact scope. The owning current ledger is +link:../PROOF-STATUS.adoc[]. The implementation is constructive and lives under +`src/EpistemicTypes/Kripke/`; it is a scoped Kripke semantics, not a complete +epistemic logic. + +== Local checked claims [cols="1,3,1",options="header"] |=== | ID | Claim | Status -| E-1 | `Modality` cannot express Kripke knowledge: its carrier has no world index. `IndexedModality`/`IndexedFactive`/`IndexedAccessible` are `Base`/`Access` field for field with `E : K → (W → Set) → (W → Set)`; the originals are the `W = ⊤` case (`toModality`) | PROVEN (`Kripke/Indexed.agda`) -| E-2 | Frames and `Box`; `Box` is an `IndexedModality` | PROVEN (`Kripke/Frame.agda`) -| E-3 | Correspondences, constructively: reflexive ⇔ factive (T, both directions); transitive ⇔ positively introspective (4, both directions); Euclidean ⇒ 5; serial ⇒ D. The converses of 5 and D need classical reasoning and are not claimed | PROVEN / OPEN as stated -| E-4 | A reflexive frame yields an `IndexedFactive` (`factive`) | PROVEN -| E-5 | *The non-factive model*: two worlds, access only w₀ → w₁; at w₀ there is a `Warrant` (evidence: a `Box` proof) for a false proposition, and no `sound` field can exist for it. `Warrant ≠ SoundWarrant`, witnessed | PROVEN (`Kripke/Belief.agda`: `believed`, `false-at-w₀`, `no-sound-warrant`); TESTED (`tests/reject/BeliefIsKnowledge`: factivity refused on this frame) -| E-6 | Global soundness of warrants in a reflexive frame — every type-determined warrant sound — is proved externally in choreographic-types (`Choreographic.Kripke`, `Frame.sound-warrant`), which imports this repo's `EpistemicTypes.Warrant` at `495db9cca003e12066a3cb9c9f2d7afa1a953aec` (`Warrant.agda`, `Base.agda` and `Access.agda` are unchanged between that commit and this one). Recorded external revision: choreographic-types `d8536184366f4ac4567aa066c5dbcb9220e3607a`. Type-check: its `Agda proofs` workflow, run 39288705455 on that commit, succeeded under Agda 2.6.4.3 with `--safe --without-K --no-libraries --ignore-interfaces --double-check` (the import is pinned by `scripts/fetch-siblings.sh` there) | RECORDED externally on 2026-10-19 (revision and CI run above; the rest of this table is the 2026-10-12 snapshot); not re-checked in this repository +| E-1 | `IndexedModality`, `IndexedFactive`, and `IndexedAccessible` are the +world-indexed analogues of the base interfaces; `toModality` constructs the +one-world case. The stronger prose claim that no other encoding could use the +unindexed API is not a theorem. | PROVEN (construction only, +`Kripke/Indexed.agda`) +| E-2 | Frames and `Box`; `Box` has the indexed map action. | PROVEN +(`Kripke/Frame.agda`) +| E-3 | Reflexive iff the T/factivity map exists; transitive iff the +4/positive-introspection map exists; Euclidean implies 5; serial implies D. +The converses of 5 and D are not claimed. | PROVEN for the six named +constructive maps; converse 5 and D OPEN (`Kripke/Frame.agda`) +| E-4 | A reflexive frame constructs an `IndexedFactive`. | PROVEN (`factive`) +| E-5 | On a two-world non-reflexive frame, a `Box` witness and an +`epistemic-types.Warrant` exist for a proposition false at the current world, +and no soundness map for that evidence exists. | PROVEN +(`Kripke/Belief.agda`: `believed`, `false-at-w₀`, `warrant`, +`no-sound-warrant`, `not-reflexive`); the `BeliefIsKnowledge` expected +rejection is TESTED |=== -Separation (family bar, criterion 2): the belief model is a modality with -evidence and no extraction, which no grade algebra and no secret label can -express; the factive/non-factive split is the family's own. +These declarations prove the propositions in their types. They do not prove +completeness of an epistemic calculus, decidability, proof irrelevance, +classical modal correspondences, or a runtime implementation. + +== Warrant soundness boundary + +Choreographic-types provides external evidence for the explicitly scoped +result formerly recorded as E-6: on its reflexive frame, warrants determined by +the finite binary/plain-merge choreography are sound. Its current ledger also +reports K-CUT-LOSS, directional K-CUT-WARRANT bounds and transport, plus +asynchronous variants, for that fragment. Data-dependent warrants, recursion, +full merge, and broader asynchronous results remain open there. + +This repository retains its originally pinned evidence: -Builtins only; checked with the repo's own flags (`--safe --without-K ---double-check -W error`). +* epistemic-types source pin + `495db9cca003e12066a3cb9c9f2d7afa1a953aec`; +* choreographic-types source pin + `d8536184366f4ac4567aa066c5dbcb9220e3607a`; +* successful choreographic-types Agda workflow run `39288705455`. -== Residual-evidence, read in the frame (`Kripke/Residual.agda`) +That is external pinned evidence, not a local recheck and not a theorem of +global warrant soundness. In this repository, `SoundWarrant` remains an +explicit interface and data-dependent soundness remains `OPEN`. + +== Residual-evidence reading [cols="1,3,1",options="header"] |=== | ID | Claim | Status -| E-7 | residual-evidence-types' `Holds c P` is `Box` over the accessibility "is a candidate" (same reading, satisfies the evidence): the Echo fibre cut down by evidence. Its four verdicts are the joint cases of `Box P`, `Box (¬ P)` | PROVEN by definition (`residualFrame`, `Holds`) -| E-8 | "Presence without identification" is de dicto without de re: `Box (∃ x. Is x)` with no `Box (Is x)`; witnessed on a three-world model | PROVEN (`presence`, `no-identification`) -| E-9 | DECISION-002 test 1 (dependence is not a function of the candidate set), run in a faithful mirror of residual-evidence's `Dependent`: contexts `[P]` and `[P, P]` have the same candidates pointwise, yet a claim can rest on a *proper* sub-context in the second and not the first. A box sees worlds; dependence sees assumptions | PROVEN in the mirror (`Kripke/Dependence.agda`); re-proof against residual-evidence's own record OPEN (same kernel, same shape) +| E-7 | For the local definition, residual `Holds` is `Box` over accessibility +"is a candidate" (matching observation and evidence). | PROVEN by definition +(`Kripke/Residual.agda`: `residualFrame`, `Holds`) +| E-8 | Presence without identification: `Box (∃ x. Is x)` while no chosen +`Box (Is x)` holds, witnessed on a three-world model. | PROVEN +(`presence`, `no-identification`) +| E-9 | In the local faithful mirror, contexts `[P]` and `[P,P]` have +pointwise-equivalent candidate interpretations while proper dependence differs. +| PROVEN locally (`Kripke/Dependence.agda`) +| E-10 | E-9 is propositionally identical to residual-evidence-types' current +owning `Dependent` record. | ASSUMED documentary correspondence; re-proof +against the owning record OPEN |=== + +Residual-evidence-types is operated in production, while its owning README +still classifies the mathematical/API maturity as early research with no stable +API. Its checked corpus now includes composition, revision/retraction, and a +certified finite checker/explorer correspondence. This repository does not +stabilise that sibling API or infer a dependency from the conceptual reading. + +== Verification classification + +The 2026-10-27 hosted run at commit `5422cd5` checked all five Kripke modules +under the then-current gate. The 2026-11-01 profile additionally requires the +CLI to state `--cubical-compatible` explicitly and records +`UnsupportedIndexedMatch` computation boundaries, including `believed`; the +current gate accepts the category only at its exact audited source manifest. +Proof Safety run `41326349568` passed that profile at checked revision `bf9c75a`; +the Agda leg is `AGDA-VERIFIED` and the corpus is Mathesis Grade 3. Rocq, Lean, +and proposition-bridge legs remain open. diff --git a/docs/proof-transport.adoc b/docs/proof-transport.adoc index e1a4731..36b35bf 100644 --- a/docs/proof-transport.adoc +++ b/docs/proof-transport.adoc @@ -1,5 +1,5 @@ = Proof Transport Across Trust Boundaries -:revdate: 2026-09-07 +:revdate: 2026-11-01 :toc: The module `EpistemicTypes.ProofTransport` enforces semantic soundness relative @@ -105,10 +105,11 @@ empty meaning. The examples establish: These are proofs about an actual Boolean checking function in the model, not certificates that an external physical action occurred. -`just check` checks the whole library and four files that must be rejected: -`LyingVerifier`, `ForgedAcceptance`, `ReplayedArtifact`, and -`ReplayedHolder`. The rejection runner requires the intended type-mismatch -diagnostic; a missing import or broken tool does not count as a pass. +`just check` checks all 22 source modules and 13 expected-rejection controls. +Four controls target proof transport directly: `LyingVerifier`, +`ForgedAcceptance`, `ReplayedArtifact`, and `ReplayedHolder`. The rejection +runner requires Agda exit 42 and the intended type-mismatch diagnostic; a +missing import or broken tool does not count as a pass. == Migration and remaining scope diff --git a/docs/secret-types.adoc b/docs/secret-types.adoc index 40e37af..e22619a 100644 --- a/docs/secret-types.adoc +++ b/docs/secret-types.adoc @@ -4,7 +4,7 @@ :toc: macro :toclevels: 3 :icons: font -:revdate: 2026-10-05 +:revdate: 2026-11-01 [abstract] This note records a concrete first model for issue #32: a two-level, @@ -56,6 +56,38 @@ Status of the related issues: repository, and the guard that keeps this pointer accurate is link:https://github.com/hyperpolymath/epistemic-types/issues/39[issue #39]. +[[status_2026_11_01]] +== Current standalone status — source-reviewed 2026-11-01 + +This section supersedes external-status details below without rewriting the +historical 2026-10-25 record. `hyperpolymath/secret-types` is the standalone, +production repository for this family; that operational status does not turn +its deliberately bounded formal fragment into a complete IFC system. Source +review at `f581f8295bdee854f76291ab884a16cc8114dc6f` confirms its current +`PROOF-STATUS.adoc` still records: + +* generic termination-insensitive noninterference over its `Lattice` record, + arbitrary variables with decidable equality, labels, and down-closed + observers — **PROVEN**; +* the two-point `L ⊑ H` theorem (`Public ⊑ Secret` in this note) as an + instance — **PROVEN**; +* necessity countermodels for the exact lattice/observer laws — **PROVEN**; +* rejected explicit/implicit/third-variable flows and the minimal-laws + certificate — **TESTED**; +* termination-sensitive noninterference and declassification — **OPEN**. + +The fragment excludes procedures, concurrency, timing and declassification; +termination is its named open channel. This repository imports none of that +code and gains no confidentiality theorem from the documentary pointer. Its +only live responsibility is to preserve the boundary: no `Secret` API, label +lattice, implemented noninterference theorem, or confidentiality guarantee is +added to `epistemic-types`. + +The standalone README still contains some vintage issue wording; it is not +used here to reverse the owner's closure of `epistemic-types#32` or the +standalone ownership decision. Exact current proof claims come from the +standalone proof ledger, not from those stale sentences. + [[status_2026_10_25]] == Status update — 2026-10-25 diff --git a/docs/what-epistemic-is.adoc b/docs/what-epistemic-is.adoc index 7bd7c76..1c1f930 100644 --- a/docs/what-epistemic-is.adoc +++ b/docs/what-epistemic-is.adoc @@ -7,8 +7,9 @@ Jonathan D.A. Jewell (hyperpolymath) _An upfront, scholarly statement of what the central object of this repository is, what established structure it instantiates, what is ours versus borrowed, -and what it is deliberately NOT. Read against `AFFIRMATION.adoc` (the dated, -signed ground truth) — this statement must not, and does not, contradict it._ +and what it is deliberately NOT. `AFFIRMATION.adoc` is a dated June 2026 +verification snapshot; where its inventory or roadmap differs, the source and +`PROOF-STATUS.adoc` supersede it rather than rewriting that historical record._ toc::[] @@ -26,7 +27,8 @@ accessibility contexts, warrant regimes). The reading of `E κ A` is that `A` is *epistemically available from standpoint `κ`*: known, believed, observed, warranted, inferable, or assertable under that standpoint. This is the operative definition as the code actually uses it, and it is the form named in -`README.adoc` and verified green in `AFFIRMATION.adoc`. +`README.adoc`. The current checker profile and receipt state live in +`PROOF-STATUS.adoc`; `AFFIRMATION.adoc` is a dated historical receipt. The library's defining move is to *separate the interfaces* rather than ship one omnibus modality (`src/EpistemicTypes/Base.agda`): @@ -39,10 +41,10 @@ omnibus modality (`src/EpistemicTypes/Base.agda`): * `ReturnModality` makes a strong introduction rule explicit only when wanted. Warrant is treated as deliberately *non-factive but proof-relevant* -(`src/EpistemicTypes/Warrant.agda`). `Warrant κ A` records a *type of evidence -tokens* `Evidence : Set wℓ` for a claim `A` and carries *no* field -`Evidence -> A`; `Epi κ A` packages a warrant with one such token, and holding -`Epi κ A` *still does not give you `A`*. Soundness is a *separate* interface, +(`src/EpistemicTypes/Warrant.agda`). `Warrant K κ A` records a *type of +evidence tokens* `Evidence : Set wℓ` for a claim `A` and carries *no* field +`Evidence -> A`; `Epi K κ A` packages a warrant with one such token, and +holding `Epi K κ A` *still does not give you `A`*. Soundness is a *separate* interface, `SoundWarrant`, which alone adds the map `sound : Evidence -> A` (exposed as `sound-epi`). So an evidence token is an instrument of attestation, not a licence to extract the proposition. @@ -62,22 +64,21 @@ proofhood through a successful sound check of an explicit `Meaning holder artifact claim`. `proofSound` derives that meaning; `proofNeedsChecker` remains a weaker structural projection. Public transport requires a proved implication between the holders' meanings. The earlier -token-only encoding did not establish semantic truth. All of the above -type-checks under `--safe --without-K` with zero postulates, per -`AFFIRMATION.adoc`. +token-only encoding did not establish semantic truth. All of the above is in the current 22-module source tree. The exact checker +profile and receipt status are recorded in `PROOF-STATUS.adoc`; the June counts +in `AFFIRMATION.adoc` are historical. == The established structure it instantiates (and where it is from) -Honesty first, because it is load-bearing: unlike the sibling repos echo-types -(which is provably the fibre / a graded-loss modality) and tropical-resource-typing -(provably a dioid), epistemic-types' *deep* mathematical identity is -*deliberately unsettled*. The repository's own `README.adoc` lists "concrete -Kripke-style and evidence-state models" (roadmap #2) and the -monadic/comonadic *variance* question (roadmap #7) as *intentionally -unformalized*, and `AFFIRMATION.adoc` confirms the Kripke semantics is absent, -not hidden. The object is *operationally* very clearly defined as used; its -*deep placement* is open. So below we *name the candidate established frames* -without committing to one. +Honesty first, because it is load-bearing: epistemic-types' *single deep +mathematical identity* remains deliberately unsettled. The former Kripke gap is +closed: `src/EpistemicTypes/Kripke/` now implements +a world-indexed `Box`, constructive frame correspondences, a non-factive model, +a residual-candidate frame, and a dependence counterexample. The open question +is whether this scoped semantics, explicit-warrant reading, and map-only base +select one deeper placement or remain a useful assembly of established +structures. No monadic/comonadic variance verdict follows from the Kripke +milestone. * *Epistemic logic.* The modal treatment of knowledge and belief as distinct operators, with belief deliberately lacking the truth (factivity) axiom that @@ -88,9 +89,10 @@ without committing to one. * *Kripke semantics / relational possible-worlds models.* Saul A. Kripke, "Semantical Considerations on Modal Logic," _Acta Philosophica Fennica_ 16 - (1963), pp. 83–94. Our preorder accessibility `κ ≤κ κ'` is an accessibility - relation in this sense; but we have *not* built the worlds-and-valuation - semantics, so this is a candidate frame, not a realised one. + (1963), pp. 83–94. The repository now has a realised, scoped relational + semantics: `Frame`, world-indexed `Box`, T and 4 in both constructive + directions, and the forward 5 and D maps. It is not a complete epistemic + logic, and the converses of 5 and D are not claimed. * *Justification logic / the Logic of Proofs* — the *standout* candidate. Sergei Artemov, "Explicit Provability and Constructive Semantics," @@ -116,12 +118,12 @@ without committing to one. a `Set`-indexed modality with transport along an order; we cite it conservatively at the level of the field rather than pinning one paper. -The *work that would pin the placement* is the Kripke set-out itself (roadmap -#2): take worlds to be *candidate readings / natures of an object* (the von -Neumann–data / Curry–Howard–proof / game-semantic indeterminacy of one -artefact), and a standpoint's accessibility to be *what that standpoint can -discern* among those readings. Until that is built and checked, the deep -identity is a hypothesis, and we say so. +The implemented Kripke set-out establishes one precise semantics but does not, +by itself, settle the object's positive identity. `Kripke.Residual` interprets +worlds as candidate readings constrained by observation and evidence; +`Kripke.Dependence` then proves that candidate sets alone do not determine +which assumptions a conclusion depends on. The deep-identity question remains +a hypothesis at exactly that broader level, not as a claim that no frame exists. == What is ours, and what is not (the contribution boundary) @@ -134,13 +136,15 @@ What is *ours* is the *modelling and assembly*: the specific Agda *interface-separation* (`Modality` / `LawfulModality` / `FactiveModality` / `BeliefModality` / `ReturnModality`; `Warrant` versus `SoundWarrant`), and the *standpoint-indexed proof-transport* calculus that makes proofhood holder-relative -and proves semantic soundness relative to Meaning through `proofSound`. The usefulness is *demonstrated by concrete, -checkable artefacts* recorded as ground truth in `AFFIRMATION.adoc`: - -* the whole library type-checks *cold and green* under `--safe --without-K` - (`just check`, exit 0, all 10 modules), hardened by a `-W error` pass and an - honesty probe that confirms `--safe` *rejects* an injected `postulate` - (`[SafeFlagPostulate]`, exit 42), with zero escape hatches across `src/`; +and proves semantic soundness relative to Meaning through `proofSound`. Its +usefulness is demonstrated by concrete, checkable artefacts in the source and +current proof ledger: + +* the authoritative inventory is 22 source modules and 13 expected-rejection + controls; `tests/check-policy.sh` enforces the complete strict pragma, + standalone import boundary, zero escape hatches, and a generated + `[SafeFlagPostulate]` negative control; the hosted profile receipt status is + recorded in `PROOF-STATUS.adoc`; * `Warrant.sound-epi` makes extraction `Evidence -> A` available *only* via the separate `SoundWarrant.sound` field — non-factivity by construction; * `Examples.no-polymorphic-belief-reflection` and @@ -151,9 +155,13 @@ checkable artefacts* recorded as ground truth in `AFFIRMATION.adoc`: `designatedBindsHolder`, `opaqueNotCertifying`, and `verifyReceiptIsGap` giving the explicitly qualified public portability / designated-bound / receipt-never-certifies distinction. -These results are consumed downstream: the proof-transport / warrant-gap model is -used by *snifs* (deniable, non-forging attestation) and is named as the -*K-CUT-WARRANT* proof home for choreographic-types. +These results are used as source interfaces downstream. In particular, +choreographic-types imports the warrant interface and reports K-CUT-LOSS, +directional K-CUT-WARRANT bounds and transport, and asynchronous variants as +proved for its finite binary/plain-merge fragment. It does *not* close +payload/data-dependent warrant soundness, recursion, full merge, or every +asynchronous generalisation. Those are sibling results and limits, not local +proofs silently absorbed here. [NOTE] ==== @@ -166,19 +174,49 @@ identity, BEAM sandboxing, structured information loss — in places the establi not been instantiated this way, and we report only where the fit has already produced *checkable artefacts*. The contribution is the model and its demonstrated usefulness, not the underlying mathematics. This is deliberate, and it is a strength: a claim that concedes its own -foundations is survivable; one that claims invention dies at the first citation. (Cf. the -estate discipline — echo-types' own distinctness claim was permitted to terminate negatively, -EI-2.) +foundations is survivable; one that claims invention dies at the first citation. +Echo-types' EI-2 integration-recipe investigation is now *closed negatively via +PATH B*: the recipe did not carry substantive simultaneous cross-axis content, +so the distinctness claim was narrowed and positive identity remains open. That +negative result is not an invitation to reopen EI-2 from this repository. ==== +== Current sibling boundaries (documentary, not imported) + +* *Echo Types*: EI-2 terminated negatively through PATH B and narrowed the + integration-based distinctness claim. Positive identity remains open. The + canonical Echo correspondence checked here is representation/lowering only. +* *Residual Evidence Types*: the repository is operated in production, while + its own README still classifies the mathematical/API maturity as early + research with no stable API. Its checked corpus has advanced through + dependence-preserving composition, revision/retraction, and a certified + finite checker/explorer correspondence. This repository proves one local + mirror result and does not stabilise or absorb that API. +* *Secret Types*: the standalone repository owns confidentiality labels and + proves generic termination-insensitive noninterference over its `Lattice` + record/down-closed observers, with the two-point theorem as an instance. + Termination-sensitive noninterference and declassification remain open. No + `Secret` API or IFC theorem is added here; `docs/secret-types.adoc` is a + boundary/history note. +* *Choreographic Types*: only the scoped K-CUT results described above are + imported as documentary status. Universal K-CUT or global + data-dependent-warrant soundness is not claimed. + +These statements were source-reviewed on 2026-11-01 at choreographic-types +`8751c7d192d52e79dd285be3fdd095f96bdc5fe4`, echo-types +`b0982c44f36133acd2d0e1d4e03cf031fff7a470`, residual-evidence-types +`97244f5cb63bd6697caff261b187b62e9788b692`, and secret-types +`f581f8295bdee854f76291ab884a16cc8114dc6f`. They are not build dependencies +and do not turn an external proof receipt into a local theorem. + == Is-not, and what is still open To keep boundaries un-eroded: -* epistemic-types *is NOT a complete epistemic logic or a Kripke semantics* — by - its own statement (`README.adoc` "What remains intentionally unformalized"; - `AFFIRMATION.adoc` "Prototype scope"). It formalises honesty-preserving - *interfaces* and real *separation theorems*, not a worlds-and-valuation model. +* epistemic-types *is NOT a complete epistemic logic*. It now does implement a + scoped constructive Kripke semantics, including worlds, accessibility, `Box`, + exact frame-condition maps, and countermodels. It does not claim classical + converse 5/D, completeness, decidability, or a runtime epistemic system. * epistemic-types *is NOT factive by default*. Factivity (`reflect`, `SoundWarrant.sound`) is a *separate, assumed* interface; the default `Warrant`/`Belief` carry no truth axiom. A reader who treats a warrant as a @@ -195,12 +233,10 @@ To keep boundaries un-eroded: * the `SurrealBridge` *is NOT* the full Conway proper class of surreals — only the finite `daySurrealAccess` birthday tower over `Nat` is inhabited. -*Honestly open* (the parts we do not yet claim, mirroring the readme roadmap): -the Kripke / evidence-state semantics that would *pin* the deep identity -(#2); lawful (law-bearing) modality *instances* proved rather than assumed (#3); -warrant *soundness* as an optional, proved interface (#4); a graded comonad for -echo-types and the full graded-loss logic (#5); richer day-bounded surreal -fragments (#6); and the *variance* verdict — whether any specific epistemic -modality deserves *monadic or comonadic* structure (#7). It is *too early to -name the single deep answer*, and that is the correct state to be in: the object -is sharp as used and open where it should be open. +*Honestly open*: a complete epistemic logic beyond the implemented frame +fragment; classical converse 5/D if desired; data-dependent warrant soundness; +law-bearing modality instances where laws are currently fields; a graded +comonad and full graded-loss logic; richer day-bounded surreal fragments; and +the variance verdict for any specific epistemic modality. The Kripke semantics +itself is no longer on that list. It remains too early to name one positive deep +identity, and no generic `bind` or `extract` is promised. diff --git a/explainme.adoc b/explainme.adoc index dfb9c7e..7f5148e 100644 --- a/explainme.adoc +++ b/explainme.adoc @@ -1,7 +1,11 @@ = Explain Me: Epistemic Types +:revdate: 2026-11-01 -This project is a compact Agda sketch of standpoint-indexed epistemic modal -types. It favors mathematical honesty over a large API. +This project is a compact constructive Agda formalisation of +standpoint-indexed epistemic modal types. It favours mathematical honesty over +a large API. The exact proof ledger and current checker receipt are in +link:PROOF-STATUS.adoc[]; link:EXPLAINME.adoc[] supplies the detailed +claim-by-claim evidence table. == Core choice @@ -30,9 +34,9 @@ belief-reflection function would produce an inhabitant of the empty type. == Warrant -`Warrant κ A` is proof-relevant: it tells us what counts as an evidence token -for `A` at `κ`. `Epi κ A` packages a warrant and a token. This still does not -prove `A`. A sound warrant is a separate record with an explicit soundness +`Warrant K κ A` is proof-relevant: it tells us what counts as an evidence token +for `A` at `κ`. `Epi K κ A` packages a warrant and a token. This still does not +prove `A`. A sound warrant is a separate record with an explicit soundness function. == Reads and retained information @@ -87,13 +91,25 @@ acceptance, and refutes false claims. It does not claim that a physical action occurred. The older token-only model lacked semantic soundness; the strengthened interface is a breaking correction documented in link:docs/proof-transport.adoc[]. -== Roadmap +== Constructive Kripke scope -* First keep the tiny core stable and type-checking. -* Next add small concrete models: Kripke accessibility, evidence-state - semantics, and observation rules. -* Then add law-bearing records for proven functoriality, access transport, and - optional soundness. -* Add richer day-bounded surreal fragments as concrete bridge instances. -* Finally connect to the larger echo-type story through bridge modules that - preserve the distinction between grades and standpoints. +The five modules under `src/EpistemicTypes/Kripke/` provide a world-indexed +`Box`, constructive T and 4 in both directions, Euclidean-to-5, +serial-to-D, a concrete non-factive warrant, a residual-candidate frame, and a +local dependence mirror. They do not claim a complete epistemic logic, +classical converse 5/D, or global warrant soundness. Data-dependent warrant +soundness and correspondence with residual-evidence-types' owning record remain +open. + +== Verification and roadmap + +`just check` first enforces the complete strict source profile and the exact +22-source/13-rejection inventory, then checks each source module and each +intended rejection. CI pins Agda 2.6.4.3. The current Mathesis grade is not +inferred from prose; see `PROOF-STATUS.adoc` for the hosted receipt state. + +Remaining local work includes concrete data-dependent sound warrants, the +rational/rescaling and update obligations for the RapidNJ example, any desired +law-bearing modality instances, and richer finite-day bridge models. Generic +`bind`/`extract`, Echo-as-resource, sibling API stabilisation, and +confidentiality/IFC are not commitments of this repository. diff --git a/scripts/check.sh b/scripts/check.sh index a3678e1..422db86 100755 --- a/scripts/check.sh +++ b/scripts/check.sh @@ -10,7 +10,10 @@ cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.." required_agda=2.6.4.3 +# Run the policy, proof and rejection gates in order. A failing gate stops the +# script with that gate's exit status. run_gates() { + bash tests/check-policy.sh bash tests/check-proofs.sh bash tests/check-rejections.sh } diff --git a/tests/check-policy.sh b/tests/check-policy.sh new file mode 100755 index 0000000..d381d29 --- /dev/null +++ b/tests/check-policy.sh @@ -0,0 +1,265 @@ +#!/usr/bin/env bash +# Proof-policy conformance and negative control. +set -euo pipefail +cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.." + +required_options='{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}' + +# shellcheck disable=SC2034 # consumed through require_exact_inventory namerefs +expected_source_modules=( + src/EpistemicTypes/Access.agda + src/EpistemicTypes/All.agda + src/EpistemicTypes/Applications/IntegerModel.agda + src/EpistemicTypes/Applications/OrderedGroup.agda + src/EpistemicTypes/Applications/QCriterion.agda + src/EpistemicTypes/Applications/RapidNJExamples.agda + src/EpistemicTypes/Applications/RapidNJSkip.agda + src/EpistemicTypes/Applications/SortedRow.agda + src/EpistemicTypes/Base.agda + src/EpistemicTypes/ContinuityExamples.agda + src/EpistemicTypes/EchoBridge.agda + src/EpistemicTypes/Examples.agda + src/EpistemicTypes/Kripke/Belief.agda + src/EpistemicTypes/Kripke/Dependence.agda + src/EpistemicTypes/Kripke/Frame.agda + src/EpistemicTypes/Kripke/Indexed.agda + src/EpistemicTypes/Kripke/Residual.agda + src/EpistemicTypes/ProofTransport.agda + src/EpistemicTypes/ProofTransportExample.agda + src/EpistemicTypes/ReadConsistency.agda + src/EpistemicTypes/SurrealBridge.agda + src/EpistemicTypes/Warrant.agda +) +# shellcheck disable=SC2034 # consumed through require_exact_inventory namerefs +expected_rejection_fixtures=( + tests/reject/BeliefIsKnowledge.agda + tests/reject/FakeFreshness.agda + tests/reject/ForgedAcceptance.agda + tests/reject/ForgedResidue.agda + tests/reject/ForkedHistory.agda + tests/reject/InventedMigration.agda + tests/reject/LyingVerifier.agda + tests/reject/MismatchedSource.agda + tests/reject/ReplayedArtifact.agda + tests/reject/ReplayedHolder.agda + tests/reject/StaleSample.agda + tests/reject/UncheckedSkip.agda + tests/reject/UnderstatedBound.agda +) +# shellcheck disable=SC2034 # consumed through require_exact_inventory namerefs +expected_integration_modules=( + tests/integration/CanonicalEcho.agda +) + +collect_agda_paths() { + local root=$1 array_name=$2 output + local -n destination=$array_name + destination=() + if ! output=$(find "$root" -type f -name '*.agda' -print | LC_ALL=C sort); then + printf 'FAIL: could not enumerate Agda files below %s\n' "$root" + exit 1 + fi + if [[ -n $output ]]; then + mapfile -t destination <<< "$output" + fi +} + +require_exact_inventory() { + local label=$1 expected_name=$2 actual_name=$3 index=0 + local -n expected=$expected_name actual=$actual_name + if [[ ${#expected[@]} -eq ${#actual[@]} ]]; then + for ((index = 0; index < ${#expected[@]}; index += 1)); do + [[ ${expected[index]} == "${actual[index]}" ]] || break + done + fi + if [[ ${#expected[@]} -ne ${#actual[@]} || $index -lt ${#expected[@]} ]]; then + printf 'FAIL: %s inventory differs from its authoritative manifest\n' "$label" + printf '%s\n' '--- expected' + printf '%s\n' "${expected[@]}" + printf '%s\n' '--- actual' + printf '%s\n' "${actual[@]}" + exit 1 + fi +} + +source_modules=() +rejection_fixtures=() +integration_modules=() +collect_agda_paths src/EpistemicTypes source_modules +collect_agda_paths tests/reject rejection_fixtures +collect_agda_paths tests/integration integration_modules +require_exact_inventory 'source-module' expected_source_modules source_modules +require_exact_inventory 'rejection-fixture' expected_rejection_fixtures rejection_fixtures +require_exact_inventory 'integration-module' expected_integration_modules integration_modules + +for module in "${source_modules[@]}" "${rejection_fixtures[@]}" "${integration_modules[@]}"; do + [[ $(head -n 1 "$module") == "$required_options" ]] || { + printf 'FAIL: %s does not declare the complete strict OPTIONS profile first\n' "$module" + exit 1 + } + + # The required first line must be the only OPTIONS pragma. This prevents a + # later pragma from weakening exact splitting, termination or other policy. + options_count=0 + line_number=0 + while IFS= read -r line || [[ -n $line ]]; do + ((line_number += 1)) + if [[ $line =~ \{\-\#[[:space:]]*OPTIONS([[:space:]]|#) ]]; then + ((options_count += 1)) + [[ $line_number -eq 1 && $line == "$required_options" ]] || { + printf 'FAIL: %s:%s contains an additional or non-canonical OPTIONS pragma\n' \ + "$module" "$line_number" + exit 1 + } + fi + done < "$module" + [[ $options_count -eq 1 ]] || { + printf 'FAIL: %s must contain exactly one OPTIONS pragma, found %s\n' \ + "$module" "$options_count" + exit 1 + } +done + +# The load-bearing tree and positive integration witness must not contain proof +# escape hatches or unresolved holes. The generated negative control below is +# intentionally outside the repository tree. +if rg -n \ + -e '^[[:space:]]*postulate([[:space:]]|$)' \ + -e '\{\-#[[:space:]]*(TERMINATING|NON_TERMINATING|NO_TERMINATION_CHECK|NON_COVERING|NO_COVERAGE_CHECK|NO_POSITIVITY_CHECK|NO_UNIVERSE_CHECK|POLARITY)' \ + -e '\b(believe_me|primTrustMe|trustMe|unsafeCoerce|assert_total|Admitted|sorry)\b' \ + -e '\{!' -e '!\}' \ + src tests/integration -g '*.agda'; then + echo 'FAIL: banned proof construct or unresolved hole found in positive proof sources' + exit 1 +else + rg_status=$? + [[ $rg_status -eq 1 ]] || { + printf 'FAIL: banned proof scan failed (rg exit %s)\n' "$rg_status" + exit 1 + } +fi + +# Core source is deliberately standalone: only Agda builtins/primitive and +# modules owned by this repository may be imported. Scan lexical tokens rather +# than line starts so `module M where open import X` cannot evade the boundary; +# strip line, nested block and string contents before interpreting `import`. +check_core_imports() { + local module=$1 line code pair char token imported + local line_number=0 index comment_depth=0 in_string=0 escaped=0 + local expect_module=0 import_line=0 + local -a tokens=() + + [[ -r $module ]] || { + printf 'FAIL: cannot read source while scanning imports: %s\n' "$module" + return 1 + } + + while IFS= read -r line || [[ -n $line ]]; do + ((line_number += 1)) + code= + in_string=0 + escaped=0 + for ((index = 0; index < ${#line}; index += 1)); do + char=${line:index:1} + pair=${line:index:2} + + if ((comment_depth > 0)); then + if [[ $pair == '{-' ]]; then + ((comment_depth += 1)) + ((index += 1)) + elif [[ $pair == '-}' ]]; then + comment_depth=$((comment_depth - 1)) + ((index += 1)) + fi + continue + fi + + if ((in_string)); then + if ((escaped)); then + escaped=0 + elif [[ $char == '\\' ]]; then + escaped=1 + elif [[ $char == '"' ]]; then + in_string=0 + fi + code+=' ' + continue + fi + + if [[ $pair == '--' ]]; then + break + elif [[ $pair == '{-' ]]; then + ((comment_depth += 1)) + ((index += 1)) + code+=' ' + elif [[ $char == '"' ]]; then + in_string=1 + code+=' ' + else + case "$char" in + ';'|'{'|'}'|'('|')') code+=' ' ;; + *) code+=$char ;; + esac + fi + done + + tokens=() + read -r -a tokens <<< "$code" + for token in "${tokens[@]}"; do + if ((expect_module)); then + imported=$token + case "$imported" in + Agda.Builtin.*|Agda.Primitive|EpistemicTypes.*) ;; + *) + printf 'FAIL: non-core import in standalone source at %s:%s: %s\n' \ + "$module" "$import_line" "$imported" + return 1 + ;; + esac + expect_module=0 + elif [[ $token == import ]]; then + expect_module=1 + import_line=$line_number + fi + done + done < "$module" + + ((comment_depth == 0)) || { + printf 'FAIL: unterminated block comment while scanning imports: %s\n' "$module" + return 1 + } + ((expect_module == 0)) || { + printf 'FAIL: import without a module name at %s:%s\n' "$module" "$import_line" + return 1 + } +} + +for module in "${source_modules[@]}"; do + check_core_imports "$module" +done + +# Negative control for the checker itself. A missing tool or unrelated parser +# error is not accepted as evidence that --safe rejects postulates. +tmpdir=$(mktemp -d) +trap 'rm -rf "$tmpdir"' EXIT +cat > "$tmpdir/SafeFlagPostulate.agda" <<'AGDA' +{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-} +module SafeFlagPostulate where + +postulate + escape : {A : Set} → A +AGDA +status=0 +diagnostic=$(agda --no-libraries --safe --without-K --cubical-compatible \ + --exact-split --no-sized-types --no-guardedness \ + --double-check --ignore-interfaces -W error -i "$tmpdir" \ + "$tmpdir/SafeFlagPostulate.agda" 2>&1) || status=$? +if [[ $status -ne 42 ]] || \ + ! rg -q '\[SafeFlagPostulate\]|Cannot postulate .*safe flag' <<< "$diagnostic"; then + printf 'FAIL: --safe negative control failed for an unexpected reason (exit %s)\n%s\n' \ + "$status" "$diagnostic" + exit 1 +fi + +printf 'PASS: exact policy manifest covers %s source modules, %s rejection fixtures and %s integration witness; --safe rejects the planted postulate\n' \ + "${#source_modules[@]}" "${#rejection_fixtures[@]}" "${#integration_modules[@]}" diff --git a/tests/check-proofs.sh b/tests/check-proofs.sh index c55b2f3..924531a 100644 --- a/tests/check-proofs.sh +++ b/tests/check-proofs.sh @@ -7,8 +7,98 @@ cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.." # Applications/ tree) are gated even when they are not re-exported by All.agda. mapfile -t modules < <(find src/EpistemicTypes -name '*.agda' | sort) [[ ${#modules[@]} -gt 0 ]] || { echo 'FAIL: no proof modules'; exit 1; } + +agda_flags=( + --no-libraries + --safe + --without-K + --cubical-compatible + --exact-split + --no-sized-types + --no-guardedness + --double-check + --ignore-interfaces + -i src +) + +# Agda 2.6.4.3 reports cubical transport-computation limitations for these +# existing indexed eliminations. The category-level suppression in the strict +# pass is paired with a second pass that must reproduce this exact location +# manifest: a warning at any new span fails the gate, as does a stale entry. +allowed_unsupported_locations=( + "src/EpistemicTypes/Applications/IntegerModel.agda:80,1-21" + "src/EpistemicTypes/Applications/IntegerModel.agda:89,1-90,66" + "src/EpistemicTypes/Applications/IntegerModel.agda:236,22-43" + "src/EpistemicTypes/Applications/SortedRow.agda:58,3-59,54" + "src/EpistemicTypes/Applications/SortedRow.agda:78,3-82,24" + "src/EpistemicTypes/ContinuityExamples.agda:174,3-33" + "src/EpistemicTypes/EchoBridge.agda:156,1-157,49" + "src/EpistemicTypes/EchoBridge.agda:168,1-169,58" + "src/EpistemicTypes/Examples.agda:36,1-40,33" + "src/EpistemicTypes/Kripke/Belief.agda:32,1-23" + "src/EpistemicTypes/Kripke/Dependence.agda:76,1-77,67" + "src/EpistemicTypes/Kripke/Residual.agda:61,1-62,33" + "src/EpistemicTypes/ProofTransport.agda:108,1-111,91" + "src/EpistemicTypes/ProofTransport.agda:130,1-82" + "src/EpistemicTypes/ProofTransport.agda:187,1-189,59" + "src/EpistemicTypes/ProofTransport.agda:201,1-49" + "src/EpistemicTypes/ProofTransport.agda:224,1-81" + "src/EpistemicTypes/ProofTransport.agda:231,1-85" + "src/EpistemicTypes/ReadConsistency.agda:51,1-52,44" + "src/EpistemicTypes/ReadConsistency.agda:62,1-38" + "src/EpistemicTypes/SurrealBridge.agda:212,1-213,44" + "src/EpistemicTypes/SurrealBridge.agda:216,1-217,42" + "src/EpistemicTypes/SurrealBridge.agda:232,1-233,48" +) +declare -A allowed_unsupported=() +declare -A observed_unsupported=() +for location in "${allowed_unsupported_locations[@]}"; do + allowed_unsupported["$location"]=1 +done + +# All warning categories except the location-audited category remain errors. for module in "${modules[@]}"; do - agda --no-libraries --safe --without-K --double-check --ignore-interfaces \ - -W error -W noUnsupportedIndexedMatch -i src "$module" + agda "${agda_flags[@]}" -W error -W noUnsupportedIndexedMatch "$module" done -printf 'PASS: %s source modules checked under the required proof discipline\n' "${#modules[@]}" + +for module in "${modules[@]}"; do + status=0 + diagnostic=$(agda "${agda_flags[@]}" -W noerror "$module" 2>&1) || status=$? + [[ $status -eq 0 ]] || { + printf 'FAIL: warning audit could not check %s (Agda exit %s)\n%s\n' \ + "$module" "$status" "$diagnostic" + exit 1 + } + + previous_line= + while IFS= read -r diagnostic_line; do + if [[ $diagnostic_line == 'warning: -W[no]UnsupportedIndexedMatch' ]]; then + location=${previous_line#"$PWD/"} + [[ -n ${allowed_unsupported["$location"]+present} ]] || { + printf 'FAIL: UnsupportedIndexedMatch outside the reviewed manifest while checking %s\n' \ + "$module" + printf 'location: %s\n' "$location" + exit 1 + } + observed_unsupported["$location"]=1 + fi + previous_line=$diagnostic_line + done <<< "$diagnostic" +done + +# Fail when an exception becomes stale: removing or moving a warning must also +# update the suppression audit and the corresponding proof-ledger qualification. +for location in "${allowed_unsupported_locations[@]}"; do + [[ -n ${observed_unsupported["$location"]+present} ]] || { + printf 'FAIL: documented UnsupportedIndexedMatch was not observed at %s\n' "$location" + exit 1 + } +done +[[ ${#observed_unsupported[@]} -eq ${#allowed_unsupported_locations[@]} ]] || { + printf 'FAIL: warning manifest cardinality mismatch (expected %s, observed %s)\n' \ + "${#allowed_unsupported_locations[@]}" "${#observed_unsupported[@]}" + exit 1 +} + +printf 'PASS: %s source modules checked; UnsupportedIndexedMatch is confined to %s audited source spans\n' \ + "${#modules[@]}" "${#allowed_unsupported_locations[@]}" diff --git a/tests/check-rejections.sh b/tests/check-rejections.sh index c529d89..82c2127 100644 --- a/tests/check-rejections.sh +++ b/tests/check-rejections.sh @@ -12,8 +12,13 @@ actual_files=$(rg --files tests/reject -g '*.agda' | sort) [[ "$actual_files" == "$expected_files" ]] || { echo 'FAIL: rejection manifest differs from files'; exit 1; } for fixture in "${fixtures[@]}"; do status=0 - diagnostic=$(agda --no-libraries --safe --without-K --double-check --ignore-interfaces -W error -W noUnsupportedIndexedMatch \ - -i src -i tests/reject "tests/reject/$fixture.agda" 2>&1) || status=$? + # Source warning locations are audited by check-proofs.sh; this suppression + # only lets each negative fixture reach the exact mismatch asserted below. + diagnostic=$(agda --no-libraries --safe --without-K --cubical-compatible \ + --exact-split --no-sized-types --no-guardedness \ + --double-check --ignore-interfaces \ + -W error -W noUnsupportedIndexedMatch -i src -i tests/reject \ + "tests/reject/$fixture.agda" 2>&1) || status=$? if [[ "$status" -eq 0 ]]; then printf 'FAIL: %s unexpectedly type-checked\n' "$fixture" exit 1 diff --git a/tests/integration/CanonicalEcho.agda b/tests/integration/CanonicalEcho.agda index 665d10c..f612e9c 100644 --- a/tests/integration/CanonicalEcho.agda +++ b/tests/integration/CanonicalEcho.agda @@ -1,4 +1,4 @@ -{-# OPTIONS --safe --without-K #-} +{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-} module CanonicalEcho where diff --git a/www/.well-known/ai.txt b/www/.well-known/ai.txt index 60ae8f6..df58eb3 100644 --- a/www/.well-known/ai.txt +++ b/www/.well-known/ai.txt @@ -8,27 +8,30 @@ Disallow-Generation: yes # 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: a constructive development checked -# under {-# OPTIONS --safe --without-K #-}, with no postulates and no use of -# the Agda standard library (built with 'agda --no-libraries', relying only -# on Agda.Builtin.* and Agda.Primitive). +# mathematical honesty over a large API. Every first-party module declares +# --safe --without-K --cubical-compatible --exact-split --no-sized-types and +# --no-guardedness. Core source has no postulates, proof escape hatches, or +# Agda-standard-library imports; the pinned canonical-Echo integration is a +# separate check with explicit sibling/stdlib inputs. # # AI agents may read and analyze this code to assist contributors, to reason # about the proofs, and to answer questions about the formalization. # AI agents must NOT use this code for model training without explicit consent. -# AI agents must not introduce postulates, must not depend on the Agda standard -# library, and must not weaken the --safe --without-K guarantees. +# AI agents must not introduce postulates, depend on the Agda standard library +# from core source, or weaken the strict profile. # # For AI agent integration instructions, see: -# .machine_readable/descriptiles/0-AI-MANIFEST.a2ml (universal AI entry point) -# .machine_readable/descriptiles/STATE.a2ml (structured project state) -# .machine_readable/proof-transport/ (a2ml + k9 rendering of the -# ProofTransport attestation model) +# 0-AI-MANIFEST.a2ml (universal AI entry point) +# .machine_readable/descriptiles/STATE.a2ml (structured project state) +# .machine_readable/proof-transport/ (a2ml + k9 rendering of the +# ProofTransport model) # -# Human-facing docs: readme.adoc, explainme.adoc +# Human-facing docs: README.adoc, explainme.adoc, EXPLAINME.adoc, +# PROOF-STATUS.adoc, PROOF-NEEDS.adoc # # Build / check: 'just check' -# == agda --no-libraries -i src src/EpistemicTypes/All.agda (Agda 2.6.4.3) +# == policy guard + all 22 source modules + all 13 expected rejections +# under the canonical profile (CI-pinned Agda 2.6.4.3) # # CI is enabled: proof constructions, semantic rejections, canonical Echo # correspondence, CodeQL Actions and secret scanning. See docs/ci-safety.adoc. diff --git a/www/.well-known/humans.txt b/www/.well-known/humans.txt index 8172f83..9a5aba7 100644 --- a/www/.well-known/humans.txt +++ b/www/.well-known/humans.txt @@ -7,20 +7,20 @@ From: United Kingdom /* THANKS */ The Agda developers, for a proof assistant honest enough to refuse -unsound shortcuts (--safe --without-K, no postulates). -The echo-types and ephapax projects, whose loss-with-residue and -echo-obligation work this library's EchoBridge composes with. +unsound shortcuts under the repository's strict safe profile. +The echo-types and ephapax projects, whose proof-relevant Echo and +echo-obligation work inform the separately pinned integration boundary. The standards / a2ml / k9-svc estate tooling, the engineering target for the ProofTransport attestation layer. /* SITE */ -Last update: 2026-06-15 +Last update: 2026-11-01 Standards: RSR (Rhodium Standard Repository) Version: 0.1.0 (prototype) Components: Agda formalization of standpoint-indexed modal / epistemic / echo-like type formers; favours mathematical honesty over a large - API. Constructive, no standard library (Agda.Builtin.* only). + API. Constructive; core source imports only builtins/primitive/local modules. Languages: Agda (source), a2ml + Nickel/k9 (machine-readable), AsciiDoc (docs) Tools: just, Agda 2.6.4.3 -Build: just check == agda --no-libraries -i src src/EpistemicTypes/All.agda -CI: not enabled (see AUDIT.adoc) +Build: just check == policy guard + 22 source modules + 13 expected rejections +CI: proof/security workflows enabled; see AUDIT.adoc and docs/ci-safety.adoc diff --git a/www/.well-known/security.txt b/www/.well-known/security.txt index f1268de..7014b2b 100644 --- a/www/.well-known/security.txt +++ b/www/.well-known/security.txt @@ -4,11 +4,12 @@ # epistemic-types: a small, deliberately honest Agda formalization of # standpoint-indexed modal / epistemic / echo-like type formers. # This is a single-tool Agda library (checked by 'just check'); it ships -# no runtime, services, network endpoints, or CI. Security reports should -# concern the library source, its proofs, or the machine-readable artifacts. +# no runtime, services, or network endpoints. Proof and security CI are enabled. +# Security reports should concern the library source, its proofs, its proof +# gates, or the machine-readable artifacts. Contact: mailto:j.d.a.jewell@open.ac.uk -Expires: 2027-06-15T23:59:59.000Z +Expires: 2027-11-01T23:59:59.000Z Preferred-Languages: en Canonical: https://github.com/hyperpolymath/epistemic-types/blob/main/.well-known/security.txt -Policy: https://github.com/hyperpolymath/epistemic-types/blob/main/SECURITY.md +Policy: https://github.com/hyperpolymath/epistemic-types/blob/main/SECURITY.adoc