From d879221a145cbae5429417dba50c1d61c43811be Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 24 Aug 2026 08:30:10 +0100 Subject: [PATCH] refactor: migrate repository documentation from Markdown to AsciiDoc --- AGENTS.adoc | 14 + AGENTS.md | 13 - CODE_OF_CONDUCT.adoc | 339 ++++++++++++ CODE_OF_CONDUCT.md | 307 ----------- CONTRIBUTING.md => CONTRIBUTING.adoc | 75 +-- PROOF-NEEDS.adoc | 77 +++ PROOF-NEEDS.md | 46 -- SECURITY.adoc | 437 ++++++++++++++++ SECURITY.md | 374 -------------- TEST-NEEDS.adoc | 144 ++++++ TEST-NEEDS.md | 86 ---- TOPOLOGY.md => TOPOLOGY.adoc | 39 +- llm-warmup-dev.adoc | 19 + llm-warmup-dev.md | 16 - llm-warmup-user.adoc | 19 + llm-warmup-user.md | 16 - nqc/README.adoc | 30 ++ nqc/README.md | 24 - nqc/web/DESIGN-2026-02-22-nqc-web-ui.adoc | 182 +++++++ nqc/web/DESIGN-2026-02-22-nqc-web-ui.md | 160 ------ typeql-experimental/WHITEPAPER.adoc | 487 ++++++++++++++++++ typeql-experimental/WHITEPAPER.md | 461 ----------------- ...emantics.md => operational-semantics.adoc} | 172 ++++--- .../{system-specs.md => system-specs.adoc} | 96 ++-- verisim-modular-experiment/PROOF-NEEDS.adoc | 90 ++++ verisim-modular-experiment/PROOF-NEEDS.md | 92 ---- 26 files changed, 2036 insertions(+), 1779 deletions(-) create mode 100644 AGENTS.adoc delete mode 100644 AGENTS.md create mode 100644 CODE_OF_CONDUCT.adoc delete mode 100644 CODE_OF_CONDUCT.md rename CONTRIBUTING.md => CONTRIBUTING.adoc (64%) create mode 100644 PROOF-NEEDS.adoc delete mode 100644 PROOF-NEEDS.md create mode 100644 SECURITY.adoc delete mode 100644 SECURITY.md create mode 100644 TEST-NEEDS.adoc delete mode 100644 TEST-NEEDS.md rename TOPOLOGY.md => TOPOLOGY.adoc (90%) create mode 100644 llm-warmup-dev.adoc delete mode 100644 llm-warmup-dev.md create mode 100644 llm-warmup-user.adoc delete mode 100644 llm-warmup-user.md create mode 100644 nqc/README.adoc delete mode 100644 nqc/README.md create mode 100644 nqc/web/DESIGN-2026-02-22-nqc-web-ui.adoc delete mode 100644 nqc/web/DESIGN-2026-02-22-nqc-web-ui.md create mode 100644 typeql-experimental/WHITEPAPER.adoc delete mode 100644 typeql-experimental/WHITEPAPER.md rename typeql-experimental/spec/{operational-semantics.md => operational-semantics.adoc} (82%) rename typeql-experimental/spec/{system-specs.md => system-specs.adoc} (52%) create mode 100644 verisim-modular-experiment/PROOF-NEEDS.adoc delete mode 100644 verisim-modular-experiment/PROOF-NEEDS.md diff --git a/AGENTS.adoc b/AGENTS.adoc new file mode 100644 index 00000000..3d227395 --- /dev/null +++ b/AGENTS.adoc @@ -0,0 +1,14 @@ +== AGENTS.md + +This is the *nextgen-databases coordination repo* — it does *not* hold +database implementations. Per-database code, schemas, docs, and query +languages each live in their *own repo* (see `+REGISTRY.adoc+`). + +*Do not add per-database implementation content here.* If you are about +to add database source, schemas, migrations, a query-language +implementation, or per-database docs, it belongs in that database’s own +repo — not here. + +Full guidance: *`+CLAUDE.md+`* (same directory). Universal AI entry +point: *`+0-AI-MANIFEST.a2ml+`*. Authoritative repo map: +*`+REGISTRY.adoc+`*. diff --git a/AGENTS.md b/AGENTS.md deleted file mode 100644 index d5f77ee3..00000000 --- a/AGENTS.md +++ /dev/null @@ -1,13 +0,0 @@ - -# AGENTS.md - -This is the **nextgen-databases coordination repo** — it does **not** hold database -implementations. Per-database code, schemas, docs, and query languages each live in -their **own repo** (see `REGISTRY.adoc`). - -**Do not add per-database implementation content here.** If you are about to add database -source, schemas, migrations, a query-language implementation, or per-database docs, it -belongs in that database's own repo — not here. - -Full guidance: **`CLAUDE.md`** (same directory). Universal AI entry point: -**`0-AI-MANIFEST.a2ml`**. Authoritative repo map: **`REGISTRY.adoc`**. diff --git a/CODE_OF_CONDUCT.adoc b/CODE_OF_CONDUCT.adoc new file mode 100644 index 00000000..10490da3 --- /dev/null +++ b/CODE_OF_CONDUCT.adoc @@ -0,0 +1,339 @@ +== Code of Conduct + +=== Our Pledge + +We as members, contributors, and leaders pledge to make participation in +Nextgen Databases 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 *5 working days* +. The conduct team 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 conduct team 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 conduct team 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 conduct team 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/nextgen-databases/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 cd205343..00000000 --- a/CODE_OF_CONDUCT.md +++ /dev/null @@ -1,307 +0,0 @@ -# Code of Conduct - -## Our Pledge - -We as members, contributors, and leaders pledge to make participation in Nextgen Databases 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 **5 working days** -2. The conduct team 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 conduct team 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 conduct team 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 conduct team 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/nextgen-databases/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.md b/CONTRIBUTING.adoc similarity index 64% rename from CONTRIBUTING.md rename to CONTRIBUTING.adoc index 7ee55411..b2eb6c74 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.adoc @@ -1,37 +1,41 @@ -# Clone the repository -git clone https://github.com/hyperpolymath/nextgen-databases.git -cd nextgen-databases +== Clone the repository + +git clone https://github.com/hyperpolymath/nextgen-databases.git cd +nextgen-databases + +== Using Nix (recommended for reproducibility) -# Using Nix (recommended for reproducibility) nix develop -# Or using toolbox/distrobox -toolbox create nextgen-databases-dev -toolbox enter nextgen-databases-dev +== Or using toolbox/distrobox + +toolbox create nextgen-databases-dev toolbox enter nextgen-databases-dev # Install dependencies manually -# Verify setup -just check # or: cargo check / mix compile / etc. -just test # Run test suite -``` +== Verify setup + +just check # or: cargo check / mix compile / etc. just test # Run test +suite + +.... ### Repository Structure `nextgen-databases` is a **coordination repo** — it does not hold database implementations. Each database and query language has its own repo (see `REGISTRY.adoc`). +.... -``` -nextgen-databases/ -├── README.adoc / EXPLAINME.adoc / TOPOLOGY.md / ROADMAP.adoc # Portfolio docs -├── REGISTRY.adoc # Authoritative map: database/language -> its own repo -├── CLAUDE.md / AGENTS.md / 0-AI-MANIFEST.a2ml # Agent guardrails -├── docs/ # Coordination docs (incl. migration runbooks) -├── tests/ # CROSS-database integration tests only -├── .machine_readable/ # Canonical SCM metadata -├── .github/ # CI/CD, issue templates, governance -├── .well-known/ LICENSES/ -└── flake.nix / Justfile / stapeln.toml / opsm.toml # Shared env & orchestration -``` +nextgen-databases/ ├── README.adoc / EXPLAINME.adoc / TOPOLOGY.md / +ROADMAP.adoc # Portfolio docs ├── REGISTRY.adoc # Authoritative map: +database/language -> its own repo ├── CLAUDE.md / AGENTS.md / +0-AI-MANIFEST.a2ml # Agent guardrails ├── docs/ # Coordination docs +(incl. migration runbooks) ├── tests/ # CROSS-database integration tests +only ├── .machine_readable/ # Canonical SCM metadata ├── .github/ # +CI/CD, issue templates, governance ├── .well-known/ LICENSES/ └── +flake.nix / Justfile / stapeln.toml / opsm.toml # Shared env & +orchestration + +.... #### What belongs here vs. in a database repo @@ -95,21 +99,22 @@ Look for issues labelled: ## 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) -``` +.... + +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] +{empty}[optional body] -[optional footer] +{empty}[optional footer] diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc new file mode 100644 index 00000000..f6bbe1a8 --- /dev/null +++ b/PROOF-NEEDS.adoc @@ -0,0 +1,77 @@ +== PROOF-NEEDS.md — nextgen-databases + +=== Current State (Updated 2026-04-11 — V3/V4 L4 DONE) + +* *VeriSimDB ABI*: `+verisimdb/src/abi/+` — `+Types.idr+`, +`+Layout.idr+`, `+Foreign.idr+` (873 LOC, genuine domain ABI) +* *Lithoglyph ABI*: `+lithoglyph/+` — `+BofigEntities.idr+`, +`+GQLdt/ABI/Foreign.idr+` +* *Dangerous patterns*: 0 (4 references are documentation asserting "`no +believe_me`" invariant) +* *LOC*: ~202,000 (Rust + Idris2) +* *Connector Obj.magic casts*: ELIMINATED 2026-04-10 — 5 ReScript +connectors now use typed externals + +=== What Needs Proving + +==== P0 — Critical (require Lean4/TLA+/Coq — not I2) + +[width="100%",cols="12%,37%,27%,24%",options="header",] +|=== +|# |Component |Prover |Notes +|V1 |Octad coherence invariant |I2 |8 modalities mutually consistent +post-operation + +|V2 |VCL type inference soundness |Cq/L4 |Bidirectional inference +correct + +|*V3* |*VCL subtyping transitivity + decidability* |*L4* |*DONE +2026-04-11* — `+verisimdb/verification/proofs/lean4/VCLSubtyping.lean+` + +|*V4* |*Raft consensus safety* |*L4* |*DONE 2026-04-11* — +`+verisimdb/verification/proofs/lean4/RaftSafety.lean+` (single-node; +distributed in TLA+) + +|V5 |Transaction atomicity |TLA |All-or-nothing across 8 modalities +|=== + +==== P1 — High + +[width="100%",cols="12%,37%,27%,24%",options="header",] +|=== +|# |Component |Prover |Notes +|*V6* |*WAL integrity* |*L4* |*DONE 2026-04-12* — +`+verisimdb/verification/proofs/lean4/WALIntegrity.lean+` — sequence +monotonicity, CRC validity, replay compositionality + checkpoint +idempotence + +|*V7* |*Provenance chain immutability* |*Ag* |*DONE 2026-04-11* — +`+verisimdb/verification/proofs/agda/ProvenanceChain.agda+` + +|V8 |Drift metric correctness |Iz |Detection algorithm numerical bounds +|=== + +==== P2 — Standard (I2 actionable) + +[width="100%",cols="12%,37%,27%,24%",options="header",] +|=== +|# |Component |Prover |Notes +|V11 |Connector type safety |I2 |Obj.magic eliminated; Idris2 proof of +typed external shapes + +|V12 |FFI pointer validity + memory ownership |I2 +|`+verisimdb/src/abi/Foreign.idr+` lifetime model +|=== + +Note: V9/V10 require TLA+ (not I2). + +=== Recommended Prover + +*Idris2* for V11/V12 (P2, I2-actionable). V0-V8 require +Lean4/Agda/Isabelle/TLA+ specialists. + +=== Priority + +*MEDIUM* (was HIGH) — V1-V8 require non-Idris2 provers. V11/V12 (I2/P2) +are the remaining I2-actionable items; Obj.magic already eliminated from +connectors. WAL/transaction/consensus remain open for L4/TLA+ sessions. diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md deleted file mode 100644 index 0dff44f0..00000000 --- a/PROOF-NEEDS.md +++ /dev/null @@ -1,46 +0,0 @@ -# PROOF-NEEDS.md — nextgen-databases - -## Current State (Updated 2026-04-11 — V3/V4 L4 DONE) - -- **VeriSimDB ABI**: `verisimdb/src/abi/` — `Types.idr`, `Layout.idr`, `Foreign.idr` (873 LOC, genuine domain ABI) -- **Lithoglyph ABI**: `lithoglyph/` — `BofigEntities.idr`, `GQLdt/ABI/Foreign.idr` -- **Dangerous patterns**: 0 (4 references are documentation asserting "no believe_me" invariant) -- **LOC**: ~202,000 (Rust + Idris2) -- **Connector Obj.magic casts**: ELIMINATED 2026-04-10 — 5 ReScript connectors now use typed externals - -## What Needs Proving - -### P0 — Critical (require Lean4/TLA+/Coq — not I2) - -| # | Component | Prover | Notes | -|---|-----------|--------|-------| -| V1 | Octad coherence invariant | I2 | 8 modalities mutually consistent post-operation | -| V2 | VCL type inference soundness | Cq/L4 | Bidirectional inference correct | -| **V3** | **VCL subtyping transitivity + decidability** | **L4** | **DONE 2026-04-11** — `verisimdb/verification/proofs/lean4/VCLSubtyping.lean` | -| **V4** | **Raft consensus safety** | **L4** | **DONE 2026-04-11** — `verisimdb/verification/proofs/lean4/RaftSafety.lean` (single-node; distributed in TLA+) | -| V5 | Transaction atomicity | TLA | All-or-nothing across 8 modalities | - -### P1 — High - -| # | Component | Prover | Notes | -|---|-----------|--------|-------| -| **V6** | **WAL integrity** | **L4** | **DONE 2026-04-12** — `verisimdb/verification/proofs/lean4/WALIntegrity.lean` — sequence monotonicity, CRC validity, replay compositionality + checkpoint idempotence | -| **V7** | **Provenance chain immutability** | **Ag** | **DONE 2026-04-11** — `verisimdb/verification/proofs/agda/ProvenanceChain.agda` | -| V8 | Drift metric correctness | Iz | Detection algorithm numerical bounds | - -### P2 — Standard (I2 actionable) - -| # | Component | Prover | Notes | -|---|-----------|--------|-------| -| V11 | Connector type safety | I2 | Obj.magic eliminated; Idris2 proof of typed external shapes | -| V12 | FFI pointer validity + memory ownership | I2 | `verisimdb/src/abi/Foreign.idr` lifetime model | - -Note: V9/V10 require TLA+ (not I2). - -## Recommended Prover - -**Idris2** for V11/V12 (P2, I2-actionable). V0-V8 require Lean4/Agda/Isabelle/TLA+ specialists. - -## Priority - -**MEDIUM** (was HIGH) — V1-V8 require non-Idris2 provers. V11/V12 (I2/P2) are the remaining I2-actionable items; Obj.magic already eliminated from connectors. WAL/transaction/consensus remain open for L4/TLA+ sessions. diff --git a/SECURITY.adoc b/SECURITY.adoc new file mode 100644 index 00000000..68c30afd --- /dev/null +++ b/SECURITY.adoc @@ -0,0 +1,437 @@ +== 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/nextgen-databases/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: Email + +If you cannot use GitHub Security Advisories, you may email us directly: + +[cols=",",] +|=== +|*Email* |j.d.a.jewell@open.ac.uk +|=== + +____ +*⚠️ 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/nextgen-databases+`) 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/nextgen-databases/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 Nextgen Databases, 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 + +* https://github.com/hyperpolymath/nextgen-databases/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/nextgen-databases/security/advisories/new[Report +via GitHub] or j.d.a.jewell@open.ac.uk + +|*General questions* +|https://github.com/hyperpolymath/nextgen-databases/discussions[GitHub +Discussions] + +|*Other enquiries* |See link:README.adoc[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 Nextgen Databases 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 25b4fdfe..00000000 --- a/SECURITY.md +++ /dev/null @@ -1,374 +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/nextgen-databases/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: Email - -If you cannot use GitHub Security Advisories, you may email us directly: - -| | | -|---|---| -| **Email** | j.d.a.jewell@open.ac.uk | - -> **⚠️ 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/nextgen-databases`) 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/nextgen-databases/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 Nextgen Databases, 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 - -- [Security Advisories](https://github.com/hyperpolymath/nextgen-databases/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/nextgen-databases/security/advisories/new) or j.d.a.jewell@open.ac.uk | -| **General questions** | [GitHub Discussions](https://github.com/hyperpolymath/nextgen-databases/discussions) | -| **Other enquiries** | See [README](README.adoc) 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 Nextgen Databases and its users safe.* 🛡️ - ---- - -Last updated: 2026 · Policy version: 1.0.0 diff --git a/TEST-NEEDS.adoc b/TEST-NEEDS.adoc new file mode 100644 index 00000000..0e54d349 --- /dev/null +++ b/TEST-NEEDS.adoc @@ -0,0 +1,144 @@ +== TEST-NEEDS.md — nextgen-databases + +=== CRG Grade: C — ACHIEVED 2026-04-04 + +____ +Generated 2026-03-29 by punishing audit. Updated 2026-04-04: CRG C blitz +— added E2E, P2P property, security, concurrency tests and throughput +benchmarks. +____ + +=== Current State + +[width="100%",cols="47%,28%,25%",options="header",] +|=== +|Category |Count |Notes +|Unit tests |~40 |VeriSimDB Elixir: consensus (kraft_node, kraft_wal, +kraft_recovery, kraft_transport), federation adapters (mongodb, redis, +duckdb, clickhouse, surrealdb, sqlite, neo4j, vector_db, influxdb, +object_storage), resolver, adapter + base tests + +|Integration |~12 |Federation adapter integration tests (mongodb, redis, +neo4j, clickhouse, surrealdb, influxdb) + +|E2E |18 +|`+verisimdb/elixir-orchestration/test/verisim/e2e_verisimdb_test.exs+` +— lifecycle, VCL, schema, error handling + +|P2P (property) |5 props + 1 test +|`+verisimdb/elixir-orchestration/test/verisim/consensus/kraft_property_test.exs+` +— leader uniqueness, log replication, state machine, partition +tolerance, read-your-writes + +|Aspect: Security |10 tests +|`+verisimdb/elixir-orchestration/test/verisim/aspect/security_test.exs+` +— VCL injection, unauthorised access, cross-tenant isolation, error +disclosure + +|Aspect: Concurrency |14 tests +|`+verisimdb/elixir-orchestration/test/verisim/aspect/concurrency_test.exs+` +— concurrent entity writes, parallel VCL, concurrent Kraft proposals, +DriftMonitor load, SchemaRegistry concurrency + +|lithoglyph smoke |Gleam +|`+lithoglyph/beam/test/lith_beam_smoke_test.gleam+` — version, connect, +lifecycle, error handling + +|Benchmarks |2 real files |`+verisimdb/benches/modality_benchmarks.rs+` +(Rust, pre-existing), `+verisimdb/benches/throughput_benchmarks.rs+` +(Rust, new — write throughput, read latency, VCL complexity) +|=== + +*Source modules:* ~833 across 2 major subsystems. verisimdb: ~248 files +(Rust core, Elixir orchestration, Gleam, Idris2 ABI, Zig FFI, ReScript). +lithoglyph: ~212 files (Gleam, Rust, Factor). + +=== What’s Done (2026-04-04) + +==== Completed + +* [x] VeriSimDB E2E tests (18 tests): write→read lifecycle, VCL +pipeline, schema validation, error handling +* [x] Kraft consensus P2P property tests (5 properties + 1 unit): leader +uniqueness, log replication, state machine safety, partition tolerance, +read-your-writes +* [x] VCL security aspect tests (10 tests): injection hardening, auth +rejection, cross-tenant isolation, error disclosure +* [x] Concurrency aspect tests (14 tests): concurrent EntityServer +writes, parallel VCL, concurrent Kraft proposals, DriftMonitor load, +SchemaRegistry concurrent registration +* [x] lithoglyph Gleam smoke test: lifecycle smoke (graceful-failure +when NIF not compiled) +* [x] Rust throughput benchmarks: write throughput (1/10/100 batch), +read latency (hot/cold), VCL complexity tiers, write-read round-trip +latency + +==== Known Gaps Surfaced by Tests + +* VCLTypeChecker calls `+:erlang.binary_to_existing_atom/1+` for unknown +proof types → ArgumentError (hardening gap, P1) +* VCL built-in parser does NOT strip null bytes from entity IDs +(C-string truncation risk at FFI layer, P1) +* SchemaRegistry.register_type/1 returns `+{:error, :already_exists}+` +for duplicate IRIs rather than idempotent `+:ok+` (P2) +* `+kraft_node_test.exs+` `+remove_server+` test has a GenServer timeout +(pre-existing, P2) + +=== What’s Still Missing + +==== P2P (Property-Based) Tests + +* [ ] CRDT convergence: property tests for VeriSimDB’s CRDT operations +* [ ] VCL query parsing: arbitrary query fuzzing (replace fuzz +placeholder) +* [ ] Federation: property tests for data consistency across adapters +* [ ] lithoglyph: data structure invariant tests + +==== E2E Tests + +* [ ] Federation: write through adapter → verify in external DB → read +back +* [ ] Kraft consensus: cluster formation → leader election → write → +node failure → recovery +* [ ] VCL: complex query execution with joins/aggregations + +==== Build & Execution + +* [ ] `+mix test+` for VeriSimDB Elixir (currently 6 pre-existing +failures, not from new tests) +* [ ] `+cargo test+` for VeriSimDB Rust (integration test uses old API) +* [ ] `+gleam test+` for lithoglyph Gleam (requires compiled NIF) +* [ ] Zig FFI tests + +==== Benchmarks Still Needed + +* [ ] Kraft consensus round-trip time +* [ ] Federation adapter roundtrip per backend +* [ ] lithoglyph query performance +* [ ] Replication lag measurement (multi-node) + +==== Self-Tests + +* [ ] Cluster health self-check +* [ ] Federation adapter connectivity verification +* [ ] Data integrity checksums +* [ ] WAL consistency validation + +=== Priority + +*Partially addressed.* All CRG C test categories are now represented: - +Unit + smoke: pre-existing + new E2E lifecycle tests - Build +verification: `+mix test+` runs (6 pre-existing failures, not from new +tests) - P2P: KRaft property tests - E2E: full lifecycle + VCL + schema ++ error paths - Reflexive: type hierarchy, schema self-validation - +Contract: VCL proof certificate tests (pre-existing) - Aspect: security +injection + concurrency tests - Benchmarks: Rust throughput/latency/VCL +complexity baselines + +=== 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/TEST-NEEDS.md b/TEST-NEEDS.md deleted file mode 100644 index 78586ff6..00000000 --- a/TEST-NEEDS.md +++ /dev/null @@ -1,86 +0,0 @@ -# TEST-NEEDS.md — nextgen-databases - -## CRG Grade: C — ACHIEVED 2026-04-04 - -> Generated 2026-03-29 by punishing audit. -> Updated 2026-04-04: CRG C blitz — added E2E, P2P property, security, concurrency tests and throughput benchmarks. - -## Current State - -| Category | Count | Notes | -|-------------|--------|-------| -| Unit tests | ~40 | VeriSimDB Elixir: consensus (kraft_node, kraft_wal, kraft_recovery, kraft_transport), federation adapters (mongodb, redis, duckdb, clickhouse, surrealdb, sqlite, neo4j, vector_db, influxdb, object_storage), resolver, adapter + base tests | -| Integration | ~12 | Federation adapter integration tests (mongodb, redis, neo4j, clickhouse, surrealdb, influxdb) | -| E2E | 18 | `verisimdb/elixir-orchestration/test/verisim/e2e_verisimdb_test.exs` — lifecycle, VCL, schema, error handling | -| P2P (property) | 5 props + 1 test | `verisimdb/elixir-orchestration/test/verisim/consensus/kraft_property_test.exs` — leader uniqueness, log replication, state machine, partition tolerance, read-your-writes | -| Aspect: Security | 10 tests | `verisimdb/elixir-orchestration/test/verisim/aspect/security_test.exs` — VCL injection, unauthorised access, cross-tenant isolation, error disclosure | -| Aspect: Concurrency | 14 tests | `verisimdb/elixir-orchestration/test/verisim/aspect/concurrency_test.exs` — concurrent entity writes, parallel VCL, concurrent Kraft proposals, DriftMonitor load, SchemaRegistry concurrency | -| lithoglyph smoke | Gleam | `lithoglyph/beam/test/lith_beam_smoke_test.gleam` — version, connect, lifecycle, error handling | -| Benchmarks | 2 real files | `verisimdb/benches/modality_benchmarks.rs` (Rust, pre-existing), `verisimdb/benches/throughput_benchmarks.rs` (Rust, new — write throughput, read latency, VCL complexity) | - -**Source modules:** ~833 across 2 major subsystems. verisimdb: ~248 files (Rust core, Elixir orchestration, Gleam, Idris2 ABI, Zig FFI, ReScript). lithoglyph: ~212 files (Gleam, Rust, Factor). - -## What's Done (2026-04-04) - -### Completed -- [x] VeriSimDB E2E tests (18 tests): write→read lifecycle, VCL pipeline, schema validation, error handling -- [x] Kraft consensus P2P property tests (5 properties + 1 unit): leader uniqueness, log replication, state machine safety, partition tolerance, read-your-writes -- [x] VCL security aspect tests (10 tests): injection hardening, auth rejection, cross-tenant isolation, error disclosure -- [x] Concurrency aspect tests (14 tests): concurrent EntityServer writes, parallel VCL, concurrent Kraft proposals, DriftMonitor load, SchemaRegistry concurrent registration -- [x] lithoglyph Gleam smoke test: lifecycle smoke (graceful-failure when NIF not compiled) -- [x] Rust throughput benchmarks: write throughput (1/10/100 batch), read latency (hot/cold), VCL complexity tiers, write-read round-trip latency - -### Known Gaps Surfaced by Tests -- VCLTypeChecker calls `:erlang.binary_to_existing_atom/1` for unknown proof types → ArgumentError (hardening gap, P1) -- VCL built-in parser does NOT strip null bytes from entity IDs (C-string truncation risk at FFI layer, P1) -- SchemaRegistry.register_type/1 returns `{:error, :already_exists}` for duplicate IRIs rather than idempotent `:ok` (P2) -- `kraft_node_test.exs` `remove_server` test has a GenServer timeout (pre-existing, P2) - -## What's Still Missing - -### P2P (Property-Based) Tests -- [ ] CRDT convergence: property tests for VeriSimDB's CRDT operations -- [ ] VCL query parsing: arbitrary query fuzzing (replace fuzz placeholder) -- [ ] Federation: property tests for data consistency across adapters -- [ ] lithoglyph: data structure invariant tests - -### E2E Tests -- [ ] Federation: write through adapter → verify in external DB → read back -- [ ] Kraft consensus: cluster formation → leader election → write → node failure → recovery -- [ ] VCL: complex query execution with joins/aggregations - -### Build & Execution -- [ ] `mix test` for VeriSimDB Elixir (currently 6 pre-existing failures, not from new tests) -- [ ] `cargo test` for VeriSimDB Rust (integration test uses old API) -- [ ] `gleam test` for lithoglyph Gleam (requires compiled NIF) -- [ ] Zig FFI tests - -### Benchmarks Still Needed -- [ ] Kraft consensus round-trip time -- [ ] Federation adapter roundtrip per backend -- [ ] lithoglyph query performance -- [ ] Replication lag measurement (multi-node) - -### Self-Tests -- [ ] Cluster health self-check -- [ ] Federation adapter connectivity verification -- [ ] Data integrity checksums -- [ ] WAL consistency validation - -## Priority - -**Partially addressed.** All CRG C test categories are now represented: -- Unit + smoke: pre-existing + new E2E lifecycle tests -- Build verification: `mix test` runs (6 pre-existing failures, not from new tests) -- P2P: KRaft property tests -- E2E: full lifecycle + VCL + schema + error paths -- Reflexive: type hierarchy, schema self-validation -- Contract: VCL proof certificate tests (pre-existing) -- Aspect: security injection + concurrency tests -- Benchmarks: Rust throughput/latency/VCL complexity baselines - -## 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/TOPOLOGY.md b/TOPOLOGY.adoc similarity index 90% rename from TOPOLOGY.md rename to TOPOLOGY.adoc index 1765ce34..1cd36533 100644 --- a/TOPOLOGY.md +++ b/TOPOLOGY.adoc @@ -1,12 +1,8 @@ - - - +== Next-Gen Databases — Project Topology -# Next-Gen Databases — Project Topology +=== System Architecture -## System Architecture - -``` +.... ┌─────────────────────────────────────────┐ │ DB ANALYST / USER │ │ (KQL, VCL, Web Dashboards) │ @@ -52,11 +48,11 @@ │ No Local Code 0-AI-MANIFEST.a2ml│ │ Groove Discovery nqc/.well-known/ │ └─────────────────────────────────────────┘ -``` +.... -## Completion Dashboard +=== Completion Dashboard -``` +.... COMPONENT STATUS NOTES ───────────────────────────────── ────────────────── ───────────────────────────────── DATABASE PORTFOLIO @@ -77,25 +73,26 @@ REPO INFRASTRUCTURE ───────────────────────────────────────────────────────────────────────────── OVERALL: ██████████ 100% Portfolio Architected & Indexed -``` +.... -## Key Dependencies +=== Key Dependencies -``` +.... Database Engine ──────► Query DSL ────────► HTTP API ─────────► Web UI │ │ │ │ ▼ ▼ ▼ ▼ Julia / Rust ──────► ReScript Parser ────► JSON Endpoints ──► React SPA -``` +.... -## 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/llm-warmup-dev.adoc b/llm-warmup-dev.adoc new file mode 100644 index 00000000..e0991a4b --- /dev/null +++ b/llm-warmup-dev.adoc @@ -0,0 +1,19 @@ +== LLM Warmup — nextgen-databases (Developer) + +=== What is nextgen-databases? + +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: PMPL-1.0-or-later +* Part of hyperpolymath ecosystem +* See EXPLAINME.adoc for architecture diff --git a/llm-warmup-dev.md b/llm-warmup-dev.md deleted file mode 100644 index c0403e08..00000000 --- a/llm-warmup-dev.md +++ /dev/null @@ -1,16 +0,0 @@ -# LLM Warmup — nextgen-databases (Developer) - -## What is nextgen-databases? -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: PMPL-1.0-or-later -- Part of hyperpolymath ecosystem -- See EXPLAINME.adoc for architecture diff --git a/llm-warmup-user.adoc b/llm-warmup-user.adoc new file mode 100644 index 00000000..fd77b223 --- /dev/null +++ b/llm-warmup-user.adoc @@ -0,0 +1,19 @@ +== LLM Warmup — nextgen-databases (User) + +=== What is nextgen-databases? + +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: PMPL-1.0-or-later +* Part of hyperpolymath ecosystem +* See EXPLAINME.adoc for architecture diff --git a/llm-warmup-user.md b/llm-warmup-user.md deleted file mode 100644 index 63bac91f..00000000 --- a/llm-warmup-user.md +++ /dev/null @@ -1,16 +0,0 @@ -# LLM Warmup — nextgen-databases (User) - -## What is nextgen-databases? -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: PMPL-1.0-or-later -- Part of hyperpolymath ecosystem -- See EXPLAINME.adoc for architecture diff --git a/nqc/README.adoc b/nqc/README.adoc new file mode 100644 index 00000000..84f24e22 --- /dev/null +++ b/nqc/README.adoc @@ -0,0 +1,30 @@ +== nqc + +https://hex.pm/packages/nqc[image:https://img.shields.io/hexpm/v/nqc[Package +Version]] +https://hexdocs.pm/nqc/[image:https://img.shields.io/badge/hex-docs-ffaff3[Hex +Docs]] + +[source,sh] +---- +gleam add nqc@1 +---- + +[source,gleam] +---- +import nqc + +pub fn main() -> Nil { + // TODO: An example of the project in use +} +---- + +Further documentation can be found at https://hexdocs.pm/nqc. + +=== Development + +[source,sh] +---- +gleam run # Run the project +gleam test # Run the tests +---- diff --git a/nqc/README.md b/nqc/README.md deleted file mode 100644 index 7c0cbc01..00000000 --- a/nqc/README.md +++ /dev/null @@ -1,24 +0,0 @@ -# nqc - -[![Package Version](https://img.shields.io/hexpm/v/nqc)](https://hex.pm/packages/nqc) -[![Hex Docs](https://img.shields.io/badge/hex-docs-ffaff3)](https://hexdocs.pm/nqc/) - -```sh -gleam add nqc@1 -``` -```gleam -import nqc - -pub fn main() -> Nil { - // TODO: An example of the project in use -} -``` - -Further documentation can be found at . - -## Development - -```sh -gleam run # Run the project -gleam test # Run the tests -``` diff --git a/nqc/web/DESIGN-2026-02-22-nqc-web-ui.adoc b/nqc/web/DESIGN-2026-02-22-nqc-web-ui.adoc new file mode 100644 index 00000000..cc7e6e80 --- /dev/null +++ b/nqc/web/DESIGN-2026-02-22-nqc-web-ui.adoc @@ -0,0 +1,182 @@ +== NQC Web UI — Design Document + +*Date:* 2026-02-22 *Repo:* `+nextgen-databases/nqc/+` *Author:* Claude +(with Jonathan D.A. Jewell) *Status:* COMPLETE — 48 modules, 0 errors, 0 +warnings. All features implemented. + +''''' + +=== Overview + +A companion web UI for the NQC (NextGen Query Client) Gleam REPL. Built +with *rescript-tea* (TEA architecture) and *cadre-router* (URL routing). +The Gleam REPL at `+src/+` is UNCHANGED — this is a standalone addition +in `+web/+`. + +=== Architecture + +.... +web/ +├── rescript.json # ReScript 12 config, references local tea + cadre-router +├── deno.json # Deno deps + tasks (npm specifiers for react, rescript) +├── setup.sh # Creates symlinks for local ReScript packages +├── index.html # HTML shell + all CSS (dark terminal theme) +├── serve.js # DONE — Deno static file server (SPA fallback) +├── src/ +│ ├── Database.res # DONE — Profile type + VCL/GQL/KQL builtins (mirrors Gleam) +│ ├── Route.res # DONE — Route type + URL parser (cadre-router) +│ ├── Msg.res # DONE — Message variants + outputFormat/connectionState types +│ ├── Model.res # DONE — Application state + init function +│ ├── Api.res # DONE — HTTP commands (query, health) via CORS proxy +│ ├── Update.res # DONE — Pure update function (all state transitions) +│ ├── Subs.res # DONE — Subscriptions (currently none, placeholder) +│ ├── View.res # DONE Top-level view dispatch by route +│ ├── App.res # DONE TEA app wiring (MakeWithDispatch functor) +│ ├── Index.res # DONE ReactDOM.render entry point +│ ├── Pages/ +│ │ ├── Picker.res # DONE Database picker — card grid with health dots +│ │ └── Query.res # DONE Query interface — editor + results + format switch +│ └── Components/ +│ ├── Header.res # DONE — Nav bar with db badge, DT toggle, format tabs +│ ├── Editor.res # DONE — Query textarea with Ctrl+Enter and history +│ ├── Results.res # DONE — Table/JSON/CSV result renderer +│ └── Status.res # DONE — Connection health dot indicator +├── proxy/ +│ └── server.js # DONE Deno CORS proxy (forwards to db ports) +.... + +=== Key Decisions + +==== 1. MakeWithDispatch, not MakeSimple + +`+rescript-tea+`’s `+Tea_Html+` module has NO element constructors (no +`+div+`, `+span+`, etc.). It expects JSX usage. Since JSX needs a +`+dispatch+` function for event handlers, we use +`+Tea_App.MakeWithDispatch+` which passes `+(model, dispatch)+` to the +view. + +==== 2. URL routing via init command + +`+cadre-router+`’s `+Tea_Router.listen+` is set up once in the app’s +init command via `+Tea_Cmd.effect+`. It fires `+UrlChanged+` messages on +browser back/forward. Programmatic navigation uses +`+Tea_Navigation.execute(Push(...))+` directly. + +==== 3. CORS proxy pattern + +Browser → localhost:4000 (Deno proxy) → localhost:808x (database +engines). The proxy maps `+/api/:dbId/*+` to the correct port based on +database profiles. + +==== 4. Raw JSON responses + +Database engines return heterogeneous JSON. We decode as `+JSON.t+` +(raw) and render client-side based on the format selector +(Table/JSON/CSV). The `+Results.res+` component auto-detects columns +from the first row. + +=== Dependency Chain + +.... +nqc-web + ├── rescript-tea (local: ../../developer-ecosystem/rescript-ecosystem/packages/web/tea) + │ ├── @rescript/react (npm) + │ ├── @rescript/core (npm) + │ └── @proven/rescript-bindings (STUB — created by setup.sh) + ├── @anthropics/cadre-router (local: ../../developer-ecosystem/rescript-ecosystem/cadre-router) + │ ├── @rescript/react (npm) + │ ├── @rescript/core (npm) + │ └── rescript-wasm-runtime (STUB — created by setup.sh) + ├── @rescript/core (npm via deno.json) + └── @rescript/react (npm via deno.json) +.... + +`+setup.sh+` creates symlinks for local packages and stub rescript.json +for transitive deps. + +=== API Contracts + +==== Query execution + +.... +POST /api/{dbId}{executePath} +Body: {"query": "SELECT ...", "dt": false} +Response: JSON (shape varies by engine) +.... + +==== Health check + +.... +GET /api/{dbId}{healthPath} +Response: any 2xx = healthy +.... + +==== Database ports + +[cols=",,,",options="header",] +|=== +|DB |Port |Execute Path |Health Path +|VCL (VeriSimDB) |8080 |/vcl/execute |/health +|GQL (Lithoglyph) |8081 |/gql/execute |/health +|KQL (QuandleDB) |8082 |/kql/execute |/health +|=== + +=== How to Resume + +If this session was interrupted, here’s what remains: + +==== Files still TODO (as of writing): + +[arabic] +. `+web/src/View.res+` — Route-based view dispatch (calls Picker or +Query page) +. `+web/src/App.res+` — TEA MakeWithDispatch functor wiring + init +command +. `+web/src/Index.res+` — ReactDOM entry (render App into #root) +. `+web/src/Pages/Picker.res+` — Database card grid (uses Status, fires +SelectDatabase) +. `+web/src/Pages/Query.res+` — Combines Editor + Results + error banner +. `+web/proxy/server.js+` — Deno CORS proxy server +. `+web/serve.js+` — Deno static file server for dev + +==== To implement each: + +*View.res*: Simple pattern match on `+model.route+`: - `+Picker+` → +`+Picker.make(~model, ~dispatch)+` - `+Query(_)+` → +`+Query.make(~model, ~dispatch)+` - `+NotFound+` → 404 page inline + +*App.res*: Use `+Tea_App.MakeWithDispatch+` with: - +`+type flags = unit+`, `+type model = Model.t+`, `+type msg = Msg.t+` - +`+init+` reads current URL via `+Tea_Url.current()+`, parses route, +creates model - `+init+` returns health-check command + URL listener +setup command - `+update = Update.update+`, `+view = View.make+`, +`+subscriptions = Subs.subscriptions+` + +*Index.res*: `+ReactDOM.Client.createRoot(...)+` → +`+root.render()+` + +*Picker.res*: Grid of cards, one per `+Database.all+`. Each card shows: +- displayName, languageName badge, description - Port number, health +status dot (from model.healthMap) - onClick dispatches +`+SelectDatabase(db.id)+` + +*Query.res*: Vertical layout: - Error banner (if model.error is Some) - +Editor pane (Editor.make) - Results pane (Results.make) + +*proxy/server.js*: Deno.serve on port 4000. Route `+/api/:dbId/*+` → +extract dbId, look up port from hardcoded map, forward request, add CORS +headers. + +*serve.js*: Deno.serve on port 8000, serves `+index.html+` + static +files. + +=== Build & Run + +[source,bash] +---- +cd nextgen-databases/nqc/web +bash setup.sh # One-time: install deps + symlink packages +deno task build # Compile ReScript +deno task proxy & # Start CORS proxy on :4000 +deno task dev # Serve web UI on :8000 +---- diff --git a/nqc/web/DESIGN-2026-02-22-nqc-web-ui.md b/nqc/web/DESIGN-2026-02-22-nqc-web-ui.md deleted file mode 100644 index c4590d41..00000000 --- a/nqc/web/DESIGN-2026-02-22-nqc-web-ui.md +++ /dev/null @@ -1,160 +0,0 @@ -# NQC Web UI — Design Document - -**Date:** 2026-02-22 -**Repo:** `nextgen-databases/nqc/` -**Author:** Claude (with Jonathan D.A. Jewell) -**Status:** COMPLETE — 48 modules, 0 errors, 0 warnings. All features implemented. - ---- - -## Overview - -A companion web UI for the NQC (NextGen Query Client) Gleam REPL. -Built with **rescript-tea** (TEA architecture) and **cadre-router** (URL routing). -The Gleam REPL at `src/` is UNCHANGED — this is a standalone addition in `web/`. - -## Architecture - -``` -web/ -├── rescript.json # ReScript 12 config, references local tea + cadre-router -├── deno.json # Deno deps + tasks (npm specifiers for react, rescript) -├── setup.sh # Creates symlinks for local ReScript packages -├── index.html # HTML shell + all CSS (dark terminal theme) -├── serve.js # DONE — Deno static file server (SPA fallback) -├── src/ -│ ├── Database.res # DONE — Profile type + VCL/GQL/KQL builtins (mirrors Gleam) -│ ├── Route.res # DONE — Route type + URL parser (cadre-router) -│ ├── Msg.res # DONE — Message variants + outputFormat/connectionState types -│ ├── Model.res # DONE — Application state + init function -│ ├── Api.res # DONE — HTTP commands (query, health) via CORS proxy -│ ├── Update.res # DONE — Pure update function (all state transitions) -│ ├── Subs.res # DONE — Subscriptions (currently none, placeholder) -│ ├── View.res # DONE Top-level view dispatch by route -│ ├── App.res # DONE TEA app wiring (MakeWithDispatch functor) -│ ├── Index.res # DONE ReactDOM.render entry point -│ ├── Pages/ -│ │ ├── Picker.res # DONE Database picker — card grid with health dots -│ │ └── Query.res # DONE Query interface — editor + results + format switch -│ └── Components/ -│ ├── Header.res # DONE — Nav bar with db badge, DT toggle, format tabs -│ ├── Editor.res # DONE — Query textarea with Ctrl+Enter and history -│ ├── Results.res # DONE — Table/JSON/CSV result renderer -│ └── Status.res # DONE — Connection health dot indicator -├── proxy/ -│ └── server.js # DONE Deno CORS proxy (forwards to db ports) -``` - -## Key Decisions - -### 1. MakeWithDispatch, not MakeSimple -`rescript-tea`'s `Tea_Html` module has NO element constructors (no `div`, `span`, etc.). -It expects JSX usage. Since JSX needs a `dispatch` function for event handlers, -we use `Tea_App.MakeWithDispatch` which passes `(model, dispatch)` to the view. - -### 2. URL routing via init command -`cadre-router`'s `Tea_Router.listen` is set up once in the app's init command -via `Tea_Cmd.effect`. It fires `UrlChanged` messages on browser back/forward. -Programmatic navigation uses `Tea_Navigation.execute(Push(...))` directly. - -### 3. CORS proxy pattern -Browser → localhost:4000 (Deno proxy) → localhost:808x (database engines). -The proxy maps `/api/:dbId/*` to the correct port based on database profiles. - -### 4. Raw JSON responses -Database engines return heterogeneous JSON. We decode as `JSON.t` (raw) -and render client-side based on the format selector (Table/JSON/CSV). -The `Results.res` component auto-detects columns from the first row. - -## Dependency Chain - -``` -nqc-web - ├── rescript-tea (local: ../../developer-ecosystem/rescript-ecosystem/packages/web/tea) - │ ├── @rescript/react (npm) - │ ├── @rescript/core (npm) - │ └── @proven/rescript-bindings (STUB — created by setup.sh) - ├── @anthropics/cadre-router (local: ../../developer-ecosystem/rescript-ecosystem/cadre-router) - │ ├── @rescript/react (npm) - │ ├── @rescript/core (npm) - │ └── rescript-wasm-runtime (STUB — created by setup.sh) - ├── @rescript/core (npm via deno.json) - └── @rescript/react (npm via deno.json) -``` - -`setup.sh` creates symlinks for local packages and stub rescript.json for transitive deps. - -## API Contracts - -### Query execution -``` -POST /api/{dbId}{executePath} -Body: {"query": "SELECT ...", "dt": false} -Response: JSON (shape varies by engine) -``` - -### Health check -``` -GET /api/{dbId}{healthPath} -Response: any 2xx = healthy -``` - -### Database ports -| DB | Port | Execute Path | Health Path | -|----|------|-------------|-------------| -| VCL (VeriSimDB) | 8080 | /vcl/execute | /health | -| GQL (Lithoglyph) | 8081 | /gql/execute | /health | -| KQL (QuandleDB) | 8082 | /kql/execute | /health | - -## How to Resume - -If this session was interrupted, here's what remains: - -### Files still TODO (as of writing): -1. `web/src/View.res` — Route-based view dispatch (calls Picker or Query page) -2. `web/src/App.res` — TEA MakeWithDispatch functor wiring + init command -3. `web/src/Index.res` — ReactDOM entry (render App into #root) -4. `web/src/Pages/Picker.res` — Database card grid (uses Status, fires SelectDatabase) -5. `web/src/Pages/Query.res` — Combines Editor + Results + error banner -6. `web/proxy/server.js` — Deno CORS proxy server -7. `web/serve.js` — Deno static file server for dev - -### To implement each: - -**View.res**: Simple pattern match on `model.route`: - - `Picker` → `Picker.make(~model, ~dispatch)` - - `Query(_)` → `Query.make(~model, ~dispatch)` - - `NotFound` → 404 page inline - -**App.res**: Use `Tea_App.MakeWithDispatch` with: - - `type flags = unit`, `type model = Model.t`, `type msg = Msg.t` - - `init` reads current URL via `Tea_Url.current()`, parses route, creates model - - `init` returns health-check command + URL listener setup command - - `update = Update.update`, `view = View.make`, `subscriptions = Subs.subscriptions` - -**Index.res**: `ReactDOM.Client.createRoot(...)` → `root.render()` - -**Picker.res**: Grid of cards, one per `Database.all`. Each card shows: - - displayName, languageName badge, description - - Port number, health status dot (from model.healthMap) - - onClick dispatches `SelectDatabase(db.id)` - -**Query.res**: Vertical layout: - - Error banner (if model.error is Some) - - Editor pane (Editor.make) - - Results pane (Results.make) - -**proxy/server.js**: Deno.serve on port 4000. Route `/api/:dbId/*` → - extract dbId, look up port from hardcoded map, forward request, add CORS headers. - -**serve.js**: Deno.serve on port 8000, serves `index.html` + static files. - -## Build & Run - -```bash -cd nextgen-databases/nqc/web -bash setup.sh # One-time: install deps + symlink packages -deno task build # Compile ReScript -deno task proxy & # Start CORS proxy on :4000 -deno task dev # Serve web UI on :8000 -``` diff --git a/typeql-experimental/WHITEPAPER.adoc b/typeql-experimental/WHITEPAPER.adoc new file mode 100644 index 00000000..f92f337a --- /dev/null +++ b/typeql-experimental/WHITEPAPER.adoc @@ -0,0 +1,487 @@ +== SPDX-License-Identifier: CC-BY-SA-4.0 + +== Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) j.d.a.jewell@open.ac.uk + +== TypeQL-Experimental: Dependent Types for Query Language Safety + +*Author:* Jonathan D.A. Jewell *Version:* 1.0 *Date:* 2026-03-14 +*Status:* Research (85% complete) + +''''' + +=== Abstract + +TypeQL-Experimental (VCL-UT) explores the application of Quantitative +Type Theory (QTT) to database query languages, demonstrating that six +categories of runtime database errors—connection leaks, protocol +violations, effect misuse, scope leakage, missing postcondition +guarantees, and resource over-consumption— can be eliminated entirely at +compile time through dependent types. Using Idris2’s native QTT, we +implement linear types for connection safety, indexed types for session +protocol compliance, effect subsumption for side-effect tracking, modal +types for transaction isolation, proof-carrying results for +postcondition guarantees, and bounded resource accounting for query +budgets. All nine Idris2 modules type-check with `+%default total+` and +zero uses of axiom-bypassing constructs (`+believe_me+`, +`+assert_total+`, `+assert_smaller+`), meaning every safety guarantee is +backed by a machine-checked proof. + +''''' + +=== 1. Introduction + +==== 1.1 The State of Database Safety + +Modern databases offer sophisticated query languages, transaction +protocols, and access control mechanisms. Yet six categories of bugs +persist across every major database system: + +[arabic] +. *Connection leaks:* Connections opened but never closed, or used after +closing, eventually exhausting the connection pool. +. *Protocol violations:* Querying before authenticating, committing +outside a transaction, or using a connection in an invalid state. +. *Effect misuse:* Write operations executed in read-only contexts, or +queries that silently perform side effects not declared in their +interface. +. *Scope leakage:* Data from one transaction scope leaking into another, +violating isolation guarantees. +. *Missing postconditions:* Query results lacking guarantees about +integrity, freshness, or provenance that downstream consumers require. +. *Resource over-consumption:* Queries that exceed their allocated +budget (connections, API calls, federation requests). + +These bugs are not caused by careless programming. They arise because +the _type systems_ of existing query languages and host language +bindings cannot express the relevant invariants. Connection safety +requires linear types. Protocol compliance requires indexed types. +Effect tracking requires effect systems. Transaction isolation requires +modal types. These are all features of dependent type theory that SQL +and its derivatives lack. + +==== 1.2 Dependent Types for Databases + +Dependent types (Martin-Löf, 1984) allow types to depend on values, +enabling the expression of precise invariants at the type level. A +dependent type system can express: + +* "`This connection has exactly 3 uses remaining`" (indexed type). +* "`This session is in the Authenticated state`" (indexed type). +* "`This query performs only Read effects`" (effect system via dependent +pairs). +* "`This data was produced in transaction scope W₁`" (modal type). + +Idris2 (Brady, 2021) implements Quantitative Type Theory (Atkey, 2018), +which adds _usage quantities_ to every binding: `+0+` (erased at +runtime), `+1+` (used exactly once, i.e., linear), or `+ω+` +(unrestricted). This makes linear types a native feature of the +language, not an encoding. + +==== 1.3 Contributions + +[arabic] +. *Six type-theoretic extensions* to VCL (VeriSim Consonance Language) +that eliminate the six bug categories above at compile time (Section 3). +. *A dual-language architecture* where Idris2 proves properties and +ReScript parses queries, connected by a Zig FFI bridge (Section 4). +. *Zero-axiom proofs*: All guarantees are machine-checked with no escape +hatches (Section 5). +. *Backwards-compatible grammar*: All extensions are optional clauses +appended to standard VCL queries, requiring no changes to existing +queries (Section 6). + +''''' + +=== 2. Background + +==== 2.1 VCL v3.0 + +VeriSim Consonance Language (VCL) is the query language for VeriSimDB, a +multi-modal database with eight query modalities (GRAPH, DOCUMENT, +VECTOR, TIME_SERIES, SPATIAL, STATISTICAL, SEMANTIC, RELATIONAL). VCL +supports cross-modal queries via HEXAD references (content-addressed +UUIDs). + +==== 2.2 Quantitative Type Theory + +QTT (Atkey, 2018; McBride, 2016) extends dependent type theory with a +semiring of quantities on each variable binding. In Idris2: + +[source,idris] +---- +-- Unrestricted: can use 'x' any number of times +f : (x : Nat) -> Nat + +-- Linear: must use 'conn' exactly once +g : (1 conn : Connection) -> IO Result + +-- Erased: 'prf' exists only at compile time +h : (0 prf : IsValid x) -> Result +---- + +The quantity `+1+` enforces linearity: the compiler rejects any code +that uses a linear variable zero times or more than once. This is not an +annotation—it is a _proof obligation_ that the compiler verifies. + +==== 2.3 Prior Work + +* *HoTTSQL* (Chu et al., PLDI 2017): Uses HoTT to prove SQL query +rewrite equivalence. Does not extend SQL’s type system. +* *Links* (Cooper et al., 2006): Language-integrated query with row +types. No linear types or session types. +* *Ur/Web* (Chlipala, 2015): Dependent types for web programming with +SQL. Closest predecessor, but no QTT, no session types, no effect +tracking. + +TypeQL-Experimental differs from all prior work in applying QTT +_natively_ to database queries, making linear types and resource +accounting first-class rather than encoded. + +''''' + +=== 3. The Six Extensions + +==== 3.1 Linear Types: CONSUME AFTER N USE + +*Problem:* Connection leaks and use-after-close bugs. + +*Solution:* Connections carry a type-level usage counter: + +[source,vcl] +---- +SELECT GRAPH, DOCUMENT +FROM HEXAD 550e8400-e29b-41d4-a716-446655440000 +CONSUME AFTER 1 USE +---- + +*Type-level encoding:* + +[source,idris] +---- +data LinConn : (remaining : Nat) -> Type where + MkLinConn : (handle : Bits64) -> LinConn remaining + +useConn : (1 _ : LinConn (S n)) -> (QueryResult, LinConn n) +closeConn : (1 _ : LinConn 0) -> IO () +---- + +The type `+LinConn (S n)+` can be used (producing `+LinConn n+`), and +`+LinConn 0+` can only be closed. The `+1+` quantity on the argument +ensures exactly-once consumption. Attempting to use a connection twice +is a _compile error_, not a runtime exception. + +==== 3.2 Session Types: WITH SESSION + +*Problem:* Protocol violations (querying before auth, committing twice). + +*Solution:* Sessions are indexed by their protocol state: + +[source,vcl] +---- +SELECT GRAPH FROM HEXAD ... +WITH SESSION ReadOnlyProtocol +---- + +*Type-level encoding:* + +[source,idris] +---- +data SessionState = Fresh | Authenticated | InTransaction | Committed | Closed + +data Session : SessionState -> Type where + MkFresh : Session Fresh + +authenticate : (1 _ : Session Fresh) -> Either AuthError (Session Authenticated) +beginTx : (1 _ : Session Authenticated) -> Session InTransaction +query : (1 _ : Session InTransaction) -> QueryPlan -> (QueryResult, Session InTransaction) +commit : (1 _ : Session InTransaction) -> Either TxError (Session Committed) +close : (1 _ : Session s) -> {auto prf : CanClose s} -> IO () +---- + +Each operation consumes the session linearly and produces the next +state. `+query+` requires `+Session InTransaction+`—calling it with +`+Session Fresh+` is a type error. The state machine is enforced by the +compiler. + +==== 3.3 Effect Systems: EFFECTS \{ Read, Write, … } + +*Problem:* Undeclared side effects in queries. + +*Solution:* Queries declare their effects; the type checker verifies +actual effects are a subset of declared effects: + +[source,vcl] +---- +SELECT GRAPH FROM HEXAD ... +EFFECTS { Read } +---- + +*Type-level encoding:* + +[source,idris] +---- +data Effect = Read | Write | Cite | Audit | Transform | Federate + +Subsumes : (declared : List Effect) -> (actual : List Effect) -> Type +Subsumes declared actual = Subset actual declared +---- + +If a query declared as `+EFFECTS { Read }+` attempts a Write, the type +checker cannot construct `+Subsumes [Read] [Write]+` (because Write ∉ +[Read]), and the query is rejected. + +==== 3.4 Modal Types: IN TRANSACTION + +*Problem:* Data leaking between transaction scopes. + +*Solution:* Data is tagged with its transaction scope at the type level: + +[source,vcl] +---- +SELECT GRAPH FROM HEXAD ... +IN TRANSACTION Committed +---- + +*Type-level encoding:* + +[source,idris] +---- +data World = Fresh | Active | Committed | RolledBack | ReadSnapshot + +data Box : World -> Type -> Type where + MkBox : a -> Box w a + +extract : Box w a -> {auto prf : InScope w} -> a +marshal : Box w1 a -> (a -> b) -> Box w2 b +---- + +Data in `+Box w1 a+` can only be extracted with evidence that we are +`+InScope w1+`. Moving data between worlds requires explicit +`+marshal+`, making cross-scope data flow visible in types. + +==== 3.5 Proof-Carrying Code: PROOF ATTACHED + +*Problem:* Results lack formal guarantees for downstream consumers. + +*Solution:* Results are bundled with proofs of postconditions: + +[source,vcl] +---- +SELECT GRAPH FROM HEXAD ... +PROOF ATTACHED IntegrityTheorem +---- + +*Type-level encoding:* + +[source,idris] +---- +data Theorem = IntegrityThm | FreshnessThm | ProvenanceThm | ConsistencyThm + +ProvedResult : Type -> Theorem -> Type +ProvedResult a thm = (result : a ** ProofOf thm result) +---- + +The result type is a dependent pair: the data _and_ a proof that the +data satisfies the stated theorem. Downstream consumers can verify the +proof independently. + +==== 3.6 Quantitative Type Theory: USAGE LIMIT + +*Problem:* Resource over-consumption in federation or API-limited +contexts. + +*Solution:* Resources carry a type-level budget: + +[source,vcl] +---- +SELECT GRAPH FROM FEDERATION /universities/* +USAGE LIMIT 100 +---- + +*Type-level encoding:* + +[source,idris] +---- +data BoundedResource : (limit : Nat) -> Type where + MkBounded : a -> BoundedResource limit + +consume : BoundedResource (S n) a -> (a, BoundedResource n a) +-- BoundedResource 0 has no consume operation: it's depleted +---- + +This generalises linear types: `+BoundedResource 1+` is equivalent to a +linear resource, while `+BoundedResource 100+` allows exactly 100 uses. + +''''' + +=== 4. Architecture + +==== 4.1 Dual-Language Split + +[width="100%",cols="28%,38%,34%",options="header",] +|=== +|Layer |Language |Purpose +|*Type kernel* |Idris2 (9 modules) |Formal specification, proof checking +|*Parser* |ReScript (2 files) |Surface syntax parsing +|*FFI bridge* |Zig (3 files) |C-ABI bridge for external consumers +|=== + +*Design rationale:* In the research phase, Idris2 and ReScript operate +independently. Idris2 proves type properties; ReScript parses queries. +Future integration would wire parsed ASTs to Idris2 proofs. This +separation allows rapid iteration on both fronts. + +==== 4.2 Module Structure + +.... +src/abi/ +├── Core.idr -- Foundation: modalities, effects, quantities +├── Linear.idr -- LinConn indexed by remaining uses +├── Session.idr -- Session state machine +├── Effects.idr -- Effect subsumption +├── Modal.idr -- World-indexed boxes +├── ProofCarrying.idr -- Theorem attachment +├── Quantitative.idr -- Bounded resources +├── Checker.idr -- Unified validation (composes all 6) +└── Proofs.idr -- Cross-cutting proofs +.... + +==== 4.3 Verification Status + +All 9 modules compile under `+%default total+` with zero banned +patterns: + +* Zero `+believe_me+` (axiom assertion) +* Zero `+assert_total+` (totality override) +* Zero `+assert_smaller+` (termination override) + +Every proof is real. The type system enforces soundness. + +''''' + +=== 5. Cross-Extension Proofs + +==== 5.1 Key Theorems + +The `+Proofs.idr+` module proves cross-cutting properties: + +[arabic] +. *Linear exact use:* Using a `+LinConn n+` exactly n times produces +`+LinConn 0+`. This ensures connection pools are never exhausted by +"`stranded`" connections. +. *Effect subsumption reflexivity:* `+Subsumes es es+` is always +provable. A query’s declared effects always permit themselves. +. *Effect subsumption transitivity:* If `+Subsumes a b+` and +`+Subsumes b c+`, then `+Subsumes a c+`. Effect permissions compose. +. *Budget fits:* A `+BoundedResource n+` can perform at most n +operations before depletion. The type system prevents over-consumption. + +==== 5.2 Composability + +The six extensions compose without interference: + +[source,vcl] +---- +SELECT GRAPH, DOCUMENT +FROM HEXAD 550e8400-e29b-41d4-a716-446655440000 +CONSUME AFTER 1 USE +WITH SESSION ReadOnlyProtocol +EFFECTS { Read, Cite } +IN TRANSACTION Committed +PROOF ATTACHED IntegrityTheorem +USAGE LIMIT 100 +---- + +The type checker validates all six constraints simultaneously. The +`+Checker.idr+` module composes individual checks, and their +independence is guaranteed by the fact that each extension operates on a +different dimension of the type. + +''''' + +=== 6. Grammar + +==== 6.1 Backwards Compatibility + +All extensions are optional clauses appended after standard VCL queries: + +[source,ebnf] +---- +extended_query = query, + [consume_clause], + [session_clause], + [effects_clause], + [modal_clause], + [proof_attached_clause], + [usage_clause] ; + +consume_clause = 'CONSUME', 'AFTER', positive_integer, 'USE' ; +session_clause = 'WITH', 'SESSION', protocol_name ; +effects_clause = 'EFFECTS', '{', effect_list, '}' ; +modal_clause = 'IN', 'TRANSACTION', transaction_state ; +proof_attached_clause = 'PROOF', 'ATTACHED', theorem_name ; +usage_clause = 'USAGE', 'LIMIT', positive_integer ; +---- + +No existing VCL keywords are reused. All new keywords (CONSUME, AFTER, +USE, SESSION, EFFECTS, TRANSACTION, ATTACHED, USAGE) are disjoint from +VCL’s 60+ existing keywords. + +==== 6.2 File Extension + +TypeQL-Experimental queries use the `+.vclut+` extension (VCL Ultimate +Type-Safe), distinguishing them from standard `+.vcl+` files. +(Previously `+.vclpp+` — renamed to align with VCL-UT canonical naming.) + +''''' + +=== 7. Related Work + +[width="100%",cols="16%,13%,15%,13%,11%,11%,21%",options="header",] +|=== +|System |Linear |Session |Effect |Modal |Proof |Quantitative +|SQL |No |No |No |No |No |No +|HoTTSQL |No |No |No |No |Yes* |No +|Ur/Web |No |No |No |No |Partial |No +|Links |No |No |No |No |No |No +|*TypeQL-Exp* |*Yes* |*Yes* |*Yes* |*Yes* |*Yes* |*Yes* +|=== + +*HoTTSQL proves query rewrite equivalence, not result properties. + +''''' + +=== 8. Conclusion + +TypeQL-Experimental demonstrates that dependent types—specifically +Quantitative Type Theory as implemented in Idris2—can eliminate six +entire categories of database errors at compile time. The key insight is +that QTT’s native linear types make connection safety and resource +budgeting _free_: the language already tracks usage quantities on every +binding, so `+CONSUME AFTER 1 USE+` maps directly to +`+(1 conn : Connection)+`. + +The six extensions compose independently, require no changes to existing +VCL queries, and are backed by machine-checked proofs with no axiom +escape hatches. This work suggests that the next generation of query +languages should integrate dependent type systems not as an academic +exercise but as a practical tool for eliminating entire bug categories. + +''''' + +=== References + +[arabic] +. Atkey, R. (2018). "`Syntax and Semantics of Quantitative Type +Theory.`" _LICS 2018_, 56–65. +. Brady, E. (2021). "`Idris 2: Quantitative Type Theory in Practice.`" +_ECOOP 2021_, 9:1–9:26. +. Chlipala, A. (2015). "`Ur/Web: A Simple Model for Programming the +Web.`" _POPL 2015_, 153–165. +. Chu, S. et al. (2017). "`HoTTSQL: Proving Query Rewrites with +Univalent SQL Semantics.`" _PLDI 2017_, 510–524. +. Cooper, E. et al. (2006). "`Links: Web Programming Without Tiers.`" +_FMCO 2006_, 266–296. +. Martin-Löf, P. (1984). _Intuitionistic Type Theory_. Bibliopolis. +. McBride, C. (2016). "`I Got Plenty o’ Nuttin’.`" _A List of Successes +That Can Change the World_, 207–233. diff --git a/typeql-experimental/WHITEPAPER.md b/typeql-experimental/WHITEPAPER.md deleted file mode 100644 index 1f5ba4ec..00000000 --- a/typeql-experimental/WHITEPAPER.md +++ /dev/null @@ -1,461 +0,0 @@ -# SPDX-License-Identifier: CC-BY-SA-4.0 -# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) - -# TypeQL-Experimental: Dependent Types for Query Language Safety - -**Author:** Jonathan D.A. Jewell -**Version:** 1.0 -**Date:** 2026-03-14 -**Status:** Research (85% complete) - ---- - -## Abstract - -TypeQL-Experimental (VCL-UT) explores the application of Quantitative Type -Theory (QTT) to database query languages, demonstrating that six categories of -runtime database errors—connection leaks, protocol violations, effect misuse, -scope leakage, missing postcondition guarantees, and resource over-consumption— -can be eliminated entirely at compile time through dependent types. Using Idris2's -native QTT, we implement linear types for connection safety, indexed types for -session protocol compliance, effect subsumption for side-effect tracking, modal -types for transaction isolation, proof-carrying results for postcondition -guarantees, and bounded resource accounting for query budgets. All nine Idris2 -modules type-check with `%default total` and zero uses of axiom-bypassing -constructs (`believe_me`, `assert_total`, `assert_smaller`), meaning every -safety guarantee is backed by a machine-checked proof. - ---- - -## 1. Introduction - -### 1.1 The State of Database Safety - -Modern databases offer sophisticated query languages, transaction protocols, -and access control mechanisms. Yet six categories of bugs persist across every -major database system: - -1. **Connection leaks:** Connections opened but never closed, or used after - closing, eventually exhausting the connection pool. - -2. **Protocol violations:** Querying before authenticating, committing outside - a transaction, or using a connection in an invalid state. - -3. **Effect misuse:** Write operations executed in read-only contexts, or - queries that silently perform side effects not declared in their interface. - -4. **Scope leakage:** Data from one transaction scope leaking into another, - violating isolation guarantees. - -5. **Missing postconditions:** Query results lacking guarantees about integrity, - freshness, or provenance that downstream consumers require. - -6. **Resource over-consumption:** Queries that exceed their allocated budget - (connections, API calls, federation requests). - -These bugs are not caused by careless programming. They arise because the -*type systems* of existing query languages and host language bindings cannot -express the relevant invariants. Connection safety requires linear types. -Protocol compliance requires indexed types. Effect tracking requires effect -systems. Transaction isolation requires modal types. These are all features -of dependent type theory that SQL and its derivatives lack. - -### 1.2 Dependent Types for Databases - -Dependent types (Martin-Löf, 1984) allow types to depend on values, enabling -the expression of precise invariants at the type level. A dependent type system -can express: - -- "This connection has exactly 3 uses remaining" (indexed type). -- "This session is in the Authenticated state" (indexed type). -- "This query performs only Read effects" (effect system via dependent pairs). -- "This data was produced in transaction scope W₁" (modal type). - -Idris2 (Brady, 2021) implements Quantitative Type Theory (Atkey, 2018), which -adds *usage quantities* to every binding: `0` (erased at runtime), `1` (used -exactly once, i.e., linear), or `ω` (unrestricted). This makes linear types -a native feature of the language, not an encoding. - -### 1.3 Contributions - -1. **Six type-theoretic extensions** to VCL (VeriSim Consonance Language) that - eliminate the six bug categories above at compile time (Section 3). - -2. **A dual-language architecture** where Idris2 proves properties and ReScript - parses queries, connected by a Zig FFI bridge (Section 4). - -3. **Zero-axiom proofs**: All guarantees are machine-checked with no escape - hatches (Section 5). - -4. **Backwards-compatible grammar**: All extensions are optional clauses appended - to standard VCL queries, requiring no changes to existing queries (Section 6). - ---- - -## 2. Background - -### 2.1 VCL v3.0 - -VeriSim Consonance Language (VCL) is the query language for VeriSimDB, a multi-modal -database with eight query modalities (GRAPH, DOCUMENT, VECTOR, TIME_SERIES, -SPATIAL, STATISTICAL, SEMANTIC, RELATIONAL). VCL supports cross-modal queries -via HEXAD references (content-addressed UUIDs). - -### 2.2 Quantitative Type Theory - -QTT (Atkey, 2018; McBride, 2016) extends dependent type theory with a semiring -of quantities on each variable binding. In Idris2: - -```idris --- Unrestricted: can use 'x' any number of times -f : (x : Nat) -> Nat - --- Linear: must use 'conn' exactly once -g : (1 conn : Connection) -> IO Result - --- Erased: 'prf' exists only at compile time -h : (0 prf : IsValid x) -> Result -``` - -The quantity `1` enforces linearity: the compiler rejects any code that uses -a linear variable zero times or more than once. This is not an annotation—it -is a *proof obligation* that the compiler verifies. - -### 2.3 Prior Work - -- **HoTTSQL** (Chu et al., PLDI 2017): Uses HoTT to prove SQL query rewrite - equivalence. Does not extend SQL's type system. -- **Links** (Cooper et al., 2006): Language-integrated query with row types. - No linear types or session types. -- **Ur/Web** (Chlipala, 2015): Dependent types for web programming with SQL. - Closest predecessor, but no QTT, no session types, no effect tracking. - -TypeQL-Experimental differs from all prior work in applying QTT *natively* to -database queries, making linear types and resource accounting first-class -rather than encoded. - ---- - -## 3. The Six Extensions - -### 3.1 Linear Types: CONSUME AFTER N USE - -**Problem:** Connection leaks and use-after-close bugs. - -**Solution:** Connections carry a type-level usage counter: - -```vcl -SELECT GRAPH, DOCUMENT -FROM HEXAD 550e8400-e29b-41d4-a716-446655440000 -CONSUME AFTER 1 USE -``` - -**Type-level encoding:** - -```idris -data LinConn : (remaining : Nat) -> Type where - MkLinConn : (handle : Bits64) -> LinConn remaining - -useConn : (1 _ : LinConn (S n)) -> (QueryResult, LinConn n) -closeConn : (1 _ : LinConn 0) -> IO () -``` - -The type `LinConn (S n)` can be used (producing `LinConn n`), and `LinConn 0` -can only be closed. The `1` quantity on the argument ensures exactly-once -consumption. Attempting to use a connection twice is a *compile error*, not a -runtime exception. - -### 3.2 Session Types: WITH SESSION - -**Problem:** Protocol violations (querying before auth, committing twice). - -**Solution:** Sessions are indexed by their protocol state: - -```vcl -SELECT GRAPH FROM HEXAD ... -WITH SESSION ReadOnlyProtocol -``` - -**Type-level encoding:** - -```idris -data SessionState = Fresh | Authenticated | InTransaction | Committed | Closed - -data Session : SessionState -> Type where - MkFresh : Session Fresh - -authenticate : (1 _ : Session Fresh) -> Either AuthError (Session Authenticated) -beginTx : (1 _ : Session Authenticated) -> Session InTransaction -query : (1 _ : Session InTransaction) -> QueryPlan -> (QueryResult, Session InTransaction) -commit : (1 _ : Session InTransaction) -> Either TxError (Session Committed) -close : (1 _ : Session s) -> {auto prf : CanClose s} -> IO () -``` - -Each operation consumes the session linearly and produces the next state. -`query` requires `Session InTransaction`—calling it with `Session Fresh` is -a type error. The state machine is enforced by the compiler. - -### 3.3 Effect Systems: EFFECTS { Read, Write, ... } - -**Problem:** Undeclared side effects in queries. - -**Solution:** Queries declare their effects; the type checker verifies actual -effects are a subset of declared effects: - -```vcl -SELECT GRAPH FROM HEXAD ... -EFFECTS { Read } -``` - -**Type-level encoding:** - -```idris -data Effect = Read | Write | Cite | Audit | Transform | Federate - -Subsumes : (declared : List Effect) -> (actual : List Effect) -> Type -Subsumes declared actual = Subset actual declared -``` - -If a query declared as `EFFECTS { Read }` attempts a Write, the type checker -cannot construct `Subsumes [Read] [Write]` (because Write ∉ [Read]), and the -query is rejected. - -### 3.4 Modal Types: IN TRANSACTION - -**Problem:** Data leaking between transaction scopes. - -**Solution:** Data is tagged with its transaction scope at the type level: - -```vcl -SELECT GRAPH FROM HEXAD ... -IN TRANSACTION Committed -``` - -**Type-level encoding:** - -```idris -data World = Fresh | Active | Committed | RolledBack | ReadSnapshot - -data Box : World -> Type -> Type where - MkBox : a -> Box w a - -extract : Box w a -> {auto prf : InScope w} -> a -marshal : Box w1 a -> (a -> b) -> Box w2 b -``` - -Data in `Box w1 a` can only be extracted with evidence that we are `InScope w1`. -Moving data between worlds requires explicit `marshal`, making cross-scope -data flow visible in types. - -### 3.5 Proof-Carrying Code: PROOF ATTACHED - -**Problem:** Results lack formal guarantees for downstream consumers. - -**Solution:** Results are bundled with proofs of postconditions: - -```vcl -SELECT GRAPH FROM HEXAD ... -PROOF ATTACHED IntegrityTheorem -``` - -**Type-level encoding:** - -```idris -data Theorem = IntegrityThm | FreshnessThm | ProvenanceThm | ConsistencyThm - -ProvedResult : Type -> Theorem -> Type -ProvedResult a thm = (result : a ** ProofOf thm result) -``` - -The result type is a dependent pair: the data *and* a proof that the data -satisfies the stated theorem. Downstream consumers can verify the proof -independently. - -### 3.6 Quantitative Type Theory: USAGE LIMIT - -**Problem:** Resource over-consumption in federation or API-limited contexts. - -**Solution:** Resources carry a type-level budget: - -```vcl -SELECT GRAPH FROM FEDERATION /universities/* -USAGE LIMIT 100 -``` - -**Type-level encoding:** - -```idris -data BoundedResource : (limit : Nat) -> Type where - MkBounded : a -> BoundedResource limit - -consume : BoundedResource (S n) a -> (a, BoundedResource n a) --- BoundedResource 0 has no consume operation: it's depleted -``` - -This generalises linear types: `BoundedResource 1` is equivalent to a linear -resource, while `BoundedResource 100` allows exactly 100 uses. - ---- - -## 4. Architecture - -### 4.1 Dual-Language Split - -| Layer | Language | Purpose | -|-------|----------|---------| -| **Type kernel** | Idris2 (9 modules) | Formal specification, proof checking | -| **Parser** | ReScript (2 files) | Surface syntax parsing | -| **FFI bridge** | Zig (3 files) | C-ABI bridge for external consumers | - -**Design rationale:** In the research phase, Idris2 and ReScript operate -independently. Idris2 proves type properties; ReScript parses queries. Future -integration would wire parsed ASTs to Idris2 proofs. This separation allows -rapid iteration on both fronts. - -### 4.2 Module Structure - -``` -src/abi/ -├── Core.idr -- Foundation: modalities, effects, quantities -├── Linear.idr -- LinConn indexed by remaining uses -├── Session.idr -- Session state machine -├── Effects.idr -- Effect subsumption -├── Modal.idr -- World-indexed boxes -├── ProofCarrying.idr -- Theorem attachment -├── Quantitative.idr -- Bounded resources -├── Checker.idr -- Unified validation (composes all 6) -└── Proofs.idr -- Cross-cutting proofs -``` - -### 4.3 Verification Status - -All 9 modules compile under `%default total` with zero banned patterns: - -- Zero `believe_me` (axiom assertion) -- Zero `assert_total` (totality override) -- Zero `assert_smaller` (termination override) - -Every proof is real. The type system enforces soundness. - ---- - -## 5. Cross-Extension Proofs - -### 5.1 Key Theorems - -The `Proofs.idr` module proves cross-cutting properties: - -1. **Linear exact use:** Using a `LinConn n` exactly n times produces - `LinConn 0`. This ensures connection pools are never exhausted by - "stranded" connections. - -2. **Effect subsumption reflexivity:** `Subsumes es es` is always provable. - A query's declared effects always permit themselves. - -3. **Effect subsumption transitivity:** If `Subsumes a b` and `Subsumes b c`, - then `Subsumes a c`. Effect permissions compose. - -4. **Budget fits:** A `BoundedResource n` can perform at most n operations - before depletion. The type system prevents over-consumption. - -### 5.2 Composability - -The six extensions compose without interference: - -```vcl -SELECT GRAPH, DOCUMENT -FROM HEXAD 550e8400-e29b-41d4-a716-446655440000 -CONSUME AFTER 1 USE -WITH SESSION ReadOnlyProtocol -EFFECTS { Read, Cite } -IN TRANSACTION Committed -PROOF ATTACHED IntegrityTheorem -USAGE LIMIT 100 -``` - -The type checker validates all six constraints simultaneously. The `Checker.idr` -module composes individual checks, and their independence is guaranteed by the -fact that each extension operates on a different dimension of the type. - ---- - -## 6. Grammar - -### 6.1 Backwards Compatibility - -All extensions are optional clauses appended after standard VCL queries: - -```ebnf -extended_query = query, - [consume_clause], - [session_clause], - [effects_clause], - [modal_clause], - [proof_attached_clause], - [usage_clause] ; - -consume_clause = 'CONSUME', 'AFTER', positive_integer, 'USE' ; -session_clause = 'WITH', 'SESSION', protocol_name ; -effects_clause = 'EFFECTS', '{', effect_list, '}' ; -modal_clause = 'IN', 'TRANSACTION', transaction_state ; -proof_attached_clause = 'PROOF', 'ATTACHED', theorem_name ; -usage_clause = 'USAGE', 'LIMIT', positive_integer ; -``` - -No existing VCL keywords are reused. All new keywords (CONSUME, AFTER, USE, -SESSION, EFFECTS, TRANSACTION, ATTACHED, USAGE) are disjoint from VCL's 60+ -existing keywords. - -### 6.2 File Extension - -TypeQL-Experimental queries use the `.vclut` extension (VCL Ultimate Type-Safe), -distinguishing them from standard `.vcl` files. (Previously `.vclpp` — renamed to align with VCL-UT canonical naming.) - ---- - -## 7. Related Work - -| System | Linear | Session | Effect | Modal | Proof | Quantitative | -|--------|--------|---------|--------|-------|-------|-------------| -| SQL | No | No | No | No | No | No | -| HoTTSQL | No | No | No | No | Yes* | No | -| Ur/Web | No | No | No | No | Partial | No | -| Links | No | No | No | No | No | No | -| **TypeQL-Exp** | **Yes** | **Yes** | **Yes** | **Yes** | **Yes** | **Yes** | - -*HoTTSQL proves query rewrite equivalence, not result properties. - ---- - -## 8. Conclusion - -TypeQL-Experimental demonstrates that dependent types—specifically Quantitative -Type Theory as implemented in Idris2—can eliminate six entire categories of -database errors at compile time. The key insight is that QTT's native linear -types make connection safety and resource budgeting *free*: the language already -tracks usage quantities on every binding, so `CONSUME AFTER 1 USE` maps directly -to `(1 conn : Connection)`. - -The six extensions compose independently, require no changes to existing VCL -queries, and are backed by machine-checked proofs with no axiom escape hatches. -This work suggests that the next generation of query languages should integrate -dependent type systems not as an academic exercise but as a practical tool for -eliminating entire bug categories. - ---- - -## References - -1. Atkey, R. (2018). "Syntax and Semantics of Quantitative Type Theory." - *LICS 2018*, 56–65. -2. Brady, E. (2021). "Idris 2: Quantitative Type Theory in Practice." - *ECOOP 2021*, 9:1–9:26. -3. Chlipala, A. (2015). "Ur/Web: A Simple Model for Programming the Web." - *POPL 2015*, 153–165. -4. Chu, S. et al. (2017). "HoTTSQL: Proving Query Rewrites with Univalent - SQL Semantics." *PLDI 2017*, 510–524. -5. Cooper, E. et al. (2006). "Links: Web Programming Without Tiers." - *FMCO 2006*, 266–296. -6. Martin-Löf, P. (1984). *Intuitionistic Type Theory*. Bibliopolis. -7. McBride, C. (2016). "I Got Plenty o' Nuttin'." *A List of Successes That - Can Change the World*, 207–233. diff --git a/typeql-experimental/spec/operational-semantics.md b/typeql-experimental/spec/operational-semantics.adoc similarity index 82% rename from typeql-experimental/spec/operational-semantics.md rename to typeql-experimental/spec/operational-semantics.adoc index 87d4a49c..bdc49140 100644 --- a/typeql-experimental/spec/operational-semantics.md +++ b/typeql-experimental/spec/operational-semantics.adoc @@ -1,26 +1,27 @@ -# SPDX-License-Identifier: CC-BY-SA-4.0 -# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +== SPDX-License-Identifier: CC-BY-SA-4.0 -# TypeQL-Experimental Operational Semantics +== Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) j.d.a.jewell@open.ac.uk -**Version:** 1.0.0 -**Date:** 2026-03-14 +== TypeQL-Experimental Operational Semantics ---- +*Version:* 1.0.0 *Date:* 2026-03-14 -## 1. Notation +''''' -- `Γ` — Type context (variable typing assumptions) -- `D` — Database state -- `Γ, D ⊢ q : τ ⇓ v` — Query `q` has type `τ` and evaluates to `v` -- `Γ ⊢ q : τ` — Query `q` type-checks to `τ` (compile-time) -- Quantities: `0` (erased), `1` (linear), `ω` (unrestricted) +=== 1. Notation ---- +* `+Γ+` — Type context (variable typing assumptions) +* `+D+` — Database state +* `+Γ, D ⊢ q : τ ⇓ v+` — Query `+q+` has type `+τ+` and evaluates to +`+v+` +* `+Γ ⊢ q : τ+` — Query `+q+` type-checks to `+τ+` (compile-time) +* Quantities: `+0+` (erased), `+1+` (linear), `+ω+` (unrestricted) -## 2. Values +''''' -``` +=== 2. Values + +.... v ∈ Value ::= QueryResult(rows) query result set | LinConn(handle, remaining) linear connection (indexed by uses) @@ -29,15 +30,15 @@ v ∈ Value ::= | ProvedResult(v, proof) result with attached theorem | BoundedResource(v, remaining) usage-limited resource | EffectSet(effects) declared effect set -``` +.... ---- +''''' -## 3. Type System (Compile-Time) +=== 3. Type System (Compile-Time) -### 3.1 Linear Types (CONSUME AFTER N USE) +==== 3.1 Linear Types (CONSUME AFTER N USE) -``` +.... Γ, (1 conn : LinConn (S n)) ⊢ query : τ ───────────────────────────────────────────────────────── [Lin-Use] Γ ⊢ useConn(conn) : (QueryResult, LinConn n) @@ -49,11 +50,11 @@ v ∈ Value ::= conn used twice (linear quantity violated) ────────────────────────────────────────────────────── [Lin-Error] Γ ⊢ program ⇒ TYPE ERROR: linear variable used more than once -``` +.... -### 3.2 Session Types (WITH SESSION) +==== 3.2 Session Types (WITH SESSION) -``` +.... Γ, (1 s : Session Fresh) ⊢ auth(s) : Either AuthError (Session Authenticated) ──────────────────────────────────────────────────────────────────────────── [Sess-Auth] @@ -66,11 +67,11 @@ v ∈ Value ::= Γ, (1 s : Session Fresh) ⊢ query(s, plan) ⇒ TYPE ERROR ───────────────────────────────────────────────────────── [Sess-Error] (query requires Session InTransaction, not Session Fresh) -``` +.... -### 3.3 Effect System (EFFECTS) +==== 3.3 Effect System (EFFECTS) -``` +.... actual_effects(q) = {Read} declared = {Read} actual ⊆ declared ────────────────────────────────────────────────────── [Eff-Ok] @@ -84,11 +85,11 @@ v ∈ Value ::= Subsumes(declared, actual) = ∀e ∈ actual. e ∈ declared ────────────────────────────────────────────────── [Eff-Subsumes] Γ ⊢ Subsumes(declared, actual) : Type -``` +.... -### 3.4 Modal Types (IN TRANSACTION) +==== 3.4 Modal Types (IN TRANSACTION) -``` +.... Γ ⊢ v : a w : World ─────────────────────────── [Modal-Box] Γ ⊢ MkBox(v) : Box w a @@ -104,11 +105,11 @@ v ∈ Value ::= Γ ⊢ b : Box w₁ a attempt extract without InScope w₁ ────────────────────────────────────────────────────────── [Modal-Error] TYPE ERROR: cannot extract from Box w₁ without InScope w₁ evidence -``` +.... -### 3.5 Proof-Carrying Code (PROOF ATTACHED) +==== 3.5 Proof-Carrying Code (PROOF ATTACHED) -``` +.... Γ ⊢ q : QueryResult Γ ⊢ thm : Theorem Γ ⊢ verify(q, thm) succeeds ───────────────────────────────────────────────── [Proof-Attach] @@ -117,34 +118,34 @@ v ∈ Value ::= ProvedResult(v, prf) = (result : τ ** ProofOf thm result) ───────────────────────────────────────────────────────── [Proof-Type] (dependent pair: data bundled with its proof) -``` +.... -### 3.6 Quantitative Types (USAGE LIMIT) +==== 3.6 Quantitative Types (USAGE LIMIT) -``` +.... Γ, (r : BoundedResource (S n) a) ⊢ consume(r) : (a, BoundedResource n a) ───────────────────────────────────────────────────────────────────────── [Quant-Consume] Γ, (r : BoundedResource 0 a) ⊢ consume(r) ⇒ TYPE ERROR ────────────────────────────────────────────────────────── [Quant-Depleted] (no consume operation exists on BoundedResource 0) -``` +.... ---- +''''' -## 4. Runtime Semantics +=== 4. Runtime Semantics -### 4.1 Query Evaluation (standard VCL pipeline) +==== 4.1 Query Evaluation (standard VCL pipeline) -``` +.... D ⊢ SELECT modalities FROM hexad WHERE conditions ⇓ rows ──────────────────────────────────────────────────────────── [Query-Base] Γ, D ⊢ query ⇓ QueryResult(rows) -``` +.... -### 4.2 Linear Connection Runtime +==== 4.2 Linear Connection Runtime -``` +.... handle = open_connection(db_url) remaining = n ──────────────────────────────────────────────────── [LinConn-Open] Γ, D ⊢ openConn(n) ⇓ LinConn(handle, n) @@ -159,11 +160,11 @@ v ∈ Value ::= close(handle) ──────────────────────────────────────── [LinConn-Close] Γ, D ⊢ closeConn(conn) ⇓ () -``` +.... -### 4.3 Session State Machine Runtime +==== 4.3 Session State Machine Runtime -``` +.... s = Session Fresh auth_result = authenticate(credentials) ──────────────────────────────────────────────────── [Session-Auth] @@ -184,21 +185,21 @@ v ∈ Value ::= ──────────────────────────────────────────────────── [Session-Commit] Γ, D ⊢ commit(s) ⇓ Right(Session Committed) | Left(TxError) -``` +.... -### 4.4 Effect Checking Runtime +==== 4.4 Effect Checking Runtime -``` +.... query_plan = plan(q) actual = collect_effects(query_plan) actual ⊆ declared (verified at compile time by Idris2) ──────────────────────────────────────────────────────────── [Effects-Run] Γ, D ⊢ q EFFECTS { declared } ⇓ execute(query_plan) -``` +.... -### 4.5 Modal Scoping Runtime +==== 4.5 Modal Scoping Runtime -``` +.... v computed in transaction scope w ──────────────────────────────────── [Modal-Wrap] Γ, D ⊢ MkBox(v) ⇓ Box(w, v) @@ -206,11 +207,11 @@ v ∈ Value ::= b = Box(w, v) current_scope = w (scope matches) ──────────────────────────────────────────────────────── [Modal-Open] Γ, D ⊢ extract(b) ⇓ v -``` +.... -### 4.6 Proof Verification Runtime +==== 4.6 Proof Verification Runtime -``` +.... result = execute(q) proof = verify_theorem(thm, result) proof succeeds @@ -220,26 +221,26 @@ v ∈ Value ::= proof fails ───────────────────────────────────────────────── [Proof-Fail] Γ, D ⊢ q PROOF ATTACHED thm ⇓ ⊥("theorem verification failed") -``` +.... -### 4.7 Resource Budget Runtime +==== 4.7 Resource Budget Runtime -``` +.... r = BoundedResource(v, S(k)) ──────────────────────────────────────────────────── [Resource-Use] Γ, D ⊢ consume(r) ⇓ (v, BoundedResource(v, k)) budget_remaining = 0 (enforced at compile time; never reached at runtime) -``` +.... ---- +''''' -## 5. Extension Composition +=== 5. Extension Composition -The six extensions compose independently because each operates on a different -dimension of the type: +The six extensions compose independently because each operates on a +different dimension of the type: -``` +.... Γ ⊢ q : QueryResult Γ ⊢ q CONSUME AFTER 1 USE (LinConn dimension) Γ ⊢ q WITH SESSION ReadOnly (Session dimension) @@ -250,20 +251,29 @@ dimension of the type: ────────────────────────────────────────────────────────────── [Compose] Γ ⊢ composed_query : ProvedResult (Box Committed QueryResult) IntegrityThm with linear connection, session protocol, effect bounds, and resource limit -``` - -The `Checker.idr` module validates all six constraints simultaneously by -composing individual check functions. - ---- - -## 6. Invariants - -1. **Linear safety:** A `LinConn n` is used exactly `n` times before closing. Enforced by QTT at compile time. -2. **Protocol compliance:** Session operations only succeed in valid states. Enforced by indexed types. -3. **Effect containment:** Actual effects ⊆ declared effects. Enforced by `Subsumes` proof. -4. **Scope isolation:** Data in `Box w₁` cannot be extracted without `InScope w₁` evidence. -5. **Proof integrity:** `ProvedResult` pairs are unforgeable — the proof must type-check. -6. **Budget monotonicity:** `BoundedResource n` can only decrease to `BoundedResource (n-1)`. -7. **Totality:** All Idris2 modules compile with `%default total` — no infinite loops, no partial functions. -8. **Zero axioms:** No `believe_me`, `assert_total`, or `assert_smaller` in proof code. +.... + +The `+Checker.idr+` module validates all six constraints simultaneously +by composing individual check functions. + +''''' + +=== 6. Invariants + +[arabic] +. *Linear safety:* A `+LinConn n+` is used exactly `+n+` times before +closing. Enforced by QTT at compile time. +. *Protocol compliance:* Session operations only succeed in valid +states. Enforced by indexed types. +. *Effect containment:* Actual effects ⊆ declared effects. Enforced by +`+Subsumes+` proof. +. *Scope isolation:* Data in `+Box w₁+` cannot be extracted without +`+InScope w₁+` evidence. +. *Proof integrity:* `+ProvedResult+` pairs are unforgeable — the proof +must type-check. +. *Budget monotonicity:* `+BoundedResource n+` can only decrease to +`+BoundedResource (n-1)+`. +. *Totality:* All Idris2 modules compile with `+%default total+` — no +infinite loops, no partial functions. +. *Zero axioms:* No `+believe_me+`, `+assert_total+`, or +`+assert_smaller+` in proof code. diff --git a/typeql-experimental/spec/system-specs.md b/typeql-experimental/spec/system-specs.adoc similarity index 52% rename from typeql-experimental/spec/system-specs.md rename to typeql-experimental/spec/system-specs.adoc index 645a2d5a..5117c8b4 100644 --- a/typeql-experimental/spec/system-specs.md +++ b/typeql-experimental/spec/system-specs.adoc @@ -1,120 +1,122 @@ -# SPDX-License-Identifier: CC-BY-SA-4.0 -# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +== SPDX-License-Identifier: CC-BY-SA-4.0 -# TypeQL-Experimental System Specification +== Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) j.d.a.jewell@open.ac.uk -## Overview +== TypeQL-Experimental System Specification + +=== Overview TypeQL-Experimental is a research-stage type-theoretic query language that enforces resource safety, session protocols, and proof obligations at compile time. The stack comprises Idris2 (type kernel and effect enforcement), ReScript (parser), and Zig (FFI bridge). -## Memory Model +=== Memory Model -### Idris2 Type Kernel +==== Idris2 Type Kernel -Through Quantitative Type Theory (QTT), types with quantity `0` are +Through Quantitative Type Theory (QTT), types with quantity `+0+` are erased at compile time and occupy no runtime memory. Proof terms exist -only during type checking. Runtime values use Idris2's reference-counted +only during type checking. Runtime values use Idris2’s reference-counted backend (Chez Scheme or RefC). The kernel is invoked as a compile-time tool, so memory pressure is bounded by program size. -### ReScript Parser +==== ReScript Parser The parser runs on the JS heap (Deno runtime). Source text is tokenized into an immutable AST (ReScript variant types), serialized to JSON for handoff to Idris2. Parser memory is short-lived: each invocation allocates, serializes, and releases. No persistent state between calls. -### Zig FFI Bridge +==== Zig FFI Bridge The bridge uses per-invocation arena allocators, freed in bulk on call completion. This eliminates fragmentation and ensures deterministic cleanup. Linear types in Idris2 guarantee that connection handles crossing the bridge are consumed exactly once. -### Linear Resource Guarantee +==== Linear Resource Guarantee Connection handles, file descriptors, and transaction tokens are typed -as `Linear a` (quantity `1`). The type checker verifies each linear +as `+Linear a+` (quantity `+1+`). The type checker verifies each linear resource is used exactly once. The Zig bridge asserts linearity at runtime via one-shot flags as defense-in-depth. -## Concurrency Model +=== Concurrency Model TypeQL-Experimental is a compile-time research tool, not a runtime engine. There is no runtime concurrency model. The Idris2 checker is single-threaded, the ReScript parser synchronous, and the Zig bridge processes one invocation at a time. Build-time parallelism is delegated -to `idris2 --threads` and `build.zig` parallel compilation. +to `+idris2 --threads+` and `+build.zig+` parallel compilation. -## Effect System +=== Effect System Six typed effects, all enforced at compile time by Idris2 QTT. -### 1. Linear Consumption +==== 1. Linear Consumption -Resources at quantity `1` must be consumed exactly once. Covers database -connections, prepared statements, and result cursors. No resource leaks -or double-frees are expressible in well-typed programs. +Resources at quantity `+1+` must be consumed exactly once. Covers +database connections, prepared statements, and result cursors. No +resource leaks or double-frees are expressible in well-typed programs. -### 2. Session Protocol +==== 2. Session Protocol Client-server interaction follows a session type (Idris2 indexed type) specifying the legal operation sequence: connect, authenticate, query, commit/rollback, disconnect. Deviating from the protocol is a type error. Parameterized by authentication state. -### 3. Effect Subsumption +==== 3. Effect Subsumption Effects form a lattice. Computations requiring fewer effects embed into contexts permitting more (covariant). Pure computations compose into effectful contexts without annotation. Lattice ordering checked during elaboration. -### 4. Modal Scoping +==== 4. Modal Scoping -Computations carry a modality: `Compile` or `Runtime`. Compile-time -proofs cannot reference runtime values. Erased terms (quantity `0`) are -never demanded at runtime. +Computations carry a modality: `+Compile+` or `+Runtime+`. Compile-time +proofs cannot reference runtime values. Erased terms (quantity `+0+`) +are never demanded at runtime. -### 5. Proof Attachment +==== 5. Proof Attachment -Query results carry proof witnesses (e.g., `NoInjection`) of statically -verified properties. Proofs are erased at runtime (quantity `0`) but -available during type checking for downstream composition. +Query results carry proof witnesses (e.g., `+NoInjection+`) of +statically verified properties. Proofs are erased at runtime (quantity +`+0+`) but available during type checking for downstream composition. -### 6. Resource Budgeting +==== 6. Resource Budgeting Effectful computations declare resource budgets (max allocations, max recursion depth). Checked statically via dependent types on naturals; enforced dynamically for data-dependent bounds. Violations produce a -`BudgetExceeded` type-level error requiring explicit handling. +`+BudgetExceeded+` type-level error requiring explicit handling. -## Module System +=== Module System -### Idris2 Packages +==== Idris2 Packages -Organized as `.ipkg` packages: `typeql-kernel` (type rules), -`typeql-effects` (effect lattice), `typeql-session` (session protocol), -`typeql-proofs` (proof combinators). Dependencies declared in `depends`. +Organized as `+.ipkg+` packages: `+typeql-kernel+` (type rules), +`+typeql-effects+` (effect lattice), `+typeql-session+` (session +protocol), `+typeql-proofs+` (proof combinators). Dependencies declared +in `+depends+`. -### ReScript Modules +==== ReScript Modules -`Lexer.res` (tokenization), `Parser.res` (recursive descent), `Ast.res` -(types), `Serializer.res` (AST to JSON). Interface files (`.resi`) -define public APIs. +`+Lexer.res+` (tokenization), `+Parser.res+` (recursive descent), +`+Ast.res+` (types), `+Serializer.res+` (AST to JSON). Interface files +(`+.resi+`) define public APIs. -### Zig Build System +==== Zig Build System -Built with `build.zig`: `bridge.zig` (entry points), `arena.zig` -(allocator), `protocol.zig` (serialization), `linear_check.zig` +Built with `+build.zig+`: `+bridge.zig+` (entry points), `+arena.zig+` +(allocator), `+protocol.zig+` (serialization), `+linear_check.zig+` (runtime linearity). Produces a shared library consumed by Idris2 -(`%foreign`) and ReScript (Deno FFI). +(`+%foreign+`) and ReScript (Deno FFI). -### Cross-Language Integration +==== Cross-Language Integration -Idris2 calls Zig via `%foreign "C:function_name,libbridge"`. ReScript -calls Zig via `Deno.dlopen`. The shared library exposes a flat C ABI +Idris2 calls Zig via `+%foreign "C:function_name,libbridge"+`. ReScript +calls Zig via `+Deno.dlopen+`. The shared library exposes a flat C ABI with no global state; all functions take explicit context pointers. diff --git a/verisim-modular-experiment/PROOF-NEEDS.adoc b/verisim-modular-experiment/PROOF-NEEDS.adoc new file mode 100644 index 00000000..3a5ac01d --- /dev/null +++ b/verisim-modular-experiment/PROOF-NEEDS.adoc @@ -0,0 +1,90 @@ +== Proof Needs — verisim-modular-experiment + +=== Central obligation + +*Claim:* There exists a subset `+Core ⊆ Octad+` and a federation +contract `+F+` such that, for every federation +`+S = Core ⊎ {external shapes honouring F}+`, VCL’s consonance +judgements on `+S+` are sound — i.e. no weaker than on `+Core+` alone, +and equivalent to the full octad for claims that stay within shapes +present in `+S+`. + +*Or the negation:* No such `+Core+` and `+F+` exist, and the octad is +indivisible w.r.t. VCL’s consonance guarantees. + +Either resolution is acceptable. The experiment succeeds by _deciding_ +which holds. + +=== Subordinate obligations + +[arabic] +. *Core closure.* Consonance claims purely over `+Core+` are verifiable +without appeal to federated shapes. +. *Federation soundness.* If external shape `+E+` honours contract +`+F+`, then VCL claims crossing the `+Core+`/`+E+` boundary are sound +relative to `+E+`’s externally-verified invariants. +. *Degradation honesty.* For every shape omitted from a federation, the +guarantees weakened by that omission are enumerated and documented. +. *Non-interference.* Federating shape `+E1+` does not silently weaken +claims about shape `+E2+` or about `+Core+`. + +=== Proof stack (intended) + +* Idris2 for the federation contract ABI (per hyperpolymath standard) +* VCL’s existing proof apparatus for consonance claims +* Zig FFI at the external-shape boundary + +=== Status (updated 2026-04-05) + +*Central obligation — positive direction:* runtime-discharged for the +minimal case. Core = \{Semantic, Temporal, Provenance} + one Federable +peer (Vector) honouring all 5 contract clauses gives aggregate-drift +numerically equal to the monolithic full-octad computation on the same +data (24/24 parity assertions). + +*Subordinate obligation 1 (Core closure):* partially discharged. +VerisimCore smoke tests (25/25) show that Core-only operation — +enrichment, attestation, verification, Identity Persistence — is sound +without any federated shapes. Consonance claims over Core-only shapes +(i.e. not crossing boundaries) are verifiable. + +*Subordinate obligation 2 (Federation soundness):* runtime-discharged +for single-peer case. Federated drift equals monolithic drift. See +`+docs/SEAMS.adoc+` for the ABI↔impl alignment that this rests on. + +*Subordinate obligation 3 (Degradation honesty):* structurally +satisfied. Two independent soundness routes documented: (a) Clause 1 +renormalisation → threshold-preserving reduction. (b) Absent-pair +convention `+d(⊥,·)=0+` → vacuous-drift reduction. Both tested and +green. + +*Subordinate obligation 4 (Non-interference):* NOT YET DISCHARGED. Phase +3 tests only one Federable peer. Multi-peer non-interference requires ≥2 +registered peers + a scenario where federating one shape could (in +principle) weaken claims about the other. Scheduled as next Phase 3 +follow-up. + +=== Remaining obligations + +* [x] Non-interference with N ≥ 2 simultaneous Federable peers. +*DISCHARGED runtime:* `+test_noninterference.jl+` (15 assertions) with +Vector + Document peers. Independent keypairs, isolated LWW writes, +3-way parity over (S,V)/(S,D)/(V,D). +* [x] Byzantine-peer resistance baseline — real Ed25519 via libsodium. +`+test_seams.jl+` round-trip + tamper rejection. +* [ ] Formal (Idris2 type-level) proof of non-interference at arbitrary +N. Discharged at runtime only. +* [ ] Byzantine-peer resistance beyond Clause 3 (e.g., peers that accept +LWW order but serve stale reads). +* [ ] Conditional-shape gating (Graph): runtime check that Graph is +registered only when cross-entity-claim workload is in scope. + +=== Phase 4 + 5 closure + +* [x] *Phase 4 dogfood:* `+test_krladapter_integration.jl+` (19 +assertions). KRLAdapter.jl client fully satisfied by Core alone — no +Federable shapes required. See `+examples/krladapter_integration.jl+` + +`+docs/FINDINGS.adoc+`. +* [x] *Phase 5 findings writeup:* `+docs/FINDINGS.adoc+` with +classification, contract, degradation routes, adoption guide, foldback +log, and productisation recommendation. diff --git a/verisim-modular-experiment/PROOF-NEEDS.md b/verisim-modular-experiment/PROOF-NEEDS.md deleted file mode 100644 index 5a36e1c2..00000000 --- a/verisim-modular-experiment/PROOF-NEEDS.md +++ /dev/null @@ -1,92 +0,0 @@ - -# Proof Needs — verisim-modular-experiment - -## Central obligation - -**Claim:** There exists a subset `Core ⊆ Octad` and a federation contract -`F` such that, for every federation `S = Core ⊎ {external shapes honouring F}`, -VCL's consonance judgements on `S` are sound — i.e. no weaker than on -`Core` alone, and equivalent to the full octad for claims that stay within -shapes present in `S`. - -**Or the negation:** No such `Core` and `F` exist, and the octad is -indivisible w.r.t. VCL's consonance guarantees. - -Either resolution is acceptable. The experiment succeeds by *deciding* -which holds. - -## Subordinate obligations - -1. **Core closure.** Consonance claims purely over `Core` are verifiable - without appeal to federated shapes. - -2. **Federation soundness.** If external shape `E` honours contract `F`, - then VCL claims crossing the `Core`/`E` boundary are sound relative to - `E`'s externally-verified invariants. - -3. **Degradation honesty.** For every shape omitted from a federation, the - guarantees weakened by that omission are enumerated and documented. - -4. **Non-interference.** Federating shape `E1` does not silently weaken - claims about shape `E2` or about `Core`. - -## Proof stack (intended) - -- Idris2 for the federation contract ABI (per hyperpolymath standard) -- VCL's existing proof apparatus for consonance claims -- Zig FFI at the external-shape boundary - -## Status (updated 2026-04-05) - -**Central obligation — positive direction:** runtime-discharged for the -minimal case. Core = {Semantic, Temporal, Provenance} + one Federable -peer (Vector) honouring all 5 contract clauses gives aggregate-drift -numerically equal to the monolithic full-octad computation on the same -data (24/24 parity assertions). - -**Subordinate obligation 1 (Core closure):** partially discharged. -VerisimCore smoke tests (25/25) show that Core-only operation — -enrichment, attestation, verification, Identity Persistence — is -sound without any federated shapes. Consonance claims over Core-only -shapes (i.e. not crossing boundaries) are verifiable. - -**Subordinate obligation 2 (Federation soundness):** runtime-discharged -for single-peer case. Federated drift equals monolithic drift. See -`docs/SEAMS.adoc` for the ABI↔impl alignment that this rests on. - -**Subordinate obligation 3 (Degradation honesty):** structurally satisfied. -Two independent soundness routes documented: - (a) Clause 1 renormalisation → threshold-preserving reduction. - (b) Absent-pair convention `d(⊥,·)=0` → vacuous-drift reduction. -Both tested and green. - -**Subordinate obligation 4 (Non-interference):** NOT YET DISCHARGED. -Phase 3 tests only one Federable peer. Multi-peer non-interference -requires ≥2 registered peers + a scenario where federating one shape -could (in principle) weaken claims about the other. Scheduled as -next Phase 3 follow-up. - -## Remaining obligations - -- [x] Non-interference with N ≥ 2 simultaneous Federable peers. - **DISCHARGED runtime:** `test_noninterference.jl` (15 assertions) - with Vector + Document peers. Independent keypairs, isolated LWW - writes, 3-way parity over (S,V)/(S,D)/(V,D). -- [x] Byzantine-peer resistance baseline — real Ed25519 via libsodium. - `test_seams.jl` round-trip + tamper rejection. -- [ ] Formal (Idris2 type-level) proof of non-interference at arbitrary N. - Discharged at runtime only. -- [ ] Byzantine-peer resistance beyond Clause 3 (e.g., peers that accept - LWW order but serve stale reads). -- [ ] Conditional-shape gating (Graph): runtime check that Graph is - registered only when cross-entity-claim workload is in scope. - -## Phase 4 + 5 closure - -- [x] **Phase 4 dogfood:** `test_krladapter_integration.jl` (19 assertions). - KRLAdapter.jl client fully satisfied by Core alone — no Federable - shapes required. See `examples/krladapter_integration.jl` + - `docs/FINDINGS.adoc`. -- [x] **Phase 5 findings writeup:** `docs/FINDINGS.adoc` with - classification, contract, degradation routes, adoption guide, - foldback log, and productisation recommendation.