diff --git a/.claude/PROJECT.adoc b/.claude/PROJECT.adoc new file mode 100644 index 0000000..379e40d --- /dev/null +++ b/.claude/PROJECT.adoc @@ -0,0 +1,33 @@ +== Jaffascript - Claude Code Instructions + +This repository contains the Jaffascript project. + +=== Project Structure + +.... +jaffascript/ +├── .claude/ # AI assistant instructions +├── .git/ # Version control +├── .gitignore # Git ignore rules +├── .editorconfig # Editor configuration +└── ... # Project files +.... + +=== Build Commands + +Refer to project-specific documentation. + +=== Coding Conventions + +* Follow hyperpolymath standards +* All code must have SPDX license headers +* Use approved languages only (see CLAUDE.md) +* Document all non-obvious decisions + +=== Security + +* No hardcoded secrets +* All secrets through environment variables or secret management +* SHA-pinned dependencies where applicable +* HTTPS only, no HTTP URLs +* No MD5/SHA1 for security purposes diff --git a/.claude/PROJECT.md b/.claude/PROJECT.md deleted file mode 100644 index 839bbec..0000000 --- a/.claude/PROJECT.md +++ /dev/null @@ -1,37 +0,0 @@ - -# Jaffascript - Claude Code Instructions - -This repository contains the Jaffascript project. - -## Project Structure - -``` -jaffascript/ -├── .claude/ # AI assistant instructions -├── .git/ # Version control -├── .gitignore # Git ignore rules -├── .editorconfig # Editor configuration -└── ... # Project files -``` - -## Build Commands - -Refer to project-specific documentation. - -## Coding Conventions - -- Follow hyperpolymath standards -- All code must have SPDX license headers -- Use approved languages only (see CLAUDE.md) -- Document all non-obvious decisions - -## Security - -- No hardcoded secrets -- All secrets through environment variables or secret management -- SHA-pinned dependencies where applicable -- HTTPS only, no HTTP URLs -- No MD5/SHA1 for security purposes 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..0051cb5 --- /dev/null +++ b/CHANGELOG.adoc @@ -0,0 +1,4 @@ +== Changelog for jaffascript + +All changes are tracked in the main AffineScript repository. This is a +thin shim layer - no independent releases. diff --git a/CHANGELOG.md b/CHANGELOG.md deleted file mode 100644 index c2eb5ea..0000000 --- a/CHANGELOG.md +++ /dev/null @@ -1,4 +0,0 @@ -# Changelog for jaffascript - -All changes are tracked in the main AffineScript repository. -This is a thin shim layer - no independent releases. diff --git a/CODE_OF_CONDUCT.adoc b/CODE_OF_CONDUCT.adoc new file mode 100644 index 0000000..bd2a83c --- /dev/null +++ b/CODE_OF_CONDUCT.adoc @@ -0,0 +1,24 @@ +== Contributor Covenant Code of Conduct + +=== Our Pledge + +We pledge to make participation a harassment-free experience for +everyone. + +=== Our Standards + +*Positive behavior:* * Using welcoming language * Being respectful of +differing viewpoints * Accepting constructive criticism * Focusing on +what is best for the community + +*Unacceptable behavior:* * Harassment, trolling, or personal attacks * +Publishing private information without permission + +=== Enforcement + +Report issues to the maintainers. All complaints will be reviewed. + +=== Attribution + +Adapted from https://www.contributor-covenant.org/[Contributor Covenant] +v2.1. diff --git a/CODE_OF_CONDUCT.md b/CODE_OF_CONDUCT.md deleted file mode 100644 index 9020def..0000000 --- a/CODE_OF_CONDUCT.md +++ /dev/null @@ -1,30 +0,0 @@ - -# Contributor Covenant Code of Conduct - -## Our Pledge - -We pledge to make participation a harassment-free experience for everyone. - -## Our Standards - -**Positive behavior:** -* Using welcoming language -* Being respectful of differing viewpoints -* Accepting constructive criticism -* Focusing on what is best for the community - -**Unacceptable behavior:** -* Harassment, trolling, or personal attacks -* Publishing private information without permission - -## Enforcement - -Report issues to the maintainers. All complaints will be reviewed. - -## Attribution - -Adapted from [Contributor Covenant](https://www.contributor-covenant.org/) v2.1. - diff --git a/CONTRIBUTING.adoc b/CONTRIBUTING.adoc new file mode 100644 index 0000000..c236587 --- /dev/null +++ b/CONTRIBUTING.adoc @@ -0,0 +1,55 @@ +== Contributing to JaffaScript + +This is a *brand-surface repo*. The compiler, type checker, borrow +checker, codegen, and face transformer all live in +https://github.com/hyperpolymath/affinescript[affinescript]. + +=== Where to file what + +[width="100%",cols="50%,50%",options="header",] +|=== +|Issue |Repo +|The face transformer mangles my code +|https://github.com/hyperpolymath/affinescript/issues[affinescript] + +|The error message uses the wrong vocabulary for this face +|https://github.com/hyperpolymath/affinescript/issues[affinescript] — +the face vocabulary lives in `+lib/face.ml+` + +|New language feature needed (extern types, dependent types, etc.) +|https://github.com/hyperpolymath/affinescript/issues[affinescript] + +|Brand README is unclear / wrong |this repo + +|Example program doesn’t compile |this repo (and probably also +affinescript if it’s a transformer bug) + +|Tutorial / migration guide additions |this repo + +|Add this face to my IDE / build tool |this repo, but expect it to +depend on affinescript work first +|=== + +=== Local workflow + +[source,bash] +---- +opam install affinescript # installs the compiler +git clone https://github.com/hyperpolymath/jaffascript +cd jaffascript +just hello # smoke-test the example +just check examples/hello.affine +just preview examples/hello.affine +---- + +=== Pull requests + +* SPDX header on every new file (`+AGPL-3.0-or-later+`). +* Run `+just hello+` and any other examples added before opening the PR. +* If you’re touching the face transformer, open the PR against +https://github.com/hyperpolymath/affinescript[affinescript], not here. + +=== Code of conduct + +See `+CODE_OF_CONDUCT.md+` (TBD; for now follow the affinescript code of +conduct). diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md deleted file mode 100644 index c327198..0000000 --- a/CONTRIBUTING.md +++ /dev/null @@ -1,45 +0,0 @@ - - - -# Contributing to JaffaScript - -This is a **brand-surface repo**. The compiler, type checker, borrow checker, -codegen, and face transformer all live in -[affinescript](https://github.com/hyperpolymath/affinescript). - -## Where to file what - -| Issue | Repo | -|---|---| -| The face transformer mangles my code | [affinescript](https://github.com/hyperpolymath/affinescript/issues) | -| The error message uses the wrong vocabulary for this face | [affinescript](https://github.com/hyperpolymath/affinescript/issues) — the face vocabulary lives in `lib/face.ml` | -| New language feature needed (extern types, dependent types, etc.) | [affinescript](https://github.com/hyperpolymath/affinescript/issues) | -| Brand README is unclear / wrong | this repo | -| Example program doesn't compile | this repo (and probably also affinescript if it's a transformer bug) | -| Tutorial / migration guide additions | this repo | -| Add this face to my IDE / build tool | this repo, but expect it to depend on affinescript work first | - -## Local workflow - -```bash -opam install affinescript # installs the compiler -git clone https://github.com/hyperpolymath/jaffascript -cd jaffascript -just hello # smoke-test the example -just check examples/hello.affine -just preview examples/hello.affine -``` - -## Pull requests - -* SPDX header on every new file (`AGPL-3.0-or-later`). -* Run `just hello` and any other examples added before opening the PR. -* If you're touching the face transformer, open the PR against - [affinescript](https://github.com/hyperpolymath/affinescript), not here. - -## Code of conduct - -See `CODE_OF_CONDUCT.md` (TBD; for now follow the affinescript code of conduct). diff --git a/GOVERNANCE.adoc b/GOVERNANCE.adoc index 8bbf167..9b836fb 100644 --- a/GOVERNANCE.adoc +++ b/GOVERNANCE.adoc @@ -1,162 +1,60 @@ -// SPDX-License-Identifier: MPL-2.0 -// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell -= Governance Model -:toc: preamble +== Governance -This document describes the governance model for this repository. +=== Overview -== Overview +This project is governed by the following principles and structures to +ensure transparent, inclusive, and effective decision-making. -This repository follows a **Sole Maintainer Governance Model**: +=== Roles and Responsibilities -* Single maintainer (@hyperpolymath) has full authority over the project -* All contributions are welcome and reviewed by the maintainer -* Decisions are made transparently through GitHub issues and discussions -* The project adheres to the hyperpolymath estate policies where applicable +==== Maintainers -== Core Principles +Maintainers are responsible for: - Reviewing and merging pull requests - +Managing releases and versioning - Ensuring code quality and standards - +Triaging issues and bug reports - Community engagement and support -[cols="1,2"] -|=== -| Principle | Description +==== Contributors -| **Benevolent Dictatorship** | Maintainer has final decision authority but seeks community input +Contributors are expected to: - Follow the code of conduct - Submit +well-documented pull requests - Write tests for new functionality - +Maintain existing tests - Update documentation as needed -| **Meritocracy** | Contributions are judged on technical merit, not contributor identity +=== Decision Making -| **Transparency** | All significant decisions are documented publicly +==== Minor Changes -| **Consensus-Seeking** | Maintainer prefers consensus but will decide when necessary +* Can be made by any maintainer +* Include bug fixes, documentation updates, dependency updates -| **Open Contribution** | Anyone can contribute via fork and pull request +==== Major Changes -|=== +* Require discussion in issues or pull requests +* Include new features, architectural changes, API changes +* Need approval from at least 2 maintainers -== Roles and Permissions +==== Breaking Changes -[cols="1,2,2"] -|=== -| Role | Permissions | Assignment +* Require RFC (Request for Comments) process +* Need approval from majority of maintainers +* Must include migration guide -| **Maintainer** | Write access, merge rights, admin | @hyperpolymath -| **Contributors** | Read access, fork, submit PRs | All GitHub users -| **Users** | Use the software, report issues | All GitHub users +=== Code of Conduct -|=== +All participants are expected to follow our Code of Conduct. Violations +can be reported to the maintainers. -== Decision Making Framework +=== Communication -=== Routine Decisions +* *Issues*: For bug reports and feature requests +* *Discussions*: For questions and general discussion +* *Pull Requests*: For code contributions -* Bug fixes -* Documentation improvements -* Minor feature additions -* Dependency updates +=== Licensing -**Process**: Maintainer reviews and merges PRs that meet quality standards. +All contributions are made under the terms of the repository’s LICENSE +file. By submitting a pull request, you agree to license your +contributions accordingly. -=== Significant Changes +''''' -* New major features -* API changes -* Architecture modifications -* Breaking changes - -**Process**: -. Open issue describing the change -. Discuss with community (minimum 72 hours) -. Maintainer makes final decision -. Document rationale in issue/PR - -=== Structural Decisions - -* Repository purpose/renaming -* License changes -* Ownership transfer -* Deprecation/archival - -**Process**: -. Extended discussion (minimum 1 week) -. Maintainer makes final decision -. Document in CHANGELOG and governance docs - -== Contribution Lifecycle - -[cols="1,2"] -|=== -| Stage | Process - -| **Ideation** | Open issue, discuss feasibility - -| **Development** | Fork, implement, test thoroughly - -| **Review** | Submit PR, maintainer reviews within 7 days - -| **Merge** | Maintainer merges or requests changes - -| **Release** | Maintainer publishes according to project conventions - -|=== - -== Conflict Resolution - -In case of disagreements: - -. Discuss in the relevant GitHub issue or PR -. Provide technical justification for positions -. Maintainer mediates and makes final decision -. Decision is documented and can be revisited later - -== Project Policies - -This repository adheres to hyperpolymath estate-wide policies: - -* **License**: MPL-2.0 for code, CC-BY-SA-4.0 for prose (per standards/LICENCE-POLICY.adoc) -* **Code of Conduct**: Follows hyperpolymath CODE_OF_CONDUCT.md -* **Security**: Follows hyperpolymath SECURITY.md -* **Contributing**: Follows hyperpolymath CONTRIBUTING.adoc conventions - -== Repository-Specific Conventions - -[cols="1,2"] -|=== -| Convention | Description - -| **Signing** | All commits must be signed (SSH or GPG) - -| **SPDX Headers** | All source files must have SPDX license identifiers - -| **Contractiles** | Mustfile, Trustfile, Intendfile, Adjustfile in root - -| **Machine Readable** | META.a2ml in .machine_readable/6a2/ - -| **CI/CD** | GitHub Actions workflows in .github/workflows/ - -|=== - -== Governance Evolution - -As the project grows, this governance model may evolve: - -* **Adding Co-Maintainers**: When contribution volume warrants it -* **Forming a Team**: For complex multi-maintainer projects -* **Adopting TPCF**: For large, multi-repository projects (see rhodium-standard-repositories) - -Changes to this document require the same process as Significant Changes above. - -== See Also - -* link:MAINTAINERS.adoc[Maintainers] -* link:CODE_OF_CONDUCT.md[Code of Conduct] -* link:CONTRIBUTING.adoc[Contributing Guide] -* link:https://github.com/hyperpolymath/standards/blob/main/LICENCE-POLICY.adoc[Estate License Policy] -* link:https://github.com/hyperpolymath/standards[rhodium-standard-repositories (TPCF)] - -== Changelog - -[cols="1,1,1"] -|=== -| Date | Change | By - -| 2026-06-07 | Initial governance model established | @hyperpolymath -|=== +_Last updated: 2026-07-18_ diff --git a/GOVERNANCE.md b/GOVERNANCE.md deleted file mode 100644 index e27364c..0000000 --- a/GOVERNANCE.md +++ /dev/null @@ -1,60 +0,0 @@ -# Governance - -## Overview - -This project is governed by the following principles and structures to ensure transparent, inclusive, and effective decision-making. - -## Roles and Responsibilities - -### Maintainers - -Maintainers are responsible for: -- Reviewing and merging pull requests -- Managing releases and versioning -- Ensuring code quality and standards -- Triaging issues and bug reports -- Community engagement and support - -### Contributors - -Contributors are expected to: -- Follow the code of conduct -- Submit well-documented pull requests -- Write tests for new functionality -- Maintain existing tests -- Update documentation as needed - -## Decision Making - -### Minor Changes -- Can be made by any maintainer -- Include bug fixes, documentation updates, dependency updates - -### Major Changes -- Require discussion in issues or pull requests -- Include new features, architectural changes, API changes -- Need approval from at least 2 maintainers - -### Breaking Changes -- Require RFC (Request for Comments) process -- Need approval from majority of maintainers -- Must include migration guide - -## Code of Conduct - -All participants are expected to follow our Code of Conduct. Violations can be reported to the maintainers. - -## Communication - -- **Issues**: For bug reports and feature requests -- **Discussions**: For questions and general discussion -- **Pull Requests**: For code contributions - -## Licensing - -All contributions are made under the terms of the repository's LICENSE file. -By submitting a pull request, you agree to license your contributions accordingly. - ---- - -*Last updated: 2026-07-18* diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc new file mode 100644 index 0000000..ba4f03b --- /dev/null +++ b/PROOF-NEEDS.adoc @@ -0,0 +1,135 @@ +== Proof Requirements — \{\{PROJECT}} + +=== Proof Tier + +*Tier*: T3 — Standard + +=== Proof Categories + +[width="100%",cols="24%,36%,40%",options="header",] +|=== +|Code |Meaning |Applies? +|*TP* |Typing Proofs (type soundness, type safety) |Yes + +|*INV* |Invariant Proofs (state machines, monotonicity, bounds) | + +|*SEC* |Security Proofs (crypto, injection freedom, access control) | + +|*CONC* |Concurrency Proofs (linearizability, deadlock freedom) | + +|*ALG* |Algorithm Proofs (termination, correctness, bounds) | + +|*ABI* |ABI/FFI Proofs (memory layout, pointer safety, platform compat) +|Yes + +|*DOM* |Domain-Specific Proofs (bespoke to this project) | +|=== + +=== Mandatory Proofs (All RSR Repos) + +These proofs come from the rsr-template-repo and MUST be present in +every repo: + +==== ABI/FFI Boundary Proofs (Idris2) + +[width="100%",cols="13%,29%,33%,25%",options="header",] +|=== +|# |Proof |Status |File +|ABI-1 |Non-null pointer proofs (`+So (ptr /= 0)+`) |Needed +|`+verification/proofs/idris2/ABI/Pointers.idr+` + +|ABI-2 |Memory layout correctness (`+HasSize+`, `+HasAlignment+`) +|Needed |`+verification/proofs/idris2/ABI/Layout.idr+` + +|ABI-3 |Platform type size proofs (per platform) |Needed +|`+verification/proofs/idris2/ABI/Platform.idr+` + +|ABI-4 |FFI function return type proofs |Needed +|`+verification/proofs/idris2/ABI/Foreign.idr+` + +|ABI-5 |C ABI compliance (`+CABICompliant+`, `+FieldsAligned+`) |Needed +|`+verification/proofs/idris2/ABI/Compliance.idr+` +|=== + +==== Typing Proofs (Prover Varies) + +[width="100%",cols="13%,29%,33%,25%",options="header",] +|=== +|# |Proof |Status |File +|TP-1 |Core data type well-formedness |Needed +|`+verification/proofs/idris2/Types.idr+` + +|TP-2 |Public API type safety (exported functions) |Needed +|`+verification/proofs/lean4/ApiTypes.lean+` +|=== + +=== Project-Specific Proofs + +[cols=",,,,,",options="header",] +|=== +|# |Proof Needed |Category |Prover |Priority |File(s) +| | | | | | +|=== + +=== Dangerous Patterns (BANNED) + +The following MUST NOT appear anywhere in proof files: + +[cols=",,",options="header",] +|=== +|Pattern |Language |Meaning +|`+believe_me+` |Idris2 |Unsafe cast / trust-me +|`+assert_total+` |Idris2 |Skip totality check +|`+postulate+` |Idris2/Agda |Unproven axiom +|`+sorry+` |Lean4 |Incomplete proof +|`+Admitted+` |Coq |Incomplete proof +|`+unsafeCoerce+` |Haskell |Unsafe type cast +|`+Obj.magic+` |OCaml/ReScript |Unsafe type cast +|`+unsafe+` (unaudited) |Rust |Unsafe block without safety comment +|=== + +CI will reject any PR introducing these patterns (enforced by +`+panic-attack assail+`). + +=== Prover Selection Guide + +[width="100%",cols="31%,55%,14%",options="header",] +|=== +|Use Case |Recommended Prover |Why +|ABI/FFI boundaries |*Idris2* |Dependent types model layouts precisely + +|Type system proofs |*Coq* or *Lean4* |Mature proof assistants for +metatheory + +|Algebraic properties |*Lean4* |Good mathlib support + +|Inductive/coinductive |*Agda* |Native support for (co)induction + +|Distributed systems |*TLA+* |Model checking for protocols + +|Numerical properties |*Isabelle* |Strong real analysis library +|=== + +=== Proof File Locations + +.... +verification/proofs/ +├── idris2/ # Idris2 proofs (ABI, dependent types) +│ ├── ABI/ # ABI-specific proofs +│ └── *.idr # Project-specific Idris2 proofs +├── lean4/ # Lean4 proofs (algebra, lattices) +│ └── *.lean +├── agda/ # Agda proofs (induction, metatheory) +│ └── *.agda +├── coq/ # Coq proofs (type systems, compilation) +│ └── *.v +└── tlaplus/ # TLA+ specs (distributed protocols) + └── *.tla +.... + +=== References + +* Master list: `+~/Desktop/PROOF-REQUIREMENTS-MASTER.md+` +* Proof status tracking: `+PROOF-STATUS.md+` (this repo) +* Proven library: `+proven+` repo (Idris2 verified foundations) +* Template: `+rsr-template-repo/PROOF-NEEDS.md+` diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md deleted file mode 100644 index 7e8631a..0000000 --- a/PROOF-NEEDS.md +++ /dev/null @@ -1,106 +0,0 @@ - -# Proof Requirements — {{PROJECT}} - - - -## Proof Tier - - -**Tier**: T3 — Standard - -## Proof Categories - -| Code | Meaning | Applies? | -|------|---------|----------| -| **TP** | Typing Proofs (type soundness, type safety) | Yes | -| **INV** | Invariant Proofs (state machines, monotonicity, bounds) | | -| **SEC** | Security Proofs (crypto, injection freedom, access control) | | -| **CONC** | Concurrency Proofs (linearizability, deadlock freedom) | | -| **ALG** | Algorithm Proofs (termination, correctness, bounds) | | -| **ABI** | ABI/FFI Proofs (memory layout, pointer safety, platform compat) | Yes | -| **DOM** | Domain-Specific Proofs (bespoke to this project) | | - -## Mandatory Proofs (All RSR Repos) - -These proofs come from the rsr-template-repo and MUST be present in every repo: - -### ABI/FFI Boundary Proofs (Idris2) - -| # | Proof | Status | File | -|---|-------|--------|------| -| ABI-1 | Non-null pointer proofs (`So (ptr /= 0)`) | Needed | `verification/proofs/idris2/ABI/Pointers.idr` | -| ABI-2 | Memory layout correctness (`HasSize`, `HasAlignment`) | Needed | `verification/proofs/idris2/ABI/Layout.idr` | -| ABI-3 | Platform type size proofs (per platform) | Needed | `verification/proofs/idris2/ABI/Platform.idr` | -| ABI-4 | FFI function return type proofs | Needed | `verification/proofs/idris2/ABI/Foreign.idr` | -| ABI-5 | C ABI compliance (`CABICompliant`, `FieldsAligned`) | Needed | `verification/proofs/idris2/ABI/Compliance.idr` | - -### Typing Proofs (Prover Varies) - -| # | Proof | Status | File | -|---|-------|--------|------| -| TP-1 | Core data type well-formedness | Needed | `verification/proofs/idris2/Types.idr` | -| TP-2 | Public API type safety (exported functions) | Needed | `verification/proofs/lean4/ApiTypes.lean` | - -## Project-Specific Proofs - - - - -| # | Proof Needed | Category | Prover | Priority | File(s) | -|---|-------------|----------|--------|----------|---------| -| | | | | | | - -## Dangerous Patterns (BANNED) - -The following MUST NOT appear anywhere in proof files: - -| Pattern | Language | Meaning | -|---------|----------|---------| -| `believe_me` | Idris2 | Unsafe cast / trust-me | -| `assert_total` | Idris2 | Skip totality check | -| `postulate` | Idris2/Agda | Unproven axiom | -| `sorry` | Lean4 | Incomplete proof | -| `Admitted` | Coq | Incomplete proof | -| `unsafeCoerce` | Haskell | Unsafe type cast | -| `Obj.magic` | OCaml/ReScript | Unsafe type cast | -| `unsafe` (unaudited) | Rust | Unsafe block without safety comment | - -CI will reject any PR introducing these patterns (enforced by `panic-attack assail`). - -## Prover Selection Guide - -| Use Case | Recommended Prover | Why | -|----------|-------------------|-----| -| ABI/FFI boundaries | **Idris2** | Dependent types model layouts precisely | -| Type system proofs | **Coq** or **Lean4** | Mature proof assistants for metatheory | -| Algebraic properties | **Lean4** | Good mathlib support | -| Inductive/coinductive | **Agda** | Native support for (co)induction | -| Distributed systems | **TLA+** | Model checking for protocols | -| Numerical properties | **Isabelle** | Strong real analysis library | - -## Proof File Locations - -``` -verification/proofs/ -├── idris2/ # Idris2 proofs (ABI, dependent types) -│ ├── ABI/ # ABI-specific proofs -│ └── *.idr # Project-specific Idris2 proofs -├── lean4/ # Lean4 proofs (algebra, lattices) -│ └── *.lean -├── agda/ # Agda proofs (induction, metatheory) -│ └── *.agda -├── coq/ # Coq proofs (type systems, compilation) -│ └── *.v -└── tlaplus/ # TLA+ specs (distributed protocols) - └── *.tla -``` - -## References - -- Master list: `~/Desktop/PROOF-REQUIREMENTS-MASTER.md` -- Proof status tracking: `PROOF-STATUS.md` (this repo) -- Proven library: `proven` repo (Idris2 verified foundations) -- Template: `rsr-template-repo/PROOF-NEEDS.md` diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc new file mode 100644 index 0000000..2f531bd --- /dev/null +++ b/PROOF-STATUS.adoc @@ -0,0 +1,87 @@ +== Proof Status — \{\{PROJECT}} + +=== Summary + +[cols=",,,,,",options="header",] +|=== +|Category |Total |Done |In Progress |Blocked |Remaining +|ABI/FFI (ABI) |5 |0 |0 |0 |5 +|Typing (TP) |2 |0 |0 |0 |2 +|Invariant (INV) |0 |0 |0 |0 |0 +|Security (SEC) |0 |0 |0 |0 |0 +|Concurrency (CONC) |0 |0 |0 |0 |0 +|Algorithm (ALG) |0 |0 |0 |0 |0 +|Domain (DOM) |0 |0 |0 |0 |0 +|*Total* |*7* |*0* |*0* |*0* |*7* +|=== + +*Overall*: 0% proven + +=== Proofs Done + +[cols=",,,,,",options="header",] +|=== +|ID |Proof |Prover |File |Date |Verified By +|— |No proofs completed yet |— |— |— |— +|=== + +=== Proofs In Progress + +[cols=",,,,,",options="header",] +|=== +|ID |Proof |Prover |Assignee |Started |Blocker +|— |— |— |— |— |— +|=== + +=== Proofs Blocked + +[cols=",,,",options="header",] +|=== +|ID |Proof |Blocked By |Notes +|— |— |— |— +|=== + +=== Proofs Remaining + +[cols=",,,,,",options="header",] +|=== +|ID |Proof |Category |Prover |Priority |Est. Effort +|ABI-1 |Non-null pointer proofs |ABI |Idris2 |P1 |2h +|ABI-2 |Memory layout correctness |ABI |Idris2 |P1 |4h +|ABI-3 |Platform type size proofs |ABI |Idris2 |P1 |2h +|ABI-4 |FFI function return type proofs |ABI |Idris2 |P1 |2h +|ABI-5 |C ABI compliance |ABI |Idris2 |P1 |4h +|TP-1 |Core data type well-formedness |TP |Idris2 |P1 |4h +|TP-2 |Public API type safety |TP |Lean4 |P2 |4h +|=== + +=== Verification Commands + +[source,bash] +---- +# Check all Idris2 proofs +just proof-check-idris2 + +# Check all Lean4 proofs +just proof-check-lean4 + +# Check all Agda proofs +just proof-check-agda + +# Check all Coq proofs +just proof-check-coq + +# Run all proof checks +just proof-check-all + +# Scan for dangerous patterns +panic-attack assail --proofs-only +---- + +=== Changelog + +[cols=",,",options="header",] +|=== +|Date |Change |By +|2026-04-04 |Initial proof status tracking |Template +|=== diff --git a/PROOF-STATUS.md b/PROOF-STATUS.md deleted file mode 100644 index aed5e41..0000000 --- a/PROOF-STATUS.md +++ /dev/null @@ -1,84 +0,0 @@ - -# Proof Status — {{PROJECT}} - - - -## Summary - -| Category | Total | Done | In Progress | Blocked | Remaining | -|----------|-------|------|-------------|---------|-----------| -| ABI/FFI (ABI) | 5 | 0 | 0 | 0 | 5 | -| Typing (TP) | 2 | 0 | 0 | 0 | 2 | -| Invariant (INV) | 0 | 0 | 0 | 0 | 0 | -| Security (SEC) | 0 | 0 | 0 | 0 | 0 | -| Concurrency (CONC) | 0 | 0 | 0 | 0 | 0 | -| Algorithm (ALG) | 0 | 0 | 0 | 0 | 0 | -| Domain (DOM) | 0 | 0 | 0 | 0 | 0 | -| **Total** | **7** | **0** | **0** | **0** | **7** | - -**Overall**: 0% proven - -## Proofs Done - - - - - -| ID | Proof | Prover | File | Date | Verified By | -|----|-------|--------|------|------|-------------| -| — | No proofs completed yet | — | — | — | — | - -## Proofs In Progress - -| ID | Proof | Prover | Assignee | Started | Blocker | -|----|-------|--------|----------|---------|---------| -| — | — | — | — | — | — | - -## Proofs Blocked - -| ID | Proof | Blocked By | Notes | -|----|-------|------------|-------| -| — | — | — | — | - -## Proofs Remaining - -| ID | Proof | Category | Prover | Priority | Est. Effort | -|----|-------|----------|--------|----------|-------------| -| ABI-1 | Non-null pointer proofs | ABI | Idris2 | P1 | 2h | -| ABI-2 | Memory layout correctness | ABI | Idris2 | P1 | 4h | -| ABI-3 | Platform type size proofs | ABI | Idris2 | P1 | 2h | -| ABI-4 | FFI function return type proofs | ABI | Idris2 | P1 | 2h | -| ABI-5 | C ABI compliance | ABI | Idris2 | P1 | 4h | -| TP-1 | Core data type well-formedness | TP | Idris2 | P1 | 4h | -| TP-2 | Public API type safety | TP | Lean4 | P2 | 4h | - -## Verification Commands - -```bash -# Check all Idris2 proofs -just proof-check-idris2 - -# Check all Lean4 proofs -just proof-check-lean4 - -# Check all Agda proofs -just proof-check-agda - -# Check all Coq proofs -just proof-check-coq - -# Run all proof checks -just proof-check-all - -# Scan for dangerous patterns -panic-attack assail --proofs-only -``` - -## Changelog - -| Date | Change | By | -|------|--------|-----| -| 2026-04-04 | Initial proof status tracking | Template | diff --git a/READINESS.adoc b/READINESS.adoc new file mode 100644 index 0000000..4962c9a --- /dev/null +++ b/READINESS.adoc @@ -0,0 +1,55 @@ +== rattlescript Component Readiness Assessment + +*Standard:* +https://github.com/hyperpolymath/standards/tree/main/component-readiness-grades[Component +Readiness Grades (CRG) v2.2] *Current Grade:* C *Assessed:* \{\{DATE}} +*Assessor:* Jonathan D.A. Jewell + +''''' + +=== Summary + +[width="100%",cols="25%,8%,17%,50%",options="header",] +|=== +|Component |Grade |Release Stage |Evidence Summary +|Primary component |C |Alpha-stable |Dogfooded on own project; CI +passing +|=== + +*Overall:* Grade C — dogfooding confirmed, CI passing, deep annotation +in place. + +''''' + +=== Grade C Evidence + +* Deployed and dogfooded on the rattlescript project itself +* CI passing (dogfood-gate, hypatia-scan, static-analysis-gate) +* TEST-NEEDS.md documents test matrix +* No home failures +* Deep code and folder annotation in place per CRG v2 requirements + +''''' + +=== Promotion Path to Grade B + +Grade B requires: *6+ diverse external targets tested, issues fed back*. + +Diversity means: different languages, different architectures, different +use cases. + +To reach B: 1. Deploy on at least 6 external projects that differ +meaningfully from each other 2. Confirm it works in each (or document +failures) 3. Feed back any issues found (GitHub issues or PRs) 4. Update +this file with the evidence + +''''' + +=== Concerns and Maintenance Notes + +_Document any known limitations, demotion risks, or maintenance concerns +here._ + +''''' + +=== Run `+just crg-badge+` to generate the shields.io badge for your README. diff --git a/READINESS.md b/READINESS.md deleted file mode 100644 index ba16ce0..0000000 --- a/READINESS.md +++ /dev/null @@ -1,56 +0,0 @@ - - - -# rattlescript Component Readiness Assessment - -**Standard:** [Component Readiness Grades (CRG) v2.2](https://github.com/hyperpolymath/standards/tree/main/component-readiness-grades) -**Current Grade:** C -**Assessed:** {{DATE}} -**Assessor:** Jonathan D.A. Jewell - ---- - -## Summary - -| Component | Grade | Release Stage | Evidence Summary | -|---------------------|-------|---------------|-------------------------------------------| -| Primary component | C | Alpha-stable | Dogfooded on own project; CI passing | - -**Overall:** Grade C — dogfooding confirmed, CI passing, deep annotation in place. - ---- - -## Grade C Evidence - -- Deployed and dogfooded on the rattlescript project itself -- CI passing (dogfood-gate, hypatia-scan, static-analysis-gate) -- TEST-NEEDS.md documents test matrix -- No home failures -- Deep code and folder annotation in place per CRG v2 requirements - ---- - -## Promotion Path to Grade B - -Grade B requires: **6+ diverse external targets tested, issues fed back**. - -Diversity means: different languages, different architectures, different use cases. - -To reach B: -1. Deploy on at least 6 external projects that differ meaningfully from each other -2. Confirm it works in each (or document failures) -3. Feed back any issues found (GitHub issues or PRs) -4. Update this file with the evidence - ---- - -## Concerns and Maintenance Notes - -*Document any known limitations, demotion risks, or maintenance concerns here.* - ---- - -## Run `just crg-badge` to generate the shields.io badge for your README. diff --git a/README.adoc b/README.adoc new file mode 100644 index 0000000..4f5ef81 --- /dev/null +++ b/README.adoc @@ -0,0 +1,138 @@ +https://opensource.org/licenses/MPL-2.0[image:https://img.shields.io/badge/License-MPL_2.0-blue.svg[License: +MPL-2.0]] + +JavaScript / TypeScript-syntax AffineScript. Write code that looks like +JS or TS, get affine resource guarantees and typed-wasm output. + +== What it is + +JaffaScript is +https://github.com/hyperpolymath/affinescript[AffineScript] with its +`+jaffa+` face pre-selected. If you write JavaScript or TypeScript, you +already know most of the syntax. The compiler checks that your resources +(files, sockets, tokens, handles) are used *exactly as many times as you +declare* — and proves it at compile time. No null pointer exceptions. No +use-after-free. No silent data races. No GC overhead. + +This repo is a *brand surface only*. The compiler, type checker, borrow +checker, and codegen all live in +https://github.com/hyperpolymath/affinescript[affinescript]. This repo +carries: + +* Examples idiomatic to JS / TS developers +* Documentation aimed at the web-development community +* A `+jaffa+` shim CLI that aliases `+affinescript+` `+--face+` +`+jaffa+` +* Tutorial and migration guides for moving TypeScript codebases into a +strongly-typed, affine-typed, WASM-targeting world + +== Hello + +`+examples/hello.affine+`: + +[source,affine] +---- +// face: jaffascript + +effect IO { + fn println(s: String) -> (); +} + +function main() -{IO}-> () { + const greeting = "Hello, JaffaScript!"; + println(greeting); +} +---- + +`+function+`, `+const+`, `+===+`, `+null+`/`+undefined+`, `+import+` +`+{+` `+x+` `+}+` `+from+` `+"module"+` — all lower to canonical +AffineScript and produce the same typed-wasm output as every other face. + +== Install + +[source,bash] +---- +opam install affinescript +git clone https://github.com/hyperpolymath/jaffascript +cd jaffascript +---- + +The `+affinescript+` binary does the work. The `+bin/jaffa+` shim in +this repo just defaults the `+--face+` flag. + +== Use + +[source,bash] +---- +# Direct, via affinescript: +affinescript eval --face jaffa examples/hello.affine +affinescript compile --face jaffa examples/hello.affine -o hello.wasm + +# Or via the jaffa shim (same thing): +./bin/jaffa eval examples/hello.affine +./bin/jaffa compile examples/hello.affine -o hello.wasm + +# Or via the justfile: +just run examples/hello.affine +just preview examples/hello.affine # show the canonical lowering +---- + +Source files use the canonical `+.affine+` extension. The face is +selected by the pragma on the first comment line, or by the `+--face+` +`+jaffa+` flag. + +== Different faces, same cube + +JaffaScript is one of six established faces over the AffineScript core: + +* AffineScript — the canonical face +* https://github.com/hyperpolymath/rattlescript[RattleScript] — +Python-style +* *JaffaScript* — JavaScript / TypeScript-style (this repo) +* https://github.com/hyperpolymath/lucidscript[LucidScript] — PureScript +/ Haskell-style +* https://github.com/hyperpolymath/cafescripto[CafeScripto] — +CoffeeScript-style +* https://github.com/hyperpolymath/pseudoscript[PseudoScript] — +pseudocode-style + +All six share the canonical `+.affine+` extension and lower to the same +AST. Errors are reported in face-appropriate vocabulary. + +== Why JaffaScript + +JavaScript and TypeScript are the dominant languages of the web. +TypeScript adds structural typing on top of dynamic JS, which catches a +lot of bugs but doesn’t help with: ownership, resource leaks, effect +tracking, formal proofs, or portable native compilation. JaffaScript is +a JS-shaped on-ramp to a language that adds all of those — without +forcing you to abandon brace syntax, arrow functions, or `+import+` +`+{+` `+x+` `+}+` `+from+` `+"module"+`. + +For a TypeScript developer migrating in, the steps are: + +[arabic] +. Rename `+.ts+` files to `+.affine+` and add at the top. +. Replace `+import+` `+{+` `+…+` `+}+` `+from+` `+"module"+` (TS) with +the same syntax in canonical AffineScript form. +. Replace `+null+`/`+undefined+` with `+()+` (canonical unit) in +semantics-relevant positions. +. Keep writing `+===+` — the face transforms `+===+` → `+==+` +automatically. +. Compile to typed-wasm; the output runs in browsers, Node, Deno, +Wasmtime, and any WASI runtime. + +== Status + +Alpha. The face transformer is implemented in +`+affinescript/lib/js_face.ml+`. Known limitations are tracked in +https://github.com/hyperpolymath/affinescript/blob/main/examples/faces/README.adoc[the +affinescript faces README] under "`Known transformer gaps`". + +== License + +This project is licensed under the Mozilla Public License, v. 2.0. See +the `+LICENSE+` file for details. Documentation is licensed +CC-BY-SA-4.0. + +SPDX-License-Identifier: CC-BY-SA-4.0 diff --git a/README.md b/README.md deleted file mode 100644 index 6cbf67b..0000000 --- a/README.md +++ /dev/null @@ -1,148 +0,0 @@ - - -[![License: MPL-2.0](https://img.shields.io/badge/License-MPL_2.0-blue.svg)](https://opensource.org/licenses/MPL-2.0) - -JavaScript / TypeScript-syntax AffineScript. Write code that looks like -JS or TS, get affine resource guarantees and typed-wasm output. - -# What it is - -JaffaScript is -[AffineScript](https://github.com/hyperpolymath/affinescript) with its -`jaffa` face pre-selected. If you write JavaScript or TypeScript, you -already know most of the syntax. The compiler checks that your resources -(files, sockets, tokens, handles) are used **exactly as many times as -you declare** — and proves it at compile time. No null pointer -exceptions. No use-after-free. No silent data races. No GC overhead. - -This repo is a **brand surface only**. The compiler, type checker, -borrow checker, and codegen all live in -[affinescript](https://github.com/hyperpolymath/affinescript). This repo -carries: - -- Examples idiomatic to JS / TS developers - -- Documentation aimed at the web-development community - -- A `jaffa` shim CLI that aliases `affinescript` `--face` `jaffa` - -- Tutorial and migration guides for moving TypeScript codebases into a - strongly-typed, affine-typed, WASM-targeting world - -# Hello - -`examples/hello.affine`: - -```affine -// face: jaffascript - -effect IO { - fn println(s: String) -> (); -} - -function main() -{IO}-> () { - const greeting = "Hello, JaffaScript!"; - println(greeting); -} -``` - -`function`, `const`, `===`, `null`/`undefined`, `import` `{` `x` `}` -`from` `"module"` — all lower to canonical AffineScript and produce the -same typed-wasm output as every other face. - -# Install - -```bash -opam install affinescript -git clone https://github.com/hyperpolymath/jaffascript -cd jaffascript -``` - -The `affinescript` binary does the work. The `bin/jaffa` shim in this -repo just defaults the `--face` flag. - -# Use - -```bash -# Direct, via affinescript: -affinescript eval --face jaffa examples/hello.affine -affinescript compile --face jaffa examples/hello.affine -o hello.wasm - -# Or via the jaffa shim (same thing): -./bin/jaffa eval examples/hello.affine -./bin/jaffa compile examples/hello.affine -o hello.wasm - -# Or via the justfile: -just run examples/hello.affine -just preview examples/hello.affine # show the canonical lowering -``` - -Source files use the canonical `.affine` extension. The face is selected -by the pragma on the first comment line, or by the `--face` `jaffa` -flag. - -# Different faces, same cube - -JaffaScript is one of six established faces over the AffineScript core: - -- AffineScript — the canonical face - -- [RattleScript](https://github.com/hyperpolymath/rattlescript) — - Python-style - -- **JaffaScript** — JavaScript / TypeScript-style (this repo) - -- [LucidScript](https://github.com/hyperpolymath/lucidscript) — - PureScript / Haskell-style - -- [CafeScripto](https://github.com/hyperpolymath/cafescripto) — - CoffeeScript-style - -- [PseudoScript](https://github.com/hyperpolymath/pseudoscript) — - pseudocode-style - -All six share the canonical `.affine` extension and lower to the same -AST. Errors are reported in face-appropriate vocabulary. - -# Why JaffaScript - -JavaScript and TypeScript are the dominant languages of the web. -TypeScript adds structural typing on top of dynamic JS, which catches a -lot of bugs but doesn’t help with: ownership, resource leaks, effect -tracking, formal proofs, or portable native compilation. JaffaScript is -a JS-shaped on-ramp to a language that adds all of those — without -forcing you to abandon brace syntax, arrow functions, or `import` `{` -`x` `}` `from` `"module"`. - -For a TypeScript developer migrating in, the steps are: - -1. Rename `.ts` files to `.affine` and add at the top. - -2. Replace `import` `{` `…` `}` `from` `"module"` (TS) with the same - syntax in canonical AffineScript form. - -3. Replace `null`/`undefined` with `()` (canonical unit) in - semantics-relevant positions. - -4. Keep writing `===` — the face transforms `===` → `==` automatically. - -5. Compile to typed-wasm; the output runs in browsers, Node, Deno, - Wasmtime, and any WASI runtime. - -# Status - -Alpha. The face transformer is implemented in -`affinescript/lib/js_face.ml`. Known limitations are tracked in [the -affinescript faces -README](https://github.com/hyperpolymath/affinescript/blob/main/examples/faces/README.adoc) -under "Known transformer gaps". - -# License - -This project is licensed under the Mozilla Public License, v. 2.0. See -the `LICENSE` file for details. Documentation is licensed CC-BY-SA-4.0. - -SPDX-License-Identifier: CC-BY-SA-4.0 diff --git a/SECURITY.adoc b/SECURITY.adoc new file mode 100644 index 0000000..e47fdd9 --- /dev/null +++ b/SECURITY.adoc @@ -0,0 +1,16 @@ +== Security Policy + +=== Reporting a Vulnerability + +If you discover a security vulnerability, please report it responsibly. + +*Email:* j.d.a.jewell@open.ac.uk + +*Please include:* - Description of the vulnerability - Steps to +reproduce - Potential impact + +*Response timeline:* - Acknowledgement within 48 hours - Initial +assessment within 7 days - Fix or mitigation within 90 days + +*Safe harbour:* We will not pursue legal action against security +researchers who follow responsible disclosure. diff --git a/SECURITY.md b/SECURITY.md deleted file mode 100644 index 88df5ba..0000000 --- a/SECURITY.md +++ /dev/null @@ -1,23 +0,0 @@ - -# Security Policy - -## Reporting a Vulnerability - -If you discover a security vulnerability, please report it responsibly. - -**Email:** j.d.a.jewell@open.ac.uk - -**Please include:** -- Description of the vulnerability -- Steps to reproduce -- Potential impact - -**Response timeline:** -- Acknowledgement within 48 hours -- Initial assessment within 7 days -- Fix or mitigation within 90 days - -**Safe harbour:** We will not pursue legal action against security researchers who follow responsible disclosure. diff --git a/TEST-NEEDS.adoc b/TEST-NEEDS.adoc new file mode 100644 index 0000000..167becf --- /dev/null +++ b/TEST-NEEDS.adoc @@ -0,0 +1,138 @@ +== TEST-NEEDS: rsr-template-repo + +=== CRG Grade: C — ACHIEVED 2026-04-04 + +=== Current State (Updated 2026-04-04) + +[width="100%",cols="40%,26%,34%",options="header",] +|=== +|Category |Count |Details +|*Source modules* |6 |3 Idris2 ABI (Foreign, Layout, Types), 2 Zig FFI +(build, main), 1 Zig integration test template + +|*Unit tests* |0 |None in main source (inline tests in main.zig) + +|*Integration tests* |1 |test/integration_test.zig (documented template, +1 placeholder test) + +|*E2E tests* |1 |tests/e2e/template_instantiation_test.sh (full +instantiation + validation) + +|*Workflow tests* |1 |tests/workflows/validate_workflows_test.sh (21 +workflows validated) + +|*Validation tests* |1 |scripts/validate-template.sh (8-phase +comprehensive validation) + +|*Benchmarks* |5 |benches/template_bench.sh (validation, Zig build, +tests, workflows, instantiation) + +|*Fuzz tests* |0 |README.adoc scaffold with harness instructions +|=== + +=== Completed Work (CRG C - Testing & Benchmarking) + +==== Template Validation Script ✅ + +* [x] `+scripts/validate-template.sh+` — 8-phase validation +** Phase 1: Core repository structure (root files, directories) +** Phase 2: Machine-readable metadata (.machine_readable/) +** Phase 3: GitHub Actions workflows (17 required + all present) +** Phase 4: Idris2 ABI and Zig FFI source files +** Phase 5: Placeholder token replacement (skipped in template) +** Phase 6: SPDX license headers (100% coverage, 6/6 files) +** Phase 7: Build system verification (zig build + idris2 syntax check) +** Phase 8: Documentation requirements (TOPOLOGY, ABI-FFI-README, etc) +* Status: *PASSING* (0 errors, 3 warnings about template placeholders) + +==== E2E Template Instantiation Test ✅ + +* [x] `+tests/e2e/template_instantiation_test.sh+` — full workflow +** Clones template to temp directory +** Replaces all \{\{PLACEHOLDER}} tokens with test values +** Validates resulting structure with scripts/validate-template.sh +** Verifies Zig build works after instantiation +** Checks no remaining placeholders +** Cleans up temp directory +* Status: *READY TO TEST* (can be verified by CI) + +==== Workflow Validation Test ✅ + +* [x] `+tests/workflows/validate_workflows_test.sh+` +** Validates all 21 workflows exist and have proper structure +** Checks SPDX headers, '`name`' field +** Verifies all 15 required workflows present +* Status: *PASSING* (0 errors, 15/15 required workflows found) + +==== Zig FFI Tests ✅ + +* [x] `+src/interface/ffi/test/integration_test.zig+` — template with +examples +** Converted from \{\{project}} placeholders to "`template`" namespace +** Added comprehensive comments for how to instantiate +** Tests grouped by category (lifecycle, operations, strings, errors, +version, memory safety, threading) +** Compiles and passes placeholder test +* Status: *PASSING* (1 test: placeholder_test_implementation_required +passes) + +==== Benchmarks ✅ + +* [x] `+benches/template_bench.sh+` — 5 benchmark suites +** Validation script: ~5.8s average (3 runs) +** Zig build: ~19ms (clean build) +** Zig tests: ~20ms +** Workflow validation: ~117ms +** Template instantiation: ~427ms +* Formats: human, json, csv +* Status: *PASSING* (all benchmarks execute) + +==== Build System ✅ + +* [x] `+src/interface/ffi/build.zig+` — updated for Zig 0.15.2 +** Simplified to test-only configuration +** Supports both unit tests and integration tests +** Works with `+zig build+` without errors +* Status: *PASSING* (builds successfully) + +=== Test Results Summary + +.... +Validation Script: PASS (0 errors, 3 warnings) +Workflow Validation: PASS (21/21 workflows valid) +Integration Tests: PASS (1/1 placeholder test) +E2E Instantiation: READY (needs CI confirmation) +Benchmarks: PASS (5/5 benchmark suites) +Build System: PASS (zig build succeeds) +.... + +=== CRG C Compliance + +* *Coverage*: 6/6 test categories (unit, integration, E2E, workflow, +validation, benchmarks) +* *Documentation*: All test files have SPDX headers + inline +documentation +* *Author Attribution*: Jonathan D.A. Jewell +6759885+hyperpolymath@users.noreply.github.com +* *License*: PMPL-1.0-or-later on all new files +* *Automation*: All scripts executable + working + +=== FLAGGED ISSUES - ALL RESOLVED + +* [line-through]#*Template repo used by ALL new repos has 0 validation +tests*# → FIXED: 4 test suites + validation script +* [line-through]#*fuzz/placeholder.txt*# → FIXED: replaced with +README.adoc containing real harness instructions +* [line-through]#*No E2E tests for template instantiation*# → FIXED: +full E2E test suite +* [line-through]#*Zig FFI integration tests are placeholders*# → FIXED: +converted to documented template format + +=== Next Steps (Future Sessions) + +* [ ] Integrate test scripts into CI/CD workflows +* [ ] Generate test coverage reports +* [ ] Add more specialized benchmarks (memory, threading stress) +* [ ] Document test instantiation patterns for new repos + +=== Priority: P0 (COMPLETE) ✅ diff --git a/TEST-NEEDS.md b/TEST-NEEDS.md deleted file mode 100644 index f73943c..0000000 --- a/TEST-NEEDS.md +++ /dev/null @@ -1,111 +0,0 @@ - -# TEST-NEEDS: rsr-template-repo - -## CRG Grade: C — ACHIEVED 2026-04-04 - -## Current State (Updated 2026-04-04) - -| Category | Count | Details | -|----------|-------|---------| -| **Source modules** | 6 | 3 Idris2 ABI (Foreign, Layout, Types), 2 Zig FFI (build, main), 1 Zig integration test template | -| **Unit tests** | 0 | None in main source (inline tests in main.zig) | -| **Integration tests** | 1 | test/integration_test.zig (documented template, 1 placeholder test) | -| **E2E tests** | 1 | tests/e2e/template_instantiation_test.sh (full instantiation + validation) | -| **Workflow tests** | 1 | tests/workflows/validate_workflows_test.sh (21 workflows validated) | -| **Validation tests** | 1 | scripts/validate-template.sh (8-phase comprehensive validation) | -| **Benchmarks** | 5 | benches/template_bench.sh (validation, Zig build, tests, workflows, instantiation) | -| **Fuzz tests** | 0 | README.adoc scaffold with harness instructions | - -## Completed Work (CRG C - Testing & Benchmarking) - -### Template Validation Script ✅ -- [x] `scripts/validate-template.sh` — 8-phase validation - - Phase 1: Core repository structure (root files, directories) - - Phase 2: Machine-readable metadata (.machine_readable/) - - Phase 3: GitHub Actions workflows (17 required + all present) - - Phase 4: Idris2 ABI and Zig FFI source files - - Phase 5: Placeholder token replacement (skipped in template) - - Phase 6: SPDX license headers (100% coverage, 6/6 files) - - Phase 7: Build system verification (zig build + idris2 syntax check) - - Phase 8: Documentation requirements (TOPOLOGY, ABI-FFI-README, etc) -- Status: **PASSING** (0 errors, 3 warnings about template placeholders) - -### E2E Template Instantiation Test ✅ -- [x] `tests/e2e/template_instantiation_test.sh` — full workflow - - Clones template to temp directory - - Replaces all {{PLACEHOLDER}} tokens with test values - - Validates resulting structure with scripts/validate-template.sh - - Verifies Zig build works after instantiation - - Checks no remaining placeholders - - Cleans up temp directory -- Status: **READY TO TEST** (can be verified by CI) - -### Workflow Validation Test ✅ -- [x] `tests/workflows/validate_workflows_test.sh` - - Validates all 21 workflows exist and have proper structure - - Checks SPDX headers, 'name' field - - Verifies all 15 required workflows present -- Status: **PASSING** (0 errors, 15/15 required workflows found) - -### Zig FFI Tests ✅ -- [x] `src/interface/ffi/test/integration_test.zig` — template with examples - - Converted from {{project}} placeholders to "template" namespace - - Added comprehensive comments for how to instantiate - - Tests grouped by category (lifecycle, operations, strings, errors, version, memory safety, threading) - - Compiles and passes placeholder test -- Status: **PASSING** (1 test: placeholder_test_implementation_required passes) - -### Benchmarks ✅ -- [x] `benches/template_bench.sh` — 5 benchmark suites - - Validation script: ~5.8s average (3 runs) - - Zig build: ~19ms (clean build) - - Zig tests: ~20ms - - Workflow validation: ~117ms - - Template instantiation: ~427ms -- Formats: human, json, csv -- Status: **PASSING** (all benchmarks execute) - -### Build System ✅ -- [x] `src/interface/ffi/build.zig` — updated for Zig 0.15.2 - - Simplified to test-only configuration - - Supports both unit tests and integration tests - - Works with `zig build` without errors -- Status: **PASSING** (builds successfully) - -## Test Results Summary - -``` -Validation Script: PASS (0 errors, 3 warnings) -Workflow Validation: PASS (21/21 workflows valid) -Integration Tests: PASS (1/1 placeholder test) -E2E Instantiation: READY (needs CI confirmation) -Benchmarks: PASS (5/5 benchmark suites) -Build System: PASS (zig build succeeds) -``` - -## CRG C Compliance - -- **Coverage**: 6/6 test categories (unit, integration, E2E, workflow, validation, benchmarks) -- **Documentation**: All test files have SPDX headers + inline documentation -- **Author Attribution**: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com> -- **License**: PMPL-1.0-or-later on all new files -- **Automation**: All scripts executable + working - -## FLAGGED ISSUES - ALL RESOLVED - -- ~~**Template repo used by ALL new repos has 0 validation tests**~~ → FIXED: 4 test suites + validation script -- ~~**fuzz/placeholder.txt**~~ → FIXED: replaced with README.adoc containing real harness instructions -- ~~**No E2E tests for template instantiation**~~ → FIXED: full E2E test suite -- ~~**Zig FFI integration tests are placeholders**~~ → FIXED: converted to documented template format - -## Next Steps (Future Sessions) - -- [ ] Integrate test scripts into CI/CD workflows -- [ ] Generate test coverage reports -- [ ] Add more specialized benchmarks (memory, threading stress) -- [ ] Document test instantiation patterns for new repos - -## Priority: P0 (COMPLETE) ✅ diff --git a/TOPOLOGY.adoc b/TOPOLOGY.adoc new file mode 100644 index 0000000..a975f58 --- /dev/null +++ b/TOPOLOGY.adoc @@ -0,0 +1,36 @@ +== Architecture Topology + +=== System Overview + +RSR (Rhodium Standard Repository) template provides the canonical +scaffold for all hyperpolymath projects, with integrated CI/CD, +documentation, and service discovery patterns. + +=== Component Overview + +[width="100%",cols="37%,33%,30%",options="header",] +|=== +|Component |Language |Purpose +|dogfood-gate workflow |YAML |Quality checks (CRG, security, linting) +|eclexiaiser-validate job |YAML |Resource cost awareness scoring +|Groove discovery |JSON |Service endpoint registration +|=== + +=== Data Flow + +.... +[Code Push] → [GitHub Actions] → [hypatia scan] → [eclexiaiser validate] → [Results] +.... + +=== Integration Points + +* *Upstream*: Hypatia (neurosymbolic CI/CD), eclexiaiser (resource +scoring) +* *Downstream*: All RSR-based repositories (500+ instances) + +=== Deployment + +* Container: Stapeln Six ecosystem +* CI/CD: GitHub Actions → Hypatia scan → eclexiaiser-validate (6 +scorecard dimensions) → Mirror +* Service Discovery: Groove protocol (.well-known/groove/manifest.json) diff --git a/TOPOLOGY.md b/TOPOLOGY.md deleted file mode 100644 index 98995e1..0000000 --- a/TOPOLOGY.md +++ /dev/null @@ -1,36 +0,0 @@ - - - -# Architecture Topology - -## System Overview - -RSR (Rhodium Standard Repository) template provides the canonical scaffold for all hyperpolymath projects, with integrated CI/CD, documentation, and service discovery patterns. - -## Component Overview - -| Component | Language | Purpose | -|-----------|----------|---------| -| dogfood-gate workflow | YAML | Quality checks (CRG, security, linting) | -| eclexiaiser-validate job | YAML | Resource cost awareness scoring | -| Groove discovery | JSON | Service endpoint registration | - -## Data Flow - -``` -[Code Push] → [GitHub Actions] → [hypatia scan] → [eclexiaiser validate] → [Results] -``` - -## Integration Points - -- **Upstream**: Hypatia (neurosymbolic CI/CD), eclexiaiser (resource scoring) -- **Downstream**: All RSR-based repositories (500+ instances) - -## Deployment - -- Container: Stapeln Six ecosystem -- CI/CD: GitHub Actions → Hypatia scan → eclexiaiser-validate (6 scorecard dimensions) → Mirror -- Service Discovery: Groove protocol (.well-known/groove/manifest.json) diff --git a/docs/reports/audit/audit-2026-04-15-post.adoc b/docs/reports/audit/audit-2026-04-15-post.adoc new file mode 100644 index 0000000..2faec23 --- /dev/null +++ b/docs/reports/audit/audit-2026-04-15-post.adoc @@ -0,0 +1,39 @@ +== Post-audit Status Report: jaffascript + +* *Date:* 2026-04-15 +* *Status:* Complete (M5 Sweep) +* *Repo:* /var/mnt/eclipse/repos/jaffascript + +=== Actions Taken + +[arabic] +. Standard CI/Workflow Sweep: Added blocker workflows +(`+ts-blocker.yml+`, `+npm-bun-blocker.yml+`) and updated `+Justfile+`. +. SCM-to-A2ML Migration: Staged and committed deletions of legacy +`+.scm+` files. +. Lockfile Sweep: Generated and tracked missing lockfiles where +manifests were present. +. Static Analysis: Verified with `+panic-attack assail+`. + +=== Findings Summary + +* 14 TODO/FIXME/HACK markers in +.machine_readable/contractiles/self-validating/template-hunt.k9.ncl +* flake.nix declares inputs without narHash, rev pinning, or sibling +flake.lock — dependency revision is unpinned in flake.nix +* Hardcoded /tmp/ path without mktemp in tests/e2e.sh +* 14 TODO/FIXME/HACK markers in +affinescript/contractiles/self-validating/template-hunt.k9.ncl +* DOM manipulation (innerHTML/document.write) in +affinescript/tools/affine-doc/assets/search.js +* 18 TODO/FIXME/HACK markers in +affinescript/tools/affine-pkg/src/main.rs +* 9 unwrap/expect calls in +affinescript/tools/affinescript-lsp/src/handlers.rs +* Rust project has test infrastructure but no mutation-test +configuration (cargo-mutants/.cargo-mutants.toml) — add +`+cargo mutants+` to verify test suite kills mutations + +=== Final Grade + +* *CRG Grade:* D (Promoted from E/X) - CI and lockfiles are in place. diff --git a/docs/reports/audit/audit-2026-04-15-post.md b/docs/reports/audit/audit-2026-04-15-post.md deleted file mode 100644 index 454c201..0000000 --- a/docs/reports/audit/audit-2026-04-15-post.md +++ /dev/null @@ -1,27 +0,0 @@ - -# Post-audit Status Report: jaffascript -- **Date:** 2026-04-15 -- **Status:** Complete (M5 Sweep) -- **Repo:** /var/mnt/eclipse/repos/jaffascript - -## Actions Taken -1. Standard CI/Workflow Sweep: Added blocker workflows (`ts-blocker.yml`, `npm-bun-blocker.yml`) and updated `Justfile`. -2. SCM-to-A2ML Migration: Staged and committed deletions of legacy `.scm` files. -3. Lockfile Sweep: Generated and tracked missing lockfiles where manifests were present. -4. Static Analysis: Verified with `panic-attack assail`. - -## Findings Summary -- 14 TODO/FIXME/HACK markers in .machine_readable/contractiles/self-validating/template-hunt.k9.ncl -- flake.nix declares inputs without narHash, rev pinning, or sibling flake.lock — dependency revision is unpinned in flake.nix -- Hardcoded /tmp/ path without mktemp in tests/e2e.sh -- 14 TODO/FIXME/HACK markers in affinescript/contractiles/self-validating/template-hunt.k9.ncl -- DOM manipulation (innerHTML/document.write) in affinescript/tools/affine-doc/assets/search.js -- 18 TODO/FIXME/HACK markers in affinescript/tools/affine-pkg/src/main.rs -- 9 unwrap/expect calls in affinescript/tools/affinescript-lsp/src/handlers.rs -- Rust project has test infrastructure but no mutation-test configuration (cargo-mutants/.cargo-mutants.toml) — add `cargo mutants` to verify test suite kills mutations - -## Final Grade -- **CRG Grade:** D (Promoted from E/X) - CI and lockfiles are in place. diff --git a/docs/tech-debt-2026-05-26.adoc b/docs/tech-debt-2026-05-26.adoc new file mode 100644 index 0000000..da26e7f --- /dev/null +++ b/docs/tech-debt-2026-05-26.adoc @@ -0,0 +1,80 @@ +== Tech-Debt Audit — jaffascript — 2026-05-26 + +*Source:* estate-wide automated scan 2026-05-26. *Companion:* +https://github.com/hyperpolymath/standards/tree/main/docs/audits[`+hyperpolymath/standards+` +2026-05-26-estate-*-debt audits]. *Combined severity:* `+LOW+`. + +This file records the _raw findings_ — it does not by itself fix the +debt. Each section ends with a '`Recommended next move`' line; closing +the debt is follow-up work. + +=== 1. Proof debt + +Scanner counted the following markers in proof-bearing files of this +repo: + +.... +files= 13 | Coq-Axm/Adm= 0 | Lean-srry/ax= 0 | Agda-pst= 0 | Idr-blv= 6 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0 +.... + +*Total markers:* 6. *Severity:* `+>06+`. + +*Marker types* (any non-zero counts above): - Coq `+Axiom+`/`+Admitted+` +— unconditional proof escapes. - Lean `+sorry+`/`+axiom+` — Lean’s +equivalent. - Agda `+postulate+` — accepted axiomatically. - Idris2 +`+believe_me+`/`+assert_total+` — runtime-safe coercion / totality +assumption. - Idris2 top-level `+partial+` — totality-check waived. - F* +`+assume val+`/`+admit_p+` — F* admit. - `+TODO PROOF+` / `+OWED:+` — +self-documented debt markers. - `+unsafePerformIO+`/`+unsafeCoerce+` — +soundness-relevant escape hatches in Haskell/Rust source. + +*Recommended next move:* triage each finding into one of: (a) discharge +by proof, (b) cover with property-tests + a documented refutation +budget, or (c) annotate as a known/necessary axiom (e.g. `+funExt+`) in +`+docs/proof-debt.md+`. + +=== 2. Licence debt + +[cols=",",options="header",] +|=== +|Field |Value +|LICENSE file |`+LICENSE+` +|SPDX header |`+PMPL-1.0-or-later+` +|Manifest licence |`+NONE+` +|Body classifier |`+PMPL-1.0-or-later+` +|Severity |`+ok+` +|=== + +*Recommended next move:* none for licence. + +=== 3. Documentation debt + +[cols=",",options="header",] +|=== +|Field |Value +|README lines |99 +|`+docs/+` files |55 +|`+docs/+` LoC |2261 +|CHANGELOG.md |Y +|CONTRIBUTING.md |Y +|CODE_OF_CONDUCT.md |Y +|SECURITY.md |Y +|Severity |`+OK+` +|=== + +*Recommended next move:* none for docs. + +=== Cross-references + +* Estate proof-debt audit: +`+hyperpolymath/standards/docs/audits/2026-05-26-estate-proof-debt.md+` +* Estate licence-debt audit: +`+hyperpolymath/standards/docs/audits/2026-05-26-estate-licence-debt.md+` +* Estate documentation-debt audit: +`+hyperpolymath/standards/docs/audits/2026-05-26-estate-documentation-debt.md+` + +''''' + +🤖 Generated by Claude Code estate-wide tech-debt scan (2026-05-26). +This file is informational — closing the debt is follow-up work owned by +the maintainer. diff --git a/docs/tech-debt-2026-05-26.md b/docs/tech-debt-2026-05-26.md deleted file mode 100644 index a742757..0000000 --- a/docs/tech-debt-2026-05-26.md +++ /dev/null @@ -1,71 +0,0 @@ - - -# Tech-Debt Audit — jaffascript — 2026-05-26 - -**Source:** estate-wide automated scan 2026-05-26. -**Companion:** [`hyperpolymath/standards` 2026-05-26-estate-*-debt audits](https://github.com/hyperpolymath/standards/tree/main/docs/audits). -**Combined severity:** `LOW`. - -This file records the *raw findings* — it does not by itself fix the debt. Each section ends with a 'Recommended next move' line; closing the debt is follow-up work. - -## 1. Proof debt - -Scanner counted the following markers in proof-bearing files of this repo: - -``` -files= 13 | Coq-Axm/Adm= 0 | Lean-srry/ax= 0 | Agda-pst= 0 | Idr-blv= 6 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0 -``` - -**Total markers:** 6. **Severity:** `>06`. - -**Marker types** (any non-zero counts above): -- Coq `Axiom`/`Admitted` — unconditional proof escapes. -- Lean `sorry`/`axiom` — Lean's equivalent. -- Agda `postulate` — accepted axiomatically. -- Idris2 `believe_me`/`assert_total` — runtime-safe coercion / totality assumption. -- Idris2 top-level `partial` — totality-check waived. -- F\* `assume val`/`admit_p` — F\* admit. -- `TODO PROOF` / `OWED:` — self-documented debt markers. -- `unsafePerformIO`/`unsafeCoerce` — soundness-relevant escape hatches in Haskell/Rust source. - -**Recommended next move:** triage each finding into one of: (a) discharge by proof, (b) cover with property-tests + a documented refutation budget, or (c) annotate as a known/necessary axiom (e.g. `funExt`) in `docs/proof-debt.md`. - -## 2. Licence debt - -| Field | Value | -|---|---| -| LICENSE file | `LICENSE` | -| SPDX header | `PMPL-1.0-or-later` | -| Manifest licence | `NONE` | -| Body classifier | `PMPL-1.0-or-later` | -| Severity | `ok` | - -**Recommended next move:** none for licence. - -## 3. Documentation debt - -| Field | Value | -|---|---| -| README lines | 99 | -| `docs/` files | 55 | -| `docs/` LoC | 2261 | -| CHANGELOG.md | Y | -| CONTRIBUTING.md | Y | -| CODE_OF_CONDUCT.md | Y | -| SECURITY.md | Y | -| Severity | `OK` | - -**Recommended next move:** none for docs. - -## Cross-references - -- Estate proof-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-proof-debt.md` -- Estate licence-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-licence-debt.md` -- Estate documentation-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-documentation-debt.md` - ---- - -🤖 Generated by Claude Code estate-wide tech-debt scan (2026-05-26). This file is informational — closing the debt is follow-up work owned by the maintainer. diff --git a/llm-warmup-dev.adoc b/llm-warmup-dev.adoc new file mode 100644 index 0000000..e47a82c --- /dev/null +++ b/llm-warmup-dev.adoc @@ -0,0 +1,19 @@ +== LLM Warmup — rsr-template-repo (Developer) + +=== What is rsr-template-repo? + +See README.adoc for overview. + +=== Key Commands + +* `+just setup+` — set up development environment +* `+just build+` — build the project +* `+just test+` — run tests +* `+just doctor+` — diagnose issues +* `+just heal+` — attempt auto-repair + +=== Quick Context + +* License: 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 7f2ee64..0000000 --- a/llm-warmup-dev.md +++ /dev/null @@ -1,20 +0,0 @@ - -# LLM Warmup — rsr-template-repo (Developer) - -## What is rsr-template-repo? -See README.adoc for overview. - -## Key Commands -- `just setup` — set up development environment -- `just build` — build the project -- `just test` — run tests -- `just doctor` — diagnose issues -- `just heal` — attempt auto-repair - -## Quick Context -- License: 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 0000000..7d5d7e5 --- /dev/null +++ b/llm-warmup-user.adoc @@ -0,0 +1,19 @@ +== LLM Warmup — rsr-template-repo (User) + +=== What is rsr-template-repo? + +See README.adoc for overview. + +=== Key Commands + +* `+just setup+` — set up development environment +* `+just build+` — build the project +* `+just test+` — run tests +* `+just doctor+` — diagnose issues +* `+just heal+` — attempt auto-repair + +=== Quick Context + +* License: 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 1b55c1f..0000000 --- a/llm-warmup-user.md +++ /dev/null @@ -1,20 +0,0 @@ - -# LLM Warmup — rsr-template-repo (User) - -## What is rsr-template-repo? -See README.adoc for overview. - -## Key Commands -- `just setup` — set up development environment -- `just build` — build the project -- `just test` — run tests -- `just doctor` — diagnose issues -- `just heal` — attempt auto-repair - -## Quick Context -- License: PMPL-1.0-or-later -- Part of hyperpolymath ecosystem -- See EXPLAINME.adoc for architecture diff --git a/session/README.adoc b/session/README.adoc new file mode 100644 index 0000000..d14a6d7 --- /dev/null +++ b/session/README.adoc @@ -0,0 +1,45 @@ +== Session Bindings (Thin Local Layer) + +This directory provides local integration for central session-management +standards. + +Authoritative protocols live in: + +* `+../standards/session-management-standards/+` (or +`+$SESSION_STANDARDS_DIR+`) + +This repo keeps only thin bindings: + +* `+dispatch.sh+` maps canonical commands to central protocol paths. +* `+custom-checks.k9+` defines repo-local policy checks. +* `+local-hooks.sh+` provides optional repo-specific hook behavior. + +=== Canonical Commands + +* `+intake repo +` +* `+checkpoint change +` +* `+verify maintenance +` +* `+verify substantial +` +* `+verify release +` +* `+close planned +` +* `+close urgent +` +* `+recover repo +` +* `+handover full +` +* `+handover split +` +* `+handover model +` +* `+handover human +` + +=== Justfile Aliases + +Run `+just session-help+` to list aliases, then use recipes such as: + +* `+just intake-repo path=.+` +* `+just checkpoint-change path=.+` +* `+just verify-maintenance path=.+` +* `+just close-planned path=.+` +* `+just handover-model path=.+` + +=== Runtime Artifacts + +Runtime files are generated per repository in `+.session/+` and are not +canonical standards text. diff --git a/session/README.md b/session/README.md deleted file mode 100644 index ee83d59..0000000 --- a/session/README.md +++ /dev/null @@ -1,46 +0,0 @@ - -# Session Bindings (Thin Local Layer) - -This directory provides local integration for central session-management standards. - -Authoritative protocols live in: - -- `../standards/session-management-standards/` (or `$SESSION_STANDARDS_DIR`) - -This repo keeps only thin bindings: - -- `dispatch.sh` maps canonical commands to central protocol paths. -- `custom-checks.k9` defines repo-local policy checks. -- `local-hooks.sh` provides optional repo-specific hook behavior. - -## Canonical Commands - -- `intake repo ` -- `checkpoint change ` -- `verify maintenance ` -- `verify substantial ` -- `verify release ` -- `close planned ` -- `close urgent ` -- `recover repo ` -- `handover full ` -- `handover split ` -- `handover model ` -- `handover human ` - -## Justfile Aliases - -Run `just session-help` to list aliases, then use recipes such as: - -- `just intake-repo path=.` -- `just checkpoint-change path=.` -- `just verify-maintenance path=.` -- `just close-planned path=.` -- `just handover-model path=.` - -## Runtime Artifacts - -Runtime files are generated per repository in `.session/` and are not canonical standards text.