diff --git a/ARCHITECTURE.adoc b/ARCHITECTURE.adoc new file mode 100644 index 0000000..1c0a7a6 --- /dev/null +++ b/ARCHITECTURE.adoc @@ -0,0 +1,48 @@ +== Architecture + +=== Overview + +This repository follows a modular, maintainable architecture designed +for clarity, scalability, and long-term sustainability. + +=== Directory Structure + +.... +. +├── src/ # Source code +├── tests/ # Test suites +├── docs/ # Documentation +├── scripts/ # Utility scripts +├── config/ # Configuration files +├── LICENSE # License file +├── LICENSES/ # Full license texts +└── README.adoc # Project documentation +.... + +=== Design Principles + +* *Separation of Concerns*: Each module has a single responsibility +* *Testability*: Code is written to be easily testable +* *Documentation*: All public APIs are documented +* *Configuration*: Environment-specific settings are externalized + +=== Dependencies + +* External dependencies are minimized and clearly declared +* Version pinning is used for reproducibility + +=== Security Considerations + +* Sensitive data is never committed to the repository +* Secrets are managed through environment variables or secure vaults +* Regular dependency audits are performed + +=== Maintainability + +* Code follows consistent style guidelines +* Pull requests require review and CI checks +* Issues and discussions are tracked transparently + +''''' + +_Last updated: 2026-07-18_ diff --git a/ARCHITECTURE.md b/ARCHITECTURE.md deleted file mode 100644 index 607e3d8..0000000 --- a/ARCHITECTURE.md +++ /dev/null @@ -1,47 +0,0 @@ -# Architecture - -## Overview - -This repository follows a modular, maintainable architecture designed for clarity, scalability, and long-term sustainability. - -## Directory Structure - -``` -. -├── src/ # Source code -├── tests/ # Test suites -├── docs/ # Documentation -├── scripts/ # Utility scripts -├── config/ # Configuration files -├── LICENSE # License file -├── LICENSES/ # Full license texts -└── README.adoc # Project documentation -``` - -## Design Principles - -- **Separation of Concerns**: Each module has a single responsibility -- **Testability**: Code is written to be easily testable -- **Documentation**: All public APIs are documented -- **Configuration**: Environment-specific settings are externalized - -## Dependencies - -- External dependencies are minimized and clearly declared -- Version pinning is used for reproducibility - -## Security Considerations - -- Sensitive data is never committed to the repository -- Secrets are managed through environment variables or secure vaults -- Regular dependency audits are performed - -## Maintainability - -- Code follows consistent style guidelines -- Pull requests require review and CI checks -- Issues and discussions are tracked transparently - ---- - -*Last updated: 2026-07-18* diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc new file mode 100644 index 0000000..f5cf878 --- /dev/null +++ b/CHANGELOG.adoc @@ -0,0 +1,58 @@ +== Changelog + +All notable changes to `+modshells+` will be documented in this file. + +This file is generated from conventional commits by the +https://github.com/hyperpolymath/standards/blob/main/.github/workflows/changelog-reusable.yml[`+changelog-reusable.yml+`] +workflow (`+hyperpolymath/standards#206+`). Adopt the workflow in this +repo’s CI to keep this file in sync automatically — see +https://github.com/hyperpolymath/standards/blob/main/templates/cliff.toml[`+templates/cliff.toml+`] +for the canonical config. + +The format follows https://keepachangelog.com/en/1.1.0/[Keep a +Changelog]; this project aims to follow +https://semver.org/spec/v2.0.0.html[Semantic Versioning]. + +=== [Unreleased] + +==== Added + +* feat(validator): add comprehensive shell validation package +* feat: Switch mirror workflow to SSH +* feat(init): Rhodium Standard project structure (v0.0) with Ada, LMDB +stubs, and GitLab CI. + +==== Fixed + +* fix(ci): sync hypatia-scan.yml to canonical (#46) +* fix(ci): point CodeQL at `+actions+` so SAST runs every commit (#72) +(#41) +* fix(ci): adopt canonical hypatia-scan.yml (#39) +* fix(security): update editorconfig SHA and CodeQL language +* fix: correct author name in CITATION.cff +* fix(ci): update quality.yml workflow +* fix: align CodeQL with repo languages (robot-cleaner) + +==== Changed + +* refactor: Rename project to '`modshells`' for conciseness and update +GNAT project file (Rhodium Standard). + +==== Documentation + +* docs(proof): modshells SPARK no-op exemption (reconcile stale audit) +(#49) + +==== CI + +* ci(spark): adopt estate SPARK Theatre Gate (#135) (#50) + +=== Pre-history + +Prior commits to this file’s introduction are recorded in git history +but not formally classified into Keep-a-Changelog sections. To backfill, +run `+git cliff -o CHANGELOG.md+` locally using the canonical +https://github.com/hyperpolymath/standards/blob/main/templates/cliff.toml[`+cliff.toml+`] +— this is one-shot mechanical work. + +''''' diff --git a/CHANGELOG.md b/CHANGELOG.md deleted file mode 100644 index 9018134..0000000 --- a/CHANGELOG.md +++ /dev/null @@ -1,54 +0,0 @@ - -# Changelog - -All notable changes to `modshells` will be documented in this file. - -This file is generated from conventional commits by the -[`changelog-reusable.yml`](https://github.com/hyperpolymath/standards/blob/main/.github/workflows/changelog-reusable.yml) -workflow (`hyperpolymath/standards#206`). Adopt the workflow in this repo's CI to keep this file in sync automatically — see -[`templates/cliff.toml`](https://github.com/hyperpolymath/standards/blob/main/templates/cliff.toml) -for the canonical config. - -The format follows [Keep a Changelog](https://keepachangelog.com/en/1.1.0/); -this project aims to follow [Semantic Versioning](https://semver.org/spec/v2.0.0.html). - -## [Unreleased] - -### Added - -- feat(validator): add comprehensive shell validation package -- feat: Switch mirror workflow to SSH -- feat(init): Rhodium Standard project structure (v0.0) with Ada, LMDB stubs, and GitLab CI. - -### Fixed - -- fix(ci): sync hypatia-scan.yml to canonical (#46) -- fix(ci): point CodeQL at `actions` so SAST runs every commit (#72) (#41) -- fix(ci): adopt canonical hypatia-scan.yml (#39) -- fix(security): update editorconfig SHA and CodeQL language -- fix: correct author name in CITATION.cff -- fix(ci): update quality.yml workflow -- fix: align CodeQL with repo languages (robot-cleaner) - -### Changed - -- refactor: Rename project to 'modshells' for conciseness and update GNAT project file (Rhodium Standard). - -### Documentation - -- docs(proof): modshells SPARK no-op exemption (reconcile stale audit) (#49) - -### CI - -- ci(spark): adopt estate SPARK Theatre Gate (#135) (#50) - -## Pre-history - -Prior commits to this file's introduction are recorded in git history but not formally classified into Keep-a-Changelog sections. To backfill, run `git cliff -o CHANGELOG.md` locally using the canonical [`cliff.toml`](https://github.com/hyperpolymath/standards/blob/main/templates/cliff.toml) — this is one-shot mechanical work. - ---- - - diff --git a/CODE_OF_CONDUCT.adoc b/CODE_OF_CONDUCT.adoc new file mode 100644 index 0000000..a600393 --- /dev/null +++ b/CODE_OF_CONDUCT.adoc @@ -0,0 +1,39 @@ +== Contributor Covenant Code of Conduct + +=== Our Pledge + +We as members, contributors, and leaders pledge to make participation in +our community 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, religion, or sexual identity and orientation. + +=== Our Standards + +Examples of behavior that contributes to a positive environment include: + +* Demonstrating empathy and kindness toward other people +* Being respectful of differing opinions, viewpoints, and experiences +* Giving and gracefully accepting constructive feedback +* Accepting responsibility and apologizing to those affected by our +mistakes + +Examples of unacceptable behavior include: + +* The use of sexualized language or imagery +* Trolling, insulting or derogatory comments, and personal or political +attacks +* Public or private harassment +* Publishing others’ private information without explicit permission + +=== Enforcement + +Instances of abusive, harassing, or otherwise unacceptable behavior may +be reported to the project maintainers. All complaints will be reviewed +and investigated promptly and fairly. + +=== Attribution + +This Code of Conduct is adapted from the +https://www.contributor-covenant.org[Contributor Covenant], version 2.1. diff --git a/CODE_OF_CONDUCT.md b/CODE_OF_CONDUCT.md deleted file mode 100644 index b568190..0000000 --- a/CODE_OF_CONDUCT.md +++ /dev/null @@ -1,41 +0,0 @@ - -# Contributor Covenant Code of Conduct - -## Our Pledge - -We as members, contributors, and leaders pledge to make participation in our -community 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, religion, or sexual identity -and orientation. - -## Our Standards - -Examples of behavior that contributes to a positive environment include: - -* Demonstrating empathy and kindness toward other people -* Being respectful of differing opinions, viewpoints, and experiences -* Giving and gracefully accepting constructive feedback -* Accepting responsibility and apologizing to those affected by our mistakes - -Examples of unacceptable behavior include: - -* The use of sexualized language or imagery -* Trolling, insulting or derogatory comments, and personal or political attacks -* Public or private harassment -* Publishing others' private information without explicit permission - -## Enforcement - -Instances of abusive, harassing, or otherwise unacceptable behavior may be -reported to the project maintainers. All complaints will be reviewed and -investigated promptly and fairly. - -## Attribution - -This Code of Conduct is adapted from the [Contributor Covenant](https://www.contributor-covenant.org), version 2.1. - diff --git a/CONTRIBUTING.adoc b/CONTRIBUTING.adoc index e9b1993..16f545b 100644 --- a/CONTRIBUTING.adoc +++ b/CONTRIBUTING.adoc @@ -1,21 +1,109 @@ -// SPDX-License-Identifier: CC-BY-SA-4.0 -// Copyright (c) Jonathan D.A. Jewell -= Contributing Guide +== Clone the repository -== Getting Started +git clone https://github.com/hyperpolymath/squisher-corpus.git cd +squisher-corpus -1. Fork the repository -2. Create a feature branch from `main` -3. Sign off commits (`git commit -s`) -4. Submit a pull request +== Using Nix (recommended for reproducibility) -== Commit Guidelines +nix develop -* Conventional commits: `type(scope): description` -* Sign all commits (DCO required) -* Atomic, focused commits +== Or using toolbox/distrobox -== License +toolbox create squisher-corpus-dev toolbox enter squisher-corpus-dev # +Install dependencies manually -Contributions licensed under project license. +== Verify setup +just check # or: cargo check / mix compile / etc. just test # Run test +suite + +.... + +### Repository Structure +.... + +squisher-corpus/ ├── src/ # Source code (Perimeter 1-2) ├── lib/ # +Library code (Perimeter 1-2) ├── extensions/ # Extensions (Perimeter 2) +├── plugins/ # Plugins (Perimeter 2) ├── tools/ # Tooling (Perimeter 2) +├── docs/ # Documentation (Perimeter 3) │ ├── architecture/ # ADRs, +specs (Perimeter 2) │ └── proposals/ # RFCs (Perimeter 3) ├── examples/ +# Examples (Perimeter 3) ├── spec/ # Spec tests (Perimeter 3) ├── tests/ +# Test suite (Perimeter 2-3) ├── .well-known/ # Protocol files +(Perimeter 1-3) ├── .github/ # GitHub config (Perimeter 1) │ ├── +ISSUE_TEMPLATE/ │ └── workflows/ ├── CHANGELOG.md ├── CODE_OF_CONDUCT.md +├── CONTRIBUTING.md # This file ├── GOVERNANCE.md ├── LICENSE ├── +MAINTAINERS.md ├── README.adoc ├── SECURITY.md ├── flake.nix # Nix flake +(Perimeter 1) └── Justfile # Task runner (Perimeter 1) + +.... + +--- + +## How to Contribute + +### Reporting Bugs + +**Before reporting**: +1. Search existing issues +2. Check if it's already fixed in `main` +3. Determine which perimeter the bug affects + +**When reporting**: + +Use the [bug report template](.github/ISSUE_TEMPLATE/bug_report.md) and include: + +- Clear, descriptive title +- Environment details (OS, versions, toolchain) +- Steps to reproduce +- Expected vs actual behaviour +- Logs, screenshots, or minimal reproduction + +### Suggesting Features + +**Before suggesting**: +1. Check the [roadmap](ROADMAP.md) if available +2. Search existing issues and discussions +3. Consider which perimeter the feature belongs to + +**When suggesting**: + +Use the [feature request template](.github/ISSUE_TEMPLATE/feature_request.md) and include: + +- Problem statement (what pain point does this solve?) +- Proposed solution +- Alternatives considered +- Which perimeter this affects + +### Your First Contribution + +Look for issues labelled: + +- [`good first issue`](https://github.com/hyperpolymath/squisher-corpus/labels/good%20first%20issue) — Simple Perimeter 3 tasks +- [`help wanted`](https://github.com/hyperpolymath/squisher-corpus/labels/help%20wanted) — Community help needed +- [`documentation`](https://github.com/hyperpolymath/squisher-corpus/labels/documentation) — Docs improvements +- [`perimeter-3`](https://github.com/hyperpolymath/squisher-corpus/labels/perimeter-3) — Community sandbox scope + +--- + +## Development Workflow + +### Branch Naming +.... + +docs/short-description # Documentation (P3) test/what-added # Test +additions (P3) feat/short-description # New features (P2) +fix/issue-number-description # Bug fixes (P2) refactor/what-changed # +Code improvements (P2) security/what-fixed # Security fixes (P1-2) + +.... + +### Commit Messages + +We follow [Conventional Commits](https://www.conventionalcommits.org/): +.... + +(): + +{empty}[optional body] + +{empty}[optional footer] diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md deleted file mode 100644 index 594b265..0000000 --- a/CONTRIBUTING.md +++ /dev/null @@ -1,116 +0,0 @@ -# Clone the repository -git clone https://github.com/hyperpolymath/squisher-corpus.git -cd squisher-corpus - -# Using Nix (recommended for reproducibility) -nix develop - -# Or using toolbox/distrobox -toolbox create squisher-corpus-dev -toolbox enter squisher-corpus-dev -# Install dependencies manually - -# Verify setup -just check # or: cargo check / mix compile / etc. -just test # Run test suite -``` - -### Repository Structure -``` -squisher-corpus/ -├── src/ # Source code (Perimeter 1-2) -├── lib/ # Library code (Perimeter 1-2) -├── extensions/ # Extensions (Perimeter 2) -├── plugins/ # Plugins (Perimeter 2) -├── tools/ # Tooling (Perimeter 2) -├── docs/ # Documentation (Perimeter 3) -│ ├── architecture/ # ADRs, specs (Perimeter 2) -│ └── proposals/ # RFCs (Perimeter 3) -├── examples/ # Examples (Perimeter 3) -├── spec/ # Spec tests (Perimeter 3) -├── tests/ # Test suite (Perimeter 2-3) -├── .well-known/ # Protocol files (Perimeter 1-3) -├── .github/ # GitHub config (Perimeter 1) -│ ├── ISSUE_TEMPLATE/ -│ └── workflows/ -├── CHANGELOG.md -├── CODE_OF_CONDUCT.md -├── CONTRIBUTING.md # This file -├── GOVERNANCE.md -├── LICENSE -├── MAINTAINERS.md -├── README.adoc -├── SECURITY.md -├── flake.nix # Nix flake (Perimeter 1) -└── Justfile # Task runner (Perimeter 1) -``` - ---- - -## How to Contribute - -### Reporting Bugs - -**Before reporting**: -1. Search existing issues -2. Check if it's already fixed in `main` -3. Determine which perimeter the bug affects - -**When reporting**: - -Use the [bug report template](.github/ISSUE_TEMPLATE/bug_report.md) and include: - -- Clear, descriptive title -- Environment details (OS, versions, toolchain) -- Steps to reproduce -- Expected vs actual behaviour -- Logs, screenshots, or minimal reproduction - -### Suggesting Features - -**Before suggesting**: -1. Check the [roadmap](ROADMAP.md) if available -2. Search existing issues and discussions -3. Consider which perimeter the feature belongs to - -**When suggesting**: - -Use the [feature request template](.github/ISSUE_TEMPLATE/feature_request.md) and include: - -- Problem statement (what pain point does this solve?) -- Proposed solution -- Alternatives considered -- Which perimeter this affects - -### Your First Contribution - -Look for issues labelled: - -- [`good first issue`](https://github.com/hyperpolymath/squisher-corpus/labels/good%20first%20issue) — Simple Perimeter 3 tasks -- [`help wanted`](https://github.com/hyperpolymath/squisher-corpus/labels/help%20wanted) — Community help needed -- [`documentation`](https://github.com/hyperpolymath/squisher-corpus/labels/documentation) — Docs improvements -- [`perimeter-3`](https://github.com/hyperpolymath/squisher-corpus/labels/perimeter-3) — Community sandbox scope - ---- - -## Development Workflow - -### Branch Naming -``` -docs/short-description # Documentation (P3) -test/what-added # Test additions (P3) -feat/short-description # New features (P2) -fix/issue-number-description # Bug fixes (P2) -refactor/what-changed # Code improvements (P2) -security/what-fixed # Security fixes (P1-2) -``` - -### Commit Messages - -We follow [Conventional Commits](https://www.conventionalcommits.org/): -``` -(): - -[optional body] - -[optional footer] diff --git a/GOVERNANCE.adoc b/GOVERNANCE.adoc new file mode 100644 index 0000000..9b836fb --- /dev/null +++ b/GOVERNANCE.adoc @@ -0,0 +1,60 @@ +== Governance + +=== Overview + +This project is governed by the following principles and structures to +ensure transparent, inclusive, and effective decision-making. + +=== Roles and Responsibilities + +==== Maintainers + +Maintainers are responsible for: - Reviewing and merging pull requests - +Managing releases and versioning - Ensuring code quality and standards - +Triaging issues and bug reports - Community engagement and support + +==== Contributors + +Contributors are expected to: - Follow the code of conduct - Submit +well-documented pull requests - Write tests for new functionality - +Maintain existing tests - Update documentation as needed + +=== Decision Making + +==== Minor Changes + +* Can be made by any maintainer +* Include bug fixes, documentation updates, dependency updates + +==== Major Changes + +* Require discussion in issues or pull requests +* Include new features, architectural changes, API changes +* Need approval from at least 2 maintainers + +==== Breaking Changes + +* Require RFC (Request for Comments) process +* Need approval from majority of maintainers +* Must include migration guide + +=== Code of Conduct + +All participants are expected to follow our Code of Conduct. Violations +can be reported to the maintainers. + +=== Communication + +* *Issues*: For bug reports and feature requests +* *Discussions*: For questions and general discussion +* *Pull Requests*: For code contributions + +=== Licensing + +All contributions are made under the terms of the repository’s LICENSE +file. By submitting a pull request, you agree to license your +contributions accordingly. + +''''' + +_Last updated: 2026-07-18_ diff --git a/GOVERNANCE.md b/GOVERNANCE.md deleted file mode 100644 index e27364c..0000000 --- a/GOVERNANCE.md +++ /dev/null @@ -1,60 +0,0 @@ -# Governance - -## Overview - -This project is governed by the following principles and structures to ensure transparent, inclusive, and effective decision-making. - -## Roles and Responsibilities - -### Maintainers - -Maintainers are responsible for: -- Reviewing and merging pull requests -- Managing releases and versioning -- Ensuring code quality and standards -- Triaging issues and bug reports -- Community engagement and support - -### Contributors - -Contributors are expected to: -- Follow the code of conduct -- Submit well-documented pull requests -- Write tests for new functionality -- Maintain existing tests -- Update documentation as needed - -## Decision Making - -### Minor Changes -- Can be made by any maintainer -- Include bug fixes, documentation updates, dependency updates - -### Major Changes -- Require discussion in issues or pull requests -- Include new features, architectural changes, API changes -- Need approval from at least 2 maintainers - -### Breaking Changes -- Require RFC (Request for Comments) process -- Need approval from majority of maintainers -- Must include migration guide - -## Code of Conduct - -All participants are expected to follow our Code of Conduct. Violations can be reported to the maintainers. - -## Communication - -- **Issues**: For bug reports and feature requests -- **Discussions**: For questions and general discussion -- **Pull Requests**: For code contributions - -## Licensing - -All contributions are made under the terms of the repository's LICENSE file. -By submitting a pull request, you agree to license your contributions accordingly. - ---- - -*Last updated: 2026-07-18* diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc new file mode 100644 index 0000000..1aa1b22 --- /dev/null +++ b/PROOF-NEEDS.adoc @@ -0,0 +1,48 @@ +== Proof Requirements + +=== Current state (reconciled 2026-05-19) + +The original 2026-05-18 audit entry claimed "`Rust only, no SPARK +present`". That was *stale*. Ground truth (direct census 2026-05-19): + +* Source is *Ada* (9 units: `+config_store+`, `+shell_validator+`, +`+shell_manager+`, `+modshells+` main, tests), *not* "`Rust only`". +* *Zero `+SPARK_Mode+` markers* anywhere. There is therefore *no SPARK +proof theatre to demote*, and nothing for the estate SPARK Theatre Gate +(hyperpolymath/standards#135) to flag — modshells passes it vacuously. +* A Rust/SPARK rewrite is in flight on branch +`+wip/rust-spark-migration+` (bounded consolidation into one verified +binary; tracked in the migration plan outside this repo). + +=== SPARK proof stance — DOCUMENTED NO-OP / EXEMPTION + +*No SPARK proof action is owed for modshells in the current audit +cycle.* This is an explicit, deliberate exemption, not unresolved drift: + +[arabic] +. The Ada units are _migration source_, scheduled for replacement by the +`+wip/rust-spark-migration+` Rust/SPARK consolidation. Adding SPARK +contracts to soon-to-be-deleted Ada would be wasted effort. +. Because there are zero `+SPARK_Mode+` markers, modshells makes *no +proof claim* — it cannot be "`SPARK theatre`" (theatre requires a hollow +claim). It is honest by absence. +. Estate audits and the SPARK Theatre Gate should treat modshells as +*resolved-by-exemption* and not re-triage it until the Rust/SPARK +migration lands, at which point the _Rust/SPARK_ tier (seam + stance) is +assessed against the new binary, not the Ada source. + +Re-open trigger: merge of `+wip/rust-spark-migration+` to `+main+` +(assess the Rust/SPARK seam then), or any new `+SPARK_Mode+` marker +appearing in the Ada source before then (would reintroduce theatre +risk). + +=== Recommended prover + +* *Idris2* if a contract surface is warranted post-migration; otherwise +N/A under the exemption above. + +=== Priority + +*RESOLVED-BY-EXEMPTION* (2026-05-19). Was LOW/policy-relevant; the +seam-or-exemption decision is now made: documented exemption pending the +`+wip/rust-spark-migration+` rewrite. No SPARK work owed this cycle. diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md deleted file mode 100644 index 0a1ccdd..0000000 --- a/PROOF-NEEDS.md +++ /dev/null @@ -1,52 +0,0 @@ - -# Proof Requirements - - - -## Current state (reconciled 2026-05-19) - -The original 2026-05-18 audit entry claimed "Rust only, no SPARK present". -That was **stale**. Ground truth (direct census 2026-05-19): - -- Source is **Ada** (9 units: `config_store`, `shell_validator`, - `shell_manager`, `modshells` main, tests), **not** "Rust only". -- **Zero `SPARK_Mode` markers** anywhere. There is therefore **no SPARK - proof theatre to demote**, and nothing for the estate SPARK Theatre Gate - (hyperpolymath/standards#135) to flag — modshells passes it vacuously. -- A Rust/SPARK rewrite is in flight on branch `wip/rust-spark-migration` - (bounded consolidation into one verified binary; tracked in the - migration plan outside this repo). - -## SPARK proof stance — DOCUMENTED NO-OP / EXEMPTION - -**No SPARK proof action is owed for modshells in the current audit cycle.** -This is an explicit, deliberate exemption, not unresolved drift: - -1. The Ada units are *migration source*, scheduled for replacement by the - `wip/rust-spark-migration` Rust/SPARK consolidation. Adding SPARK - contracts to soon-to-be-deleted Ada would be wasted effort. -2. Because there are zero `SPARK_Mode` markers, modshells makes **no proof - claim** — it cannot be "SPARK theatre" (theatre requires a hollow - claim). It is honest by absence. -3. Estate audits and the SPARK Theatre Gate should treat modshells as - **resolved-by-exemption** and not re-triage it until the Rust/SPARK - migration lands, at which point the *Rust/SPARK* tier (seam + stance) - is assessed against the new binary, not the Ada source. - -Re-open trigger: merge of `wip/rust-spark-migration` to `main` (assess the -Rust/SPARK seam then), or any new `SPARK_Mode` marker appearing in the Ada -source before then (would reintroduce theatre risk). - -## Recommended prover - -- **Idris2** if a contract surface is warranted post-migration; otherwise - N/A under the exemption above. - -## Priority - -**RESOLVED-BY-EXEMPTION** (2026-05-19). Was LOW/policy-relevant; the -seam-or-exemption decision is now made: documented exemption pending the -`wip/rust-spark-migration` rewrite. No SPARK work owed this cycle. diff --git a/SECURITY.adoc b/SECURITY.adoc new file mode 100644 index 0000000..abb6fbb --- /dev/null +++ b/SECURITY.adoc @@ -0,0 +1,24 @@ +== Security Policy + +=== Reporting a Vulnerability + +If you discover a security vulnerability, please report it responsibly: + +[arabic] +. *Do not* open a public issue +. Email security concerns to the maintainer +. Include steps to reproduce the vulnerability +. Allow reasonable time for a fix before disclosure + +=== Supported Versions + +[cols=",",options="header",] +|=== +|Version |Supported +|latest |:white_check_mark: +|< latest |Best effort +|=== + +=== Security Updates + +Security patches are released as soon as possible after verification. diff --git a/SECURITY.md b/SECURITY.md deleted file mode 100644 index 9c8c60d..0000000 --- a/SECURITY.md +++ /dev/null @@ -1,26 +0,0 @@ - -# Security Policy - -## Reporting a Vulnerability - -If you discover a security vulnerability, please report it responsibly: - -1. **Do not** open a public issue -2. Email security concerns to the maintainer -3. Include steps to reproduce the vulnerability -4. Allow reasonable time for a fix before disclosure - -## Supported Versions - -| Version | Supported | -| ------- | ------------------ | -| latest | :white_check_mark: | -| < latest| Best effort | - -## Security Updates - -Security patches are released as soon as possible after verification. - diff --git a/docs/tech-debt-2026-05-26.adoc b/docs/tech-debt-2026-05-26.adoc new file mode 100644 index 0000000..f66489b --- /dev/null +++ b/docs/tech-debt-2026-05-26.adoc @@ -0,0 +1,70 @@ +== Tech-Debt Audit — modshells — 2026-05-26 + +*Source:* estate-wide automated scan 2026-05-26. *Companion:* +https://github.com/hyperpolymath/standards/tree/main/docs/audits[`+hyperpolymath/standards+` +2026-05-26-estate-*-debt audits]. *Combined severity:* `+2026-05-22+`. + +This file records the _raw findings_ — it does not by itself fix the +debt. Each section ends with a '`Recommended next move`' line; closing +the debt is follow-up work. + +=== 1. Proof debt + +Scanner counted the following markers in proof-bearing files of this +repo: + +.... +files= 9 | Coq-Axm/Adm= 0 | Lean-srry/ax= 0 | Agda-pst= 0 | Idr-blv= 0 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0 +.... + +*Total markers:* 0. *Severity:* `+>00+`. + +*Recommended next move:* none — no proof-debt markers detected. + +=== 2. Licence debt + +[cols=",",options="header",] +|=== +|Field |Value +|LICENSE file |`+LICENSE+` +|SPDX header |`+MPL-2.0+` +|Manifest licence |`+NONE+` +|Body classifier |`+MPL-2.0-pure+` +|Severity |`+ok+` +|=== + +*Recommended next move:* none for licence. + +=== 3. Documentation debt + +[cols=",",options="header",] +|=== +|Field |Value +|README lines |449 +|`+docs/+` files |1 +|`+docs/+` LoC |36 +|CHANGELOG.md |N +|CONTRIBUTING.md |N +|CODE_OF_CONDUCT.md |Y +|SECURITY.md |Y +|Severity |`+readme=449 docs=1/36+` +|=== + +Additionally: *CHANGELOG.md is missing.* 65% of estate repos lack one — +adopting a CHANGELOG (or auto-generating via `+git-cliff+`) is a +recommended estate-wide follow-up. + +=== Cross-references + +* Estate proof-debt audit: +`+hyperpolymath/standards/docs/audits/2026-05-26-estate-proof-debt.md+` +* Estate licence-debt audit: +`+hyperpolymath/standards/docs/audits/2026-05-26-estate-licence-debt.md+` +* Estate documentation-debt audit: +`+hyperpolymath/standards/docs/audits/2026-05-26-estate-documentation-debt.md+` + +''''' + +🤖 Generated by Claude Code estate-wide tech-debt scan (2026-05-26). +This file is informational — closing the debt is follow-up work owned by +the maintainer. diff --git a/docs/tech-debt-2026-05-26.md b/docs/tech-debt-2026-05-26.md deleted file mode 100644 index 7976636..0000000 --- a/docs/tech-debt-2026-05-26.md +++ /dev/null @@ -1,61 +0,0 @@ - -# Tech-Debt Audit — modshells — 2026-05-26 - -**Source:** estate-wide automated scan 2026-05-26. -**Companion:** [`hyperpolymath/standards` 2026-05-26-estate-*-debt audits](https://github.com/hyperpolymath/standards/tree/main/docs/audits). -**Combined severity:** `2026-05-22`. - -This file records the *raw findings* — it does not by itself fix the debt. Each section ends with a 'Recommended next move' line; closing the debt is follow-up work. - -## 1. Proof debt - -Scanner counted the following markers in proof-bearing files of this repo: - -``` -files= 9 | Coq-Axm/Adm= 0 | Lean-srry/ax= 0 | Agda-pst= 0 | Idr-blv= 0 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0 -``` - -**Total markers:** 0. **Severity:** `>00`. - -**Recommended next move:** none — no proof-debt markers detected. - -## 2. Licence debt - -| Field | Value | -|---|---| -| LICENSE file | `LICENSE` | -| SPDX header | `MPL-2.0` | -| Manifest licence | `NONE` | -| Body classifier | `MPL-2.0-pure` | -| Severity | `ok` | - -**Recommended next move:** none for licence. - -## 3. Documentation debt - -| Field | Value | -|---|---| -| README lines | 449 | -| `docs/` files | 1 | -| `docs/` LoC | 36 | -| CHANGELOG.md | N | -| CONTRIBUTING.md | N | -| CODE_OF_CONDUCT.md | Y | -| SECURITY.md | Y | -| Severity | `readme=449 docs=1/36` | - - -Additionally: **CHANGELOG.md is missing.** 65% of estate repos lack one — adopting a CHANGELOG (or auto-generating via `git-cliff`) is a recommended estate-wide follow-up. - -## Cross-references - -- Estate proof-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-proof-debt.md` -- Estate licence-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-licence-debt.md` -- Estate documentation-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-documentation-debt.md` - ---- - -🤖 Generated by Claude Code estate-wide tech-debt scan (2026-05-26). This file is informational — closing the debt is follow-up work owned by the maintainer.