diff --git a/.clinerules b/.clinerules new file mode 100644 index 0000000..0e8f23d --- /dev/null +++ b/.clinerules @@ -0,0 +1,24 @@ +# SPDX-License-Identifier: MPL-2.0 +# Cline rules for nextgen-typing. Full rules: AGENTS.md / CLAUDE.md. + +# ⛔ COORDINATION REPO — NOT A CODE REPO. +# nextgen-typing documents and connects the type-theory pipeline +# (katagoria → typell → typed-wasm → PanLL). It does NOT hold compiler, +# kernel, language, or single-project code — including single-project proofs, +# benchmarks, and tests. +# +# Before creating ANY implementation file or single-project proof here: STOP. +# Put it in the owning repo. Routing table: +# .machine_readable/bot_directives/placement.a2ml (authoritative) +# AGENTS.md (human-readable) +# CI enforces this: scripts/check-coordination-boundary.sh +# +# Only these belong here: coordination/architecture docs, .machine_readable/ +# state, estate governance/CI scaffold, and CROSS-project proofs in +# verification/proofs/ that import >=2 constituent repos (e.g. agda/EchoTyping.agda). + +# Then: read 0-AI-MANIFEST.a2ml, then .machine_readable/6a2/STATE.a2ml. +# Licence MPL-2.0 (never AGPL) + SPDX header on every file. +# Banned langs: TypeScript->ReScript, npm/Node->Deno, Go->Rust, Python->Julia/Rust. +# Containers: Podman + Containerfile. Build via just. +# No believe_me / assert_total / postulate / sorry / Admitted / unsafeCoerce. diff --git a/.cursorrules b/.cursorrules new file mode 100644 index 0000000..697cd70 --- /dev/null +++ b/.cursorrules @@ -0,0 +1,24 @@ +# SPDX-License-Identifier: MPL-2.0 +# Cursor rules for nextgen-typing. Full rules: AGENTS.md / CLAUDE.md. + +# ⛔ COORDINATION REPO — NOT A CODE REPO. +# nextgen-typing documents and connects the type-theory pipeline +# (katagoria → typell → typed-wasm → PanLL). It does NOT hold compiler, +# kernel, language, or single-project code — including single-project proofs, +# benchmarks, and tests. +# +# Before creating ANY implementation file or single-project proof here: STOP. +# Put it in the owning repo. Routing table: +# .machine_readable/bot_directives/placement.a2ml (authoritative) +# AGENTS.md (human-readable) +# CI enforces this: scripts/check-coordination-boundary.sh +# +# Only these belong here: coordination/architecture docs, .machine_readable/ +# state, estate governance/CI scaffold, and CROSS-project proofs in +# verification/proofs/ that import >=2 constituent repos (e.g. agda/EchoTyping.agda). + +# Then: read 0-AI-MANIFEST.a2ml, then .machine_readable/6a2/STATE.a2ml. +# Licence MPL-2.0 (never AGPL) + SPDX header on every file. +# Banned langs: TypeScript->ReScript, npm/Node->Deno, Go->Rust, Python->Julia/Rust. +# Containers: Podman + Containerfile. Build via just. +# No believe_me / assert_total / postulate / sorry / Admitted / unsafeCoerce. diff --git a/.github/copilot-instructions.md b/.github/copilot-instructions.md index cd2d3fb..9fceca8 100644 --- a/.github/copilot-instructions.md +++ b/.github/copilot-instructions.md @@ -7,6 +7,18 @@ Copyright (c) Jonathan D.A. Jewell # Copilot Instructions +## ⛔ Before Writing Anything — Placement Boundary + +`nextgen-typing` is a **coordination repo**, not a code repo. Do NOT add +compiler/application code or single-project proofs here. If content implements +or proves something about ONE project, put it in that project's repo. Routing +table: `.machine_readable/bot_directives/placement.a2ml` (enforced in CI by +`scripts/check-coordination-boundary.sh`). Full guidance: `AGENTS.md`. + +Only these belong here: coordination/architecture docs, `.machine_readable/` +state, estate governance/CI scaffold, and CROSS-project proofs (importing ≥2 +constituent repos) under `verification/proofs/`. + ## Before Writing Code - Read `0-AI-MANIFEST.a2ml` in the repo root for canonical file locations. @@ -47,12 +59,6 @@ Copyright (c) Jonathan D.A. Jewell - Name the file `Containerfile`, never `Dockerfile`. - Base image: `cgr.dev/chainguard/wolfi-base:latest`. -## ABI/FFI - -- ABI definitions in Idris2 (`src/interface/abi/`). -- FFI implementations in Zig (`src/interface/ffi/`). -- Generated C headers in `src/interface/generated/`. - ## State Files Never create these in the repo root: diff --git a/.github/workflows/coordination-boundary.yml b/.github/workflows/coordination-boundary.yml new file mode 100644 index 0000000..293a06e --- /dev/null +++ b/.github/workflows/coordination-boundary.yml @@ -0,0 +1,32 @@ +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# Coordination-boundary guard: nextgen-typing must stay docs + machine-readable +# state + estate scaffold + CROSS-project proofs only — no compiler/application +# code and no single-project proofs. Routing table: +# .machine_readable/bot_directives/placement.a2ml +name: Coordination Boundary + +on: + push: + branches: [main, master, develop] + pull_request: + branches: [main, master, develop] + +permissions: + contents: read + +concurrency: + group: coord-boundary-${{ github.ref }} + cancel-in-progress: true + +jobs: + boundary: + runs-on: ubuntu-latest + timeout-minutes: 5 + permissions: + contents: read + steps: + - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + - name: Enforce coordination boundary + run: bash scripts/check-coordination-boundary.sh diff --git a/.machine_readable/6a2/AGENTIC.a2ml b/.machine_readable/6a2/AGENTIC.a2ml index 79484e4..b9efdcb 100644 --- a/.machine_readable/6a2/AGENTIC.a2ml +++ b/.machine_readable/6a2/AGENTIC.a2ml @@ -22,6 +22,10 @@ can-create-files = true # - Never use banned languages (TypeScript, Python, Go, etc.) # - Never place state files in repository root (must be in .machine_readable/) # - Never use AGPL license (use MPL-2.0) +# - Never add compiler/application code or single-project proofs to this +# coordination repo; route them to the owning repo per +# .machine_readable/bot_directives/placement.a2ml (CI-enforced by +# scripts/check-coordination-boundary.sh). [maintenance-integrity] fail-closed = true diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index f8b79ca..3c24792 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -6,7 +6,7 @@ [metadata] project = "nextgen-typing" version = "0.1.0" -last-updated = "2026-06-15" +last-updated = "2026-06-19" status = "active" [project-context] @@ -24,6 +24,11 @@ Does NOT contain compiler code. # scaffold was removed (it was a strict subset of the canonical proofs in # verification/proofs/); "no compiler code" is affirmed. Completion still reflects # early state: the verification proofs in verification/proofs/ are not yet built in CI. +# 2026-06-19: the "7 mandated proofs" were RSR template residue (ABI/TP proofs +# owned by typed-wasm/typell); PROOF-NEEDS/PROOF-STATUS reconciled to track only +# cross-project proofs. The coordination boundary is now CI-enforced +# (scripts/check-coordination-boundary.sh) and documented in AGENTS.md/CLAUDE.md +# + .machine_readable/bot_directives/placement.a2ml. completion-percentage = 10 [position] @@ -84,6 +89,7 @@ events = [ { date = "2026-05-30", kind = "ci", detail = "CI reusable-wrapper rework (2026-05-26..2026-05-30): hypatia-scan, scorecard, secret-scanner, rust-ci, and mirror workflows converted to thin wrappers of standards reusables; reusable SHA pins repinned to live merge-commit SHAs (commit 4a848fd)." }, { date = "2026-06-09", kind = "docs", detail = "README.adoc: TypeFix Zero (TF0) calibration-calculus section added (commits f11cc29..ec3496f)." }, { date = "2026-06-12", kind = "governance", detail = "Estate standardization merged (governance docs, bot_directives, self-validating, flat contractiles, flake.nix removal); codeql cron monthly; checkpoint layer: dual STATE reconciled (root pointer-ized to 6a2), bot_directives trio added, contractiles populated with repo-true obligations." }, + { date = "2026-06-19", kind = "governance", detail = "Coordination-boundary remediation: added AGENTS.md/CLAUDE.md + root .clinerules/.cursorrules/.windsurfrules, placement.a2ml routing directive, and a coordination-boundary CI guard + pre-commit hook; stripped the RSR src/interface ABI/FFI instructions from copilot-instructions/cline/cursor/windsurf/AI-CONVENTIONS and rewrote the template-residue AI.a2ml; removed the RSR ABI/TP proof scaffold from verification/proofs/ (owned by typed-wasm/typell), keeping the cross-project echo-types proof; reconciled PROOF-NEEDS/PROOF-STATUS." }, ] [ecosystem] diff --git a/.machine_readable/ai/.clinerules b/.machine_readable/ai/.clinerules index a29ed5f..bbb3eb6 100644 --- a/.machine_readable/ai/.clinerules +++ b/.machine_readable/ai/.clinerules @@ -34,10 +34,11 @@ # File: Containerfile (never Dockerfile). # Base: cgr.dev/chainguard/wolfi-base:latest or cgr.dev/chainguard/static:latest. -# ABI/FFI -# ABI: Idris2 with dependent types (src/interface/abi/). -# FFI: Zig with C ABI (src/interface/ffi/). -# Headers: src/interface/generated/. +# COORDINATION REPO — NO PROJECT CODE +# nextgen-typing is coordination-only: docs, .machine_readable/ state, estate +# scaffold, and CROSS-project proofs (>=2 constituent repos) in +# verification/proofs/. Do NOT add compiler/app code or single-project proofs. +# Route per .machine_readable/bot_directives/placement.a2ml (CI-enforced). # BUILD: Use just (justfile) for all tasks. # STYLE: Descriptive names. Document all files. SPDX headers everywhere. diff --git a/.machine_readable/ai/.cursorrules b/.machine_readable/ai/.cursorrules index c13b393..a63bdbe 100644 --- a/.machine_readable/ai/.cursorrules +++ b/.machine_readable/ai/.cursorrules @@ -33,10 +33,11 @@ # File: Containerfile (never Dockerfile) # Base: cgr.dev/chainguard/wolfi-base:latest -# ABI/FFI STANDARD -# ABI definitions: Idris2 with dependent types (src/interface/abi/) -# FFI implementation: Zig with C ABI (src/interface/ffi/) -# Generated C headers: src/interface/generated/ +# COORDINATION REPO — NO PROJECT CODE +# nextgen-typing is coordination-only: docs, .machine_readable/ state, estate +# scaffold, and CROSS-project proofs (>=2 constituent repos) in +# verification/proofs/. Do NOT add compiler/app code or single-project proofs. +# Route per .machine_readable/bot_directives/placement.a2ml (CI-enforced). # BUILD SYSTEM # Use just (justfile) for all build, test, lint, and format tasks. diff --git a/.machine_readable/ai/.windsurfrules b/.machine_readable/ai/.windsurfrules index a29ed5f..bbb3eb6 100644 --- a/.machine_readable/ai/.windsurfrules +++ b/.machine_readable/ai/.windsurfrules @@ -34,10 +34,11 @@ # File: Containerfile (never Dockerfile). # Base: cgr.dev/chainguard/wolfi-base:latest or cgr.dev/chainguard/static:latest. -# ABI/FFI -# ABI: Idris2 with dependent types (src/interface/abi/). -# FFI: Zig with C ABI (src/interface/ffi/). -# Headers: src/interface/generated/. +# COORDINATION REPO — NO PROJECT CODE +# nextgen-typing is coordination-only: docs, .machine_readable/ state, estate +# scaffold, and CROSS-project proofs (>=2 constituent repos) in +# verification/proofs/. Do NOT add compiler/app code or single-project proofs. +# Route per .machine_readable/bot_directives/placement.a2ml (CI-enforced). # BUILD: Use just (justfile) for all tasks. # STYLE: Descriptive names. Document all files. SPDX headers everywhere. diff --git a/.machine_readable/ai/AI.a2ml b/.machine_readable/ai/AI.a2ml index 8d89c20..147a3c0 100644 --- a/.machine_readable/ai/AI.a2ml +++ b/.machine_readable/ai/AI.a2ml @@ -1,38 +1,38 @@ # SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -# AI Assistant Instructions +# AI Assistant Instructions — nextgen-typing -## Repository Focus -- `rsr-template-repo` is treated as a Rhodium Standard Repository; obey the Rhodium policies and keep `.machine_readable/` authoritative. -- All machine-readable content lives under `.machine_readable/` — state files (a2ml), bot directives, and contractiles. -- Prefer to keep generated files out of source control, and regenerate them with the documented commands before committing. +## ⛔ Placement Boundary (read first) + +nextgen-typing is the **coordination repo** for the type-theory pipeline +(katagoria → typell → typed-wasm → PanLL). It is NOT a code repo: no compiler, +kernel, language, or single-project code — and no single-project proofs, +benchmarks, or tests. + +If content implements or proves something about ONE project, it belongs in that +project's repo. Use the routing table: +- `.machine_readable/bot_directives/placement.a2ml` (authoritative, CI-enforced) +- `AGENTS.md` / `CLAUDE.md` (human-readable) + +Only these belong here: coordination/architecture docs, `.machine_readable/` +state, estate governance/CI scaffold, and CROSS-project proofs (importing ≥2 +constituent repos) under `verification/proofs/`. ## Workflow -1. Inspect `.machine_readable/6a2/STATE.a2ml` for blockers and next actions. -2. Respect any constraints listed inside `.machine_readable/AGENTIC.a2ml` when tooling changes are requested. -3. After finishing edits, update STATE with your outcomes and commit with a concise, imperative message. - -## Delivery Promises -- Mention in summaries whether STATE, `.machine_readable/contractiles/`, or `.machine_readable/bot_directives/` changed. -- Keep this file in sync with the repository's status; update it if the governance changes. - -[foundational-integrations] -# These tools form the architectural floor for all hyperpolymath repos. -# Integrate them incrementally as the project matures. - -proven = "Formally verified safety library — replace raw string/JSON/URL/crypto ops" -panic-attacker = "Static analysis — run `just assail` before every commit" -feedback-o-tron = "Autonomous bug filing — auto-report upstream dependency failures" -verisimdb = "Cross-repo analytics — emit scan results and build metrics" -vexometer = "Irritation surface analysis — measure friction in CLI/UI tools" -hypatia = "Neurosymbolic CI/CD — safety-triangle routing for automated fixes" -boj-server = "MCP gateway — all external service integrations route through BoJ" - -[floor-raise-checklist] -step-1 = "Ensure 0-AI-MANIFEST.a2ml exists at repo root" -step-2 = "Ensure Mustfile.a2ml + Trustfile.a2ml + Dustfile.a2ml in .machine_readable/contractiles/" -step-3 = "Add `assail` recipe to Justfile and wire into pre-commit hook" -step-4 = "Add proven integration reference in .machine_readable/integrations/" -step-5 = "Add verisimdb feed configuration" -step-6 = "Add feedback-o-tron integration for upstream reporting" -step-7 = "Add vexometer hooks for friction measurement (CLI/UI repos)" + +1. Read `0-AI-MANIFEST.a2ml`, then `.machine_readable/6a2/STATE.a2ml` for + blockers and next actions. +2. Respect `.machine_readable/6a2/AGENTIC.a2ml` constraints. +3. Before creating any file, confirm placement against `placement.a2ml`. +4. After edits, update STATE with outcomes; commit with a concise message. + +## Conventions + +- Licence MPL-2.0 + SPDX header on every file (never AGPL). +- `.a2ml` state files live in `.machine_readable/` only, never the repo root. +- Banned languages: TypeScript→ReScript, npm/Node→Deno, Go→Rust, Python→Julia/Rust. +- Containers: Podman + `Containerfile`. Build/test via `just`. +- No unsound escape hatches: believe_me, assert_total, postulate, sorry, + Admitted, unsafeCoerce, Obj.magic. +- Full rules: `docs/practice/AI-CONVENTIONS.adoc`. diff --git a/.machine_readable/bot_directives/README.adoc b/.machine_readable/bot_directives/README.adoc index 688dbb6..d8ea13d 100644 --- a/.machine_readable/bot_directives/README.adoc +++ b/.machine_readable/bot_directives/README.adoc @@ -38,10 +38,17 @@ interactive agents. | `debt.a2ml` | Meander debt — things found but not fixed, carried between sessions + +| `placement.a2ml` +| Content-routing directive — WHERE content belongs in the estate. What this + coordination repo accepts vs what must be routed to a constituent repo. + Authoritative source behind AGENTS.md and the coordination-boundary CI check. |=== == How Agents Use These +0. Consult `placement.a2ml` BEFORE creating any file — confirm it belongs in a + coordination repo; if it implements or proves one project, route it out. 1. Read `methodology.a2ml` at session start — know mode, invariants, ceiling 2. Read `coverage.a2ml` — know what was visited last time, what was skipped 3. Read `debt.a2ml` — know what's outstanding from previous sessions diff --git a/.machine_readable/bot_directives/placement.a2ml b/.machine_readable/bot_directives/placement.a2ml new file mode 100644 index 0000000..40b78ba --- /dev/null +++ b/.machine_readable/bot_directives/placement.a2ml @@ -0,0 +1,83 @@ +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# placement.a2ml — content-routing directive (authoritative) +# +# WHERE content belongs in the type-theory estate. This is the machine-readable +# source of truth behind AGENTS.md / CLAUDE.md and the coordination-boundary CI +# check (scripts/check-coordination-boundary.sh). Agents MUST consult this +# before creating files in nextgen-typing. + +[metadata] +version = "1.0.0" +last-updated = "2026-06-19" +applies-to = "nextgen-typing" +precedence = "maintainer > this directive > bot defaults" + +[identity] +repo = "nextgen-typing" +role = "coordination-monorepo" +rule = """ +nextgen-typing documents and connects the type-theory pipeline +(katagoria -> typell -> typed-wasm -> PanLL). It contains NO compiler, kernel, +language, or single-project code -- including single-project proofs, benchmarks, +and tests. If content implements or proves something about ONE project, it +belongs in that project's repo, not here. +""" + +# What this repo accepts. Anything not matching belongs elsewhere (see [routing]). +[accepts] +allowed = [ + "Coordination & architecture docs (README, ROADMAP, TOPOLOGY, docs/ARCHITECTURE, docs/PIPELINE, docs/decisions ADRs)", + "Machine-readable pipeline state (.machine_readable/)", + "Estate governance / CI scaffold", + "Cross-project formal proofs in verification/proofs/ that import or relate >=2 constituent repos", + "Research artefacts that genuinely span multiple projects", +] + +# What this repo rejects -> route to the owning repo. +[rejects] +disallowed = [ + "Compiler / kernel / language implementation code", + "Single-project formal proofs (proofs about exactly one constituent repo)", + "Single-project ABI/FFI definitions, benchmarks, or tests", + "A code scaffold (src/, crates/, Cargo.toml) of any kind", +] + +# Routing table. `owns` = the canonical repo for that subject matter. +[routing] +rules = [ + { subject = "type-theory research prototypes, Idris2/Lean PoCs, reading notes", owns = "kategoria" }, + { subject = "TypeLL kernel: dependent/linear/session types, QTT, proof-carrying code, effects", owns = "typell" }, + { subject = "WasmGC memory-safety proofs, verified convergence ABI, aggregate-library conventions", owns = "typed-wasm" }, + { subject = "echo-types library: fiber-based structured loss (Echo/EchoLinear/EchoResidue/EchoCharacteristic)", owns = "echo-types", companion = "EchoTypes.jl" }, + { subject = "choreographic / multiparty session types", owns = "choreographic-types" }, + { subject = "TypeFix Zero / micro-Type-0 calibration calculus", owns = "typefix-zero" }, + { subject = "AffineScript language code", owns = "affinescript" }, + { subject = "Ephapax language code / region calculus", owns = "ephapax" }, + { subject = "query-language type safety (SQL/GraphQL/Cypher/SPARQL/VQL)", owns = "typedqliser", also = "vcl-ut" }, + { subject = "tropical / semiring type theory (Isabelle/Lean)", owns = "tropical-resource-typing" }, + { subject = "transport-adapter / max-plus pathfinding", owns = "protocol-squisher" }, + { subject = "eNSAID reference env (downstream consumer of TypeLL)", owns = "panll" }, +] + +# Cross-project proofs are the ONLY proofs allowed in verification/proofs/. +# A proof qualifies only if it imports/relates >=2 constituent repos. New +# entries require a conscious decision: add the path here AND to the allowlist +# in scripts/check-coordination-boundary.sh. +[verification] +cross-project-only = true +allowed-proofs = [ + "verification/proofs/agda/EchoTyping.agda", # relates echo-types <-> AffineScript/typed-wasm pipeline + "verification/proofs/agda/Verification.agda", # aggregator that typechecks the cross-project set + "verification/proofs/agda/nextgen-typing.agda-lib", +] +route-elsewhere = [ + "ABI/FFI/memory-layout proofs -> typed-wasm", + "TypeLL kernel proofs -> typell", + "echo-types library proofs -> echo-types", + "single-project type-soundness proofs -> the owning repo", +] + +[on-uncertainty] +action = "Open an issue in nextgen-typing proposing where the content should live. Do NOT commit code or single-project proofs here on spec." diff --git a/.pre-commit-config.yaml b/.pre-commit-config.yaml index 29d0fef..aed03b7 100644 --- a/.pre-commit-config.yaml +++ b/.pre-commit-config.yaml @@ -50,3 +50,13 @@ repos: rev: v8.24.3 hooks: - id: gitleaks + + # --- Coordination boundary (this repo is coordination-only) --- + - repo: local + hooks: + - id: coordination-boundary + name: Coordination boundary (no project code / single-project proofs) + entry: scripts/check-coordination-boundary.sh + language: script + pass_filenames: false + always_run: true diff --git a/.windsurfrules b/.windsurfrules new file mode 100644 index 0000000..c399b67 --- /dev/null +++ b/.windsurfrules @@ -0,0 +1,24 @@ +# SPDX-License-Identifier: MPL-2.0 +# Windsurf rules for nextgen-typing. Full rules: AGENTS.md / CLAUDE.md. + +# ⛔ COORDINATION REPO — NOT A CODE REPO. +# nextgen-typing documents and connects the type-theory pipeline +# (katagoria → typell → typed-wasm → PanLL). It does NOT hold compiler, +# kernel, language, or single-project code — including single-project proofs, +# benchmarks, and tests. +# +# Before creating ANY implementation file or single-project proof here: STOP. +# Put it in the owning repo. Routing table: +# .machine_readable/bot_directives/placement.a2ml (authoritative) +# AGENTS.md (human-readable) +# CI enforces this: scripts/check-coordination-boundary.sh +# +# Only these belong here: coordination/architecture docs, .machine_readable/ +# state, estate governance/CI scaffold, and CROSS-project proofs in +# verification/proofs/ that import >=2 constituent repos (e.g. agda/EchoTyping.agda). + +# Then: read 0-AI-MANIFEST.a2ml, then .machine_readable/6a2/STATE.a2ml. +# Licence MPL-2.0 (never AGPL) + SPDX header on every file. +# Banned langs: TypeScript->ReScript, npm/Node->Deno, Go->Rust, Python->Julia/Rust. +# Containers: Podman + Containerfile. Build via just. +# No believe_me / assert_total / postulate / sorry / Admitted / unsafeCoerce. diff --git a/0-AI-MANIFEST.a2ml b/0-AI-MANIFEST.a2ml index 0adc017..a7f3785 100644 --- a/0-AI-MANIFEST.a2ml +++ b/0-AI-MANIFEST.a2ml @@ -8,6 +8,21 @@ theory pipeline. It does NOT contain compiler code. Pipeline: katagoria → typell → typed-wasm → PanLL +## STOP — Placement Rule (the most common mistake here) + +Before creating ANY file, confirm it belongs in a coordination repo. This repo +holds ONLY: coordination/architecture docs, `.machine_readable/` state, estate +governance/CI scaffold, and CROSS-project proofs (importing ≥2 constituent +repos) under `verification/proofs/`. + +If the content implements or proves something about ONE project, it belongs in +that project's repo — NOT here. Route it with the table in +`.machine_readable/bot_directives/placement.a2ml` (authoritative; CI-enforced +by `scripts/check-coordination-boundary.sh`). Examples: TypeLL kernel → +`typell`; ABI/WasmGC → `typed-wasm`; echo-types library → `echo-types`; +research PoCs → `kategoria`; μType₀ → `typefix-zero`; choreographic types → +`choreographic-types`. When unsure, open an issue — do not commit code on spec. + ## Critical Invariants 1. **TypeLL is open-ended** — never say "TypeLL is a 10-level system". The @@ -27,6 +42,7 @@ Pipeline: katagoria → typell → typed-wasm → PanLL - Current state + blockers: `.machine_readable/6a2/STATE.a2ml` - ADRs: `.machine_readable/6a2/META.a2ml` - Ecosystem relationships: `.machine_readable/6a2/ECOSYSTEM.a2ml` +- Content routing (what goes where): `.machine_readable/bot_directives/placement.a2ml` - Human overview: `README.adoc` - What-is-this explainer: `EXPLAINME.adoc` diff --git a/AGENTS.md b/AGENTS.md new file mode 100644 index 0000000..47fbcd5 --- /dev/null +++ b/AGENTS.md @@ -0,0 +1,72 @@ + + + +# AGENTS.md — read this before writing any file + +> This is the cross-tool agent entry point (Claude, Copilot, Cursor, Cline, +> Windsurf, Gemini, the gitbot fleet, …). `CLAUDE.md` is identical to this file. + +## ⛔ STOP — `nextgen-typing` is a COORDINATION repo, not a code repo + +It **documents and connects** the hyperpolymath type-theory pipeline. It does +**NOT** contain compiler, kernel, language, or single-project code — and that +includes proofs, benchmarks, and tests that belong to one project. + +**If you are about to add implementation code or a single-project proof here: +stop and put it in the owning repo instead** (table below). Adding project code +to this repo is the single most common mistake agents make here, and CI will +reject it (`scripts/check-coordination-boundary.sh`). + +The pipeline: + +``` +katagoria → typell → typed-wasm → PanLL (TypeFix Zero / μType₀ sits beside it) +(research) (kernel) (target) (eNSAID env) +``` + +## ✅ What belongs HERE — and only this + +- Coordination & architecture docs: `README.adoc`, `ROADMAP.adoc`, `TOPOLOGY.md`, + `docs/ARCHITECTURE.adoc`, `docs/PIPELINE.adoc`, ADRs in `docs/decisions/`. +- Machine-readable pipeline state: `.machine_readable/`. +- Estate governance / CI scaffold shared across hyperpolymath repos. +- **Cross-project** formal proofs in `verification/proofs/` — *only* proofs that + import/relate **two or more** constituent repos. The one current example is + `verification/proofs/agda/EchoTyping.agda`, which relates the `echo-types` + library to the AffineScript/typed-wasm pipeline. +- Research artefacts that genuinely span multiple projects. + +## ❌ What does NOT belong here — route it to the owning repo + +| If the content is about… | Put it in… | +|---|---| +| Type-theory research prototypes, Idris2/Lean PoCs, reading notes | `kategoria` | +| The TypeLL kernel: dependent / linear / session types, QTT, proof-carrying code, effects | `typell` | +| WasmGC memory-safety proofs, the verified convergence ABI, aggregate-library conventions | `typed-wasm` | +| The echo-types library itself (Echo / EchoLinear / EchoResidue / structured-loss) | `echo-types` (Agda) · `EchoTypes.jl` (Julia) | +| Choreographic / multiparty session types | `choreographic-types` | +| TypeFix Zero / μType₀ calibration calculus | `typefix-zero` | +| AffineScript / Ephapax language code | `affinescript` · `ephapax` | +| Query-language type safety (SQL/GraphQL/Cypher/SPARQL/VQL) | `typedqliser` · `vcl-ut` | +| Tropical / semiring type theory (Isabelle/Lean) | `tropical-resource-typing` | +| Transport-adapter / max-plus pathfinding | `protocol-squisher` | +| Any compiler/app code, single-project ABI/FFI, benchmarks, or tests | the owning project repo | + +**Rule of thumb:** if it *implements* or *proves* something about **one** +project, it does **not** go here. If you are unsure where something belongs, +open an issue in this repo proposing a home — do **not** commit code here on spec. + +The machine-readable form of this table is the source of truth: +`.machine_readable/bot_directives/placement.a2ml`. It is enforced in CI by +`.github/workflows/coordination-boundary.yml`. + +## After the boundary, follow the estate conventions + +1. Read `0-AI-MANIFEST.a2ml`, then `.machine_readable/6a2/STATE.a2ml`. +2. Full rules: `docs/practice/AI-CONVENTIONS.adoc`. +3. Licence **MPL-2.0** + SPDX header on every file (never AGPL). +4. Banned languages: TypeScript→ReScript, npm/Node→Deno, Go→Rust, Python→Julia/Rust. + Containers: Podman + `Containerfile`. Build/test via `just`. +5. No unsound escape hatches in any proof: `believe_me`, `assert_total`, + `postulate`, `sorry`, `Admitted`, `unsafeCoerce`, `Obj.magic`. +6. Author: Jonathan D.A. Jewell (hyperpolymath) . diff --git a/CLAUDE.md b/CLAUDE.md new file mode 100644 index 0000000..d71df0e --- /dev/null +++ b/CLAUDE.md @@ -0,0 +1,73 @@ + + + +# CLAUDE.md — read this before writing any file + +> This file is **identical to `AGENTS.md`** and exists so tools that look for +> `CLAUDE.md` get the same rules. The machine-readable routing table is +> `.machine_readable/bot_directives/placement.a2ml` (authoritative). + +## ⛔ STOP — `nextgen-typing` is a COORDINATION repo, not a code repo + +It **documents and connects** the hyperpolymath type-theory pipeline. It does +**NOT** contain compiler, kernel, language, or single-project code — and that +includes proofs, benchmarks, and tests that belong to one project. + +**If you are about to add implementation code or a single-project proof here: +stop and put it in the owning repo instead** (table below). Adding project code +to this repo is the single most common mistake agents make here, and CI will +reject it (`scripts/check-coordination-boundary.sh`). + +The pipeline: + +``` +katagoria → typell → typed-wasm → PanLL (TypeFix Zero / μType₀ sits beside it) +(research) (kernel) (target) (eNSAID env) +``` + +## ✅ What belongs HERE — and only this + +- Coordination & architecture docs: `README.adoc`, `ROADMAP.adoc`, `TOPOLOGY.md`, + `docs/ARCHITECTURE.adoc`, `docs/PIPELINE.adoc`, ADRs in `docs/decisions/`. +- Machine-readable pipeline state: `.machine_readable/`. +- Estate governance / CI scaffold shared across hyperpolymath repos. +- **Cross-project** formal proofs in `verification/proofs/` — *only* proofs that + import/relate **two or more** constituent repos. The one current example is + `verification/proofs/agda/EchoTyping.agda`, which relates the `echo-types` + library to the AffineScript/typed-wasm pipeline. +- Research artefacts that genuinely span multiple projects. + +## ❌ What does NOT belong here — route it to the owning repo + +| If the content is about… | Put it in… | +|---|---| +| Type-theory research prototypes, Idris2/Lean PoCs, reading notes | `kategoria` | +| The TypeLL kernel: dependent / linear / session types, QTT, proof-carrying code, effects | `typell` | +| WasmGC memory-safety proofs, the verified convergence ABI, aggregate-library conventions | `typed-wasm` | +| The echo-types library itself (Echo / EchoLinear / EchoResidue / structured-loss) | `echo-types` (Agda) · `EchoTypes.jl` (Julia) | +| Choreographic / multiparty session types | `choreographic-types` | +| TypeFix Zero / μType₀ calibration calculus | `typefix-zero` | +| AffineScript / Ephapax language code | `affinescript` · `ephapax` | +| Query-language type safety (SQL/GraphQL/Cypher/SPARQL/VQL) | `typedqliser` · `vcl-ut` | +| Tropical / semiring type theory (Isabelle/Lean) | `tropical-resource-typing` | +| Transport-adapter / max-plus pathfinding | `protocol-squisher` | +| Any compiler/app code, single-project ABI/FFI, benchmarks, or tests | the owning project repo | + +**Rule of thumb:** if it *implements* or *proves* something about **one** +project, it does **not** go here. If you are unsure where something belongs, +open an issue in this repo proposing a home — do **not** commit code here on spec. + +The machine-readable form of this table is the source of truth: +`.machine_readable/bot_directives/placement.a2ml`. It is enforced in CI by +`.github/workflows/coordination-boundary.yml`. + +## After the boundary, follow the estate conventions + +1. Read `0-AI-MANIFEST.a2ml`, then `.machine_readable/6a2/STATE.a2ml`. +2. Full rules: `docs/practice/AI-CONVENTIONS.adoc`. +3. Licence **MPL-2.0** + SPDX header on every file (never AGPL). +4. Banned languages: TypeScript→ReScript, npm/Node→Deno, Go→Rust, Python→Julia/Rust. + Containers: Podman + `Containerfile`. Build/test via `just`. +5. No unsound escape hatches in any proof: `believe_me`, `assert_total`, + `postulate`, `sorry`, `Admitted`, `unsafeCoerce`, `Obj.magic`. +6. Author: Jonathan D.A. Jewell (hyperpolymath) . diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md index d4292d5..299ae0d 100644 --- a/PROOF-NEEDS.md +++ b/PROOF-NEEDS.md @@ -2,60 +2,44 @@ SPDX-License-Identifier: MPL-2.0 Copyright (c) Jonathan D.A. Jewell --> -# Proof Requirements — NEXTGEN_TYPING - - +# Proof Requirements — nextgen-typing -## Proof Tier - - -**Tier**: T3 — Standard - -## Proof Categories - -| Code | Meaning | Applies? | -|------|---------|----------| -| **TP** | Typing Proofs (type soundness, type safety) | Yes | -| **INV** | Invariant Proofs (state machines, monotonicity, bounds) | | -| **SEC** | Security Proofs (crypto, injection freedom, access control) | | -| **CONC** | Concurrency Proofs (linearizability, deadlock freedom) | | -| **ALG** | Algorithm Proofs (termination, correctness, bounds) | | -| **ABI** | ABI/FFI Proofs (memory layout, pointer safety, platform compat) | Yes | -| **DOM** | Domain-Specific Proofs (bespoke to this project) | | - -## Mandatory Proofs (All RSR Repos) - -These proofs come from the rsr-template-repo and MUST be present in every repo: +> **nextgen-typing is a coordination repo.** It does not own compiler or +> application code, so it has **no single-project proof obligations**. The +> RSR-template "mandatory ABI/FFI + typing proofs" do **not** apply here — +> those obligations live in the repos that own the code (e.g. ABI/FFI and +> memory-layout proofs belong in `typed-wasm`; kernel proofs in `typell`). +> +> This repo hosts only **cross-project** proofs — proofs that import or relate +> two or more constituent repos. Routing: `.machine_readable/bot_directives/placement.a2ml`. -### ABI/FFI Boundary Proofs (Idris2) - -| # | Proof | Status | File | -|---|-------|--------|------| -| ABI-1 | Non-null pointer proofs (`So (ptr /= 0)`) | Needed | `verification/proofs/idris2/ABI/Pointers.idr` | -| ABI-2 | Memory layout correctness (`HasSize`, `HasAlignment`) | Needed | `verification/proofs/idris2/ABI/Layout.idr` | -| ABI-3 | Platform type size proofs (per platform) | Needed | `verification/proofs/idris2/ABI/Platform.idr` | -| ABI-4 | FFI function return type proofs | Needed | `verification/proofs/idris2/ABI/Foreign.idr` | -| ABI-5 | C ABI compliance (`CABICompliant`, `FieldsAligned`) | Needed | `verification/proofs/idris2/ABI/Compliance.idr` | +## Proof Tier -### Typing Proofs (Prover Varies) +**Tier**: T5 — Exempt (coordination layer; no owned code to prove). +Cross-project proofs are hosted, not mandated. -| # | Proof | Status | File | -|---|-------|--------|------| -| TP-1 | Core data type well-formedness | Needed | `verification/proofs/idris2/Types.idr` | -| TP-2 | Public API type safety (exported functions) | Needed | `verification/proofs/lean4/ApiTypes.lean` | +## Cross-Project Proofs (the only category that applies here) -## Project-Specific Proofs +| # | Proof | Spans | Prover | Status | File | +|---|-------|-------|--------|--------|------| +| XP-1 | Pipeline information-loss = echo-types fibers (affine weakening + refinement erasure) | echo-types ↔ affinescript ↔ typed-wasm | Agda | Present | `verification/proofs/agda/EchoTyping.agda` | - - +A proof qualifies for this list only if it relates ≥2 constituent repos. When +adding one, register it in `[verification].allowed-proofs` of +`placement.a2ml` and in `ALLOWED_PROOFS` of +`scripts/check-coordination-boundary.sh`. -| # | Proof Needed | Category | Prover | Priority | File(s) | -|---|-------------|----------|--------|----------|---------| -| | | | | | | +## Where single-project proofs go (NOT here) -## Dangerous Patterns (BANNED) +| Subject | Owning repo | +|---------|-------------| +| ABI/FFI, memory layout, pointer safety, C-ABI compliance, WasmGC safety | `typed-wasm` | +| TypeLL kernel: dependent/linear/session types, QTT, proof-carrying code | `typell` | +| echo-types library internals (Echo/EchoLinear/EchoResidue) | `echo-types` | +| Research prototypes / PoCs | `kategoria` | +| Tropical / semiring type theory | `tropical-resource-typing` | -The following MUST NOT appear anywhere in proof files: +## Dangerous Patterns (BANNED in any hosted proof) | Pattern | Language | Meaning | |---------|----------|---------| @@ -66,41 +50,11 @@ The following MUST NOT appear anywhere in proof files: | `Admitted` | Coq | Incomplete proof | | `unsafeCoerce` | Haskell | Unsafe type cast | | `Obj.magic` | OCaml/ReScript | Unsafe type cast | -| `unsafe` (unaudited) | Rust | Unsafe block without safety comment | - -CI will reject any PR introducing these patterns (enforced by `panic-attack assail`). - -## Prover Selection Guide - -| Use Case | Recommended Prover | Why | -|----------|-------------------|-----| -| ABI/FFI boundaries | **Idris2** | Dependent types model layouts precisely | -| Type system proofs | **Coq** or **Lean4** | Mature proof assistants for metatheory | -| Algebraic properties | **Lean4** | Good mathlib support | -| Inductive/coinductive | **Agda** | Native support for (co)induction | -| Distributed systems | **TLA+** | Model checking for protocols | -| Numerical properties | **Isabelle** | Strong real analysis library | - -## Proof File Locations -``` -verification/proofs/ -├── idris2/ # Idris2 proofs (ABI, dependent types) -│ ├── ABI/ # ABI-specific proofs -│ └── *.idr # Project-specific Idris2 proofs -├── lean4/ # Lean4 proofs (algebra, lattices) -│ └── *.lean -├── agda/ # Agda proofs (induction, metatheory) -│ └── *.agda -├── coq/ # Coq proofs (type systems, compilation) -│ └── *.v -└── tlaplus/ # TLA+ specs (distributed protocols) - └── *.tla -``` +CI rejects any PR introducing these (`panic-attack assail`). ## References -- Master list: the canonical master list maintained in the hyperpolymath/standards repo +- Routing table: `.machine_readable/bot_directives/placement.a2ml` +- CI guard: `scripts/check-coordination-boundary.sh` / `.github/workflows/coordination-boundary.yml` - Proof status tracking: `PROOF-STATUS.md` (this repo) -- Proven library: `proven` repo (Idris2 verified foundations) -- Template: `rsr-template-repo/PROOF-NEEDS.md` diff --git a/PROOF-STATUS.md b/PROOF-STATUS.md index 15b9bea..ddb813c 100644 --- a/PROOF-STATUS.md +++ b/PROOF-STATUS.md @@ -2,83 +2,44 @@ SPDX-License-Identifier: MPL-2.0 Copyright (c) Jonathan D.A. Jewell --> -# Proof Status — NEXTGEN_TYPING - - +# Proof Status — nextgen-typing -## Summary - -| Category | Total | Done | In Progress | Blocked | Remaining | -|----------|-------|------|-------------|---------|-----------| -| ABI/FFI (ABI) | 5 | 0 | 0 | 0 | 5 | -| Typing (TP) | 2 | 0 | 0 | 0 | 2 | -| Invariant (INV) | 0 | 0 | 0 | 0 | 0 | -| Security (SEC) | 0 | 0 | 0 | 0 | 0 | -| Concurrency (CONC) | 0 | 0 | 0 | 0 | 0 | -| Algorithm (ALG) | 0 | 0 | 0 | 0 | 0 | -| Domain (DOM) | 0 | 0 | 0 | 0 | 0 | -| **Total** | **7** | **0** | **0** | **0** | **7** | - -**Overall**: 0% proven - -## Proofs Done - - - - - -| ID | Proof | Prover | File | Date | Verified By | -|----|-------|--------|------|------|-------------| -| — | No proofs completed yet | — | — | — | — | +> Coordination repo. The only proofs tracked here are **cross-project** proofs +> (spanning ≥2 constituent repos). Single-project proof status is tracked in the +> owning repos. Requirements: `PROOF-NEEDS.md`. -## Proofs In Progress - -| ID | Proof | Prover | Assignee | Started | Blocker | -|----|-------|--------|----------|---------|---------| -| — | — | — | — | — | — | +## Summary -## Proofs Blocked +| Category | Total | Done | In Progress | Remaining | +|----------|-------|------|-------------|-----------| +| Cross-project (XP) | 1 | 1 | 0 | 0 | +| **Total** | **1** | **1** | **0** | **0** | -| ID | Proof | Blocked By | Notes | -|----|-------|------------|-------| -| — | — | — | — | +The earlier "0 of 7" RSR ABI/TP figure was template residue: it counted +mandatory ABI/FFI + typing proofs that belong in `typed-wasm` / `typell`, not in +this coordination layer. Those scaffold files were removed (the ABI proof +obligations are owned by `typed-wasm`). -## Proofs Remaining +## Proofs Present -| ID | Proof | Category | Prover | Priority | Est. Effort | -|----|-------|----------|--------|----------|-------------| -| ABI-1 | Non-null pointer proofs | ABI | Idris2 | P1 | 2h | -| ABI-2 | Memory layout correctness | ABI | Idris2 | P1 | 4h | -| ABI-3 | Platform type size proofs | ABI | Idris2 | P1 | 2h | -| ABI-4 | FFI function return type proofs | ABI | Idris2 | P1 | 2h | -| ABI-5 | C ABI compliance | ABI | Idris2 | P1 | 4h | -| TP-1 | Core data type well-formedness | TP | Idris2 | P1 | 4h | -| TP-2 | Public API type safety | TP | Lean4 | P2 | 4h | +| ID | Proof | Spans | Prover | File | Verified By | +|----|-------|-------|--------|------|-------------| +| XP-1 | Pipeline information-loss = echo-types fibers | echo-types ↔ affinescript ↔ typed-wasm | Agda (`--safe --without-K`) | `verification/proofs/agda/EchoTyping.agda` | `agda Verification.agda` | -## Verification Commands +## Verification ```bash -# Check all Idris2 proofs -just proof-check-idris2 - -# Check all Lean4 proofs -just proof-check-lean4 - -# Check all Agda proofs -just proof-check-agda - -# Check all Coq proofs -just proof-check-coq - -# Run all proof checks -just proof-check-all +# Typecheck the cross-project Agda set (requires the echo-types library on the +# Agda include path; see verification/proofs/agda/nextgen-typing.agda-lib) +agda verification/proofs/agda/Verification.agda -# Scan for dangerous patterns -panic-attack assail --proofs-only +# Enforce the coordination boundary (no project code / non-allowlisted proofs) +bash scripts/check-coordination-boundary.sh ``` ## Changelog | Date | Change | By | |------|--------|-----| +| 2026-06-19 | Reconciled to coordination reality: removed RSR ABI/TP scaffold proofs (owned by typed-wasm/typell); tracking cross-project proofs only | maintainer | | 2026-04-04 | Initial proof status tracking | Template | diff --git a/docs/practice/AI-CONVENTIONS.adoc b/docs/practice/AI-CONVENTIONS.adoc index 1f45744..aa52167 100644 --- a/docs/practice/AI-CONVENTIONS.adoc +++ b/docs/practice/AI-CONVENTIONS.adoc @@ -9,6 +9,11 @@ All AI coding agents working in this repository MUST follow these rules. Per-tool config files (.cursorrules, .clinerules, etc.) reference this document. +**⛔ Placement first:** `nextgen-typing` is a *coordination repo*. Do not add +compiler/application code or single-project proofs here — route them to the +owning repo per `.machine_readable/bot_directives/placement.a2ml` (CI-enforced). +See `AGENTS.md` for the routing table. + ## Session Startup 1. Read `0-AI-MANIFEST.a2ml` FIRST (mandatory gatekeeper). @@ -66,11 +71,17 @@ MAINTENANCE-CHECKLIST.a2ml, or SOFTWARE-DEVELOPMENT-APPROACH.a2ml in the reposit - File: **Containerfile** (never Dockerfile). - Base images: `cgr.dev/chainguard/wolfi-base:latest` or `cgr.dev/chainguard/static:latest`. -## ABI/FFI Standard +## Coordination Boundary (what may be created here) + +`nextgen-typing` is a coordination repo: it holds coordination/architecture +docs, `.machine_readable/` state, estate governance/CI scaffold, and +*cross-project* proofs (importing ≥2 constituent repos) under +`verification/proofs/`. It contains NO compiler/application code and NO +single-project proofs — those belong in the owning repo. -- ABI definitions: **Idris2** with dependent types (`src/interface/Abi/`). -- FFI implementation: **Zig** with C ABI compatibility (`ffi/zig/`). -- Generated C headers: `generated/abi/`. +Routing is defined in `.machine_readable/bot_directives/placement.a2ml` +(authoritative) and enforced by `scripts/check-coordination-boundary.sh`. +ABI/FFI and memory-layout proofs in particular belong in `typed-wasm`, not here. ## Build System diff --git a/scripts/check-coordination-boundary.sh b/scripts/check-coordination-boundary.sh new file mode 100755 index 0000000..46e16f7 --- /dev/null +++ b/scripts/check-coordination-boundary.sh @@ -0,0 +1,84 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# Coordination-boundary guard. +# +# nextgen-typing is a coordination repo: docs + machine-readable state + +# estate scaffold + CROSS-project proofs only. It must never accumulate +# compiler/application code or single-project proofs. This check fails the +# build when project code or a non-allowlisted proof appears, and points the +# author at the routing table. +# +# Routing table (authoritative): .machine_readable/bot_directives/placement.a2ml +# Human-readable: AGENTS.md / CLAUDE.md + +set -euo pipefail + +ROUTE=".machine_readable/bot_directives/placement.a2ml" +fail=0 +err() { printf '❌ %s\n' "$1"; fail=1; } + +# --- 1. No code-project scaffolding at the repo root ------------------------ +for marker in src crates Cargo.toml Cargo.lock go.mod mix.exs; do + if [ -e "$marker" ]; then + err "Found '$marker'. nextgen-typing is a coordination repo and must not carry a code scaffold. Route the code to its owning repo (see $ROUTE)." + fi +done + +# --- 2. Only cross-project proofs may live under verification/proofs/ ------- +# Allowlist = proofs that span >=2 constituent repos. Keep it small and +# deliberate; it must match [verification].allowed-proofs in placement.a2ml. +ALLOWED_PROOFS=( + "verification/proofs/agda/EchoTyping.agda" + "verification/proofs/agda/Verification.agda" + "verification/proofs/agda/nextgen-typing.agda-lib" +) +is_allowed_proof() { + local f="$1" a + for a in "${ALLOWED_PROOFS[@]}"; do + [ "$f" = "$a" ] && return 0 + done + return 1 +} + +if [ -d verification/proofs ]; then + while IFS= read -r f; do + case "$f" in + *.a2ml | *.adoc | *.md | *.gitkeep) continue ;; # docs/metadata are fine + esac + if ! is_allowed_proof "$f"; then + err "Proof outside the cross-project allowlist: $f + Single-project proofs belong in the owning repo (kategoria / typell / + typed-wasm / echo-types / ...). Only proofs that import or relate >=2 + constituent repos belong here. If this genuinely spans the pipeline, add + it to ALLOWED_PROOFS here AND to [verification].allowed-proofs in $ROUTE." + fi + done < <(find verification/proofs -type f | sed 's|^\./||' | sort) +fi + +# --- 3. No implementation/proof source languages outside verification/proofs/ +# The coordination repo holds docs, .a2ml, k9/ncl, shell, and CI — not Rust, +# Zig, Idris, Agda, Lean, Coq, Isabelle, Haskell, or OCaml source. +while IFS= read -r f; do + err "Implementation source outside the coordination boundary: $f + Compiler / kernel / proof code belongs in the owning project repo (see $ROUTE)." +done < <( + find . \ + -path ./.git -prune -o \ + -path ./verification/proofs -prune -o \ + -type f \( \ + -name '*.rs' -o -name '*.zig' -o -name '*.idr' -o -name '*.lean' \ + -o -name '*.v' -o -name '*.agda' -o -name '*.thy' -o -name '*.hs' \ + -o -name '*.ml' \ + \) -print | sed 's|^\./||' | sort +) + +if [ "$fail" -ne 0 ]; then + printf '\nCoordination-boundary check FAILED.\n' + printf 'nextgen-typing coordinates the typing pipeline; it does not host project code.\n' + printf 'See %s for where this content belongs.\n' "$ROUTE" + exit 1 +fi + +printf '✅ Coordination boundary intact: docs + cross-project proofs only.\n' diff --git a/verification/proofs/README.adoc b/verification/proofs/README.adoc index 520f5e9..eccbe38 100644 --- a/verification/proofs/README.adoc +++ b/verification/proofs/README.adoc @@ -1,60 +1,64 @@ // SPDX-License-Identifier: MPL-2.0 // Copyright (c) Jonathan D.A. Jewell -= Formal Verification Proofs += Cross-Project Formal Proofs -This directory contains formal proofs organised by proof assistant. +This directory hosts *cross-project* formal proofs only — proofs that import +or relate **two or more** constituent repos of the type-theory pipeline. -== Directory Structure +[IMPORTANT] +==== +`nextgen-typing` is a coordination repo. *Single-project* proofs do **not** +belong here — they belong in the repo that owns the subject matter: + +* TypeLL kernel proofs (dependent/linear/session types, QTT) → `typell` +* WasmGC memory-safety / ABI / FFI / memory-layout proofs → `typed-wasm` +* The echo-types library's own proofs (Echo/EchoLinear/EchoResidue) → `echo-types` +* Research prototype proofs → `kategoria` + +The authoritative routing table is +`.machine_readable/bot_directives/placement.a2ml`, and CI enforces this +boundary via `.github/workflows/coordination-boundary.yml` +(`scripts/check-coordination-boundary.sh`). +==== + +== Current contents [source] ---- proofs/ -├── idris2/ # Idris2 proofs (ABI, dependent types) -│ ├── ABI/ # ABI-specific proofs (mandatory) -│ │ ├── Pointers.idr # Non-null pointer safety -│ │ ├── Layout.idr # Memory layout correctness -│ │ ├── Platform.idr # Platform type size proofs -│ │ ├── Foreign.idr # FFI return type proofs -│ │ └── Compliance.idr # C ABI compliance -│ └── Types.idr # Core data type well-formedness -├── lean4/ # Lean4 proofs (algebra, lattices) -│ └── ApiTypes.lean -├── agda/ # Agda proofs (induction, metatheory) -│ └── Properties.agda -├── coq/ # Coq proofs (type systems, compilation) -│ └── TypeSafety.v -└── tlaplus/ # TLA+ specs (distributed protocols) - └── StateMachine.tla +└── agda/ + ├── EchoTyping.agda # echo-types <-> AffineScript/typed-wasm pipeline + ├── Verification.agda # aggregator: `agda Verification.agda` checks the set + └── nextgen-typing.agda-lib # depends on: standard-library, echo-types ---- -== Verification Commands +`EchoTyping.agda` is the worked example of a qualifying proof: it depends on the +`hyperpolymath/echo-types` Agda library and proves that the pipeline's +information-losing typing operations (AffineScript affine weakening; refinement +erasure into the typed-wasm/kernel layer) are instances of echo-types' fiber +construction. It genuinely spans `echo-types`, `affinescript`, and `typed-wasm`, +so it is coordination material rather than any one project's. -[source,bash] ----- -just proof-check-all # Run all proof checkers -just proof-check-idris2 # Idris2 only -just proof-check-lean4 # Lean4 only -just proof-check-agda # Agda only -just proof-check-coq # Coq only ----- +== Adding a proof here -== Banned Patterns +Before adding anything, check the gate: -The following MUST NOT appear in any proof file: +. *Does it import or relate two or more constituent repos?* If not, it is a + single-project proof — put it in the owning repo (see `placement.a2ml`). +. If it qualifies, add the file under the appropriate prover subdirectory, then + register it in **both**: + * `[verification].allowed-proofs` in `.machine_readable/bot_directives/placement.a2ml`, and + * `ALLOWED_PROOFS` in `scripts/check-coordination-boundary.sh`. +. Ensure `--safe` / `%default total` / no escape hatches (see Banned Patterns). -- `believe_me` (Idris2) -- `assert_total` (Idris2) -- `postulate` (Idris2/Agda) -- `sorry` (Lean4) -- `Admitted` (Coq) -- `unsafeCoerce` (Haskell) +== Banned patterns -CI enforces this via `panic-attack assail --proofs-only`. +The following MUST NOT appear in any proof file: -== Adding New Proofs +* `believe_me`, `assert_total` (Idris2) +* `postulate` (Idris2/Agda) +* `sorry` (Lean4) +* `Admitted` (Coq) +* `unsafeCoerce` (Haskell) -1. Choose the appropriate prover (see PROOF-NEEDS.md) -2. Create the `.idr`/`.lean`/`.agda`/`.v`/`.tla` file in the right directory -3. Ensure `%default total` (Idris2) or equivalent -4. Run the verification command -5. Update PROOF-STATUS.md +CI enforces this via `panic-attack assail --proofs-only`. diff --git a/verification/proofs/agda/Properties.agda b/verification/proofs/agda/Properties.agda deleted file mode 100644 index 2afbdd1..0000000 --- a/verification/proofs/agda/Properties.agda +++ /dev/null @@ -1,38 +0,0 @@ -{-# OPTIONS --safe --without-K #-} --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) --- --- Agda Proof Template: Inductive and coinductive properties --- Replace with your project's domain-specific proofs. --- All proofs must be total (no postulate, no {-# TERMINATING #-}). - -module Properties where - -open import Data.Nat using (ℕ; zero; suc; _+_; _≤_; z≤n; s≤s; _<_) -open import Data.Nat.Properties using (+-comm; +-assoc; ≤-refl; ≤-trans) -open import Data.List using (List; []; _∷_; length; _++_) -open import Data.List.Properties using (length-++ ) -open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym; trans) - --- Example: Proof that list append preserves total length --- Replace with your project's domain proofs. - -append-length : ∀ {A : Set} (xs ys : List A) → - length (xs ++ ys) ≡ length xs + length ys -append-length xs ys = length-++ xs - --- Example: Monotonicity proof template --- Use for state machines, confidence scores, trust levels -record Monotone {A : Set} (_≤A_ : A → A → Set) (f : A → A) : Set where - field - preserves : ∀ {x y} → x ≤A y → f x ≤A f y - --- Example: Idempotence proof template --- Use for normalisation, deduplication, formatting -record Idempotent {A : Set} (_≡A_ : A → A → Set) (f : A → A) : Set where - field - idem : ∀ (x : A) → f (f x) ≡A f x - --- Example: Natural number successor is monotone -suc-monotone : Monotone _≤_ suc -suc-monotone = record { preserves = s≤s } diff --git a/verification/proofs/agda/Verification.agda b/verification/proofs/agda/Verification.agda index ed2f432..0c2d837 100644 --- a/verification/proofs/agda/Verification.agda +++ b/verification/proofs/agda/Verification.agda @@ -12,5 +12,4 @@ module Verification where -open import Properties open import EchoTyping diff --git a/verification/proofs/coq/TypeSafety.v b/verification/proofs/coq/TypeSafety.v deleted file mode 100644 index 8f5b418..0000000 --- a/verification/proofs/coq/TypeSafety.v +++ /dev/null @@ -1,73 +0,0 @@ -(* SPDX-License-Identifier: MPL-2.0 *) -(* Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) *) -(* - Coq Proof Template: Type system soundness - Replace with your project's type system proofs. - All proofs must be complete — NO Admitted allowed. -*) - -Require Import Coq.Lists.List. -Require Import Coq.Arith.Arith. -Require Import Coq.Bool.Bool. -Import ListNotations. - -(** * Example: Simple expression language with type safety *) -(** Replace this entire section with your project's type system. *) - -(** Types *) -Inductive ty : Type := - | TyNat : ty - | TyBool : ty. - -(** Expressions *) -Inductive expr : Type := - | EConst : nat -> expr - | ETrue : expr - | EFalse : expr - | EPlus : expr -> expr -> expr - | EEq : expr -> expr -> expr. - -(** Values *) -Inductive value : Type := - | VNat : nat -> value - | VBool : bool -> value. - -(** Typing relation *) -Inductive has_type : expr -> ty -> Prop := - | T_Const : forall n, has_type (EConst n) TyNat - | T_True : has_type ETrue TyBool - | T_False : has_type EFalse TyBool - | T_Plus : forall e1 e2, - has_type e1 TyNat -> has_type e2 TyNat -> - has_type (EPlus e1 e2) TyNat - | T_Eq : forall e1 e2, - has_type e1 TyNat -> has_type e2 TyNat -> - has_type (EEq e1 e2) TyBool. - -(** Evaluation *) -Inductive eval : expr -> value -> Prop := - | E_Const : forall n, eval (EConst n) (VNat n) - | E_True : eval ETrue (VBool true) - | E_False : eval EFalse (VBool false) - | E_Plus : forall e1 e2 n1 n2, - eval e1 (VNat n1) -> eval e2 (VNat n2) -> - eval (EPlus e1 e2) (VNat (n1 + n2)) - | E_Eq : forall e1 e2 n1 n2, - eval e1 (VNat n1) -> eval e2 (VNat n2) -> - eval (EEq e1 e2) (VBool (Nat.eqb n1 n2)). - -(** Value typing *) -Definition value_has_type (v : value) (t : ty) : Prop := - match v, t with - | VNat _, TyNat => True - | VBool _, TyBool => True - | _, _ => False - end. - -(** Type soundness: well-typed expressions evaluate to well-typed values *) -Theorem type_soundness : forall e t v, - has_type e t -> eval e v -> value_has_type v t. -Proof. - intros e t v Htype Heval. - induction Htype; inversion Heval; subst; simpl; auto. -Qed. diff --git a/verification/proofs/idris2/ABI/Compliance.idr b/verification/proofs/idris2/ABI/Compliance.idr deleted file mode 100644 index b94a5db..0000000 --- a/verification/proofs/idris2/ABI/Compliance.idr +++ /dev/null @@ -1,41 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) Jonathan D.A. Jewell --- --- ABI Proof: C ABI compliance --- Proves that struct layouts are C ABI compliant. --- All proofs MUST be constructive (no believe_me, no assert_total). - -module ABI.Compliance - -import ABI.Layout -import ABI.Platform - -%default total - -||| Evidence that every field in a layout is correctly aligned. -public export -data AllFieldsAligned : List StructField -> Type where - AFANil : AllFieldsAligned [] - AFACons : FieldAligned f -> AllFieldsAligned fs -> AllFieldsAligned (f :: fs) - -||| Evidence that every field is within the struct bounds. -public export -data AllFieldsInBounds : (size : Nat) -> List StructField -> Type where - AFBNil : AllFieldsInBounds size [] - AFBCons : FieldInBounds size f -> AllFieldsInBounds size fs -> AllFieldsInBounds size (f :: fs) - -||| A struct layout is C ABI compliant when: -||| 1. All fields are aligned to their natural alignment -||| 2. All fields are within bounds of the struct size -||| 3. The struct size is a multiple of the struct alignment -public export -record CABICompliant (layout : StructLayout) where - constructor MkCompliant - fieldsAligned : AllFieldsAligned (layoutFields layout) - fieldsInBounds : AllFieldsInBounds (layoutSize layout) (layoutFields layout) - sizeAligned : modNatNZ (layoutSize layout) (layoutAlignment layout) SIsNonZero = 0 - -||| An empty struct is trivially compliant (size=1, alignment=1). -export -emptyStructCompliant : CABICompliant (MkLayout "empty" [] 1 1) -emptyStructCompliant = MkCompliant AFANil AFBNil Refl diff --git a/verification/proofs/idris2/ABI/Foreign.idr b/verification/proofs/idris2/ABI/Foreign.idr deleted file mode 100644 index 1e550dd..0000000 --- a/verification/proofs/idris2/ABI/Foreign.idr +++ /dev/null @@ -1,53 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) Jonathan D.A. Jewell --- --- ABI Proof: FFI function return type proofs --- Proves that all FFI functions return expected types. --- All proofs MUST be constructive (no believe_me, no assert_total). - -module ABI.Foreign - -%default total - -||| Result type for FFI operations. -||| All FFI functions must return through this type. -public export -data FFIResult : Type -> Type where - FFISuccess : (value : a) -> FFIResult a - FFIError : (code : Int) -> (msg : String) -> FFIResult a - -||| Proof that FFIResult is a functor (map preserves structure). -export -mapFFIResult : (a -> b) -> FFIResult a -> FFIResult b -mapFFIResult f (FFISuccess value) = FFISuccess (f value) -mapFFIResult f (FFIError code msg) = FFIError code msg - -||| Proof that mapping identity preserves the result. -export -mapIdPreserves : (r : FFIResult a) -> mapFFIResult Prelude.id r = r -mapIdPreserves (FFISuccess value) = Refl -mapIdPreserves (FFIError code msg) = Refl - -||| An FFI function specification: name, argument types, return type. -public export -record FFISpec where - constructor MkFFISpec - ffiName : String - ffiReturnType : Type - -||| Proof that an FFI spec has a specific return type. -||| Use this to verify at compile time that FFI functions return the -||| types we expect across the C ABI boundary. -public export -FFIReturns : FFISpec -> Type -> Type -FFIReturns spec ty = ffiReturnType spec = ty - -||| C calling convention marker. -||| Proofs about calling convention compatibility. -public export -data CallingConv = CDecl | StdCall | FastCall - -||| All hyperpolymath FFI uses CDecl. -public export -defaultCallingConv : CallingConv -defaultCallingConv = CDecl diff --git a/verification/proofs/idris2/ABI/Layout.idr b/verification/proofs/idris2/ABI/Layout.idr deleted file mode 100644 index 9040a5e..0000000 --- a/verification/proofs/idris2/ABI/Layout.idr +++ /dev/null @@ -1,63 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) Jonathan D.A. Jewell --- --- ABI Proof: Memory layout correctness --- Proves struct size, alignment, and padding properties. --- All proofs MUST be constructive (no believe_me, no assert_total). - -module ABI.Layout - -%default total - -||| Witness that a type has a known size in bytes at compile time. -public export -interface HasSize (ty : Type) where - sizeOf : Nat - -||| Witness that a type has a known alignment in bytes. -public export -interface HasAlignment (ty : Type) where - alignOf : Nat - -||| Calculate padding needed to reach the next aligned offset. -||| paddingFor offset alignment = bytes to add so (offset + padding) `mod` alignment == 0 -public export -paddingFor : (offset : Nat) -> (alignment : Nat) -> {auto 0 ok : NonZero alignment} -> Nat -paddingFor offset alignment = let r = modNatNZ offset alignment ok - in case r of - Z => Z - (S _) => minus alignment r - -||| Proof that an offset with zero remainder needs zero padding. -export -alignedNeedsPadding : (n : Nat) -> (a : Nat) -> {auto 0 ok : NonZero a} -> - modNatNZ n a ok = 0 -> paddingFor n a = 0 -alignedNeedsPadding n a prf = rewrite prf in Refl - -||| A field within a struct, carrying its offset and size. -public export -record StructField where - constructor MkField - fieldName : String - fieldOffset : Nat - fieldSize : Nat - fieldAlignment : Nat - -||| Proof that a field is correctly aligned within a struct. -public export -FieldAligned : StructField -> Type -FieldAligned f = modNatNZ (fieldOffset f) (fieldAlignment f) SIsNonZero = 0 - -||| Proof that a field does not overflow past a given struct size. -public export -FieldInBounds : (structSize : Nat) -> StructField -> Type -FieldInBounds sz f = LTE (fieldOffset f + fieldSize f) sz - -||| A struct layout is a list of fields with a total size. -public export -record StructLayout where - constructor MkLayout - layoutName : String - layoutFields : List StructField - layoutSize : Nat - layoutAlignment : Nat diff --git a/verification/proofs/idris2/ABI/Platform.idr b/verification/proofs/idris2/ABI/Platform.idr deleted file mode 100644 index a8d6b94..0000000 --- a/verification/proofs/idris2/ABI/Platform.idr +++ /dev/null @@ -1,63 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) Jonathan D.A. Jewell --- --- ABI Proof: Platform-specific type size proofs --- Proves that C type sizes are correct per platform. --- All proofs MUST be constructive (no believe_me, no assert_total). - -module ABI.Platform - -%default total - -||| Supported target platforms for ABI verification. -public export -data Platform = Linux64 | LinuxARM64 | MacOS64 | MacOSARM64 - | Windows64 | FreeBSD64 | WASM32 - -||| Pointer size in bytes for each platform. -public export -ptrSize : Platform -> Nat -ptrSize WASM32 = 4 -ptrSize _ = 8 - -||| C `int` size in bytes. -public export -cIntSize : Platform -> Nat -cIntSize _ = 4 - -||| C `size_t` size in bytes (matches pointer size). -public export -cSizeT : Platform -> Nat -cSizeT = ptrSize - -||| Proof that size_t always equals pointer size on all platforms. -export -sizeTEqPtrSize : (p : Platform) -> cSizeT p = ptrSize p -sizeTEqPtrSize _ = Refl - -||| Proof that pointer size is always 4 or 8 bytes. -export -ptrSizeValid : (p : Platform) -> Either (ptrSize p = 4) (ptrSize p = 8) -ptrSizeValid WASM32 = Left Refl -ptrSizeValid Linux64 = Right Refl -ptrSizeValid LinuxARM64 = Right Refl -ptrSizeValid MacOS64 = Right Refl -ptrSizeValid MacOSARM64 = Right Refl -ptrSizeValid Windows64 = Right Refl -ptrSizeValid FreeBSD64 = Right Refl - -||| Proof that C int is always 4 bytes on all platforms. -export -cIntAlways4 : (p : Platform) -> cIntSize p = 4 -cIntAlways4 _ = Refl - -||| Proof that pointer size is always at least 4 bytes. -export -ptrSizeAtLeast4 : (p : Platform) -> LTE 4 (ptrSize p) -ptrSizeAtLeast4 WASM32 = lteRefl -ptrSizeAtLeast4 Linux64 = lteSuccRight (lteSuccRight (lteSuccRight (lteSuccRight lteRefl))) -ptrSizeAtLeast4 LinuxARM64 = lteSuccRight (lteSuccRight (lteSuccRight (lteSuccRight lteRefl))) -ptrSizeAtLeast4 MacOS64 = lteSuccRight (lteSuccRight (lteSuccRight (lteSuccRight lteRefl))) -ptrSizeAtLeast4 MacOSARM64 = lteSuccRight (lteSuccRight (lteSuccRight (lteSuccRight lteRefl))) -ptrSizeAtLeast4 Windows64 = lteSuccRight (lteSuccRight (lteSuccRight (lteSuccRight lteRefl))) -ptrSizeAtLeast4 FreeBSD64 = lteSuccRight (lteSuccRight (lteSuccRight (lteSuccRight lteRefl))) diff --git a/verification/proofs/idris2/ABI/Pointers.idr b/verification/proofs/idris2/ABI/Pointers.idr deleted file mode 100644 index 31b6c5f..0000000 --- a/verification/proofs/idris2/ABI/Pointers.idr +++ /dev/null @@ -1,52 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) Jonathan D.A. Jewell --- --- ABI Proof: Non-null pointer safety --- Template proof — customise for your project's pointer types. --- All proofs MUST be constructive (no believe_me, no assert_total). - -module ABI.Pointers - -import Data.So - -%default total - -||| A pointer value that has been proven non-null. -||| The `So` constraint carries a compile-time witness that `ptr /= 0`. -public export -record SafePtr where - constructor MkSafePtr - ptr : Bits64 - {auto 0 nonNull : So (ptr /= 0)} - -||| Proof that SafePtr can never hold a null (zero) value. -||| This is enforced by the `So` constraint in the record. -export -safePtrNeverNull : (sp : SafePtr) -> So (sp.ptr /= 0) -safePtrNeverNull sp = sp.nonNull - -||| Wrap a raw pointer with a runtime null check. -||| Returns Nothing if the pointer is null. -export -checkPtr : (raw : Bits64) -> Maybe SafePtr -checkPtr 0 = Nothing -checkPtr raw = case choose (raw /= 0) of - Left prf => Just (MkSafePtr raw) - Right _ => Nothing - -||| Proof that checkPtr 0 always returns Nothing. -export -checkPtrZeroIsNothing : checkPtr 0 = Nothing -checkPtrZeroIsNothing = Refl - -||| An opaque handle backed by a non-null pointer. -||| Use this for FFI resource handles (file descriptors, sockets, etc.). -public export -record Handle (tag : String) where - constructor MkHandle - safePtr : SafePtr - -||| Proof that two handles with equal pointers are equal. -export -handlePtrEq : (h1, h2 : Handle tag) -> h1.safePtr.ptr = h2.safePtr.ptr -> h1 = h2 -handlePtrEq (MkHandle (MkSafePtr p)) (MkHandle (MkSafePtr p)) Refl = Refl diff --git a/verification/proofs/idris2/Types.idr b/verification/proofs/idris2/Types.idr deleted file mode 100644 index cc7cce8..0000000 --- a/verification/proofs/idris2/Types.idr +++ /dev/null @@ -1,38 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) Jonathan D.A. Jewell --- --- Typing Proof: Core data type well-formedness --- Template — replace with your project's core types. --- All proofs MUST be constructive (no believe_me, no assert_total). - -module Types - -%default total - -||| Example: A bounded natural number (0 to max). -||| Replace with your project's core types. -public export -record Bounded (max : Nat) where - constructor MkBounded - value : Nat - {auto 0 inBounds : LTE value max} - -||| Proof that a Bounded value is always <= max. -export -boundedLeMax : (b : Bounded max) -> LTE b.value max -boundedLeMax b = b.inBounds - -||| Proof that zero is always a valid Bounded value. -export -zeroIsBounded : {max : Nat} -> Bounded (S max) -zeroIsBounded = MkBounded 0 - -||| Example: A non-empty list with a compile-time guarantee. -public export -data NonEmpty : List a -> Type where - IsNonEmpty : NonEmpty (x :: xs) - -||| Proof that cons always produces a non-empty list. -export -consIsNonEmpty : (x : a) -> (xs : List a) -> NonEmpty (x :: xs) -consIsNonEmpty _ _ = IsNonEmpty diff --git a/verification/proofs/lean4/ApiTypes.lean b/verification/proofs/lean4/ApiTypes.lean deleted file mode 100644 index 9ed78b7..0000000 --- a/verification/proofs/lean4/ApiTypes.lean +++ /dev/null @@ -1,44 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) --- --- Typing Proof: Public API type safety --- Template — replace with your project's API types. --- Proves properties about exported function signatures. - --- Example: Result type used across API boundaries -inductive ApiResult (α : Type) where - | ok : α → ApiResult α - | error : Nat → String → ApiResult α - -namespace ApiResult - -- Proof: map preserves structure (functor law: map id = id) - def map (f : α → β) : ApiResult α → ApiResult β - | .ok v => .ok (f v) - | .error c m => .error c m - - theorem map_id : ∀ (r : ApiResult α), map id r = r := by - intro r - cases r with - | ok v => simp [map] - | error c m => simp [map] - - -- Proof: map composition (functor law: map (g ∘ f) = map g ∘ map f) - theorem map_comp (f : α → β) (g : β → γ) : - ∀ (r : ApiResult α), map (g ∘ f) r = map g (map f r) := by - intro r - cases r with - | ok v => simp [map, Function.comp] - | error c m => simp [map] - --- Example: Bounded confidence value (0.0 to 1.0 modelled as Nat/1000) --- Replace with your project's numeric invariants -structure BoundedNat (max : Nat) where - val : Nat - le_max : val ≤ max - -theorem bounded_nat_le (b : BoundedNat max) : b.val ≤ max := - b.le_max - --- Proof: zero is always bounded -def zeroBounded (h : 0 < max) : BoundedNat max := - ⟨0, Nat.zero_le max⟩ diff --git a/verification/proofs/tlaplus/StateMachine.tla b/verification/proofs/tlaplus/StateMachine.tla deleted file mode 100644 index f348494..0000000 --- a/verification/proofs/tlaplus/StateMachine.tla +++ /dev/null @@ -1,91 +0,0 @@ ---------------------------- MODULE StateMachine ---------------------------- -(* SPDX-License-Identifier: MPL-2.0 *) -(* Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) *) -(* *) -(* TLA+ Specification Template: State Machine *) -(* Replace with your project's distributed protocol or state machine. *) -(* Use TLC model checker to verify properties. *) -(* *) -(* Example: A simple request pipeline with safety properties. *) -(* Replace States, Init, Next with your project's actual states. *) -(***************************************************************************) - -EXTENDS Naturals, Sequences, FiniteSets - -CONSTANTS - MaxRequests \* Upper bound on concurrent requests (for model checking) - -VARIABLES - state, \* Current pipeline state - processed, \* Number of processed requests - queue \* Request queue - -vars == <> - -\* Pipeline states — replace with your project's states -States == {"idle", "scanning", "routing", "dispatching", "done", "failed"} - -\* Valid transitions — replace with your project's transition rules -ValidTransition(from, to) == - \/ from = "idle" /\ to = "scanning" - \/ from = "scanning" /\ to = "routing" - \/ from = "scanning" /\ to = "failed" - \/ from = "routing" /\ to = "dispatching" - \/ from = "routing" /\ to = "failed" - \/ from = "dispatching" /\ to = "done" - \/ from = "dispatching" /\ to = "failed" - \/ from = "done" /\ to = "idle" - \/ from = "failed" /\ to = "idle" - -\* Initial state -Init == - /\ state = "idle" - /\ processed = 0 - /\ queue = <<>> - -\* Transition action -Transition(newState) == - /\ ValidTransition(state, newState) - /\ state' = newState - /\ IF newState = "done" - THEN processed' = processed + 1 - ELSE processed' = processed - /\ UNCHANGED queue - -\* Enqueue a request (only when idle or scanning) -Enqueue == - /\ state \in {"idle", "scanning"} - /\ Len(queue) < MaxRequests - /\ queue' = Append(queue, "request") - /\ UNCHANGED <> - -\* Next-state relation -Next == - \/ \E s \in States : Transition(s) - \/ Enqueue - -\* Fairness: the system must eventually process -Spec == Init /\ [][Next]_vars /\ WF_vars(Next) - -\* ---- SAFETY PROPERTIES ---- - -\* State is always valid -TypeInvariant == state \in States - -\* Processed count never decreases (monotonicity) -ProcessedMonotonic == processed >= 0 - -\* Queue never exceeds max -QueueBounded == Len(queue) <= MaxRequests - -\* No impossible transitions (e.g., idle -> done) -NoSkipStates == - [][state' # state => - ValidTransition(state, state')]_state - -\* ---- LIVENESS PROPERTIES ---- - -\* Every request eventually completes or fails -EventualCompletion == <>(state = "done" \/ state = "failed") - -============================================================================