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 caeda1c..0000000 --- a/CODE_OF_CONDUCT.md +++ /dev/null @@ -1,27 +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 8725e71..0000000 --- a/CONTRIBUTING.md +++ /dev/null @@ -1,9 +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/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc new file mode 100644 index 0000000..547b41d --- /dev/null +++ b/PROOF-NEEDS.adoc @@ -0,0 +1,135 @@ +== Proof Requirements — KATAGORIA + +=== Proof Tier + +*Tier*: T3 — Standard + +=== Proof Categories + +[width="100%",cols="24%,36%,40%",options="header",] +|=== +|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: + +==== ABI/FFI Boundary Proofs (Idris2) + +[width="100%",cols="13%,29%,33%,25%",options="header",] +|=== +|# |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+` +|=== + +==== Typing Proofs (Prover Varies) + +[width="100%",cols="13%,29%,33%,25%",options="header",] +|=== +|# |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+` +|=== + +=== Project-Specific Proofs + +[cols=",,,,,",options="header",] +|=== +|# |Proof Needed |Category |Prover |Priority |File(s) +| | | | | | +|=== + +=== Dangerous Patterns (BANNED) + +The following MUST NOT appear anywhere in proof files: + +[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 +|`+unsafe+` (unaudited) |Rust |Unsafe block without safety comment +|=== + +CI will reject any PR introducing these patterns (enforced by +`+panic-attack assail+`). + +=== Prover Selection Guide + +[width="100%",cols="31%,55%,14%",options="header",] +|=== +|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 +.... + +=== References + +* Master list: `+~/Desktop/PROOF-REQUIREMENTS-MASTER.md+` +* 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-NEEDS.md b/PROOF-NEEDS.md deleted file mode 100644 index 8d46487..0000000 --- a/PROOF-NEEDS.md +++ /dev/null @@ -1,103 +0,0 @@ -# Proof Requirements — KATAGORIA - - - - -## 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: - -### 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` | - -### Typing Proofs (Prover Varies) - -| # | 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` | - -## Project-Specific Proofs - - - - -| # | Proof Needed | Category | Prover | Priority | File(s) | -|---|-------------|----------|--------|----------|---------| -| | | | | | | - -## Dangerous Patterns (BANNED) - -The following MUST NOT appear anywhere in proof files: - -| 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 | -| `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 -``` - -## References - -- Master list: `~/Desktop/PROOF-REQUIREMENTS-MASTER.md` -- 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.adoc b/PROOF-STATUS.adoc new file mode 100644 index 0000000..32c5a14 --- /dev/null +++ b/PROOF-STATUS.adoc @@ -0,0 +1,87 @@ +== Proof Status — KATAGORIA + +=== Summary + +[cols=",,,,,",options="header",] +|=== +|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 + +[cols=",,,,,",options="header",] +|=== +|ID |Proof |Prover |File |Date |Verified By +|— |No proofs completed yet |— |— |— |— +|=== + +=== Proofs In Progress + +[cols=",,,,,",options="header",] +|=== +|ID |Proof |Prover |Assignee |Started |Blocker +|— |— |— |— |— |— +|=== + +=== Proofs Blocked + +[cols=",,,",options="header",] +|=== +|ID |Proof |Blocked By |Notes +|— |— |— |— +|=== + +=== Proofs Remaining + +[cols=",,,,,",options="header",] +|=== +|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 +|=== + +=== Verification Commands + +[source,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 + +# Scan for dangerous patterns +panic-attack assail --proofs-only +---- + +=== Changelog + +[cols=",,",options="header",] +|=== +|Date |Change |By +|2026-04-04 |Initial proof status tracking |Template +|=== diff --git a/PROOF-STATUS.md b/PROOF-STATUS.md deleted file mode 100644 index 154a24e..0000000 --- a/PROOF-STATUS.md +++ /dev/null @@ -1,81 +0,0 @@ -# Proof Status — KATAGORIA - - - - -## 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 | — | — | — | — | - -## Proofs In Progress - -| ID | Proof | Prover | Assignee | Started | Blocker | -|----|-------|--------|----------|---------|---------| -| — | — | — | — | — | — | - -## Proofs Blocked - -| ID | Proof | Blocked By | Notes | -|----|-------|------------|-------| -| — | — | — | — | - -## Proofs Remaining - -| 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 | - -## Verification Commands - -```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 - -# Scan for dangerous patterns -panic-attack assail --proofs-only -``` - -## Changelog - -| Date | Change | By | -|------|--------|-----| -| 2026-04-04 | Initial proof status tracking | Template | diff --git a/READINESS.adoc b/READINESS.adoc new file mode 100644 index 0000000..fee6ee0 --- /dev/null +++ b/READINESS.adoc @@ -0,0 +1,55 @@ +== katagoria 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-08-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 katagoria 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 3f67810..0000000 --- a/READINESS.md +++ /dev/null @@ -1,53 +0,0 @@ - - - -# katagoria 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-08-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 katagoria 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/README.adoc b/README.adoc index 864854c..5e7f259 100644 --- a/README.adoc +++ b/README.adoc @@ -1,169 +1,76 @@ -// SPDX-License-Identifier: MPL-2.0 -= Ideas to Alphas — The Type Theory Incubator -:toc: preamble -:toc-title: Contents -:icons: font -:doctype: article +Jonathan D.A. Jewell :toc: :icons: font -image:https://img.shields.io/badge/OpenSSF-BestPractices-green[link="https://www.bestpractices.dev/projects/XXXX"] +____ +[!TIP] *AI agents:* read `+0-AI-MANIFEST.a2ml+` first, then +`+.machine_readable/6a2/STATE.a2ml+`. +____ -The theory→practice incubator for the hyperpolymath type theory pipeline. Findings from the lab (Kategoria) are matured from idea to alpha here, before earning their own production repository. +== What This Is -== Overview +`+ideas-to-alphas+` is the *incubator* of the hyperpolymath type theory +pipeline: the theory→practice stage where a finding from the *lab* +(`+kategoria+`) is matured from *idea to alpha* before it earns its own +production (typed) repo. -Ideas to Alphas is the middle stage of the type theory pipeline: +____ +[!NOTE] This repo is mid-rename. The GitHub repo and local directory are +still named `+kategoria-pipeline+` until the owner runs `+gh+` `+repo+` +`+rename+` `+ideas-to-alphas+` (+ local `+mv+`). The role split — *lab* += `+kategoria+` (research/discovery), *incubator* = this repo +(idea→alpha), *portal* = `+nextgen-typing+` (front-page on-ramp for +people) — is captured in +`+dev-notes/2026-06-16-typing-sub-estate-roles-and-lifecycle.adoc+`. +Also update `+project+` `+=+` `+"katagoria"+` → `+"ideas-to-alphas"+` in +`+.machine_readable/6a2/STATE.a2ml+` at rename time. +____ - Kategoria → ideas-to-alphas → typell → typed-wasm → PanLL - (lab) (this repo) (kernel) (target) (eNSAID) +== Pipeline Position -Kategoria is upstream research and discovery. This repo is the incubator: proofs-of-concept, reading notes, prototype formalisations, and experimental definitions. Typell is downstream: the production verification kernel. Artefacts graduate from here to Typell when they are ready for integration. +.... +katagoria → typell → typed-wasm → PanLL +(this repo) (kernel) (target) (eNSAID env) +.... -This is where the ceiling gets pushed. The current type-safety levels (L1–L10) were designed here first, then promoted. Future levels (L11, L12, …) will originate here. +`+katagoria+` is upstream of everything. Ideas here are *speculative*: +proofs-of-concept, reading notes, prototype Idris2/Lean formalizations. +They graduate to `+typell+` when they are ready to be integrated into +the production verification kernel. -== What lives here +Coordination monorepo: +https://github.com/hyperpolymath/nextgen-typing[nextgen-typing] -* **Type theory prototypes** — Idris 2, Lean 4, Agda proofs-of-concept for speculative constructions. -* **Research notes** — papers being read, formalised, and annotated. -* **Experimental level definitions** — candidate type-safety levels beyond L10. -* **Speculative session type extensions** — multi-party, probabilistic, temporal variants. -* **Tropical type theory experiments** — connections to protocol-squisher and resource grading. -* **Constitutional proofs** — `a-sounder-constitution/` (Idris 2 formalisation of soundness constraints). +== What Lives Here -== What does NOT live here +* Type theory prototypes — Idris2, Lean 4, Agda proofs-of-concept +* Research notes on papers being read and formalized +* Experimental level definitions for the TypeLL open-ended progression +* Speculative session type extensions (multi-party, probabilistic, +temporal) +* Tropical type theory experiments (connections to protocol-squisher) -* **Production Rust code** — belongs in Typell. -* **WasmGC type safety proofs** — belongs in `typed-wasm`. -* **Anything with stability guarantees** — this repo is deliberately unstable. Artefacts here may be retracted, rewritten, or abandoned without notice. +== What Does NOT Live Here -== Pipeline role +* Production Rust code — goes in `+typell+` +* WasmGC type safety proofs — goes in `+typed-wasm+` +* Anything with stability guarantees — this repo is deliberately +unstable -[cols="1,2,2", options="header"] -|=== -| Stage | Repository | Guarantees +== Relationship to TypeLL -| Lab (discovery) -| link:https://github.com/hyperpolymath/kategoria[Kategoria] -| None. Research, falsification, stumble journal. +TypeLL is an *open-ended progressive* type safety framework. The current +L1-L10 implementation in typell was designed here first, then graduated. +Future levels (L11, L12, …) will originate here before promotion. -| Incubator (idea → alpha) -| **This repo** -| Proof-of-concept compiles. No stability. +There is no fixed ceiling. katagoria is where the ceiling gets pushed. -| Kernel (production) -| link:https://github.com/hyperpolymath/typell[Typell] -| Soundness. ABI contract. No `believe_me`. +== Status -| Target (deployment) -| link:https://github.com/hyperpolymath/typed-wasm[typed-wasm] -| WasmGC type safety. Browser/runtime target. - -| Environment (use) -| link:https://github.com/hyperpolymath/panll[PanLL] -| Cognitive relief. TEA architecture. Working UI. -|=== - -Coordination monorepo: `nextgen-typing`. - -== What is standard and what is ours - -[cols="1,2,2", options="header"] -|=== -| Concept | Status | Home - -| Prototype Idris 2 / Lean 4 / Agda formalisations -| Standard methodology -| `research/`, `verification/` - -| Research reading notes -| Standard practice -| `research/` - -| The pipeline role (lab → incubator → kernel → target) -| **Novel organisational pattern** -| Estate architecture - -| Experimental type-safety level definitions -| **Novel** (speculative) -| `research/` - -| Graduation criterion (idea → alpha → production) -| **Novel governance pattern** -| Pipeline design -|=== - -== Known scope boundaries - -[CAUTION] -==== -**Pre-alpha.** This repository is a research incubator. Its contents are speculative. Proofs-of-concept may be incorrect, incomplete, or abandoned. Nothing here carries stability guarantees. -==== - -[CAUTION] -==== -**Mid-rename.** The GitHub repository and local directory are still named `kategoria-pipeline`. The rename to `ideas-to-alphas` is pending (`gh repo rename ideas-to-alphas`). See `dev-notes/2026-06-16-typing-sub-estate-roles-and-lifecycle.adoc`. -==== - -[CAUTION] -==== -**No fixed ceiling on type-safety levels.** The L1–L10 framework is the current understanding. Future levels will originate here. The number of levels may grow, shrink, or restructure. -==== - -== Repository Layout - -[cols="1,3", options="header"] -|=== -| Path | Purpose - -| `a-sounder-constitution/` -| Idris 2 formalisation of soundness constraints - -| `research/` -| Reading notes, paper formalisations, experimental definitions - -| `verification/` -| Prototype proofs and proof-of-concept checkers - -| `silo/` -| Secret-silo design (ALARP handle/vault incubation) - -| `src/`, `tests/` -| Supporting source and test infrastructure - -| `docs/` -| Research documentation and dev notes - -| `session/` -| Speculative session type extensions - -| `features/` -| Feature specifications for graduation candidates -|=== - -== Build - -[source,bash] ----- -# Idris 2 proofs (a-sounder-constitution) -cd a-sounder-constitution/ -idris2 --check Constitution.idr - -# General build (if Justfile targets exist) -just check ----- - -See `QUICKSTART-DEV.adoc` for developer setup. - -== Documentation - -* link:EXPLAINME.adoc[EXPLAINME] — claim-by-claim receipts and known gaps -* link:Glossary.adoc[Glossary] — terminology reference -* `dev-notes/2026-06-16-typing-sub-estate-roles-and-lifecycle.adoc` — pipeline role definitions -* `ROADMAP.adoc` — research roadmap -* `PROOF-STATUS.md` — proof status tracking -* `0-AI-MANIFEST.a2ml` — AI agent entry point +Pre-alpha. Newly created (2026-04-11). Research artefacts will +accumulate over time. == License -SPDX-License-Identifier: MPL-2.0 — see link:LICENSE[LICENSE]. +MPL-2.0 -Prose documentation is licensed under CC-BY-SA-4.0; see `LICENSES/`. +Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + diff --git a/README.md b/README.md deleted file mode 100644 index 5968933..0000000 --- a/README.md +++ /dev/null @@ -1,85 +0,0 @@ - - -Jonathan D.A. Jewell \<[j.d.a.jewell@open.ac](j.d.a.jewell@open.ac).uk\> -:toc: :icons: font - -> [!TIP] -> **AI agents:** read `0-AI-MANIFEST.a2ml` first, then -> `.machine_readable/6a2/STATE.a2ml`. - -# What This Is - -`ideas-to-alphas` is the **incubator** of the hyperpolymath type theory -pipeline: the theory→practice stage where a finding from the **lab** -(`kategoria`) is matured from **idea to alpha** before it earns its own -production (typed) repo. - -> [!NOTE] -> This repo is mid-rename. The GitHub repo and local directory are still -> named `kategoria-pipeline` until the owner runs `gh` `repo` `rename` -> `ideas-to-alphas` (+ local `mv`). The role split — **lab** = -> `kategoria` (research/discovery), **incubator** = this repo -> (idea→alpha), **portal** = `nextgen-typing` (front-page on-ramp for -> people) — is captured in -> `dev-notes/2026-06-16-typing-sub-estate-roles-and-lifecycle.adoc`. -> Also update `project` `=` `"katagoria"` → `"ideas-to-alphas"` in -> `.machine_readable/6a2/STATE.a2ml` at rename time. - -# Pipeline Position - - katagoria → typell → typed-wasm → PanLL - (this repo) (kernel) (target) (eNSAID env) - -`katagoria` is upstream of everything. Ideas here are **speculative**: -proofs-of-concept, reading notes, prototype Idris2/Lean formalizations. -They graduate to `typell` when they are ready to be integrated into the -production verification kernel. - -Coordination monorepo: -[nextgen-typing](https://github.com/hyperpolymath/nextgen-typing) - -# What Lives Here - -- Type theory prototypes — Idris2, Lean 4, Agda proofs-of-concept - -- Research notes on papers being read and formalized - -- Experimental level definitions for the TypeLL open-ended progression - -- Speculative session type extensions (multi-party, probabilistic, - temporal) - -- Tropical type theory experiments (connections to protocol-squisher) - -# What Does NOT Live Here - -- Production Rust code — goes in `typell` - -- WasmGC type safety proofs — goes in `typed-wasm` - -- Anything with stability guarantees — this repo is deliberately - unstable - -# Relationship to TypeLL - -TypeLL is an **open-ended progressive** type safety framework. The -current L1-L10 implementation in typell was designed here first, then -graduated. Future levels (L11, L12, …) will originate here before -promotion. - -There is no fixed ceiling. katagoria is where the ceiling gets pushed. - -# Status - -Pre-alpha. Newly created (2026-04-11). Research artefacts will -accumulate over time. - -# License - -MPL-2.0 - -Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -\<[j.d.a.jewell@open.ac](j.d.a.jewell@open.ac).uk\> diff --git a/REQUIRES_INITIALISATION.adoc b/REQUIRES_INITIALISATION.adoc new file mode 100644 index 0000000..ea466a3 --- /dev/null +++ b/REQUIRES_INITIALISATION.adoc @@ -0,0 +1,289 @@ +== REQUIRES INITIALISATION + +*This repository is not finished being set up.* 25 substitution token(s) +across 21 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+` + +==== `+{{CONDUCT_TEAM}}+` + +Name of the conduct body. If there is no committee, rewrite the sentence +rather than substituting a plural noun into '`a \{\{CONDUCT_TEAM}} +member`'. + +Appears in: + +* `+.github/CODE_OF_CONDUCT.md+` + +==== `+{{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+` +* `+docs/developer/ABI-FFI-README.adoc+` + +==== `+{{MUST_INVARIANTS}}+` + +The invariants this project guarantees. Not answerable in a bootstrap; +it is the point of the repo. + +Appears in: + +* `+QUICKSTART-DEV.adoc+` + +==== `+{{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_DOMAIN}}+` + +Taxonomy value for the subject domain. + +Appears in: + +* `+.machine_readable/6a2/anchor/ANCHOR.a2ml+` + +==== `+{{PROJECT_KIND}}+` + +Taxonomy value (library, service, tool, lab…). + +Appears in: + +* `+.machine_readable/6a2/anchor/ANCHOR.a2ml+` + +==== `+{{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+` + +==== `+{{RESPONSE_TIME}}+` + +Initial-response SLA for a security or conduct report. Promise only what +a solo maintainer can actually meet. + +Appears in: + +* `+.github/CODE_OF_CONDUCT.md+` + +==== `+{{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 9ae3c20..0000000 --- a/REQUIRES_INITIALISATION.md +++ /dev/null @@ -1,274 +0,0 @@ - - -# REQUIRES INITIALISATION - -**This repository is not finished being set up.** 25 substitution token(s) across 21 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` - -### `{{CONDUCT_TEAM}}` - -Name of the conduct body. If there is no committee, rewrite the sentence rather than substituting a plural noun into 'a {{CONDUCT_TEAM}} member'. - -Appears in: - -- `.github/CODE_OF_CONDUCT.md` - -### `{{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` -- `docs/developer/ABI-FFI-README.adoc` - -### `{{MUST_INVARIANTS}}` - -The invariants this project guarantees. Not answerable in a bootstrap; it is the point of the repo. - -Appears in: - -- `QUICKSTART-DEV.adoc` - -### `{{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_DOMAIN}}` - -Taxonomy value for the subject domain. - -Appears in: - -- `.machine_readable/6a2/anchor/ANCHOR.a2ml` - -### `{{PROJECT_KIND}}` - -Taxonomy value (library, service, tool, lab…). - -Appears in: - -- `.machine_readable/6a2/anchor/ANCHOR.a2ml` - -### `{{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` - -### `{{RESPONSE_TIME}}` - -Initial-response SLA for a security or conduct report. Promise only what a solo maintainer can actually meet. - -Appears in: - -- `.github/CODE_OF_CONDUCT.md` - -### `{{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 5c4d5e9..0000000 --- a/SECURITY.md +++ /dev/null @@ -1,20 +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..10ff0af --- /dev/null +++ b/TEST-NEEDS.adoc @@ -0,0 +1,138 @@ +== 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 katagoria 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 +6759885+hyperpolymath@users.noreply.github.com +* *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 6c785bf..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 katagoria 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 <6759885+hyperpolymath@users.noreply.github.com> -- **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 61cdc22..0000000 --- a/TOPOLOGY.md +++ /dev/null @@ -1,33 +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..faf54f3 --- /dev/null +++ b/docs/tech-debt-2026-05-26.adoc @@ -0,0 +1,80 @@ +== Tech-Debt Audit — kategoria-pipeline — 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= 15 | Coq-Axm/Adm= 0 | Lean-srry/ax= 0 | Agda-pst= 0 | Idr-blv= 9 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0 +.... + +*Total markers:* 9. *Severity:* `+>09+`. + +*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 |63 +|`+docs/+` files |54 +|`+docs/+` LoC |2238 +|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 cc30d71..0000000 --- a/docs/tech-debt-2026-05-26.md +++ /dev/null @@ -1,71 +0,0 @@ - - -# Tech-Debt Audit — kategoria-pipeline — 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= 15 | Coq-Axm/Adm= 0 | Lean-srry/ax= 0 | Agda-pst= 0 | Idr-blv= 9 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0 -``` - -**Total markers:** 9. **Severity:** `>09`. - -**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 | 63 | -| `docs/` files | 54 | -| `docs/` LoC | 2238 | -| 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.