From 07d7553543c0ae3cff16fa1092055759a0a66d78 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 24 Aug 2026 08:49:52 +0100 Subject: [PATCH] refactor: migrate repository documentation from Markdown to AsciiDoc --- CHANGELOG.adoc | 9 + CHANGELOG.md | 11 - CODE_OF_CONDUCT.adoc | 338 +++++++++ CODE_OF_CONDUCT.md | 327 --------- CONTRIBUTING.adoc | 112 +++ CONTRIBUTING.md | 121 ---- GOVERNANCE.adoc | 177 +++++ GOVERNANCE.md | 158 ----- PLACEHOLDERS.adoc | 219 ++++++ PLACEHOLDERS.md | 141 ---- READINESS.adoc | 59 ++ READINESS.md | 55 -- SECURITY.adoc | 451 ++++++++++++ SECURITY.md | 406 ----------- archive/MAINTAINERS.adoc | 42 ++ archive/MAINTAINERS.md | 38 - docs/AI-CONVENTIONS.adoc | 99 +++ docs/AI-CONVENTIONS.md | 84 --- docs/QUICKSTART.adoc | 69 ++ docs/QUICKSTART.md | 64 -- docs/THREAT-MODEL.adoc | 254 +++++++ docs/THREAT-MODEL.md | 161 ----- docs/{TOPOLOGY.md => TOPOLOGY.adoc} | 45 +- docs/decisions/0000-template.adoc | 33 + docs/decisions/0000-template.md | 34 - docs/decisions/0001-adopt-rsr-standard.adoc | 94 +++ docs/decisions/0001-adopt-rsr-standard.md | 85 --- ...02-reversibility-as-typing-case-study.adoc | 189 +++++ ...0002-reversibility-as-typing-case-study.md | 182 ----- docs/decisions/README.adoc | 18 + docs/decisions/README.md | 16 - ...{ABI-FFI-README.md => ABI-FFI-README.adoc} | 240 ++++--- .../DESIGN-2026-03-01-typell-vision.adoc | 632 +++++++++++++++++ .../design/DESIGN-2026-03-01-typell-vision.md | 527 -------------- docs/maintenance/MAINTENANCE-CHECKLIST.adoc | 670 ++++++++++++++++++ docs/maintenance/MAINTENANCE-CHECKLIST.md | 568 --------------- docs/onboarding/llm-warmup-dev.adoc | 19 + docs/onboarding/llm-warmup-dev.md | 16 - docs/onboarding/llm-warmup-user.adoc | 19 + docs/onboarding/llm-warmup-user.md | 16 - docs/reports/audit/audit-2026-04-04.adoc | 86 +++ docs/reports/audit/audit-2026-04-04.md | 75 -- docs/status/PROOF-NEEDS.adoc | 50 ++ docs/status/PROOF-NEEDS.md | 42 -- docs/status/TEST-NEEDS.adoc | 88 +++ docs/status/TEST-NEEDS.md | 58 -- docs/status/UNIFIED-LEVELS.adoc | 57 ++ docs/status/UNIFIED-LEVELS.md | 57 -- docs/tech-debt-2026-05-26.adoc | 84 +++ docs/tech-debt-2026-05-26.md | 71 -- integrations/{README.md => README.adoc} | 23 +- spec/{README.md => README.adoc} | 35 +- src/abi/README.adoc | 83 +++ src/abi/README.md | 76 -- src/backends/README.adoc | 43 ++ src/backends/README.md | 44 -- src/kernel/{README.md => README.adoc} | 42 +- 57 files changed, 4199 insertions(+), 3613 deletions(-) create mode 100644 CHANGELOG.adoc delete mode 100644 CHANGELOG.md create mode 100644 CODE_OF_CONDUCT.adoc delete mode 100644 CODE_OF_CONDUCT.md create mode 100644 CONTRIBUTING.adoc delete mode 100644 CONTRIBUTING.md create mode 100644 GOVERNANCE.adoc delete mode 100644 GOVERNANCE.md create mode 100644 PLACEHOLDERS.adoc delete mode 100644 PLACEHOLDERS.md create mode 100644 READINESS.adoc delete mode 100644 READINESS.md create mode 100644 SECURITY.adoc delete mode 100644 SECURITY.md create mode 100644 archive/MAINTAINERS.adoc delete mode 100644 archive/MAINTAINERS.md create mode 100644 docs/AI-CONVENTIONS.adoc delete mode 100644 docs/AI-CONVENTIONS.md create mode 100644 docs/QUICKSTART.adoc delete mode 100644 docs/QUICKSTART.md create mode 100644 docs/THREAT-MODEL.adoc delete mode 100644 docs/THREAT-MODEL.md rename docs/{TOPOLOGY.md => TOPOLOGY.adoc} (95%) create mode 100644 docs/decisions/0000-template.adoc delete mode 100644 docs/decisions/0000-template.md create mode 100644 docs/decisions/0001-adopt-rsr-standard.adoc delete mode 100644 docs/decisions/0001-adopt-rsr-standard.md create mode 100644 docs/decisions/0002-reversibility-as-typing-case-study.adoc delete mode 100644 docs/decisions/0002-reversibility-as-typing-case-study.md create mode 100644 docs/decisions/README.adoc delete mode 100644 docs/decisions/README.md rename docs/design/{ABI-FFI-README.md => ABI-FFI-README.adoc} (74%) create mode 100644 docs/design/DESIGN-2026-03-01-typell-vision.adoc delete mode 100644 docs/design/DESIGN-2026-03-01-typell-vision.md create mode 100644 docs/maintenance/MAINTENANCE-CHECKLIST.adoc delete mode 100644 docs/maintenance/MAINTENANCE-CHECKLIST.md create mode 100644 docs/onboarding/llm-warmup-dev.adoc delete mode 100644 docs/onboarding/llm-warmup-dev.md create mode 100644 docs/onboarding/llm-warmup-user.adoc delete mode 100644 docs/onboarding/llm-warmup-user.md create mode 100644 docs/reports/audit/audit-2026-04-04.adoc delete mode 100644 docs/reports/audit/audit-2026-04-04.md create mode 100644 docs/status/PROOF-NEEDS.adoc delete mode 100644 docs/status/PROOF-NEEDS.md create mode 100644 docs/status/TEST-NEEDS.adoc delete mode 100644 docs/status/TEST-NEEDS.md create mode 100644 docs/status/UNIFIED-LEVELS.adoc delete mode 100644 docs/status/UNIFIED-LEVELS.md create mode 100644 docs/tech-debt-2026-05-26.adoc delete mode 100644 docs/tech-debt-2026-05-26.md rename integrations/{README.md => README.adoc} (70%) rename spec/{README.md => README.adoc} (55%) create mode 100644 src/abi/README.adoc delete mode 100644 src/abi/README.md create mode 100644 src/backends/README.adoc delete mode 100644 src/backends/README.md rename src/kernel/{README.md => README.adoc} (52%) 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 8109476..0000000 --- a/CHANGELOG.md +++ /dev/null @@ -1,11 +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..f9c930a --- /dev/null +++ b/CODE_OF_CONDUCT.adoc @@ -0,0 +1,338 @@ +== Code of Conduct + +=== Our Pledge + +We as members, contributors, and leaders pledge to make participation in +Typell a harassment-free experience for everyone, regardless of age, +body size, visible or invisible disability, ethnicity, sex +characteristics, gender identity and expression, level of experience, +education, socio-economic status, nationality, personal appearance, +race, caste, colour, religion, or sexual identity and orientation. + +We pledge to act and interact in ways that contribute to an open, +welcoming, diverse, inclusive, and healthy community. + +We recognise that a thriving open source community requires +*psychological safety* — an environment where people can contribute, ask +questions, make mistakes, and learn without fear of ridicule or +retaliation. + +''''' + +=== Our Standards + +==== Expected Behaviour + +The following behaviours contribute to a positive environment: + +*Communication* - Using welcoming and inclusive language - Being +respectful of differing viewpoints and experiences - Giving and +gracefully accepting constructive feedback - Assuming good intent while +addressing impact - Communicating clearly and patiently, especially with +newcomers + +*Collaboration* - Focusing on what is best for the community - Showing +empathy and kindness toward other community members - Being +collaborative rather than competitive - Mentoring and supporting less +experienced contributors - Celebrating others’ contributions and +successes + +*Professionalism* - Accepting responsibility and apologising to those +affected by our mistakes - Learning from the experience and avoiding +repetition - Respecting others’ time and attention - Staying on topic in +project spaces - Following project guidelines and conventions + +*Accessibility* - Using plain language and avoiding unnecessary jargon - +Providing alt text for images and transcripts for audio/video - Being +patient with those using assistive technologies - Accommodating +different communication styles and needs - Recognising that not everyone +communicates the same way + +==== Unacceptable Behaviour + +The following behaviours are considered harassment and are unacceptable: + +*Harassment* - The use of sexualised language or imagery, and sexual +attention or advances of any kind - Trolling, insulting or derogatory +comments, and personal or political attacks - Public or private +harassment - Deliberate intimidation, stalking, or following (online or +in-person) - Unwelcome physical contact or simulated physical contact +(e.g., emoji) - Sustained disruption of talks, events, or online +discussions + +*Discrimination* - Discriminatory jokes and language - Posting or +threatening to post others’ personally identifying information +("`doxing`") - Advocating for, or encouraging, any of the above +behaviour - Microaggressions — subtle, often unintentional, +discriminatory comments or actions + +*Professional Misconduct* - Publishing others’ private information +without explicit permission - Misrepresenting affiliation or +contributions - Plagiarism or claiming credit for others’ work - +Retaliating against anyone who reports a Code of Conduct violation - +Other conduct which could reasonably be considered inappropriate in a +professional setting + +==== Grey Areas + +Some situations require judgement. When uncertain: + +* *Intent vs Impact*: Good intentions do not excuse harmful impact. +Focus on making things right. +* *Power Dynamics*: Those with more power (maintainers, employers, +experienced contributors) must be especially mindful of their impact. +* *Cultural Differences*: What’s acceptable varies by culture. When in +doubt, err on the side of caution and ask. +* *Humour*: Jokes at others’ expense are rarely funny to everyone. Punch +up, not down. + +''''' + +=== Scope + +This Code of Conduct applies within all community spaces, including: + +*Online Spaces* - Repository discussions, issues, and pull/merge +requests - Project chat channels (Matrix, Discord, Slack, IRC) - Mailing +lists and forums - Social media when representing the project - Video +calls and virtual meetings + +*In-Person Spaces* - Conferences, meetups, and events - Workshops and +training sessions - Any gathering where you represent the project + +*Representation* This Code of Conduct also applies when an individual is +officially representing the community in public spaces. Examples +include: + +* Using an official project email address +* Posting via an official social media account +* Acting as an appointed representative at an event +* Speaking on behalf of the project + +''''' + +=== Enforcement + +==== Reporting + +If you experience or witness unacceptable behaviour, or have any other +concerns, please report it as soon as possible. + +*How to Report* + +[width="99%",cols="30%,33%,37%",options="header",] +|=== +|Method |Details |Best For +|*Email* |j.d.a.jewell@open.ac.uk |Detailed reports, sensitive matters + +|*Private Message* |Contact any maintainer directly |Quick questions, +minor issues + +|*Anonymous Form* |[Link to form if available] |When you need anonymity +|=== + +*What to Include* + +* Your contact information (unless anonymous) +* Names/usernames of those involved +* Description of what happened +* When and where it occurred +* Any witnesses +* Any supporting evidence (screenshots, links) +* How you would like us to respond (if you have a preference) + +*What Happens Next* + +[arabic] +. You will receive acknowledgment within *48 hours* +. The Typell Maintainers will review the report +. We may ask for additional information +. We will determine appropriate action +. We will inform you of the outcome (respecting others’ privacy) + +==== Confidentiality + +All reports will be handled with discretion: + +* Reporter identity is protected by default +* Details are shared only with those who need to know +* We will ask before naming you in any communication +* Anonymous reports are accepted and investigated + +==== Conflicts of Interest + +If a Typell Maintainers member is involved in an incident: + +* They will recuse themselves from the process +* Another maintainer or external party will handle the report +* We will disclose any potential conflicts + +''''' + +=== Enforcement Guidelines + +The Typell Maintainers will follow these guidelines in determining +consequences: + +==== 1. Correction + +*Community Impact*: Use of inappropriate language or other behaviour +deemed unprofessional or unwelcome. + +*Consequence*: A private, written warning providing clarity around the +nature of the violation and an explanation of why the behaviour was +inappropriate. A public apology may be requested. + +*Duration*: Immediate + +==== 2. Warning + +*Community Impact*: A violation through a single incident or series of +actions. + +*Consequence*: A warning with consequences for continued behaviour. No +interaction with the people involved, including unsolicited interaction +with those enforcing the Code of Conduct, for a specified period. This +includes avoiding interactions in community spaces as well as external +channels like social media. Violating these terms may lead to a +temporary or permanent ban. + +*Duration*: 1-4 weeks + +==== 3. Temporary Ban + +*Community Impact*: A serious violation of community standards, +including sustained inappropriate behaviour. + +*Consequence*: A temporary ban from any sort of interaction or public +communication with the community for a specified period. No public or +private interaction with the people involved, including unsolicited +interaction with those enforcing the Code of Conduct, is allowed during +this period. Violating these terms may lead to a permanent ban. + +*Duration*: 1-6 months + +==== 4. Permanent Ban + +*Community Impact*: Demonstrating a pattern of violation of community +standards, including sustained inappropriate behaviour, harassment of an +individual, or aggression toward or disparagement of classes of +individuals. + +*Consequence*: A permanent ban from any sort of public interaction +within the community. + +*Duration*: Permanent (with appeal rights after 12 months) + +==== Enforcement Across Perimeters + +For contributors with elevated access (Perimeter 2 or 1): + +[cols=",",options="header",] +|=== +|Level |Additional Consequence +|Correction |Noted in contributor record +|Warning |Access privileges may be temporarily reduced +|Temporary Ban |Access reduced to Perimeter 3 for ban duration +|Permanent Ban |All access revoked +|=== + +''''' + +=== Appeals + +If you believe an enforcement decision was made in error: + +[arabic] +. *Wait 7 days* after the decision (cooling-off period) +. *Email* j.d.a.jewell@open.ac.uk with subject line "`Appeal: [Original +Report ID]`" +. *Explain* why you believe the decision should be reconsidered +. *Provide* any new information not previously available + +*Appeals Process* + +* Appeals are reviewed by a different Typell Maintainers member than the +original +* You will receive a response within 14 days +* The appeals decision is final +* You may only appeal once per incident + +*Grounds for Appeal* + +* Procedural errors in the original investigation +* New evidence not previously available +* Disproportionate response to the violation +* Misunderstanding of facts + +''''' + +=== Supporting Those Who Report + +We are committed to supporting those who report violations: + +*We Will* - Believe and take all reports seriously - Respect your +privacy and confidentiality preferences - Keep you informed of progress +(if you wish) - Take steps to protect you from retaliation - Provide +resources if you need support + +*We Will Not* - Require you to confront the person directly - Dismiss +reports without investigation - Reveal your identity without consent - +Tolerate retaliation against reporters - Rush you to make decisions + +''''' + +=== Prevention + +Beyond enforcement, we actively work to prevent issues: + +*Onboarding* - All contributors are expected to read this Code of +Conduct - Perimeter 2 applicants must confirm they’ve read and +understood it - Maintainers receive additional training on enforcement + +*Culture* - We model the behaviour we expect - We intervene early when +we see potential issues - We thank people for positive contributions - +We create opportunities for diverse voices + +*Review* - This Code of Conduct is reviewed annually - Community +feedback is welcomed - Changes are communicated clearly + +''''' + +=== Acknowledgments + +This Code of Conduct is adapted from: + +* https://www.contributor-covenant.org/[Contributor Covenant], version +2.1 +* https://www.djangoproject.com/conduct/[Django Code of Conduct] +* https://www.rust-lang.org/policies/code-of-conduct[Rust Code of +Conduct] +* https://www.python.org/psf/conduct/[Python Community Code of Conduct] + +We thank these communities for their leadership in creating welcoming +spaces. + +''''' + +=== Questions? + +If you have questions about this Code of Conduct: + +* Open a https://github.com/hyperpolymath/typell/discussions[Discussion] +(for general questions) +* Email j.d.a.jewell@open.ac.uk (for private questions) +* Contact any maintainer directly + +''''' + +=== Summary + +*Be kind. Be respectful. Be collaborative.* + +We’re all here because we care about this project. Let’s make it a place +where everyone can do their best work. + +''''' + +Last updated: 2026 · Based on Contributor Covenant 2.1 diff --git a/CODE_OF_CONDUCT.md b/CODE_OF_CONDUCT.md deleted file mode 100644 index 0643584..0000000 --- a/CODE_OF_CONDUCT.md +++ /dev/null @@ -1,327 +0,0 @@ -# Code of Conduct - - - -## Our Pledge - -We as members, contributors, and leaders pledge to make participation in Typell a harassment-free experience for everyone, regardless of age, body size, visible or invisible disability, ethnicity, sex characteristics, gender identity and expression, level of experience, education, socio-economic status, nationality, personal appearance, race, caste, colour, religion, or sexual identity and orientation. - -We pledge to act and interact in ways that contribute to an open, welcoming, diverse, inclusive, and healthy community. - -We recognise that a thriving open source community requires **psychological safety** — an environment where people can contribute, ask questions, make mistakes, and learn without fear of ridicule or retaliation. - ---- - -## Our Standards - -### Expected Behaviour - -The following behaviours contribute to a positive environment: - -**Communication** -- Using welcoming and inclusive language -- Being respectful of differing viewpoints and experiences -- Giving and gracefully accepting constructive feedback -- Assuming good intent while addressing impact -- Communicating clearly and patiently, especially with newcomers - -**Collaboration** -- Focusing on what is best for the community -- Showing empathy and kindness toward other community members -- Being collaborative rather than competitive -- Mentoring and supporting less experienced contributors -- Celebrating others' contributions and successes - -**Professionalism** -- Accepting responsibility and apologising to those affected by our mistakes -- Learning from the experience and avoiding repetition -- Respecting others' time and attention -- Staying on topic in project spaces -- Following project guidelines and conventions - -**Accessibility** -- Using plain language and avoiding unnecessary jargon -- Providing alt text for images and transcripts for audio/video -- Being patient with those using assistive technologies -- Accommodating different communication styles and needs -- Recognising that not everyone communicates the same way - -### Unacceptable Behaviour - -The following behaviours are considered harassment and are unacceptable: - -**Harassment** -- The use of sexualised language or imagery, and sexual attention or advances of any kind -- Trolling, insulting or derogatory comments, and personal or political attacks -- Public or private harassment -- Deliberate intimidation, stalking, or following (online or in-person) -- Unwelcome physical contact or simulated physical contact (e.g., emoji) -- Sustained disruption of talks, events, or online discussions - -**Discrimination** -- Discriminatory jokes and language -- Posting or threatening to post others' personally identifying information ("doxing") -- Advocating for, or encouraging, any of the above behaviour -- Microaggressions — subtle, often unintentional, discriminatory comments or actions - -**Professional Misconduct** -- Publishing others' private information without explicit permission -- Misrepresenting affiliation or contributions -- Plagiarism or claiming credit for others' work -- Retaliating against anyone who reports a Code of Conduct violation -- Other conduct which could reasonably be considered inappropriate in a professional setting - -### Grey Areas - -Some situations require judgement. When uncertain: - -- **Intent vs Impact**: Good intentions do not excuse harmful impact. Focus on making things right. -- **Power Dynamics**: Those with more power (maintainers, employers, experienced contributors) must be especially mindful of their impact. -- **Cultural Differences**: What's acceptable varies by culture. When in doubt, err on the side of caution and ask. -- **Humour**: Jokes at others' expense are rarely funny to everyone. Punch up, not down. - ---- - -## Scope - -This Code of Conduct applies within all community spaces, including: - -**Online Spaces** -- Repository discussions, issues, and pull/merge requests -- Project chat channels (Matrix, Discord, Slack, IRC) -- Mailing lists and forums -- Social media when representing the project -- Video calls and virtual meetings - -**In-Person Spaces** -- Conferences, meetups, and events -- Workshops and training sessions -- Any gathering where you represent the project - -**Representation** -This Code of Conduct also applies when an individual is officially representing the community in public spaces. Examples include: - -- Using an official project email address -- Posting via an official social media account -- Acting as an appointed representative at an event -- Speaking on behalf of the project - ---- - -## Enforcement - -### Reporting - -If you experience or witness unacceptable behaviour, or have any other concerns, please report it as soon as possible. - -**How to Report** - -| Method | Details | Best For | -|--------|---------|----------| -| **Email** | j.d.a.jewell@open.ac.uk | Detailed reports, sensitive matters | -| **Private Message** | Contact any maintainer directly | Quick questions, minor issues | -| **Anonymous Form** | [Link to form if available] | When you need anonymity | - -**What to Include** - -- Your contact information (unless anonymous) -- Names/usernames of those involved -- Description of what happened -- When and where it occurred -- Any witnesses -- Any supporting evidence (screenshots, links) -- How you would like us to respond (if you have a preference) - -**What Happens Next** - -1. You will receive acknowledgment within **48 hours** -2. The Typell Maintainers will review the report -3. We may ask for additional information -4. We will determine appropriate action -5. We will inform you of the outcome (respecting others' privacy) - -### Confidentiality - -All reports will be handled with discretion: - -- Reporter identity is protected by default -- Details are shared only with those who need to know -- We will ask before naming you in any communication -- Anonymous reports are accepted and investigated - -### Conflicts of Interest - -If a Typell Maintainers member is involved in an incident: - -- They will recuse themselves from the process -- Another maintainer or external party will handle the report -- We will disclose any potential conflicts - ---- - -## Enforcement Guidelines - -The Typell Maintainers will follow these guidelines in determining consequences: - -### 1. Correction - -**Community Impact**: Use of inappropriate language or other behaviour deemed unprofessional or unwelcome. - -**Consequence**: A private, written warning providing clarity around the nature of the violation and an explanation of why the behaviour was inappropriate. A public apology may be requested. - -**Duration**: Immediate - -### 2. Warning - -**Community Impact**: A violation through a single incident or series of actions. - -**Consequence**: A warning with consequences for continued behaviour. No interaction with the people involved, including unsolicited interaction with those enforcing the Code of Conduct, for a specified period. This includes avoiding interactions in community spaces as well as external channels like social media. Violating these terms may lead to a temporary or permanent ban. - -**Duration**: 1-4 weeks - -### 3. Temporary Ban - -**Community Impact**: A serious violation of community standards, including sustained inappropriate behaviour. - -**Consequence**: A temporary ban from any sort of interaction or public communication with the community for a specified period. No public or private interaction with the people involved, including unsolicited interaction with those enforcing the Code of Conduct, is allowed during this period. Violating these terms may lead to a permanent ban. - -**Duration**: 1-6 months - -### 4. Permanent Ban - -**Community Impact**: Demonstrating a pattern of violation of community standards, including sustained inappropriate behaviour, harassment of an individual, or aggression toward or disparagement of classes of individuals. - -**Consequence**: A permanent ban from any sort of public interaction within the community. - -**Duration**: Permanent (with appeal rights after 12 months) - -### Enforcement Across Perimeters - -For contributors with elevated access (Perimeter 2 or 1): - -| Level | Additional Consequence | -|-------|----------------------| -| Correction | Noted in contributor record | -| Warning | Access privileges may be temporarily reduced | -| Temporary Ban | Access reduced to Perimeter 3 for ban duration | -| Permanent Ban | All access revoked | - ---- - -## Appeals - -If you believe an enforcement decision was made in error: - -1. **Wait 7 days** after the decision (cooling-off period) -2. **Email** j.d.a.jewell@open.ac.uk with subject line "Appeal: [Original Report ID]" -3. **Explain** why you believe the decision should be reconsidered -4. **Provide** any new information not previously available - -**Appeals Process** - -- Appeals are reviewed by a different Typell Maintainers member than the original -- You will receive a response within 14 days -- The appeals decision is final -- You may only appeal once per incident - -**Grounds for Appeal** - -- Procedural errors in the original investigation -- New evidence not previously available -- Disproportionate response to the violation -- Misunderstanding of facts - ---- - -## Supporting Those Who Report - -We are committed to supporting those who report violations: - -**We Will** -- Believe and take all reports seriously -- Respect your privacy and confidentiality preferences -- Keep you informed of progress (if you wish) -- Take steps to protect you from retaliation -- Provide resources if you need support - -**We Will Not** -- Require you to confront the person directly -- Dismiss reports without investigation -- Reveal your identity without consent -- Tolerate retaliation against reporters -- Rush you to make decisions - ---- - -## Prevention - -Beyond enforcement, we actively work to prevent issues: - -**Onboarding** -- All contributors are expected to read this Code of Conduct -- Perimeter 2 applicants must confirm they've read and understood it -- Maintainers receive additional training on enforcement - -**Culture** -- We model the behaviour we expect -- We intervene early when we see potential issues -- We thank people for positive contributions -- We create opportunities for diverse voices - -**Review** -- This Code of Conduct is reviewed annually -- Community feedback is welcomed -- Changes are communicated clearly - ---- - -## Acknowledgments - -This Code of Conduct is adapted from: - -- [Contributor Covenant](https://www.contributor-covenant.org/), version 2.1 -- [Django Code of Conduct](https://www.djangoproject.com/conduct/) -- [Rust Code of Conduct](https://www.rust-lang.org/policies/code-of-conduct) -- [Python Community Code of Conduct](https://www.python.org/psf/conduct/) - -We thank these communities for their leadership in creating welcoming spaces. - ---- - -## Questions? - -If you have questions about this Code of Conduct: - -- Open a [Discussion](https://github.com/hyperpolymath/typell/discussions) (for general questions) -- Email j.d.a.jewell@open.ac.uk (for private questions) -- Contact any maintainer directly - ---- - -## Summary - -**Be kind. Be respectful. Be collaborative.** - -We're all here because we care about this project. Let's make it a place where everyone can do their best work. - ---- - -Last updated: 2026 · Based on Contributor Covenant 2.1 diff --git a/CONTRIBUTING.adoc b/CONTRIBUTING.adoc new file mode 100644 index 0000000..3ddff7e --- /dev/null +++ b/CONTRIBUTING.adoc @@ -0,0 +1,112 @@ +== Clone the repository + +git clone https://github.com/hyperpolymath/typell.git cd typell + +== Using Nix (recommended for reproducibility) + +nix develop + +== Or using toolbox/distrobox + +toolbox create typell-dev toolbox enter typell-dev # Install +dependencies manually + +== Verify setup + +just check # or: cargo check / mix compile / etc. just test # Run test +suite + +.... + +### Repository Structure +.... + +typell/ ├── src/ # Source code (Perimeter 1-2) ├── lib/ # Library code +(Perimeter 1-2) ├── extensions/ # Extensions (Perimeter 2) ├── plugins/ +# Plugins (Perimeter 2) ├── tools/ # Tooling (Perimeter 2) ├── docs/ # +Documentation (Perimeter 3) │ ├── architecture/ # ADRs, specs (Perimeter +2) │ └── proposals/ # RFCs (Perimeter 3) ├── examples/ # Examples +(Perimeter 3) ├── spec/ # Spec tests (Perimeter 3) ├── tests/ # Test +suite (Perimeter 2-3) ├── .machine_readable/ # ALL machine-readable +content (Perimeter 1) │ ├── *.a2ml # State files (STATE, META, +ECOSYSTEM, etc.) │ ├── bot_directives/ # Bot configs │ └── contractiles/ +# Policy contracts (k9, dust, lust, must, trust) ├── .well-known/ # +Protocol files (Perimeter 1-3) ├── .github/ # GitHub config (Perimeter +1) │ ├── ISSUE_TEMPLATE/ │ └── workflows/ ├── CHANGELOG.md ├── +CODE_OF_CONDUCT.md ├── CONTRIBUTING.md # This file ├── GOVERNANCE.md ├── +LICENSE ├── MAINTAINERS.adoc ├── README.adoc ├── SECURITY.md ├── +flake.nix # Nix flake — fallback (Perimeter 1) ├── guix.scm # Guix +package — primary (Perimeter 1) └── Justfile # Task runner (Perimeter 1) + +.... + +--- + +## How to Contribute + +### Reporting Bugs + +**Before reporting**: +1. Search existing issues +2. Check if it's already fixed in `main` +3. Determine which perimeter the bug affects + +**When reporting**: + +Use the [bug report template](.github/ISSUE_TEMPLATE/bug_report.md) and include: + +- Clear, descriptive title +- Environment details (OS, versions, toolchain) +- Steps to reproduce +- Expected vs actual behaviour +- Logs, screenshots, or minimal reproduction + +### Suggesting Features + +**Before suggesting**: +1. Check the [roadmap](ROADMAP.md) if available +2. Search existing issues and discussions +3. Consider which perimeter the feature belongs to + +**When suggesting**: + +Use the [feature request template](.github/ISSUE_TEMPLATE/feature_request.md) and include: + +- Problem statement (what pain point does this solve?) +- Proposed solution +- Alternatives considered +- Which perimeter this affects + +### Your First Contribution + +Look for issues labelled: + +- [`good first issue`](https://github.com/hyperpolymath/typell/labels/good%20first%20issue) — Simple Perimeter 3 tasks +- [`help wanted`](https://github.com/hyperpolymath/typell/labels/help%20wanted) — Community help needed +- [`documentation`](https://github.com/hyperpolymath/typell/labels/documentation) — Docs improvements +- [`perimeter-3`](https://github.com/hyperpolymath/typell/labels/perimeter-3) — Community sandbox scope + +--- + +## Development Workflow + +### Branch Naming +.... + +docs/short-description # Documentation (P3) test/what-added # Test +additions (P3) feat/short-description # New features (P2) +fix/issue-number-description # Bug fixes (P2) refactor/what-changed # +Code improvements (P2) security/what-fixed # Security fixes (P1-2) + +.... + +### Commit Messages + +We follow [Conventional Commits](https://www.conventionalcommits.org/): +.... + +(): + +{empty}[optional body] + +{empty}[optional footer] diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md deleted file mode 100644 index 6899990..0000000 --- a/CONTRIBUTING.md +++ /dev/null @@ -1,121 +0,0 @@ -# Clone the repository -git clone https://github.com/hyperpolymath/typell.git -cd typell - -# Using Nix (recommended for reproducibility) -nix develop - -# Or using toolbox/distrobox -toolbox create typell-dev -toolbox enter typell-dev -# Install dependencies manually - -# Verify setup -just check # or: cargo check / mix compile / etc. -just test # Run test suite -``` - -### Repository Structure -``` -typell/ -├── src/ # Source code (Perimeter 1-2) -├── lib/ # Library code (Perimeter 1-2) -├── extensions/ # Extensions (Perimeter 2) -├── plugins/ # Plugins (Perimeter 2) -├── tools/ # Tooling (Perimeter 2) -├── docs/ # Documentation (Perimeter 3) -│ ├── architecture/ # ADRs, specs (Perimeter 2) -│ └── proposals/ # RFCs (Perimeter 3) -├── examples/ # Examples (Perimeter 3) -├── spec/ # Spec tests (Perimeter 3) -├── tests/ # Test suite (Perimeter 2-3) -├── .machine_readable/ # ALL machine-readable content (Perimeter 1) -│ ├── *.a2ml # State files (STATE, META, ECOSYSTEM, etc.) -│ ├── bot_directives/ # Bot configs -│ └── contractiles/ # Policy contracts (k9, dust, lust, must, trust) -├── .well-known/ # Protocol files (Perimeter 1-3) -├── .github/ # GitHub config (Perimeter 1) -│ ├── ISSUE_TEMPLATE/ -│ └── workflows/ -├── CHANGELOG.md -├── CODE_OF_CONDUCT.md -├── CONTRIBUTING.md # This file -├── GOVERNANCE.md -├── LICENSE -├── MAINTAINERS.adoc -├── README.adoc -├── SECURITY.md -├── flake.nix # Nix flake — fallback (Perimeter 1) -├── guix.scm # Guix package — primary (Perimeter 1) -└── Justfile # Task runner (Perimeter 1) -``` - ---- - -## How to Contribute - -### Reporting Bugs - -**Before reporting**: -1. Search existing issues -2. Check if it's already fixed in `main` -3. Determine which perimeter the bug affects - -**When reporting**: - -Use the [bug report template](.github/ISSUE_TEMPLATE/bug_report.md) and include: - -- Clear, descriptive title -- Environment details (OS, versions, toolchain) -- Steps to reproduce -- Expected vs actual behaviour -- Logs, screenshots, or minimal reproduction - -### Suggesting Features - -**Before suggesting**: -1. Check the [roadmap](ROADMAP.md) if available -2. Search existing issues and discussions -3. Consider which perimeter the feature belongs to - -**When suggesting**: - -Use the [feature request template](.github/ISSUE_TEMPLATE/feature_request.md) and include: - -- Problem statement (what pain point does this solve?) -- Proposed solution -- Alternatives considered -- Which perimeter this affects - -### Your First Contribution - -Look for issues labelled: - -- [`good first issue`](https://github.com/hyperpolymath/typell/labels/good%20first%20issue) — Simple Perimeter 3 tasks -- [`help wanted`](https://github.com/hyperpolymath/typell/labels/help%20wanted) — Community help needed -- [`documentation`](https://github.com/hyperpolymath/typell/labels/documentation) — Docs improvements -- [`perimeter-3`](https://github.com/hyperpolymath/typell/labels/perimeter-3) — Community sandbox scope - ---- - -## Development Workflow - -### Branch Naming -``` -docs/short-description # Documentation (P3) -test/what-added # Test additions (P3) -feat/short-description # New features (P2) -fix/issue-number-description # Bug fixes (P2) -refactor/what-changed # Code improvements (P2) -security/what-fixed # Security fixes (P1-2) -``` - -### Commit Messages - -We follow [Conventional Commits](https://www.conventionalcommits.org/): -``` -(): - -[optional body] - -[optional footer] diff --git a/GOVERNANCE.adoc b/GOVERNANCE.adoc new file mode 100644 index 0000000..58f1228 --- /dev/null +++ b/GOVERNANCE.adoc @@ -0,0 +1,177 @@ +== Project Governance + +This document describes the governance model for *Typell*. + +''''' + +=== Project Governance Model + +Typell follows a *Benevolent Dictator For Life (BDFL)* governance model. +This model is well-suited for solo maintainers and small project teams +where rapid, consistent decision-making is more valuable than formal +consensus processes. + +The BDFL has final authority on all project decisions, including +technical direction, release schedules, contributor access, and +community standards. + +____ +*Transition clause:* When the core team exceeds three active +maintainers, this project should transition to a *consensus-based +governance model* with documented voting procedures. That transition +should itself be recorded as an Architecture Decision Record (ADR) in +`+docs/decisions/+`. +____ + +''''' + +=== Decision Making + +==== Day-to-day decisions + +* The BDFL makes final decisions on all matters. +* Routine decisions (bug fixes, dependency updates, minor improvements) +may be made by any maintainer with commit access. +* Maintainers are expected to use good judgement and seek input on +non-trivial changes. + +==== Proposing changes + +* Contributors can propose changes by opening issues or pull requests. +* Significant changes (new features, breaking changes, architectural +shifts) should be discussed in an issue before implementation begins. +* The BDFL will provide a clear accept/reject decision with reasoning. + +==== Architecture Decision Records (ADRs) + +* Significant technical decisions are documented as ADRs in +`+docs/decisions/+`. +* ADR statuses: `+proposed+`, `+accepted+`, `+deprecated+`, +`+superseded+`, `+rejected+`. +* ADRs provide a historical record of why decisions were made and what +alternatives were considered. +* See `+.machine_readable/META.a2ml+` for the machine-readable ADR +index. + +''''' + +=== Roles + +==== BDFL (Benevolent Dictator For Life) + +* The project creator and ultimate decision-maker. +* Sets the project’s technical direction and long-term vision. +* Has final say on all matters, including maintainer appointments and +removals. +* Responsible for ensuring the project adheres to RSR standards. + +==== Maintainer + +* Has commit access to the repository. +* Reviews and merges pull requests. +* Triages issues and manages releases. +* Upholds code quality, security standards, and the Code of Conduct. +* Listed in MAINTAINERS.adoc. + +==== Contributor + +* Anyone who submits pull requests, opens issues, or participates in +discussions. +* Does not have direct commit access. +* Contributions are reviewed by maintainers before merging. +* All contributors must follow the link:CODE_OF_CONDUCT.md[Code of +Conduct]. + +==== Bot + +* Automated agents managed via your bot orchestration system. +* Perform automated code review, security scanning, dependency updates, +and standards enforcement. +* Bot actions are subject to the same quality and review standards as +human contributions. +* Configure your bots in `+.machine_readable/bot_directives/+`. + +''''' + +=== Becoming a Maintainer + +A contributor may be nominated to become a maintainer when they +demonstrate: + +[arabic] +. *Sustained quality contributions* – a track record of well-crafted +pull requests that follow project conventions and require minimal +revision. +. *Understanding of RSR standards* – familiarity with the Repository +Structure Requirements, security policies, and CI/CD workflows used +across the project. +. *Constructive participation* – helpful issue triage, thoughtful code +review comments, and mentoring of other contributors. +. *Reliability* – consistent engagement over a meaningful period +(typically 3+ months of active contribution). + +==== Process + +[arabic] +. An existing maintainer nominates the candidate by opening a private +discussion with the BDFL. +. The BDFL reviews the candidate’s contribution history and community +interactions. +. The BDFL approves or declines the nomination, with reasoning provided +to the nominator. +. If approved, the new maintainer is added to MAINTAINERS.adoc and +granted appropriate repository access. + +''''' + +=== Removing a Maintainer + +A maintainer may be removed under the following circumstances: + +* *Inactivity*: No meaningful contributions or reviews for 12 or more +consecutive months. The maintainer will be contacted before removal and +offered the option to move to emeritus status voluntarily. +* *Code of Conduct violation*: Behaviour that violates the +link:CODE_OF_CONDUCT.md[Code of Conduct], as determined through the +enforcement process described therein. +* *BDFL discretion*: The BDFL may remove a maintainer for other reasons +(e.g., repeated disregard for project standards, loss of trust). +Reasoning will be documented privately. + +Removed maintainers are moved to the Emeritus section of +MAINTAINERS.adoc unless removal was due to a serious Code of Conduct +violation. + +''''' + +=== Code of Conduct + +All participants in this project are expected to follow the +link:CODE_OF_CONDUCT.md[Code of Conduct]. The Code of Conduct applies to +all project spaces, including issues, pull requests, discussions, and +any forum where the project is represented. + +Enforcement of the Code of Conduct is described in that document. The +BDFL serves as the final arbiter in conduct disputes. + +''''' + +=== Amendments + +This governance document may be amended by the BDFL at any time. All +amendments will be: + +[arabic] +. Documented as an ADR in `+docs/decisions/+` explaining the rationale +for the change. +. Committed to the repository with a clear commit message. +. Communicated to existing maintainers and contributors via the +project’s usual channels. + +Substantive changes (e.g., changing the governance model itself) should +be discussed with the community before adoption, even though the BDFL +retains final authority. + +''''' + +Copyright (c) 2026 hyperpolymath. Licensed under MPL-2.0. diff --git a/GOVERNANCE.md b/GOVERNANCE.md deleted file mode 100644 index aa93d75..0000000 --- a/GOVERNANCE.md +++ /dev/null @@ -1,158 +0,0 @@ - - -# Project Governance - -This document describes the governance model for **Typell**. - ---- - -## Project Governance Model - -Typell follows a **Benevolent Dictator For Life (BDFL)** governance model. -This model is well-suited for solo maintainers and small project teams where rapid, -consistent decision-making is more valuable than formal consensus processes. - -The BDFL has final authority on all project decisions, including technical direction, -release schedules, contributor access, and community standards. - -> **Transition clause:** When the core team exceeds three active maintainers, this -> project should transition to a **consensus-based governance model** with documented -> voting procedures. That transition should itself be recorded as an Architecture -> Decision Record (ADR) in `docs/decisions/`. - ---- - -## Decision Making - -### Day-to-day decisions - -- The BDFL makes final decisions on all matters. -- Routine decisions (bug fixes, dependency updates, minor improvements) may be made - by any maintainer with commit access. -- Maintainers are expected to use good judgement and seek input on non-trivial changes. - -### Proposing changes - -- Contributors can propose changes by opening issues or pull requests. -- Significant changes (new features, breaking changes, architectural shifts) should - be discussed in an issue before implementation begins. -- The BDFL will provide a clear accept/reject decision with reasoning. - -### Architecture Decision Records (ADRs) - -- Significant technical decisions are documented as ADRs in `docs/decisions/`. -- ADR statuses: `proposed`, `accepted`, `deprecated`, `superseded`, `rejected`. -- ADRs provide a historical record of why decisions were made and what alternatives - were considered. -- See `.machine_readable/META.a2ml` for the machine-readable ADR index. - ---- - -## Roles - -### BDFL (Benevolent Dictator For Life) - -- The project creator and ultimate decision-maker. -- Sets the project's technical direction and long-term vision. -- Has final say on all matters, including maintainer appointments and removals. -- Responsible for ensuring the project adheres to RSR standards. - -### Maintainer - -- Has commit access to the repository. -- Reviews and merges pull requests. -- Triages issues and manages releases. -- Upholds code quality, security standards, and the Code of Conduct. -- Listed in [MAINTAINERS.adoc](MAINTAINERS.adoc). - -### Contributor - -- Anyone who submits pull requests, opens issues, or participates in discussions. -- Does not have direct commit access. -- Contributions are reviewed by maintainers before merging. -- All contributors must follow the [Code of Conduct](CODE_OF_CONDUCT.md). - -### Bot - -- Automated agents managed via your bot orchestration system. -- Perform automated code review, security scanning, dependency updates, and - standards enforcement. -- Bot actions are subject to the same quality and review standards as human - contributions. -- Configure your bots in `.machine_readable/bot_directives/`. - ---- - -## Becoming a Maintainer - -A contributor may be nominated to become a maintainer when they demonstrate: - -1. **Sustained quality contributions** -- a track record of well-crafted pull requests - that follow project conventions and require minimal revision. -2. **Understanding of RSR standards** -- familiarity with the Repository Structure - Requirements, security policies, and CI/CD workflows used across the project. -3. **Constructive participation** -- helpful issue triage, thoughtful code review - comments, and mentoring of other contributors. -4. **Reliability** -- consistent engagement over a meaningful period (typically 3+ - months of active contribution). - -### Process - -1. An existing maintainer nominates the candidate by opening a private discussion - with the BDFL. -2. The BDFL reviews the candidate's contribution history and community interactions. -3. The BDFL approves or declines the nomination, with reasoning provided to the - nominator. -4. If approved, the new maintainer is added to [MAINTAINERS.adoc](MAINTAINERS.adoc) and - granted appropriate repository access. - ---- - -## Removing a Maintainer - -A maintainer may be removed under the following circumstances: - -- **Inactivity**: No meaningful contributions or reviews for 12 or more consecutive - months. The maintainer will be contacted before removal and offered the option to - move to emeritus status voluntarily. -- **Code of Conduct violation**: Behaviour that violates the - [Code of Conduct](CODE_OF_CONDUCT.md), as determined through the enforcement - process described therein. -- **BDFL discretion**: The BDFL may remove a maintainer for other reasons (e.g., - repeated disregard for project standards, loss of trust). Reasoning will be - documented privately. - -Removed maintainers are moved to the Emeritus section of -[MAINTAINERS.adoc](MAINTAINERS.adoc) unless removal was due to a serious Code of Conduct -violation. - ---- - -## Code of Conduct - -All participants in this project are expected to follow the -[Code of Conduct](CODE_OF_CONDUCT.md). The Code of Conduct applies to all project -spaces, including issues, pull requests, discussions, and any forum where the project -is represented. - -Enforcement of the Code of Conduct is described in that document. The BDFL serves as -the final arbiter in conduct disputes. - ---- - -## Amendments - -This governance document may be amended by the BDFL at any time. All amendments will -be: - -1. Documented as an ADR in `docs/decisions/` explaining the rationale for the change. -2. Committed to the repository with a clear commit message. -3. Communicated to existing maintainers and contributors via the project's usual - channels. - -Substantive changes (e.g., changing the governance model itself) should be discussed -with the community before adoption, even though the BDFL retains final authority. - ---- - -Copyright (c) 2026 hyperpolymath. Licensed under MPL-2.0. diff --git a/PLACEHOLDERS.adoc b/PLACEHOLDERS.adoc new file mode 100644 index 0000000..c8cd7bb --- /dev/null +++ b/PLACEHOLDERS.adoc @@ -0,0 +1,219 @@ +== Template Placeholders + +All placeholders in this template follow the `+{{PLACEHOLDER}}+` +pattern. After cloning, replace them with your project-specific values. + +=== Recommended: Interactive Bootstrap + +[source,bash] +---- +just init +---- + +This interactively prompts for all values, replaces every placeholder, +validates the result, and runs k9-svc checks if available. + +=== Manual Replace + +[source,bash] +---- +# If you prefer manual replacement (run from repo root) + +sed -i 's/Jonathan D.A. Jewell/Jane Doe/g' $(grep -rl 'Jonathan D.A. Jewell' .) +sed -i 's/j.d.a.jewell@open.ac.uk/jane@example.org/g' $(grep -rl 'j.d.a.jewell@open.ac.uk' .) +sed -i 's/hyperpolymath/my-org/g' $(grep -rl 'hyperpolymath' .) +sed -i 's/Typell/my-project/g' $(grep -rl 'Typell' .) +sed -i 's/{{PROJECT}}/MY_PROJECT/g' $(grep -rl '{{PROJECT}}' .) +sed -i 's/{{project}}/my_project/g' $(grep -rl '{{project}}' .) +sed -i 's/typell/my-project/g' $(grep -rl 'typell' .) +sed -i 's/github.com/github.com/g' $(grep -rl 'github.com' .) +sed -i "s/2026/$(date +%Y)/g" $(grep -rl '2026' .) +sed -i "s/2026-03-16/$(date +%Y-%m-%d)/g" $(grep -rl '2026-03-16' .) +---- + +=== Placeholder Reference + +==== Author & Copyright + +[width="100%",cols="25%,25%,25%,25%",options="header",] +|=== +|Placeholder |Description |Example |Files +|`+Jonathan D.A. Jewell+` |Full legal name |`+Jane Doe+` |SPDX headers +(all files), MAINTAINERS.md, .mailmap, .reuse/dep5, +docs/AI-CONVENTIONS.md + +|`+j.d.a.jewell@open.ac.uk+` |Primary contact email +|`+jane@example.org+` |SPDX headers (all files), .mailmap, .reuse/dep5, +.well-known/humans.txt + +|`+{{AUTHOR_EMAIL_ALT}}+` |Previous/secondary email (for .mailmap) +|`+old@example.com+` |.mailmap + +|`+{{AUTHOR_ORG}}+` |Author’s organization/affiliation +|`+Acme University+` |project-metadata.k9.ncl + +|`+{{AUTHOR_LAST}}+` |Author surname (for citations) |`+Doe+` +|docs/CITATIONS.adoc + +|`+{{AUTHOR_FIRST}}+` |Author first name (for citations) |`+Jane+` +|docs/CITATIONS.adoc + +|`+{{AUTHOR_INITIALS}}+` |Author initials (for citations) |`+J.+` +|docs/CITATIONS.adoc +|=== + +==== Project Identity + +[width="100%",cols="25%,25%,25%,25%",options="header",] +|=== +|Placeholder |Description |Example |Files +|`+Typell+` |Human-readable project name |`+My Project+` |SECURITY.md, +CODE_OF_CONDUCT.md, TOPOLOGY.md, STATE.a2ml, Justfile, GOVERNANCE.md, +MAINTAINERS.md, flake.nix, devcontainer.json + +|`+{{PROJECT_DESCRIPTION}}+` |One-line description |`+A tool for X+` +|flake.nix + +|`+{{PROJECT}}+` |Uppercase identifier (for Idris2 modules, C macros) +|`+MY_PROJECT+` |ABI-FFI-README.md, src/abi/_.idr, ffi/zig/_.zig + +|`+{{project}}+` |Lowercase identifier (for C symbols, filenames) +|`+my_project+` |ABI-FFI-README.md, ffi/zig/*.zig + +|`+typell+` |Repository name (slug) |`+my-project+` |CONTRIBUTING.md, +SECURITY.md, CODE_OF_CONDUCT.md, cliff.toml + +|`+hyperpolymath+` |GitHub/GitLab org or username |`+my-org+` |SPDX +headers, CONTRIBUTING.md, SECURITY.md, GOVERNANCE.md, MAINTAINERS.md, +CODEOWNERS, mirror.yml, cliff.toml + +|`+github.com+` |Git forge domain |`+github.com+` |CONTRIBUTING.md +|=== + +==== Dates + +[width="100%",cols="25%,25%,25%,25%",options="header",] +|=== +|Placeholder |Description |Example |Files +|`+2026+` |Current year |`+2026+` |SPDX headers (all files), +GOVERNANCE.md, MAINTAINERS.md + +|`+2026-03-16+` |Current date (ISO) |`+2026-02-14+` |STATE.a2ml, +MAINTAINERS.md + +|`+{{DATE}}+` |Last updated date |`+2026-02-14+` |TOPOLOGY.md, +THREAT-MODEL.md +|=== + +==== Contact & Security + +[width="100%",cols="25%,25%,25%,25%",options="header",] +|=== +|Placeholder |Description |Example |Files +|`+6759885+hyperpolymath@users.noreply.github.com+` |Security contact +email |`+security@example.org+` |SECURITY.md + +|`+[PGP fingerprint not set]+` |40-char PGP fingerprint +|`+ABCD 1234 ...+` |SECURITY.md + +|`+{{PGP_KEY_URL}}+` |URL to public PGP key +|`+https://keys.openpgp.org/...+` |SECURITY.md + +|`+{{WEBSITE}}+` |Project website |`+https://example.org+` |SECURITY.md + +|`+{{CONDUCT_EMAIL}}+` |Conduct reports email |`+conduct@example.org+` +|CODE_OF_CONDUCT.md + +|`+{{CONDUCT_TEAM}}+` |Conduct committee name +|`+Code of Conduct Committee+` |CODE_OF_CONDUCT.md + +|`+{{RESPONSE_TIME}}+` |SLA for initial response |`+48 hours+` +|CODE_OF_CONDUCT.md +|=== + +==== Git + +[cols=",,,",options="header",] +|=== +|Placeholder |Description |Example |Files +|`+main+` |Main branch name |`+main+` |CONTRIBUTING.md +|=== + +==== Build + +[width="100%",cols="25%,25%,25%,25%",options="header",] +|=== +|Placeholder |Description |Example |Files +|`+MPL-2.0+` |License name |`+MPL-2.0+` |ABI-FFI-README.md + +|`+{{PROJECT_PURPOSE}}+` |One-line project description +|`+FFI bridges between languages+` |STATE.a2ml +|=== + +==== AI Manifest + +[width="100%",cols="25%,25%,25%,25%",options="header",] +|=== +|Placeholder |Description |Example |Files +|`+[YOUR-REPO-NAME]+` |Repository name |`+my-project+` +|0-AI-MANIFEST.a2ml + +|`+[DATE]+` |Creation date |`+2026-02-14+` |0-AI-MANIFEST.a2ml + +|`+[YOUR-NAME/ORG]+` |Maintainer name |`+hyperpolymath+` +|0-AI-MANIFEST.a2ml +|=== + +==== AI Installation Guide + +[width="100%",cols="34%,33%,33%",options="header",] +|=== +|Marker |Description |Files +|`+[TODO-AI-INSTALL]+` |Unfilled section in AI installation guide +|`+docs/AI_INSTALLATION_GUIDE.adoc+`, +`+docs/AI-INSTALL-README-SECTION.adoc+`, `+README.adoc+` +|=== + +These are *not* standard `+{{PLACEHOLDER}}+` markers – they are TODO +markers that must be replaced with project-specific content before +release. They mark sections where the developer (or AI) must fill in: + +* What questions the AI should ask the user +* Exact prerequisite check and install commands +* Privacy notice specific to this project +* Complete installation command block +* Credential setup instructions (URLs, scopes, env vars) +* Verification commands and expected output +* Error handling table +* Example conversation + +*finishbot checks:* `+just validate-ai-install+` verifies no +`+[TODO-AI-INSTALL]+` markers remain. + +=== Deletion Markers + +Some files contain deletion instructions: + +[width="100%",cols="34%,33%,33%",options="header",] +|=== +|Marker |Meaning |File +|`+{{~ ... ~}}+` |Delete this entire line after reading +|ABI-FFI-README.md (line 1) +|=== + +=== Verification + +After replacing all placeholders, verify none remain: + +[source,bash] +---- +grep -rn '{{' . --include='*.md' --include='*.adoc' --include='*.a2ml' \ + --include='*.scm' --include='*.idr' --include='*.zig' --include='*.res' \ + --include='Justfile' --include='*.nix' --include='*.toml' --include='*.yml' \ + --include='*.yaml' --include='*.hs' --include='*.ncl' --include='*.txt' \ + --include='*.json' --include='Containerfile' --include='dep5' \ + | grep -v 'PLACEHOLDERS.md' | grep -v 'node_modules' +---- + +If the above command produces no output, all placeholders have been +replaced. diff --git a/PLACEHOLDERS.md b/PLACEHOLDERS.md deleted file mode 100644 index f6a5153..0000000 --- a/PLACEHOLDERS.md +++ /dev/null @@ -1,141 +0,0 @@ -# Template Placeholders - -All placeholders in this template follow the `{{PLACEHOLDER}}` pattern. -After cloning, replace them with your project-specific values. - -## Recommended: Interactive Bootstrap - -```bash -just init -``` - -This interactively prompts for all values, replaces every placeholder, -validates the result, and runs k9-svc checks if available. - -## Manual Replace - -```bash -# If you prefer manual replacement (run from repo root) - -sed -i 's/Jonathan D.A. Jewell/Jane Doe/g' $(grep -rl 'Jonathan D.A. Jewell' .) -sed -i 's/j.d.a.jewell@open.ac.uk/jane@example.org/g' $(grep -rl 'j.d.a.jewell@open.ac.uk' .) -sed -i 's/hyperpolymath/my-org/g' $(grep -rl 'hyperpolymath' .) -sed -i 's/Typell/my-project/g' $(grep -rl 'Typell' .) -sed -i 's/{{PROJECT}}/MY_PROJECT/g' $(grep -rl '{{PROJECT}}' .) -sed -i 's/{{project}}/my_project/g' $(grep -rl '{{project}}' .) -sed -i 's/typell/my-project/g' $(grep -rl 'typell' .) -sed -i 's/github.com/github.com/g' $(grep -rl 'github.com' .) -sed -i "s/2026/$(date +%Y)/g" $(grep -rl '2026' .) -sed -i "s/2026-03-16/$(date +%Y-%m-%d)/g" $(grep -rl '2026-03-16' .) -``` - -## Placeholder Reference - -### Author & Copyright - -| Placeholder | Description | Example | Files | -|---|---|---|---| -| `Jonathan D.A. Jewell` | Full legal name | `Jane Doe` | SPDX headers (all files), MAINTAINERS.md, .mailmap, .reuse/dep5, docs/AI-CONVENTIONS.md | -| `j.d.a.jewell@open.ac.uk` | Primary contact email | `jane@example.org` | SPDX headers (all files), .mailmap, .reuse/dep5, .well-known/humans.txt | -| `{{AUTHOR_EMAIL_ALT}}` | Previous/secondary email (for .mailmap) | `old@example.com` | .mailmap | -| `{{AUTHOR_ORG}}` | Author's organization/affiliation | `Acme University` | project-metadata.k9.ncl | -| `{{AUTHOR_LAST}}` | Author surname (for citations) | `Doe` | docs/CITATIONS.adoc | -| `{{AUTHOR_FIRST}}` | Author first name (for citations) | `Jane` | docs/CITATIONS.adoc | -| `{{AUTHOR_INITIALS}}` | Author initials (for citations) | `J.` | docs/CITATIONS.adoc | - -### Project Identity - -| Placeholder | Description | Example | Files | -|---|---|---|---| -| `Typell` | Human-readable project name | `My Project` | SECURITY.md, CODE_OF_CONDUCT.md, TOPOLOGY.md, STATE.a2ml, Justfile, GOVERNANCE.md, MAINTAINERS.md, flake.nix, devcontainer.json | -| `{{PROJECT_DESCRIPTION}}` | One-line description | `A tool for X` | flake.nix | -| `{{PROJECT}}` | Uppercase identifier (for Idris2 modules, C macros) | `MY_PROJECT` | ABI-FFI-README.md, src/abi/*.idr, ffi/zig/*.zig | -| `{{project}}` | Lowercase identifier (for C symbols, filenames) | `my_project` | ABI-FFI-README.md, ffi/zig/*.zig | -| `typell` | Repository name (slug) | `my-project` | CONTRIBUTING.md, SECURITY.md, CODE_OF_CONDUCT.md, cliff.toml | -| `hyperpolymath` | GitHub/GitLab org or username | `my-org` | SPDX headers, CONTRIBUTING.md, SECURITY.md, GOVERNANCE.md, MAINTAINERS.md, CODEOWNERS, mirror.yml, cliff.toml | -| `github.com` | Git forge domain | `github.com` | CONTRIBUTING.md | - -### Dates - -| Placeholder | Description | Example | Files | -|---|---|---|---| -| `2026` | Current year | `2026` | SPDX headers (all files), GOVERNANCE.md, MAINTAINERS.md | -| `2026-03-16` | Current date (ISO) | `2026-02-14` | STATE.a2ml, MAINTAINERS.md | -| `{{DATE}}` | Last updated date | `2026-02-14` | TOPOLOGY.md, THREAT-MODEL.md | - -### Contact & Security - -| Placeholder | Description | Example | Files | -|---|---|---|---| -| `6759885+hyperpolymath@users.noreply.github.com` | Security contact email | `security@example.org` | SECURITY.md | -| `[PGP fingerprint not set]` | 40-char PGP fingerprint | `ABCD 1234 ...` | SECURITY.md | -| `{{PGP_KEY_URL}}` | URL to public PGP key | `https://keys.openpgp.org/...` | SECURITY.md | -| `{{WEBSITE}}` | Project website | `https://example.org` | SECURITY.md | -| `{{CONDUCT_EMAIL}}` | Conduct reports email | `conduct@example.org` | CODE_OF_CONDUCT.md | -| `{{CONDUCT_TEAM}}` | Conduct committee name | `Code of Conduct Committee` | CODE_OF_CONDUCT.md | -| `{{RESPONSE_TIME}}` | SLA for initial response | `48 hours` | CODE_OF_CONDUCT.md | - -### Git - -| Placeholder | Description | Example | Files | -|---|---|---|---| -| `main` | Main branch name | `main` | CONTRIBUTING.md | - -### Build - -| Placeholder | Description | Example | Files | -|---|---|---|---| -| `MPL-2.0` | License name | `MPL-2.0` | ABI-FFI-README.md | -| `{{PROJECT_PURPOSE}}` | One-line project description | `FFI bridges between languages` | STATE.a2ml | - -### AI Manifest - -| Placeholder | Description | Example | Files | -|---|---|---|---| -| `[YOUR-REPO-NAME]` | Repository name | `my-project` | 0-AI-MANIFEST.a2ml | -| `[DATE]` | Creation date | `2026-02-14` | 0-AI-MANIFEST.a2ml | -| `[YOUR-NAME/ORG]` | Maintainer name | `hyperpolymath` | 0-AI-MANIFEST.a2ml | - -### AI Installation Guide - -| Marker | Description | Files | -|---|---|---| -| `[TODO-AI-INSTALL]` | Unfilled section in AI installation guide | `docs/AI_INSTALLATION_GUIDE.adoc`, `docs/AI-INSTALL-README-SECTION.adoc`, `README.adoc` | - -These are **not** standard `{{PLACEHOLDER}}` markers -- they are TODO markers -that must be replaced with project-specific content before release. They mark -sections where the developer (or AI) must fill in: - -- What questions the AI should ask the user -- Exact prerequisite check and install commands -- Privacy notice specific to this project -- Complete installation command block -- Credential setup instructions (URLs, scopes, env vars) -- Verification commands and expected output -- Error handling table -- Example conversation - -**finishbot checks:** `just validate-ai-install` verifies no `[TODO-AI-INSTALL]` markers remain. - -## Deletion Markers - -Some files contain deletion instructions: - -| Marker | Meaning | File | -|---|---|---| -| `{{~ ... ~}}` | Delete this entire line after reading | ABI-FFI-README.md (line 1) | - -## Verification - -After replacing all placeholders, verify none remain: - -```bash -grep -rn '{{' . --include='*.md' --include='*.adoc' --include='*.a2ml' \ - --include='*.scm' --include='*.idr' --include='*.zig' --include='*.res' \ - --include='Justfile' --include='*.nix' --include='*.toml' --include='*.yml' \ - --include='*.yaml' --include='*.hs' --include='*.ncl' --include='*.txt' \ - --include='*.json' --include='Containerfile' --include='dep5' \ - | grep -v 'PLACEHOLDERS.md' | grep -v 'node_modules' -``` - -If the above command produces no output, all placeholders have been replaced. diff --git a/READINESS.adoc b/READINESS.adoc new file mode 100644 index 0000000..7a05a91 --- /dev/null +++ b/READINESS.adoc @@ -0,0 +1,59 @@ +== TYPELL Component Readiness Assessment + +*Standard:* +https://github.com/hyperpolymath/standards/tree/main/component-readiness-grades[Component +Readiness Grades (CRG) v1.0] *Assessed:* 2026-03-01 *Assessor:* Jonathan +D.A. Jewell + +*Current Grade:* C + +=== Grade Reference + +[width="100%",cols="8%,22%,19%,51%",options="header",] +|=== +|Grade |Name |Release Stage |Meaning +|X |Untested |— |No testing performed. Status unknown. + +|F |Harmful / Wasteful |— |Reject, deprecate, or delegate. + +|E |Minimal / Salvageable |Pre-alpha |Barely functional. Needs redesign +or major work. + +|D |Partial / Inconsistent |Alpha |Works on some things but not +systematically. + +|C |Self-Validated |Beta |Dogfooded and reliable in home context. + +|B |Broadly Validated |Release Candidate |Tested on 6+ diverse external +targets. + +|A |Field-Proven |Stable |Real-world feedback confirms value. No harm in +wild. +|=== + +=== Component Assessment + +[width="99%",cols="21%,6%,18%,42%,13%",options="header",] +|=== +|Component |Grade |Release Stage |Evidence Summary |Last Assessed +|`+example-command+` |X |— |Not yet tested. |2026-03-01 +|`+another-feature+` |X |— |Not yet tested. |2026-03-01 +|=== + +=== Detailed Assessment + +=== Notes + +* Grades are per-component, not per-project. +* Grade A does not mean perfection — it means demonstrated value in the +field. +* Grade F includes opportunity cost — maintaining something when a +better tool exists. +* Grades can be skipped if evidence supports it (e.g., X → C if +dogfooded immediately). +* Review all grades before each release and at least once per release +cycle. +* See the +https://github.com/hyperpolymath/standards/tree/main/component-readiness-grades[full +CRG standard] for complete definitions, evidence requirements, and +transition criteria. diff --git a/READINESS.md b/READINESS.md deleted file mode 100644 index 74eeb36..0000000 --- a/READINESS.md +++ /dev/null @@ -1,55 +0,0 @@ - - - -# TYPELL Component Readiness Assessment - -**Standard:** [Component Readiness Grades (CRG) v1.0](https://github.com/hyperpolymath/standards/tree/main/component-readiness-grades) -**Assessed:** 2026-03-01 -**Assessor:** Jonathan D.A. Jewell - -**Current Grade:** C - -## Grade Reference - -| Grade | Name | Release Stage | Meaning | -|-------|-----------------------|--------------------|------------------------------------------------------| -| X | Untested | — | No testing performed. Status unknown. | -| F | Harmful / Wasteful | — | Reject, deprecate, or delegate. | -| E | Minimal / Salvageable | Pre-alpha | Barely functional. Needs redesign or major work. | -| D | Partial / Inconsistent| Alpha | Works on some things but not systematically. | -| C | Self-Validated | Beta | Dogfooded and reliable in home context. | -| B | Broadly Validated | Release Candidate | Tested on 6+ diverse external targets. | -| A | Field-Proven | Stable | Real-world feedback confirms value. No harm in wild. | - -## Component Assessment - - - -| Component | Grade | Release Stage | Evidence Summary | Last Assessed | -|---------------------|-------|--------------------|-----------------------------------------------|---------------| -| `example-command` | X | — | Not yet tested. | 2026-03-01 | -| `another-feature` | X | — | Not yet tested. | 2026-03-01 | - -## Detailed Assessment - - - - - -## Notes - -- Grades are per-component, not per-project. -- Grade A does not mean perfection — it means demonstrated value in the field. -- Grade F includes opportunity cost — maintaining something when a better tool exists. -- Grades can be skipped if evidence supports it (e.g., X → C if dogfooded immediately). -- Review all grades before each release and at least once per release cycle. -- See the [full CRG standard](https://github.com/hyperpolymath/standards/tree/main/component-readiness-grades) for complete definitions, evidence requirements, and transition criteria. diff --git a/SECURITY.adoc b/SECURITY.adoc new file mode 100644 index 0000000..de0f12c --- /dev/null +++ b/SECURITY.adoc @@ -0,0 +1,451 @@ +== Security Policy + +We take security seriously. We appreciate your efforts to responsibly +disclose vulnerabilities and will make every effort to acknowledge your +contributions. + +=== Table of Contents + +* link:#reporting-a-vulnerability[Reporting a Vulnerability] +* link:#what-to-include[What to Include] +* link:#response-timeline[Response Timeline] +* link:#disclosure-policy[Disclosure Policy] +* link:#scope[Scope] +* link:#safe-harbour[Safe Harbour] +* link:#recognition[Recognition] +* link:#security-updates[Security Updates] +* link:#security-best-practices[Security Best Practices] + +''''' + +=== Reporting a Vulnerability + +==== Preferred Method: GitHub Security Advisories + +The preferred method for reporting security vulnerabilities is through +GitHub’s Security Advisory feature: + +[arabic] +. Navigate to +https://github.com/hyperpolymath/typell/security/advisories/new[Report a +Vulnerability] +. Click *"`Report a vulnerability`"* +. Complete the form with as much detail as possible +. Submit — we’ll receive a private notification + +This method ensures: + +* End-to-end encryption of your report +* Private discussion space for collaboration +* Coordinated disclosure tooling +* Automatic credit when the advisory is published + +==== Alternative: Encrypted Email + +If you cannot use GitHub Security Advisories, you may email us directly: + +[cols=",",] +|=== +|*Email* |j.d.a.jewell@open.ac.uk +|*PGP Key* |link:TODO[Download Public Key] +|*Fingerprint* |`+TODO+` +|=== + +[source,bash] +---- +# Import our PGP key +curl -sSL TODO | gpg --import + +# Verify fingerprint +gpg --fingerprint j.d.a.jewell@open.ac.uk + +# Encrypt your report +gpg --armor --encrypt --recipient j.d.a.jewell@open.ac.uk report.txt +---- + +____ +*⚠️ Important:* Do not report security vulnerabilities through public +GitHub issues, pull requests, discussions, or social media. +____ + +''''' + +=== What to Include + +A good vulnerability report helps us understand and reproduce the issue +quickly. + +==== Required Information + +* *Description*: Clear explanation of the vulnerability +* *Impact*: What an attacker could achieve (confidentiality, integrity, +availability) +* *Affected versions*: Which versions/commits are affected +* *Reproduction steps*: Detailed steps to reproduce the issue + +==== Helpful Additional Information + +* *Proof of concept*: Code, scripts, or screenshots demonstrating the +vulnerability +* *Attack scenario*: Realistic attack scenario showing exploitability +* *CVSS score*: Your assessment of severity (use +https://www.first.org/cvss/calculator/3.1[CVSS 3.1 Calculator]) +* *CWE ID*: Common Weakness Enumeration identifier if known +* *Suggested fix*: If you have ideas for remediation +* *References*: Links to related vulnerabilities, research, or +advisories + +==== Example Report Structure + +[source,markdown] +---- +## Summary +[One-sentence description of the vulnerability] + +## Vulnerability Type +[e.g., SQL Injection, XSS, SSRF, Path Traversal, etc.] + +## Affected Component +[File path, function name, API endpoint, etc.] + +## Affected Versions +[Version range or specific commits] + +## Severity Assessment +- CVSS 3.1 Score: [X.X] +- CVSS Vector: [CVSS:3.1/AV:X/AC:X/PR:X/UI:X/S:X/C:X/I:X/A:X] + +## Description +[Detailed technical description] + +## Steps to Reproduce +1. [First step] +2. [Second step] +3. [...] + +## Proof of Concept +[Code, curl commands, screenshots, etc.] + +## Impact +[What can an attacker achieve?] + +## Suggested Remediation +[Optional: your ideas for fixing] + +## References +[Links to related issues, CVEs, research] +---- + +''''' + +=== Response Timeline + +We commit to the following response times: + +[width="100%",cols="24%,35%,41%",options="header",] +|=== +|Stage |Timeframe |Description +|*Initial Response* |48 hours |We acknowledge receipt and confirm we’re +investigating + +|*Triage* |7 days |We assess severity, confirm the vulnerability, and +estimate timeline + +|*Status Update* |Every 7 days |Regular updates on remediation progress + +|*Resolution* |90 days |Target for fix development and release (complex +issues may take longer) + +|*Disclosure* |90 days |Public disclosure after fix is available +(coordinated with you) +|=== + +____ +*Note:* These are targets, not guarantees. Complex vulnerabilities may +require more time. We’ll communicate openly about any delays. +____ + +''''' + +=== Disclosure Policy + +We follow *coordinated disclosure* (also known as responsible +disclosure): + +[arabic] +. *You report* the vulnerability privately +. *We acknowledge* and begin investigation +. *We develop* a fix and prepare a release +. *We coordinate* disclosure timing with you +. *We publish* security advisory and fix simultaneously +. *You may publish* your research after disclosure + +==== Our Commitments + +* We will not take legal action against researchers who follow this +policy +* We will work with you to understand and resolve the issue +* We will credit you in the security advisory (unless you prefer +anonymity) +* We will notify you before public disclosure +* We will publish advisories with sufficient detail for users to assess +risk + +==== Your Commitments + +* Report vulnerabilities promptly after discovery +* Give us reasonable time to address the issue before disclosure +* Do not access, modify, or delete data beyond what’s necessary to +demonstrate the vulnerability +* Do not degrade service availability (no DoS testing on production) +* Do not share vulnerability details with others until coordinated +disclosure + +==== Disclosure Timeline + +.... +Day 0 You report vulnerability +Day 1-2 We acknowledge receipt +Day 7 We confirm vulnerability and share initial assessment +Day 7-90 We develop and test fix +Day 90 Coordinated public disclosure + (earlier if fix is ready; later by mutual agreement) +.... + +If we cannot reach agreement on disclosure timing, we default to 90 days +from your initial report. + +''''' + +=== Scope + +==== In Scope ✅ + +The following are within scope for security research: + +* This repository (`+hyperpolymath/typell+`) and all its code +* Official releases and packages published from this repository +* Documentation that could lead to security issues +* Build and deployment configurations in this repository +* Dependencies (report here, we’ll coordinate with upstream) + +==== Out of Scope ❌ + +The following are *not* in scope: + +* Third-party services we integrate with (report directly to them) +* Social engineering attacks against maintainers +* Physical security +* Denial of service attacks against production infrastructure +* Spam, phishing, or other non-technical attacks +* Issues already reported or publicly known +* Theoretical vulnerabilities without proof of concept + +==== Qualifying Vulnerabilities + +We’re particularly interested in: + +* Remote code execution +* SQL injection, command injection, code injection +* Authentication/authorisation bypass +* Cross-site scripting (XSS) and cross-site request forgery (CSRF) +* Server-side request forgery (SSRF) +* Path traversal / local file inclusion +* Information disclosure (credentials, PII, secrets) +* Cryptographic weaknesses +* Deserialisation vulnerabilities +* Memory safety issues (buffer overflows, use-after-free, etc.) +* Supply chain vulnerabilities (dependency confusion, etc.) +* Significant logic flaws + +==== Non-Qualifying Issues + +The following generally do not qualify as security vulnerabilities: + +* Missing security headers on non-sensitive pages +* Clickjacking on pages without sensitive actions +* Self-XSS (requires victim to paste code) +* Missing rate limiting (unless it enables a specific attack) +* Username/email enumeration (unless high-risk context) +* Missing cookie flags on non-sensitive cookies +* Software version disclosure +* Verbose error messages (unless exposing secrets) +* Best practice deviations without demonstrable impact + +''''' + +=== Safe Harbour + +We support security research conducted in good faith. + +==== Our Promise + +If you conduct security research in accordance with this policy: + +* ✅ We will not initiate legal action against you +* ✅ We will not report your activity to law enforcement +* ✅ We will work with you in good faith to resolve issues +* ✅ We consider your research authorised under the Computer Fraud and +Abuse Act (CFAA), UK Computer Misuse Act, and similar laws +* ✅ We waive any potential claim against you for circumvention of +security controls + +==== Good Faith Requirements + +To qualify for safe harbour, you must: + +* Comply with this security policy +* Report vulnerabilities promptly +* Avoid privacy violations (do not access others’ data) +* Avoid service degradation (no destructive testing) +* Not exploit vulnerabilities beyond proof-of-concept +* Not use vulnerabilities for profit (beyond bug bounties where offered) + +____ +*⚠️ Important:* This safe harbour does not extend to third-party +systems. Always check their policies before testing. +____ + +''''' + +=== Recognition + +We believe in recognising security researchers who help us improve. + +==== Hall of Fame + +Researchers who report valid vulnerabilities will be acknowledged in our +link:SECURITY-ACKNOWLEDGMENTS.md[Security Acknowledgments] (unless they +prefer anonymity). + +Recognition includes: + +* Your name (or chosen alias) +* Link to your website/profile (optional) +* Brief description of the vulnerability class +* Date of report + +==== What We Offer + +* ✅ Public credit in security advisories +* ✅ Acknowledgment in release notes +* ✅ Entry in our Hall of Fame +* ✅ Reference/recommendation letter upon request (for significant +findings) + +==== What We Don’t Currently Offer + +* ❌ Monetary bug bounties +* ❌ Hardware or swag +* ❌ Paid security research contracts + +____ +*Note:* We’re a community project with limited resources. Your +contributions help everyone who uses this software. +____ + +''''' + +=== Security Updates + +==== Receiving Updates + +To stay informed about security updates: + +* *Watch this repository*: Click "`Watch`" → "`Custom`" → Select +"`Security alerts`" +* *GitHub Security Advisories*: Published at +https://github.com/hyperpolymath/typell/security/advisories[Security +Advisories] +* *Release notes*: Security fixes noted in link:CHANGELOG.md[CHANGELOG] + +==== Update Policy + +[cols=",",options="header",] +|=== +|Severity |Response +|*Critical/High* |Patch release as soon as fix is ready +|*Medium* |Included in next scheduled release (or earlier) +|*Low* |Included in next scheduled release +|=== + +==== Supported Versions + +[cols=",,",options="header",] +|=== +|Version |Supported |Notes +|`+main+` branch |✅ Yes |Latest development +|Latest release |✅ Yes |Current stable +|Previous minor release |✅ Yes |Security fixes backported +|Older versions |❌ No |Please upgrade +|=== + +''''' + +=== Security Best Practices + +When using Typell, we recommend: + +==== General + +* Keep dependencies up to date +* Use the latest stable release +* Subscribe to security notifications +* Review configuration against security documentation +* Follow principle of least privilege + +==== For Contributors + +* Never commit secrets, credentials, or API keys +* Use signed commits (`+git config commit.gpgsign true+`) +* Review dependencies before adding them +* Run security linters locally before pushing +* Report any concerns about existing code + +''''' + +=== Additional Resources + +* link:TODO[Our PGP Public Key] +* https://github.com/hyperpolymath/typell/security/advisories[Security +Advisories] +* link:CHANGELOG.md[Changelog] +* link:CONTRIBUTING.md[Contributing Guidelines] +* https://cve.mitre.org/[CVE Database] +* https://www.first.org/cvss/calculator/3.1[CVSS Calculator] + +''''' + +=== Contact + +[width="100%",cols="50%,50%",options="header",] +|=== +|Purpose |Contact +|*Security issues* +|https://github.com/hyperpolymath/typell/security/advisories/new[Report +via GitHub] or j.d.a.jewell@open.ac.uk + +|*General questions* +|https://github.com/hyperpolymath/typell/discussions[GitHub Discussions] + +|*Other enquiries* |See link:README.md[README] for contact information +|=== + +''''' + +=== Policy Changes + +This security policy may be updated from time to time. Significant +changes will be: + +* Committed to this repository with a clear commit message +* Noted in the changelog +* Announced via GitHub Discussions (for major changes) + +''''' + +_Thank you for helping keep Typell and its users safe._ 🛡️ + +''''' + +Last updated: 2026 · Policy version: 1.0.0 diff --git a/SECURITY.md b/SECURITY.md deleted file mode 100644 index cee6942..0000000 --- a/SECURITY.md +++ /dev/null @@ -1,406 +0,0 @@ -# Security Policy - - - -We take security seriously. We appreciate your efforts to responsibly disclose vulnerabilities and will make every effort to acknowledge your contributions. - -## Table of Contents - -- [Reporting a Vulnerability](#reporting-a-vulnerability) -- [What to Include](#what-to-include) -- [Response Timeline](#response-timeline) -- [Disclosure Policy](#disclosure-policy) -- [Scope](#scope) -- [Safe Harbour](#safe-harbour) -- [Recognition](#recognition) -- [Security Updates](#security-updates) -- [Security Best Practices](#security-best-practices) - ---- - -## Reporting a Vulnerability - -### Preferred Method: GitHub Security Advisories - -The preferred method for reporting security vulnerabilities is through GitHub's Security Advisory feature: - -1. Navigate to [Report a Vulnerability](https://github.com/hyperpolymath/typell/security/advisories/new) -2. Click **"Report a vulnerability"** -3. Complete the form with as much detail as possible -4. Submit — we'll receive a private notification - -This method ensures: - -- End-to-end encryption of your report -- Private discussion space for collaboration -- Coordinated disclosure tooling -- Automatic credit when the advisory is published - -### Alternative: Encrypted Email - -If you cannot use GitHub Security Advisories, you may email us directly: - -| | | -|---|---| -| **Email** | j.d.a.jewell@open.ac.uk | -| **PGP Key** | [Download Public Key](TODO) | -| **Fingerprint** | `TODO` | - -```bash -# Import our PGP key -curl -sSL TODO | gpg --import - -# Verify fingerprint -gpg --fingerprint j.d.a.jewell@open.ac.uk - -# Encrypt your report -gpg --armor --encrypt --recipient j.d.a.jewell@open.ac.uk report.txt -``` - -> **⚠️ Important:** Do not report security vulnerabilities through public GitHub issues, pull requests, discussions, or social media. - ---- - -## What to Include - -A good vulnerability report helps us understand and reproduce the issue quickly. - -### Required Information - -- **Description**: Clear explanation of the vulnerability -- **Impact**: What an attacker could achieve (confidentiality, integrity, availability) -- **Affected versions**: Which versions/commits are affected -- **Reproduction steps**: Detailed steps to reproduce the issue - -### Helpful Additional Information - -- **Proof of concept**: Code, scripts, or screenshots demonstrating the vulnerability -- **Attack scenario**: Realistic attack scenario showing exploitability -- **CVSS score**: Your assessment of severity (use [CVSS 3.1 Calculator](https://www.first.org/cvss/calculator/3.1)) -- **CWE ID**: Common Weakness Enumeration identifier if known -- **Suggested fix**: If you have ideas for remediation -- **References**: Links to related vulnerabilities, research, or advisories - -### Example Report Structure - -```markdown -## Summary -[One-sentence description of the vulnerability] - -## Vulnerability Type -[e.g., SQL Injection, XSS, SSRF, Path Traversal, etc.] - -## Affected Component -[File path, function name, API endpoint, etc.] - -## Affected Versions -[Version range or specific commits] - -## Severity Assessment -- CVSS 3.1 Score: [X.X] -- CVSS Vector: [CVSS:3.1/AV:X/AC:X/PR:X/UI:X/S:X/C:X/I:X/A:X] - -## Description -[Detailed technical description] - -## Steps to Reproduce -1. [First step] -2. [Second step] -3. [...] - -## Proof of Concept -[Code, curl commands, screenshots, etc.] - -## Impact -[What can an attacker achieve?] - -## Suggested Remediation -[Optional: your ideas for fixing] - -## References -[Links to related issues, CVEs, research] -``` - ---- - -## Response Timeline - -We commit to the following response times: - -| Stage | Timeframe | Description | -|-------|-----------|-------------| -| **Initial Response** | 48 hours | We acknowledge receipt and confirm we're investigating | -| **Triage** | 7 days | We assess severity, confirm the vulnerability, and estimate timeline | -| **Status Update** | Every 7 days | Regular updates on remediation progress | -| **Resolution** | 90 days | Target for fix development and release (complex issues may take longer) | -| **Disclosure** | 90 days | Public disclosure after fix is available (coordinated with you) | - -> **Note:** These are targets, not guarantees. Complex vulnerabilities may require more time. We'll communicate openly about any delays. - ---- - -## Disclosure Policy - -We follow **coordinated disclosure** (also known as responsible disclosure): - -1. **You report** the vulnerability privately -2. **We acknowledge** and begin investigation -3. **We develop** a fix and prepare a release -4. **We coordinate** disclosure timing with you -5. **We publish** security advisory and fix simultaneously -6. **You may publish** your research after disclosure - -### Our Commitments - -- We will not take legal action against researchers who follow this policy -- We will work with you to understand and resolve the issue -- We will credit you in the security advisory (unless you prefer anonymity) -- We will notify you before public disclosure -- We will publish advisories with sufficient detail for users to assess risk - -### Your Commitments - -- Report vulnerabilities promptly after discovery -- Give us reasonable time to address the issue before disclosure -- Do not access, modify, or delete data beyond what's necessary to demonstrate the vulnerability -- Do not degrade service availability (no DoS testing on production) -- Do not share vulnerability details with others until coordinated disclosure - -### Disclosure Timeline - -``` -Day 0 You report vulnerability -Day 1-2 We acknowledge receipt -Day 7 We confirm vulnerability and share initial assessment -Day 7-90 We develop and test fix -Day 90 Coordinated public disclosure - (earlier if fix is ready; later by mutual agreement) -``` - -If we cannot reach agreement on disclosure timing, we default to 90 days from your initial report. - ---- - -## Scope - -### In Scope ✅ - -The following are within scope for security research: - -- This repository (`hyperpolymath/typell`) and all its code -- Official releases and packages published from this repository -- Documentation that could lead to security issues -- Build and deployment configurations in this repository -- Dependencies (report here, we'll coordinate with upstream) - -### Out of Scope ❌ - -The following are **not** in scope: - -- Third-party services we integrate with (report directly to them) -- Social engineering attacks against maintainers -- Physical security -- Denial of service attacks against production infrastructure -- Spam, phishing, or other non-technical attacks -- Issues already reported or publicly known -- Theoretical vulnerabilities without proof of concept - -### Qualifying Vulnerabilities - -We're particularly interested in: - -- Remote code execution -- SQL injection, command injection, code injection -- Authentication/authorisation bypass -- Cross-site scripting (XSS) and cross-site request forgery (CSRF) -- Server-side request forgery (SSRF) -- Path traversal / local file inclusion -- Information disclosure (credentials, PII, secrets) -- Cryptographic weaknesses -- Deserialisation vulnerabilities -- Memory safety issues (buffer overflows, use-after-free, etc.) -- Supply chain vulnerabilities (dependency confusion, etc.) -- Significant logic flaws - -### Non-Qualifying Issues - -The following generally do not qualify as security vulnerabilities: - -- Missing security headers on non-sensitive pages -- Clickjacking on pages without sensitive actions -- Self-XSS (requires victim to paste code) -- Missing rate limiting (unless it enables a specific attack) -- Username/email enumeration (unless high-risk context) -- Missing cookie flags on non-sensitive cookies -- Software version disclosure -- Verbose error messages (unless exposing secrets) -- Best practice deviations without demonstrable impact - ---- - -## Safe Harbour - -We support security research conducted in good faith. - -### Our Promise - -If you conduct security research in accordance with this policy: - -- ✅ We will not initiate legal action against you -- ✅ We will not report your activity to law enforcement -- ✅ We will work with you in good faith to resolve issues -- ✅ We consider your research authorised under the Computer Fraud and Abuse Act (CFAA), UK Computer Misuse Act, and similar laws -- ✅ We waive any potential claim against you for circumvention of security controls - -### Good Faith Requirements - -To qualify for safe harbour, you must: - -- Comply with this security policy -- Report vulnerabilities promptly -- Avoid privacy violations (do not access others' data) -- Avoid service degradation (no destructive testing) -- Not exploit vulnerabilities beyond proof-of-concept -- Not use vulnerabilities for profit (beyond bug bounties where offered) - -> **⚠️ Important:** This safe harbour does not extend to third-party systems. Always check their policies before testing. - ---- - -## Recognition - -We believe in recognising security researchers who help us improve. - -### Hall of Fame - -Researchers who report valid vulnerabilities will be acknowledged in our [Security Acknowledgments](SECURITY-ACKNOWLEDGMENTS.md) (unless they prefer anonymity). - -Recognition includes: - -- Your name (or chosen alias) -- Link to your website/profile (optional) -- Brief description of the vulnerability class -- Date of report - -### What We Offer - -- ✅ Public credit in security advisories -- ✅ Acknowledgment in release notes -- ✅ Entry in our Hall of Fame -- ✅ Reference/recommendation letter upon request (for significant findings) - -### What We Don't Currently Offer - -- ❌ Monetary bug bounties -- ❌ Hardware or swag -- ❌ Paid security research contracts - -> **Note:** We're a community project with limited resources. Your contributions help everyone who uses this software. - ---- - -## Security Updates - -### Receiving Updates - -To stay informed about security updates: - -- **Watch this repository**: Click "Watch" → "Custom" → Select "Security alerts" -- **GitHub Security Advisories**: Published at [Security Advisories](https://github.com/hyperpolymath/typell/security/advisories) -- **Release notes**: Security fixes noted in [CHANGELOG](CHANGELOG.md) - -### Update Policy - -| Severity | Response | -|----------|----------| -| **Critical/High** | Patch release as soon as fix is ready | -| **Medium** | Included in next scheduled release (or earlier) | -| **Low** | Included in next scheduled release | - -### Supported Versions - - - -| Version | Supported | Notes | -|---------|-----------|-------| -| `main` branch | ✅ Yes | Latest development | -| Latest release | ✅ Yes | Current stable | -| Previous minor release | ✅ Yes | Security fixes backported | -| Older versions | ❌ No | Please upgrade | - ---- - -## Security Best Practices - -When using Typell, we recommend: - -### General - -- Keep dependencies up to date -- Use the latest stable release -- Subscribe to security notifications -- Review configuration against security documentation -- Follow principle of least privilege - -### For Contributors - -- Never commit secrets, credentials, or API keys -- Use signed commits (`git config commit.gpgsign true`) -- Review dependencies before adding them -- Run security linters locally before pushing -- Report any concerns about existing code - ---- - -## Additional Resources - -- [Our PGP Public Key](TODO) -- [Security Advisories](https://github.com/hyperpolymath/typell/security/advisories) -- [Changelog](CHANGELOG.md) -- [Contributing Guidelines](CONTRIBUTING.md) -- [CVE Database](https://cve.mitre.org/) -- [CVSS Calculator](https://www.first.org/cvss/calculator/3.1) - ---- - -## Contact - -| Purpose | Contact | -|---------|---------| -| **Security issues** | [Report via GitHub](https://github.com/hyperpolymath/typell/security/advisories/new) or j.d.a.jewell@open.ac.uk | -| **General questions** | [GitHub Discussions](https://github.com/hyperpolymath/typell/discussions) | -| **Other enquiries** | See [README](README.md) for contact information | - ---- - -## Policy Changes - -This security policy may be updated from time to time. Significant changes will be: - -- Committed to this repository with a clear commit message -- Noted in the changelog -- Announced via GitHub Discussions (for major changes) - ---- - -*Thank you for helping keep Typell and its users safe.* 🛡️ - ---- - -Last updated: 2026 · Policy version: 1.0.0 diff --git a/archive/MAINTAINERS.adoc b/archive/MAINTAINERS.adoc new file mode 100644 index 0000000..b115b8e --- /dev/null +++ b/archive/MAINTAINERS.adoc @@ -0,0 +1,42 @@ +== Maintainers + +This document lists the current and former maintainers of *Typell*. + +''''' + +=== Current Maintainers + +[width="100%",cols="24%,29%,22%,25%",options="header",] +|=== +|Name |GitHub |Role |Since +|Jonathan D.A. Jewell |https://github.com/hyperpolymath[@hyperpolymath] +|BDFL |2026-03-01 +|=== + +''''' + +=== How to Become a Maintainer + +Contributors who demonstrate sustained, high-quality contributions and a +solid understanding of the project’s standards and goals may be +nominated to become maintainers. The full criteria and process are +described in GOVERNANCE.md. If you are interested, the best path is to +start contributing consistently and engage constructively in issues and +code reviews. + +''''' + +=== Emeritus + +Former maintainers who have stepped back from active maintenance. We are +grateful for their contributions. + +[cols=",,,",options="header",] +|=== +|Name |GitHub |Role |Active +|_None yet_ | | | +|=== + +''''' + +Copyright (c) 2026 hyperpolymath. Licensed under MPL-2.0. diff --git a/archive/MAINTAINERS.md b/archive/MAINTAINERS.md deleted file mode 100644 index 0378a56..0000000 --- a/archive/MAINTAINERS.md +++ /dev/null @@ -1,38 +0,0 @@ - - -# Maintainers - -This document lists the current and former maintainers of **Typell**. - ---- - -## Current Maintainers - -| Name | GitHub | Role | Since | -|------|--------|------|-------| -| Jonathan D.A. Jewell | [@hyperpolymath](https://github.com/hyperpolymath) | BDFL | 2026-03-01 | - ---- - -## How to Become a Maintainer - -Contributors who demonstrate sustained, high-quality contributions and a solid -understanding of the project's standards and goals may be nominated to become -maintainers. The full criteria and process are described in -[GOVERNANCE.md](GOVERNANCE.md). If you are interested, the best path is to start -contributing consistently and engage constructively in issues and code reviews. - ---- - -## Emeritus - -Former maintainers who have stepped back from active maintenance. We are grateful -for their contributions. - -| Name | GitHub | Role | Active | -|------|--------|------|--------| -| *None yet* | | | | - ---- - -Copyright (c) 2026 hyperpolymath. Licensed under MPL-2.0. diff --git a/docs/AI-CONVENTIONS.adoc b/docs/AI-CONVENTIONS.adoc new file mode 100644 index 0000000..980985e --- /dev/null +++ b/docs/AI-CONVENTIONS.adoc @@ -0,0 +1,99 @@ +== AI Conventions (Authoritative Source) + +All AI coding agents working in this repository MUST follow these rules. +Per-tool config files (.cursorrules, .clinerules, etc.) reference this +document. + +=== Session Startup + +[arabic] +. Read `+0-AI-MANIFEST.a2ml+` FIRST (mandatory gatekeeper). +. Read `+.machine_readable/STATE.a2ml+` for current status and blockers. +. Read `+.machine_readable/anchors/ANCHOR.a2ml+` for canonical authority +boundaries. +. Read `+.machine_readable/policies/MAINTENANCE-AXES.a2ml+` for +maintenance/audit sequencing. +. Read `+.machine_readable/policies/MAINTENANCE-CHECKLIST.a2ml+` for +baseline controls. +. Read `+.machine_readable/policies/SOFTWARE-DEVELOPMENT-APPROACH.a2ml+` +for execution order. +. Read `+.machine_readable/AGENTIC.a2ml+` for agent constraints. + +=== License + +* All original code: *MPL-2.0* +* Fallback (platform-required only): MPL-2.0 with comment explaining +why. +* NEVER use AGPL-3.0. +* Preserve third-party licenses verbatim. +* Every source file needs `+# SPDX-License-Identifier: CC-BY-SA-4.0+`. + +=== Author Attribution + +* Name: *Jonathan D.A. Jewell* +* Email: *j.d.a.jewell@open.ac.uk* +* Copyright: +`+Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +` + +=== State Files + +State/metadata files, anchors, and policies (.a2ml) belong in +`+.machine_readable/+` ONLY. NEVER create STATE.a2ml, META.a2ml, +ECOSYSTEM.a2ml, AGENTIC.a2ml, NEUROSYM.a2ml, PLAYBOOK.a2ml, ANCHOR.a2ml, +MAINTENANCE-AXES.a2ml, MAINTENANCE-CHECKLIST.a2ml, or +SOFTWARE-DEVELOPMENT-APPROACH.a2ml in the repository root. + +=== Banned Patterns + +[width="100%",cols="14%,50%,36%",options="header",] +|=== +|Language |Banned |Reason +|Idris2 |`+believe_me+`, `+assert_total+` |Unsound escape hatches +|Haskell |`+unsafeCoerce+`, `+unsafePerformIO+` |Breaks type safety +|OCaml |`+Obj.magic+`, `+Obj.repr+`, `+Obj.obj+` |Unsafe casting +|Coq |`+Admitted+` |Unproven assumption +|Lean |`+sorry+` |Unproven assumption +|Rust |`+transmute+` (unless FFI + SAFETY:) |Unsound reinterpret +|=== + +=== Banned Languages + +[cols=",",options="header",] +|=== +|Banned |Use Instead +|TypeScript |ReScript +|Node.js / npm / bun |Deno +|Go |Rust +|Python |Julia / Rust +|=== + +=== Container Standard + +* Runtime: *Podman* (never Docker). +* File: *Containerfile* (never Dockerfile). +* Base images: `+cgr.dev/chainguard/wolfi-base:latest+` or +`+cgr.dev/chainguard/static:latest+`. + +=== ABI/FFI Standard + +* ABI definitions: *Idris2* with dependent types (`+src/abi/+`). +* FFI implementation: *Zig* with C ABI compatibility (`+ffi/zig/+`). +* Generated C headers: `+generated/abi/+`. + +=== Build System + +Use `+just+` (Justfile) for all build, test, lint, and format tasks. + +=== References + +* `+0-AI-MANIFEST.a2ml+` – universal AI entry point +* `+.machine_readable/AGENTIC.a2ml+` – agent permissions and constraints +* `+.machine_readable/STATE.a2ml+` – current project state +* `+.machine_readable/anchors/ANCHOR.a2ml+` – canonical authority and +policy boundary +* `+.machine_readable/policies/MAINTENANCE-AXES.a2ml+` – canonical axis +sequencing and audit requirements +* `+.machine_readable/policies/MAINTENANCE-CHECKLIST.a2ml+` – baseline +maintenance checklist policy +* `+.machine_readable/policies/SOFTWARE-DEVELOPMENT-APPROACH.a2ml+` – +axis execution approach policy diff --git a/docs/AI-CONVENTIONS.md b/docs/AI-CONVENTIONS.md deleted file mode 100644 index 197bfcc..0000000 --- a/docs/AI-CONVENTIONS.md +++ /dev/null @@ -1,84 +0,0 @@ - - - -# AI Conventions (Authoritative Source) - -All AI coding agents working in this repository MUST follow these rules. -Per-tool config files (.cursorrules, .clinerules, etc.) reference this document. - -## Session Startup - -1. Read `0-AI-MANIFEST.a2ml` FIRST (mandatory gatekeeper). -2. Read `.machine_readable/STATE.a2ml` for current status and blockers. -3. Read `.machine_readable/anchors/ANCHOR.a2ml` for canonical authority boundaries. -4. Read `.machine_readable/policies/MAINTENANCE-AXES.a2ml` for maintenance/audit sequencing. -5. Read `.machine_readable/policies/MAINTENANCE-CHECKLIST.a2ml` for baseline controls. -6. Read `.machine_readable/policies/SOFTWARE-DEVELOPMENT-APPROACH.a2ml` for execution order. -7. Read `.machine_readable/AGENTIC.a2ml` for agent constraints. - -## License - -- All original code: **MPL-2.0** -- Fallback (platform-required only): MPL-2.0 with comment explaining why. -- NEVER use AGPL-3.0. -- Preserve third-party licenses verbatim. -- Every source file needs `# SPDX-License-Identifier: CC-BY-SA-4.0`. - -## Author Attribution - -- Name: **Jonathan D.A. Jewell** -- Email: **j.d.a.jewell@open.ac.uk** -- Copyright: `Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) ` - -## State Files - -State/metadata files, anchors, and policies (.a2ml) belong in `.machine_readable/` ONLY. -NEVER create STATE.a2ml, META.a2ml, ECOSYSTEM.a2ml, AGENTIC.a2ml, -NEUROSYM.a2ml, PLAYBOOK.a2ml, ANCHOR.a2ml, MAINTENANCE-AXES.a2ml, -MAINTENANCE-CHECKLIST.a2ml, or SOFTWARE-DEVELOPMENT-APPROACH.a2ml in the repository root. - -## Banned Patterns - -| Language | Banned | Reason | -|----------|-------------------------------------|---------------------------| -| Idris2 | `believe_me`, `assert_total` | Unsound escape hatches | -| Haskell | `unsafeCoerce`, `unsafePerformIO` | Breaks type safety | -| OCaml | `Obj.magic`, `Obj.repr`, `Obj.obj` | Unsafe casting | -| Coq | `Admitted` | Unproven assumption | -| Lean | `sorry` | Unproven assumption | -| Rust | `transmute` (unless FFI + SAFETY:) | Unsound reinterpret | - -## Banned Languages - -| Banned | Use Instead | -|---------------------|--------------------| -| TypeScript | ReScript | -| Node.js / npm / bun | Deno | -| Go | Rust | -| Python | Julia / Rust | - -## Container Standard - -- Runtime: **Podman** (never Docker). -- File: **Containerfile** (never Dockerfile). -- Base images: `cgr.dev/chainguard/wolfi-base:latest` or `cgr.dev/chainguard/static:latest`. - -## ABI/FFI Standard - -- ABI definitions: **Idris2** with dependent types (`src/abi/`). -- FFI implementation: **Zig** with C ABI compatibility (`ffi/zig/`). -- Generated C headers: `generated/abi/`. - -## Build System - -Use `just` (Justfile) for all build, test, lint, and format tasks. - -## References - -- `0-AI-MANIFEST.a2ml` -- universal AI entry point -- `.machine_readable/AGENTIC.a2ml` -- agent permissions and constraints -- `.machine_readable/STATE.a2ml` -- current project state -- `.machine_readable/anchors/ANCHOR.a2ml` -- canonical authority and policy boundary -- `.machine_readable/policies/MAINTENANCE-AXES.a2ml` -- canonical axis sequencing and audit requirements -- `.machine_readable/policies/MAINTENANCE-CHECKLIST.a2ml` -- baseline maintenance checklist policy -- `.machine_readable/policies/SOFTWARE-DEVELOPMENT-APPROACH.a2ml` -- axis execution approach policy diff --git a/docs/QUICKSTART.adoc b/docs/QUICKSTART.adoc new file mode 100644 index 0000000..e03cc2b --- /dev/null +++ b/docs/QUICKSTART.adoc @@ -0,0 +1,69 @@ +== Quickstart + +Get up and running in 60 seconds. + +=== Prerequisites + +* https://git-scm.com/[Git] 2.40+ +* https://github.com/casey/just[just] (command runner) +* Your language toolchain (see `+Justfile+` for details) + +=== From Template (New Project) + +[source,bash] +---- +git clone https://github.com/hyperpolymath/rsr-template-repo my-project +cd my-project +rm -rf .git && git init -b main +just init # interactive placeholder replacement +---- + +=== Clone and Setup (Existing Project) + +[source,bash] +---- +git clone https://github.com/hyperpolymath/typell.git +cd typell +just deps +---- + +=== Build and Test + +[source,bash] +---- +just build +just test +---- + +=== Verify Everything Works + +[source,bash] +---- +just check +---- + +=== Project Structure + +.... +src/ # Source code +tests/ # Test suite +benches/ # Benchmarks +docs/ # Documentation +.github/ # CI/CD workflows +.... + +=== What Next? + +* Browse the link:.[docs/] for architecture and conventions +* Run `+just --list+` to see all available commands +* Read link:../CONTRIBUTING.md[CONTRIBUTING.md] when you are ready to +contribute + +=== Troubleshooting + +If `+just deps+` fails, ensure your toolchain version matches the +project requirements listed in the `+Justfile+` or +`+.machine_readable/ECOSYSTEM.a2ml+`. + +Open a https://github.com/hyperpolymath/typell/discussions[Discussion] +if you get stuck. diff --git a/docs/QUICKSTART.md b/docs/QUICKSTART.md deleted file mode 100644 index 8fff3ef..0000000 --- a/docs/QUICKSTART.md +++ /dev/null @@ -1,64 +0,0 @@ - -# Quickstart - -Get up and running in 60 seconds. - -## Prerequisites - -- [Git](https://git-scm.com/) 2.40+ -- [just](https://github.com/casey/just) (command runner) -- Your language toolchain (see `Justfile` for details) - -## From Template (New Project) - -```bash -git clone https://github.com/hyperpolymath/rsr-template-repo my-project -cd my-project -rm -rf .git && git init -b main -just init # interactive placeholder replacement -``` - -## Clone and Setup (Existing Project) - -```bash -git clone https://github.com/hyperpolymath/typell.git -cd typell -just deps -``` - -## Build and Test - -```bash -just build -just test -``` - -## Verify Everything Works - -```bash -just check -``` - -## Project Structure - -``` -src/ # Source code -tests/ # Test suite -benches/ # Benchmarks -docs/ # Documentation -.github/ # CI/CD workflows -``` - -## What Next? - -- Browse the [docs/](.) for architecture and conventions -- Run `just --list` to see all available commands -- Read [CONTRIBUTING.md](../CONTRIBUTING.md) when you are ready to contribute - -## Troubleshooting - -If `just deps` fails, ensure your toolchain version matches the -project requirements listed in the `Justfile` or `.machine_readable/ECOSYSTEM.a2ml`. - -Open a [Discussion](https://github.com/hyperpolymath/typell/discussions) -if you get stuck. diff --git a/docs/THREAT-MODEL.adoc b/docs/THREAT-MODEL.adoc new file mode 100644 index 0000000..acf4be9 --- /dev/null +++ b/docs/THREAT-MODEL.adoc @@ -0,0 +1,254 @@ +== Threat Model: Typell + +=== Document Info + +[cols=",",options="header",] +|=== +|Field |Value +|Project |Typell +|Version |1.0 +|Last Reviewed |2026-03-01 +|Author |Jonathan D.A. Jewell +|Methodology |STRIDE +|=== + +=== Scope + +==== In Scope + +* Application source code and build pipeline +* CI/CD workflows (GitHub Actions) +* Container images and runtime environment +* Secrets and credential management +* Dependencies (direct and transitive) +* Deployment artifacts (binaries, containers, SBOM) + +==== Out of Scope + +* Physical security of hosting infrastructure +* GitHub/GitLab platform-level vulnerabilities +* End-user device security +* Social engineering attacks against maintainers (handled by org policy) + +=== System Overview + +Brief description of Typell and its architecture. + +____ +See TOPOLOGY.md for the full architecture diagram and completion +dashboard. +____ + +=== Assets + +[width="100%",cols="25%,16%,13%,46%",options="header",] +|=== +|Asset |Classification |Owner |Notes +|Source code |Internal |Maintainers |Public repos are still +internal-integrity + +|Signing keys |Restricted |Release lead |Signing keys (e.g., Ed25519), +GPG keys + +|CI/CD secrets |Restricted |Maintainers |GITHUB_TOKEN, deploy tokens, +PATs + +|User/contributor data |Confidential |Org |Emails, contributor identity + +|Build artifacts |Internal |CI pipeline |Binaries, WASM bundles + +|Container images |Internal |CI pipeline |Chainguard-based, signed via +image signing tool + +|SBOM / provenance |Public |CI pipeline |SLSA attestations + +|Dependencies |Public |Lockfile |Cargo.lock, deno.lock, gleam.toml + +|Infrastructure config |Confidential |Maintainers |Containerfiles, +compose files, orchestration config +|=== + +=== Trust Boundaries + +[width="100%",cols="35%,32%,33%",options="header",] +|=== +|Boundary |From (Lower Trust) |To (Higher Trust) +|Pull request submission |External contributor |Repository codebase + +|CI/CD workflow execution |Workflow definition |Runner with secrets +access + +|Container build boundary |Build stage |Runtime stage + +|External API calls |Third-party service |Application internals + +|User input (CLI/Web) |End user |Application logic + +|Dependency resolution |Package registry |Build environment + +|Forge mirroring |GitHub |GitLab / Bitbucket +|=== + +=== Threat Actors + +[width="100%",cols="39%,44%,17%",options="header",] +|=== +|Actor |Motivation |Capability +|Script kiddie |Vandalism, clout |Low +|Disgruntled contributor |Sabotage, backdoor insertion |Medium +|Supply chain attacker |Wide-impact compromise |High +|Nation state |Espionage, disruption |Very High +|Automated bot |Credential stuffing, spam PRs |Low-Medium +|=== + +=== STRIDE Analysis + +==== Spoofing + +[width="100%",cols="28%,14%,9%,6%,6%,37%",options="header",] +|=== +|Threat |Affected Asset |Likelihood |Impact |Risk |Mitigation +|Unsigned commits impersonate maintainer |Source code |Medium |High +|High |Require GPG-signed commits; vigilant code review + +|Forged bot actions (automated agents) |CI/CD pipeline |Low |High +|Medium |Bot tokens scoped minimally; audit bot activity + +|Spoofed package registry identity |Dependencies |Low |High |Medium |Pin +dependencies by hash; verify provenance +|=== + +==== Tampering + +[width="100%",cols="28%,14%,9%,6%,6%,37%",options="header",] +|=== +|Threat |Affected Asset |Likelihood |Impact |Risk |Mitigation +|Malicious pull request |Source code |Medium |High |High |Branch +protection; required reviews; CodeQL + +|Dependency poisoning (typosquat) |Dependencies |Medium |High |High +|Lockfiles; secret-scanner; security scans + +|Tampered container base image |Container images |Low |High |Medium +|Chainguard images; image signing verification + +|Workflow file modification |CI/CD pipeline |Low |High |Medium +|CODEOWNERS on .github/; workflow-linter +|=== + +==== Repudiation + +[width="100%",cols="28%,14%,9%,6%,6%,37%",options="header",] +|=== +|Threat |Affected Asset |Likelihood |Impact |Risk |Mitigation +|Unlogged deployment |Build artifacts |Medium |Medium |Medium |SLSA +provenance; deployment audit trail + +|Denied merge of vulnerable code |Source code |Low |Medium |Low |Git +history is immutable; signed commits + +|Secret rotation without record |CI/CD secrets |Low |Low |Low |Secret +rotation logged in STATE.a2ml +|=== + +==== Information Disclosure + +[width="100%",cols="28%,14%,9%,6%,6%,37%",options="header",] +|=== +|Threat |Affected Asset |Likelihood |Impact |Risk |Mitigation +|Secrets leaked in git history |CI/CD secrets |Medium |High |High +|TruffleHog in CI; secret-scanner workflow + +|Verbose error messages in prod |Application logic |Medium |Medium +|Medium |Sanitize outputs; structured logging + +|SBOM reveals internal structure |Infrastructure |Low |Low |Low +|Accepted risk; SBOM is intentionally public +|=== + +==== Denial of Service + +[width="100%",cols="28%,14%,9%,6%,6%,37%",options="header",] +|=== +|Threat |Affected Asset |Likelihood |Impact |Risk |Mitigation +|CI resource exhaustion (fork bomb in PR) |CI/CD pipeline |Medium +|Medium |Medium |Concurrency limits; timeout on workflows + +|Spam issues/PRs flooding triage |Maintainer time |Medium |Low |Low +|GitHub rate limits; bot auto-close stale + +|Large binary commits bloating repo |Source code |Low |Medium |Low +|.gitattributes LFS policy; pre-commit hooks +|=== + +==== Elevation of Privilege + +[width="100%",cols="28%,14%,9%,6%,6%,37%",options="header",] +|=== +|Threat |Affected Asset |Likelihood |Impact |Risk |Mitigation +|Workflow injection via PR title/body |CI/CD pipeline |Medium |High +|High |Never interpolate PR fields in `+run:+`; use env vars + +|GITHUB_TOKEN over-scoped |CI/CD secrets |Medium |High |High +|`+permissions: read-all+` default; per-job scoping + +|Container escape |Runtime environment |Low |High |Medium |Hardened +container runtime; read-only rootfs; no-new-privileges + +|Compromised action dependency |CI/CD pipeline |Medium |High |High +|SHA-pin all actions; never use `+@latest+` tags +|=== + +=== Mitigations in Place + +* *SLSA Provenance*: Build attestations via slsa-github-generator +* *Secret Scanning*: TruffleHog + secret-scanner workflow on every push +* *Static Analysis*: CodeQL on supported languages +* *Supply Chain*: OpenSSF Scorecard (scorecard.yml + +scorecard-enforcer.yml) +* *Container Signing*: Ed25519 signatures on all published images +(optional: use your signing tool) +* *Container Runtime*: Hardened container runtime with formal +verification (optional) +* *Dependency Pinning*: All GitHub Actions SHA-pinned; lockfiles +committed +* *Workflow Validation*: workflow-linter.yml checks all workflow changes +* *Security Scanning*: Neurosymbolic scanning (hypatia-scan.yml, +optional) +* *Bot Governance*: Bot orchestration with confidence thresholds +(optional) +* *Edge Security*: Gateway with policy enforcement (optional, where +applicable) +* *SBOM*: Generated and published with releases + +=== Residual Risks + +[width="100%",cols="39%,41%,20%",options="header",] +|=== +|Risk |Accepted Because |Review Trigger +|Zero-day in GitHub Actions runner |Platform responsibility; no feasible +mitigation |GitHub advisory + +|Maintainer account compromise |Mitigated by 2FA requirement; residual +remains |Any suspicious activity + +|Transitive dependency vulnerability (0-day) |Lockfiles limit blast +radius; scanning catches known CVEs |CVE database update + +|SBOM exposes internal component names |Transparency is a design goal +|Policy change +|=== + +=== Review Schedule + +This threat model should be reviewed: + +* *Quarterly* as a standing item +* *When architecture changes* (new services, new trust boundaries, new +deployment targets) +* *Before major releases* (v1.0, v2.0, etc.) +* *After any security incident* affecting this project or its +dependencies + +Reviewer should update the "`Last Reviewed`" date and version in +Document Info above. diff --git a/docs/THREAT-MODEL.md b/docs/THREAT-MODEL.md deleted file mode 100644 index 4bcaa4b..0000000 --- a/docs/THREAT-MODEL.md +++ /dev/null @@ -1,161 +0,0 @@ - - - -# Threat Model: Typell - -## Document Info - -| Field | Value | -|---------------|--------------------------------| -| Project | Typell | -| Version | 1.0 | -| Last Reviewed | 2026-03-01 | -| Author | Jonathan D.A. Jewell | -| Methodology | STRIDE | - -## Scope - -### In Scope - -- Application source code and build pipeline -- CI/CD workflows (GitHub Actions) -- Container images and runtime environment -- Secrets and credential management -- Dependencies (direct and transitive) -- Deployment artifacts (binaries, containers, SBOM) - -### Out of Scope - -- Physical security of hosting infrastructure -- GitHub/GitLab platform-level vulnerabilities -- End-user device security -- Social engineering attacks against maintainers (handled by org policy) - -## System Overview - -Brief description of Typell and its architecture. - -> See [TOPOLOGY.md](TOPOLOGY.md) for the full architecture diagram and completion dashboard. - -## Assets - -| Asset | Classification | Owner | Notes | -|----------------------|----------------|-------------|--------------------------------------------| -| Source code | Internal | Maintainers | Public repos are still internal-integrity | -| Signing keys | Restricted | Release lead | Signing keys (e.g., Ed25519), GPG keys | -| CI/CD secrets | Restricted | Maintainers | GITHUB_TOKEN, deploy tokens, PATs | -| User/contributor data | Confidential | Org | Emails, contributor identity | -| Build artifacts | Internal | CI pipeline | Binaries, WASM bundles | -| Container images | Internal | CI pipeline | Chainguard-based, signed via image signing tool | -| SBOM / provenance | Public | CI pipeline | SLSA attestations | -| Dependencies | Public | Lockfile | Cargo.lock, deno.lock, gleam.toml | -| Infrastructure config | Confidential | Maintainers | Containerfiles, compose files, orchestration config | - -## Trust Boundaries - -| Boundary | From (Lower Trust) | To (Higher Trust) | -|-----------------------------|---------------------------|----------------------------| -| Pull request submission | External contributor | Repository codebase | -| CI/CD workflow execution | Workflow definition | Runner with secrets access | -| Container build boundary | Build stage | Runtime stage | -| External API calls | Third-party service | Application internals | -| User input (CLI/Web) | End user | Application logic | -| Dependency resolution | Package registry | Build environment | -| Forge mirroring | GitHub | GitLab / Bitbucket | - -## Threat Actors - -| Actor | Motivation | Capability | -|--------------------------|-------------------------------|------------| -| Script kiddie | Vandalism, clout | Low | -| Disgruntled contributor | Sabotage, backdoor insertion | Medium | -| Supply chain attacker | Wide-impact compromise | High | -| Nation state | Espionage, disruption | Very High | -| Automated bot | Credential stuffing, spam PRs | Low-Medium | - -## STRIDE Analysis - -### Spoofing - -| Threat | Affected Asset | Likelihood | Impact | Risk | Mitigation | -|---------------------------------|-------------------|------------|--------|--------|------------------------------------------------| -| Unsigned commits impersonate maintainer | Source code | Medium | High | High | Require GPG-signed commits; vigilant code review | -| Forged bot actions (automated agents) | CI/CD pipeline | Low | High | Medium | Bot tokens scoped minimally; audit bot activity | -| Spoofed package registry identity | Dependencies | Low | High | Medium | Pin dependencies by hash; verify provenance | - -### Tampering - -| Threat | Affected Asset | Likelihood | Impact | Risk | Mitigation | -|---------------------------------|-------------------|------------|--------|--------|------------------------------------------------| -| Malicious pull request | Source code | Medium | High | High | Branch protection; required reviews; CodeQL | -| Dependency poisoning (typosquat) | Dependencies | Medium | High | High | Lockfiles; secret-scanner; security scans | -| Tampered container base image | Container images | Low | High | Medium | Chainguard images; image signing verification | -| Workflow file modification | CI/CD pipeline | Low | High | Medium | CODEOWNERS on .github/; workflow-linter | - -### Repudiation - -| Threat | Affected Asset | Likelihood | Impact | Risk | Mitigation | -|---------------------------------|-------------------|------------|--------|--------|------------------------------------------------| -| Unlogged deployment | Build artifacts | Medium | Medium | Medium | SLSA provenance; deployment audit trail | -| Denied merge of vulnerable code | Source code | Low | Medium | Low | Git history is immutable; signed commits | -| Secret rotation without record | CI/CD secrets | Low | Low | Low | Secret rotation logged in STATE.a2ml | - -### Information Disclosure - -| Threat | Affected Asset | Likelihood | Impact | Risk | Mitigation | -|---------------------------------|-------------------|------------|--------|--------|------------------------------------------------| -| Secrets leaked in git history | CI/CD secrets | Medium | High | High | TruffleHog in CI; secret-scanner workflow | -| Verbose error messages in prod | Application logic | Medium | Medium | Medium | Sanitize outputs; structured logging | -| SBOM reveals internal structure | Infrastructure | Low | Low | Low | Accepted risk; SBOM is intentionally public | - -### Denial of Service - -| Threat | Affected Asset | Likelihood | Impact | Risk | Mitigation | -|---------------------------------|-------------------|------------|--------|--------|------------------------------------------------| -| CI resource exhaustion (fork bomb in PR) | CI/CD pipeline | Medium | Medium | Medium | Concurrency limits; timeout on workflows | -| Spam issues/PRs flooding triage | Maintainer time | Medium | Low | Low | GitHub rate limits; bot auto-close stale | -| Large binary commits bloating repo | Source code | Low | Medium | Low | .gitattributes LFS policy; pre-commit hooks | - -### Elevation of Privilege - -| Threat | Affected Asset | Likelihood | Impact | Risk | Mitigation | -|---------------------------------|-------------------|------------|--------|--------|------------------------------------------------| -| Workflow injection via PR title/body | CI/CD pipeline | Medium | High | High | Never interpolate PR fields in `run:`; use env vars | -| GITHUB_TOKEN over-scoped | CI/CD secrets | Medium | High | High | `permissions: read-all` default; per-job scoping | -| Container escape | Runtime environment | Low | High | Medium | Hardened container runtime; read-only rootfs; no-new-privileges | -| Compromised action dependency | CI/CD pipeline | Medium | High | High | SHA-pin all actions; never use `@latest` tags | - -## Mitigations in Place - -- **SLSA Provenance**: Build attestations via slsa-github-generator -- **Secret Scanning**: TruffleHog + secret-scanner workflow on every push -- **Static Analysis**: CodeQL on supported languages -- **Supply Chain**: OpenSSF Scorecard (scorecard.yml + scorecard-enforcer.yml) -- **Container Signing**: Ed25519 signatures on all published images (optional: use your signing tool) -- **Container Runtime**: Hardened container runtime with formal verification (optional) -- **Dependency Pinning**: All GitHub Actions SHA-pinned; lockfiles committed -- **Workflow Validation**: workflow-linter.yml checks all workflow changes -- **Security Scanning**: Neurosymbolic scanning (hypatia-scan.yml, optional) -- **Bot Governance**: Bot orchestration with confidence thresholds (optional) -- **Edge Security**: Gateway with policy enforcement (optional, where applicable) -- **SBOM**: Generated and published with releases - -## Residual Risks - -| Risk | Accepted Because | Review Trigger | -|-----------------------------------------------|---------------------------------------------------|-------------------------| -| Zero-day in GitHub Actions runner | Platform responsibility; no feasible mitigation | GitHub advisory | -| Maintainer account compromise | Mitigated by 2FA requirement; residual remains | Any suspicious activity | -| Transitive dependency vulnerability (0-day) | Lockfiles limit blast radius; scanning catches known CVEs | CVE database update | -| SBOM exposes internal component names | Transparency is a design goal | Policy change | - -## Review Schedule - -This threat model should be reviewed: - -- **Quarterly** as a standing item -- **When architecture changes** (new services, new trust boundaries, new deployment targets) -- **Before major releases** (v1.0, v2.0, etc.) -- **After any security incident** affecting this project or its dependencies - -Reviewer should update the "Last Reviewed" date and version in Document Info above. diff --git a/docs/TOPOLOGY.md b/docs/TOPOLOGY.adoc similarity index 95% rename from docs/TOPOLOGY.md rename to docs/TOPOLOGY.adoc index 007e70a..273a4a1 100644 --- a/docs/TOPOLOGY.md +++ b/docs/TOPOLOGY.adoc @@ -1,12 +1,8 @@ - - - +== Typell — Project Topology -# Typell — Project Topology +=== System Architecture -## System Architecture - -``` +.... ┌──────────────────────────────────────────────────────┐ │ PanLL (Primary Consumer) │ │ │ @@ -74,11 +70,11 @@ │ │Extension │ │ Tool │ │ (GitHub Actions) │ │ │ └──────────┘ └──────────┘ └──────────────────┘ │ └─────────────────────────────────────────────────────┘ -``` +.... -## Completion Dashboard +=== Completion Dashboard -``` +.... COMPONENT STATUS NOTES ────────────────────────────────── ────────────────── ─────────────────────────── FOUNDATION (Phase 0) @@ -138,11 +134,11 @@ INTEGRATIONS (Phases 9-10) ────────────────────────────────────────────────────────────────────────────── OVERALL: ██░░░░░░░░ 20% Phase 0 complete. ABI+FFI+grammar done. Formal specs next. -``` +.... -## Key Dependencies +=== Key Dependencies -``` +.... PanLL ──────────────► Typell Kernel ──────────► Idris2 ABI (proofs) │ │ │ │ │ ▼ @@ -157,11 +153,11 @@ PanLL ──────────────► Typell Kernel ──── ├──► VS Code ext ──► Typell Protocol (JSON-RPC) ├──► CLI tool ─────► Typell Protocol (JSON-RPC) └──► CI/CD ────────► Typell Protocol (JSON-RPC) -``` +.... -## Critical Path +=== Critical Path -``` +.... Phase 0 (DONE) ──► Phase 1 (Specs) ──► Phase 3 (Kernel) ──► Phase 9 (PanLL) │ │ ▼ ▼ @@ -169,16 +165,17 @@ Phase 0 (DONE) ──► Phase 1 (Specs) ──► Phase 3 (Kernel) ──► Ph │ ▼ Phase 2 (Protocol) -``` +.... -## Update Protocol +=== Update Protocol This file is maintained by both humans and AI agents. When updating: -1. **After completing a component**: Change its bar and percentage -2. **After adding a component**: Add a new row in the appropriate section -3. **After architectural changes**: Update the ASCII diagram -4. **Date**: Update the `Last updated` comment at the top of this file +[arabic] +. *After completing a component*: Change its bar and percentage +. *After adding a component*: Add a new row in the appropriate section +. *After architectural changes*: Update the ASCII diagram +. *Date*: Update the `+Last updated+` comment at the top of this file -Progress bars use: `█` (filled) and `░` (empty), 10 characters wide. -Percentages: 0%, 10%, 20%, ... 100% (in 10% increments). +Progress bars use: `+█+` (filled) and `+░+` (empty), 10 characters wide. +Percentages: 0%, 10%, 20%, … 100% (in 10% increments). diff --git a/docs/decisions/0000-template.adoc b/docs/decisions/0000-template.adoc new file mode 100644 index 0000000..de603ad --- /dev/null +++ b/docs/decisions/0000-template.adoc @@ -0,0 +1,33 @@ +== [NUMBER]. [TITLE] + +Date: YYYY-MM-DD + +=== Status + +{empty}[Proposed | Accepted | Deprecated | Superseded by +link:NNNN-title.md[ADR-NNNN] | Rejected] + +=== Context + +What is the issue that we’re seeing that is motivating this decision or +change? + +=== Decision + +What is the change that we’re proposing and/or doing? + +=== Consequences + +What becomes easier or more difficult to do because of this change? + +==== Positive + +* … + +==== Negative + +* … + +==== Neutral + +* … diff --git a/docs/decisions/0000-template.md b/docs/decisions/0000-template.md deleted file mode 100644 index b20356f..0000000 --- a/docs/decisions/0000-template.md +++ /dev/null @@ -1,34 +0,0 @@ - - - -# [NUMBER]. [TITLE] - -Date: YYYY-MM-DD - -## Status - -[Proposed | Accepted | Deprecated | Superseded by [ADR-NNNN](NNNN-title.md) | Rejected] - -## Context - -What is the issue that we're seeing that is motivating this decision or change? - -## Decision - -What is the change that we're proposing and/or doing? - -## Consequences - -What becomes easier or more difficult to do because of this change? - -### Positive - -- ... - -### Negative - -- ... - -### Neutral - -- ... diff --git a/docs/decisions/0001-adopt-rsr-standard.adoc b/docs/decisions/0001-adopt-rsr-standard.adoc new file mode 100644 index 0000000..0dbd05a --- /dev/null +++ b/docs/decisions/0001-adopt-rsr-standard.adoc @@ -0,0 +1,94 @@ +== 1. Adopt Rhodium Standard Repository (RSR) Template + +Date: 2026-02-14 + +=== Status + +Accepted + +=== Context + +Managing multiple repositories with an ad-hoc approach led to +significant inconsistencies across the ecosystem. Common problems +included: + +* Missing or incomplete configuration files (SECURITY.md, +CONTRIBUTING.md, .editorconfig, etc.) +* State files (STATE.a2ml, META.a2ml, ECOSYSTEM.a2ml) placed in the +repository root instead of the canonical `+.machine_readable/+` +directory +* Duplicate or conflicting workflow definitions across repos +* No standardized entry point for AI agents interacting with +repositories +* Inconsistent bot directive configurations leading to unreliable +automation +* No contractile enforcement or Justfile automation + +Without a single source of truth for repository structure, each new repo +required manual setup and inevitably drifted from best practices over +time. + +=== Decision + +Adopt the Rhodium Standard Repository (RSR) template +(`+rsr-template-repo+`) as the canonical starting point for all new +repositories. Existing repositories will migrate incrementally as they +receive active development. + +The RSR template provides: + +* *Machine-readable state files* in `+.machine_readable/+` (STATE.a2ml, +ECOSYSTEM.a2ml, META.a2ml, AGENTIC.a2ml, NEUROSYM.a2ml, PLAYBOOK.a2ml) +* *AI manifest* (`+0-AI-MANIFEST.a2ml+`) as a universal entry point for +all AI agents +* *Bot directives* in `+.machine_readable/bot_directives/+` for bot +orchestration integration +* *Contractiles* in `+.machine_readable/contractiles/+` (k9, dust, lust, +must, trust) for policy enforcement +* *Standardized workflows* (16+ GitHub Actions workflows, all +SHA-pinned) +* *Justfile automation* with standard recipes for common tasks +* *Security and governance files*: SECURITY.md, CONTRIBUTING.md, +CODE_OF_CONDUCT.md, LICENSE (MPL-2.0) +* *Architecture Decision Records* in `+docs/decisions/+` + +New repositories are created by cloning the template: + +[source,bash] +---- +git clone https://github.com/hyperpolymath/rsr-template-repo new-repo-name +cd new-repo-name +rm -rf .git && git init +---- + +=== Consequences + +==== Positive + +* Consistency across all repositories, enforced from creation +* Automated compliance checking via `+rsr-antipattern.yml+` workflow +* Bot fleet can operate reliably across all repos with predictable +structure +* AI agents (Claude, Gemini, etc.) have a standardized entry point via +`+0-AI-MANIFEST.a2ml+` +* New contributors can onboard faster with familiar, documented +structure +* Reduced maintenance burden: fix once in template, propagate to all +repos +* Machine-readable state enables tooling and automation pipelines + +==== Negative + +* Migration effort for existing repos requires time and attention +* Learning curve for contributors unfamiliar with RSR conventions +* Template updates need propagation mechanism to existing repos +* Some repos may have unique needs that do not fit the standard template +without customization + +==== Neutral + +* Existing CI/CD pipelines continue to work; RSR workflows are additive +* Third-party dependencies retain their original licenses regardless of +repo structure +* ADR process itself is part of the template, enabling future decisions +to be recorded consistently diff --git a/docs/decisions/0001-adopt-rsr-standard.md b/docs/decisions/0001-adopt-rsr-standard.md deleted file mode 100644 index bcb6933..0000000 --- a/docs/decisions/0001-adopt-rsr-standard.md +++ /dev/null @@ -1,85 +0,0 @@ - - - -# 1. Adopt Rhodium Standard Repository (RSR) Template - -Date: 2026-02-14 - -## Status - -Accepted - -## Context - -Managing multiple repositories with an ad-hoc approach led to significant -inconsistencies across the ecosystem. Common problems included: - -- Missing or incomplete configuration files (SECURITY.md, CONTRIBUTING.md, - .editorconfig, etc.) -- State files (STATE.a2ml, META.a2ml, ECOSYSTEM.a2ml) placed in the repository - root instead of the canonical `.machine_readable/` directory -- Duplicate or conflicting workflow definitions across repos -- No standardized entry point for AI agents interacting with repositories -- Inconsistent bot directive configurations leading to unreliable automation -- No contractile enforcement or Justfile automation - -Without a single source of truth for repository structure, each new repo -required manual setup and inevitably drifted from best practices over time. - -## Decision - -Adopt the Rhodium Standard Repository (RSR) template (`rsr-template-repo`) as -the canonical starting point for all new repositories. Existing repositories -will migrate incrementally as they receive active development. - -The RSR template provides: - -- **Machine-readable state files** in `.machine_readable/` (STATE.a2ml, - ECOSYSTEM.a2ml, META.a2ml, AGENTIC.a2ml, NEUROSYM.a2ml, PLAYBOOK.a2ml) -- **AI manifest** (`0-AI-MANIFEST.a2ml`) as a universal entry point for all - AI agents -- **Bot directives** in `.machine_readable/bot_directives/` for bot orchestration integration -- **Contractiles** in `.machine_readable/contractiles/` (k9, dust, lust, must, trust) for - policy enforcement -- **Standardized workflows** (16+ GitHub Actions workflows, all SHA-pinned) -- **Justfile automation** with standard recipes for common tasks -- **Security and governance files**: SECURITY.md, CONTRIBUTING.md, - CODE_OF_CONDUCT.md, LICENSE (MPL-2.0) -- **Architecture Decision Records** in `docs/decisions/` - -New repositories are created by cloning the template: - -```bash -git clone https://github.com/hyperpolymath/rsr-template-repo new-repo-name -cd new-repo-name -rm -rf .git && git init -``` - -## Consequences - -### Positive - -- Consistency across all repositories, enforced from creation -- Automated compliance checking via `rsr-antipattern.yml` workflow -- Bot fleet can operate reliably across all repos with predictable structure -- AI agents (Claude, Gemini, etc.) have a standardized entry point via - `0-AI-MANIFEST.a2ml` -- New contributors can onboard faster with familiar, documented structure -- Reduced maintenance burden: fix once in template, propagate to all repos -- Machine-readable state enables tooling and automation pipelines - -### Negative - -- Migration effort for existing repos requires time and attention -- Learning curve for contributors unfamiliar with RSR conventions -- Template updates need propagation mechanism to existing repos -- Some repos may have unique needs that do not fit the standard template - without customization - -### Neutral - -- Existing CI/CD pipelines continue to work; RSR workflows are additive -- Third-party dependencies retain their original licenses regardless of - repo structure -- ADR process itself is part of the template, enabling future decisions - to be recorded consistently diff --git a/docs/decisions/0002-reversibility-as-typing-case-study.adoc b/docs/decisions/0002-reversibility-as-typing-case-study.adoc new file mode 100644 index 0000000..5523363 --- /dev/null +++ b/docs/decisions/0002-reversibility-as-typing-case-study.adoc @@ -0,0 +1,189 @@ +== 2. Reversibility Design as a Case Study in Type-System Power + +Date: 2026-04-12 + +=== Status + +Accepted + +=== Context + +In April 2026, the JTV v2 reversibility system for the 007 language +underwent a comprehensive design session. Five open design decisions +were closed, covering: variable mutation model, linear handle behaviour, +agent state rollback, the reversible–reverse pairing mechanism, and +branch interaction. + +During that session, three occasions arose where a proposed runtime +mechanism, tooling addition, or syntactic obligation was found to be +*entirely redundant* because the type system already expressed the same +constraint. Each time, the mechanism was dropped and the type system did +the work alone. + +These three collapses are documented here as a TypeLL case study — +concrete evidence of the principle that a well-designed type system +eliminates mechanisms rather than multiplying them. + +''''' + +=== Decision + +Record the three type-system collapses from the 007 JTV v2 reversibility +design as canonical examples of type-system power, for use in TypeLL +documentation, teaching material, and type-system design rationale. + +''''' + +=== The Three Collapses + +==== Collapse 1 — `+ExternalHandle+` type eliminates `+unsend+` primitive + +*Proposed mechanism:* A new `+unsend(h, v)+` primitive, callable only +inside `+reverse { }+` blocks, to undo a `+send+` on a linear handle. +Required a new grammar production, a new typechecker rule for +reversal-context tracking, and a handle state machine +(`+Ready → Consumed → Ready+`). + +*The type-system observation:* The handle already carries a type. If the +handle’s type is `+ExternalHandle+` (crossing an agent boundary), then +attempting to `+send+` inside a `+reversible { }+` block is a *static +error* — the same way any other type violation is caught. No new +primitive. No new runtime check. No reversal-context flag in the +typechecker. + +*What the type does:* The `+ExternalHandle+` annotation is the +enforcement mechanism. The type tells you at the call site whether the +send is reversible-safe. `+unsend+` becomes unreachable — its only +purpose was to handle the case the type system now prevents statically. + +*Lesson:* Before adding a primitive to handle a dangerous operation, ask +whether the operation’s danger is already expressible in the type +system. If the type of the target already encodes the relevant +constraint, the primitive is redundant. + +''''' + +==== Collapse 2 — `+Option+` eliminates the asymmetric-branch lint + +*Proposed mechanism:* A compiler lint warning: "`this `+branch+` is +asymmetric — some arms produce a `+ReversalToken+`, some do not. Did you +mean to handle both cases?`" Required a separate analysis pass, a +warning type, and documentation of when to suppress it. + +*The type-system observation:* At a `+branch+` join point where some +arms produce a `+ReversalToken+` and some do not, path-sensitive typing +automatically promotes the join type to `+Option>+`. +The programmer who receives `+Option>+` in scope +_already knows_ the branch was asymmetric — the type told them. And +`+match+` on `+Option>+` forces exhaustive handling of +`+Some(tok)+` and `+None+`. The programmer cannot ignore or forget the +asymmetric case. + +*What the type does:* The `+Option+`-lifting IS the warning. It is +stronger than a lint — a lint can be suppressed, ignored, or not seen in +CI. An `+Option+` that the programmer must `+match+` on cannot be +silently skipped. The type enforces the handling; the lint would merely +have suggested it. + +*Lesson:* When you find yourself wanting to add a lint for "`this +pattern is probably wrong,`" ask whether a type transformation at the +relevant join point would make the pattern impossible to ignore rather +than merely flagged. Lints are hints; types are guarantees. + +''''' + +==== Collapse 3 — `+ReversalToken+` type parameter eliminates the snapshot data structure for local bindings + +*Proposed mechanism:* A `+ReversalLog+` / snapshot data structure in the +evaluator — a `+HashMap+` capturing all local bindings +at `+reversible+` entry, restored at `+reverse+`. Required a new struct, +insertion on every binding within a reversible block, and a restore +pass. + +*The type-system observation:* In a purely functional language, local +bindings do not need snapshotting. `+let x = x + 3+` inside a +`+reversible+` block creates a _new_ binding that shadows the outer +`+x = 5+`. When the block exits, the shadow goes out of scope and the +outer binding reappears. Lexical scope provides snapshot-and-restore for +local bindings automatically and for free. The `+HashMap+` snapshot +would have been capturing something the language already maintained. + +The _only_ things that genuinely require snapshotting are `+@state+` +fields — because those escape lexical scope, persisting at agent +lifetime. And these are precisely what the `+ReversalToken+` type +parameter encodes: `+S+` is the record type of the captured `+@state+` +field values. The token IS the snapshot. No separate data structure. No +general-purpose `+HashMap+`. The type parameter makes it precise, typed, +and statically verified. + +*What the type does:* `+ReversalToken<{ @balance: Int }>+` carries +exactly what was captured, at the type level. The evaluator’s restore +path unpacks the token’s payload and rebinds those fields — a typed +operation over a known structure, not a dynamic HashMap lookup. +Decisions 1 (snapshot) and 4 (linear token) collapse into a single +mechanism: the token IS the snapshot, for the only things that actually +needed snapshotting. + +*Lesson:* Before adding a runtime data structure to track something, ask +whether the language’s existing semantics already maintain it. In a +purely functional language, immutability and lexical scoping do enormous +amounts of tracking work invisibly. The snapshot data structure was +solving a problem that didn’t exist in the language as designed. + +''''' + +=== The Pattern + +All three collapses follow the same shape: + +[arabic] +. A mechanism is proposed to handle a problem. +. On closer inspection, the type system already expresses the relevant +constraint, handles the relevant distinction, or maintains the relevant +invariant. +. The mechanism is dropped. The type system does the work. + +The result in each case: *fewer moving parts, stronger guarantees, +smaller implementation surface.* A lint that can be suppressed becomes a +type that cannot be ignored. A primitive with a dangerous footgun +becomes a type error. A runtime data structure becomes a type parameter. + +This is the direction a well-typed language should run: each addition to +the type system should eliminate at least one mechanism elsewhere. If +you are adding to the type system and also adding runtime machinery for +the same concern, the design is not finished. + +''''' + +=== Consequences + +==== Positive + +* Three concrete, worked examples of the "`type system as mechanism +eliminator`" principle, grounded in a real language design session. +* Usable directly in TypeLL documentation, teaching material on linear +types, and type-system design rationale documents. +* Demonstrates that the principle applies across different type-system +features: type annotations on values (`+ExternalHandle+`), type algebra +at join points (`+Option+`-lifting), and type parameters encoding +captured state (`+ReversalToken+`). +* The three collapses are believed to constitute a novel contribution to +the reversible computation and type theory literature, publishable as +part of the 007 / JTV v2 language papers. + +==== Negative + +* The collapses only reveal themselves during design — they require the +designer to resist the momentum toward adding a mechanism and instead +ask "`what does the type system already know?`" This is a discipline, +not a technique that can be automated. + +==== Neutral + +* The underlying reversibility design decisions are documented fully in: +** `+007/docs/session-2026-04-12-jtv-v2-reversibility-design.adoc+` +** `+julia-the-viper/docs/language/DESIGN-JTV-V2-REVERSIBILITY.md+` +** `+nextgen-languages/docs/design/jtv-007-reversibility-fork.adoc+` +* TypeLL does not implement the 007 reversibility system; this ADR +records the design patterns as transferable knowledge, not as an +implementation commitment. diff --git a/docs/decisions/0002-reversibility-as-typing-case-study.md b/docs/decisions/0002-reversibility-as-typing-case-study.md deleted file mode 100644 index e688527..0000000 --- a/docs/decisions/0002-reversibility-as-typing-case-study.md +++ /dev/null @@ -1,182 +0,0 @@ - - - -# 2. Reversibility Design as a Case Study in Type-System Power - -Date: 2026-04-12 - -## Status - -Accepted - -## Context - -In April 2026, the JTV v2 reversibility system for the 007 language underwent -a comprehensive design session. Five open design decisions were closed, covering: -variable mutation model, linear handle behaviour, agent state rollback, the -reversible–reverse pairing mechanism, and branch interaction. - -During that session, three occasions arose where a proposed runtime mechanism, -tooling addition, or syntactic obligation was found to be **entirely redundant** -because the type system already expressed the same constraint. Each time, -the mechanism was dropped and the type system did the work alone. - -These three collapses are documented here as a TypeLL case study — concrete -evidence of the principle that a well-designed type system eliminates -mechanisms rather than multiplying them. - ---- - -## Decision - -Record the three type-system collapses from the 007 JTV v2 reversibility -design as canonical examples of type-system power, for use in TypeLL -documentation, teaching material, and type-system design rationale. - ---- - -## The Three Collapses - -### Collapse 1 — `ExternalHandle` type eliminates `unsend` primitive - -**Proposed mechanism:** A new `unsend(h, v)` primitive, callable only inside -`reverse { }` blocks, to undo a `send` on a linear handle. Required a new -grammar production, a new typechecker rule for reversal-context tracking, -and a handle state machine (`Ready → Consumed → Ready`). - -**The type-system observation:** The handle already carries a type. If the -handle's type is `ExternalHandle` (crossing an agent boundary), then -attempting to `send` inside a `reversible { }` block is a **static error** — -the same way any other type violation is caught. No new primitive. No new -runtime check. No reversal-context flag in the typechecker. - -**What the type does:** The `ExternalHandle` annotation is the enforcement -mechanism. The type tells you at the call site whether the send is -reversible-safe. `unsend` becomes unreachable — its only purpose was to -handle the case the type system now prevents statically. - -**Lesson:** Before adding a primitive to handle a dangerous operation, ask -whether the operation's danger is already expressible in the type system. If -the type of the target already encodes the relevant constraint, the primitive -is redundant. - ---- - -### Collapse 2 — `Option` eliminates the asymmetric-branch lint - -**Proposed mechanism:** A compiler lint warning: "this `branch` is asymmetric -— some arms produce a `ReversalToken`, some do not. Did you mean to handle -both cases?" Required a separate analysis pass, a warning type, and -documentation of when to suppress it. - -**The type-system observation:** At a `branch` join point where some arms -produce a `ReversalToken` and some do not, path-sensitive typing automatically -promotes the join type to `Option>`. The programmer who -receives `Option>` in scope *already knows* the branch was -asymmetric — the type told them. And `match` on `Option>` -forces exhaustive handling of `Some(tok)` and `None`. The programmer cannot -ignore or forget the asymmetric case. - -**What the type does:** The `Option`-lifting IS the warning. It is stronger -than a lint — a lint can be suppressed, ignored, or not seen in CI. An -`Option` that the programmer must `match` on cannot be silently skipped. -The type enforces the handling; the lint would merely have suggested it. - -**Lesson:** When you find yourself wanting to add a lint for "this pattern -is probably wrong," ask whether a type transformation at the relevant join -point would make the pattern impossible to ignore rather than merely -flagged. Lints are hints; types are guarantees. - ---- - -### Collapse 3 — `ReversalToken` type parameter eliminates the snapshot data structure for local bindings - -**Proposed mechanism:** A `ReversalLog` / snapshot data structure in the -evaluator — a `HashMap` capturing all local bindings at -`reversible` entry, restored at `reverse`. Required a new struct, insertion -on every binding within a reversible block, and a restore pass. - -**The type-system observation:** In a purely functional language, local -bindings do not need snapshotting. `let x = x + 3` inside a `reversible` -block creates a *new* binding that shadows the outer `x = 5`. When the block -exits, the shadow goes out of scope and the outer binding reappears. Lexical -scope provides snapshot-and-restore for local bindings automatically and for -free. The `HashMap` snapshot would have been capturing something the language -already maintained. - -The *only* things that genuinely require snapshotting are `@state` fields — -because those escape lexical scope, persisting at agent lifetime. And these -are precisely what the `ReversalToken` type parameter encodes: `S` is -the record type of the captured `@state` field values. The token IS the -snapshot. No separate data structure. No general-purpose `HashMap`. The -type parameter makes it precise, typed, and statically verified. - -**What the type does:** `ReversalToken<{ @balance: Int }>` carries exactly -what was captured, at the type level. The evaluator's restore path unpacks -the token's payload and rebinds those fields — a typed operation over a -known structure, not a dynamic HashMap lookup. Decisions 1 (snapshot) and 4 -(linear token) collapse into a single mechanism: the token IS the snapshot, -for the only things that actually needed snapshotting. - -**Lesson:** Before adding a runtime data structure to track something, ask -whether the language's existing semantics already maintain it. In a purely -functional language, immutability and lexical scoping do enormous amounts of -tracking work invisibly. The snapshot data structure was solving a problem -that didn't exist in the language as designed. - ---- - -## The Pattern - -All three collapses follow the same shape: - -1. A mechanism is proposed to handle a problem. -2. On closer inspection, the type system already expresses the relevant - constraint, handles the relevant distinction, or maintains the relevant - invariant. -3. The mechanism is dropped. The type system does the work. - -The result in each case: **fewer moving parts, stronger guarantees, smaller -implementation surface.** A lint that can be suppressed becomes a type that -cannot be ignored. A primitive with a dangerous footgun becomes a type error. -A runtime data structure becomes a type parameter. - -This is the direction a well-typed language should run: each addition to the -type system should eliminate at least one mechanism elsewhere. If you are -adding to the type system and also adding runtime machinery for the same -concern, the design is not finished. - ---- - -## Consequences - -### Positive - -- Three concrete, worked examples of the "type system as mechanism eliminator" - principle, grounded in a real language design session. -- Usable directly in TypeLL documentation, teaching material on linear types, - and type-system design rationale documents. -- Demonstrates that the principle applies across different type-system features: - type annotations on values (`ExternalHandle`), type algebra at join points - (`Option`-lifting), and type parameters encoding captured state - (`ReversalToken`). -- The three collapses are believed to constitute a novel contribution to the - reversible computation and type theory literature, publishable as part of - the 007 / JTV v2 language papers. - -### Negative - -- The collapses only reveal themselves during design — they require the - designer to resist the momentum toward adding a mechanism and instead ask - "what does the type system already know?" This is a discipline, not a - technique that can be automated. - -### Neutral - -- The underlying reversibility design decisions are documented fully in: - - `007/docs/session-2026-04-12-jtv-v2-reversibility-design.adoc` - - `julia-the-viper/docs/language/DESIGN-JTV-V2-REVERSIBILITY.md` - - `nextgen-languages/docs/design/jtv-007-reversibility-fork.adoc` -- TypeLL does not implement the 007 reversibility system; this ADR records - the design patterns as transferable knowledge, not as an implementation - commitment. diff --git a/docs/decisions/README.adoc b/docs/decisions/README.adoc new file mode 100644 index 0000000..3dc7a48 --- /dev/null +++ b/docs/decisions/README.adoc @@ -0,0 +1,18 @@ +== Architecture Decision Records + +We record significant architectural decisions using +https://cognitect.com/blog/2011/11/15/documenting-architecture-decisions[Architecture +Decision Records (ADRs)], as described by Michael Nygard. + +Each ADR captures the context, decision, and consequences of a choice +that affects the project’s structure, dependencies, or conventions. + +=== Creating a new ADR + +[source,bash] +---- +just adr "Title of decision" +---- + +This creates a new numbered file in `+docs/decisions/+` from the +template at `+0000-template.md+`. diff --git a/docs/decisions/README.md b/docs/decisions/README.md deleted file mode 100644 index 1ee15bb..0000000 --- a/docs/decisions/README.md +++ /dev/null @@ -1,16 +0,0 @@ - - - -# Architecture Decision Records - -We record significant architectural decisions using [Architecture Decision Records (ADRs)](https://cognitect.com/blog/2011/11/15/documenting-architecture-decisions), as described by Michael Nygard. - -Each ADR captures the context, decision, and consequences of a choice that affects the project's structure, dependencies, or conventions. - -## Creating a new ADR - -```bash -just adr "Title of decision" -``` - -This creates a new numbered file in `docs/decisions/` from the template at `0000-template.md`. diff --git a/docs/design/ABI-FFI-README.md b/docs/design/ABI-FFI-README.adoc similarity index 74% rename from docs/design/ABI-FFI-README.md rename to docs/design/ABI-FFI-README.adoc index 07c00db..fe10c05 100644 --- a/docs/design/ABI-FFI-README.md +++ b/docs/design/ABI-FFI-README.adoc @@ -1,19 +1,22 @@ -{{~ Aditionally delete this line and fill out the template below ~}} +\{\{~ Aditionally delete this line and fill out the template below ~}} -# TYPELL ABI/FFI Documentation +== TYPELL ABI/FFI Documentation -## Overview +=== Overview -This library follows the **Hyperpolymath RSR Standard** for ABI and FFI design: +This library follows the *Hyperpolymath RSR Standard* for ABI and FFI +design: -- **ABI (Application Binary Interface)** defined in **Idris2** with formal proofs -- **FFI (Foreign Function Interface)** implemented in **Zig** for C compatibility -- **Generated C headers** bridge Idris2 ABI to Zig FFI -- **Any language** can call through standard C ABI +* *ABI (Application Binary Interface)* defined in *Idris2* with formal +proofs +* *FFI (Foreign Function Interface)* implemented in *Zig* for C +compatibility +* *Generated C headers* bridge Idris2 ABI to Zig FFI +* *Any language* can call through standard C ABI -## Architecture +=== Architecture -``` +.... ┌─────────────────────────────────────────────┐ │ ABI Definitions (Idris2) │ │ src/abi/ │ @@ -45,11 +48,11 @@ This library follows the **Hyperpolymath RSR Standard** for ABI and FFI design: │ Any Language via C ABI │ │ - Rust, ReScript, Julia, Python, etc. │ └─────────────────────────────────────────────┘ -``` +.... -## Directory Structure +=== Directory Structure -``` +.... typell/ ├── src/ │ ├── abi/ # ABI definitions (Idris2) @@ -77,15 +80,17 @@ typell/ ├── rust/ ├── rescript/ └── julia/ -``` +.... -## Why Idris2 for ABI? +=== Why Idris2 for ABI? -### 1. **Formal Verification** +==== 1. *Formal Verification* -Idris2's dependent types allow proving properties about the ABI at compile-time: +Idris2’s dependent types allow proving properties about the ABI at +compile-time: -```idris +[source,idris] +---- -- Prove struct size is correct public export exampleStructSize : HasSize ExampleStruct 16 @@ -97,13 +102,14 @@ fieldAligned : Divides 8 (offsetOf ExampleStruct.field) -- Prove ABI is platform-compatible public export abiCompatible : Compatible (ABI 1) (ABI 2) -``` +---- -### 2. **Type Safety** +==== 2. *Type Safety* Encode invariants that C/Zig cannot express: -```idris +[source,idris] +---- -- Non-null pointer guaranteed at type level data Handle : Type where MkHandle : (ptr : Bits64) -> {auto 0 nonNull : So (ptr /= 0)} -> Handle @@ -111,13 +117,14 @@ data Handle : Type where -- Array with length proof data Buffer : (n : Nat) -> Type where MkBuffer : Vect n Byte -> Buffer n -``` +---- -### 3. **Platform Abstraction** +==== 3. *Platform Abstraction* Platform-specific types with compile-time selection: -```idris +[source,idris] +---- CInt : Platform -> Type CInt Linux = Bits32 CInt Windows = Bits32 @@ -125,13 +132,14 @@ CInt Windows = Bits32 CSize : Platform -> Type CSize Linux = Bits64 CSize Windows = Bits64 -``` +---- -### 4. **Safe Evolution** +==== 4. *Safe Evolution* Prove that new ABI versions are backward-compatible: -```idris +[source,idris] +---- -- Compiler enforces compatibility abiUpgrade : ABI 1 -> ABI 2 abiUpgrade old = MkABI2 { @@ -140,71 +148,78 @@ abiUpgrade old = MkABI2 { -- Can add new fields new_features = defaults } -``` +---- -## Why Zig for FFI? +=== Why Zig for FFI? -### 1. **C ABI Compatibility** +==== 1. *C ABI Compatibility* Zig exports C-compatible functions naturally: -```zig +[source,zig] +---- export fn library_function(param: i32) i32 { return param * 2; } -``` +---- -### 2. **Memory Safety** +==== 2. *Memory Safety* Compile-time safety without runtime overhead: -```zig +[source,zig] +---- // Null check enforced at compile time const handle = init() orelse return error.InitFailed; defer free(handle); -``` +---- -### 3. **Cross-Compilation** +==== 3. *Cross-Compilation* Built-in cross-compilation to any platform: -```bash +[source,bash] +---- zig build -Dtarget=x86_64-linux zig build -Dtarget=aarch64-macos zig build -Dtarget=x86_64-windows -``` +---- -### 4. **Zero Dependencies** +==== 4. *Zero Dependencies* No runtime, no libc required (unless explicitly needed): -```zig +[source,zig] +---- // Minimal binary size pub const lib = @import("std"); // Only includes what you use -``` +---- -## Building +=== Building -### Build FFI Library +==== Build FFI Library -```bash +[source,bash] +---- cd ffi/zig zig build # Build debug zig build -Doptimize=ReleaseFast # Build optimized zig build test # Run tests -``` +---- -### Generate C Header from Idris2 ABI +==== Generate C Header from Idris2 ABI -```bash +[source,bash] +---- cd src/abi idris2 --cg c-header Types.idr -o ../../generated/abi/typell.h -``` +---- -### Cross-Compile +==== Cross-Compile -```bash +[source,bash] +---- cd ffi/zig # Linux x86_64 @@ -215,13 +230,14 @@ zig build -Dtarget=aarch64-macos # Windows x86_64 zig build -Dtarget=x86_64-windows -``` +---- -## Usage +=== Usage -### From C +==== From C -```c +[source,c] +---- #include "typell.h" int main() { @@ -237,16 +253,19 @@ int main() { typell_free(handle); return 0; } -``` +---- Compile with: -```bash + +[source,bash] +---- gcc -o example example.c -ltypell -L./zig-out/lib -``` +---- -### From Idris2 +==== From Idris2 -```idris +[source,idris] +---- import TYPELL.ABI.Foreign main : IO () @@ -259,11 +278,12 @@ main = do free handle putStrLn "Success" -``` +---- -### From Rust +==== From Rust -```rust +[source,rust] +---- #[link(name = "typell")] extern "C" { fn typell_init() -> *mut std::ffi::c_void; @@ -282,11 +302,12 @@ fn main() { typell_free(handle); } } -``` +---- -### From Julia +==== From Julia -```julia +[source,julia] +---- const libtypell = "libtypell" function init() @@ -312,27 +333,30 @@ try finally cleanup(handle) end -``` +---- -## Testing +=== Testing -### Unit Tests (Zig) +==== Unit Tests (Zig) -```bash +[source,bash] +---- cd ffi/zig zig build test -``` +---- -### Integration Tests +==== Integration Tests -```bash +[source,bash] +---- cd ffi/zig zig build test-integration -``` +---- -### ABI Verification (Idris2) +==== ABI Verification (Idris2) -```idris +[source,idris] +---- -- Compile-time verification %runElab verifyABI @@ -342,44 +366,44 @@ main = do verifyLayoutsCorrect verifyAlignmentsCorrect putStrLn "ABI verification passed" -``` +---- -## Contributing +=== Contributing When modifying the ABI/FFI: -1. **Update ABI first** (`src/abi/*.idr`) - - Modify type definitions - - Update proofs - - Ensure backward compatibility - -2. **Generate C header** - ```bash - idris2 --cg c-header src/abi/Types.idr -o generated/abi/typell.h - ``` - -3. **Update FFI implementation** (`ffi/zig/src/main.zig`) - - Implement new functions - - Match ABI types exactly - -4. **Add tests** - - Unit tests in Zig - - Integration tests - - ABI verification tests - -5. **Update documentation** - - Function signatures - - Usage examples - - Migration guide (if breaking changes) - -## License +[arabic] +. *Update ABI first* (`+src/abi/*.idr+`) +* Modify type definitions +* Update proofs +* Ensure backward compatibility +. *Generate C header* ++ +[source,bash] +---- +idris2 --cg c-header src/abi/Types.idr -o generated/abi/typell.h +---- +. *Update FFI implementation* (`+ffi/zig/src/main.zig+`) +* Implement new functions +* Match ABI types exactly +. *Add tests* +* Unit tests in Zig +* Integration tests +* ABI verification tests +. *Update documentation* +* Function signatures +* Usage examples +* Migration guide (if breaking changes) + +=== License MPL-2.0 -## See Also +=== See Also -- [Idris2 Documentation](https://idris2.readthedocs.io) -- [Zig Documentation](https://ziglang.org/documentation/master/) -- [Rhodium Standard Repositories](https://github.com/hyperpolymath/rhodium-standard-repositories) -- [FFI Migration Guide](../ffi-migration-guide.md) -- [ABI Migration Guide](../abi-migration-guide.md) +* https://idris2.readthedocs.io[Idris2 Documentation] +* https://ziglang.org/documentation/master/[Zig Documentation] +* https://github.com/hyperpolymath/rhodium-standard-repositories[Rhodium +Standard Repositories] +* link:../ffi-migration-guide.md[FFI Migration Guide] +* link:../abi-migration-guide.md[ABI Migration Guide] diff --git a/docs/design/DESIGN-2026-03-01-typell-vision.adoc b/docs/design/DESIGN-2026-03-01-typell-vision.adoc new file mode 100644 index 0000000..5ac4bae --- /dev/null +++ b/docs/design/DESIGN-2026-03-01-typell-vision.adoc @@ -0,0 +1,632 @@ +== SPDX-License-Identifier: CC-BY-SA-4.0 + +== Design Document: Typell Vision + +== Date: 2026-03-01 + +== Repo: typell + +== Author: Jonathan D.A. Jewell (hyperpolymath) + +=== Summary + +Typell is PanLL’s verification kernel — the type-theoretic engine that +provides the "`best of the best`" type system coverage for neurosymbolic +query languages. It is not a standalone IDE. It is not a pane. It is the +formal verification substrate that makes PanLL’s panes intelligent. + +=== The Problem + +PanLL (the eNASAID — Environment for NeSy-Agentic Integrated +Development) needs a type-theory backbone to deliver on its promise. The +nextgen-databases trilogy (VeriSimDB, LithoGlyph, QuandleDB) each have +or plan dependently typed query languages (VCL-dt, GQL-dt, KQL-dt). +These need to be extended to the ultimate level of type-system +strictness and connected to PanLL’s interface. + +The risk: building this as a separate IDE creates two competing tools +that both collapse under their own weight. Building it as "`just a +pane`" undersells the architectural depth required. The challenge is +making the verification infrastructure core to PanLL without interfering +with PanLL’s own development. + +=== The Solution: Layered Architecture + +Typell is to PanLL what LLVM is to Clang. One system, two separable +layers: + +.... +┌─────────────────────────────────────────────────┐ +│ PanLL (Layer 2: Development Environment) │ +│ ├─ Pane-L ←── constraints from Typell │ +│ ├─ Pane-N ←── reasoning from Typell │ +│ └─ Pane-W ←── validated results from Typell │ +│ ├─ Anti-Crash (validates Typell's output) │ +│ ├─ Vexometer (operator stress tracking) │ +│ ├─ OrbitalSync (cross-pane synchronisation) │ +│ └─ Binary Star co-orbit governance │ +└──────────────┬──────────────────────────────────┘ + │ Verification Protocol (JSON-RPC) + │ (the clean API boundary) +┌──────────────┴──────────────────────────────────┐ +│ Typell (Layer 1: Verification Kernel) │ +│ │ +│ ┌──────────────────────────────────────────┐ │ +│ │ Type Checker (Bidirectional) │ │ +│ │ ├─ Dependent types (Pi, Sigma) │ │ +│ │ ├─ Linear types (use exactly once) │ │ +│ │ ├─ Affine types (use at most once) │ │ +│ │ ├─ Session types (protocol safety) │ │ +│ │ ├─ QTT (resource quantity tracking) │ │ +│ │ ├─ Effect system (read/write/memory) │ │ +│ │ └─ Modal types (contextual access) │ │ +│ └──────────────────────────────────────────┘ │ +│ ┌──────────────────────────────────────────┐ │ +│ │ Proof Engine │ │ +│ │ ├─ Automated generation (simple proofs) │ │ +│ │ ├─ Echidna dispatch (complex proofs) │ │ +│ │ ├─ Verification (certificate checking) │ │ +│ │ ├─ Caching (proof repository) │ │ +│ │ └─ Certificates (cryptographic PCC) │ │ +│ └──────────────────────────────────────────┘ │ +│ ┌──────────────────────────────────────────┐ │ +│ │ Language Backends │ │ +│ │ ├─ VCL-dt++ (VeriSimDB) │ │ +│ │ ├─ GQL-dt++ (LithoGlyph) │ │ +│ │ └─ KQL-dt++ (QuandleDB) │ │ +│ └──────────────────────────────────────────┘ │ +│ │ +│ Formal Specs: Idris2 (src/abi/) │ +│ Implementation: Rust (src/kernel/) │ +│ FFI Bridge: Zig (ffi/zig/) │ +└──────────────────────────────────────────────────┘ + ↑ ↑ ↑ + VS Code CLI/CI Databases + extension pipelines (direct query + validation) +.... + +==== Why This Works + +[arabic] +. *PanLL can’t be hijacked* — Typell IS PanLL’s backend, not a +competitor +. *No duplication* — one verification engine, many consumers +. *Independent development* — PanLL UI can progress without waiting for +Typell +. *Graceful degradation* — PanLL works without Typell (string-based +constraints) +. *Incremental value* — each type system feature is independently useful +. *External value* — VS Code/CLI/CI users don’t need PanLL to benefit + +=== Type System Coverage: "`The Best of the Best`" + +The goal is maximal strictness — every type system feature that makes +formal verification practical for database queries. Not as a theoretical +exercise, but with tooling that makes it usable. + +==== Tier 1: Core (Must Have) + +[width="100%",cols="32%,36%,32%",options="header",] +|=== +|System |Purpose |Source +|*Dependent Types* |Types that depend on values. `+Vector 5 Int+` = +exactly 5 integers. Schema-aware queries, precise result specs, proof +obligations. |Existing in VCL-dt (Pi, Sigma types), GQL-dt (Lean 4 +refinement types) + +|*Linear Types* |Resources used exactly once. No duplicate reads, no +data leaks, transaction safety. +`+SELECT LINEAR GRAPH.* ... CONSUME AFTER 1 USE+` |New for all query +languages + +|*Session Types* |Protocol safety. Connections opened/closed correctly, +transactions atomic. `+WITH SESSION (OPEN, QUERY, CLOSE)+` |New for all +query languages + +|*Proof-Carrying Code* |Cryptographic proof certificates attached to +queries. Zero-trust verification. +`+PROOF ATTACHED { theorem, proof: "sha256:..." }+` |Partial in VCL-dt +(proof obligations), full in GQL-dt (RATIONALE clause) +|=== + +==== Tier 2: Advanced (Should Have) + +[width="100%",cols="32%,36%,32%",options="header",] +|=== +|System |Purpose |Source +|*Quantitative Type Theory* |Track resource usage quantities. Rate +limiting, cost analysis. `+USAGE LIMIT 3+` |Idris2 already has QTT +natively + +|*Effect Systems* |Explicit side effects. +`+EFFECTS { read: [GRAPH, DOCUMENT], write: [], memory: <50MB }+` +|VCL-dt has partial effect tracking + +|*Modal Types* |Contextual access. Data only available within specific +scopes. `+IN TRANSACTION tx1+` |New + +|*Affine Types* |Resources used at most once (relaxation of linear). +Graceful cleanup. |Natural extension of linear types +|=== + +==== Tier 3: Research (Could Have) + +[width="100%",cols="32%,36%,32%",options="header",] +|=== +|System |Purpose |Source +|*HoTT* |Homotopy Type Theory for query equivalence proofs |KQL-dt++ +research (knot equivalence) + +|*Equality Saturation* |E-graphs for equivalence classes (egglog) +|KQL-dt++ research + +|*Category-Theoretic Types* |Schema = category, query = natural +transformation, migration = functor |KQL-dt++ research (Spivak CQL) + +|*Substructural Types* |Unified framework for linear/affine/relevant +disciplines |Long-term unification +|=== + +=== The Verification Protocol + +The primary interface. Any consumer talks to Typell via JSON-RPC. + +==== Core Operations + +.... +typell.check(query, language) → TypeResult + Returns: types, proof obligations, effects, session protocol, errors + +typell.prove(obligation, strategy) → ProofResult + Returns: proof certificate, verification status, time taken + +typell.infer(partial_query, context) → InferenceResult + Returns: inferred types, suggestions, completions + +typell.validate(query, proof_certificate) → ValidationResult + Returns: valid/invalid, violations, counterexamples + +typell.refactor(query, transformation) → RefactorResult + Returns: rewritten query, proof of equivalence + +typell.effects(query) → EffectResult + Returns: reads, writes, memory estimate, modality access + +typell.session(interaction_sequence) → SessionResult + Returns: protocol compliance, violations, suggested fixes + +typell.drift(proof_certificate, current_data_state) → DriftResult + Returns: still valid / invalidated, repair suggestions +.... + +==== Example Flow (PanLL Integration) + +.... +Operator writes in Pane-L: + SELECT GRAPH.*, DOCUMENT.* FROM HEXAD 'entity-001' + PROOF EXISTENCE(entity-001) + EFFECTS { read: [GRAPH, DOCUMENT], memory: <50MB } + +PanLL sends to Typell via protocol: + typell.check(query, "vcl-dt++") + +Typell responds: + { + "type": "ProvedResult, [ExistenceProof]>", + "proof_obligations": [ + { "kind": "EXISTENCE", "target": "entity-001", "status": "auto-generated" } + ], + "effects": { "read": ["GRAPH", "DOCUMENT"], "write": [], "memory_estimate": "42MB" }, + "session": { "protocol": "valid", "connection_lifecycle": "single-shot" }, + "errors": [], + "warnings": [] + } + +PanLL renders in: + Pane-N: "Proof obligation: EXISTENCE(entity-001) — auto-generated. ✅" + Pane-N: "Memory effect: 42MB (under 50MB limit). ✅" + Pane-W: ProvedResult with certificate sha256:abc123... +.... + +=== Language Backend Strategy + +==== VCL-dt++ (VeriSimDB) + +*Source:* `+nextgen-databases/verisim/src/vcl/+` — ReScript +implementation *Status:* ~70% complete (parser, type checker, +bidirectional inference, proof obligations) *Strategy:* Port logic from +ReScript to Rust kernel. Extend with linear/session/QTT/effects during +port. + +Key existing components to port: - `+VQLParser.res+` — Full untyped AST +with 8-modality awareness - `+VQLTypes.res+` — Pi, Sigma, ProofType, +ProvedResultType - `+VQLBidir.res+` — Bidirectional type inference (250+ +lines) - `+VQLProofObligation.res+` — Proof obligation generation with +composition - `+VQLContext.res+` — Type context with contract registry - +`+VQLSubtyping.res+` — Subtyping relation for dependent types - +`+VQLCircuit.res+` — Custom circuit DSL for PROOF CUSTOM + +==== GQL-dt++ (LithoGlyph) + +*Source:* `+nextgen-databases/lithoglyph/gql-dt/+` — Lean 4 +implementation *Status:* 100% production ready (LSP, VS Code extension, +Zig FFI, SLSA Level 3) *Strategy:* Do NOT port. Bridge via Verification +Protocol. Lean 4’s type system is already powerful. Extend GQL-dt with +linear/session types via protocol-level composition. + +Key existing components to bridge: - Lean 4 refinement types +(BoundedNat, NonEmptyString) - RATIONALE clause (proof tracking) - LSP +server (180 LOC, already protocol-based) - Zig FFI bridge (5 core +functions) - VS Code extension (TextMate grammar, syntax highlighting) + +==== KQL-dt++ (QuandleDB) + +*Source:* Research document only +(`+nextgen-databases/quandledb/docs/design/KQL-SQL-LANDSCAPE-RESEARCH-2026-02-22.md+`) +*Status:* Research phase — no implementation *Strategy:* Design from +scratch within Typell. Category-theoretic foundation (Spivak CQL). HoTT +identity types for knot equivalence. Equality saturation (egglog) for +optimisation. + +Key design decisions needed: - Pipeline syntax (PRQL-style) +vs. declarative (SQL-style) vs. hybrid - Category-theoretic schema model +(functorial data migration) - E-graph integration for equivalence +classes - Lean 4 mathlib quandle formalisation integration + +=== Tooling Ecosystem + +What makes Typell practical, not just theoretically powerful: + +==== 1. Type-Aware Editor Experience + +When connected to PanLL (or VS Code via extension): - *Real-time type +annotations* for every clause - *Proof obligation display* ("`You must +prove EXISTENCE(entity-001)`") - *Resource usage tracking* ("`45MB +memory, reads GRAPH + DOCUMENT`") - *Linear variable colour-coding* +(used-once vs. unused vs. consumed) - *Session protocol visualisation* +(sidebar showing connection lifecycle) - *Autocompletion for proofs* +(suggests available proof kinds from schema) - *Auto-generated proof +skeletons* for common queries - *Query refactoring* (type-safe rewrites +preserving correctness) + +==== 2. Proof Assistant Integration + +* *Simple proofs:* Auto-generated by Typell kernel (existence, basic +integrity) +* *Complex proofs:* Delegated to Echidna (Z3 SMT, CVC5 SMT, E ATP) +* *Interactive proofs:* Open proof assistant pane for custom proof +construction +* *Proof repository:* Store and reuse proofs across teams/federated +nodes +* *Counterexample debugging:* When a proof fails, suggest +counterexamples +* *Proof certificates:* Compact cryptographic certificates attached to +queries + +==== 3. Compiler Pipeline + +.... +Query Source + │ + ▼ +Parse (AST) + │ + ▼ +Bidirectional Type Check +├─ Dependent type inference/checking +├─ Linear resource tracking +├─ Session protocol verification +├─ QTT resource accounting +├─ Effect inference +└─ Modal scope checking + │ + ▼ +Proof Obligation Generation + │ + ▼ +Proof Resolution +├─ Auto-generate simple proofs +├─ Dispatch complex to Echidna +└─ Verify provided certificates + │ + ▼ +ProvedResult + Certificate + │ + ▼ +Execute (database) or Display (PanLL/editor) +.... + +==== 4. Monitoring and Debugging + +* *Query tracer:* Step-through execution with proof/effect visualisation +* *Proof coverage:* Which parts of a query are proven, which are not +* *Drift dashboard:* Real-time detection of proof invalidation due to +data changes +* *Proof health metrics:* Success/failure rates, resource usage, session +compliance +* *CI/CD integration:* Automated proof checking in pipelines + +==== 5. Education and Onboarding + +* *Interactive tutorials:* Teach linear types, session types, proofs by +example +* *Query templates:* Pre-approved templates for common tasks +* *Error explanations:* User-friendly messages ("`This variable is +linear and cannot be copied`") +* *Progressive disclosure:* Start simple, reveal complexity as needed + +=== VCL-dt vs VCL-dt++ Feature Comparison + +[width="99%",cols="16%,26%,30%,28%",options="header",] +|=== +|Feature |VCL-dt (current) |VCL-dt++ (Typell) |Kernel Component +|Dependent types (Pi, Sigma) |Yes |Yes |Bidirectional type checker + +|Proof obligations (EXISTENCE, etc.) |Yes |Yes |Proof engine + +|ZKP witness generation |Yes |Yes |Proof certificates + +|*Linear types* |No |`+CONSUME AFTER n USE+` |Linear resource tracker + +|*Session types* |No |`+WITH SESSION protocol+` |Session protocol +manager + +|*Effect systems* |Partial |`+EFFECTS { Read, Write, ... }+` +|Compositional effect inference + +|*Modal types* |No |`+IN TRANSACTION state+` |Modal scope checker + +|*Proof-carrying code* |Partial (pre-conditions) +|`+PROOF ATTACHED theorem+` |Cryptographic PCC + +|*QTT* |No |`+USAGE LIMIT n+` |Quantitative type tracker +|=== + +Grammar delta: +`+nextgen-databases/typeql-experimental/docs/vcl-dtpp-grammar.ebnf+` +(199 lines) Normative spec: +`+nextgen-databases/verisim/docs/VCL-SPEC.adoc+` Appendix E + +=== Individual Feature Syntax Examples + +Each dt++ clause shown in isolation. These are independently useful — +not all-or-nothing. + +==== Linear Types — CONSUME AFTER + +[source,sql] +---- +-- Single-use: result consumed exactly once, then invalidated +SELECT GRAPH.*, DOCUMENT.* FROM HEXAD 'entity-001' + PROOF EXISTENCE(entity-001) + CONSUME AFTER 1 USE; + +-- Multi-use with budget: federation retry budget of 3 +SELECT * FROM FEDERATION '/universities/*' + WITH DRIFT STRICT + CONSUME AFTER 3 USE; +---- + +*What it prevents:* duplicate reads, data leaks, unbounded result +sharing. *Idris2 ABI:* `+(1 conn : Connection)+` for single-use, +`+(n conn : BoundedConn n)+` for multi-use. + +==== Session Types — WITH SESSION + +[source,sql] +---- +-- Read-only: can query but type system prevents mutations +SELECT GRAPH FROM HEXAD 'entity-001' + WITH SESSION ReadOnlyProtocol; + +-- Mutation: INSERT/UPDATE/DELETE allowed +INSERT HEXAD WITH DOCUMENT(title = 'New Entry') + WITH SESSION MutationProtocol; + +-- Streaming: cursor-based result batching +SELECT * FROM FEDERATION '/sensors/*' + WITH SESSION StreamProtocol; +---- + +*What it prevents:* protocol violations (writing in read-only session, +querying on closed connection, committing without opening transaction). +*State machine:* Fresh → Authenticated → InTransaction → Committed → +Closed. *Built-in protocols:* `+ReadOnlyProtocol+`, +`+MutationProtocol+`, `+StreamProtocol+`, `+BatchProtocol+`. + +==== Effect Systems — EFFECTS + +[source,sql] +---- +-- Pure read: type checker rejects any writes +SELECT GRAPH FROM HEXAD 'entity-001' + EFFECTS { Read }; + +-- Mutation with audit trail +INSERT HEXAD WITH DOCUMENT(title = 'Audited Entry') + PROOF INTEGRITY(schema-v2) + EFFECTS { Read, Write, Audit }; + +-- Federation with data transformation +SELECT VECTOR FROM FEDERATION '/cluster/*' + EFFECTS { Read, Federate, Transform }; +---- + +*What it prevents:* undeclared side effects. Checker verifies actual +operations ⊆ declared effects. *Available effects:* `+Read+`, `+Write+`, +`+Cite+`, `+Audit+`, `+Transform+`, `+Federate+` (extensible). + +==== Modal Types — IN TRANSACTION + +[source,sql] +---- +-- Only visible in committed state +SELECT GRAPH FROM HEXAD 'entity-001' + IN TRANSACTION Committed; + +-- Snapshot isolation: consistent view at query time +SELECT * FROM FEDERATION '/analytics/*' + IN TRANSACTION ReadSnapshot; +---- + +*What it prevents:* data scope leaks. Data in one transaction scope +cannot leak to another without explicit marshalling. *Transaction +states:* `+Fresh+`, `+Active+`, `+Committed+`, `+RolledBack+`, +`+ReadSnapshot+`. + +==== Proof-Carrying Code — PROOF ATTACHED + +[source,sql] +---- +-- Attach post-condition theorem to result (different from PROOF pre-condition) +SELECT GRAPH FROM HEXAD 'entity-001' + PROOF EXISTENCE(entity-001) + PROOF ATTACHED IntegrityTheorem; + +-- Freshness guarantee on federation results +SELECT * FROM FEDERATION '/realtime/*' + WITH DRIFT STRICT + PROOF ATTACHED FreshnessGuarantee; + +-- Parameterised theorem +SELECT DOCUMENT FROM HEXAD 'entity-001' + PROOF ATTACHED CrossModalConsistency(tolerance = 0.01); +---- + +*What it provides:* cryptographic proof certificates attached to query +results. Zero-trust verification — consumers can verify results without +trusting the source. *Idris2 ABI:* +`+ProvedResult : (result : QueryResult) -> (prf : Theorem) -> Type+`. + +==== Quantitative Type Theory — USAGE LIMIT + +[source,sql] +---- +-- Cap resource operations (connections, store reads, API calls) +SELECT GRAPH FROM HEXAD 'entity-001' + USAGE LIMIT 100; + +-- Federation with bounded resource budget +SELECT * FROM FEDERATION '/global/*' + WITH DRIFT TOLERATE + USAGE LIMIT 1000; +---- + +*What it provides:* bounded resource consumption across the query plan. +Different from `+LIMIT+` (which caps result rows). *Idris2 ABI:* +`+BoundedResource : (n : Nat) -> Type+`. Generalises linear types from +exact-1 to at-most-n. + +=== Example: A VCL-dt++ Query Through Typell (All Six Combined) + +[source,sql] +---- +-- Maximal strictness: linear, session-typed, effect-annotated, proof-carrying +WITH SESSION ( + OPEN CONNECTION TO FEDERATION, + QUERY LINEAR GRAPH.*, DOCUMENT.* FROM HEXAD 'entity-001' + PROOF EXISTENCE(entity-001) AND PROVENANCE(entity-001) + EFFECTS { read: [GRAPH, DOCUMENT], write: [], memory: <50MB } + USAGE LIMIT 1 + IN TRANSACTION tx1, + CLOSE CONNECTION +) AS strict_query +SELECT * FROM strict_query + PROOF ATTACHED { + theorem: "cross_modal_consistency", + proof: "sha256:def456..." + }; +---- + +Typell’s response: + +[source,json] +---- +{ + "type": "ProvedResult>, [ExistenceProof, ProvenanceProof, ConsistencyProof]>", + "proof_obligations": [ + { "kind": "EXISTENCE", "target": "entity-001", "status": "auto-generated", "time_ms": 50 }, + { "kind": "PROVENANCE", "target": "entity-001", "status": "auto-generated", "time_ms": 200 }, + { "kind": "CROSS_MODAL_CONSISTENCY", "status": "verified", "certificate": "sha256:def456..." } + ], + "linear_tracking": { "strict_query": { "uses": 1, "limit": 1, "status": "compliant" } }, + "session_protocol": { "status": "valid", "sequence": ["OPEN", "QUERY", "CLOSE"], "transaction": "tx1" }, + "effects": { "read": ["GRAPH", "DOCUMENT"], "write": [], "memory_estimate_mb": 42 }, + "modal_scope": { "transaction": "tx1", "data_accessible_only_within": true }, + "errors": [], + "warnings": [], + "certificate": { + "hash": "sha256:abc123...", + "timestamp": "2026-03-01T12:00:00Z", + "verifier": "typell-kernel-v0.1.0" + } +} +---- + +=== Implementation Technology + +[width="100%",cols="26%,37%,37%",options="header",] +|=== +|Layer |Technology |Rationale +|*Formal Specs* |Idris2 (`+src/abi/+`) |Dependent types prove type +system soundness. Zero believe_me. + +|*Kernel* |Rust (`+src/kernel/+`) |Performance, safety, Tauri +compatibility (PanLL backend). + +|*FFI* |Zig (`+ffi/zig/+`) |C ABI compatibility per hyperpolymath +standard. + +|*Protocol* |JSON-RPC |Language-agnostic, well-tooled, LSP-adjacent. + +|*GQL-dt bridge* |Lean 4 (existing) |Don’t port — bridge. Lean’s type +system is already powerful. + +|*Proof dispatch* |gRPC to Echidna |Multi-solver theorem proving (Z3, +CVC5, E). +|=== + +=== What Typell Is NOT + +* *NOT a standalone IDE* — it’s a verification engine consumed by IDEs +* *NOT a pane* — it’s the intelligence behind all three panes +* *NOT a database* — it validates queries, doesn’t store data +* *NOT a replacement for PanLL* — it IS PanLL’s backend +* *NOT a general-purpose type checker* — it’s specialised for query +languages +* *NOT a theorem prover* — it delegates complex proofs to Echidna + +=== Development Priorities + +*Rule:* PanLL is the priority. Typell must never divert effort from +PanLL. + +[arabic] +. *Phase 0 (NOW):* Capture the vision. This document. Repo scaffolding. +. *Phase 1:* Formal type system spec in Idris2 (dependent + linear + +QTT) +. *Phase 2:* Verification Protocol specification (JSON-RPC schema) +. *Phase 3:* Rust kernel — bidirectional type checker (port VCL-dt +logic) +. *Phase 4:* Rust kernel — proof engine +. *Phase 5:* PanLL integration (Pane-N + Pane-L) +. *Phase 6-8:* Language backends (VCL-dt++, GQL-dt++, KQL-dt++) +. *Phase 9-10:* VS Code extension, CLI, CI/CD plugins + +Each phase delivers independent value. No big bang. + +=== Open Questions + +[arabic] +. Should the VCL-dt ReScript code be ported to Rust, or should Typell +call VeriSimDB’s existing type checker via the protocol? +. How tightly should Typell couple with Echidna for proof dispatch? +. [line-through]#What is the right syntax for linear/session annotations +in each query language?# *RESOLVED:* VCL-dt++ grammar delta specifies +all six clauses (`+vcl-dtpp-grammar.ebnf+`). GQL-dt++ and KQL-dt++ +syntax TBD but will follow the same clause pattern. +. Should Typell define a universal query AST that all backends parse +into, or should each backend maintain its own AST? +. How does the PanLL v0.2.0 VeriSimDB integration timeline align with +Typell? diff --git a/docs/design/DESIGN-2026-03-01-typell-vision.md b/docs/design/DESIGN-2026-03-01-typell-vision.md deleted file mode 100644 index 36e73f5..0000000 --- a/docs/design/DESIGN-2026-03-01-typell-vision.md +++ /dev/null @@ -1,527 +0,0 @@ -# SPDX-License-Identifier: CC-BY-SA-4.0 -# Design Document: Typell Vision -# Date: 2026-03-01 -# Repo: typell -# Author: Jonathan D.A. Jewell (hyperpolymath) - -## Summary - -Typell is PanLL's verification kernel — the type-theoretic engine that provides -the "best of the best" type system coverage for neurosymbolic query languages. -It is not a standalone IDE. It is not a pane. It is the formal verification -substrate that makes PanLL's panes intelligent. - -## The Problem - -PanLL (the eNASAID — Environment for NeSy-Agentic Integrated Development) needs -a type-theory backbone to deliver on its promise. The nextgen-databases trilogy -(VeriSimDB, LithoGlyph, QuandleDB) each have or plan dependently typed query -languages (VCL-dt, GQL-dt, KQL-dt). These need to be extended to the ultimate -level of type-system strictness and connected to PanLL's interface. - -The risk: building this as a separate IDE creates two competing tools that both -collapse under their own weight. Building it as "just a pane" undersells the -architectural depth required. The challenge is making the verification -infrastructure core to PanLL without interfering with PanLL's own development. - -## The Solution: Layered Architecture - -Typell is to PanLL what LLVM is to Clang. One system, two separable layers: - -``` -┌─────────────────────────────────────────────────┐ -│ PanLL (Layer 2: Development Environment) │ -│ ├─ Pane-L ←── constraints from Typell │ -│ ├─ Pane-N ←── reasoning from Typell │ -│ └─ Pane-W ←── validated results from Typell │ -│ ├─ Anti-Crash (validates Typell's output) │ -│ ├─ Vexometer (operator stress tracking) │ -│ ├─ OrbitalSync (cross-pane synchronisation) │ -│ └─ Binary Star co-orbit governance │ -└──────────────┬──────────────────────────────────┘ - │ Verification Protocol (JSON-RPC) - │ (the clean API boundary) -┌──────────────┴──────────────────────────────────┐ -│ Typell (Layer 1: Verification Kernel) │ -│ │ -│ ┌──────────────────────────────────────────┐ │ -│ │ Type Checker (Bidirectional) │ │ -│ │ ├─ Dependent types (Pi, Sigma) │ │ -│ │ ├─ Linear types (use exactly once) │ │ -│ │ ├─ Affine types (use at most once) │ │ -│ │ ├─ Session types (protocol safety) │ │ -│ │ ├─ QTT (resource quantity tracking) │ │ -│ │ ├─ Effect system (read/write/memory) │ │ -│ │ └─ Modal types (contextual access) │ │ -│ └──────────────────────────────────────────┘ │ -│ ┌──────────────────────────────────────────┐ │ -│ │ Proof Engine │ │ -│ │ ├─ Automated generation (simple proofs) │ │ -│ │ ├─ Echidna dispatch (complex proofs) │ │ -│ │ ├─ Verification (certificate checking) │ │ -│ │ ├─ Caching (proof repository) │ │ -│ │ └─ Certificates (cryptographic PCC) │ │ -│ └──────────────────────────────────────────┘ │ -│ ┌──────────────────────────────────────────┐ │ -│ │ Language Backends │ │ -│ │ ├─ VCL-dt++ (VeriSimDB) │ │ -│ │ ├─ GQL-dt++ (LithoGlyph) │ │ -│ │ └─ KQL-dt++ (QuandleDB) │ │ -│ └──────────────────────────────────────────┘ │ -│ │ -│ Formal Specs: Idris2 (src/abi/) │ -│ Implementation: Rust (src/kernel/) │ -│ FFI Bridge: Zig (ffi/zig/) │ -└──────────────────────────────────────────────────┘ - ↑ ↑ ↑ - VS Code CLI/CI Databases - extension pipelines (direct query - validation) -``` - -### Why This Works - -1. **PanLL can't be hijacked** — Typell IS PanLL's backend, not a competitor -2. **No duplication** — one verification engine, many consumers -3. **Independent development** — PanLL UI can progress without waiting for Typell -4. **Graceful degradation** — PanLL works without Typell (string-based constraints) -5. **Incremental value** — each type system feature is independently useful -6. **External value** — VS Code/CLI/CI users don't need PanLL to benefit - -## Type System Coverage: "The Best of the Best" - -The goal is maximal strictness — every type system feature that makes formal -verification practical for database queries. Not as a theoretical exercise, -but with tooling that makes it usable. - -### Tier 1: Core (Must Have) - -| System | Purpose | Source | -|--------|---------|--------| -| **Dependent Types** | Types that depend on values. `Vector 5 Int` = exactly 5 integers. Schema-aware queries, precise result specs, proof obligations. | Existing in VCL-dt (Pi, Sigma types), GQL-dt (Lean 4 refinement types) | -| **Linear Types** | Resources used exactly once. No duplicate reads, no data leaks, transaction safety. `SELECT LINEAR GRAPH.* ... CONSUME AFTER 1 USE` | New for all query languages | -| **Session Types** | Protocol safety. Connections opened/closed correctly, transactions atomic. `WITH SESSION (OPEN, QUERY, CLOSE)` | New for all query languages | -| **Proof-Carrying Code** | Cryptographic proof certificates attached to queries. Zero-trust verification. `PROOF ATTACHED { theorem, proof: "sha256:..." }` | Partial in VCL-dt (proof obligations), full in GQL-dt (RATIONALE clause) | - -### Tier 2: Advanced (Should Have) - -| System | Purpose | Source | -|--------|---------|--------| -| **Quantitative Type Theory** | Track resource usage quantities. Rate limiting, cost analysis. `USAGE LIMIT 3` | Idris2 already has QTT natively | -| **Effect Systems** | Explicit side effects. `EFFECTS { read: [GRAPH, DOCUMENT], write: [], memory: <50MB }` | VCL-dt has partial effect tracking | -| **Modal Types** | Contextual access. Data only available within specific scopes. `IN TRANSACTION tx1` | New | -| **Affine Types** | Resources used at most once (relaxation of linear). Graceful cleanup. | Natural extension of linear types | - -### Tier 3: Research (Could Have) - -| System | Purpose | Source | -|--------|---------|--------| -| **HoTT** | Homotopy Type Theory for query equivalence proofs | KQL-dt++ research (knot equivalence) | -| **Equality Saturation** | E-graphs for equivalence classes (egglog) | KQL-dt++ research | -| **Category-Theoretic Types** | Schema = category, query = natural transformation, migration = functor | KQL-dt++ research (Spivak CQL) | -| **Substructural Types** | Unified framework for linear/affine/relevant disciplines | Long-term unification | - -## The Verification Protocol - -The primary interface. Any consumer talks to Typell via JSON-RPC. - -### Core Operations - -``` -typell.check(query, language) → TypeResult - Returns: types, proof obligations, effects, session protocol, errors - -typell.prove(obligation, strategy) → ProofResult - Returns: proof certificate, verification status, time taken - -typell.infer(partial_query, context) → InferenceResult - Returns: inferred types, suggestions, completions - -typell.validate(query, proof_certificate) → ValidationResult - Returns: valid/invalid, violations, counterexamples - -typell.refactor(query, transformation) → RefactorResult - Returns: rewritten query, proof of equivalence - -typell.effects(query) → EffectResult - Returns: reads, writes, memory estimate, modality access - -typell.session(interaction_sequence) → SessionResult - Returns: protocol compliance, violations, suggested fixes - -typell.drift(proof_certificate, current_data_state) → DriftResult - Returns: still valid / invalidated, repair suggestions -``` - -### Example Flow (PanLL Integration) - -``` -Operator writes in Pane-L: - SELECT GRAPH.*, DOCUMENT.* FROM HEXAD 'entity-001' - PROOF EXISTENCE(entity-001) - EFFECTS { read: [GRAPH, DOCUMENT], memory: <50MB } - -PanLL sends to Typell via protocol: - typell.check(query, "vcl-dt++") - -Typell responds: - { - "type": "ProvedResult, [ExistenceProof]>", - "proof_obligations": [ - { "kind": "EXISTENCE", "target": "entity-001", "status": "auto-generated" } - ], - "effects": { "read": ["GRAPH", "DOCUMENT"], "write": [], "memory_estimate": "42MB" }, - "session": { "protocol": "valid", "connection_lifecycle": "single-shot" }, - "errors": [], - "warnings": [] - } - -PanLL renders in: - Pane-N: "Proof obligation: EXISTENCE(entity-001) — auto-generated. ✅" - Pane-N: "Memory effect: 42MB (under 50MB limit). ✅" - Pane-W: ProvedResult with certificate sha256:abc123... -``` - -## Language Backend Strategy - -### VCL-dt++ (VeriSimDB) - -**Source:** `nextgen-databases/verisim/src/vcl/` — ReScript implementation -**Status:** ~70% complete (parser, type checker, bidirectional inference, proof obligations) -**Strategy:** Port logic from ReScript to Rust kernel. Extend with linear/session/QTT/effects during port. - -Key existing components to port: -- `VQLParser.res` — Full untyped AST with 8-modality awareness -- `VQLTypes.res` — Pi, Sigma, ProofType, ProvedResultType -- `VQLBidir.res` — Bidirectional type inference (250+ lines) -- `VQLProofObligation.res` — Proof obligation generation with composition -- `VQLContext.res` — Type context with contract registry -- `VQLSubtyping.res` — Subtyping relation for dependent types -- `VQLCircuit.res` — Custom circuit DSL for PROOF CUSTOM - -### GQL-dt++ (LithoGlyph) - -**Source:** `nextgen-databases/lithoglyph/gql-dt/` — Lean 4 implementation -**Status:** 100% production ready (LSP, VS Code extension, Zig FFI, SLSA Level 3) -**Strategy:** Do NOT port. Bridge via Verification Protocol. Lean 4's type system is already -powerful. Extend GQL-dt with linear/session types via protocol-level composition. - -Key existing components to bridge: -- Lean 4 refinement types (BoundedNat, NonEmptyString) -- RATIONALE clause (proof tracking) -- LSP server (180 LOC, already protocol-based) -- Zig FFI bridge (5 core functions) -- VS Code extension (TextMate grammar, syntax highlighting) - -### KQL-dt++ (QuandleDB) - -**Source:** Research document only (`nextgen-databases/quandledb/docs/design/KQL-SQL-LANDSCAPE-RESEARCH-2026-02-22.md`) -**Status:** Research phase — no implementation -**Strategy:** Design from scratch within Typell. Category-theoretic foundation (Spivak CQL). -HoTT identity types for knot equivalence. Equality saturation (egglog) for optimisation. - -Key design decisions needed: -- Pipeline syntax (PRQL-style) vs. declarative (SQL-style) vs. hybrid -- Category-theoretic schema model (functorial data migration) -- E-graph integration for equivalence classes -- Lean 4 mathlib quandle formalisation integration - -## Tooling Ecosystem - -What makes Typell practical, not just theoretically powerful: - -### 1. Type-Aware Editor Experience - -When connected to PanLL (or VS Code via extension): -- **Real-time type annotations** for every clause -- **Proof obligation display** ("You must prove EXISTENCE(entity-001)") -- **Resource usage tracking** ("45MB memory, reads GRAPH + DOCUMENT") -- **Linear variable colour-coding** (used-once vs. unused vs. consumed) -- **Session protocol visualisation** (sidebar showing connection lifecycle) -- **Autocompletion for proofs** (suggests available proof kinds from schema) -- **Auto-generated proof skeletons** for common queries -- **Query refactoring** (type-safe rewrites preserving correctness) - -### 2. Proof Assistant Integration - -- **Simple proofs:** Auto-generated by Typell kernel (existence, basic integrity) -- **Complex proofs:** Delegated to Echidna (Z3 SMT, CVC5 SMT, E ATP) -- **Interactive proofs:** Open proof assistant pane for custom proof construction -- **Proof repository:** Store and reuse proofs across teams/federated nodes -- **Counterexample debugging:** When a proof fails, suggest counterexamples -- **Proof certificates:** Compact cryptographic certificates attached to queries - -### 3. Compiler Pipeline - -``` -Query Source - │ - ▼ -Parse (AST) - │ - ▼ -Bidirectional Type Check -├─ Dependent type inference/checking -├─ Linear resource tracking -├─ Session protocol verification -├─ QTT resource accounting -├─ Effect inference -└─ Modal scope checking - │ - ▼ -Proof Obligation Generation - │ - ▼ -Proof Resolution -├─ Auto-generate simple proofs -├─ Dispatch complex to Echidna -└─ Verify provided certificates - │ - ▼ -ProvedResult + Certificate - │ - ▼ -Execute (database) or Display (PanLL/editor) -``` - -### 4. Monitoring and Debugging - -- **Query tracer:** Step-through execution with proof/effect visualisation -- **Proof coverage:** Which parts of a query are proven, which are not -- **Drift dashboard:** Real-time detection of proof invalidation due to data changes -- **Proof health metrics:** Success/failure rates, resource usage, session compliance -- **CI/CD integration:** Automated proof checking in pipelines - -### 5. Education and Onboarding - -- **Interactive tutorials:** Teach linear types, session types, proofs by example -- **Query templates:** Pre-approved templates for common tasks -- **Error explanations:** User-friendly messages ("This variable is linear and cannot be copied") -- **Progressive disclosure:** Start simple, reveal complexity as needed - -## VCL-dt vs VCL-dt++ Feature Comparison - -| Feature | VCL-dt (current) | VCL-dt++ (Typell) | Kernel Component | -|---------|-----------------|-------------------|------------------| -| Dependent types (Pi, Sigma) | Yes | Yes | Bidirectional type checker | -| Proof obligations (EXISTENCE, etc.) | Yes | Yes | Proof engine | -| ZKP witness generation | Yes | Yes | Proof certificates | -| **Linear types** | No | `CONSUME AFTER n USE` | Linear resource tracker | -| **Session types** | No | `WITH SESSION protocol` | Session protocol manager | -| **Effect systems** | Partial | `EFFECTS { Read, Write, ... }` | Compositional effect inference | -| **Modal types** | No | `IN TRANSACTION state` | Modal scope checker | -| **Proof-carrying code** | Partial (pre-conditions) | `PROOF ATTACHED theorem` | Cryptographic PCC | -| **QTT** | No | `USAGE LIMIT n` | Quantitative type tracker | - -Grammar delta: `nextgen-databases/typeql-experimental/docs/vcl-dtpp-grammar.ebnf` (199 lines) -Normative spec: `nextgen-databases/verisim/docs/VCL-SPEC.adoc` Appendix E - -## Individual Feature Syntax Examples - -Each dt++ clause shown in isolation. These are independently useful — not -all-or-nothing. - -### Linear Types — CONSUME AFTER - -```sql --- Single-use: result consumed exactly once, then invalidated -SELECT GRAPH.*, DOCUMENT.* FROM HEXAD 'entity-001' - PROOF EXISTENCE(entity-001) - CONSUME AFTER 1 USE; - --- Multi-use with budget: federation retry budget of 3 -SELECT * FROM FEDERATION '/universities/*' - WITH DRIFT STRICT - CONSUME AFTER 3 USE; -``` - -**What it prevents:** duplicate reads, data leaks, unbounded result sharing. -**Idris2 ABI:** `(1 conn : Connection)` for single-use, `(n conn : BoundedConn n)` for multi-use. - -### Session Types — WITH SESSION - -```sql --- Read-only: can query but type system prevents mutations -SELECT GRAPH FROM HEXAD 'entity-001' - WITH SESSION ReadOnlyProtocol; - --- Mutation: INSERT/UPDATE/DELETE allowed -INSERT HEXAD WITH DOCUMENT(title = 'New Entry') - WITH SESSION MutationProtocol; - --- Streaming: cursor-based result batching -SELECT * FROM FEDERATION '/sensors/*' - WITH SESSION StreamProtocol; -``` - -**What it prevents:** protocol violations (writing in read-only session, querying -on closed connection, committing without opening transaction). -**State machine:** Fresh → Authenticated → InTransaction → Committed → Closed. -**Built-in protocols:** `ReadOnlyProtocol`, `MutationProtocol`, `StreamProtocol`, `BatchProtocol`. - -### Effect Systems — EFFECTS - -```sql --- Pure read: type checker rejects any writes -SELECT GRAPH FROM HEXAD 'entity-001' - EFFECTS { Read }; - --- Mutation with audit trail -INSERT HEXAD WITH DOCUMENT(title = 'Audited Entry') - PROOF INTEGRITY(schema-v2) - EFFECTS { Read, Write, Audit }; - --- Federation with data transformation -SELECT VECTOR FROM FEDERATION '/cluster/*' - EFFECTS { Read, Federate, Transform }; -``` - -**What it prevents:** undeclared side effects. Checker verifies actual operations ⊆ declared effects. -**Available effects:** `Read`, `Write`, `Cite`, `Audit`, `Transform`, `Federate` (extensible). - -### Modal Types — IN TRANSACTION - -```sql --- Only visible in committed state -SELECT GRAPH FROM HEXAD 'entity-001' - IN TRANSACTION Committed; - --- Snapshot isolation: consistent view at query time -SELECT * FROM FEDERATION '/analytics/*' - IN TRANSACTION ReadSnapshot; -``` - -**What it prevents:** data scope leaks. Data in one transaction scope cannot leak -to another without explicit marshalling. -**Transaction states:** `Fresh`, `Active`, `Committed`, `RolledBack`, `ReadSnapshot`. - -### Proof-Carrying Code — PROOF ATTACHED - -```sql --- Attach post-condition theorem to result (different from PROOF pre-condition) -SELECT GRAPH FROM HEXAD 'entity-001' - PROOF EXISTENCE(entity-001) - PROOF ATTACHED IntegrityTheorem; - --- Freshness guarantee on federation results -SELECT * FROM FEDERATION '/realtime/*' - WITH DRIFT STRICT - PROOF ATTACHED FreshnessGuarantee; - --- Parameterised theorem -SELECT DOCUMENT FROM HEXAD 'entity-001' - PROOF ATTACHED CrossModalConsistency(tolerance = 0.01); -``` - -**What it provides:** cryptographic proof certificates attached to query results. -Zero-trust verification — consumers can verify results without trusting the source. -**Idris2 ABI:** `ProvedResult : (result : QueryResult) -> (prf : Theorem) -> Type`. - -### Quantitative Type Theory — USAGE LIMIT - -```sql --- Cap resource operations (connections, store reads, API calls) -SELECT GRAPH FROM HEXAD 'entity-001' - USAGE LIMIT 100; - --- Federation with bounded resource budget -SELECT * FROM FEDERATION '/global/*' - WITH DRIFT TOLERATE - USAGE LIMIT 1000; -``` - -**What it provides:** bounded resource consumption across the query plan. -Different from `LIMIT` (which caps result rows). -**Idris2 ABI:** `BoundedResource : (n : Nat) -> Type`. Generalises linear types -from exact-1 to at-most-n. - -## Example: A VCL-dt++ Query Through Typell (All Six Combined) - -```sql --- Maximal strictness: linear, session-typed, effect-annotated, proof-carrying -WITH SESSION ( - OPEN CONNECTION TO FEDERATION, - QUERY LINEAR GRAPH.*, DOCUMENT.* FROM HEXAD 'entity-001' - PROOF EXISTENCE(entity-001) AND PROVENANCE(entity-001) - EFFECTS { read: [GRAPH, DOCUMENT], write: [], memory: <50MB } - USAGE LIMIT 1 - IN TRANSACTION tx1, - CLOSE CONNECTION -) AS strict_query -SELECT * FROM strict_query - PROOF ATTACHED { - theorem: "cross_modal_consistency", - proof: "sha256:def456..." - }; -``` - -Typell's response: - -```json -{ - "type": "ProvedResult>, [ExistenceProof, ProvenanceProof, ConsistencyProof]>", - "proof_obligations": [ - { "kind": "EXISTENCE", "target": "entity-001", "status": "auto-generated", "time_ms": 50 }, - { "kind": "PROVENANCE", "target": "entity-001", "status": "auto-generated", "time_ms": 200 }, - { "kind": "CROSS_MODAL_CONSISTENCY", "status": "verified", "certificate": "sha256:def456..." } - ], - "linear_tracking": { "strict_query": { "uses": 1, "limit": 1, "status": "compliant" } }, - "session_protocol": { "status": "valid", "sequence": ["OPEN", "QUERY", "CLOSE"], "transaction": "tx1" }, - "effects": { "read": ["GRAPH", "DOCUMENT"], "write": [], "memory_estimate_mb": 42 }, - "modal_scope": { "transaction": "tx1", "data_accessible_only_within": true }, - "errors": [], - "warnings": [], - "certificate": { - "hash": "sha256:abc123...", - "timestamp": "2026-03-01T12:00:00Z", - "verifier": "typell-kernel-v0.1.0" - } -} -``` - -## Implementation Technology - -| Layer | Technology | Rationale | -|-------|-----------|-----------| -| **Formal Specs** | Idris2 (`src/abi/`) | Dependent types prove type system soundness. Zero believe_me. | -| **Kernel** | Rust (`src/kernel/`) | Performance, safety, Tauri compatibility (PanLL backend). | -| **FFI** | Zig (`ffi/zig/`) | C ABI compatibility per hyperpolymath standard. | -| **Protocol** | JSON-RPC | Language-agnostic, well-tooled, LSP-adjacent. | -| **GQL-dt bridge** | Lean 4 (existing) | Don't port — bridge. Lean's type system is already powerful. | -| **Proof dispatch** | gRPC to Echidna | Multi-solver theorem proving (Z3, CVC5, E). | - -## What Typell Is NOT - -- **NOT a standalone IDE** — it's a verification engine consumed by IDEs -- **NOT a pane** — it's the intelligence behind all three panes -- **NOT a database** — it validates queries, doesn't store data -- **NOT a replacement for PanLL** — it IS PanLL's backend -- **NOT a general-purpose type checker** — it's specialised for query languages -- **NOT a theorem prover** — it delegates complex proofs to Echidna - -## Development Priorities - -**Rule:** PanLL is the priority. Typell must never divert effort from PanLL. - -1. **Phase 0 (NOW):** Capture the vision. This document. Repo scaffolding. -2. **Phase 1:** Formal type system spec in Idris2 (dependent + linear + QTT) -3. **Phase 2:** Verification Protocol specification (JSON-RPC schema) -4. **Phase 3:** Rust kernel — bidirectional type checker (port VCL-dt logic) -5. **Phase 4:** Rust kernel — proof engine -6. **Phase 5:** PanLL integration (Pane-N + Pane-L) -7. **Phase 6-8:** Language backends (VCL-dt++, GQL-dt++, KQL-dt++) -8. **Phase 9-10:** VS Code extension, CLI, CI/CD plugins - -Each phase delivers independent value. No big bang. - -## Open Questions - -1. Should the VCL-dt ReScript code be ported to Rust, or should Typell - call VeriSimDB's existing type checker via the protocol? -2. How tightly should Typell couple with Echidna for proof dispatch? -3. ~~What is the right syntax for linear/session annotations in each query language?~~ - **RESOLVED:** VCL-dt++ grammar delta specifies all six clauses (`vcl-dtpp-grammar.ebnf`). - GQL-dt++ and KQL-dt++ syntax TBD but will follow the same clause pattern. -4. Should Typell define a universal query AST that all backends parse into, - or should each backend maintain its own AST? -5. How does the PanLL v0.2.0 VeriSimDB integration timeline align with Typell? diff --git a/docs/maintenance/MAINTENANCE-CHECKLIST.adoc b/docs/maintenance/MAINTENANCE-CHECKLIST.adoc new file mode 100644 index 0000000..a0f1d84 --- /dev/null +++ b/docs/maintenance/MAINTENANCE-CHECKLIST.adoc @@ -0,0 +1,670 @@ +== Maintenance Checklist (Cross-Repo) + +Use this as a repeatable maintenance runbook for any repo. + +Companion policy: + +* `+docs/practice/SOFTWARE-DEVELOPMENT-APPROACH.adoc+` (human-readable) +* `+.machine_readable/policies/SOFTWARE-DEVELOPMENT-APPROACH.a2ml+` +(machine-readable) + +=== Canonical Repo Baseline (Final) + +Apply this baseline to every repo unless an explicit exception is +recorded. + +==== Three-Axis Default Model + +* [ ] Axis 1 (scope priority, runs first): `+must > intend > like+` +* [ ] Axis 2 (maintenance priority): +`+corrective > adaptive > perfective+` +* [ ] Axis 3 (audit priority): `+systems > compliance > effects+` +* [ ] Perfective items are derived from Axis 1 honest state (not started +independently). + +==== Axis 1 Scoping Pass (Mandatory) + +Before Axis 2/3 execution, assemble a scoped worklist from evidence: + +* [ ] Read and reconcile: `+README+`, roadmap, status docs, maintenance +checklist, and current CI/security docs. +* [ ] Scan for unfinished markers: `+TODO+`, `+FIXME+`, `+XXX+`, +`+HACK+`, `+STUB+`, `+PARTIAL+`. +* [ ] If Idris is present, scan unsoundness markers: `+believe_me+`, +`+assert_total+`. +* [ ] Identify declared intent vs actual implementation (docs honesty +check). +* [ ] Produce a scope assembly artifact with prioritized entries under: +** `+must+` (release blockers / safety / correctness) +** `+intend+` (planned near-term) +** `+like+` (nice-to-have) + +==== Axis 2 Maintenance Execution Rules + +* [ ] Corrective first: fix breakage, defects, regressions, safety +issues. +* [ ] Adaptive second: reconcile changed scope, remove stale references, +cull no-longer-relevant work. +* [ ] Perfective third: only from current honest state established by +Axis 1 and updated by corrective/adaptive actions. + +==== Axis 3 Audit Rules + +* [ ] Verify systems are in place and actually operating. +* [ ] Verify documentation explains the real/current state (not +aspirational-only), including documented exceptions. +* [ ] Verify safety and security controls are present, active, and +evidenced. +* [ ] Verify observed effects/impacts are captured and reviewed. +* [ ] Effects audit includes: +** benchmark execution and recorded results (with before/after where +relevant) +** explicit maintainer dialogue/status review on what changed, why, and +next risks +* [ ] Audit compliance seams/compromises explicitly: +** policy exceptions are recorded with rationale, scope, and +expiry/review +** exception does not silently broaden into general policy drift +** language-policy contamination checks run (example: a single TS +exception must not trigger broad TypeScript conversion) +** run `+panic-attack+` as the compliance-audit scanner +** run ecological checking under effects (using sustainabot guidance as +current baseline) + +==== Generic Cleanup And Finish-Off Pass + +Run this pass at the end of a corrective/adaptive/perfective cycle: + +* [ ] Root cleanup: +** keep only required control/entry files in root +** move non-essential docs/reports/fixtures to canonical folders +* [ ] Remove or archive stale work: +** close out completed TODO/STUB/PARTIAL items +** cull obsolete references, dead files, and superseded plans +* [ ] Documentation finish-off: +** ensure README, roadmap, status, and wiki match actual implementation +state +** ensure machine-readable policy/state files match human docs +* [ ] Security/compliance finish-off: +** run compliance scanner (`+panic-attack+`) and resolve high-priority +findings +** verify exception register and seams/compromises are explicitly +bounded +* [ ] Effects finish-off: +** run benchmark/effects checks and record evidence +** conduct explicit maintainer review dialogue (what changed, why, +remaining risks) +* [ ] Release-prep finish-off: +** produce Must/Should/Could summary +** produce immediate corrective/adaptive/perfective next-actions list + +==== Must + +* [ ] Keep required control files at repository root: +** `+.gitignore+`, `+.gitattributes+`, `+.editorconfig+`, +`+.tool-versions+` +** `+Containerfile+` +** `+.containerignore+` (or `+.dockerignore+` only when required for +compatibility) +** `+CNAME+` and `+.nojekyll+` when using GitHub Pages/custom domain +** `+Justfile+` (root by convention) +* [ ] Keep ownership/governance files present: +** `+MAINTAINER+` in root +** `+.github/CODEOWNERS+` +* [ ] Keep machine-readable canonical structure under +`+.machine_readable/+`: +** state/meta/ecosystem files (`+*.a2ml+` or repo standard) +** `+anchors/ANCHOR.a2ml+` +** `+contractiles/+` (`+must+`, `+trust+`, `+lust+`, and related) +** `+ai/+` for AI guidance files +** `+bot_directives/+` for bot control files +* [ ] Keep contractiles/invariants present and wired: +** root `+Mustfile+` (or equivalent) with enforceable checks +** `+Trustfile+` and `+Intentfile+` present +* [ ] Keep security metadata present: +** `+.well-known/security.txt+` and relevant policy metadata +** CI security scanning configured and runnable +* [ ] Keep docs and navigation coherent: +** single navigation entry point in root (`+NAVIGATION.adoc+` or +equivalent) +** no duplicate conflicting docs for same purpose (for example both +`+.md+` and `+.adoc+` in root unless intentionally required) +* [ ] Enforce ABI/FFI purity where the policy applies: +** ABI definitions in Idris2 (`+src/abi/*.idr+`) +** FFI implementations in Zig (`+ffi/**/*.zig+`) +* [ ] Ensure quality gate includes: formatting, lint, unit/integration +tests, p2p/e2e checks, benchmark smoke, docs checks, security scan. + +==== Should + +* [ ] Keep human docs primarily in AsciiDoc (`+.adoc+`) except where +ecosystem rules require other formats (GitHub/community health, legal +text, tool-specific files). +* [ ] Keep non-essential root files moved into structured folders: +** `+docs/+` (theory/practice/whitepapers/proofs/reports) +** `+tests/+` (fixtures/outputs) +** `+licensing/+` (while retaining root `+LICENSE+` when forge detection +needs it) +* [ ] Maintain `+.well-known/+` for public metadata where applicable +(`+security.txt+`, `+humans.txt+`, `+ads.txt+` mirrors if used). +* [ ] Keep CI policy checks for doc-format conventions and canonical +file placement. +* [ ] Keep roadmap/status docs honest with dated evidence. + +==== Could + +* [ ] Maintain both human and machine views of maintenance policy from a +single source (generate one from the other). +* [ ] Add policy bots for corrective/adaptive/perfective/audit modes. +* [ ] Add repo-level architecture map (`+TOPOLOGY.md+`) and +release-readiness dashboards. +* [ ] Add per-repo exception registry for approved policy deviations. + +==== Explicit Root-Placement Rule + +Do *not* move the following out of root if you want default tool +behavior: + +* `+.gitignore+`, `+.gitattributes+`, `+.editorconfig+`, +`+.tool-versions+` +* `+Containerfile+` and ignore file +(`+.containerignore+`/`+.dockerignore+`) +* `+CNAME+` and `+.nojekyll+` for GitHub Pages +* `+Justfile+` + +=== Quick Automated Run (Script) + +Use the helper script first, then use the checklist for deeper/manual +follow-up. + +Script locations: - `+/var$REPOS_DIR/run-maintenance.sh+` - +`+~/Desktop/run-maintenance.sh+` + +[source,bash] +---- +~/Desktop/run-maintenance.sh --repo /absolute/path/to/repo --output /tmp/maintenance-report.json +jq . /tmp/maintenance-report.json +---- + +Useful flags: + +[source,bash] +---- +# Strict mode: fail process on failed checks +~/Desktop/run-maintenance.sh --repo /absolute/path/to/repo --strict + +# Skip expensive checks when needed +~/Desktop/run-maintenance.sh --repo /absolute/path/to/repo --skip-panic + +# Explicit language selection +~/Desktop/run-maintenance.sh --repo /absolute/path/to/repo --rust --python + +# Release hard-pass mode (fails on warnings or failures) +~/Desktop/run-maintenance.sh --repo /absolute/path/to/repo --fail-on-warn +---- + +Permission policy in script: - Flags `+g+w/o+w+` files/dirs - Flags +suspicious executable files - Flags shebang scripts missing executable +bit - Supports repo-local exceptions via `+.maintenance-perms-ignore+` +(regex per line) - *Audit-first by default* (non-mutating) - +`+--fix-perms+` is explicit opt-in only (never implicit) - For +reversible local hardening, pair snapshot/restore scripts where +available: - `+scripts/maintenance/perms-state.sh snapshot+` - +`+scripts/maintenance/perms-state.sh lock+` - +`+scripts/maintenance/perms-state.sh restore+` + +Important git behavior: - Git generally tracks execute bit, not full +UNIX mode matrix. - Permission hardening audits do not force +collaborators to re-unlock every file on pull. - Keep lock mode opt-in, +with restore path documented. + +[source,bash] +---- +# Audit-only (recommended default) +~/Desktop/run-maintenance.sh --repo /absolute/path/to/repo + +# Opt-in permission fixes (review output before commit) +~/Desktop/run-maintenance.sh --repo /absolute/path/to/repo --fix-perms +---- + +=== 0) Setup + +[source,bash] +---- +REPO="/absolute/path/to/repo" +cd "$REPO" +---- + +[source,bash] +---- +date -u +git rev-parse --abbrev-ref HEAD +git rev-parse HEAD +git status --porcelain +---- + +=== 1) Preflight + +* [ ] Confirm clean intent: note existing unrelated dirty files before +edits. +* [ ] Confirm runtime/toolchain versions. +* [ ] Confirm container mode expectation (`+podman+`/`+podman-compose+`) +if required. + +[source,bash] +---- +command -v rg git jq || true +command -v podman podman-compose || true +---- + +=== 2) Dependency/Env Prereqs + +* [ ] Python deps in active interpreter (for Python paths). +* [ ] Language-specific tooling installed. + +[source,bash] +---- +python -c "import sys; print(sys.executable)" +python -c "import pydantic; print(pydantic.__version__)" || echo "pydantic missing" +---- + +=== 3) Corrective Maintenance First + +* [ ] Fix regressions, runtime errors, panics, broken commands, failing +tests. +* [ ] Re-run failing checks immediately after each fix. + +=== 4) Code Health Scans + +* [ ] `+TODO/FIXME/XXX/HACK/STUB/PARTIAL+` scan. +* [ ] Permission policy scan (`+g+w/o+w+`, executable hygiene). +* [ ] ABI/FFI policy scan (if applicable: Idris2 ABI, Zig FFI). + +[source,bash] +---- +rg -n "TODO|FIXME|XXX|HACK|STUB|PARTIAL" -g '!**/.git/**' -g '!**/target/**' . +---- + +[source,bash] +---- +# Optional per-repo exceptions (regex per line): +# .maintenance-perms-ignore +# ^vendor/ +# ^third_party/ +---- + +[source,bash] +---- +# Adjust paths for your repo layout +find . -type f \( -name '*.idr' -o -name '*.idris2' -o -name '*.zig' \) +---- + +=== 5) Panic/Safety/Security Pass + +* [ ] Run `+panic-attacker+` assail/assault. +* [ ] Triage findings by severity. +* [ ] Fix high first, then medium. +* [ ] Re-run until acceptable. + +[source,bash] +---- +PANIC_BIN="/var$REPOS_DIR/panic-attacker/target/release/panic-attack" +"$PANIC_BIN" assail "$REPO" --output /tmp/assail.json --output-format json --quiet +jq -r '.weak_points | length' /tmp/assail.json +jq -r '.weak_points[] | "\(.severity)|\(.location)|\(.description)"' /tmp/assail.json +---- + +[source,bash] +---- +# If repo has production-only source builder, prefer this for baseline checks: +./scripts/ci/build-panic-assail-source.sh /tmp/panic-src +"$PANIC_BIN" assail /tmp/panic-src --output /tmp/assail-prod.json --output-format json --quiet +---- + +=== 6) Language-Specific Validation + +==== Rust + +* [ ] Format +* [ ] Lint +* [ ] Tests +* [ ] Doc tests +* [ ] Benches (where relevant) + +[source,bash] +---- +cargo fmt --all --check +cargo clippy --workspace --all-targets -- -D warnings +cargo test --workspace +cargo test --workspace --doc +# Optional targeted benchmarks: +cargo bench +---- + +==== Python + +* [ ] Format/lint +* [ ] Type check +* [ ] Tests + +[source,bash] +---- +ruff check . +ruff format --check . +mypy . +pytest -q +---- + +==== Elixir + +* [ ] Format check +* [ ] Lint/static checks +* [ ] Tests + +[source,bash] +---- +mix format --check-formatted +mix credo --strict +mix test +---- + +=== 7) Container/Runtime Checks (Podman) + +* [ ] Build container path. +* [ ] Run smoke tests inside containerized flow. +* [ ] Compare host vs container behavior for parity. + +[source,bash] +---- +podman --version +podman compose version || podman-compose --version +---- + +=== 8) Benchmark + Regression Check + +* [ ] Capture before/after metrics for touched hot paths. +* [ ] Record command + sample size + output. +* [ ] Fail change if critical path regresses beyond threshold. + +=== 9) Adaptive and Perfective Maintenance + +* [ ] Adaptive: compatibility updates (tooling/API/deprecations/config +flags). +* [ ] Perfective: clarity, docs parity, developer workflow improvements. +* [ ] Update roadmap/checklist/docs to match actual implementation +state. + +=== 10) Final QA and Release Hygiene + +* [ ] Re-run full relevant checks one final time. +* [ ] Confirm no unintended file changes. +* [ ] Commit scoped changes with clear message. +* [ ] Push and capture commit SHA. + +[source,bash] +---- +git status --short +git diff --stat +git add +git commit -m "maint: " +git push +---- + +=== 11) Maintenance Report Template + +Copy this block per repo run: + +[source,text] +---- +Repo: +Branch: +Start UTC: +End UTC: + +Scope: +- Corrective: +- Adaptive: +- Perfective: + +Checks Run: +- TODO/FIXME scan: +- Panic-attacker: +- Rust/Python/Elixir checks: +- Container checks: +- Benchmark checks: + +Findings: +- High: +- Medium: +- Low: + +Fixes Applied: +1. +2. +3. + +Validation Results: +- Tests: +- Benchmarks: +- Panic-attacker rerun: + +Artifacts: +- assail report: +- benchmark output: +- logs: + +Commit(s): +- SHA: + +Remaining Risks / Follow-ups: +1. +2. +---- + +=== 12) Language-Repo Additions (Eclexia-Specific) + +Add these checks for language/compiler repositories with formal ABI/FFI +constraints: + +* [x] README structure restored (index/TOC, audience paths, quickstart +sanity). +* [x] Wiki split by audience (laypeople/users/developers) and linked +from docs index. +* [x] Root-level clutter reduced (archive, analysis, reports relegated +to `+docs/+` subtrees). +* [x] Machine-readable docs synchronized (`+STATE.scm+`, `+META.scm+`, +`+ECOSYSTEM.scm+`, contractiles). +* [x] Human-readable docs synchronized (`+README+`, `+QUICK_STATUS+`, +roadmap, wiki home). +* [x] `+Mustfile+` invariants present and enforceable in CI. +* [x] `+Trustfile+` and `+Intentfile+` present and complete. +* [x] FFI/ABI purity policy enforced (`+*.zig+` for FFI, +`+*.idr+`/Idris2 for ABI). +* [x] `+panic-attack+` findings triaged with explicit severity budget +for release. +* [x] Point-to-point, end-to-end, and benchmark checks wired in one +quality gate. +* [x] CI workflows include quality + security + docs checks with +explicit policy. +* [x] Release audit includes corrective/adaptive/perfective + +Must/Should/Could. +* [x] Roadmap/status honesty pass completed (dates and current evidence +updated). + +=== 13) Latest Execution Record (Eclexia, 2026-02-24) + +Repo: `+/tmp/eclexia-releaseprep+` (branch `+release-prep+`, base +`+533ec9e9447f374135cc9e2e81021624ddb3c0ad+`) + +==== 13.1 Setup/Preflight + +* [x] Captured UTC timestamp and git state. +* [x] Tooling presence verified (`+rg+`, `+git+`, `+jq+`, `+cargo+`, +`+rustc+`, `+just+`). +* [x] Runtime/toolchain versions captured. +* [x] Container tooling checked (`+podman+`, `+podman-compose+`). + +==== 13.2 Corrective Maintenance + +* [x] Fixed `+panic-attack+` script path handling (`+mktemp+` output + +local fallback binary detection). +* [x] Removed Idris `+believe_me+` usage from ABI wrappers. +* [x] Fixed conformance crash-noise path by skipping known intentional +stack-overflow case in default runner. +* [x] Re-ran affected checks after each fix. + +==== 13.3 Code-Health Scans + +* [x] TODO/FIXME/STUB/PARTIAL scan run on active code paths. +* [x] ABI/FFI file inventory run (`+*.idr+`, `+*.zig+`). +* [x] Active-code marker count reduced/triaged; remaining items tracked +in release audit. + +==== 13.4 Security/Panic Pass + +* [x] `+panic-attack+` run and triaged. +* [x] Critical findings cleared (Idris unsoundness markers removed). +* [x] Current baseline: 0 weak points (Critical 0, High 0, Medium 0, Low +0). +* [x] High/Medium backlog fully eliminated. + +==== 13.5 Language Validation + +* [x] Final `+just quality-gate+` pass completed (docs, fmt, lint, unit, +conformance, integration, p2p, e2e, bench). +* [x] Additional targeted reruns completed (`+just test-conformance+`, +`+just panic-attack+`, `+just docs-check+`). + +==== 13.6 Adaptive/Perfective/Docs + +* [x] README/wiki/docs structure and indexing restored. +* [x] Root tidy/relegation pass executed. +* [x] Roadmap/status honesty update performed with current date and +evidence links. +* [x] Release audit created with corrective/adaptive/perfective + +Must/Should/Could. +* [x] Full quality-gate rerun passed after hardening updates. +* [x] ABI/FFI extension lane added without breaking stable symbols +(`+ecl_abi_get_info+`, `+ecl_tracker_create_ex+`, +`+ecl_tracker_snapshot+`). +* [x] CI quality workflow now validates sibling `+proven+` repo presence +and critical binding files. +* [x] Proven roadmap now includes explicit "`critical core, not full +rewrite`" adoption guidance and flowchart. + +==== 13.7 Outstanding Items (Explicit) + +* [x] Stable `+v1.0.0+` technical gate readiness met (quality + panic +scan clean). +* [x] Parser/codegen/runtime panic-path hardening completed for +scanner-flagged paths. +* [x] Non-eclexia `+proven+` library checked: already Idris2-first with +Zig ABI bridge; no additional integration changes required in this run. +* [ ] Remote push blocked by token scope: GitHub rejected branch updates +(`+release-prep+`, `+release-prep-pushable+`) due missing `+workflow+` +OAuth scope. + +==== 13.8 Artifacts + +* Release audit: `+docs/reports/V1-READINESS-AUDIT-2026-02-24.md+` +* Panic report: `+/tmp/eclexia-panic-attack.KZ1jpC.json+` (0 weak +points) +* Final quality gate log: `+/tmp/eclexia-quality-gate-final2.log+` (plus +post-change reruns via terminal sessions) +* Local commits: `+88fa2af+` (`+release-prep+`), `+baa3d1c+` +(`+release-prep-pushable+`) + pending new commit from this pass + +=== 12) LLM Operator Instructions + +Use this prompt with an LLM agent when you want the process run +end-to-end: + +[source,text] +---- +Run the maintenance workflow for this repo using MAINTENANCE-CHECKLIST.md. + +Required behavior: +1. Run ~/Desktop/run-maintenance.sh first and collect the JSON report. +2. Triage report results by severity: fail > warn > pass. +3. Execute corrective maintenance first (fix regressions, panics, broken tests/commands). +4. Run TODO/FIXME/stub scan and address relevant items. +5. Run panic-attacker and fix findings in priority order; rerun to confirm. +6. Run language-specific checks (Rust/Python/Elixir) relevant to this repo. +7. Run benchmark/regression checks for touched hot paths. +8. Enforce permission policy: + - no group/world writable source files unless justified + - executable bit only where intended + - use .maintenance-perms-ignore for justified exceptions +9. Update docs/roadmap/checklist entries to reflect actual state. +10. Produce a final report using the template in MAINTENANCE-CHECKLIST.md. + +Constraints: +- Do not revert unrelated existing dirty changes. +- Stage and commit only scoped intended files. +- If blocked, state exactly what is blocked and why. +---- + +=== 13) AI Execution Integrity Contract (Mandatory) + +Use this when delegating maintenance to any AI +(Gemini/Claude/ChatGPT/etc.). + +[source,text] +---- +You must execute this maintenance run with strict integrity. + +Non-negotiable rules: +1. Do not claim any step is complete unless you actually ran it. +2. Do not silently skip checklist items. If skipped, state SKIPPED + exact reason. +3. For every check, provide evidence: + - command executed + - pass/fail/warn + - key output summary + - artifact/log path +4. If a command fails, stop claiming success and report the failure clearly. +5. After each fix, re-run the relevant failing check and report the rerun result. +6. Do not hide uncertainty. If unsure, say so and run additional verification. +7. Never mark “all done” while any fail/warn remains unexplained. +8. Do not make destructive or broad permission changes by default. + - permission changes must be audit-first + - use --fix-perms only with explicit intent +9. Final output must include: + - checklist coverage matrix (each item: PASS/FAIL/WARN/SKIPPED) + - unresolved risks + - exact next actions +10. Prioritize user safety and reputation: no “looks fine” claims without evidence. +---- + +Recommended enforcement line for AI prompts: + +[source,text] +---- +Fail closed: if evidence is missing for any checklist item, treat that item as NOT DONE. +---- + +=== 14) Fleet Enrollment Automation (Gitbot + Hypatia) + +For centralized coverage across existing and new repos: + +[source,bash] +---- +cd /var$REPOS_DIR/gitbot-fleet +just enroll-repos +---- + +Optional directive write-back to repos that already have +`+.machine_readable/+`: + +[source,bash] +---- +cd /var$REPOS_DIR/gitbot-fleet +just enroll-repos /var$REPOS_DIR true +---- + +Release hard gate from fleet: + +[source,bash] +---- +cd /var$REPOS_DIR/gitbot-fleet +just maintenance-hard-pass /absolute/path/to/repo +---- diff --git a/docs/maintenance/MAINTENANCE-CHECKLIST.md b/docs/maintenance/MAINTENANCE-CHECKLIST.md deleted file mode 100644 index cf4263b..0000000 --- a/docs/maintenance/MAINTENANCE-CHECKLIST.md +++ /dev/null @@ -1,568 +0,0 @@ -# Maintenance Checklist (Cross-Repo) - -Use this as a repeatable maintenance runbook for any repo. - -Companion policy: - -- `docs/practice/SOFTWARE-DEVELOPMENT-APPROACH.adoc` (human-readable) -- `.machine_readable/policies/SOFTWARE-DEVELOPMENT-APPROACH.a2ml` (machine-readable) - -## Canonical Repo Baseline (Final) - -Apply this baseline to every repo unless an explicit exception is recorded. - -### Three-Axis Default Model - -- [ ] Axis 1 (scope priority, runs first): `must > intend > like` -- [ ] Axis 2 (maintenance priority): `corrective > adaptive > perfective` -- [ ] Axis 3 (audit priority): `systems > compliance > effects` -- [ ] Perfective items are derived from Axis 1 honest state (not started independently). - -### Axis 1 Scoping Pass (Mandatory) - -Before Axis 2/3 execution, assemble a scoped worklist from evidence: - -- [ ] Read and reconcile: `README`, roadmap, status docs, maintenance checklist, and current CI/security docs. -- [ ] Scan for unfinished markers: `TODO`, `FIXME`, `XXX`, `HACK`, `STUB`, `PARTIAL`. -- [ ] If Idris is present, scan unsoundness markers: `believe_me`, `assert_total`. -- [ ] Identify declared intent vs actual implementation (docs honesty check). -- [ ] Produce a scope assembly artifact with prioritized entries under: - - `must` (release blockers / safety / correctness) - - `intend` (planned near-term) - - `like` (nice-to-have) - -### Axis 2 Maintenance Execution Rules - -- [ ] Corrective first: fix breakage, defects, regressions, safety issues. -- [ ] Adaptive second: reconcile changed scope, remove stale references, cull no-longer-relevant work. -- [ ] Perfective third: only from current honest state established by Axis 1 and updated by corrective/adaptive actions. - -### Axis 3 Audit Rules - -- [ ] Verify systems are in place and actually operating. -- [ ] Verify documentation explains the real/current state (not aspirational-only), including documented exceptions. -- [ ] Verify safety and security controls are present, active, and evidenced. -- [ ] Verify observed effects/impacts are captured and reviewed. -- [ ] Effects audit includes: - - benchmark execution and recorded results (with before/after where relevant) - - explicit maintainer dialogue/status review on what changed, why, and next risks -- [ ] Audit compliance seams/compromises explicitly: - - policy exceptions are recorded with rationale, scope, and expiry/review - - exception does not silently broaden into general policy drift - - language-policy contamination checks run (example: a single TS exception must not trigger broad TypeScript conversion) - - run `panic-attack` as the compliance-audit scanner - - run ecological checking under effects (using sustainabot guidance as current baseline) - -### Generic Cleanup And Finish-Off Pass - -Run this pass at the end of a corrective/adaptive/perfective cycle: - -- [ ] Root cleanup: - - keep only required control/entry files in root - - move non-essential docs/reports/fixtures to canonical folders -- [ ] Remove or archive stale work: - - close out completed TODO/STUB/PARTIAL items - - cull obsolete references, dead files, and superseded plans -- [ ] Documentation finish-off: - - ensure README, roadmap, status, and wiki match actual implementation state - - ensure machine-readable policy/state files match human docs -- [ ] Security/compliance finish-off: - - run compliance scanner (`panic-attack`) and resolve high-priority findings - - verify exception register and seams/compromises are explicitly bounded -- [ ] Effects finish-off: - - run benchmark/effects checks and record evidence - - conduct explicit maintainer review dialogue (what changed, why, remaining risks) -- [ ] Release-prep finish-off: - - produce Must/Should/Could summary - - produce immediate corrective/adaptive/perfective next-actions list - -### Must - -- [ ] Keep required control files at repository root: - - `.gitignore`, `.gitattributes`, `.editorconfig`, `.tool-versions` - - `Containerfile` - - `.containerignore` (or `.dockerignore` only when required for compatibility) - - `CNAME` and `.nojekyll` when using GitHub Pages/custom domain - - `Justfile` (root by convention) -- [ ] Keep ownership/governance files present: - - `MAINTAINER` in root - - `.github/CODEOWNERS` -- [ ] Keep machine-readable canonical structure under `.machine_readable/`: - - state/meta/ecosystem files (`*.a2ml` or repo standard) - - `anchors/ANCHOR.a2ml` - - `contractiles/` (`must`, `trust`, `lust`, and related) - - `ai/` for AI guidance files - - `bot_directives/` for bot control files -- [ ] Keep contractiles/invariants present and wired: - - root `Mustfile` (or equivalent) with enforceable checks - - `Trustfile` and `Intentfile` present -- [ ] Keep security metadata present: - - `.well-known/security.txt` and relevant policy metadata - - CI security scanning configured and runnable -- [ ] Keep docs and navigation coherent: - - single navigation entry point in root (`NAVIGATION.adoc` or equivalent) - - no duplicate conflicting docs for same purpose (for example both `.md` and `.adoc` in root unless intentionally required) -- [ ] Enforce ABI/FFI purity where the policy applies: - - ABI definitions in Idris2 (`src/abi/*.idr`) - - FFI implementations in Zig (`ffi/**/*.zig`) -- [ ] Ensure quality gate includes: formatting, lint, unit/integration tests, p2p/e2e checks, benchmark smoke, docs checks, security scan. - -### Should - -- [ ] Keep human docs primarily in AsciiDoc (`.adoc`) except where ecosystem rules require other formats (GitHub/community health, legal text, tool-specific files). -- [ ] Keep non-essential root files moved into structured folders: - - `docs/` (theory/practice/whitepapers/proofs/reports) - - `tests/` (fixtures/outputs) - - `licensing/` (while retaining root `LICENSE` when forge detection needs it) -- [ ] Maintain `.well-known/` for public metadata where applicable (`security.txt`, `humans.txt`, `ads.txt` mirrors if used). -- [ ] Keep CI policy checks for doc-format conventions and canonical file placement. -- [ ] Keep roadmap/status docs honest with dated evidence. - -### Could - -- [ ] Maintain both human and machine views of maintenance policy from a single source (generate one from the other). -- [ ] Add policy bots for corrective/adaptive/perfective/audit modes. -- [ ] Add repo-level architecture map (`TOPOLOGY.md`) and release-readiness dashboards. -- [ ] Add per-repo exception registry for approved policy deviations. - -### Explicit Root-Placement Rule - -Do **not** move the following out of root if you want default tool behavior: - -- `.gitignore`, `.gitattributes`, `.editorconfig`, `.tool-versions` -- `Containerfile` and ignore file (`.containerignore`/`.dockerignore`) -- `CNAME` and `.nojekyll` for GitHub Pages -- `Justfile` - -## Quick Automated Run (Script) - -Use the helper script first, then use the checklist for deeper/manual follow-up. - -Script locations: -- `/var$REPOS_DIR/run-maintenance.sh` -- `~/Desktop/run-maintenance.sh` - -```bash -~/Desktop/run-maintenance.sh --repo /absolute/path/to/repo --output /tmp/maintenance-report.json -jq . /tmp/maintenance-report.json -``` - -Useful flags: - -```bash -# Strict mode: fail process on failed checks -~/Desktop/run-maintenance.sh --repo /absolute/path/to/repo --strict - -# Skip expensive checks when needed -~/Desktop/run-maintenance.sh --repo /absolute/path/to/repo --skip-panic - -# Explicit language selection -~/Desktop/run-maintenance.sh --repo /absolute/path/to/repo --rust --python - -# Release hard-pass mode (fails on warnings or failures) -~/Desktop/run-maintenance.sh --repo /absolute/path/to/repo --fail-on-warn -``` - -Permission policy in script: -- Flags `g+w/o+w` files/dirs -- Flags suspicious executable files -- Flags shebang scripts missing executable bit -- Supports repo-local exceptions via `.maintenance-perms-ignore` (regex per line) -- **Audit-first by default** (non-mutating) -- `--fix-perms` is explicit opt-in only (never implicit) -- For reversible local hardening, pair snapshot/restore scripts where available: - - `scripts/maintenance/perms-state.sh snapshot` - - `scripts/maintenance/perms-state.sh lock` - - `scripts/maintenance/perms-state.sh restore` - -Important git behavior: -- Git generally tracks execute bit, not full UNIX mode matrix. -- Permission hardening audits do not force collaborators to re-unlock every file on pull. -- Keep lock mode opt-in, with restore path documented. - -```bash -# Audit-only (recommended default) -~/Desktop/run-maintenance.sh --repo /absolute/path/to/repo - -# Opt-in permission fixes (review output before commit) -~/Desktop/run-maintenance.sh --repo /absolute/path/to/repo --fix-perms -``` - -## 0) Setup - -```bash -REPO="/absolute/path/to/repo" -cd "$REPO" -``` - -```bash -date -u -git rev-parse --abbrev-ref HEAD -git rev-parse HEAD -git status --porcelain -``` - -## 1) Preflight - -- [ ] Confirm clean intent: note existing unrelated dirty files before edits. -- [ ] Confirm runtime/toolchain versions. -- [ ] Confirm container mode expectation (`podman`/`podman-compose`) if required. - -```bash -command -v rg git jq || true -command -v podman podman-compose || true -``` - -## 2) Dependency/Env Prereqs - -- [ ] Python deps in active interpreter (for Python paths). -- [ ] Language-specific tooling installed. - -```bash -python -c "import sys; print(sys.executable)" -python -c "import pydantic; print(pydantic.__version__)" || echo "pydantic missing" -``` - -## 3) Corrective Maintenance First - -- [ ] Fix regressions, runtime errors, panics, broken commands, failing tests. -- [ ] Re-run failing checks immediately after each fix. - -## 4) Code Health Scans - -- [ ] `TODO/FIXME/XXX/HACK/STUB/PARTIAL` scan. -- [ ] Permission policy scan (`g+w/o+w`, executable hygiene). -- [ ] ABI/FFI policy scan (if applicable: Idris2 ABI, Zig FFI). - -```bash -rg -n "TODO|FIXME|XXX|HACK|STUB|PARTIAL" -g '!**/.git/**' -g '!**/target/**' . -``` - -```bash -# Optional per-repo exceptions (regex per line): -# .maintenance-perms-ignore -# ^vendor/ -# ^third_party/ -``` - -```bash -# Adjust paths for your repo layout -find . -type f \( -name '*.idr' -o -name '*.idris2' -o -name '*.zig' \) -``` - -## 5) Panic/Safety/Security Pass - -- [ ] Run `panic-attacker` assail/assault. -- [ ] Triage findings by severity. -- [ ] Fix high first, then medium. -- [ ] Re-run until acceptable. - -```bash -PANIC_BIN="/var$REPOS_DIR/panic-attacker/target/release/panic-attack" -"$PANIC_BIN" assail "$REPO" --output /tmp/assail.json --output-format json --quiet -jq -r '.weak_points | length' /tmp/assail.json -jq -r '.weak_points[] | "\(.severity)|\(.location)|\(.description)"' /tmp/assail.json -``` - -```bash -# If repo has production-only source builder, prefer this for baseline checks: -./scripts/ci/build-panic-assail-source.sh /tmp/panic-src -"$PANIC_BIN" assail /tmp/panic-src --output /tmp/assail-prod.json --output-format json --quiet -``` - -## 6) Language-Specific Validation - -### Rust - -- [ ] Format -- [ ] Lint -- [ ] Tests -- [ ] Doc tests -- [ ] Benches (where relevant) - -```bash -cargo fmt --all --check -cargo clippy --workspace --all-targets -- -D warnings -cargo test --workspace -cargo test --workspace --doc -# Optional targeted benchmarks: -cargo bench -``` - -### Python - -- [ ] Format/lint -- [ ] Type check -- [ ] Tests - -```bash -ruff check . -ruff format --check . -mypy . -pytest -q -``` - -### Elixir - -- [ ] Format check -- [ ] Lint/static checks -- [ ] Tests - -```bash -mix format --check-formatted -mix credo --strict -mix test -``` - -## 7) Container/Runtime Checks (Podman) - -- [ ] Build container path. -- [ ] Run smoke tests inside containerized flow. -- [ ] Compare host vs container behavior for parity. - -```bash -podman --version -podman compose version || podman-compose --version -``` - -## 8) Benchmark + Regression Check - -- [ ] Capture before/after metrics for touched hot paths. -- [ ] Record command + sample size + output. -- [ ] Fail change if critical path regresses beyond threshold. - -## 9) Adaptive and Perfective Maintenance - -- [ ] Adaptive: compatibility updates (tooling/API/deprecations/config flags). -- [ ] Perfective: clarity, docs parity, developer workflow improvements. -- [ ] Update roadmap/checklist/docs to match actual implementation state. - -## 10) Final QA and Release Hygiene - -- [ ] Re-run full relevant checks one final time. -- [ ] Confirm no unintended file changes. -- [ ] Commit scoped changes with clear message. -- [ ] Push and capture commit SHA. - -```bash -git status --short -git diff --stat -git add -git commit -m "maint: " -git push -``` - -## 11) Maintenance Report Template - -Copy this block per repo run: - -```text -Repo: -Branch: -Start UTC: -End UTC: - -Scope: -- Corrective: -- Adaptive: -- Perfective: - -Checks Run: -- TODO/FIXME scan: -- Panic-attacker: -- Rust/Python/Elixir checks: -- Container checks: -- Benchmark checks: - -Findings: -- High: -- Medium: -- Low: - -Fixes Applied: -1. -2. -3. - -Validation Results: -- Tests: -- Benchmarks: -- Panic-attacker rerun: - -Artifacts: -- assail report: -- benchmark output: -- logs: - -Commit(s): -- SHA: - -Remaining Risks / Follow-ups: -1. -2. -``` - -## 12) Language-Repo Additions (Eclexia-Specific) - -Add these checks for language/compiler repositories with formal ABI/FFI constraints: - -- [x] README structure restored (index/TOC, audience paths, quickstart sanity). -- [x] Wiki split by audience (laypeople/users/developers) and linked from docs index. -- [x] Root-level clutter reduced (archive, analysis, reports relegated to `docs/` subtrees). -- [x] Machine-readable docs synchronized (`STATE.scm`, `META.scm`, `ECOSYSTEM.scm`, contractiles). -- [x] Human-readable docs synchronized (`README`, `QUICK_STATUS`, roadmap, wiki home). -- [x] `Mustfile` invariants present and enforceable in CI. -- [x] `Trustfile` and `Intentfile` present and complete. -- [x] FFI/ABI purity policy enforced (`*.zig` for FFI, `*.idr`/Idris2 for ABI). -- [x] `panic-attack` findings triaged with explicit severity budget for release. -- [x] Point-to-point, end-to-end, and benchmark checks wired in one quality gate. -- [x] CI workflows include quality + security + docs checks with explicit policy. -- [x] Release audit includes corrective/adaptive/perfective + Must/Should/Could. -- [x] Roadmap/status honesty pass completed (dates and current evidence updated). - -## 13) Latest Execution Record (Eclexia, 2026-02-24) - -Repo: `/tmp/eclexia-releaseprep` (branch `release-prep`, base `533ec9e9447f374135cc9e2e81021624ddb3c0ad`) - -### 13.1 Setup/Preflight - -- [x] Captured UTC timestamp and git state. -- [x] Tooling presence verified (`rg`, `git`, `jq`, `cargo`, `rustc`, `just`). -- [x] Runtime/toolchain versions captured. -- [x] Container tooling checked (`podman`, `podman-compose`). - -### 13.2 Corrective Maintenance - -- [x] Fixed `panic-attack` script path handling (`mktemp` output + local fallback binary detection). -- [x] Removed Idris `believe_me` usage from ABI wrappers. -- [x] Fixed conformance crash-noise path by skipping known intentional stack-overflow case in default runner. -- [x] Re-ran affected checks after each fix. - -### 13.3 Code-Health Scans - -- [x] TODO/FIXME/STUB/PARTIAL scan run on active code paths. -- [x] ABI/FFI file inventory run (`*.idr`, `*.zig`). -- [x] Active-code marker count reduced/triaged; remaining items tracked in release audit. - -### 13.4 Security/Panic Pass - -- [x] `panic-attack` run and triaged. -- [x] Critical findings cleared (Idris unsoundness markers removed). -- [x] Current baseline: 0 weak points (Critical 0, High 0, Medium 0, Low 0). -- [x] High/Medium backlog fully eliminated. - -### 13.5 Language Validation - -- [x] Final `just quality-gate` pass completed (docs, fmt, lint, unit, conformance, integration, p2p, e2e, bench). -- [x] Additional targeted reruns completed (`just test-conformance`, `just panic-attack`, `just docs-check`). - -### 13.6 Adaptive/Perfective/Docs - -- [x] README/wiki/docs structure and indexing restored. -- [x] Root tidy/relegation pass executed. -- [x] Roadmap/status honesty update performed with current date and evidence links. -- [x] Release audit created with corrective/adaptive/perfective + Must/Should/Could. -- [x] Full quality-gate rerun passed after hardening updates. -- [x] ABI/FFI extension lane added without breaking stable symbols (`ecl_abi_get_info`, `ecl_tracker_create_ex`, `ecl_tracker_snapshot`). -- [x] CI quality workflow now validates sibling `proven` repo presence and critical binding files. -- [x] Proven roadmap now includes explicit "critical core, not full rewrite" adoption guidance and flowchart. - -### 13.7 Outstanding Items (Explicit) - -- [x] Stable `v1.0.0` technical gate readiness met (quality + panic scan clean). -- [x] Parser/codegen/runtime panic-path hardening completed for scanner-flagged paths. -- [x] Non-eclexia `proven` library checked: already Idris2-first with Zig ABI bridge; no additional integration changes required in this run. -- [ ] Remote push blocked by token scope: GitHub rejected branch updates (`release-prep`, `release-prep-pushable`) due missing `workflow` OAuth scope. - -### 13.8 Artifacts - -- Release audit: `docs/reports/V1-READINESS-AUDIT-2026-02-24.md` -- Panic report: `/tmp/eclexia-panic-attack.KZ1jpC.json` (0 weak points) -- Final quality gate log: `/tmp/eclexia-quality-gate-final2.log` (plus post-change reruns via terminal sessions) -- Local commits: `88fa2af` (`release-prep`), `baa3d1c` (`release-prep-pushable`) + pending new commit from this pass - -## 12) LLM Operator Instructions - -Use this prompt with an LLM agent when you want the process run end-to-end: - -```text -Run the maintenance workflow for this repo using MAINTENANCE-CHECKLIST.md. - -Required behavior: -1. Run ~/Desktop/run-maintenance.sh first and collect the JSON report. -2. Triage report results by severity: fail > warn > pass. -3. Execute corrective maintenance first (fix regressions, panics, broken tests/commands). -4. Run TODO/FIXME/stub scan and address relevant items. -5. Run panic-attacker and fix findings in priority order; rerun to confirm. -6. Run language-specific checks (Rust/Python/Elixir) relevant to this repo. -7. Run benchmark/regression checks for touched hot paths. -8. Enforce permission policy: - - no group/world writable source files unless justified - - executable bit only where intended - - use .maintenance-perms-ignore for justified exceptions -9. Update docs/roadmap/checklist entries to reflect actual state. -10. Produce a final report using the template in MAINTENANCE-CHECKLIST.md. - -Constraints: -- Do not revert unrelated existing dirty changes. -- Stage and commit only scoped intended files. -- If blocked, state exactly what is blocked and why. -``` - -## 13) AI Execution Integrity Contract (Mandatory) - -Use this when delegating maintenance to any AI (Gemini/Claude/ChatGPT/etc.). - -```text -You must execute this maintenance run with strict integrity. - -Non-negotiable rules: -1. Do not claim any step is complete unless you actually ran it. -2. Do not silently skip checklist items. If skipped, state SKIPPED + exact reason. -3. For every check, provide evidence: - - command executed - - pass/fail/warn - - key output summary - - artifact/log path -4. If a command fails, stop claiming success and report the failure clearly. -5. After each fix, re-run the relevant failing check and report the rerun result. -6. Do not hide uncertainty. If unsure, say so and run additional verification. -7. Never mark “all done” while any fail/warn remains unexplained. -8. Do not make destructive or broad permission changes by default. - - permission changes must be audit-first - - use --fix-perms only with explicit intent -9. Final output must include: - - checklist coverage matrix (each item: PASS/FAIL/WARN/SKIPPED) - - unresolved risks - - exact next actions -10. Prioritize user safety and reputation: no “looks fine” claims without evidence. -``` - -Recommended enforcement line for AI prompts: - -```text -Fail closed: if evidence is missing for any checklist item, treat that item as NOT DONE. -``` - -## 14) Fleet Enrollment Automation (Gitbot + Hypatia) - -For centralized coverage across existing and new repos: - -```bash -cd /var$REPOS_DIR/gitbot-fleet -just enroll-repos -``` - -Optional directive write-back to repos that already have `.machine_readable/`: - -```bash -cd /var$REPOS_DIR/gitbot-fleet -just enroll-repos /var$REPOS_DIR true -``` - -Release hard gate from fleet: - -```bash -cd /var$REPOS_DIR/gitbot-fleet -just maintenance-hard-pass /absolute/path/to/repo -``` diff --git a/docs/onboarding/llm-warmup-dev.adoc b/docs/onboarding/llm-warmup-dev.adoc new file mode 100644 index 0000000..7e6860c --- /dev/null +++ b/docs/onboarding/llm-warmup-dev.adoc @@ -0,0 +1,19 @@ +== LLM Warmup — typell (Developer) + +=== What is typell? + +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/docs/onboarding/llm-warmup-dev.md b/docs/onboarding/llm-warmup-dev.md deleted file mode 100644 index 14cb7f1..0000000 --- a/docs/onboarding/llm-warmup-dev.md +++ /dev/null @@ -1,16 +0,0 @@ -# LLM Warmup — typell (Developer) - -## What is typell? -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/docs/onboarding/llm-warmup-user.adoc b/docs/onboarding/llm-warmup-user.adoc new file mode 100644 index 0000000..0c3f234 --- /dev/null +++ b/docs/onboarding/llm-warmup-user.adoc @@ -0,0 +1,19 @@ +== LLM Warmup — typell (User) + +=== What is typell? + +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/docs/onboarding/llm-warmup-user.md b/docs/onboarding/llm-warmup-user.md deleted file mode 100644 index ab107fe..0000000 --- a/docs/onboarding/llm-warmup-user.md +++ /dev/null @@ -1,16 +0,0 @@ -# LLM Warmup — typell (User) - -## What is typell? -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/docs/reports/audit/audit-2026-04-04.adoc b/docs/reports/audit/audit-2026-04-04.adoc new file mode 100644 index 0000000..a177672 --- /dev/null +++ b/docs/reports/audit/audit-2026-04-04.adoc @@ -0,0 +1,86 @@ +== Audit Report — typell (2026-04-04) + +=== Summary + +Typell is PanLL’s type-theoretic verification engine featuring dependent +types, linear types, and session types. The codebase demonstrates strong +RSR compliance with complete documentation standards, CI/CD automation, +and zero dangerous patterns detected in actual code. The project +maintains a "`zero believe_me`" policy enforced through both automated +scanning and policy documentation. + +=== Findings + +==== Critical + +* *ZERO dangerous patterns detected* — No actual instances of +believe_me, assert_total, Admitted, sorry, unsafeCoerce, or Obj.magic in +source code (excluding docs/rules/tests) +* *RSR compliance complete* — All required artifacts present and +maintained + +==== High + +None identified. + +==== Medium + +* Test coverage exists but test file inventory incomplete in initial +scan (test discovery needed) +* CI pipeline has 14 workflows including formal proof validation + +=== RSR Compliance + +* *EXPLAINME.adoc*: present ✓ +* *0-AI-MANIFEST.a2ml*: present ✓ +* *.machine_readable/*: present ✓ +* *SECURITY.md*: present ✓ +* *CONTRIBUTING.md*: present ✓ + +=== Test Coverage + +Typell includes extensive testing infrastructure: + +* *Cargo test suites*: property_test, e2e_test, integration-test suites +* *Test infrastructure*: 63 source files across src/abi, crates/ +* *Proof validation*: Idris2 totality checks via CI +* *E2E testing*: .github/workflows/e2e.yml with formal proof scanning +* *CI dangerous pattern scanning*: grep for +believe_me/assert_total/sorry/Admitted/unsafeCoerce in CI + +=== Proof Debt + +*Status: CLEAN* + +* Proof integrity actively enforced via CI (e2e.yml lines 69-75) +* Policy declaration (0-AI-MANIFEST.a2ml line 169-178): "`No +believe_me`" +* All Idris2 ABI proofs documented as genuine in src/abi/README.md +* Architectural Decision Record ADR-010 (2026-03-01) formalizes "`Zero +believe_me policy`" + +Dangerous pattern counts from documentation: - believe_me: 0 (verified +by policy + CI + docs) - assert_total: 0 (verified by policy + CI + +docs) - Admitted (Coq): 0 (verified by policy enforcement) - sorry: 0 +(verified by policy enforcement) - unsafeCoerce: 0 (verified by policy +enforcement) - Obj.magic: 0 (verified by policy enforcement) + +=== Verdict + +*PUBLISHABLE NOW* + +This is a mature, well-engineered verification kernel suitable for +production use in formal verification contexts. The "`zero believe_me`" +policy is not merely aspirational—it’s enforced through: 1. CI scanning +(e2e.yml) 2. Architectural decision documentation (ADR-010) 3. +Maintenance checklists (.machine_readable/policies/) 4. Pull request +templates with explicit checks 5. Machine-readable policy declarations +(MUST.contractile) + +The codebase demonstrates exemplary standards for safety-critical +infrastructure. No repairs needed. + +''''' + +*Audited by*: M2 estate audit (2026-04-04) *Confidence*: HIGH +*Recommendation*: SHIP AS-IS diff --git a/docs/reports/audit/audit-2026-04-04.md b/docs/reports/audit/audit-2026-04-04.md deleted file mode 100644 index 52b57d1..0000000 --- a/docs/reports/audit/audit-2026-04-04.md +++ /dev/null @@ -1,75 +0,0 @@ -# Audit Report — typell (2026-04-04) - -## Summary - -Typell is PanLL's type-theoretic verification engine featuring dependent types, linear types, and session types. The codebase demonstrates strong RSR compliance with complete documentation standards, CI/CD automation, and zero dangerous patterns detected in actual code. The project maintains a "zero believe_me" policy enforced through both automated scanning and policy documentation. - -## Findings - -### Critical - -- **ZERO dangerous patterns detected** — No actual instances of believe_me, assert_total, Admitted, sorry, unsafeCoerce, or Obj.magic in source code (excluding docs/rules/tests) -- **RSR compliance complete** — All required artifacts present and maintained - -### High - -None identified. - -### Medium - -- Test coverage exists but test file inventory incomplete in initial scan (test discovery needed) -- CI pipeline has 14 workflows including formal proof validation - -## RSR Compliance - -- **EXPLAINME.adoc**: present ✓ -- **0-AI-MANIFEST.a2ml**: present ✓ -- **.machine_readable/**: present ✓ -- **SECURITY.md**: present ✓ -- **CONTRIBUTING.md**: present ✓ - -## Test Coverage - -Typell includes extensive testing infrastructure: - -- **Cargo test suites**: property_test, e2e_test, integration-test suites -- **Test infrastructure**: 63 source files across src/abi, crates/ -- **Proof validation**: Idris2 totality checks via CI -- **E2E testing**: .github/workflows/e2e.yml with formal proof scanning -- **CI dangerous pattern scanning**: grep for believe_me/assert_total/sorry/Admitted/unsafeCoerce in CI - -## Proof Debt - -**Status: CLEAN** - -- Proof integrity actively enforced via CI (e2e.yml lines 69-75) -- Policy declaration (0-AI-MANIFEST.a2ml line 169-178): "No believe_me" -- All Idris2 ABI proofs documented as genuine in src/abi/README.md -- Architectural Decision Record ADR-010 (2026-03-01) formalizes "Zero believe_me policy" - -Dangerous pattern counts from documentation: -- believe_me: 0 (verified by policy + CI + docs) -- assert_total: 0 (verified by policy + CI + docs) -- Admitted (Coq): 0 (verified by policy enforcement) -- sorry: 0 (verified by policy enforcement) -- unsafeCoerce: 0 (verified by policy enforcement) -- Obj.magic: 0 (verified by policy enforcement) - -## Verdict - -**PUBLISHABLE NOW** - -This is a mature, well-engineered verification kernel suitable for production use in formal verification contexts. The "zero believe_me" policy is not merely aspirational—it's enforced through: -1. CI scanning (e2e.yml) -2. Architectural decision documentation (ADR-010) -3. Maintenance checklists (.machine_readable/policies/) -4. Pull request templates with explicit checks -5. Machine-readable policy declarations (MUST.contractile) - -The codebase demonstrates exemplary standards for safety-critical infrastructure. No repairs needed. - ---- - -**Audited by**: M2 estate audit (2026-04-04) -**Confidence**: HIGH -**Recommendation**: SHIP AS-IS diff --git a/docs/status/PROOF-NEEDS.adoc b/docs/status/PROOF-NEEDS.adoc new file mode 100644 index 0000000..67349c4 --- /dev/null +++ b/docs/status/PROOF-NEEDS.adoc @@ -0,0 +1,50 @@ +== PROOF-NEEDS.md + +=== Current State + +* *LOC*: ~17,000 +* *Languages*: Rust, Idris2, Zig +* *Existing ABI proofs*: `+src/abi/*.idr+` (template-level) +* *Dangerous patterns*: None detected in source files + +=== What Needs Proving + +==== Core Type System (crates/typell-core/) + +* `+check.rs+` — type checking for the 10-level type system +* `+infer.rs+` — type inference +* `+unify.rs+` — unification algorithm +* `+proof.rs+` (495 lines) — proof generation/checking in Rust +* `+linear.rs+` — linear type tracking +* `+qtt.rs+` — quantitative type theory +* `+session.rs+` — session types +* `+effects.rs+` — effect system +* Prove: type checking is sound (well-typed programs do not get stuck) +* Prove: type inference is complete (finds principal types when they +exist) +* Prove: unification terminates and is most general + +==== Language Bridges (14 crates) + +* Each `+typell-*+` crate bridges TypeLL to a nextgen language +* Prove: bridge translations preserve typing judgments +* Prove: subtyping relationships are transitive across bridges + +==== Dimensional Types (crates/typell-core/src/dimensional.rs) + +* Physical dimension tracking in types +* Prove: dimensional analysis is consistent (no unit mismatch can pass +type checking) + +=== Recommended Prover + +* *Idris2* for the type system metatheory (soundness, completeness) +* *Agda* alternative for the unification/inference proofs (strong +equational reasoning) + +=== Priority + +*HIGH* — TypeLL is PanLL’s verification kernel. If the type system is +unsound, every downstream language that relies on TypeLL levels has +unsound guarantees. The 10-level type hierarchy is the central claim of +the project and must be formally verified. diff --git a/docs/status/PROOF-NEEDS.md b/docs/status/PROOF-NEEDS.md deleted file mode 100644 index e908957..0000000 --- a/docs/status/PROOF-NEEDS.md +++ /dev/null @@ -1,42 +0,0 @@ -# PROOF-NEEDS.md - - -## Current State - -- **LOC**: ~17,000 -- **Languages**: Rust, Idris2, Zig -- **Existing ABI proofs**: `src/abi/*.idr` (template-level) -- **Dangerous patterns**: None detected in source files - -## What Needs Proving - -### Core Type System (crates/typell-core/) -- `check.rs` — type checking for the 10-level type system -- `infer.rs` — type inference -- `unify.rs` — unification algorithm -- `proof.rs` (495 lines) — proof generation/checking in Rust -- `linear.rs` — linear type tracking -- `qtt.rs` — quantitative type theory -- `session.rs` — session types -- `effects.rs` — effect system -- Prove: type checking is sound (well-typed programs do not get stuck) -- Prove: type inference is complete (finds principal types when they exist) -- Prove: unification terminates and is most general - -### Language Bridges (14 crates) -- Each `typell-*` crate bridges TypeLL to a nextgen language -- Prove: bridge translations preserve typing judgments -- Prove: subtyping relationships are transitive across bridges - -### Dimensional Types (crates/typell-core/src/dimensional.rs) -- Physical dimension tracking in types -- Prove: dimensional analysis is consistent (no unit mismatch can pass type checking) - -## Recommended Prover - -- **Idris2** for the type system metatheory (soundness, completeness) -- **Agda** alternative for the unification/inference proofs (strong equational reasoning) - -## Priority - -**HIGH** — TypeLL is PanLL's verification kernel. If the type system is unsound, every downstream language that relies on TypeLL levels has unsound guarantees. The 10-level type hierarchy is the central claim of the project and must be formally verified. diff --git a/docs/status/TEST-NEEDS.adoc b/docs/status/TEST-NEEDS.adoc new file mode 100644 index 0000000..fb0ecc9 --- /dev/null +++ b/docs/status/TEST-NEEDS.adoc @@ -0,0 +1,88 @@ +== TEST-NEEDS: typell + +=== CRG Grade: C — ACHIEVED 2026-04-04 + +=== Current State (verified 2026-04-04) + +[width="100%",cols="40%,26%,34%",options="header",] +|=== +|Category |Count |Details +|*Source modules* |53 |Rust: typell-core (12: types, error, unify, +infer, check, linear, effects, qtt, dimensional, session, proof, lib), +typell-eclexia (3), typell-affinescript (3), typell-ephapax (3), +typell-wokelang (3), typell-tangle (3), typell-betlang (3), +typell-mylang (3), typell-oblibeny (3), typell-jtv (3), typell-phronesis +(3), typell-errorlang (3), typell-vcl (4) + 3 Idris2 ABI + +|*Unit tests (inline)* |106 |In typell-core inline module tests + +|*Integration tests* |95 |core_comprehensive_tests.rs + +|*E2E tests* |15 |e2e_test.rs — full pipeline, all type disciplines + +|*Property tests* |9 |property_test.rs + +|*Benchmarks* |262 lines |typell_bench.rs — Criterion benchmarks for +unification, inference, pipeline +|=== + +*Total verified: 225 tests passing, 0 failing.* + +=== What’s Missing + +==== P2P Tests + +* [ ] No tests for cross-language bridge correctness (e.g., +typell-wokelang checks match wokelang semantics) +* [ ] No tests for bridge interoperability (two language backends +against same type) + +==== E2E Tests + +* [ ] No test for language backend integration with actual language +compilers (requires those compilers installed) + +==== Aspect Tests + +* [ ] *Security*: Type system = trust boundary; no soundness fuzzing +* [ ] *Performance*: No benchmarks despite being performance-critical +type checker +* [ ] *Concurrency*: No parallel type checking tests +* [ ] *Error handling*: No tests for unsatisfiable constraints, infinite +unification, cyclic types + +==== Benchmarks Needed (CRITICAL) + +* [ ] *benches/.gitkeep is EMPTY* – phantom benchmarks +* [ ] Type checking throughput (expressions/second) +* [ ] Unification performance scaling with constraint count +* [ ] QTT resource tracking overhead +* [ ] Session type verification latency +* [ ] Proof checking throughput + +==== Self-Tests + +* [ ] No soundness self-check +* [ ] No regression suite for type system properties + +=== FLAGGED ISSUES + +* *398 inline tests across 13 crates is respectable* – best inline +coverage among non-Julia repos +* *benches/.gitkeep = phantom benchmarks* – a type checker with no +performance measurements +* *13 language backends (eclexia through vcl) each have only ~10 inline +tests* – thin coverage per backend +* *0 E2E for a 10-level type system* – can’t verify the type system +actually works on real programs +* *core_comprehensive_tests.rs (95 tests) is solid* for the kernel + +=== Priority: P1 (HIGH) – inline tests are decent but need E2E, benchmarks, and soundness proofs + +=== FAKE-FUZZ ALERT + +* `+tests/fuzz/placeholder.txt+` is a scorecard placeholder inherited +from rsr-template-repo — it does NOT provide real fuzz testing +* Replace with an actual fuzz harness (see +rsr-template-repo/tests/fuzz/README.adoc) or remove the file +* Priority: P2 — creates false impression of fuzz coverage diff --git a/docs/status/TEST-NEEDS.md b/docs/status/TEST-NEEDS.md deleted file mode 100644 index d9dfbc9..0000000 --- a/docs/status/TEST-NEEDS.md +++ /dev/null @@ -1,58 +0,0 @@ -# TEST-NEEDS: typell - -## CRG Grade: C — ACHIEVED 2026-04-04 - -## Current State (verified 2026-04-04) - -| Category | Count | Details | -|----------|-------|---------| -| **Source modules** | 53 | Rust: typell-core (12: types, error, unify, infer, check, linear, effects, qtt, dimensional, session, proof, lib), typell-eclexia (3), typell-affinescript (3), typell-ephapax (3), typell-wokelang (3), typell-tangle (3), typell-betlang (3), typell-mylang (3), typell-oblibeny (3), typell-jtv (3), typell-phronesis (3), typell-errorlang (3), typell-vcl (4) + 3 Idris2 ABI | -| **Unit tests (inline)** | 106 | In typell-core inline module tests | -| **Integration tests** | 95 | core_comprehensive_tests.rs | -| **E2E tests** | 15 | e2e_test.rs — full pipeline, all type disciplines | -| **Property tests** | 9 | property_test.rs | -| **Benchmarks** | 262 lines | typell_bench.rs — Criterion benchmarks for unification, inference, pipeline | - -**Total verified: 225 tests passing, 0 failing.** - -## What's Missing - -### P2P Tests -- [ ] No tests for cross-language bridge correctness (e.g., typell-wokelang checks match wokelang semantics) -- [ ] No tests for bridge interoperability (two language backends against same type) - -### E2E Tests -- [ ] No test for language backend integration with actual language compilers (requires those compilers installed) - -### Aspect Tests -- [ ] **Security**: Type system = trust boundary; no soundness fuzzing -- [ ] **Performance**: No benchmarks despite being performance-critical type checker -- [ ] **Concurrency**: No parallel type checking tests -- [ ] **Error handling**: No tests for unsatisfiable constraints, infinite unification, cyclic types - -### Benchmarks Needed (CRITICAL) -- [ ] **benches/.gitkeep is EMPTY** -- phantom benchmarks -- [ ] Type checking throughput (expressions/second) -- [ ] Unification performance scaling with constraint count -- [ ] QTT resource tracking overhead -- [ ] Session type verification latency -- [ ] Proof checking throughput - -### Self-Tests -- [ ] No soundness self-check -- [ ] No regression suite for type system properties - -## FLAGGED ISSUES -- **398 inline tests across 13 crates is respectable** -- best inline coverage among non-Julia repos -- **benches/.gitkeep = phantom benchmarks** -- a type checker with no performance measurements -- **13 language backends (eclexia through vcl) each have only ~10 inline tests** -- thin coverage per backend -- **0 E2E for a 10-level type system** -- can't verify the type system actually works on real programs -- **core_comprehensive_tests.rs (95 tests) is solid** for the kernel - -## Priority: P1 (HIGH) -- inline tests are decent but need E2E, benchmarks, and soundness proofs - -## FAKE-FUZZ ALERT - -- `tests/fuzz/placeholder.txt` is a scorecard placeholder inherited from rsr-template-repo — it does NOT provide real fuzz testing -- Replace with an actual fuzz harness (see rsr-template-repo/tests/fuzz/README.adoc) or remove the file -- Priority: P2 — creates false impression of fuzz coverage diff --git a/docs/status/UNIFIED-LEVELS.adoc b/docs/status/UNIFIED-LEVELS.adoc new file mode 100644 index 0000000..f6d7486 --- /dev/null +++ b/docs/status/UNIFIED-LEVELS.adoc @@ -0,0 +1,57 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 = Unified Level System — TypeLL +/ VCL-total / VeriSimDB / TypedQLiser / PanLL :toc: + +== Level Definitions + +[cols="`1,3,3`"] |=== | Level | Name | Criteria + +[verse] +-- +L0 | Scaffold | Repo exists, no functional code +L1 | Spec | Specifications/types defined, no runtime +L2 | Partial | Some code works standalone, not connected +L3 | Core | Main engine works, tests pass, standalone +L4 | Integrated | Connected to adjacent systems, data flows +L5 | End-to-end | Full pipeline works across all systems +L6 | Tested | Point-to-point, end-to-end, aspect tests + benchmarks +L7 | Production | Published, documented, CI green, ready for users +-- + +|=== + +== Current State (2026-03-21) + +[cols="`2,1,3`"] |=== | Component | Level | Notes + +[verse] +-- +TypeLL core engine | L1 | Specs exist, no runtime type checker +TypedQLiser L5-10 | L1 | Levels 1-4 work, 5-10 need TypeLL +PanLL VCL panel | L0 | Does not exist +VCL-total → VeriSimDB bridge | L2 | Parser works, no DB execution +VeriSimDB octad storage | L4 | Phase 4 validated, production tested +PanLL TypeLL panel | L2 | ReScript UI exists, not verified running +TypeLL-VCL bridge | L2 | Crate exists, depends on typell-core +-- + +|=== + +== Level-Up Plan + +Round 1: Bring trailing (L0/L1) → L3:: 1. TypeLL core engine: implement +type checker runtime 2. PanLL VCL panel: create the panel 3. TypedQLiser +L5-10: implement with TypeLL backing + +Round 2: Bring all → L4 (integrated):: 4. Wire VCL-total → VeriSimDB +runtime bridge 5. Wire TypeLL → TypedQLiser for levels 5-10 6. Wire +PanLL TypeLL panel → running TypeLL server 7. Wire PanLL VCL panel → +VCL-total + +Round 3: Bring all → L5 (end-to-end):: 8. PanLL → TypeLL → VCL-total → +VeriSimDB pipeline test 9. TypedQLiser → TypeLL → VCL-total type +checking pipeline + +Round 4: Bring all → L6 (tested + benchmarked):: 10. Point-to-point +tests for every connection 11. End-to-end tests for full pipelines 12. +Aspect tests (error handling, edge cases, concurrency) 13. Benchmarks +(latency, throughput, memory) diff --git a/docs/status/UNIFIED-LEVELS.md b/docs/status/UNIFIED-LEVELS.md deleted file mode 100644 index 4f09710..0000000 --- a/docs/status/UNIFIED-LEVELS.md +++ /dev/null @@ -1,57 +0,0 @@ -// SPDX-License-Identifier: CC-BY-SA-4.0 -= Unified Level System — TypeLL / VCL-total / VeriSimDB / TypedQLiser / PanLL -:toc: - -== Level Definitions - -[cols="1,3,3"] -|=== -| Level | Name | Criteria - -| L0 | Scaffold | Repo exists, no functional code -| L1 | Spec | Specifications/types defined, no runtime -| L2 | Partial | Some code works standalone, not connected -| L3 | Core | Main engine works, tests pass, standalone -| L4 | Integrated | Connected to adjacent systems, data flows -| L5 | End-to-end | Full pipeline works across all systems -| L6 | Tested | Point-to-point, end-to-end, aspect tests + benchmarks -| L7 | Production | Published, documented, CI green, ready for users -|=== - -== Current State (2026-03-21) - -[cols="2,1,3"] -|=== -| Component | Level | Notes - -| TypeLL core engine | L1 | Specs exist, no runtime type checker -| TypedQLiser L5-10 | L1 | Levels 1-4 work, 5-10 need TypeLL -| PanLL VCL panel | L0 | Does not exist -| VCL-total → VeriSimDB bridge | L2 | Parser works, no DB execution -| VeriSimDB octad storage | L4 | Phase 4 validated, production tested -| PanLL TypeLL panel | L2 | ReScript UI exists, not verified running -| TypeLL-VCL bridge | L2 | Crate exists, depends on typell-core -|=== - -== Level-Up Plan - -Round 1: Bring trailing (L0/L1) → L3:: - 1. TypeLL core engine: implement type checker runtime - 2. PanLL VCL panel: create the panel - 3. TypedQLiser L5-10: implement with TypeLL backing - -Round 2: Bring all → L4 (integrated):: - 4. Wire VCL-total → VeriSimDB runtime bridge - 5. Wire TypeLL → TypedQLiser for levels 5-10 - 6. Wire PanLL TypeLL panel → running TypeLL server - 7. Wire PanLL VCL panel → VCL-total - -Round 3: Bring all → L5 (end-to-end):: - 8. PanLL → TypeLL → VCL-total → VeriSimDB pipeline test - 9. TypedQLiser → TypeLL → VCL-total type checking pipeline - -Round 4: Bring all → L6 (tested + benchmarked):: - 10. Point-to-point tests for every connection - 11. End-to-end tests for full pipelines - 12. Aspect tests (error handling, edge cases, concurrency) - 13. Benchmarks (latency, throughput, memory) diff --git a/docs/tech-debt-2026-05-26.adoc b/docs/tech-debt-2026-05-26.adoc new file mode 100644 index 0000000..5cd04c3 --- /dev/null +++ b/docs/tech-debt-2026-05-26.adoc @@ -0,0 +1,84 @@ +== Tech-Debt Audit — typell — 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= 6 | Coq-Axm/Adm= 0 | Lean-srry/ax= 0 | Agda-pst= 0 | Idr-blv= 1 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0 +.... + +*Total markers:* 1. *Severity:* `+>01+`. + +*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 |`+MPL-2.0+` +|Body classifier |`+Palimp-MPL-2.0+` +|Severity |`+ok+` +|=== + +*Recommended next move:* none for licence. + +=== 3. Documentation debt + +[cols=",",options="header",] +|=== +|Field |Value +|README lines |186 +|`+docs/+` files |16 +|`+docs/+` LoC |2478 +|CHANGELOG.md |Y +|CONTRIBUTING.md |Y +|CODE_OF_CONDUCT.md |Y +|SECURITY.md |Y +|Severity |`+LOW+` +|=== + +*Recommended next move:* `+docs/+` has only 16 file(s). Aim for ≥10 +organised docs (architecture, usage, contributing-guide, +troubleshooting, design-decisions). The user’s bar for a +"`heavily-developed and well-organised wiki`" is ≥10 files with topical +organisation. + +=== 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 887509f..0000000 --- a/docs/tech-debt-2026-05-26.md +++ /dev/null @@ -1,71 +0,0 @@ - - -# Tech-Debt Audit — typell — 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= 6 | Coq-Axm/Adm= 0 | Lean-srry/ax= 0 | Agda-pst= 0 | Idr-blv= 1 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0 -``` - -**Total markers:** 1. **Severity:** `>01`. - -**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 | `MPL-2.0` | -| Body classifier | `Palimp-MPL-2.0` | -| Severity | `ok` | - -**Recommended next move:** none for licence. - -## 3. Documentation debt - -| Field | Value | -|---|---| -| README lines | 186 | -| `docs/` files | 16 | -| `docs/` LoC | 2478 | -| CHANGELOG.md | Y | -| CONTRIBUTING.md | Y | -| CODE_OF_CONDUCT.md | Y | -| SECURITY.md | Y | -| Severity | `LOW` | - -**Recommended next move:** `docs/` has only 16 file(s). Aim for ≥10 organised docs (architecture, usage, contributing-guide, troubleshooting, design-decisions). The user's bar for a "heavily-developed and well-organised wiki" is ≥10 files with topical organisation. - -## 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/integrations/README.md b/integrations/README.adoc similarity index 70% rename from integrations/README.md rename to integrations/README.adoc index 5fa4e6e..7a133da 100644 --- a/integrations/README.md +++ b/integrations/README.adoc @@ -1,14 +1,14 @@ -# SPDX-License-Identifier: CC-BY-SA-4.0 +== SPDX-License-Identifier: CC-BY-SA-4.0 -# integrations/ — Consumer Integrations +== integrations/ — Consumer Integrations -Typell's verification kernel is consumed by multiple tools through the -Verification Protocol (JSON-RPC). This directory contains the integration -code for each consumer. +Typell’s verification kernel is consumed by multiple tools through the +Verification Protocol (JSON-RPC). This directory contains the +integration code for each consumer. -## Structure +=== Structure -``` +.... integrations/ ├── panll/ # PanLL integration (PRIMARY consumer) │ Typell as PanLL's Pane-N reasoning engine. @@ -27,9 +27,10 @@ integrations/ └── ci/ # CI/CD plugins (secondary consumer) GitHub Actions, GitLab CI integration. Automated proof checking in pipelines. -``` +.... -## Priority +=== Priority -PanLL is the primary consumer. All other integrations are secondary and must -not influence architectural decisions that would complicate PanLL integration. +PanLL is the primary consumer. All other integrations are secondary and +must not influence architectural decisions that would complicate PanLL +integration. diff --git a/spec/README.md b/spec/README.adoc similarity index 55% rename from spec/README.md rename to spec/README.adoc index bb7b3bf..0b258f8 100644 --- a/spec/README.md +++ b/spec/README.adoc @@ -1,13 +1,13 @@ -# SPDX-License-Identifier: CC-BY-SA-4.0 +== SPDX-License-Identifier: CC-BY-SA-4.0 -# spec/ — Formal Specifications +== spec/ — Formal Specifications -This directory contains the formal specifications for Typell's type systems, -verification protocol, and proof infrastructure. +This directory contains the formal specifications for Typell’s type +systems, verification protocol, and proof infrastructure. -## Structure +=== Structure -``` +.... spec/ ├── protocol/ # Verification Protocol specification │ └── TYPELL-PROTOCOL.adoc # JSON-RPC protocol spec @@ -23,18 +23,19 @@ spec/ ├── verification.adoc # Proof verification ├── certificates.adoc # Proof-carrying code / certificates └── composition.adoc # Multi-proof composition -``` +.... -## Purpose +=== Purpose -These specifications are the source of truth for Typell's behaviour. The Idris2 -ABI definitions in `src/abi/` formalise these specs with machine-checked proofs. -The Rust kernel in `src/kernel/` implements them. +These specifications are the source of truth for Typell’s behaviour. The +Idris2 ABI definitions in `+src/abi/+` formalise these specs with +machine-checked proofs. The Rust kernel in `+src/kernel/+` implements +them. -## Writing Specs +=== Writing Specs -- Use AsciiDoc format (.adoc) -- Include formal typing rules where applicable -- Reference relevant academic literature -- Each spec should be self-contained but cross-reference related specs -- Update specs before changing implementation, not after +* Use AsciiDoc format (.adoc) +* Include formal typing rules where applicable +* Reference relevant academic literature +* Each spec should be self-contained but cross-reference related specs +* Update specs before changing implementation, not after diff --git a/src/abi/README.adoc b/src/abi/README.adoc new file mode 100644 index 0000000..4b56130 --- /dev/null +++ b/src/abi/README.adoc @@ -0,0 +1,83 @@ +== SPDX-License-Identifier: CC-BY-SA-4.0 + +== src/abi/ — Idris2 ABI Definitions (Formal Specifications) + +This directory contains the formal specifications for Typell’s type +systems, written in Idris2 with dependent type proofs. These specs are +the mathematical foundation that proves Typell’s type checker is sound, +complete, and decidable. + +=== Existing Modules + +.... +abi/ +├── Types.idr # ABI type definitions, platform detection, memory proofs +├── Layout.idr # Memory layout proofs, C ABI compliance, struct alignment +├── Foreign.idr # FFI declarations for the Zig layer (libtypell) +├── Soundness.idr # Progress + Preservation proofs for core calculus +├── InferenceSoundness.idr # Unification + type inference soundness proofs +└── LevelMonotonicity.idr # L1-L10 hierarchy monotonicity proofs (initial checked set; open-ended above) +.... + +=== Soundness Proofs + +==== Soundness.idr — Progress and Preservation + +Models the core STLC+let calculus underlying `+check.rs+` and +`+infer.rs+`. - *Progress*: well-typed closed terms are values or can +step (fully proved) - *Preservation*: stepping preserves types (proved +modulo standard renaming lemma) - *Type safety*: well-typed programs +never get stuck (corollary) + +==== InferenceSoundness.idr — Type Inference + +Models unification (`+unify.rs+`) and inference (`+infer.rs+`). - +*Unification soundness*: successful unification produces a valid unifier +- *Occurs check correctness*: variables absent from a type are +unaffected by substitution - *Substitution idempotence*: MGU applied +twice equals MGU applied once - *Arrow decomposition*: unifying function +types decomposes to component unification + +==== LevelMonotonicity.idr — Progressive Level Hierarchy (initial L1-L10) + +Models the L1-L10 type safety hierarchy from `+ROADMAP.adoc+`. TypeLL is +open-ended; L1-L10 is the current checked set, not a fixed ceiling. - +*Level total order*: any two levels are comparable - *Strict increase*: +each level strictly subsumes the previous - *Feature monotonicity*: +higher levels include all lower-level features - *No downgrade*: +programs requiring level N features cannot be checked at level M < N - +*Lattice bounds*: L1 is bottom, L10 is the current top (open-ended +above) + +=== Planned Modules + +.... +abi/ +├── Dependent.idr # Dependent types (Pi, Sigma) with proofs of correctness +├── Linear.idr # Linear types with proofs of resource safety +├── Session.idr # Session types with proofs of protocol compliance +├── QTT.idr # Quantitative Type Theory with usage tracking proofs +├── Effects.idr # Effect system with composition proofs +├── Modal.idr # Modal types with scope restriction proofs +├── Protocol.idr # Verification protocol message type proofs +└── Proof.idr # Proof term representation and verification proofs +.... + +=== Policy + +* *ZERO believe_me* — Every proof must be genuine. No shortcuts. +* *ZERO assert_total* — All functions must be provably total. +* *ZERO assert_smaller* — Termination must be proven structurally. +* *%default total* — All modules use total-by-default. + +These proofs are the ENTIRE POINT of Typell. If the verification kernel +has holes in its own proofs, nothing it verifies is trustworthy. + +=== Relationship to Rust Kernel + +The Idris2 modules specify WHAT the type checker must do. The Rust +kernel in `+src/kernel/+` implements HOW. The Idris2 proofs guarantee +that the Rust implementation is correct (assuming faithful translation). + +Generated C headers in `+generated/abi/+` bridge Idris2 and Zig FFI per +the hyperpolymath ABI/FFI standard. diff --git a/src/abi/README.md b/src/abi/README.md deleted file mode 100644 index 4bd89ae..0000000 --- a/src/abi/README.md +++ /dev/null @@ -1,76 +0,0 @@ -# SPDX-License-Identifier: CC-BY-SA-4.0 - -# src/abi/ — Idris2 ABI Definitions (Formal Specifications) - -This directory contains the formal specifications for Typell's type systems, -written in Idris2 with dependent type proofs. These specs are the mathematical -foundation that proves Typell's type checker is sound, complete, and decidable. - -## Existing Modules - -``` -abi/ -├── Types.idr # ABI type definitions, platform detection, memory proofs -├── Layout.idr # Memory layout proofs, C ABI compliance, struct alignment -├── Foreign.idr # FFI declarations for the Zig layer (libtypell) -├── Soundness.idr # Progress + Preservation proofs for core calculus -├── InferenceSoundness.idr # Unification + type inference soundness proofs -└── LevelMonotonicity.idr # L1-L10 hierarchy monotonicity proofs (initial checked set; open-ended above) -``` - -## Soundness Proofs - -### Soundness.idr — Progress and Preservation -Models the core STLC+let calculus underlying `check.rs` and `infer.rs`. -- **Progress**: well-typed closed terms are values or can step (fully proved) -- **Preservation**: stepping preserves types (proved modulo standard renaming lemma) -- **Type safety**: well-typed programs never get stuck (corollary) - -### InferenceSoundness.idr — Type Inference -Models unification (`unify.rs`) and inference (`infer.rs`). -- **Unification soundness**: successful unification produces a valid unifier -- **Occurs check correctness**: variables absent from a type are unaffected by substitution -- **Substitution idempotence**: MGU applied twice equals MGU applied once -- **Arrow decomposition**: unifying function types decomposes to component unification - -### LevelMonotonicity.idr — Progressive Level Hierarchy (initial L1-L10) -Models the L1-L10 type safety hierarchy from `ROADMAP.adoc`. TypeLL is open-ended; -L1-L10 is the current checked set, not a fixed ceiling. -- **Level total order**: any two levels are comparable -- **Strict increase**: each level strictly subsumes the previous -- **Feature monotonicity**: higher levels include all lower-level features -- **No downgrade**: programs requiring level N features cannot be checked at level M < N -- **Lattice bounds**: L1 is bottom, L10 is the current top (open-ended above) - -## Planned Modules - -``` -abi/ -├── Dependent.idr # Dependent types (Pi, Sigma) with proofs of correctness -├── Linear.idr # Linear types with proofs of resource safety -├── Session.idr # Session types with proofs of protocol compliance -├── QTT.idr # Quantitative Type Theory with usage tracking proofs -├── Effects.idr # Effect system with composition proofs -├── Modal.idr # Modal types with scope restriction proofs -├── Protocol.idr # Verification protocol message type proofs -└── Proof.idr # Proof term representation and verification proofs -``` - -## Policy - -- **ZERO believe_me** — Every proof must be genuine. No shortcuts. -- **ZERO assert_total** — All functions must be provably total. -- **ZERO assert_smaller** — Termination must be proven structurally. -- **%default total** — All modules use total-by-default. - -These proofs are the ENTIRE POINT of Typell. If the verification kernel -has holes in its own proofs, nothing it verifies is trustworthy. - -## Relationship to Rust Kernel - -The Idris2 modules specify WHAT the type checker must do. The Rust kernel -in `src/kernel/` implements HOW. The Idris2 proofs guarantee that the Rust -implementation is correct (assuming faithful translation). - -Generated C headers in `generated/abi/` bridge Idris2 and Zig FFI per -the hyperpolymath ABI/FFI standard. diff --git a/src/backends/README.adoc b/src/backends/README.adoc new file mode 100644 index 0000000..787f432 --- /dev/null +++ b/src/backends/README.adoc @@ -0,0 +1,43 @@ +== SPDX-License-Identifier: CC-BY-SA-4.0 + +== src/backends/ — Language-Specific Backends + +Each backend adapts Typell’s verification kernel for a specific query +language. Backends handle parsing, AST construction, and +language-specific type rules, then delegate to the kernel for core type +checking, proof management, and effect inference. + +=== Structure + +.... +backends/ +├── vcl/ # VCL-dt++ backend (VeriSimDB) +│ 8-modality queries, cross-modal proofs, hexad types. +│ Ported from nextgen-databases/verisim/src/vcl/ (ReScript). +│ +├── gql/ # GQL-dt++ backend (LithoGlyph) +│ Knowledge graph queries, RATIONALE clause, refinement types. +│ Bridged from nextgen-databases/lithoglyph/gql-dt/ (Lean 4). +│ NOT ported — Lean 4's type system is kept intact. +│ +└── kql/ # KQL-dt++ backend (QuandleDB) + Knot invariant queries, category-theoretic schema model, + equality saturation, HoTT identity types. + Designed from scratch — no existing implementation to port. +.... + +=== Backend Responsibilities + +[arabic] +. *Parse* query source into language-specific AST +. *Transform* AST into kernel-compatible representation +. *Provide* language-specific typing rules to the kernel +. *Handle* language-specific proof kinds (e.g. VCL’s EXISTENCE, GQL’s +RATIONALE) +. *Format* kernel results back into language-specific feedback + +=== Adding a New Backend + +A new backend needs: - Parser for the query language - AST → kernel +representation transformer - Language-specific typing rules - Proof kind +registry - Result formatter diff --git a/src/backends/README.md b/src/backends/README.md deleted file mode 100644 index d273838..0000000 --- a/src/backends/README.md +++ /dev/null @@ -1,44 +0,0 @@ -# SPDX-License-Identifier: CC-BY-SA-4.0 - -# src/backends/ — Language-Specific Backends - -Each backend adapts Typell's verification kernel for a specific query language. -Backends handle parsing, AST construction, and language-specific type rules, -then delegate to the kernel for core type checking, proof management, and -effect inference. - -## Structure - -``` -backends/ -├── vcl/ # VCL-dt++ backend (VeriSimDB) -│ 8-modality queries, cross-modal proofs, hexad types. -│ Ported from nextgen-databases/verisim/src/vcl/ (ReScript). -│ -├── gql/ # GQL-dt++ backend (LithoGlyph) -│ Knowledge graph queries, RATIONALE clause, refinement types. -│ Bridged from nextgen-databases/lithoglyph/gql-dt/ (Lean 4). -│ NOT ported — Lean 4's type system is kept intact. -│ -└── kql/ # KQL-dt++ backend (QuandleDB) - Knot invariant queries, category-theoretic schema model, - equality saturation, HoTT identity types. - Designed from scratch — no existing implementation to port. -``` - -## Backend Responsibilities - -1. **Parse** query source into language-specific AST -2. **Transform** AST into kernel-compatible representation -3. **Provide** language-specific typing rules to the kernel -4. **Handle** language-specific proof kinds (e.g. VCL's EXISTENCE, GQL's RATIONALE) -5. **Format** kernel results back into language-specific feedback - -## Adding a New Backend - -A new backend needs: -- Parser for the query language -- AST → kernel representation transformer -- Language-specific typing rules -- Proof kind registry -- Result formatter diff --git a/src/kernel/README.md b/src/kernel/README.adoc similarity index 52% rename from src/kernel/README.md rename to src/kernel/README.adoc index 023b8b0..ab046c5 100644 --- a/src/kernel/README.md +++ b/src/kernel/README.adoc @@ -1,13 +1,14 @@ -# SPDX-License-Identifier: CC-BY-SA-4.0 +== SPDX-License-Identifier: CC-BY-SA-4.0 -# src/kernel/ — Rust Verification Kernel +== src/kernel/ — Rust Verification Kernel -This is Typell's core implementation in Rust. It implements the type checker, -proof engine, effect tracker, session manager, and verification protocol server. +This is Typell’s core implementation in Rust. It implements the type +checker, proof engine, effect tracker, session manager, and verification +protocol server. -## Structure +=== Structure -``` +.... kernel/ ├── checker/ # Bidirectional type checker │ │ Implements: dependent, linear, affine, session, QTT, @@ -30,21 +31,22 @@ kernel/ └── protocol/ # Verification Protocol server (JSON-RPC) The primary interface. PanLL, VS Code, CLI, and CI/CD all communicate with Typell through this server. -``` +.... -## Design Principles +=== Design Principles -- **Correct by construction:** Rust's type system prevents many bugs. Idris2 - specs in `src/abi/` prove the algorithms correct. -- **Protocol-first:** The JSON-RPC protocol server is the primary interface. - Everything else is internal implementation detail. -- **Incremental:** Each type system feature can be enabled/disabled independently. - A consumer that only needs dependent types doesn't pay for session types. -- **No unsafe without SAFETY comment:** Per hyperpolymath policy. -- **No transmute unless FFI boundary:** Per hyperpolymath policy. +* *Correct by construction:* Rust’s type system prevents many bugs. +Idris2 specs in `+src/abi/+` prove the algorithms correct. +* *Protocol-first:* The JSON-RPC protocol server is the primary +interface. Everything else is internal implementation detail. +* *Incremental:* Each type system feature can be enabled/disabled +independently. A consumer that only needs dependent types doesn’t pay +for session types. +* *No unsafe without SAFETY comment:* Per hyperpolymath policy. +* *No transmute unless FFI boundary:* Per hyperpolymath policy. -## Relationship to PanLL +=== Relationship to PanLL -This kernel IS PanLL's Pane-N reasoning engine. When compiled as a Tauri plugin, -it runs in-process with PanLL. When run as a standalone server, PanLL connects -via JSON-RPC. Both modes use the same kernel code. +This kernel IS PanLL’s Pane-N reasoning engine. When compiled as a Tauri +plugin, it runs in-process with PanLL. When run as a standalone server, +PanLL connects via JSON-RPC. Both modes use the same kernel code.