diff --git a/AGENTS.adoc b/AGENTS.adoc new file mode 100644 index 0000000..5ed2c5c --- /dev/null +++ b/AGENTS.adoc @@ -0,0 +1,100 @@ +== 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 + +[width="100%",cols="50%,50%",options="header",] +|=== +|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 + +[arabic] +. Read `+0-AI-MANIFEST.a2ml+`, then +`+.machine_readable/6a2/STATE.a2ml+`. +. Full rules: `+docs/practice/AI-CONVENTIONS.adoc+`. +. Licence *MPL-2.0* + SPDX header on every file (never AGPL). +. Banned languages: TypeScript→ReScript, npm/Node→Deno, Go→Rust, +Python→Julia/Rust. Containers: Podman + `+Containerfile+`. Build/test +via `+just+`. +. No unsound escape hatches in any proof: `+believe_me+`, +`+assert_total+`, `+postulate+`, `+sorry+`, `+Admitted+`, +`+unsafeCoerce+`, `+Obj.magic+`. +. Author: Jonathan D.A. Jewell (hyperpolymath) j.d.a.jewell@open.ac.uk. diff --git a/AGENTS.md b/AGENTS.md deleted file mode 100644 index 95db5f5..0000000 --- a/AGENTS.md +++ /dev/null @@ -1,72 +0,0 @@ - - - -# 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/CHANGELOG.adoc b/CHANGELOG.adoc new file mode 100644 index 0000000..ca1c652 --- /dev/null +++ b/CHANGELOG.adoc @@ -0,0 +1,9 @@ +== Changelog + +All notable changes to this project will be documented in this file. + +The format is based on https://keepachangelog.com/en/1.1.0/[Keep a +Changelog], and this project adheres to +https://semver.org/spec/v2.0.0.html[Semantic Versioning]. + +=== [Unreleased] diff --git a/CHANGELOG.md b/CHANGELOG.md deleted file mode 100644 index ec7f2e1..0000000 --- a/CHANGELOG.md +++ /dev/null @@ -1,15 +0,0 @@ - -# Changelog - -All notable changes to this project will be documented in this file. - -The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/), -and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html). - - - - -## [Unreleased] diff --git a/CODE_OF_CONDUCT.adoc b/CODE_OF_CONDUCT.adoc new file mode 100644 index 0000000..bd2a83c --- /dev/null +++ b/CODE_OF_CONDUCT.adoc @@ -0,0 +1,24 @@ +== Contributor Covenant Code of Conduct + +=== Our Pledge + +We pledge to make participation a harassment-free experience for +everyone. + +=== Our Standards + +*Positive behavior:* * Using welcoming language * Being respectful of +differing viewpoints * Accepting constructive criticism * Focusing on +what is best for the community + +*Unacceptable behavior:* * Harassment, trolling, or personal attacks * +Publishing private information without permission + +=== Enforcement + +Report issues to the maintainers. All complaints will be reviewed. + +=== Attribution + +Adapted from https://www.contributor-covenant.org/[Contributor Covenant] +v2.1. diff --git a/CODE_OF_CONDUCT.md b/CODE_OF_CONDUCT.md deleted file mode 100644 index bbe9219..0000000 --- a/CODE_OF_CONDUCT.md +++ /dev/null @@ -1,30 +0,0 @@ - -# Contributor Covenant Code of Conduct - -## Our Pledge - -We pledge to make participation a harassment-free experience for everyone. - -## Our Standards - -**Positive behavior:** -* Using welcoming language -* Being respectful of differing viewpoints -* Accepting constructive criticism -* Focusing on what is best for the community - -**Unacceptable behavior:** -* Harassment, trolling, or personal attacks -* Publishing private information without permission - -## Enforcement - -Report issues to the maintainers. All complaints will be reviewed. - -## Attribution - -Adapted from [Contributor Covenant](https://www.contributor-covenant.org/) v2.1. - diff --git a/CONTRIBUTING.adoc b/CONTRIBUTING.adoc new file mode 100644 index 0000000..5949bf0 --- /dev/null +++ b/CONTRIBUTING.adoc @@ -0,0 +1,9 @@ +== Contributing + +[arabic] +. Fork the repository +. Create a feature branch +. Ensure SPDX headers on all files +. Submit a pull request + +*Author:* Jonathan D.A. Jewell j.d.a.jewell@open.ac.uk diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md deleted file mode 100644 index b7e3340..0000000 --- a/CONTRIBUTING.md +++ /dev/null @@ -1,12 +0,0 @@ - -# Contributing - -1. Fork the repository -2. Create a feature branch -3. Ensure SPDX headers on all files -4. Submit a pull request - -**Author:** Jonathan D.A. Jewell diff --git a/GOVERNANCE.adoc b/GOVERNANCE.adoc index e640a17..9b836fb 100644 --- a/GOVERNANCE.adoc +++ b/GOVERNANCE.adoc @@ -1,162 +1,60 @@ -// SPDX-License-Identifier: CC-BY-SA-4.0 -// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell -= Governance Model -:toc: preamble +== Governance -This document describes the governance model for this repository. +=== Overview -== Overview +This project is governed by the following principles and structures to +ensure transparent, inclusive, and effective decision-making. -This repository follows a **Sole Maintainer Governance Model**: +=== Roles and Responsibilities -* Single maintainer (@hyperpolymath) has full authority over the project -* All contributions are welcome and reviewed by the maintainer -* Decisions are made transparently through GitHub issues and discussions -* The project adheres to the hyperpolymath estate policies where applicable +==== Maintainers -== Core Principles +Maintainers are responsible for: - Reviewing and merging pull requests - +Managing releases and versioning - Ensuring code quality and standards - +Triaging issues and bug reports - Community engagement and support -[cols="1,2"] -|=== -| Principle | Description +==== Contributors -| **Benevolent Dictatorship** | Maintainer has final decision authority but seeks community input +Contributors are expected to: - Follow the code of conduct - Submit +well-documented pull requests - Write tests for new functionality - +Maintain existing tests - Update documentation as needed -| **Meritocracy** | Contributions are judged on technical merit, not contributor identity +=== Decision Making -| **Transparency** | All significant decisions are documented publicly +==== Minor Changes -| **Consensus-Seeking** | Maintainer prefers consensus but will decide when necessary +* Can be made by any maintainer +* Include bug fixes, documentation updates, dependency updates -| **Open Contribution** | Anyone can contribute via fork and pull request +==== Major Changes -|=== +* Require discussion in issues or pull requests +* Include new features, architectural changes, API changes +* Need approval from at least 2 maintainers -== Roles and Permissions +==== Breaking Changes -[cols="1,2,2"] -|=== -| Role | Permissions | Assignment +* Require RFC (Request for Comments) process +* Need approval from majority of maintainers +* Must include migration guide -| **Maintainer** | Write access, merge rights, admin | @hyperpolymath -| **Contributors** | Read access, fork, submit PRs | All GitHub users -| **Users** | Use the software, report issues | All GitHub users +=== Code of Conduct -|=== +All participants are expected to follow our Code of Conduct. Violations +can be reported to the maintainers. -== Decision Making Framework +=== Communication -=== Routine Decisions +* *Issues*: For bug reports and feature requests +* *Discussions*: For questions and general discussion +* *Pull Requests*: For code contributions -* Bug fixes -* Documentation improvements -* Minor feature additions -* Dependency updates +=== Licensing -**Process**: Maintainer reviews and merges PRs that meet quality standards. +All contributions are made under the terms of the repository’s LICENSE +file. By submitting a pull request, you agree to license your +contributions accordingly. -=== Significant Changes +''''' -* New major features -* API changes -* Architecture modifications -* Breaking changes - -**Process**: -. Open issue describing the change -. Discuss with community (minimum 72 hours) -. Maintainer makes final decision -. Document rationale in issue/PR - -=== Structural Decisions - -* Repository purpose/renaming -* License changes -* Ownership transfer -* Deprecation/archival - -**Process**: -. Extended discussion (minimum 1 week) -. Maintainer makes final decision -. Document in CHANGELOG and governance docs - -== Contribution Lifecycle - -[cols="1,2"] -|=== -| Stage | Process - -| **Ideation** | Open issue, discuss feasibility - -| **Development** | Fork, implement, test thoroughly - -| **Review** | Submit PR, maintainer reviews within 7 days - -| **Merge** | Maintainer merges or requests changes - -| **Release** | Maintainer publishes according to project conventions - -|=== - -== Conflict Resolution - -In case of disagreements: - -. Discuss in the relevant GitHub issue or PR -. Provide technical justification for positions -. Maintainer mediates and makes final decision -. Decision is documented and can be revisited later - -== Project Policies - -This repository adheres to hyperpolymath estate-wide policies: - -* **License**: MPL-2.0 for code, CC-BY-SA-4.0 for prose (per standards/LICENCE-POLICY.adoc) -* **Code of Conduct**: Follows hyperpolymath CODE_OF_CONDUCT.md -* **Security**: Follows hyperpolymath SECURITY.md -* **Contributing**: Follows hyperpolymath CONTRIBUTING.adoc conventions - -== Repository-Specific Conventions - -[cols="1,2"] -|=== -| Convention | Description - -| **Signing** | All commits must be signed (SSH or GPG) - -| **SPDX Headers** | All source files must have SPDX license identifiers - -| **Contractiles** | Mustfile, Trustfile, Intendfile, Adjustfile in root - -| **Machine Readable** | META.a2ml in .machine_readable/6a2/ - -| **CI/CD** | GitHub Actions workflows in .github/workflows/ - -|=== - -== Governance Evolution - -As the project grows, this governance model may evolve: - -* **Adding Co-Maintainers**: When contribution volume warrants it -* **Forming a Team**: For complex multi-maintainer projects -* **Adopting TPCF**: For large, multi-repository projects (see rhodium-standard-repositories) - -Changes to this document require the same process as Significant Changes above. - -== See Also - -* link:MAINTAINERS.adoc[Maintainers] -* link:CODE_OF_CONDUCT.md[Code of Conduct] -* link:CONTRIBUTING.md[Contributing Guide] -* link:https://github.com/hyperpolymath/standards/blob/main/LICENCE-POLICY.adoc[Estate License Policy] -* link:https://github.com/hyperpolymath/standards[rhodium-standard-repositories (TPCF)] - -== Changelog - -[cols="1,1,1"] -|=== -| Date | Change | By - -| 2026-06-07 | Initial governance model established | @hyperpolymath -|=== +_Last updated: 2026-07-18_ diff --git a/GOVERNANCE.md b/GOVERNANCE.md deleted file mode 100644 index e27364c..0000000 --- a/GOVERNANCE.md +++ /dev/null @@ -1,60 +0,0 @@ -# Governance - -## Overview - -This project is governed by the following principles and structures to ensure transparent, inclusive, and effective decision-making. - -## Roles and Responsibilities - -### Maintainers - -Maintainers are responsible for: -- Reviewing and merging pull requests -- Managing releases and versioning -- Ensuring code quality and standards -- Triaging issues and bug reports -- Community engagement and support - -### Contributors - -Contributors are expected to: -- Follow the code of conduct -- Submit well-documented pull requests -- Write tests for new functionality -- Maintain existing tests -- Update documentation as needed - -## Decision Making - -### Minor Changes -- Can be made by any maintainer -- Include bug fixes, documentation updates, dependency updates - -### Major Changes -- Require discussion in issues or pull requests -- Include new features, architectural changes, API changes -- Need approval from at least 2 maintainers - -### Breaking Changes -- Require RFC (Request for Comments) process -- Need approval from majority of maintainers -- Must include migration guide - -## Code of Conduct - -All participants are expected to follow our Code of Conduct. Violations can be reported to the maintainers. - -## Communication - -- **Issues**: For bug reports and feature requests -- **Discussions**: For questions and general discussion -- **Pull Requests**: For code contributions - -## Licensing - -All contributions are made under the terms of the repository's LICENSE file. -By submitting a pull request, you agree to license your contributions accordingly. - ---- - -*Last updated: 2026-07-18* diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc new file mode 100644 index 0000000..c3cd384 --- /dev/null +++ b/PROOF-NEEDS.adoc @@ -0,0 +1,76 @@ +== Proof Requirements — nextgen-typing + +____ +*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+`. +____ + +=== Proof Tier + +*Tier*: T5 — Exempt (coordination layer; no owned code to prove). +Cross-project proofs are hosted, not mandated. + +=== Cross-Project Proofs (the only category that applies here) + +[width="99%",cols="11%,17%,17%,20%,20%,15%",options="header",] +|=== +|# |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+`. + +=== Where single-project proofs go (NOT here) + +[width="100%",cols="41%,59%",options="header",] +|=== +|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+` +|=== + +=== Dangerous Patterns (BANNED in any hosted proof) + +[cols=",,",options="header",] +|=== +|Pattern |Language |Meaning +|`+believe_me+` |Idris2 |Unsafe cast / trust-me +|`+assert_total+` |Idris2 |Skip totality check +|`+postulate+` |Idris2/Agda |Unproven axiom +|`+sorry+` |Lean4 |Incomplete proof +|`+Admitted+` |Coq |Incomplete proof +|`+unsafeCoerce+` |Haskell |Unsafe type cast +|`+Obj.magic+` |OCaml/ReScript |Unsafe type cast +|=== + +CI rejects any PR introducing these (`+panic-attack assail+`). + +=== References + +* 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) diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md deleted file mode 100644 index 9a52cdb..0000000 --- a/PROOF-NEEDS.md +++ /dev/null @@ -1,60 +0,0 @@ - -# Proof Requirements — nextgen-typing - -> **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`. - -## Proof Tier - -**Tier**: T5 — Exempt (coordination layer; no owned code to prove). -Cross-project proofs are hosted, not mandated. - -## Cross-Project Proofs (the only category that applies here) - -| # | 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`. - -## Where single-project proofs go (NOT here) - -| 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` | - -## Dangerous Patterns (BANNED in any hosted proof) - -| Pattern | Language | Meaning | -|---------|----------|---------| -| `believe_me` | Idris2 | Unsafe cast / trust-me | -| `assert_total` | Idris2 | Skip totality check | -| `postulate` | Idris2/Agda | Unproven axiom | -| `sorry` | Lean4 | Incomplete proof | -| `Admitted` | Coq | Incomplete proof | -| `unsafeCoerce` | Haskell | Unsafe type cast | -| `Obj.magic` | OCaml/ReScript | Unsafe type cast | - -CI rejects any PR introducing these (`panic-attack assail`). - -## References - -- 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) diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc new file mode 100644 index 0000000..4b5741a --- /dev/null +++ b/PROOF-STATUS.adoc @@ -0,0 +1,56 @@ +== Proof Status — nextgen-typing + +____ +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+`. +____ + +=== Summary + +[cols=",,,,",options="header",] +|=== +|Category |Total |Done |In Progress |Remaining +|Cross-project (XP) |1 |1 |0 |0 +|*Total* |*1* |*1* |*0* |*0* +|=== + +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 Present + +[width="100%",cols="12%,15%,15%,17%,13%,28%",options="header",] +|=== +|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 + +[source,bash] +---- +# 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 + +# Enforce the coordination boundary (no project code / non-allowlisted proofs) +bash scripts/check-coordination-boundary.sh +---- + +=== Changelog + +[width="100%",cols="32%,42%,26%",options="header",] +|=== +|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/PROOF-STATUS.md b/PROOF-STATUS.md deleted file mode 100644 index 7c54e5a..0000000 --- a/PROOF-STATUS.md +++ /dev/null @@ -1,45 +0,0 @@ - -# Proof Status — nextgen-typing - -> 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`. - -## Summary - -| Category | Total | Done | In Progress | Remaining | -|----------|-------|------|-------------|-----------| -| Cross-project (XP) | 1 | 1 | 0 | 0 | -| **Total** | **1** | **1** | **0** | **0** | - -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 Present - -| 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 - -```bash -# 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 - -# 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/READINESS.adoc b/READINESS.adoc new file mode 100644 index 0000000..06e8da0 --- /dev/null +++ b/READINESS.adoc @@ -0,0 +1,55 @@ +== nextgen-typing Component Readiness Assessment + +*Standard:* +https://github.com/hyperpolymath/standards/tree/main/component-readiness-grades[Component +Readiness Grades (CRG) v2.2] *Current Grade:* C *Assessed:* 2026-06-05 +*Assessor:* Jonathan D.A. Jewell + +''''' + +=== Summary + +[width="100%",cols="25%,8%,17%,50%",options="header",] +|=== +|Component |Grade |Release Stage |Evidence Summary +|Primary component |C |Alpha-stable |Dogfooded on own project; CI +passing +|=== + +*Overall:* Grade C — dogfooding confirmed, CI passing, deep annotation +in place. + +''''' + +=== Grade C Evidence + +* Deployed and dogfooded on the nextgen-typing project itself +* CI passing (dogfood-gate, hypatia-scan, static-analysis-gate) +* TEST-NEEDS.md documents test matrix +* No home failures +* Deep code and folder annotation in place per CRG v2 requirements + +''''' + +=== Promotion Path to Grade B + +Grade B requires: *6+ diverse external targets tested, issues fed back*. + +Diversity means: different languages, different architectures, different +use cases. + +To reach B: 1. Deploy on at least 6 external projects that differ +meaningfully from each other 2. Confirm it works in each (or document +failures) 3. Feed back any issues found (GitHub issues or PRs) 4. Update +this file with the evidence + +''''' + +=== Concerns and Maintenance Notes + +_Document any known limitations, demotion risks, or maintenance concerns +here._ + +''''' + +=== Run `+just crg-badge+` to generate the shields.io badge for your README. diff --git a/READINESS.md b/READINESS.md deleted file mode 100644 index 8baee91..0000000 --- a/READINESS.md +++ /dev/null @@ -1,56 +0,0 @@ - - - -# nextgen-typing Component Readiness Assessment - -**Standard:** [Component Readiness Grades (CRG) v2.2](https://github.com/hyperpolymath/standards/tree/main/component-readiness-grades) -**Current Grade:** C -**Assessed:** 2026-06-05 -**Assessor:** Jonathan D.A. Jewell - ---- - -## Summary - -| Component | Grade | Release Stage | Evidence Summary | -|---------------------|-------|---------------|-------------------------------------------| -| Primary component | C | Alpha-stable | Dogfooded on own project; CI passing | - -**Overall:** Grade C — dogfooding confirmed, CI passing, deep annotation in place. - ---- - -## Grade C Evidence - -- Deployed and dogfooded on the nextgen-typing project itself -- CI passing (dogfood-gate, hypatia-scan, static-analysis-gate) -- TEST-NEEDS.md documents test matrix -- No home failures -- Deep code and folder annotation in place per CRG v2 requirements - ---- - -## Promotion Path to Grade B - -Grade B requires: **6+ diverse external targets tested, issues fed back**. - -Diversity means: different languages, different architectures, different use cases. - -To reach B: -1. Deploy on at least 6 external projects that differ meaningfully from each other -2. Confirm it works in each (or document failures) -3. Feed back any issues found (GitHub issues or PRs) -4. Update this file with the evidence - ---- - -## Concerns and Maintenance Notes - -*Document any known limitations, demotion risks, or maintenance concerns here.* - ---- - -## Run `just crg-badge` to generate the shields.io badge for your README. diff --git a/REQUIRES_INITIALISATION.adoc b/REQUIRES_INITIALISATION.adoc new file mode 100644 index 0000000..a6e6b41 --- /dev/null +++ b/REQUIRES_INITIALISATION.adoc @@ -0,0 +1,261 @@ +== REQUIRES INITIALISATION + +*This repository is not finished being set up.* 22 substitution token(s) +across 19 file(s) still have no value. + +=== Why this is not already done + +This repo was created from `+hyperpolymath/rsr-template-repo+`. The mint +(`+just repo-init+`) fills every token that has a single mechanical +answer — owner, repo, author, dates, licence, branch — and it has done +so here. + +The tokens below are the ones it _deliberately cannot_ answer. They need +a decision or a fact that exists only in your head: what this project is +for, what command builds it, which port the service listens on, whether +a PGP key is held at all. The template’s own token vocabulary says as +much — you cannot sensibly answer "`required invariants`" in a +thirty-second bootstrap. + +They were left *visibly unfilled on purpose*. The alternatives were both +worse: inventing plausible values would put confident falsehoods into a +security policy and an architecture document, and silently deleting the +sections would hide the fact that a decision is owed. A visible gap is +honest; a fabricated answer is not. + +=== Do not delete this file until every item below is resolved + +This file is the only marker that the work is outstanding. Deleting it +early does not finish the setup, it just conceals it — and the next +person or agent to arrive will reasonably assume the repo is complete. + +* *If you are a person:* delete this file yourself once the last item is +done. +* *If you are an agent:* resolve what you legitimately can, leave the +rest, and delete this file only when no token below remains anywhere in +the tree. Do not delete it to make a gate go green. + +Re-running the estate top-up tool will remove this file automatically +once nothing is outstanding, so the safest way to finish is to fix the +tokens and let the check confirm it. + +=== Do these first + +`+.github/settings.yml+` is applied to the forge by a GitHub App. An +unfilled token here can be written into the repository’s real name or +description. This has fired before in this estate: illegal braces were +collapsed to dashes and a repo was renamed `+-REPO-+`, which then read +as deleted. + +* `+{{DESCRIPTION}}+` — One-line description used in +.github/settings.yml. HIGH PRIORITY: settings.yml is applied by a GitHub +App, so an unfilled token here can be written into forge metadata +verbatim. + +=== What is needed, and where it goes + +==== `+{{ARGS}}+` + +Arguments for the justfile recipe this appears in. + +Appears in: + +* `+.machine_readable/contractiles/Justfile+` +* `+Justfile+` + +==== `+{{AUTHOR_EMAIL_ALT}}+` + +Appears in: + +* `+.github/.mailmap+` + +==== `+{{AUTHOR_ORG}}+` + +Author’s organisation. NOTE: no filled instance of this exists anywhere +in the estate — consider deleting the field instead. + +Appears in: + +* `+.machine_readable/self-validating/examples/project-metadata.k9.ncl+` + +==== `+{{BUILD_CMD}}+` + +The exact command that builds this project. + +Appears in: + +* `+QUICKSTART-DEV.adoc+` + +==== `+{{BUILD_OUTPUT_PATH}}+` + +Where the build artefact lands. + +Appears in: + +* `+QUICKSTART-MAINTAINER.adoc+` + +==== `+{{DEPS}}+` + +Prose summary of runtime/build dependencies. + +Appears in: + +* `+QUICKSTART-MAINTAINER.adoc+` + +==== `+{{DESCRIPTION}}+` + +One-line description used in .github/settings.yml. HIGH PRIORITY: +settings.yml is applied by a GitHub App, so an unfilled token here can +be written into forge metadata verbatim. + +Appears in: + +* `+.github/settings.yml+` + +==== `+{{LANG_STACK}}+` + +The language stack, in prose. + +Appears in: + +* `+QUICKSTART-DEV.adoc+` + +==== `+{{LICENSE}}+` + +SPDX identifier for this repo’s licence. + +Appears in: + +* `+container/Containerfile+` +* `+container/manifest.toml+` + +==== `+{{MUST_INVARIANTS}}+` + +The invariants this project guarantees. Not answerable in a bootstrap; +it is the point of the repo. + +Appears in: + +* `+QUICKSTART-DEV.adoc+` + +==== `+{{ONE_PARAGRAPH_PURPOSE}}+` + +A paragraph on what this is for. + +Appears in: + +* `+.machine_readable/contractiles/Intentfile.a2ml+` + +==== `+{{OPENSSF_PROJECT_ID}}+` + +OpenSSF project ID, same registration. + +Appears in: + +* `+TEMPLATE-STANDARDS-AUDIT.adoc+` + +==== `+{{PGP_KEY_URL}}+` + +Public URL the PGP key can be fetched from. Same caveat as +PGP_FINGERPRINT. + +Appears in: + +* `+.well-known/security.txt+` + +==== `+{{PORT}}+` + +Port the container service listens on. + +Appears in: + +* `+container/Containerfile+` +* `+container/compose.toml+` +* `+container/deploy.k9.ncl+` +* `+container/entrypoint.sh+` +* `+container/manifest.toml+` +* `+container/vordr.toml+` + +==== `+{{PROJECT_DESCRIPTION}}+` + +One-line description, matching the forge description. + +Appears in: + +* `+container/Containerfile+` +* `+container/manifest.toml+` + +==== `+{{PROJECT_UNIQUE_STRENGTH}}+` + +What this does that its alternatives do not. + +Appears in: + +* `+.machine_readable/bot_directives/methodology.a2ml+` + +==== `+{{REGISTRY}}+` + +Container registry to publish to. + +Appears in: + +* `+container/compose.toml+` +* `+container/ct-build.sh+` +* `+container/deploy.k9.ncl+` + +==== `+{{SECURITY_EMAIL}}+` + +Address for private vulnerability reports. Two competing values exist in +the estate (`+6759885+hyperpolymath@users.noreply.github.com+` and +`+security@hyperpolymath.org+`) — pick one deliberately. + +Appears in: + +* `+.well-known/security.txt+` + +==== `+{{SERVICE_NAME}}+` + +Container service name. + +Appears in: + +* `+container/.gatekeeper.yaml+` +* `+container/Containerfile+` +* `+container/compose.toml+` +* `+container/ct-build.sh+` +* `+container/deploy.k9.ncl+` +* `+container/entrypoint.sh+` +* `+container/manifest.toml+` +* `+container/vordr.toml+` + +==== `+{{TEST_CMD}}+` + +The exact command that runs its tests. + +Appears in: + +* `+QUICKSTART-DEV.adoc+` + +==== `+{{VERSION}}+` + +Version/tag for the container image. + +Appears in: + +* `+container/deploy.k9.ncl+` +* `+container/manifest.toml+` +* `+container/vordr.toml+` + +==== `+{{WEBSITE}}+` + +Project homepage URL, or delete the field if there is none. + +Appears in: + +* `+.well-known/security.txt+` + +''''' + +Generated by the estate top-up pass. Rationale and the governing rulings +are in `+hyperpolymath/standards+`; the token vocabulary is +`+.machine_readable/ai/PLACEHOLDERS.adoc+` in `+rsr-template-repo+`. diff --git a/REQUIRES_INITIALISATION.md b/REQUIRES_INITIALISATION.md deleted file mode 100644 index 1c5582e..0000000 --- a/REQUIRES_INITIALISATION.md +++ /dev/null @@ -1,249 +0,0 @@ - - -# REQUIRES INITIALISATION - -**This repository is not finished being set up.** 22 substitution token(s) across 19 file(s) still have no value. - -## Why this is not already done - -This repo was created from `hyperpolymath/rsr-template-repo`. The mint -(`just repo-init`) fills every token that has a single mechanical answer — -owner, repo, author, dates, licence, branch — and it has done so here. - -The tokens below are the ones it *deliberately cannot* answer. They need a -decision or a fact that exists only in your head: what this project is for, -what command builds it, which port the service listens on, whether a PGP key -is held at all. The template's own token vocabulary says as much — you cannot -sensibly answer "required invariants" in a thirty-second bootstrap. - -They were left **visibly unfilled on purpose**. The alternatives were both -worse: inventing plausible values would put confident falsehoods into a -security policy and an architecture document, and silently deleting the -sections would hide the fact that a decision is owed. A visible gap is -honest; a fabricated answer is not. - -## Do not delete this file until every item below is resolved - -This file is the only marker that the work is outstanding. Deleting it early -does not finish the setup, it just conceals it — and the next person or agent -to arrive will reasonably assume the repo is complete. - -- **If you are a person:** delete this file yourself once the last item is done. -- **If you are an agent:** resolve what you legitimately can, leave the rest, - and delete this file only when no token below remains anywhere in the tree. - Do not delete it to make a gate go green. - -Re-running the estate top-up tool will remove this file automatically once -nothing is outstanding, so the safest way to finish is to fix the tokens and -let the check confirm it. - -## Do these first - -`.github/settings.yml` is applied to the forge by a GitHub App. An -unfilled token here can be written into the repository's real name or -description. This has fired before in this estate: illegal braces were -collapsed to dashes and a repo was renamed `-REPO-`, which then read as -deleted. - -- `{{DESCRIPTION}}` — One-line description used in .github/settings.yml. HIGH PRIORITY: settings.yml is applied by a GitHub App, so an unfilled token here can be written into forge metadata verbatim. - -## What is needed, and where it goes - -### `{{ARGS}}` - -Arguments for the justfile recipe this appears in. - -Appears in: - -- `.machine_readable/contractiles/Justfile` -- `Justfile` - -### `{{AUTHOR_EMAIL_ALT}}` - -Appears in: - -- `.github/.mailmap` - -### `{{AUTHOR_ORG}}` - -Author's organisation. NOTE: no filled instance of this exists anywhere in the estate — consider deleting the field instead. - -Appears in: - -- `.machine_readable/self-validating/examples/project-metadata.k9.ncl` - -### `{{BUILD_CMD}}` - -The exact command that builds this project. - -Appears in: - -- `QUICKSTART-DEV.adoc` - -### `{{BUILD_OUTPUT_PATH}}` - -Where the build artefact lands. - -Appears in: - -- `QUICKSTART-MAINTAINER.adoc` - -### `{{DEPS}}` - -Prose summary of runtime/build dependencies. - -Appears in: - -- `QUICKSTART-MAINTAINER.adoc` - -### `{{DESCRIPTION}}` - -One-line description used in .github/settings.yml. HIGH PRIORITY: settings.yml is applied by a GitHub App, so an unfilled token here can be written into forge metadata verbatim. - -Appears in: - -- `.github/settings.yml` - -### `{{LANG_STACK}}` - -The language stack, in prose. - -Appears in: - -- `QUICKSTART-DEV.adoc` - -### `{{LICENSE}}` - -SPDX identifier for this repo's licence. - -Appears in: - -- `container/Containerfile` -- `container/manifest.toml` - -### `{{MUST_INVARIANTS}}` - -The invariants this project guarantees. Not answerable in a bootstrap; it is the point of the repo. - -Appears in: - -- `QUICKSTART-DEV.adoc` - -### `{{ONE_PARAGRAPH_PURPOSE}}` - -A paragraph on what this is for. - -Appears in: - -- `.machine_readable/contractiles/Intentfile.a2ml` - -### `{{OPENSSF_PROJECT_ID}}` - -OpenSSF project ID, same registration. - -Appears in: - -- `TEMPLATE-STANDARDS-AUDIT.adoc` - -### `{{PGP_KEY_URL}}` - -Public URL the PGP key can be fetched from. Same caveat as PGP_FINGERPRINT. - -Appears in: - -- `.well-known/security.txt` - -### `{{PORT}}` - -Port the container service listens on. - -Appears in: - -- `container/Containerfile` -- `container/compose.toml` -- `container/deploy.k9.ncl` -- `container/entrypoint.sh` -- `container/manifest.toml` -- `container/vordr.toml` - -### `{{PROJECT_DESCRIPTION}}` - -One-line description, matching the forge description. - -Appears in: - -- `container/Containerfile` -- `container/manifest.toml` - -### `{{PROJECT_UNIQUE_STRENGTH}}` - -What this does that its alternatives do not. - -Appears in: - -- `.machine_readable/bot_directives/methodology.a2ml` - -### `{{REGISTRY}}` - -Container registry to publish to. - -Appears in: - -- `container/compose.toml` -- `container/ct-build.sh` -- `container/deploy.k9.ncl` - -### `{{SECURITY_EMAIL}}` - -Address for private vulnerability reports. Two competing values exist in the estate (`6759885+hyperpolymath@users.noreply.github.com` and `security@hyperpolymath.org`) — pick one deliberately. - -Appears in: - -- `.well-known/security.txt` - -### `{{SERVICE_NAME}}` - -Container service name. - -Appears in: - -- `container/.gatekeeper.yaml` -- `container/Containerfile` -- `container/compose.toml` -- `container/ct-build.sh` -- `container/deploy.k9.ncl` -- `container/entrypoint.sh` -- `container/manifest.toml` -- `container/vordr.toml` - -### `{{TEST_CMD}}` - -The exact command that runs its tests. - -Appears in: - -- `QUICKSTART-DEV.adoc` - -### `{{VERSION}}` - -Version/tag for the container image. - -Appears in: - -- `container/deploy.k9.ncl` -- `container/manifest.toml` -- `container/vordr.toml` - -### `{{WEBSITE}}` - -Project homepage URL, or delete the field if there is none. - -Appears in: - -- `.well-known/security.txt` - ---- - -Generated by the estate top-up pass. Rationale and the governing rulings are -in `hyperpolymath/standards`; the token vocabulary is -`.machine_readable/ai/PLACEHOLDERS.adoc` in `rsr-template-repo`. diff --git a/SECURITY.adoc b/SECURITY.adoc new file mode 100644 index 0000000..e47fdd9 --- /dev/null +++ b/SECURITY.adoc @@ -0,0 +1,16 @@ +== Security Policy + +=== Reporting a Vulnerability + +If you discover a security vulnerability, please report it responsibly. + +*Email:* j.d.a.jewell@open.ac.uk + +*Please include:* - Description of the vulnerability - Steps to +reproduce - Potential impact + +*Response timeline:* - Acknowledgement within 48 hours - Initial +assessment within 7 days - Fix or mitigation within 90 days + +*Safe harbour:* We will not pursue legal action against security +researchers who follow responsible disclosure. diff --git a/SECURITY.md b/SECURITY.md deleted file mode 100644 index c7c239f..0000000 --- a/SECURITY.md +++ /dev/null @@ -1,23 +0,0 @@ - -# Security Policy - -## Reporting a Vulnerability - -If you discover a security vulnerability, please report it responsibly. - -**Email:** j.d.a.jewell@open.ac.uk - -**Please include:** -- Description of the vulnerability -- Steps to reproduce -- Potential impact - -**Response timeline:** -- Acknowledgement within 48 hours -- Initial assessment within 7 days -- Fix or mitigation within 90 days - -**Safe harbour:** We will not pursue legal action against security researchers who follow responsible disclosure. diff --git a/TEST-NEEDS.adoc b/TEST-NEEDS.adoc new file mode 100644 index 0000000..d4be499 --- /dev/null +++ b/TEST-NEEDS.adoc @@ -0,0 +1,137 @@ +== TEST-NEEDS: rsr-template-repo + +=== CRG Grade: C — ACHIEVED 2026-04-04 + +=== Current State (Updated 2026-04-04) + +[width="100%",cols="40%,26%,34%",options="header",] +|=== +|Category |Count |Details +|*Source modules* |6 |3 Idris2 ABI (Foreign, Layout, Types), 2 Zig FFI +(build, main), 1 Zig integration test template + +|*Unit tests* |0 |None in main source (inline tests in main.zig) + +|*Integration tests* |1 |test/integration_test.zig (documented template, +1 placeholder test) + +|*E2E tests* |1 |tests/e2e/template_instantiation_test.sh (full +instantiation + validation) + +|*Workflow tests* |1 |tests/workflows/validate_workflows_test.sh (21 +workflows validated) + +|*Validation tests* |1 |scripts/validate-template.sh (8-phase +comprehensive validation) + +|*Benchmarks* |5 |benches/template_bench.sh (validation, Zig build, +tests, workflows, instantiation) + +|*Fuzz tests* |0 |README.adoc scaffold with harness instructions +|=== + +=== Completed Work (CRG C - Testing & Benchmarking) + +==== Template Validation Script ✅ + +* [x] `+scripts/validate-template.sh+` — 8-phase validation +** Phase 1: Core repository structure (root files, directories) +** Phase 2: Machine-readable metadata (.machine_readable/) +** Phase 3: GitHub Actions workflows (17 required + all present) +** Phase 4: Idris2 ABI and Zig FFI source files +** Phase 5: Placeholder token replacement (skipped in template) +** Phase 6: SPDX license headers (100% coverage, 6/6 files) +** Phase 7: Build system verification (zig build + idris2 syntax check) +** Phase 8: Documentation requirements (TOPOLOGY, ABI-FFI-README, etc) +* Status: *PASSING* (0 errors, 3 warnings about template placeholders) + +==== E2E Template Instantiation Test ✅ + +* [x] `+tests/e2e/template_instantiation_test.sh+` — full workflow +** Clones template to temp directory +** Replaces all \{\{PLACEHOLDER}} tokens with test values +** Validates resulting structure with scripts/validate-template.sh +** Verifies Zig build works after instantiation +** Checks no remaining placeholders +** Cleans up temp directory +* Status: *READY TO TEST* (can be verified by CI) + +==== Workflow Validation Test ✅ + +* [x] `+tests/workflows/validate_workflows_test.sh+` +** Validates all 21 workflows exist and have proper structure +** Checks SPDX headers, '`name`' field +** Verifies all 15 required workflows present +* Status: *PASSING* (0 errors, 15/15 required workflows found) + +==== Zig FFI Tests ✅ + +* [x] `+src/interface/ffi/test/integration_test.zig+` — template with +examples +** Converted from nextgen_typing placeholders to "`template`" namespace +** Added comprehensive comments for how to instantiate +** Tests grouped by category (lifecycle, operations, strings, errors, +version, memory safety, threading) +** Compiles and passes placeholder test +* Status: *PASSING* (1 test: placeholder_test_implementation_required +passes) + +==== Benchmarks ✅ + +* [x] `+benches/template_bench.sh+` — 5 benchmark suites +** Validation script: ~5.8s average (3 runs) +** Zig build: ~19ms (clean build) +** Zig tests: ~20ms +** Workflow validation: ~117ms +** Template instantiation: ~427ms +* Formats: human, json, csv +* Status: *PASSING* (all benchmarks execute) + +==== Build System ✅ + +* [x] `+src/interface/ffi/build.zig+` — updated for Zig 0.15.2 +** Simplified to test-only configuration +** Supports both unit tests and integration tests +** Works with `+zig build+` without errors +* Status: *PASSING* (builds successfully) + +=== Test Results Summary + +.... +Validation Script: PASS (0 errors, 3 warnings) +Workflow Validation: PASS (21/21 workflows valid) +Integration Tests: PASS (1/1 placeholder test) +E2E Instantiation: READY (needs CI confirmation) +Benchmarks: PASS (5/5 benchmark suites) +Build System: PASS (zig build succeeds) +.... + +=== CRG C Compliance + +* *Coverage*: 6/6 test categories (unit, integration, E2E, workflow, +validation, benchmarks) +* *Documentation*: All test files have SPDX headers + inline +documentation +* *Author Attribution*: Jonathan D.A. Jewell j.d.a.jewell@open.ac.uk +* *License*: MPL-2.0 on all new files +* *Automation*: All scripts executable + working + +=== FLAGGED ISSUES - ALL RESOLVED + +* [line-through]#*Template repo used by ALL new repos has 0 validation +tests*# → FIXED: 4 test suites + validation script +* [line-through]#*fuzz/placeholder.txt*# → FIXED: replaced with +README.adoc containing real harness instructions +* [line-through]#*No E2E tests for template instantiation*# → FIXED: +full E2E test suite +* [line-through]#*Zig FFI integration tests are placeholders*# → FIXED: +converted to documented template format + +=== Next Steps (Future Sessions) + +* [ ] Integrate test scripts into CI/CD workflows +* [ ] Generate test coverage reports +* [ ] Add more specialized benchmarks (memory, threading stress) +* [ ] Document test instantiation patterns for new repos + +=== Priority: P0 (COMPLETE) ✅ diff --git a/TEST-NEEDS.md b/TEST-NEEDS.md deleted file mode 100644 index 60dd2c4..0000000 --- a/TEST-NEEDS.md +++ /dev/null @@ -1,111 +0,0 @@ - -# TEST-NEEDS: rsr-template-repo - -## CRG Grade: C — ACHIEVED 2026-04-04 - -## Current State (Updated 2026-04-04) - -| Category | Count | Details | -|----------|-------|---------| -| **Source modules** | 6 | 3 Idris2 ABI (Foreign, Layout, Types), 2 Zig FFI (build, main), 1 Zig integration test template | -| **Unit tests** | 0 | None in main source (inline tests in main.zig) | -| **Integration tests** | 1 | test/integration_test.zig (documented template, 1 placeholder test) | -| **E2E tests** | 1 | tests/e2e/template_instantiation_test.sh (full instantiation + validation) | -| **Workflow tests** | 1 | tests/workflows/validate_workflows_test.sh (21 workflows validated) | -| **Validation tests** | 1 | scripts/validate-template.sh (8-phase comprehensive validation) | -| **Benchmarks** | 5 | benches/template_bench.sh (validation, Zig build, tests, workflows, instantiation) | -| **Fuzz tests** | 0 | README.adoc scaffold with harness instructions | - -## Completed Work (CRG C - Testing & Benchmarking) - -### Template Validation Script ✅ -- [x] `scripts/validate-template.sh` — 8-phase validation - - Phase 1: Core repository structure (root files, directories) - - Phase 2: Machine-readable metadata (.machine_readable/) - - Phase 3: GitHub Actions workflows (17 required + all present) - - Phase 4: Idris2 ABI and Zig FFI source files - - Phase 5: Placeholder token replacement (skipped in template) - - Phase 6: SPDX license headers (100% coverage, 6/6 files) - - Phase 7: Build system verification (zig build + idris2 syntax check) - - Phase 8: Documentation requirements (TOPOLOGY, ABI-FFI-README, etc) -- Status: **PASSING** (0 errors, 3 warnings about template placeholders) - -### E2E Template Instantiation Test ✅ -- [x] `tests/e2e/template_instantiation_test.sh` — full workflow - - Clones template to temp directory - - Replaces all {{PLACEHOLDER}} tokens with test values - - Validates resulting structure with scripts/validate-template.sh - - Verifies Zig build works after instantiation - - Checks no remaining placeholders - - Cleans up temp directory -- Status: **READY TO TEST** (can be verified by CI) - -### Workflow Validation Test ✅ -- [x] `tests/workflows/validate_workflows_test.sh` - - Validates all 21 workflows exist and have proper structure - - Checks SPDX headers, 'name' field - - Verifies all 15 required workflows present -- Status: **PASSING** (0 errors, 15/15 required workflows found) - -### Zig FFI Tests ✅ -- [x] `src/interface/ffi/test/integration_test.zig` — template with examples - - Converted from nextgen_typing placeholders to "template" namespace - - Added comprehensive comments for how to instantiate - - Tests grouped by category (lifecycle, operations, strings, errors, version, memory safety, threading) - - Compiles and passes placeholder test -- Status: **PASSING** (1 test: placeholder_test_implementation_required passes) - -### Benchmarks ✅ -- [x] `benches/template_bench.sh` — 5 benchmark suites - - Validation script: ~5.8s average (3 runs) - - Zig build: ~19ms (clean build) - - Zig tests: ~20ms - - Workflow validation: ~117ms - - Template instantiation: ~427ms -- Formats: human, json, csv -- Status: **PASSING** (all benchmarks execute) - -### Build System ✅ -- [x] `src/interface/ffi/build.zig` — updated for Zig 0.15.2 - - Simplified to test-only configuration - - Supports both unit tests and integration tests - - Works with `zig build` without errors -- Status: **PASSING** (builds successfully) - -## Test Results Summary - -``` -Validation Script: PASS (0 errors, 3 warnings) -Workflow Validation: PASS (21/21 workflows valid) -Integration Tests: PASS (1/1 placeholder test) -E2E Instantiation: READY (needs CI confirmation) -Benchmarks: PASS (5/5 benchmark suites) -Build System: PASS (zig build succeeds) -``` - -## CRG C Compliance - -- **Coverage**: 6/6 test categories (unit, integration, E2E, workflow, validation, benchmarks) -- **Documentation**: All test files have SPDX headers + inline documentation -- **Author Attribution**: Jonathan D.A. Jewell -- **License**: MPL-2.0 on all new files -- **Automation**: All scripts executable + working - -## FLAGGED ISSUES - ALL RESOLVED - -- ~~**Template repo used by ALL new repos has 0 validation tests**~~ → FIXED: 4 test suites + validation script -- ~~**fuzz/placeholder.txt**~~ → FIXED: replaced with README.adoc containing real harness instructions -- ~~**No E2E tests for template instantiation**~~ → FIXED: full E2E test suite -- ~~**Zig FFI integration tests are placeholders**~~ → FIXED: converted to documented template format - -## Next Steps (Future Sessions) - -- [ ] Integrate test scripts into CI/CD workflows -- [ ] Generate test coverage reports -- [ ] Add more specialized benchmarks (memory, threading stress) -- [ ] Document test instantiation patterns for new repos - -## Priority: P0 (COMPLETE) ✅ diff --git a/TOPOLOGY.adoc b/TOPOLOGY.adoc new file mode 100644 index 0000000..a975f58 --- /dev/null +++ b/TOPOLOGY.adoc @@ -0,0 +1,36 @@ +== Architecture Topology + +=== System Overview + +RSR (Rhodium Standard Repository) template provides the canonical +scaffold for all hyperpolymath projects, with integrated CI/CD, +documentation, and service discovery patterns. + +=== Component Overview + +[width="100%",cols="37%,33%,30%",options="header",] +|=== +|Component |Language |Purpose +|dogfood-gate workflow |YAML |Quality checks (CRG, security, linting) +|eclexiaiser-validate job |YAML |Resource cost awareness scoring +|Groove discovery |JSON |Service endpoint registration +|=== + +=== Data Flow + +.... +[Code Push] → [GitHub Actions] → [hypatia scan] → [eclexiaiser validate] → [Results] +.... + +=== Integration Points + +* *Upstream*: Hypatia (neurosymbolic CI/CD), eclexiaiser (resource +scoring) +* *Downstream*: All RSR-based repositories (500+ instances) + +=== Deployment + +* Container: Stapeln Six ecosystem +* CI/CD: GitHub Actions → Hypatia scan → eclexiaiser-validate (6 +scorecard dimensions) → Mirror +* Service Discovery: Groove protocol (.well-known/groove/manifest.json) diff --git a/TOPOLOGY.md b/TOPOLOGY.md deleted file mode 100644 index 4ad8569..0000000 --- a/TOPOLOGY.md +++ /dev/null @@ -1,36 +0,0 @@ - - - -# Architecture Topology - -## System Overview - -RSR (Rhodium Standard Repository) template provides the canonical scaffold for all hyperpolymath projects, with integrated CI/CD, documentation, and service discovery patterns. - -## Component Overview - -| Component | Language | Purpose | -|-----------|----------|---------| -| dogfood-gate workflow | YAML | Quality checks (CRG, security, linting) | -| eclexiaiser-validate job | YAML | Resource cost awareness scoring | -| Groove discovery | JSON | Service endpoint registration | - -## Data Flow - -``` -[Code Push] → [GitHub Actions] → [hypatia scan] → [eclexiaiser validate] → [Results] -``` - -## Integration Points - -- **Upstream**: Hypatia (neurosymbolic CI/CD), eclexiaiser (resource scoring) -- **Downstream**: All RSR-based repositories (500+ instances) - -## Deployment - -- Container: Stapeln Six ecosystem -- CI/CD: GitHub Actions → Hypatia scan → eclexiaiser-validate (6 scorecard dimensions) → Mirror -- Service Discovery: Groove protocol (.well-known/groove/manifest.json) diff --git a/docs/tech-debt-2026-05-26.adoc b/docs/tech-debt-2026-05-26.adoc new file mode 100644 index 0000000..60d0ffd --- /dev/null +++ b/docs/tech-debt-2026-05-26.adoc @@ -0,0 +1,80 @@ +== Tech-Debt Audit — nextgen-typing — 2026-05-26 + +*Source:* estate-wide automated scan 2026-05-26. *Companion:* +https://github.com/hyperpolymath/standards/tree/main/docs/audits[`+hyperpolymath/standards+` +2026-05-26-estate-*-debt audits]. *Combined severity:* `+LOW+`. + +This file records the _raw findings_ — it does not by itself fix the +debt. Each section ends with a '`Recommended next move`' line; closing +the debt is follow-up work. + +=== 1. Proof debt + +Scanner counted the following markers in proof-bearing files of this +repo: + +.... +files= 13 | Coq-Axm/Adm= 0 | Lean-srry/ax= 0 | Agda-pst= 0 | Idr-blv= 6 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0 +.... + +*Total markers:* 6. *Severity:* `+>06+`. + +*Marker types* (any non-zero counts above): - Coq `+Axiom+`/`+Admitted+` +— unconditional proof escapes. - Lean `+sorry+`/`+axiom+` — Lean’s +equivalent. - Agda `+postulate+` — accepted axiomatically. - Idris2 +`+believe_me+`/`+assert_total+` — runtime-safe coercion / totality +assumption. - Idris2 top-level `+partial+` — totality-check waived. - F* +`+assume val+`/`+admit_p+` — F* admit. - `+TODO PROOF+` / `+OWED:+` — +self-documented debt markers. - `+unsafePerformIO+`/`+unsafeCoerce+` — +soundness-relevant escape hatches in Haskell/Rust source. + +*Recommended next move:* triage each finding into one of: (a) discharge +by proof, (b) cover with property-tests + a documented refutation +budget, or (c) annotate as a known/necessary axiom (e.g. `+funExt+`) in +`+docs/proof-debt.md+`. + +=== 2. Licence debt + +[cols=",",options="header",] +|=== +|Field |Value +|LICENSE file |`+LICENSE+` +|SPDX header |`+MPL-2.0+` +|Manifest licence |`+NONE+` +|Body classifier |`+Palimp-MPL-2.0+` +|Severity |`+ok+` +|=== + +*Recommended next move:* none for licence. + +=== 3. Documentation debt + +[cols=",",options="header",] +|=== +|Field |Value +|README lines |89 +|`+docs/+` files |56 +|`+docs/+` LoC |2436 +|CHANGELOG.md |Y +|CONTRIBUTING.md |Y +|CODE_OF_CONDUCT.md |Y +|SECURITY.md |Y +|Severity |`+OK+` +|=== + +*Recommended next move:* none for docs. + +=== Cross-references + +* Estate proof-debt audit: +`+hyperpolymath/standards/docs/audits/2026-05-26-estate-proof-debt.md+` +* Estate licence-debt audit: +`+hyperpolymath/standards/docs/audits/2026-05-26-estate-licence-debt.md+` +* Estate documentation-debt audit: +`+hyperpolymath/standards/docs/audits/2026-05-26-estate-documentation-debt.md+` + +''''' + +🤖 Generated by Claude Code estate-wide tech-debt scan (2026-05-26). +This file is informational — closing the debt is follow-up work owned by +the maintainer. diff --git a/docs/tech-debt-2026-05-26.md b/docs/tech-debt-2026-05-26.md deleted file mode 100644 index bb45307..0000000 --- a/docs/tech-debt-2026-05-26.md +++ /dev/null @@ -1,71 +0,0 @@ - - -# Tech-Debt Audit — nextgen-typing — 2026-05-26 - -**Source:** estate-wide automated scan 2026-05-26. -**Companion:** [`hyperpolymath/standards` 2026-05-26-estate-*-debt audits](https://github.com/hyperpolymath/standards/tree/main/docs/audits). -**Combined severity:** `LOW`. - -This file records the *raw findings* — it does not by itself fix the debt. Each section ends with a 'Recommended next move' line; closing the debt is follow-up work. - -## 1. Proof debt - -Scanner counted the following markers in proof-bearing files of this repo: - -``` -files= 13 | Coq-Axm/Adm= 0 | Lean-srry/ax= 0 | Agda-pst= 0 | Idr-blv= 6 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0 -``` - -**Total markers:** 6. **Severity:** `>06`. - -**Marker types** (any non-zero counts above): -- Coq `Axiom`/`Admitted` — unconditional proof escapes. -- Lean `sorry`/`axiom` — Lean's equivalent. -- Agda `postulate` — accepted axiomatically. -- Idris2 `believe_me`/`assert_total` — runtime-safe coercion / totality assumption. -- Idris2 top-level `partial` — totality-check waived. -- F\* `assume val`/`admit_p` — F\* admit. -- `TODO PROOF` / `OWED:` — self-documented debt markers. -- `unsafePerformIO`/`unsafeCoerce` — soundness-relevant escape hatches in Haskell/Rust source. - -**Recommended next move:** triage each finding into one of: (a) discharge by proof, (b) cover with property-tests + a documented refutation budget, or (c) annotate as a known/necessary axiom (e.g. `funExt`) in `docs/proof-debt.md`. - -## 2. Licence debt - -| Field | Value | -|---|---| -| LICENSE file | `LICENSE` | -| SPDX header | `MPL-2.0` | -| Manifest licence | `NONE` | -| Body classifier | `Palimp-MPL-2.0` | -| Severity | `ok` | - -**Recommended next move:** none for licence. - -## 3. Documentation debt - -| Field | Value | -|---|---| -| README lines | 89 | -| `docs/` files | 56 | -| `docs/` LoC | 2436 | -| CHANGELOG.md | Y | -| CONTRIBUTING.md | Y | -| CODE_OF_CONDUCT.md | Y | -| SECURITY.md | Y | -| Severity | `OK` | - -**Recommended next move:** none for docs. - -## Cross-references - -- Estate proof-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-proof-debt.md` -- Estate licence-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-licence-debt.md` -- Estate documentation-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-documentation-debt.md` - ---- - -🤖 Generated by Claude Code estate-wide tech-debt scan (2026-05-26). This file is informational — closing the debt is follow-up work owned by the maintainer. diff --git a/llm-warmup-dev.adoc b/llm-warmup-dev.adoc new file mode 100644 index 0000000..53a88aa --- /dev/null +++ b/llm-warmup-dev.adoc @@ -0,0 +1,19 @@ +== LLM Warmup — rsr-template-repo (Developer) + +=== What is rsr-template-repo? + +See README.adoc for overview. + +=== Key Commands + +* `+just setup+` — set up development environment +* `+just build+` — build the project +* `+just test+` — run tests +* `+just doctor+` — diagnose issues +* `+just heal+` — attempt auto-repair + +=== Quick Context + +* License: MPL-2.0 +* Part of hyperpolymath ecosystem +* See EXPLAINME.adoc for architecture diff --git a/llm-warmup-dev.md b/llm-warmup-dev.md deleted file mode 100644 index 67aac34..0000000 --- a/llm-warmup-dev.md +++ /dev/null @@ -1,20 +0,0 @@ - -# LLM Warmup — rsr-template-repo (Developer) - -## What is rsr-template-repo? -See README.adoc for overview. - -## Key Commands -- `just setup` — set up development environment -- `just build` — build the project -- `just test` — run tests -- `just doctor` — diagnose issues -- `just heal` — attempt auto-repair - -## Quick Context -- License: MPL-2.0 -- Part of hyperpolymath ecosystem -- See EXPLAINME.adoc for architecture diff --git a/llm-warmup-user.adoc b/llm-warmup-user.adoc new file mode 100644 index 0000000..c13529e --- /dev/null +++ b/llm-warmup-user.adoc @@ -0,0 +1,19 @@ +== LLM Warmup — rsr-template-repo (User) + +=== What is rsr-template-repo? + +See README.adoc for overview. + +=== Key Commands + +* `+just setup+` — set up development environment +* `+just build+` — build the project +* `+just test+` — run tests +* `+just doctor+` — diagnose issues +* `+just heal+` — attempt auto-repair + +=== Quick Context + +* License: MPL-2.0 +* Part of hyperpolymath ecosystem +* See EXPLAINME.adoc for architecture diff --git a/llm-warmup-user.md b/llm-warmup-user.md deleted file mode 100644 index 2eaf893..0000000 --- a/llm-warmup-user.md +++ /dev/null @@ -1,20 +0,0 @@ - -# LLM Warmup — rsr-template-repo (User) - -## What is rsr-template-repo? -See README.adoc for overview. - -## Key Commands -- `just setup` — set up development environment -- `just build` — build the project -- `just test` — run tests -- `just doctor` — diagnose issues -- `just heal` — attempt auto-repair - -## Quick Context -- License: MPL-2.0 -- Part of hyperpolymath ecosystem -- See EXPLAINME.adoc for architecture diff --git a/session/README.adoc b/session/README.adoc new file mode 100644 index 0000000..d14a6d7 --- /dev/null +++ b/session/README.adoc @@ -0,0 +1,45 @@ +== Session Bindings (Thin Local Layer) + +This directory provides local integration for central session-management +standards. + +Authoritative protocols live in: + +* `+../standards/session-management-standards/+` (or +`+$SESSION_STANDARDS_DIR+`) + +This repo keeps only thin bindings: + +* `+dispatch.sh+` maps canonical commands to central protocol paths. +* `+custom-checks.k9+` defines repo-local policy checks. +* `+local-hooks.sh+` provides optional repo-specific hook behavior. + +=== Canonical Commands + +* `+intake repo +` +* `+checkpoint change +` +* `+verify maintenance +` +* `+verify substantial +` +* `+verify release +` +* `+close planned +` +* `+close urgent +` +* `+recover repo +` +* `+handover full +` +* `+handover split +` +* `+handover model +` +* `+handover human +` + +=== Justfile Aliases + +Run `+just session-help+` to list aliases, then use recipes such as: + +* `+just intake-repo path=.+` +* `+just checkpoint-change path=.+` +* `+just verify-maintenance path=.+` +* `+just close-planned path=.+` +* `+just handover-model path=.+` + +=== Runtime Artifacts + +Runtime files are generated per repository in `+.session/+` and are not +canonical standards text. diff --git a/session/README.md b/session/README.md deleted file mode 100644 index af5c8d0..0000000 --- a/session/README.md +++ /dev/null @@ -1,46 +0,0 @@ - -# Session Bindings (Thin Local Layer) - -This directory provides local integration for central session-management standards. - -Authoritative protocols live in: - -- `../standards/session-management-standards/` (or `$SESSION_STANDARDS_DIR`) - -This repo keeps only thin bindings: - -- `dispatch.sh` maps canonical commands to central protocol paths. -- `custom-checks.k9` defines repo-local policy checks. -- `local-hooks.sh` provides optional repo-specific hook behavior. - -## Canonical Commands - -- `intake repo ` -- `checkpoint change ` -- `verify maintenance ` -- `verify substantial ` -- `verify release ` -- `close planned ` -- `close urgent ` -- `recover repo ` -- `handover full ` -- `handover split ` -- `handover model ` -- `handover human ` - -## Justfile Aliases - -Run `just session-help` to list aliases, then use recipes such as: - -- `just intake-repo path=.` -- `just checkpoint-change path=.` -- `just verify-maintenance path=.` -- `just close-planned path=.` -- `just handover-model path=.` - -## Runtime Artifacts - -Runtime files are generated per repository in `.session/` and are not canonical standards text.