diff --git a/.github/CONTRIBUTING.md b/.github/CONTRIBUTING.md index 0bb99d2..b4fd385 100644 --- a/.github/CONTRIBUTING.md +++ b/.github/CONTRIBUTING.md @@ -2,8 +2,8 @@ git clone https://github.com/hyperpolymath/dafniser.git cd dafniser -# Using Nix (recommended for reproducibility) -nix develop +# Using Guix (recommended for reproducibility) +guix develop # Or using toolbox/distrobox toolbox create dafniser-dev @@ -45,7 +45,7 @@ dafniser/ ├── MAINTAINERS.md ├── README.adoc ├── SECURITY.md -├── flake.nix # Nix flake — fallback (Perimeter 1) +├── flake.guix # Guix flake — fallback (Perimeter 1) ├── guix.scm # Guix package — primary (Perimeter 1) └── Justfile # Task runner (Perimeter 1) ``` diff --git a/.github/copilot-instructions.md b/.github/copilot-instructions.md index 6e2bea9..678e4a4 100644 --- a/.github/copilot-instructions.md +++ b/.github/copilot-instructions.md @@ -33,7 +33,7 @@ ## Banned Languages -- No TypeScript (use ReScript) +- No TypeScript (use AffineScript) - No Node.js / npm / bun (use Deno) - No Go (use Rust) - No Python (use Julia or Rust) diff --git a/.github/dependabot.yml b/.github/dependabot.yml index d5cd4e9..045cb8f 100644 --- a/.github/dependabot.yml +++ b/.github/dependabot.yml @@ -41,8 +41,8 @@ updates: schedule: interval: "weekly" - # Nix flakes - - package-ecosystem: "nix" + # Guix flakes + - package-ecosystem: "guix" directory: "/" schedule: interval: "weekly" diff --git a/.machine_readable/ai/PLACEHOLDERS.adoc b/.machine_readable/ai/PLACEHOLDERS.adoc index 039ab9b..29b8081 100644 --- a/.machine_readable/ai/PLACEHOLDERS.adoc +++ b/.machine_readable/ai/PLACEHOLDERS.adoc @@ -48,8 +48,8 @@ sed -i "s/{{CURRENT_DATE}}/$(date +%Y-%m-%d)/g" $(grep -rl '{{CURRENT_DATE}}' .) | Placeholder | Description | Example | Files | |---|---|---|---| -| `{{PROJECT_NAME}}` | Human-readable project name | `My Project` | SECURITY.md, CODE_OF_CONDUCT.md, TOPOLOGY.md, STATE.a2ml, Justfile, GOVERNANCE.md, MAINTAINERS.md, flake.nix, devcontainer.json | -| `{{PROJECT_DESCRIPTION}}` | One-line description | `A tool for X` | flake.nix | +| `{{PROJECT_NAME}}` | Human-readable project name | `My Project` | SECURITY.md, CODE_OF_CONDUCT.md, TOPOLOGY.md, STATE.a2ml, Justfile, GOVERNANCE.md, MAINTAINERS.md, flake.guix, devcontainer.json | +| `{{PROJECT_DESCRIPTION}}` | One-line description | `A tool for X` | flake.guix | | `{{PROJECT}}` | Uppercase identifier (for Idris2 modules, C macros) | `MY_PROJECT` | ABI-FFI-README.md, src/interface/abi/*.idr, src/interface/ffi/*.zig | | `{{project}}` | Lowercase identifier (for C symbols, filenames) | `my_project` | ABI-FFI-README.md, src/interface/ffi/*.zig | | `dafniser` | Repository name (slug) | `my-project` | CONTRIBUTING.md, SECURITY.md, CODE_OF_CONDUCT.md, cliff.toml | @@ -133,7 +133,7 @@ After replacing all placeholders, verify none remain: ```bash grep -rn '{{' . --include='*.md' --include='*.adoc' --include='*.a2ml' \ --include='*.scm' --include='*.idr' --include='*.zig' --include='*.res' \ - --include='Justfile' --include='*.nix' --include='*.toml' --include='*.yml' \ + --include='Justfile' --include='*.guix' --include='*.toml' --include='*.yml' \ --include='*.yaml' --include='*.hs' --include='*.ncl' --include='*.txt' \ --include='*.json' --include='Containerfile' --include='dep5' \ | grep -v 'PLACEHOLDERS.md' | grep -v 'node_modules' diff --git a/.machine_readable/contractiles/lust/Intentfile.a2ml b/.machine_readable/contractiles/lust/Intentfile.a2ml index 9e53535..357b141 100644 --- a/.machine_readable/contractiles/lust/Intentfile.a2ml +++ b/.machine_readable/contractiles/lust/Intentfile.a2ml @@ -16,7 +16,7 @@ design philosophy — not current state, but target state. ### reproducible-builds - description: Builds should be bit-for-bit reproducible -- target: Guix + Nix + Containerfile +- target: Guix + Guix + Containerfile - status: aspiration ### zero-dangerous-patterns diff --git a/.machine_readable/policies/MAINTENANCE-CHECKLIST.a2ml b/.machine_readable/policies/MAINTENANCE-CHECKLIST.a2ml index eaee720..698f4d0 100644 --- a/.machine_readable/policies/MAINTENANCE-CHECKLIST.a2ml +++ b/.machine_readable/policies/MAINTENANCE-CHECKLIST.a2ml @@ -67,7 +67,7 @@ compliance-seams-check = true exception-register-required = true exception-bounded-scope-required = true policy-drift-contamination-check = true -example-drift-risk = "single TypeScript exception causing broad ReScript->TypeScript migration" +example-drift-risk = "single TypeScript exception causing broad AffineScript->TypeScript migration" compliance-tooling = "panic-attack" effects-tooling = "ecological checking with sustainabot guidance" diff --git a/CODE_OF_CONDUCT.adoc b/CODE_OF_CONDUCT.adoc new file mode 100644 index 0000000..bd2a83c --- /dev/null +++ b/CODE_OF_CONDUCT.adoc @@ -0,0 +1,24 @@ +== Contributor Covenant Code of Conduct + +=== Our Pledge + +We pledge to make participation a harassment-free experience for +everyone. + +=== Our Standards + +*Positive behavior:* * Using welcoming language * Being respectful of +differing viewpoints * Accepting constructive criticism * Focusing on +what is best for the community + +*Unacceptable behavior:* * Harassment, trolling, or personal attacks * +Publishing private information without permission + +=== Enforcement + +Report issues to the maintainers. All complaints will be reviewed. + +=== Attribution + +Adapted from https://www.contributor-covenant.org/[Contributor Covenant] +v2.1. diff --git a/CODE_OF_CONDUCT.md b/CODE_OF_CONDUCT.md deleted file mode 100644 index caeda1c..0000000 --- a/CODE_OF_CONDUCT.md +++ /dev/null @@ -1,27 +0,0 @@ - -# Contributor Covenant Code of Conduct - -## Our Pledge - -We pledge to make participation a harassment-free experience for everyone. - -## Our Standards - -**Positive behavior:** -* Using welcoming language -* Being respectful of differing viewpoints -* Accepting constructive criticism -* Focusing on what is best for the community - -**Unacceptable behavior:** -* Harassment, trolling, or personal attacks -* Publishing private information without permission - -## Enforcement - -Report issues to the maintainers. All complaints will be reviewed. - -## Attribution - -Adapted from [Contributor Covenant](https://www.contributor-covenant.org/) v2.1. - diff --git a/CONTRIBUTING.adoc b/CONTRIBUTING.adoc new file mode 100644 index 0000000..dd089ae --- /dev/null +++ b/CONTRIBUTING.adoc @@ -0,0 +1,71 @@ +== Contributing + +Thank you for your interest in contributing! We follow a "`Dual-Track`" +architecture where human-readable documentation lives in the root and +machine-readable policies live in `+.machine_readable/+`. + +=== How to Contribute + +We welcome contributions in many forms: + +* *Code:* Improving the core stack or extensions +* *Documentation:* Enhancing docs or AI manifests +* *Testing:* Adding property-based tests or formal proofs +* *Bug reports:* Filing clear, reproducible issues + +=== Getting Started + +[arabic] +. *Read the AI Manifest:* Start with `+0-AI-MANIFEST.a2ml+` (if present) +to understand the repository structure. +. *Environment:* Use `+guix develop+` or `+direnv allow+` to set up your +tools. +. *Task Runner:* Use `+just+` to see available commands +(`+just --list+`). + +=== Development Workflow + +==== Branch Naming + +.... +docs/short-description # Documentation +test/what-added # Test additions +feat/short-description # New features +fix/issue-number-description # Bug fixes +refactor/what-changed # Code improvements +security/what-fixed # Security fixes +.... + +==== Commit Messages + +We follow https://www.conventionalcommits.org/[Conventional Commits]: + +.... +(): + +[optional body] + +[optional footer] +.... + +Types: `+feat+`, `+fix+`, `+docs+`, `+test+`, `+refactor+`, `+ci+`, +`+chore+`, `+security+` + +=== Reporting Bugs + +Before reporting: 1. Search existing issues 2. Check if it’s already +fixed in `+main+` + +When reporting, include: - Clear, descriptive title - Environment +details (OS, versions, toolchain) - Steps to reproduce - Expected vs +actual behaviour + +=== Code of Conduct + +All contributors are expected to adhere to our +link:CODE_OF_CONDUCT.md[Code of Conduct]. + +=== License + +By contributing, you agree that your contributions will be licensed +under the same license as the project (see LICENSE). diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md deleted file mode 100644 index 80ecdac..0000000 --- a/CONTRIBUTING.md +++ /dev/null @@ -1,66 +0,0 @@ - -# Contributing - -Thank you for your interest in contributing! We follow a "Dual-Track" architecture where human-readable documentation lives in the root and machine-readable policies live in `.machine_readable/`. - -## How to Contribute - -We welcome contributions in many forms: - -- **Code:** Improving the core stack or extensions -- **Documentation:** Enhancing docs or AI manifests -- **Testing:** Adding property-based tests or formal proofs -- **Bug reports:** Filing clear, reproducible issues - -## Getting Started - -1. **Read the AI Manifest:** Start with `0-AI-MANIFEST.a2ml` (if present) to understand the repository structure. -2. **Environment:** Use `nix develop` or `direnv allow` to set up your tools. -3. **Task Runner:** Use `just` to see available commands (`just --list`). - -## Development Workflow - -### Branch Naming - -``` -docs/short-description # Documentation -test/what-added # Test additions -feat/short-description # New features -fix/issue-number-description # Bug fixes -refactor/what-changed # Code improvements -security/what-fixed # Security fixes -``` - -### Commit Messages - -We follow [Conventional Commits](https://www.conventionalcommits.org/): - -``` -(): - -[optional body] - -[optional footer] -``` - -Types: `feat`, `fix`, `docs`, `test`, `refactor`, `ci`, `chore`, `security` - -## Reporting Bugs - -Before reporting: -1. Search existing issues -2. Check if it's already fixed in `main` - -When reporting, include: -- Clear, descriptive title -- Environment details (OS, versions, toolchain) -- Steps to reproduce -- Expected vs actual behaviour - -## Code of Conduct - -All contributors are expected to adhere to our [Code of Conduct](CODE_OF_CONDUCT.md). - -## License - -By contributing, you agree that your contributions will be licensed under the same license as the project (see [LICENSE](LICENSE)). diff --git a/README.adoc b/README.adoc new file mode 100644 index 0000000..7b1f94c --- /dev/null +++ b/README.adoc @@ -0,0 +1,131 @@ +https://github.com/sponsors/hyperpolymath[image:https://img.shields.io/badge/Sponsor-%E2%9D%A4-pink?logo=github[Sponsor]] + +== What Is This? + +Dafniser generates *correct-by-construction code* for critical functions +using https://dafny.org[Dafny], the verification-aware language created +by Rustan Leino (originally at Microsoft Research). + +Dafny programs carry formal specifications — `+requires+` / `+ensures+` +clauses, loop invariants, `+decreases+` annotations, ghost variables, +and lemmas — that an SMT solver (Z3) proves at compile time. Dafny then +compiles the verified source to C#, Java, Go, Python, or JavaScript. + +Nobody outside research groups writes Dafny by hand. Dafniser makes +verified code generation accessible: write specifications, get provably +correct implementations. + +== How It Works + +.... +dafniser.toml (specs) ← you write this + │ + ▼ +Spec extraction & validation ← Rust CLI parses pre/postconditions + │ + ▼ +Idris2 ABI meta-proofs ← proves spec consistency (Types, Layout, Foreign) + │ + ▼ +Dafny code generation ← requires/ensures, loop invariants, ghost vars, lemmas + │ + ▼ +Z3 verification ← SMT solver proves every contract + │ + ▼ +Target compilation ← Dafny → C# / Java / Go / Python / JavaScript + │ + ▼ +Zig FFI bridge ← C-ABI integration with your existing codebase +.... + +[arabic] +. Describe critical functions in `+dafniser.toml+` with preconditions, +postconditions, and optional invariants. +. Dafniser generates Dafny source with `+requires+` / `+ensures+` +contracts, `+decreases+` termination measures, ghost variables, and +supporting lemmas. +. Z3 verifies every contract at compile time — if verification fails, +you get a precise counterexample, not a runtime crash. +. The verified Dafny compiles to your chosen target language. +. A Zig FFI bridge wraps the compiled output for C-ABI integration. + +== Key Value + +* *Proven-correct code* — Z3 proves every pre/postcondition at compile +time +* *Auto-generated from specifications* — no manual Dafny authorship +required +* *Multiple output languages* — verified code in C#, Java, Go, Python, +JavaScript +* *Formal meta-proofs* — Idris2 dependent types verify spec consistency +before codegen +* *Refinement support* — layer abstract specs into concrete +implementations with proof + +== Use Cases + +Sorting and searching algorithms + +Verified implementations of quicksort, binary search, merge sort with +proved bounds and termination. + +Cryptographic primitives + +Constant-time comparisons, key derivation, hashing wrappers with proved +absence of timing side-channels (within Dafny’s model). + +Financial algorithms + +Interest calculations, rounding, settlement logic with proved +monotonicity and conservation-of-value properties. + +Consensus protocols + +Leader election, quorum logic, state machine replication steps with +proved safety invariants. + +Safety-critical control logic + +State machines with proved liveness and deadlock-freedom properties. + +== Dafny Specifics + +Dafniser generates and manages these Dafny constructs: + +* *`+requires+` / `+ensures+`* — preconditions and postconditions on +every method +* *`+decreases+`* — termination metrics for recursive functions and +loops +* *`+invariant+`* — loop invariants that hold on every iteration +* *`+ghost+`* — specification-only variables that vanish at compilation +* *`+lemma+`* — proof obligations discharged by Z3 to establish complex +properties +* *`+refines+`* — layered module refinement from abstract to concrete + +== Architecture + +Follows the hyperpolymath -iser pattern (same as +https://github.com/hyperpolymath/chapeliser[Chapeliser]): + +* *Manifest* (`+dafniser.toml+`) — declare WHAT you need: function +signatures, preconditions, postconditions, invariants, target language +* *Idris2 ABI* (`+src/interface/abi/+`) — formal proofs that +specifications are internally consistent (type-safe, non-contradictory, +well-scoped) +* *Zig FFI* (`+src/interface/ffi/+`) — C-ABI bridge to compiled Dafny +output +* *Codegen* (`+src/codegen/+`) — generates Dafny source with full +verification annotations +* *Rust CLI* — parses manifest, validates specs, invokes Dafny compiler +and Z3 + +User writes zero Dafny. Dafniser generates everything. + +Part of the https://github.com/hyperpolymath/iseriser[-iser family] of +acceleration frameworks. + +== Status + +*Pre-alpha / codebase in progress.* Architecture defined, CLI +scaffolded, ABI stubs in place. Dafny codegen and Z3 verification +integration pending. + +== License + +SPDX-License-Identifier: CC-BY-SA-4.0 diff --git a/README.md b/README.md deleted file mode 100644 index 7a0a19f..0000000 --- a/README.md +++ /dev/null @@ -1,150 +0,0 @@ - - -[![Sponsor](https://img.shields.io/badge/Sponsor-%E2%9D%A4-pink?logo=github)](https://github.com/sponsors/hyperpolymath) - -# What Is This? - -Dafniser generates **correct-by-construction code** for critical -functions using [Dafny](https://dafny.org), the verification-aware -language created by Rustan Leino (originally at Microsoft Research). - -Dafny programs carry formal specifications — `requires` / `ensures` -clauses, loop invariants, `decreases` annotations, ghost variables, and -lemmas — that an SMT solver (Z3) proves at compile time. Dafny then -compiles the verified source to C#, Java, Go, Python, or JavaScript. - -Nobody outside research groups writes Dafny by hand. Dafniser makes -verified code generation accessible: write specifications, get provably -correct implementations. - -# How It Works - - dafniser.toml (specs) ← you write this - │ - ▼ - Spec extraction & validation ← Rust CLI parses pre/postconditions - │ - ▼ - Idris2 ABI meta-proofs ← proves spec consistency (Types, Layout, Foreign) - │ - ▼ - Dafny code generation ← requires/ensures, loop invariants, ghost vars, lemmas - │ - ▼ - Z3 verification ← SMT solver proves every contract - │ - ▼ - Target compilation ← Dafny → C# / Java / Go / Python / JavaScript - │ - ▼ - Zig FFI bridge ← C-ABI integration with your existing codebase - -1. Describe critical functions in `dafniser.toml` with preconditions, - postconditions, and optional invariants. - -2. Dafniser generates Dafny source with `requires` / `ensures` - contracts, `decreases` termination measures, ghost variables, and - supporting lemmas. - -3. Z3 verifies every contract at compile time — if verification fails, - you get a precise counterexample, not a runtime crash. - -4. The verified Dafny compiles to your chosen target language. - -5. A Zig FFI bridge wraps the compiled output for C-ABI integration. - -# Key Value - -- **Proven-correct code** — Z3 proves every pre/postcondition at compile - time - -- **Auto-generated from specifications** — no manual Dafny authorship - required - -- **Multiple output languages** — verified code in C#, Java, Go, Python, - JavaScript - -- **Formal meta-proofs** — Idris2 dependent types verify spec - consistency before codegen - -- **Refinement support** — layer abstract specs into concrete - implementations with proof - -# Use Cases - -Sorting and searching algorithms -Verified implementations of quicksort, binary search, merge sort with -proved bounds and termination. - -Cryptographic primitives -Constant-time comparisons, key derivation, hashing wrappers with proved -absence of timing side-channels (within Dafny’s model). - -Financial algorithms -Interest calculations, rounding, settlement logic with proved -monotonicity and conservation-of-value properties. - -Consensus protocols -Leader election, quorum logic, state machine replication steps with -proved safety invariants. - -Safety-critical control logic -State machines with proved liveness and deadlock-freedom properties. - -# Dafny Specifics - -Dafniser generates and manages these Dafny constructs: - -- **`requires` / `ensures`** — preconditions and postconditions on every - method - -- **`decreases`** — termination metrics for recursive functions and - loops - -- **`invariant`** — loop invariants that hold on every iteration - -- **`ghost`** — specification-only variables that vanish at compilation - -- **`lemma`** — proof obligations discharged by Z3 to establish complex - properties - -- **`refines`** — layered module refinement from abstract to concrete - -# Architecture - -Follows the hyperpolymath -iser pattern (same as -[Chapeliser](https://github.com/hyperpolymath/chapeliser)): - -- **Manifest** (`dafniser.toml`) — declare WHAT you need: function - signatures, preconditions, postconditions, invariants, target language - -- **Idris2 ABI** (`src/interface/abi/`) — formal proofs that - specifications are internally consistent (type-safe, - non-contradictory, well-scoped) - -- **Zig FFI** (`src/interface/ffi/`) — C-ABI bridge to compiled Dafny - output - -- **Codegen** (`src/codegen/`) — generates Dafny source with full - verification annotations - -- **Rust CLI** — parses manifest, validates specs, invokes Dafny - compiler and Z3 - -User writes zero Dafny. Dafniser generates everything. - -Part of the [-iser family](https://github.com/hyperpolymath/iseriser) of -acceleration frameworks. - -# Status - -**Pre-alpha / codebase in progress.** Architecture defined, CLI -scaffolded, ABI stubs in place. Dafny codegen and Z3 verification -integration pending. - -# License - -SPDX-License-Identifier: CC-BY-SA-4.0 diff --git a/SECURITY.md b/SECURITY.adoc similarity index 57% rename from SECURITY.md rename to SECURITY.adoc index e1e6775..d06315b 100644 --- a/SECURITY.md +++ b/SECURITY.adoc @@ -1,21 +1,24 @@ -# Security Policy +== Security Policy -## Supported Versions +=== Supported Versions -| Version | Supported | -|---------|-----------| -| 0.1.x | ✅ | +[cols=",",options="header",] +|=== +|Version |Supported +|0.1.x |✅ +|=== -## Reporting a Vulnerability +=== Reporting a Vulnerability Please report security vulnerabilities to: j.d.a.jewell@open.ac.uk Do NOT open a public issue for security vulnerabilities. -## Response Time +=== Response Time -We aim to respond within 48 hours and provide a fix within 7 days for critical issues. +We aim to respond within 48 hours and provide a fix within 7 days for +critical issues. -## Scope +=== Scope This policy covers the dafniser CLI tool and its generated artifacts. diff --git a/TEST-NEEDS.adoc b/TEST-NEEDS.adoc new file mode 100644 index 0000000..1933bdd --- /dev/null +++ b/TEST-NEEDS.adoc @@ -0,0 +1,34 @@ +== TEST-NEEDS.md — dafniser + +=== CRG Grade: C — ACHIEVED 2026-04-04 + +=== Current Test State + +[cols=",,",options="header",] +|=== +|Category |Count |Notes +|Test directories |2 |Location(s): /tests, /verification/tests +|CI workflows |22 |Running tests on GitHub Actions +|Unit tests |Built-in |Rust/cargo test framework +|Integration tests |Configured |Via integration/ directory +|=== + +=== What’s Covered + +* [x] Rust unit test suite (cargo test) +* [x] Documentation tests +* [x] Example programs with tests + +=== Still Missing (for CRG B+) + +* [ ] Code coverage reports (codecov integration) +* [ ] Detailed test documentation in CONTRIBUTING.md +* [ ] Integration tests beyond unit tests +* [ ] Performance benchmarking suite + +=== Run Tests + +[source,bash] +---- +cargo test +---- diff --git a/TEST-NEEDS.md b/TEST-NEEDS.md deleted file mode 100644 index 99e8902..0000000 --- a/TEST-NEEDS.md +++ /dev/null @@ -1,31 +0,0 @@ -# TEST-NEEDS.md — dafniser - -## CRG Grade: C — ACHIEVED 2026-04-04 - -## Current Test State - -| Category | Count | Notes | -|----------|-------|-------| -| Test directories | 2 | Location(s): /tests, /verification/tests | -| CI workflows | 22 | Running tests on GitHub Actions | -| Unit tests | Built-in | Rust/cargo test framework | -| Integration tests | Configured | Via integration/ directory | - -## What's Covered - -- [x] Rust unit test suite (cargo test) -- [x] Documentation tests -- [x] Example programs with tests - -## Still Missing (for CRG B+) - -- [ ] Code coverage reports (codecov integration) -- [ ] Detailed test documentation in CONTRIBUTING.md -- [ ] Integration tests beyond unit tests -- [ ] Performance benchmarking suite - -## Run Tests - -```bash -cargo test -``` diff --git a/TOPOLOGY.md b/TOPOLOGY.adoc similarity index 68% rename from TOPOLOGY.md rename to TOPOLOGY.adoc index f6b1eaf..1d0373c 100644 --- a/TOPOLOGY.md +++ b/TOPOLOGY.adoc @@ -1,14 +1,19 @@ - - -# TOPOLOGY.md — dafniser +== TOPOLOGY.md — dafniser -## Purpose +=== Purpose -dafniser generates correct-by-construction code via Dafny verification. It reads function specifications — preconditions, postconditions, loop invariants, and decreases clauses — from a `dafniser.toml` manifest and emits Dafny `.dfy` source files. Dafny's Z3-backed verifier automatically proves correctness of the generated code, which is then compiled to a target language (C#, Java, Go, Python, or JavaScript). dafniser targets developers who want machine-checked guarantees for critical functions without writing Dafny by hand. +dafniser generates correct-by-construction code via Dafny verification. +It reads function specifications — preconditions, postconditions, loop +invariants, and decreases clauses — from a `+dafniser.toml+` manifest +and emits Dafny `+.dfy+` source files. Dafny’s Z3-backed verifier +automatically proves correctness of the generated code, which is then +compiled to a target language (C#, Java, Go, Python, or JavaScript). +dafniser targets developers who want machine-checked guarantees for +critical functions without writing Dafny by hand. -## Module Map +=== Module Map -``` +.... dafniser/ ├── src/ │ ├── main.rs # CLI entry point (clap): init, validate, generate, build, run, info @@ -20,11 +25,11 @@ dafniser/ ├── verification/ # Proof harnesses ├── container/ # Stapeln container ecosystem └── .machine_readable/ # A2ML metadata -``` +.... -## Data Flow +=== Data Flow -``` +.... dafniser.toml manifest │ ┌────▼────┐ @@ -43,4 +48,4 @@ dafniser.toml manifest ┌────▼────┐ │ Dafny │ Z3-backed verifier proves correctness → compile to target language └─────────┘ -``` +.... diff --git a/docs/RSR_OUTLINE.adoc b/docs/RSR_OUTLINE.adoc index 8faf3bb..83e1c15 100644 --- a/docs/RSR_OUTLINE.adoc +++ b/docs/RSR_OUTLINE.adoc @@ -204,8 +204,8 @@ project/ === Language Tiers -* **Tier 1** (Gold): Rust, Elixir, Zig, Ada, Haskell, ReScript, Gleam -* **Tier 2** (Silver): Nickel, Guile Scheme, Nix, Idris2, OCaml +* **Tier 1** (Gold): Rust, Elixir, Zig, Ada, Haskell, AffineScript, Gleam +* **Tier 2** (Silver): Nickel, Guile Scheme, Guix, Idris2, OCaml * **Infrastructure**: Guix channels, derivations, Julia batch scripts === Required Files @@ -219,12 +219,12 @@ project/ * `.well-known/security.txt` * `.well-known/ai.txt` * `.well-known/humans.txt` -* `guix.scm` OR `flake.nix` +* `guix.scm` OR `flake.guix` === Prohibited * Python outside `salt/` directory -* TypeScript/JavaScript (use ReScript) +* TypeScript/JavaScript (use AffineScript) * CUE (use Guile/Nickel) * `Dockerfile` (use `Containerfile`) * npm, Bun, pnpm, yarn (use Deno) diff --git a/docs/STATE-VISUALIZER.adoc b/docs/STATE-VISUALIZER.adoc index 4be8d44..7746b12 100644 --- a/docs/STATE-VISUALIZER.adoc +++ b/docs/STATE-VISUALIZER.adoc @@ -46,7 +46,7 @@ ┌─────────────────────────────────────────┐ │ PLATFORM INTEGRATION │ │ ┌───────────┐ ┌───────────┐ ┌───────┐│ - │ │ GitHub │ │ GitLab │ │ Nix / ││ + │ │ GitHub │ │ GitLab │ │ Guix / ││ │ │ Workflows │ │ CI/CD │ │ Guix ││ │ └───────────┘ └───────────┘ └───────┘│ └─────────────────────────────────────────┘ @@ -88,7 +88,7 @@ CONTAINER ECOSYSTEM (Phase 2) REPO INFRASTRUCTURE .machine_readable/ ██████████ 100% STATE/META/ECOSYSTEM active Governance & License ██████████ 100% MPL-2.0 & Ethical use verified - Development Shells (Nix/Guix) ██████████ 100% Reproducible env stable + Development Shells (Guix/Guix) ██████████ 100% Reproducible env stable ───────────────────────────────────────────────────────────────────────────── OVERALL: ██████████ 100% RSR Template Stable & Certified diff --git a/docs/architecture/TOPOLOGY.adoc b/docs/architecture/TOPOLOGY.adoc new file mode 100644 index 0000000..709b4f1 --- /dev/null +++ b/docs/architecture/TOPOLOGY.adoc @@ -0,0 +1,136 @@ +== SPDX-License-Identifier: CC-BY-SA-4.0 + +== Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) j.d.a.jewell@open.ac.uk + +== + +== TOPOLOGY.md — Dafniser module topology and data flow + +=== Overview + +Dafniser transforms function specifications (pre/postconditions, +invariants) into verified Dafny implementations, proves them via Z3, and +compiles to target languages with a Zig FFI bridge. + +=== Data Flow + +.... +dafniser.toml + │ + ├─► [Manifest Parser] (src/manifest/) + │ │ + │ ▼ + │ SpecTree { functions, preconditions, postconditions, + │ invariants, ghost_vars, lemma_hints } + │ │ + │ ├─► [Idris2 ABI] (src/interface/abi/) + │ │ │ + │ │ ▼ + │ │ Meta-proofs: spec consistency, termination, + │ │ ghost scoping, refinement monotonicity + │ │ │ + │ │ ▼ + │ │ C headers (src/interface/generated/abi/) + │ │ + │ └─► [Dafny Codegen] (src/codegen/) + │ │ + │ ▼ + │ .dfy files with requires/ensures/invariant/ + │ decreases/ghost/lemma annotations + │ │ + │ ▼ + │ [Dafny Compiler + Z3] + │ │ + │ ├─► Verification result (pass / counterexample) + │ │ + │ └─► Target language output (C#/Java/Go/Python/JS) + │ │ + │ ▼ + │ [Zig FFI Bridge] (src/interface/ffi/) + │ │ + │ ▼ + │ C-ABI shared library (libdafniser.so/.dylib/.dll) + │ + └─► [CLI] (src/main.rs) + Subcommands: init, validate, generate, build, run, info +.... + +=== Module Map + +[width="100%",cols="35%,26%,39%",options="header",] +|=== +|Module |Path |Purpose +|CLI |`+src/main.rs+` |Command dispatch, argument parsing + +|Library API |`+src/lib.rs+` |Public API for programmatic use + +|Manifest |`+src/manifest/+` |TOML parsing, spec extraction, validation + +|Codegen |`+src/codegen/+` |Dafny source generation with verification +annotations + +|ABI Types |`+src/interface/abi/Types.idr+` |Precondition, +Postcondition, LoopInvariant, GhostVariable, Lemma, VerificationResult + +|ABI Layout |`+src/interface/abi/Layout.idr+` |Spec tree memory layout, +field alignment proofs + +|ABI Foreign |`+src/interface/abi/Foreign.idr+` |FFI declarations for +Dafny compilation and Z3 invocation + +|FFI Impl |`+src/interface/ffi/src/main.zig+` |C-ABI implementation of +Foreign.idr declarations + +|FFI Build |`+src/interface/ffi/build.zig+` |Zig build configuration +(shared + static libs) + +|FFI Tests |`+src/interface/ffi/test/integration_test.zig+` |ABI +compliance integration tests + +|Generated |`+src/interface/generated/abi/+` |Auto-generated C headers +from Idris2 ABI +|=== + +=== External Dependencies + +[width="100%",cols="44%,21%,35%",options="header",] +|=== +|Dependency |Role |Required +|Dafny |Verification-aware language compiler |Yes (Phase 2+) +|Z3 |SMT solver backend for Dafny |Yes (Phase 3+) +|.NET / Java / Go / Python / Node |Target language runtimes |Per target +|Idris2 |ABI formal proofs |Yes (Phase 5+) +|Zig |FFI bridge compilation |Yes (Phase 4+) +|=== + +=== Key Types (Idris2 ABI) + +[width="100%",cols="40%,60%",options="header",] +|=== +|Type |Purpose +|`+Precondition+` |A `+requires+` clause bound to a function + +|`+Postcondition+` |An `+ensures+` clause bound to a function + +|`+LoopInvariant+` |An `+invariant+` annotation on a loop + +|`+GhostVariable+` |A specification-only variable (erased at +compilation) + +|`+Lemma+` |A proof obligation discharged by Z3 + +|`+VerificationResult+` |Outcome of Z3 verification (Verified / +Counterexample / Timeout) + +|`+SpecTree+` |Complete specification tree extracted from manifest +|=== + +=== Verification Pipeline + +[arabic] +. *Parse*: TOML manifest -> SpecTree (Rust) +. *Meta-prove*: SpecTree -> Idris2 ABI consistency proofs +. *Generate*: SpecTree -> .dfy source files +. *Verify*: .dfy -> Z3 -> VerificationResult +. *Compile*: verified .dfy -> target language source +. *Bridge*: target source -> Zig FFI -> C-ABI shared library diff --git a/docs/architecture/TOPOLOGY.md b/docs/architecture/TOPOLOGY.md deleted file mode 100644 index 6f32732..0000000 --- a/docs/architecture/TOPOLOGY.md +++ /dev/null @@ -1,100 +0,0 @@ -# SPDX-License-Identifier: CC-BY-SA-4.0 -# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -# -# TOPOLOGY.md — Dafniser module topology and data flow - -## Overview - -Dafniser transforms function specifications (pre/postconditions, invariants) -into verified Dafny implementations, proves them via Z3, and compiles to -target languages with a Zig FFI bridge. - -## Data Flow - -``` -dafniser.toml - │ - ├─► [Manifest Parser] (src/manifest/) - │ │ - │ ▼ - │ SpecTree { functions, preconditions, postconditions, - │ invariants, ghost_vars, lemma_hints } - │ │ - │ ├─► [Idris2 ABI] (src/interface/abi/) - │ │ │ - │ │ ▼ - │ │ Meta-proofs: spec consistency, termination, - │ │ ghost scoping, refinement monotonicity - │ │ │ - │ │ ▼ - │ │ C headers (src/interface/generated/abi/) - │ │ - │ └─► [Dafny Codegen] (src/codegen/) - │ │ - │ ▼ - │ .dfy files with requires/ensures/invariant/ - │ decreases/ghost/lemma annotations - │ │ - │ ▼ - │ [Dafny Compiler + Z3] - │ │ - │ ├─► Verification result (pass / counterexample) - │ │ - │ └─► Target language output (C#/Java/Go/Python/JS) - │ │ - │ ▼ - │ [Zig FFI Bridge] (src/interface/ffi/) - │ │ - │ ▼ - │ C-ABI shared library (libdafniser.so/.dylib/.dll) - │ - └─► [CLI] (src/main.rs) - Subcommands: init, validate, generate, build, run, info -``` - -## Module Map - -| Module | Path | Purpose | -|--------|------|---------| -| CLI | `src/main.rs` | Command dispatch, argument parsing | -| Library API | `src/lib.rs` | Public API for programmatic use | -| Manifest | `src/manifest/` | TOML parsing, spec extraction, validation | -| Codegen | `src/codegen/` | Dafny source generation with verification annotations | -| ABI Types | `src/interface/abi/Types.idr` | Precondition, Postcondition, LoopInvariant, GhostVariable, Lemma, VerificationResult | -| ABI Layout | `src/interface/abi/Layout.idr` | Spec tree memory layout, field alignment proofs | -| ABI Foreign | `src/interface/abi/Foreign.idr` | FFI declarations for Dafny compilation and Z3 invocation | -| FFI Impl | `src/interface/ffi/src/main.zig` | C-ABI implementation of Foreign.idr declarations | -| FFI Build | `src/interface/ffi/build.zig` | Zig build configuration (shared + static libs) | -| FFI Tests | `src/interface/ffi/test/integration_test.zig` | ABI compliance integration tests | -| Generated | `src/interface/generated/abi/` | Auto-generated C headers from Idris2 ABI | - -## External Dependencies - -| Dependency | Role | Required | -|------------|------|----------| -| Dafny | Verification-aware language compiler | Yes (Phase 2+) | -| Z3 | SMT solver backend for Dafny | Yes (Phase 3+) | -| .NET / Java / Go / Python / Node | Target language runtimes | Per target | -| Idris2 | ABI formal proofs | Yes (Phase 5+) | -| Zig | FFI bridge compilation | Yes (Phase 4+) | - -## Key Types (Idris2 ABI) - -| Type | Purpose | -|------|---------| -| `Precondition` | A `requires` clause bound to a function | -| `Postcondition` | An `ensures` clause bound to a function | -| `LoopInvariant` | An `invariant` annotation on a loop | -| `GhostVariable` | A specification-only variable (erased at compilation) | -| `Lemma` | A proof obligation discharged by Z3 | -| `VerificationResult` | Outcome of Z3 verification (Verified / Counterexample / Timeout) | -| `SpecTree` | Complete specification tree extracted from manifest | - -## Verification Pipeline - -1. **Parse**: TOML manifest -> SpecTree (Rust) -2. **Meta-prove**: SpecTree -> Idris2 ABI consistency proofs -3. **Generate**: SpecTree -> .dfy source files -4. **Verify**: .dfy -> Z3 -> VerificationResult -5. **Compile**: verified .dfy -> target language source -6. **Bridge**: target source -> Zig FFI -> C-ABI shared library diff --git a/docs/developer/ABI-FFI-README.adoc b/docs/developer/ABI-FFI-README.adoc index fe01f12..dd5db7a 100644 --- a/docs/developer/ABI-FFI-README.adoc +++ b/docs/developer/ABI-FFI-README.adoc @@ -44,7 +44,7 @@ This library follows the **Hyperpolymath RSR Standard** for ABI and FFI design: ▼ ┌─────────────────────────────────────────────┐ │ Any Language via C ABI │ -│ - Rust, ReScript, Julia, Python, etc. │ +│ - Rust, AffineScript, Julia, Python, etc. │ └─────────────────────────────────────────────┘ ``` @@ -76,7 +76,7 @@ This library follows the **Hyperpolymath RSR Standard** for ABI and FFI design: │ └── bindings/ # Language-specific wrappers (optional) ├── rust/ - ├── rescript/ + ├── affinescript/ └── julia/ ``` diff --git a/docs/governance/MAINTENANCE-CHECKLIST.a2ml b/docs/governance/MAINTENANCE-CHECKLIST.a2ml index eaee720..698f4d0 100644 --- a/docs/governance/MAINTENANCE-CHECKLIST.a2ml +++ b/docs/governance/MAINTENANCE-CHECKLIST.a2ml @@ -67,7 +67,7 @@ compliance-seams-check = true exception-register-required = true exception-bounded-scope-required = true policy-drift-contamination-check = true -example-drift-risk = "single TypeScript exception causing broad ReScript->TypeScript migration" +example-drift-risk = "single TypeScript exception causing broad AffineScript->TypeScript migration" compliance-tooling = "panic-attack" effects-tooling = "ecological checking with sustainabot guidance" diff --git a/docs/practice/AI-CONVENTIONS.adoc b/docs/practice/AI-CONVENTIONS.adoc index 58e132b..6a3636b 100644 --- a/docs/practice/AI-CONVENTIONS.adoc +++ b/docs/practice/AI-CONVENTIONS.adoc @@ -53,7 +53,7 @@ MAINTENANCE-CHECKLIST.a2ml, or SOFTWARE-DEVELOPMENT-APPROACH.a2ml in the reposit | Banned | Use Instead | |---------------------|--------------------| -| TypeScript | ReScript | +| TypeScript | AffineScript | | Node.js / npm / bun | Deno | | Go | Rust | | Python | Julia / Rust | diff --git a/examples/web-project-deno.json b/examples/web-project-deno.json index 5ddd3bd..ee775a4 100644 --- a/examples/web-project-deno.json +++ b/examples/web-project-deno.json @@ -1,17 +1,17 @@ { - "// NOTE": "Example deno.json for ReScript web projects", + "// NOTE": "Example deno.json for AffineScript web projects", "tasks": { - "build": "deno run -A npm:rescript", - "clean": "deno run -A npm:rescript clean", - "watch": "deno run -A npm:rescript -w", + "build": "deno run -A npm:affinescript", + "clean": "deno run -A npm:affinescript clean", + "watch": "deno run -A npm:affinescript -w", "serve": "deno run -A jsr:@std/http/file-server .", "test": "deno test --allow-all" }, "imports": { - "rescript": "^12.0.0", - "@rescript/core": "npm:@rescript/core@^1.6.0", - "safe-dom/": "https://raw.githubusercontent.com/hyperpolymath/rescript-dom-mounter/main/src/", - "proven/": "../proven/bindings/rescript/src/" + "affinescript": "^12.0.0", + "@affinescript/core": "npm:@affinescript/core@^1.6.0", + "safe-dom/": "https://raw.githubusercontent.com/hyperpolymath/affinescript-dom-mounter/main/src/", + "proven/": "../proven/bindings/affinescript/src/" }, "compilerOptions": { "allowJs": true, diff --git a/llm-warmup-dev.adoc b/llm-warmup-dev.adoc new file mode 100644 index 0000000..97ff128 --- /dev/null +++ b/llm-warmup-dev.adoc @@ -0,0 +1,19 @@ +== LLM Warmup — dafniser (Developer) + +=== What is dafniser? + +See README.adoc for overview. + +=== Key Commands + +* `+just setup+` — set up development environment +* `+just build+` — build the project +* `+just test+` — run tests +* `+just doctor+` — diagnose issues +* `+just heal+` — attempt auto-repair + +=== Quick Context + +* License: MPL-2.0 +* Part of hyperpolymath ecosystem +* See EXPLAINME.adoc for architecture diff --git a/llm-warmup-dev.md b/llm-warmup-dev.md deleted file mode 100644 index 6bde7b6..0000000 --- a/llm-warmup-dev.md +++ /dev/null @@ -1,16 +0,0 @@ -# LLM Warmup — dafniser (Developer) - -## What is dafniser? -See README.adoc for overview. - -## Key Commands -- `just setup` — set up development environment -- `just build` — build the project -- `just test` — run tests -- `just doctor` — diagnose issues -- `just heal` — attempt auto-repair - -## Quick Context -- License: MPL-2.0 -- Part of hyperpolymath ecosystem -- See EXPLAINME.adoc for architecture diff --git a/llm-warmup-user.adoc b/llm-warmup-user.adoc new file mode 100644 index 0000000..d8e675e --- /dev/null +++ b/llm-warmup-user.adoc @@ -0,0 +1,19 @@ +== LLM Warmup — dafniser (User) + +=== What is dafniser? + +See README.adoc for overview. + +=== Key Commands + +* `+just setup+` — set up development environment +* `+just build+` — build the project +* `+just test+` — run tests +* `+just doctor+` — diagnose issues +* `+just heal+` — attempt auto-repair + +=== Quick Context + +* License: MPL-2.0 +* Part of hyperpolymath ecosystem +* See EXPLAINME.adoc for architecture diff --git a/llm-warmup-user.md b/llm-warmup-user.md deleted file mode 100644 index 68f203f..0000000 --- a/llm-warmup-user.md +++ /dev/null @@ -1,16 +0,0 @@ -# LLM Warmup — dafniser (User) - -## What is dafniser? -See README.adoc for overview. - -## Key Commands -- `just setup` — set up development environment -- `just build` — build the project -- `just test` — run tests -- `just doctor` — diagnose issues -- `just heal` — attempt auto-repair - -## Quick Context -- License: MPL-2.0 -- Part of hyperpolymath ecosystem -- See EXPLAINME.adoc for architecture