diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md index 218ffc2..064d91a 100644 --- a/.claude/CLAUDE.md +++ b/.claude/CLAUDE.md @@ -24,7 +24,7 @@ | Banned | Replacement | |--------|-------------| -| ReScript | AffineScript | +| AffineScript | AffineScript | | TypeScript | AffineScript | | Node.js | Deno | | npm | Deno | @@ -48,7 +48,7 @@ Both are FOSS with independent governance (no Big Tech). ### Enforcement Rules -1. **No new ReScript files** - Port existing .res to AffineScript (.affine) +1. **No new AffineScript files** - Port existing .res to AffineScript (.affine) 2. **No new TypeScript files** - Convert existing TS to AffineScript 3. **No package.json for runtime deps** - Use deno.json imports 4. **No node_modules in production** - Deno caches deps automatically @@ -59,7 +59,7 @@ Both are FOSS with independent governance (no Big Tech). ### Package Management - **Primary**: Guix (guix.scm) -- **Fallback**: Nix (flake.nix) +- **Fallback**: Guix (flake.guix) - **JS deps**: Deno (deno.json imports) ### Security Requirements diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 1c95bde..0f96d60 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -25,7 +25,7 @@ rsr-compliance: script: - | echo "Checking RSR compliance..." - files="README.md LICENSE SECURITY.md CODE_OF_CONDUCT.md CONTRIBUTING.md GOVERNANCE.md CHANGELOG.md MAINTAINERS.md FUNDING.yml flake.nix Justfile" + files="README.md LICENSE SECURITY.md CODE_OF_CONDUCT.md CONTRIBUTING.md GOVERNANCE.md CHANGELOG.md MAINTAINERS.md FUNDING.yml flake.guix Justfile" for file in $files; do if [ -f "$file" ]; then echo "✓ $file" diff --git a/ABI-FFI-README.adoc b/ABI-FFI-README.adoc new file mode 100644 index 0000000..8be89d3 --- /dev/null +++ b/ABI-FFI-README.adoc @@ -0,0 +1,141 @@ +== Axiom.jl ABI / FFI Notes + +This file documents the current ABI/FFI split for Axiom.jl. + +=== Idris2 ABI Scaffold (illustrative, not the production ABI proof) + +The Idris2 ABI scaffold lives under: + +* `+src/Abi/Types.idr+` +* `+src/Abi/Layout.idr+` +* `+src/Abi/Foreign.idr+` + +These modules use concrete `+axiom_*+` symbol names and no unresolved +template placeholders, but they declare a *generic* lifecycle/callback +surface (`+axiom_init+`, `+axiom_process+`, `+axiom_register_callback+`, +…) that does *not* match the ~36 real Zig kernel exports +(`+axiom_matmul+`, `+axiom_relu+`, `+axiom_conv2d+`, and the rest of +`+zig/src/axiom.zig+`) actually consumed by `+src/backends/zig_ffi.jl+`. +Treat this scaffold as a worked illustration of the hyperpolymath +ABI-FFI pattern (Idris2 ABI + Zig FFI), not as a proof binding Axiom’s +production kernels. The `+Verify.*+` functions in `+Types.idr+` are +`+putStrLn+` stubs, not executed proofs. + +*ROADMAP (future work, not yet started):* extend the `+.idr+` +declarations to cover the real `+axiom_*+` Zig exports and replace the +`+Verify+` stubs with genuine size/alignment/signature proofs checked +against `+zig/src/axiom.zig+` and `+ffi/zig/include/axiom.h+`. + +==== Idris2 validation + +[source,bash] +---- +idris2 --source-dir src --check src/Abi/Types.idr +idris2 --source-dir src --check src/Abi/Layout.idr +idris2 --source-dir src --check src/Abi/Foreign.idr +---- + +=== Runtime FFI Used in Production Paths + +Current production-tested backend FFI path is Julia <-> Zig: + +* Julia bridge: `+src/backends/zig_ffi.jl+` +* Zig C ABI exports: `+zig/src/axiom.zig+` (compiled to +`+libaxiom_zig.so+` via `+zig/build.zig+`; this is the artifact CI, +benchmarks, and `+AXIOM_ZIG_LIB+`/`+ZigBackend(...)+` actually load – +see `+.github/workflows/ci.yml+`, `+benchmark/*.jl+`, `+README.md+`) + +This path is covered by CI/readiness checks (backend parity + runtime +smoke). + +The pointwise ReLU path now uses `+axiom_relu_checked+`, which returns +an explicit status and preflights null pointers, overlapping +input/output ranges, and non-finite inputs before changing output. +`+axiom_relu6_checked+` provides the same contract for ReLU6; the legacy +void exports remain for compatibility. The production Zig build is pure +Zig and does not link libc merely to expose a C-compatible calling +convention. + +The current attention implementations have fixed stack capacities. +Checked exports reject scaled-dot-product sequence lengths above 64, +flash-attention sequence lengths above 4096, and flash block sizes above +64. The legacy void exports perform the same guards and return without +writing when dimensions are outside those capacities. These guards make +the existing implementations safe; they do not turn the simplified +attention code into production evidence. + +=== KNOWN ISSUE: orphan second Zig FFI tree (`+ffi/zig/+` vs `+zig/+`) + +There are *two* Zig trees in this repository and they are not the same +code: + +* *`+zig/+`* (repo root) – the real, production Zig backend. +`+zig/src/axiom.zig+` exports the ~36 real `+axiom_*+` kernels +(`+axiom_matmul+`, `+axiom_relu+`, `+axiom_conv2d+`, activations, norm, +pooling, attention, …) consumed by `+src/backends/zig_ffi.jl+` and built +into `+libaxiom_zig.so+`. +* *`+ffi/zig/+`* – a separate, smaller Zig tree +(`+ffi/zig/src/main.zig+`, `+ffi/zig/build.zig+`, +`+ffi/zig/include/axiom.h+`) that exports *zero* `+axiom_*+` kernel +symbols (`+grep -c "export fn axiom_"+` = 0) and instead implements a +different, generic lifecycle/callback C ABI matching the +`+src/Abi/*.idr+` scaffold’s naming (`+axiom_init+`, `+axiom_process+`, +`+axiom_register_callback+`, …). Its header comment even points at +`+src/abi/Foreign.idr+`, a stale/incorrect path (the real directory is +`+src/Abi/+`, capital A) – further evidence this tree has drifted from +the rest of the repo and is not wired into anything Julia actually +loads. + +*This is flagged, not fixed here.* `+ffi/zig/+` is not deleted – it may +be salvageable as the eventual real implementation backing the +`+src/Abi/*.idr+` scaffold (see ROADMAP notes above), but as of this +writing it is disconnected from both the production Zig backend and the +Idris2 ABI’s stated symbol surface. Anyone relying on "`the Zig FFI`" +should confirm which of the two trees they mean; for release/readiness +purposes only `+zig/+` is authoritative (next section). + +=== Zig FFI Status (production: `+zig/+`) + +`+zig/+` is the sole production-tested native backend and exports +concrete `+axiom_*+` symbols (~36, see `+TOPOLOGY.md+`): + +* implementation: `+zig/src/axiom.zig+` +* build entry: `+zig/build.zig+` +* Julia-side wiring: `+src/backends/zig_ffi.jl+` + +The separate `+ffi/zig/+` tree (`+ffi/zig/src/main.zig+`, +`+ffi/zig/build.zig+`, `+ffi/zig/test/integration_test.zig+`, +`+ffi/zig/include/axiom.h+`) is also concrete (non-template) and +internally self-consistent, but – per the orphan-tree note above – +exports a different, generic `+axiom_*+` surface that is not the +production kernel FFI. Its own validation still works in isolation: + +[source,bash] +---- +cd ffi/zig +zig build test +---- + +=== Bidirectionality Status + +* Implemented and exercised: +** host -> runtime calls (`+axiom_process+`, `+axiom_process_array+`, +etc.) +** runtime -> host callback bridge (`+axiom_register_callback+`, +`+axiom_invoke_callback+`) +* Idris side includes concrete callback pointer registration and +callback invoke declarations in `+src/Abi/Foreign.idr+`. +* Still not a full cross-language compatibility matrix across all +planned targets, but no longer template-only. + +=== Practical Guidance + +For release/readiness decisions, treat `+zig/+` + +`+src/backends/zig_ffi.jl+` as the authoritative production FFI +boundary. Treat the Idris2 `+src/Abi/*.idr+` files as an illustrative +ABI-FFI scaffold that typechecks and uses concrete Axiom naming, but +does *not* prove or specify the production kernel FFI – see the ROADMAP +notes above for what closing that gap would require. Treat `+ffi/zig/+` +as a flagged, currently-disconnected second Zig tree (see "`KNOWN +ISSUE`" above) pending a decision on whether to wire it to the +`+src/Abi/*.idr+` scaffold, fold it into `+zig/+`, or retire it. diff --git a/ABI-FFI-README.md b/ABI-FFI-README.md deleted file mode 100644 index 69e5b43..0000000 --- a/ABI-FFI-README.md +++ /dev/null @@ -1,127 +0,0 @@ -# Axiom.jl ABI / FFI Notes - -This file documents the current ABI/FFI split for Axiom.jl. - -## Idris2 ABI Scaffold (illustrative, not the production ABI proof) - -The Idris2 ABI scaffold lives under: - -- `src/Abi/Types.idr` -- `src/Abi/Layout.idr` -- `src/Abi/Foreign.idr` - -These modules use concrete `axiom_*` symbol names and no unresolved template -placeholders, but they declare a **generic** lifecycle/callback surface -(`axiom_init`, `axiom_process`, `axiom_register_callback`, ...) that does -**not** match the ~36 real Zig kernel exports (`axiom_matmul`, `axiom_relu`, -`axiom_conv2d`, and the rest of `zig/src/axiom.zig`) actually consumed by -`src/backends/zig_ffi.jl`. Treat this scaffold as a -worked illustration of the hyperpolymath ABI-FFI pattern (Idris2 ABI + Zig -FFI), not as a proof binding Axiom's production kernels. The `Verify.*` -functions in `Types.idr` are `putStrLn` stubs, not executed proofs. - -**ROADMAP (future work, not yet started):** extend the `.idr` declarations -to cover the real `axiom_*` Zig exports and replace the `Verify` stubs with -genuine size/alignment/signature proofs checked against `zig/src/axiom.zig` -and `ffi/zig/include/axiom.h`. - -### Idris2 validation - -```bash -idris2 --source-dir src --check src/Abi/Types.idr -idris2 --source-dir src --check src/Abi/Layout.idr -idris2 --source-dir src --check src/Abi/Foreign.idr -``` - -## Runtime FFI Used in Production Paths - -Current production-tested backend FFI path is Julia <-> Zig: - -- Julia bridge: `src/backends/zig_ffi.jl` -- Zig C ABI exports: `zig/src/axiom.zig` (compiled to `libaxiom_zig.so` via - `zig/build.zig`; this is the artifact CI, benchmarks, and - `AXIOM_ZIG_LIB`/`ZigBackend(...)` actually load -- see `.github/workflows/ci.yml`, - `benchmark/*.jl`, `README.md`) - -This path is covered by CI/readiness checks (backend parity + runtime smoke). - -The pointwise ReLU path now uses `axiom_relu_checked`, which returns an explicit -status and preflights null pointers, overlapping input/output ranges, and -non-finite inputs before changing output. `axiom_relu6_checked` provides the -same contract for ReLU6; the legacy void exports remain for compatibility. -The production Zig build is pure Zig and does not link libc merely to expose a -C-compatible calling convention. - -The current attention implementations have fixed stack capacities. Checked -exports reject scaled-dot-product sequence lengths above 64, flash-attention -sequence lengths above 4096, and flash block sizes above 64. The legacy void -exports perform the same guards and return without writing when dimensions are -outside those capacities. These guards make the existing implementations safe; -they do not turn the simplified attention code into production evidence. - -## KNOWN ISSUE: orphan second Zig FFI tree (`ffi/zig/` vs `zig/`) - -There are **two** Zig trees in this repository and they are not the same -code: - -- **`zig/`** (repo root) -- the real, production Zig backend. `zig/src/axiom.zig` - exports the ~36 real `axiom_*` kernels (`axiom_matmul`, `axiom_relu`, - `axiom_conv2d`, activations, norm, pooling, attention, ...) consumed by - `src/backends/zig_ffi.jl` and built into `libaxiom_zig.so`. -- **`ffi/zig/`** -- a separate, smaller Zig tree (`ffi/zig/src/main.zig`, - `ffi/zig/build.zig`, `ffi/zig/include/axiom.h`) that exports **zero** - `axiom_*` kernel symbols (`grep -c "export fn axiom_"` = 0) and instead - implements a different, generic lifecycle/callback C ABI matching the - `src/Abi/*.idr` scaffold's naming (`axiom_init`, `axiom_process`, - `axiom_register_callback`, ...). Its header comment even points at - `src/abi/Foreign.idr`, a stale/incorrect path (the real directory is - `src/Abi/`, capital A) -- further evidence this tree has drifted from the - rest of the repo and is not wired into anything Julia actually loads. - -**This is flagged, not fixed here.** `ffi/zig/` is not deleted -- it may be -salvageable as the eventual real implementation backing the `src/Abi/*.idr` -scaffold (see ROADMAP notes above), but as of this writing it is disconnected -from both the production Zig backend and the Idris2 ABI's stated symbol -surface. Anyone relying on "the Zig FFI" should confirm which of the two -trees they mean; for release/readiness purposes only `zig/` is authoritative -(next section). - -## Zig FFI Status (production: `zig/`) - -`zig/` is the sole production-tested native backend and exports concrete -`axiom_*` symbols (~36, see `TOPOLOGY.md`): - -- implementation: `zig/src/axiom.zig` -- build entry: `zig/build.zig` -- Julia-side wiring: `src/backends/zig_ffi.jl` - -The separate `ffi/zig/` tree (`ffi/zig/src/main.zig`, `ffi/zig/build.zig`, -`ffi/zig/test/integration_test.zig`, `ffi/zig/include/axiom.h`) is also -concrete (non-template) and internally self-consistent, but -- per the -orphan-tree note above -- exports a different, generic `axiom_*` surface -that is not the production kernel FFI. Its own validation still works -in isolation: - -```bash -cd ffi/zig -zig build test -``` - -## Bidirectionality Status - -- Implemented and exercised: - - host -> runtime calls (`axiom_process`, `axiom_process_array`, etc.) - - runtime -> host callback bridge (`axiom_register_callback`, `axiom_invoke_callback`) -- Idris side includes concrete callback pointer registration and callback invoke declarations in `src/Abi/Foreign.idr`. -- Still not a full cross-language compatibility matrix across all planned targets, but no longer template-only. - -## Practical Guidance - -For release/readiness decisions, treat `zig/` + `src/backends/zig_ffi.jl` as -the authoritative production FFI boundary. Treat the Idris2 `src/Abi/*.idr` -files as an illustrative ABI-FFI scaffold that typechecks and uses concrete -Axiom naming, but does **not** prove or specify the production kernel FFI -- -see the ROADMAP notes above for what closing that gap would require. Treat -`ffi/zig/` as a flagged, currently-disconnected second Zig tree (see -"KNOWN ISSUE" above) pending a decision on whether to wire it to the -`src/Abi/*.idr` scaffold, fold it into `zig/`, or retire it. diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 637d4be..0c54730 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -42,7 +42,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 === Removed - Rust backend removed; Zig backend is now the sole native backend. Migrate any `RustBackend(...)` calls to `ZigBackend(...)` and update `AXIOM_RUST_LIB` references to `AXIOM_ZIG_LIB`. - Comprehensive documentation (Architecture, Performance, Safety-Critical, etc.) -- RSR compliance infrastructure (flake.nix, Justfile, security policies) +- RSR compliance infrastructure (flake.guix, Justfile, security policies) - Attention mechanisms for transformer models - Flash attention implementation - Rotary position embeddings diff --git a/CODE_OF_CONDUCT.adoc b/CODE_OF_CONDUCT.adoc new file mode 100644 index 0000000..8a96a40 --- /dev/null +++ b/CODE_OF_CONDUCT.adoc @@ -0,0 +1,92 @@ +== Code of Conduct + +=== Our Pledge + +We as members, contributors, and leaders pledge to make participation in +our community a harassment-free experience for everyone, regardless of +age, body size, visible or invisible disability, ethnicity, sex +characteristics, gender identity and expression, level of experience, +education, socio-economic status, nationality, personal appearance, +race, caste, color, religion, or sexual identity and orientation. + +We pledge to act and interact in ways that contribute to an open, +welcoming, diverse, inclusive, and healthy community. + +=== Our Standards + +Examples of behavior that contributes to a positive environment: + +* *Emotional Safety*: Creating space for experimentation without shame +* *Technical Excellence*: Valuing correctness and quality +* *Respectful Disagreement*: Engaging with ideas, not attacking people +* *Collaborative Learning*: Sharing knowledge generously +* *Inclusive Language*: Using welcoming and accessible language + +Examples of unacceptable behavior: + +* Harassment, discrimination, or exclusionary behavior +* Trolling, insulting comments, or personal attacks +* Public or private harassment +* Publishing others’ private information without consent +* Dismissing or attacking inclusion efforts +* Other conduct inappropriate in a professional setting + +=== Scope + +This Code of Conduct applies within all community spaces, including: + +* GitHub/GitLab repositories +* Issue trackers and pull requests +* Mailing lists and forums +* Chat platforms (Discord, etc.) +* Conferences and meetups +* Social media when representing the project + +=== Enforcement + +==== Reporting + +Report violations to: conduct@axiom-jl.org + +All reports will be reviewed promptly and confidentially. + +==== Response Guidelines + +Community leaders will follow these steps: + +[arabic] +. *Acknowledgment*: Within 48 hours +. *Investigation*: Fair review of the situation +. *Decision*: Based on severity and context +. *Communication*: Inform all parties of the outcome + +==== Enforcement Actions + +[cols=",,",options="header",] +|=== +|Level |Action |Duration +|1. Correction |Private warning, explanation |N/A +|2. Warning |Public warning, no interaction |30 days +|3. Temporary Ban |Suspension from community |90 days +|4. Permanent Ban |Permanent exclusion |Indefinite +|=== + +=== Attribution + +This Code of Conduct is adapted from the +https://www.contributor-covenant.org[Contributor Covenant], version 2.1, +available at +https://www.contributor-covenant.org/version/2/1/code_of_conduct.html. + +Community Impact Guidelines were inspired by +https://github.com/mozilla/diversity[Mozilla’s code of conduct +enforcement ladder]. + +For answers to common questions about this code of conduct, see the FAQ +at https://www.contributor-covenant.org/faq. Translations are available +at https://www.contributor-covenant.org/translations. + +''''' + +_This Code of Conduct is part of our RSR compliance commitment to +emotionally safe software development._ diff --git a/CODE_OF_CONDUCT.md b/CODE_OF_CONDUCT.md deleted file mode 100644 index f46842b..0000000 --- a/CODE_OF_CONDUCT.md +++ /dev/null @@ -1,96 +0,0 @@ - -# Code of Conduct - -## Our Pledge - -We as members, contributors, and leaders pledge to make participation in our -community a harassment-free experience for everyone, regardless of age, body -size, visible or invisible disability, ethnicity, sex characteristics, gender -identity and expression, level of experience, education, socio-economic status, -nationality, personal appearance, race, caste, color, religion, or sexual -identity and orientation. - -We pledge to act and interact in ways that contribute to an open, welcoming, -diverse, inclusive, and healthy community. - -## Our Standards - -Examples of behavior that contributes to a positive environment: - -* **Emotional Safety**: Creating space for experimentation without shame -* **Technical Excellence**: Valuing correctness and quality -* **Respectful Disagreement**: Engaging with ideas, not attacking people -* **Collaborative Learning**: Sharing knowledge generously -* **Inclusive Language**: Using welcoming and accessible language - -Examples of unacceptable behavior: - -* Harassment, discrimination, or exclusionary behavior -* Trolling, insulting comments, or personal attacks -* Public or private harassment -* Publishing others' private information without consent -* Dismissing or attacking inclusion efforts -* Other conduct inappropriate in a professional setting - -## Scope - -This Code of Conduct applies within all community spaces, including: - -* GitHub/GitLab repositories -* Issue trackers and pull requests -* Mailing lists and forums -* Chat platforms (Discord, etc.) -* Conferences and meetups -* Social media when representing the project - -## Enforcement - -### Reporting - -Report violations to: conduct@axiom-jl.org - -All reports will be reviewed promptly and confidentially. - -### Response Guidelines - -Community leaders will follow these steps: - -1. **Acknowledgment**: Within 48 hours -2. **Investigation**: Fair review of the situation -3. **Decision**: Based on severity and context -4. **Communication**: Inform all parties of the outcome - -### Enforcement Actions - -| Level | Action | Duration | -|-------|--------|----------| -| 1. Correction | Private warning, explanation | N/A | -| 2. Warning | Public warning, no interaction | 30 days | -| 3. Temporary Ban | Suspension from community | 90 days | -| 4. Permanent Ban | Permanent exclusion | Indefinite | - -## Attribution - -This Code of Conduct is adapted from the [Contributor Covenant][homepage], -version 2.1, available at -[https://www.contributor-covenant.org/version/2/1/code_of_conduct.html][v2.1]. - -Community Impact Guidelines were inspired by -[Mozilla's code of conduct enforcement ladder][Mozilla CoC]. - -For answers to common questions about this code of conduct, see the FAQ at -[https://www.contributor-covenant.org/faq][FAQ]. Translations are available at -[https://www.contributor-covenant.org/translations][translations]. - -[homepage]: https://www.contributor-covenant.org -[v2.1]: https://www.contributor-covenant.org/version/2/1/code_of_conduct.html -[Mozilla CoC]: https://github.com/mozilla/diversity -[FAQ]: https://www.contributor-covenant.org/faq -[translations]: https://www.contributor-covenant.org/translations - ---- - -*This Code of Conduct is part of our RSR compliance commitment to emotionally safe software development.* diff --git a/CONTRIBUTING.adoc b/CONTRIBUTING.adoc index e9b1993..dd089ae 100644 --- a/CONTRIBUTING.adoc +++ b/CONTRIBUTING.adoc @@ -1,21 +1,71 @@ -// SPDX-License-Identifier: CC-BY-SA-4.0 -// Copyright (c) Jonathan D.A. Jewell -= Contributing Guide +== Contributing -== Getting Started +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/+`. -1. Fork the repository -2. Create a feature branch from `main` -3. Sign off commits (`git commit -s`) -4. Submit a pull request +=== How to Contribute -== Commit Guidelines +We welcome contributions in many forms: -* Conventional commits: `type(scope): description` -* Sign all commits (DCO required) -* Atomic, focused commits +* *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 -== License +=== Getting Started -Contributions licensed under project license. +[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 5d695b0..0000000 --- a/CONTRIBUTING.md +++ /dev/null @@ -1,69 +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/GOVERNANCE.adoc b/GOVERNANCE.adoc index e41020d..2659760 100644 --- a/GOVERNANCE.adoc +++ b/GOVERNANCE.adoc @@ -1,162 +1,161 @@ -// SPDX-License-Identifier: CC-BY-SA-4.0 -// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell -= Governance Model -:toc: preamble +== Governance -This document describes the governance model for this repository. +=== Overview -== Overview +Axiom.jl uses a *Benevolent Dictator for Life (BDFL) + Consensus* model, +inspired by successful open source projects while incorporating RSR +principles. -This repository follows a **Sole Maintainer Governance Model**: +=== Decision Making -* 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 +==== Levels of Decision -== Core Principles - -[cols="1,2"] +[width="100%",cols="31%,30%,39%",options="header",] +|=== +|Level |Scope |Process +|*Minor* |Bug fixes, docs, typos |Single maintainer approval +|*Standard* |Features, refactors |Two maintainer approval +|*Major* |Architecture, breaking changes |BDFL + community RFC +|*Governance* |This document, CoC changes |BDFL + supermajority vote |=== -| Principle | Description -| **Benevolent Dictatorship** | Maintainer has final decision authority but seeks community input +==== RFC Process -| **Meritocracy** | Contributions are judged on technical merit, not contributor identity +For major changes: -| **Transparency** | All significant decisions are documented publicly +[arabic] +. *Draft RFC*: Open issue with `+[RFC]+` prefix +. *Discussion Period*: Minimum 14 days +. *Revision*: Address feedback +. *Final Comment Period*: 7 days +. *Decision*: BDFL decision with reasoning -| **Consensus-Seeking** | Maintainer prefers consensus but will decide when necessary +=== Roles -| **Open Contribution** | Anyone can contribute via fork and pull request +==== BDFL (Benevolent Dictator for Life) -|=== +*Current BDFL*: @hyperpolymath (Project Founder) -== Roles and Permissions +Responsibilities: - Final arbiter on technical disputes - Guardian of +project vision - Emergency decisions when needed -[cols="1,2,2"] -|=== -| Role | Permissions | Assignment +The BDFL can be changed by unanimous agreement of Core Contributors. -| **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 +==== Core Contributors -|=== +Contributors with merge rights. Requirements: -== Decision Making Framework +* Sustained contributions over 6+ months +* Deep understanding of codebase +* Demonstrated alignment with project values +* Nominated by existing Core Contributor +* Approved by BDFL -=== Routine Decisions +*Current Core Contributors*: See `+MAINTAINERS.md+` -* Bug fixes -* Documentation improvements -* Minor feature additions -* Dependency updates +==== Contributors -**Process**: Maintainer reviews and merges PRs that meet quality standards. +Anyone who has contributed code, docs, issues, or reviews. -=== Significant Changes +==== Community Members -* New major features -* API changes -* Architecture modifications -* Breaking changes +Anyone participating in discussions, using the software, or providing +feedback. -**Process**: -. Open issue describing the change -. Discuss with community (minimum 72 hours) -. Maintainer makes final decision -. Document rationale in issue/PR +=== Tri-Perimeter Contribution Framework (TPCF) -=== Structural Decisions +Following RSR standards, contributions are organized by trust level: -* Repository purpose/renaming -* License changes -* Ownership transfer -* Deprecation/archival +==== 🔒 Perimeter 1 (Core) -**Process**: -. Extended discussion (minimum 1 week) -. Maintainer makes final decision -. Document in CHANGELOG and governance docs +*Access*: Core Contributors only -== Contribution Lifecycle +Areas: - Build system (flake.guix, Justfile) - CI/CD configuration - +Security-critical code - FFI boundaries - Release process -[cols="1,2"] -|=== -| Stage | Process +==== 🧠 Perimeter 2 (Expert) -| **Ideation** | Open issue, discuss feasibility +*Access*: Trusted Contributors (established track record) -| **Development** | Fork, implement, test thoroughly +Areas: - Core algorithms - Verification system - Backend implementations +- API design - Performance-critical code -| **Review** | Submit PR, maintainer reviews within 7 days +==== 🌱 Perimeter 3 (Community) -| **Merge** | Maintainer merges or requests changes +*Access*: Open to all -| **Release** | Maintainer publishes according to project conventions +Areas: - Documentation - Examples - Tests - Bug reports - Feature +proposals - Community support -|=== +=== Meetings -== Conflict Resolution +==== Technical Meetings -In case of disagreements: +* *Frequency*: Monthly +* *Format*: Video call + text summary +* *Agenda*: Posted 7 days in advance +* *Notes*: Published in `+docs/meetings/+` -. 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 +==== Community Calls -== Project Policies +* *Frequency*: Quarterly +* *Format*: Open video call +* *Purpose*: Community Q&A, roadmap discussion -This repository adheres to hyperpolymath estate-wide policies: +=== Conflict Resolution -* **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 +[arabic] +. *Discussion*: Try to resolve through discussion +. *Mediation*: Involve neutral third party +. *Escalation*: Bring to Core Contributors +. *Final Decision*: BDFL makes final call -== Repository-Specific Conventions +=== Changes to Governance -[cols="1,2"] -|=== -| Convention | Description +This document can be changed through: -| **Signing** | All commits must be signed (SSH or GPG) +[arabic] +. RFC process (standard) +. 14-day discussion period +. Supermajority (2/3) approval from Core Contributors +. BDFL approval -| **SPDX Headers** | All source files must have SPDX license identifiers +=== Code of Conduct -| **Contractiles** | Mustfile, Trustfile, Intendfile, Adjustfile in root +All participants must follow our link:CODE_OF_CONDUCT.md[Code of +Conduct]. -| **Machine Readable** | META.a2ml in .machine_readable/6a2/ +Violations should be reported to: conduct@axiom-jl.org -| **CI/CD** | GitHub Actions workflows in .github/workflows/ +=== Licensing Decisions -|=== +* Core framework: MIT License +* All contributions must be MIT-compatible +* Third-party dependencies reviewed for license compatibility +* SPDX headers required on all source files -== Governance Evolution +=== Financial Transparency -As the project grows, this governance model may evolve: +* Funding sources listed in `+FUNDING.yml+` +* Financial reports published quarterly (when applicable) +* No individual may receive >50% of project funds +* All spending decisions made by Core Contributors -* **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) +=== Succession Planning -Changes to this document require the same process as Significant Changes above. +If the BDFL becomes unavailable: -== See Also +[arabic] +. Core Contributors elect interim leader (simple majority) +. 90-day period to establish new governance +. Options: New BDFL, Steering Committee, or Foundation -* 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)] +=== Contact -== Changelog +* General: hello@axiom-jl.org +* Governance questions: governance@axiom-jl.org +* Security issues: security@axiom-jl.org -[cols="1,1,1"] -|=== -| Date | Change | By +''''' -| 2026-06-07 | Initial governance model established | @hyperpolymath -|=== +_This governance model follows RSR community governance standards._ diff --git a/GOVERNANCE.md b/GOVERNANCE.md deleted file mode 100644 index 2646ae7..0000000 --- a/GOVERNANCE.md +++ /dev/null @@ -1,167 +0,0 @@ - -# Governance - -## Overview - -Axiom.jl uses a **Benevolent Dictator for Life (BDFL) + Consensus** model, inspired by successful open source projects while incorporating RSR principles. - -## Decision Making - -### Levels of Decision - -| Level | Scope | Process | -|-------|-------|---------| -| **Minor** | Bug fixes, docs, typos | Single maintainer approval | -| **Standard** | Features, refactors | Two maintainer approval | -| **Major** | Architecture, breaking changes | BDFL + community RFC | -| **Governance** | This document, CoC changes | BDFL + supermajority vote | - -### RFC Process - -For major changes: - -1. **Draft RFC**: Open issue with `[RFC]` prefix -2. **Discussion Period**: Minimum 14 days -3. **Revision**: Address feedback -4. **Final Comment Period**: 7 days -5. **Decision**: BDFL decision with reasoning - -## Roles - -### BDFL (Benevolent Dictator for Life) - -**Current BDFL**: @hyperpolymath (Project Founder) - -Responsibilities: -- Final arbiter on technical disputes -- Guardian of project vision -- Emergency decisions when needed - -The BDFL can be changed by unanimous agreement of Core Contributors. - -### Core Contributors - -Contributors with merge rights. Requirements: - -- Sustained contributions over 6+ months -- Deep understanding of codebase -- Demonstrated alignment with project values -- Nominated by existing Core Contributor -- Approved by BDFL - -**Current Core Contributors**: See `MAINTAINERS.md` - -### Contributors - -Anyone who has contributed code, docs, issues, or reviews. - -### Community Members - -Anyone participating in discussions, using the software, or providing feedback. - -## Tri-Perimeter Contribution Framework (TPCF) - -Following RSR standards, contributions are organized by trust level: - -### 🔒 Perimeter 1 (Core) - -**Access**: Core Contributors only - -Areas: -- Build system (flake.nix, Justfile) -- CI/CD configuration -- Security-critical code -- FFI boundaries -- Release process - -### 🧠 Perimeter 2 (Expert) - -**Access**: Trusted Contributors (established track record) - -Areas: -- Core algorithms -- Verification system -- Backend implementations -- API design -- Performance-critical code - -### 🌱 Perimeter 3 (Community) - -**Access**: Open to all - -Areas: -- Documentation -- Examples -- Tests -- Bug reports -- Feature proposals -- Community support - -## Meetings - -### Technical Meetings - -- **Frequency**: Monthly -- **Format**: Video call + text summary -- **Agenda**: Posted 7 days in advance -- **Notes**: Published in `docs/meetings/` - -### Community Calls - -- **Frequency**: Quarterly -- **Format**: Open video call -- **Purpose**: Community Q&A, roadmap discussion - -## Conflict Resolution - -1. **Discussion**: Try to resolve through discussion -2. **Mediation**: Involve neutral third party -3. **Escalation**: Bring to Core Contributors -4. **Final Decision**: BDFL makes final call - -## Changes to Governance - -This document can be changed through: - -1. RFC process (standard) -2. 14-day discussion period -3. Supermajority (2/3) approval from Core Contributors -4. BDFL approval - -## Code of Conduct - -All participants must follow our [Code of Conduct](CODE_OF_CONDUCT.md). - -Violations should be reported to: conduct@axiom-jl.org - -## Licensing Decisions - -- Core framework: MIT License -- All contributions must be MIT-compatible -- Third-party dependencies reviewed for license compatibility -- SPDX headers required on all source files - -## Financial Transparency - -- Funding sources listed in `FUNDING.yml` -- Financial reports published quarterly (when applicable) -- No individual may receive >50% of project funds -- All spending decisions made by Core Contributors - -## Succession Planning - -If the BDFL becomes unavailable: - -1. Core Contributors elect interim leader (simple majority) -2. 90-day period to establish new governance -3. Options: New BDFL, Steering Committee, or Foundation - -## Contact - -- General: hello@axiom-jl.org -- Governance questions: governance@axiom-jl.org -- Security issues: security@axiom-jl.org - ---- - -*This governance model follows RSR community governance standards.* diff --git a/MAINTAINERS.adoc b/MAINTAINERS.adoc index aa23a55..e62348c 100644 --- a/MAINTAINERS.adoc +++ b/MAINTAINERS.adoc @@ -1,48 +1,88 @@ -// SPDX-License-Identifier: CC-BY-SA-4.0 -// Copyright (c) Jonathan D.A. Jewell -= Maintainers -:toc: preamble +== Maintainers -This document lists the maintainers of this project and their responsibilities. +This document lists the maintainers of Axiom.jl and their +responsibilities. -== Current Maintainers +=== Core Maintainers -[cols="2,3,2",options="header"] +Core maintainers have full write access and are responsible for the +project’s direction. + +[cols=",,,",options="header",] +|=== +|Name |GitHub |Role |Areas +|Project Founder |@Hyperpolymath |BDFL |Architecture, Vision |=== -| Name | Role | Contact -| Jonathan D.A. Jewell -| Lead Maintainer -| https://github.com/hyperpolymath[@hyperpolymath] +=== Area Maintainers + +Area maintainers have expertise and responsibility for specific areas. + +[cols=",,",options="header",] |=== +|Area |Maintainer(s) |Description +|Julia Core |Unassigned |Core Julia implementation +|Rust Backend |Unassigned |Rust FFI and performance +|Zig Backend |Unassigned |Zig FFI and SIMD +|Verification |Unassigned |@ensure, @prove, certificates +|Documentation |Unassigned |Wiki, tutorials, API docs +|CI/CD |Unassigned |Build, test, release +|=== + +=== Responsibilities + +==== All Maintainers + +* Respond to issues and PRs within 7 days +* Follow the Code of Conduct +* Review code according to contribution guidelines +* Participate in governance decisions + +==== Core Maintainers + +* Guide overall project direction +* Make final decisions on disputed issues +* Manage releases +* Handle security issues +* Mentor new contributors + +==== Area Maintainers + +* Expert review for their area +* First response for area-specific issues +* Documentation for their area +* Onboarding contributors to their area + +=== Becoming a Maintainer -== Responsibilities +==== Requirements -Maintainers are responsible for: +[arabic] +. *Sustained Contribution*: 6+ months of regular contributions +. *Quality*: Consistently high-quality code and reviews +. *Community*: Helpful and respectful interactions +. *Understanding*: Deep knowledge of the codebase -* Reviewing and merging pull requests -* Triaging issues and feature requests -* Ensuring code quality and security standards -* Managing releases and versioning -* Upholding the project's code of conduct +==== Process -== Becoming a Maintainer +[arabic] +. Nomination by existing maintainer +. Discussion among maintainers (private) +. Vote (simple majority of core maintainers) +. Announcement and onboarding -Contributors who demonstrate: +=== Emeritus Maintainers -* Consistent, high-quality contributions -* Understanding of the project's goals and standards -* Constructive participation in discussions -* Commitment to the project's long-term health +Maintainers who have stepped back but made significant contributions: -May be invited to become maintainers at the discretion of existing maintainers. +_None yet - we’re a new project!_ -== Decision Making +=== Contact -* Routine decisions (bug fixes, minor improvements) can be made by any maintainer -* Significant changes require discussion and consensus among maintainers -* Breaking changes or major features should be discussed in issues before implementation +* General questions: maintainers@axiom-jl.org +* Security issues: security@axiom-jl.org +* Governance: governance@axiom-jl.org -== Contact +''''' -For questions about project governance, open an issue or contact the maintainers listed above. +_This document is part of RSR compliance for transparent governance._ diff --git a/MAINTAINERS.md b/MAINTAINERS.md deleted file mode 100644 index ca4443e..0000000 --- a/MAINTAINERS.md +++ /dev/null @@ -1,80 +0,0 @@ -# Maintainers - -This document lists the maintainers of Axiom.jl and their responsibilities. - -## Core Maintainers - -Core maintainers have full write access and are responsible for the project's direction. - -| Name | GitHub | Role | Areas | -|------|--------|------|-------| -| Project Founder | @Hyperpolymath | BDFL | Architecture, Vision | - -## Area Maintainers - -Area maintainers have expertise and responsibility for specific areas. - -| Area | Maintainer(s) | Description | -|------|---------------|-------------| -| Julia Core | Unassigned | Core Julia implementation | -| Rust Backend | Unassigned | Rust FFI and performance | -| Zig Backend | Unassigned | Zig FFI and SIMD | -| Verification | Unassigned | @ensure, @prove, certificates | -| Documentation | Unassigned | Wiki, tutorials, API docs | -| CI/CD | Unassigned | Build, test, release | - -## Responsibilities - -### All Maintainers - -- Respond to issues and PRs within 7 days -- Follow the Code of Conduct -- Review code according to contribution guidelines -- Participate in governance decisions - -### Core Maintainers - -- Guide overall project direction -- Make final decisions on disputed issues -- Manage releases -- Handle security issues -- Mentor new contributors - -### Area Maintainers - -- Expert review for their area -- First response for area-specific issues -- Documentation for their area -- Onboarding contributors to their area - -## Becoming a Maintainer - -### Requirements - -1. **Sustained Contribution**: 6+ months of regular contributions -2. **Quality**: Consistently high-quality code and reviews -3. **Community**: Helpful and respectful interactions -4. **Understanding**: Deep knowledge of the codebase - -### Process - -1. Nomination by existing maintainer -2. Discussion among maintainers (private) -3. Vote (simple majority of core maintainers) -4. Announcement and onboarding - -## Emeritus Maintainers - -Maintainers who have stepped back but made significant contributions: - -*None yet - we're a new project!* - -## Contact - -- General questions: maintainers@axiom-jl.org -- Security issues: security@axiom-jl.org -- Governance: governance@axiom-jl.org - ---- - -*This document is part of RSR compliance for transparent governance.* diff --git a/REGISTRY-READINESS.adoc b/REGISTRY-READINESS.adoc new file mode 100644 index 0000000..bd12b6d --- /dev/null +++ b/REGISTRY-READINESS.adoc @@ -0,0 +1,113 @@ +== Axiom.jl — Honest Registry-Readiness Assessment + +Last updated: 2026-05-18. This is a deliberately blunt self-assessment, +not marketing. It exists because the Julia General registry maintainers +(rightly) flagged this org for high-volume, LLM-generated, incoherent +package submissions. The only thing that rebuilds that trust is honesty. + +=== What was actually wrong (and is now fixed) + +[width="100%",cols="50%,50%",options="header",] +|=== +|Problem (real) |Status +|`+Project.toml+` had *9 fabricated dependency UUIDs* (`+11111111-…+`) + +9 phantom extensions for packages that do not exist |✅ Removed + +|Hard dep on *unregistered* `+AcceleratorGate+` |✅ Vendored internally; +dependency dropped + +|Docs claimed "`283 tests / 99% / Release Candidate`", broken cert +workflow described as working, `+@prove+` described as proving |✅ +README/EXPLAINME rewritten to the truth; false claims removed + +|100 erroring tests (`+size(::Tensor,::Int)+` undefined) |✅ Fixed (real +root cause) + +|`+generate_certificate+` threw `+FieldError+` (`+result.mode+` +nonexistent) — broke the shipped example |✅ Fixed +(`+verification_mode+` kwarg) + +|`+sum(::Tensor; dims)+` undefined — documented usage failed |✅ Fixed + +|Licensing self-contradictory: `+Project.toml+` MPL-2.0 vs source +headers PMPL-1.0 (non-OSI) |✅ Relicensed consistently to *MPL-2.0* +(OSI), REUSE.toml added + +|LLM-tell files in package root |⚠ Corrected (were NOT removed): +`+0-AI-MANIFEST.a2ml+` is a *required* RSR machine-readable manifest — +kept, not an LLM-tell to remove. `+llm-warmup-*.md+` remain in root as +the estate LLM-warmup convention (same as sibling repos, +e.g. `+julia-professional-registry+`). +|=== + +=== Honest current limitations (NOT hidden) + +* *`+@prove+` is experimental* — it runs but returns `+unknown+`; it +does not discharge proofs. Documented as such; not a registration claim. +* *No native GPU acceleration of Axiom’s own.* GPU/accelerator support +is optional extensions over real packages (CUDA/AMDGPU/Metal/PyCall) +only. +* *Axiom is downstream of Zygote* for AD; it implements none itself. +* The accelerator "`backends`" (TPU/NPU/FPGA/…) are *type stubs*, not +working hardware backends. The README’s prior-art section states plainly +that Flux.jl/Lux.jl/CUDA.jl/KernelAbstractions.jl are more capable for +real training on real hardware; Axiom’s only distinct contribution is +first-class runtime property-checking + packaging + multi-protocol +serving as named APIs. + +=== Registry checklist + +* [x] No fabricated UUIDs / phantom deps +* [x] All deps registered (after vendoring AcceleratorGate) +* [x] OSI license (MPL-2.0), consistent, REUSE.toml +* [x] Honest README with usage example + prior-art comparison +* [x] `+Pkg.test()+` green (verified repeatedly, incl. post-relicense) +* [x] Aqua.jl quality gate: *now a real, wired-in CI gate* +(`+test/aqua.jl+`, included from `+test/runtests.jl+`), not just a +self-assessment claim. `+Aqua.test_all(Axiom)+` passes with *zero +overrides* – ambiguities, unbound type parameters, undefined exports, +project-extras, stale deps, `+[compat]+` bounds (incl. `+julia+`), +piracy, and persistent tasks all pass clean. Getting there required two +real fixes, not exemptions: - Three genuine unbound-type-parameter bugs +in `+src/layers/normalization.jl+` (`+LayerNorm+`, `+InstanceNorm+`, +`+GroupNorm+`): their auto-generated default constructors left `+T+` +(and `+S+`) unbound because the only `+T+`-typed fields were +`+Union{_, Nothing}+` (nullable when `+affine=false+`). Fixed with +explicit inner constructors that bind `+T+`/`+S+` from the type +application itself. - The stale `+JSON3+` dependency (its sole consumer, +`+src/integrations/huggingface.jl+`, is dead code never `+include()+`d +from `+src/Axiom.jl+`) is now actually removed from `+Project.toml+`’s +`+[deps]+` – this bullet had previously been marked done without a real +Aqua run to verify it; it was not. +* [x] JET.jl static analysis gate: *new* (`+test/jet.jl+`), scoped to +Axiom’s own code via JET’s native `+target_modules+` config. +`+report_package(Axiom)+` finds 66 possible errors when run unscoped +(essentially all rooted in transitive deps: JSON/ StructUtils +conversions, LinearAlgebra QR internals, Zygote adjoint plumbing); +scoped to `+target_modules = (Axiom,)+` it finds *zero*, verified by +direct report enumeration, not just by trusting the scoping logic. +* [x] Documenter.jl docs build (`+docs/make.jl+`, `+docs/src/+`), with +`+doctest = true+`, builds clean locally +(`+julia --project=docs docs/make.jl+`, exit 0, no warnings). API +reference split across 4 pages by source-file area because a single-page +`+@autodocs+` dump of Axiom’s full public surface exceeds Documenter’s +HTML `+size_threshold+` sanity check. +* [x] Julia test-gate wired into CI +(`+.github/workflows/julia-test.yml+`): builds the hybrid +Ed448+Dilithium5 crypto cdylib (`+crypto/+`) before running +`+Pkg.test()+`, so `+test/verification/hybrid_signing_tests.jl+` +actually exercises the real signing path in CI instead of always taking +the `+@test_skip+` branch (the pre-existing `+ci.yml+` `+julia-compat+` +job never built the crypto shim, so those 27 tests were silently skipped +in every CI run to date). +* [ ] *Human maintainer track* — NOT a code task: genuine Julia +community participation, engaging the registry maintainers as a person, +and reducing org-wide package sprawl. This, not tooling, is the actual +gate. Registration should not be re-attempted until this is genuinely +addressed. + +=== Position + +This package is now technically honest and defensible. It is *not* +re-submitted to General by tooling. Whether/when to register is a human +decision contingent on the community-trust track above. diff --git a/REGISTRY-READINESS.md b/REGISTRY-READINESS.md deleted file mode 100644 index 56e720c..0000000 --- a/REGISTRY-READINESS.md +++ /dev/null @@ -1,95 +0,0 @@ - - - -# Axiom.jl — Honest Registry-Readiness Assessment - -Last updated: 2026-05-18. This is a deliberately blunt self-assessment, not -marketing. It exists because the Julia General registry maintainers -(rightly) flagged this org for high-volume, LLM-generated, incoherent -package submissions. The only thing that rebuilds that trust is honesty. - -## What was actually wrong (and is now fixed) - -| Problem (real) | Status | -|---|---| -| `Project.toml` had **9 fabricated dependency UUIDs** (`11111111-…`) + 9 phantom extensions for packages that do not exist | ✅ Removed | -| Hard dep on **unregistered** `AcceleratorGate` | ✅ Vendored internally; dependency dropped | -| Docs claimed "283 tests / 99% / Release Candidate", broken cert workflow described as working, `@prove` described as proving | ✅ README/EXPLAINME rewritten to the truth; false claims removed | -| 100 erroring tests (`size(::Tensor,::Int)` undefined) | ✅ Fixed (real root cause) | -| `generate_certificate` threw `FieldError` (`result.mode` nonexistent) — broke the shipped example | ✅ Fixed (`verification_mode` kwarg) | -| `sum(::Tensor; dims)` undefined — documented usage failed | ✅ Fixed | -| Licensing self-contradictory: `Project.toml` MPL-2.0 vs source headers PMPL-1.0 (non-OSI) | ✅ Relicensed consistently to **MPL-2.0** (OSI), REUSE.toml added | -| LLM-tell files in package root | ⚠ Corrected (were NOT removed): `0-AI-MANIFEST.a2ml` is a **required** RSR machine-readable manifest — kept, not an LLM-tell to remove. `llm-warmup-*.md` remain in root as the estate LLM-warmup convention (same as sibling repos, e.g. `julia-professional-registry`). | - -## Honest current limitations (NOT hidden) - -- **`@prove` is experimental** — it runs but returns `unknown`; it does not - discharge proofs. Documented as such; not a registration claim. -- **No native GPU acceleration of Axiom's own.** GPU/accelerator support is - optional extensions over real packages (CUDA/AMDGPU/Metal/PyCall) only. -- **Axiom is downstream of Zygote** for AD; it implements none itself. -- The accelerator "backends" (TPU/NPU/FPGA/…) are **type stubs**, not - working hardware backends. The README's prior-art section states plainly - that Flux.jl/Lux.jl/CUDA.jl/KernelAbstractions.jl are more capable for - real training on real hardware; Axiom's only distinct contribution is - first-class runtime property-checking + packaging + multi-protocol - serving as named APIs. - -## Registry checklist - -- [x] No fabricated UUIDs / phantom deps -- [x] All deps registered (after vendoring AcceleratorGate) -- [x] OSI license (MPL-2.0), consistent, REUSE.toml -- [x] Honest README with usage example + prior-art comparison -- [x] `Pkg.test()` green (verified repeatedly, incl. post-relicense) -- [x] Aqua.jl quality gate: **now a real, wired-in CI gate** - (`test/aqua.jl`, included from `test/runtests.jl`), not just a - self-assessment claim. `Aqua.test_all(Axiom)` passes with **zero - overrides** -- ambiguities, unbound type parameters, undefined - exports, project-extras, stale deps, `[compat]` bounds (incl. - `julia`), piracy, and persistent tasks all pass clean. Getting there - required two real fixes, not exemptions: - - Three genuine unbound-type-parameter bugs in - `src/layers/normalization.jl` (`LayerNorm`, `InstanceNorm`, - `GroupNorm`): their auto-generated default constructors left `T` - (and `S`) unbound because the only `T`-typed fields were - `Union{_, Nothing}` (nullable when `affine=false`). Fixed with - explicit inner constructors that bind `T`/`S` from the type - application itself. - - The stale `JSON3` dependency (its sole consumer, - `src/integrations/huggingface.jl`, is dead code never - `include()`d from `src/Axiom.jl`) is now actually removed from - `Project.toml`'s `[deps]` -- this bullet had previously been - marked done without a real Aqua run to verify it; it was not. -- [x] JET.jl static analysis gate: **new** (`test/jet.jl`), scoped to - Axiom's own code via JET's native `target_modules` config. - `report_package(Axiom)` finds 66 possible errors when run - unscoped (essentially all rooted in transitive deps: JSON/ - StructUtils conversions, LinearAlgebra QR internals, Zygote adjoint - plumbing); scoped to `target_modules = (Axiom,)` it finds **zero**, - verified by direct report enumeration, not just by trusting the - scoping logic. -- [x] Documenter.jl docs build (`docs/make.jl`, `docs/src/`), with - `doctest = true`, builds clean locally (`julia --project=docs - docs/make.jl`, exit 0, no warnings). API reference split across 4 - pages by source-file area because a single-page `@autodocs` dump - of Axiom's full public surface exceeds Documenter's HTML - `size_threshold` sanity check. -- [x] Julia test-gate wired into CI (`.github/workflows/julia-test.yml`): - builds the hybrid Ed448+Dilithium5 crypto cdylib (`crypto/`) before - running `Pkg.test()`, so `test/verification/hybrid_signing_tests.jl` - actually exercises the real signing path in CI instead of always - taking the `@test_skip` branch (the pre-existing `ci.yml` - `julia-compat` job never built the crypto shim, so those 27 tests - were silently skipped in every CI run to date). -- [ ] **Human maintainer track** — NOT a code task: genuine Julia - community participation, engaging the registry maintainers as a - person, and reducing org-wide package sprawl. This, not tooling, is - the actual gate. Registration should not be re-attempted until this - is genuinely addressed. - -## Position - -This package is now technically honest and defensible. It is **not** -re-submitted to General by tooling. Whether/when to register is a human -decision contingent on the community-trust track above. diff --git a/REQUIRES_INITIALISATION.adoc b/REQUIRES_INITIALISATION.adoc new file mode 100644 index 0000000..88f764c --- /dev/null +++ b/REQUIRES_INITIALISATION.adoc @@ -0,0 +1,56 @@ +== REQUIRES INITIALISATION + +*This repository is not finished being set up.* 1 substitution token(s) +across 1 file(s) still have no value. + +=== Why this is not already done + +This repo was created from `+hyperpolymath/rsr-template-repo+`. The mint +(`+just repo-init+`) fills every token that has a single mechanical +answer — owner, repo, author, dates, licence, branch — and it has done +so here. + +The tokens below are the ones it _deliberately cannot_ answer. They need +a decision or a fact that exists only in your head: what this project is +for, what command builds it, which port the service listens on, whether +a PGP key is held at all. The template’s own token vocabulary says as +much — you cannot sensibly answer "`required invariants`" in a +thirty-second bootstrap. + +They were left *visibly unfilled on purpose*. The alternatives were both +worse: inventing plausible values would put confident falsehoods into a +security policy and an architecture document, and silently deleting the +sections would hide the fact that a decision is owed. A visible gap is +honest; a fabricated answer is not. + +=== Do not delete this file until every item below is resolved + +This file is the only marker that the work is outstanding. Deleting it +early does not finish the setup, it just conceals it — and the next +person or agent to arrive will reasonably assume the repo is complete. + +* *If you are a person:* delete this file yourself once the last item is +done. +* *If you are an agent:* resolve what you legitimately can, leave the +rest, and delete this file only when no token below remains anywhere in +the tree. Do not delete it to make a gate go green. + +Re-running the estate top-up tool will remove this file automatically +once nothing is outstanding, so the safest way to finish is to fix the +tokens and let the check confirm it. + +=== What is needed, and where it goes + +==== `+{{PROJECT_UNIQUE_STRENGTH}}+` + +What this does that its alternatives do not. + +Appears in: + +* `+.machine_readable/bot_directives/methodology.a2ml+` + +''''' + +Generated by the estate top-up pass. Rationale and the governing rulings +are in `+hyperpolymath/standards+`; the token vocabulary is +`+.machine_readable/ai/PLACEHOLDERS.adoc+` in `+rsr-template-repo+`. diff --git a/REQUIRES_INITIALISATION.md b/REQUIRES_INITIALISATION.md deleted file mode 100644 index 9f1a17e..0000000 --- a/REQUIRES_INITIALISATION.md +++ /dev/null @@ -1,54 +0,0 @@ - - -# REQUIRES INITIALISATION - -**This repository is not finished being set up.** 1 substitution token(s) across 1 file(s) still have no value. - -## Why this is not already done - -This repo was created from `hyperpolymath/rsr-template-repo`. The mint -(`just repo-init`) fills every token that has a single mechanical answer — -owner, repo, author, dates, licence, branch — and it has done so here. - -The tokens below are the ones it *deliberately cannot* answer. They need a -decision or a fact that exists only in your head: what this project is for, -what command builds it, which port the service listens on, whether a PGP key -is held at all. The template's own token vocabulary says as much — you cannot -sensibly answer "required invariants" in a thirty-second bootstrap. - -They were left **visibly unfilled on purpose**. The alternatives were both -worse: inventing plausible values would put confident falsehoods into a -security policy and an architecture document, and silently deleting the -sections would hide the fact that a decision is owed. A visible gap is -honest; a fabricated answer is not. - -## Do not delete this file until every item below is resolved - -This file is the only marker that the work is outstanding. Deleting it early -does not finish the setup, it just conceals it — and the next person or agent -to arrive will reasonably assume the repo is complete. - -- **If you are a person:** delete this file yourself once the last item is done. -- **If you are an agent:** resolve what you legitimately can, leave the rest, - and delete this file only when no token below remains anywhere in the tree. - Do not delete it to make a gate go green. - -Re-running the estate top-up tool will remove this file automatically once -nothing is outstanding, so the safest way to finish is to fix the tokens and -let the check confirm it. - -## What is needed, and where it goes - -### `{{PROJECT_UNIQUE_STRENGTH}}` - -What this does that its alternatives do not. - -Appears in: - -- `.machine_readable/bot_directives/methodology.a2ml` - ---- - -Generated by the estate top-up pass. Rationale and the governing rulings are -in `hyperpolymath/standards`; the token vocabulary is -`.machine_readable/ai/PLACEHOLDERS.adoc` in `rsr-template-repo`. diff --git a/RSR_OUTLINE.adoc b/RSR_OUTLINE.adoc index cde01e7..52c6838 100644 --- a/RSR_OUTLINE.adoc +++ b/RSR_OUTLINE.adoc @@ -146,8 +146,8 @@ project/ === Language Tiers -* **Tier 1** (Gold): Rust, Elixir, Zig, Ada, Haskell, ReScript -* **Tier 2** (Silver): Nickel, Racket, Guile Scheme, Nix +* **Tier 1** (Gold): Rust, Elixir, Zig, Ada, Haskell, AffineScript +* **Tier 2** (Silver): Nickel, Racket, Guile Scheme, Guix * **Infrastructure**: Guix channels, derivations === Required Files @@ -161,12 +161,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`) diff --git a/SECURITY.adoc b/SECURITY.adoc new file mode 100644 index 0000000..71062fa --- /dev/null +++ b/SECURITY.adoc @@ -0,0 +1,143 @@ +== Security Policy + +=== Supported Versions + +[cols=",",options="header",] +|=== +|Version |Supported +|0.1.x |:white_check_mark: +|=== + +=== Reporting a Vulnerability + +We take security vulnerabilities seriously. If you discover a security +issue, please report it responsibly. + +==== How to Report + +*DO NOT* open a public GitHub issue for security vulnerabilities. + +Instead, please report security issues via: + +[arabic] +. *Email*: security@axiom-jl.org (preferred) +. *GitLab Security Advisory*: Use the confidential issue feature +. *PGP Encrypted Email*: See `+.well-known/security.txt+` for our PGP +key + +==== What to Include + +Please include the following in your report: + +* Description of the vulnerability +* Steps to reproduce +* Potential impact assessment +* Any suggested fixes (optional) + +==== Response Timeline + +[cols=",",options="header",] +|=== +|Action |Timeline +|Acknowledgment |Within 48 hours +|Initial assessment |Within 7 days +|Status update |Every 14 days +|Fix release |Depends on severity +|=== + +==== Severity Levels + +[cols=",,",options="header",] +|=== +|Severity |Description |Target Fix Time +|Critical |Remote code execution, data breach |24-72 hours +|High |Privilege escalation, significant data exposure |7 days +|Medium |Limited data exposure, DoS |30 days +|Low |Minor issues, hardening |90 days +|=== + +=== Security Measures + +==== Code Security + +* *Memory Safety*: Rust and Zig backends provide memory safety +guarantees +* *Type Safety*: Julia’s type system prevents many classes of bugs +* *Formal Verification*: `+@prove+` macro enables mathematical +correctness proofs +* *Runtime Checks*: `+@ensure+` macro validates invariants at runtime + +==== Supply Chain Security + +* *Dependency Auditing*: Regular `+cargo audit+` and `+cargo deny+` +checks +* *SBOM Generation*: Software Bill of Materials available +* *Reproducible Builds*: Guix flake ensures reproducibility +* *Signed Releases*: All releases are signed with GPG + +==== Development Practices + +* *Code Review*: All changes require review +* *CI/CD Security*: Automated security scanning in pipeline +* *Secrets Management*: No secrets in repository +* *SPDX Headers*: All source files have license headers + +=== Security Features for Users + +==== Verification System + +Axiom.jl provides built-in security features for ML models: + +[source,julia] +---- +# Runtime bounds checking +@ensure all(0 .≤ output .≤ 1) "Output must be valid probabilities" + +# Formal verification +@prove BoundedOutputs(0.0, 1.0) model + +# Verification certificates +cert = generate_certificate(model, properties) +---- + +==== Deterministic Inference + +For safety-critical applications: + +[source,julia] +---- +Axiom.set_deterministic!(true) # Reproducible results +---- + +==== Input Validation + +[source,julia] +---- +@ensure valid_input(x) "Input validation failed" +@ensure no_nan(x) "Input contains NaN values" +---- + +=== Security Advisories + +Security advisories are published at: + +* GitHub Security Advisories +* `+.well-known/security.txt+` +* Mailing list (security-announce@axiom-jl.org) + +=== Acknowledgments + +We thank the following security researchers for responsible disclosure: + +_No vulnerabilities reported yet._ + +=== Contact + +* Security Team: security@axiom-jl.org +* PGP Key: See `+.well-known/security.txt+` +* Response Team: See `+MAINTAINERS.md+` + +''''' + +_This security policy follows https://www.rfc-editor.org/rfc/rfc9116[RFC +9116] and RSR security standards._ diff --git a/SECURITY.md b/SECURITY.md deleted file mode 100644 index 0aa4b2a..0000000 --- a/SECURITY.md +++ /dev/null @@ -1,128 +0,0 @@ - -# Security Policy - -## Supported Versions - -| Version | Supported | -| ------- | ------------------ | -| 0.1.x | :white_check_mark: | - -## Reporting a Vulnerability - -We take security vulnerabilities seriously. If you discover a security issue, please report it responsibly. - -### How to Report - -**DO NOT** open a public GitHub issue for security vulnerabilities. - -Instead, please report security issues via: - -1. **Email**: security@axiom-jl.org (preferred) -2. **GitLab Security Advisory**: Use the confidential issue feature -3. **PGP Encrypted Email**: See `.well-known/security.txt` for our PGP key - -### What to Include - -Please include the following in your report: - -- Description of the vulnerability -- Steps to reproduce -- Potential impact assessment -- Any suggested fixes (optional) - -### Response Timeline - -| Action | Timeline | -|--------|----------| -| Acknowledgment | Within 48 hours | -| Initial assessment | Within 7 days | -| Status update | Every 14 days | -| Fix release | Depends on severity | - -### Severity Levels - -| Severity | Description | Target Fix Time | -|----------|-------------|-----------------| -| Critical | Remote code execution, data breach | 24-72 hours | -| High | Privilege escalation, significant data exposure | 7 days | -| Medium | Limited data exposure, DoS | 30 days | -| Low | Minor issues, hardening | 90 days | - -## Security Measures - -### Code Security - -- **Memory Safety**: Rust and Zig backends provide memory safety guarantees -- **Type Safety**: Julia's type system prevents many classes of bugs -- **Formal Verification**: `@prove` macro enables mathematical correctness proofs -- **Runtime Checks**: `@ensure` macro validates invariants at runtime - -### Supply Chain Security - -- **Dependency Auditing**: Regular `cargo audit` and `cargo deny` checks -- **SBOM Generation**: Software Bill of Materials available -- **Reproducible Builds**: Nix flake ensures reproducibility -- **Signed Releases**: All releases are signed with GPG - -### Development Practices - -- **Code Review**: All changes require review -- **CI/CD Security**: Automated security scanning in pipeline -- **Secrets Management**: No secrets in repository -- **SPDX Headers**: All source files have license headers - -## Security Features for Users - -### Verification System - -Axiom.jl provides built-in security features for ML models: - -```julia -# Runtime bounds checking -@ensure all(0 .≤ output .≤ 1) "Output must be valid probabilities" - -# Formal verification -@prove BoundedOutputs(0.0, 1.0) model - -# Verification certificates -cert = generate_certificate(model, properties) -``` - -### Deterministic Inference - -For safety-critical applications: - -```julia -Axiom.set_deterministic!(true) # Reproducible results -``` - -### Input Validation - -```julia -@ensure valid_input(x) "Input validation failed" -@ensure no_nan(x) "Input contains NaN values" -``` - -## Security Advisories - -Security advisories are published at: - -- GitHub Security Advisories -- `.well-known/security.txt` -- Mailing list (security-announce@axiom-jl.org) - -## Acknowledgments - -We thank the following security researchers for responsible disclosure: - -*No vulnerabilities reported yet.* - -## Contact - -- Security Team: security@axiom-jl.org -- PGP Key: See `.well-known/security.txt` -- Response Team: See `MAINTAINERS.md` - ---- - -*This security policy follows [RFC 9116](https://www.rfc-editor.org/rfc/rfc9116) and RSR security standards.* diff --git a/TEST-NEEDS.adoc b/TEST-NEEDS.adoc new file mode 100644 index 0000000..e707cbf --- /dev/null +++ b/TEST-NEEDS.adoc @@ -0,0 +1,54 @@ +== TEST-NEEDS: Axiom.jl + +=== CRG Grade: C — ACHIEVED 2026-04-04 + +=== Current State + +[width="100%",cols="40%,26%,34%",options="header",] +|=== +|Category |Count |Details +|*Source modules* |38 |18,659 lines – largest Julia package in the set +|*Test files* |21 |3,556 lines, 604 @test/@testset +|*Benchmarks* |3 files |Exist +|*E2E tests* |0 |None +|=== + +=== What’s Missing + +==== E2E Tests + +* [ ] No end-to-end axiom verification pipeline test + +==== Aspect Tests + +* [ ] *Performance*: Benchmarks exist (3 files) – need verification they +run +* [ ] *Error handling*: No tests for inconsistent axiom sets, circular +definitions +* [ ] *Concurrency*: No parallel proof checking tests + +==== Benchmarks Status + +* [x] 3 benchmark files exist – best among Julia packages + +==== Self-Tests + +* [ ] No self-consistency check for the axiom system + +=== FLAGGED ISSUES + +* *604 tests across 21 test files* – best test coverage among Julia +packages +* *38 source files = ~16 tests/module* – reasonable but could improve +* *Benchmarks exist* – verify they actually run +* *0 E2E tests* for a foundational math library + +=== Priority: P2 (MEDIUM) – solid foundation, needs E2E and benchmark verification + +=== FAKE-FUZZ ALERT + +* `+tests/fuzz/placeholder.txt+` is a scorecard placeholder inherited +from rsr-template-repo — it does NOT provide real fuzz testing +* Replace with an actual fuzz harness (see +rsr-template-repo/tests/fuzz/README.adoc) or remove the file +* Priority: P2 — creates false impression of fuzz coverage diff --git a/TEST-NEEDS.md b/TEST-NEEDS.md deleted file mode 100644 index 2b47386..0000000 --- a/TEST-NEEDS.md +++ /dev/null @@ -1,42 +0,0 @@ -# TEST-NEEDS: Axiom.jl - -## CRG Grade: C — ACHIEVED 2026-04-04 - -## Current State - -| Category | Count | Details | -|----------|-------|---------| -| **Source modules** | 38 | 18,659 lines -- largest Julia package in the set | -| **Test files** | 21 | 3,556 lines, 604 @test/@testset | -| **Benchmarks** | 3 files | Exist | -| **E2E tests** | 0 | None | - -## What's Missing - -### E2E Tests -- [ ] No end-to-end axiom verification pipeline test - -### Aspect Tests -- [ ] **Performance**: Benchmarks exist (3 files) -- need verification they run -- [ ] **Error handling**: No tests for inconsistent axiom sets, circular definitions -- [ ] **Concurrency**: No parallel proof checking tests - -### Benchmarks Status -- [x] 3 benchmark files exist -- best among Julia packages - -### Self-Tests -- [ ] No self-consistency check for the axiom system - -## FLAGGED ISSUES -- **604 tests across 21 test files** -- best test coverage among Julia packages -- **38 source files = ~16 tests/module** -- reasonable but could improve -- **Benchmarks exist** -- verify they actually run -- **0 E2E tests** for a foundational math library - -## Priority: P2 (MEDIUM) -- solid foundation, needs E2E and benchmark verification - -## FAKE-FUZZ ALERT - -- `tests/fuzz/placeholder.txt` is a scorecard placeholder inherited from rsr-template-repo — it does NOT provide real fuzz testing -- Replace with an actual fuzz harness (see rsr-template-repo/tests/fuzz/README.adoc) or remove the file -- Priority: P2 — creates false impression of fuzz coverage diff --git a/TOPOLOGY.adoc b/TOPOLOGY.adoc new file mode 100644 index 0000000..7967b4b --- /dev/null +++ b/TOPOLOGY.adoc @@ -0,0 +1,294 @@ +== Axiom.jl - System Architecture + +.... + Axiom.jl - Provably Correct Machine Learning + ============================================ + + User API Layer + +-----------------------------------------------------------------+ + | @axiom @ensure @prove* Sequential/Chain/Pipeline | + | Dense Conv2d BatchNorm LayerNorm MaxPool Dropout ReLU | + | CouplingLayer ActNorm Inv1x1Conv RevBlock NormFlow | + | train!() compile() verify() from_pytorch() | + +-----------------------------------------------------------------+ + | | | | + v v v v + +----------+ +-----------+ +-----------+ +-----------+ + | DSL & | | Training | | Verifi- | | Integra- | + | Macros | | Loop | | cation | | tions | + |----------| |-----------| |-----------| |-----------| + | axiom_ | | optimiz- | | proper- | | hugging- | + | macro | | ers.jl | | ties.jl | | face.jl | + | ensure | | loss.jl | | checker | | pytorch | + | prove* | | train.jl | | certifi- | | ext | + | pipeline | | gradient* | | cates.jl | | | + +----------+ +-----------+ | serial- | +-----------+ + | ize.jl | + | proof_ | + | export | + +-----------+ + | + +-----------------------------+-----------------------------+ + | | | + v v v + +-----------+ +-----------+ +-----------+ + | SMTLib.jl | | Lean 4 | | Coq / | + | (bundled) | | Export* | | Isabelle* | + |-----------| +-----------+ +-----------+ + | z3, cvc5 | + | yices, | + | mathsat | + +-----------+ + + Backend Abstraction Layer (15 backends incl. SmartBackend) + +-----------------------------------------------------------------+ + | abstract.jl - AbstractBackend / set_backend! / compile() | + | SmartBackend (per-op dispatch) / MixedPrecision / self-healing | + +-----------------------------------------------------------------+ + | | | + v v v + +-----------+ +-----------+ +-----------+ + | Julia | | Zig | | GPU | + | Backend | | Backend | | Backends | + |-----------| |-----------| |-----------| + | (default) | | zig/ | | CUDA | + | reference | | axiom | | ROCm | + | impl | | .zig | | Metal | + | | | SIMD+MT | | | + +-----------+ +-----------+ +-----------+ + | + Coprocessor Backends (self-healing fallback) | + +-----------------------------------------------------------------+ + | TPU | NPU | DSP | PPU | Math | FPGA | VPU | QPU | Crypto | + |-----------------------------------------------------------------| + | Environment-based detection (AXIOM_*_AVAILABLE) | + | Strict mode: AXIOM_*_REQUIRED=1 prevents fallback | + | Self-healing: graceful degradation to JuliaBackend | + +-----------------------------------------------------------------+ + + * = disabled, stub, or placeholder +.... + +=== Completion Dashboard + +==== Core Framework + +[cols=",,",options="header",] +|=== +|Component |Status |Progress +|Type System (Tensor) |Done |`+██████████+` 100% +|Layer Definitions |Done |`+██████████+` 100% +|Activation Functions |Done |`+██████████+` 100% +|Optimizers (SGD/Adam) |Done |`+██████████+` 100% +|Loss Functions |Done |`+██████████+` 100% +|Training Loop |Done |`+██████████+` 90% +|Model Save/Load |Done |`+██████████+` 100% (binary) +|Autograd (Zygote) |Done |`+██████████+` 100% +|Data Utilities |Done |`+██████████+` 100% +|Model Containers |Done |`+██████████+` 100% +|=== + +==== Reversible Computing + +[cols=",,",options="header",] +|=== +|Component |Status |Progress +|CouplingLayer (affine) |Done |`+██████████+` 100% +|ActNorm (data-dep init) |Done |`+██████████+` 100% +|Invertible1x1Conv (LU) |Done |`+██████████+` 100% +|RevBlock (reversible) |Done |`+██████████+` 100% +|InvertibleSequential |Done |`+██████████+` 100% +|NormalizingFlow |Done |`+██████████+` 100% +|Custom Zygote adjoints |Done |`+██████████+` 100% +|Roundtrip verification |Done |`+██████████+` 100% +|=== + +==== DSL & Macros + +[cols=",,",options="header",] +|=== +|Component |Status |Progress +|@axiom macro |Done |`+██████████+` 100% +|@ensure macro |Done |`+██████████+` 100% +|@prove macro |Done |`+██████████+` 100% +|Pipeline DSL |Done |`+██████████+` 100% +|=== + +==== Verification System + +[cols=",,",options="header",] +|=== +|Component |Status |Progress +|Property Checking |Done |`+██████████+` 100% +|Proof Certificates |Done |`+██████████+` 100% (JSON+text) +|Serialization |Done |`+██████████+` 100% +|SMTLib.jl (bundled) |Done |`+████████░░+` 80% +|Lean 4 Export |Done |`+████████░░+` 80% (real tactics) +|Coq Export |Done |`+████████░░+` 80% (real tactics) +|Isabelle Export |Done |`+████████░░+` 80% (real tactics) +|Proof Import |Done |`+██████████+` 100% +|=== + +==== Backends - Julia (Reference) + +[cols=",,",options="header",] +|=== +|Component |Status |Progress +|matmul |Done |`+██████████+` 100% +|conv2d |Done |`+██████████+` 100% +|activations (all) |Done |`+██████████+` 100% +|batchnorm / layernorm |Done |`+██████████+` 100% +|pooling (max/avg/glob) |Done |`+██████████+` 100% +|dropout / flatten |Done |`+██████████+` 100% +|=== + +==== Backends - Zig (sole native backend, 320KB .so) + +[cols=",,",options="header",] +|=== +|Component |Status |Progress +|matmul (SIMD tiled) |Done |`+██████████+` 100% +|activations (15 funcs) |Done |`+██████████+` 100% +|conv2d + depthwise |Done |`+██████████+` 100% +|pooling (max/avg/glob) |Done |`+██████████+` 100% +|norm (batch/layer/rms) |Done |`+██████████+` 100% +|flash attention |Done |`+██████████+` 100% +|rotary embeddings |Done |`+██████████+` 100% +|Julia-side ccall wiring |Done |`+██████████+` 100% (17 ops) +|Compiled .so artifact |Done |`+██████████+` 100% (320KB) +|FFI exports (32 syms) |Done |`+██████████+` 100% +|SIMD GELU/sigmoid/tanh |Done |`+██████████+` 100% (3x speedup) +|Multi-threaded dispatch |Done |`+██████████+` 100% (4 threads) +|=== + +==== Backends - GPU Extensions + +[cols=",,",options="header",] +|=== +|Component |Status |Progress +|CUDA: matmul |Done |`+██████████+` 100% +|CUDA: relu |Done |`+██████████+` 100% +|CUDA: softmax |Done |`+██████████+` 100% +|CUDA: conv2d |Done |`+██████████+` 100% +|CUDA: batchnorm |Done |`+██████████+` 100% +|CUDA: pooling |Done |`+██████████+` 100% +|ROCm: matmul/relu/soft |Done |`+██████████+` 100% +|ROCm: conv2d/norm/pool |Done |`+██████████+` 100% +|Metal: matmul/relu/soft |Done |`+██████████+` 100% +|Metal: conv2d/norm/pool |Done |`+██████████+` 100% +|=== + +==== Backends - Coprocessor Dispatch + +[cols=",,",options="header",] +|=== +|Component |Status |Progress +|Backend type hierarchy |Done |`+██████████+` 100% +|Env-based detection |Done |`+██████████+` 100% +|Self-healing fallback |Done |`+██████████+` 100% +|Strict mode / required |Done |`+██████████+` 100% +|Runtime diagnostics |Done |`+██████████+` 100% +|Capability reporting |Done |`+██████████+` 100% +|TPU extension skeleton |Skel |`+██░░░░░░░░+` 20% +|NPU extension skeleton |Skel |`+██░░░░░░░░+` 20% +|DSP extension skeleton |Skel |`+██░░░░░░░░+` 20% +|PPU extension skeleton |Skel |`+██░░░░░░░░+` 20% +|Math extension skeleton |Skel |`+██░░░░░░░░+` 20% +|FPGA extension skeleton |Skel |`+██░░░░░░░░+` 20% +|VPU extension skeleton |Skel |`+██░░░░░░░░+` 20% +|QPU extension skeleton |Skel |`+██░░░░░░░░+` 20% +|Crypto ext. skeleton |Skel |`+██░░░░░░░░+` 20% +|=== + +==== Integrations + +[width="100%",cols="38%,12%,50%",options="header",] +|=== +|Component |Status |Progress +|PyTorch import/export |Done |`+██████████+` 90% + +|HuggingFace framework |Done |`+████████░░+` 80% + +|HF model converters |Done |`+████████░░+` 80% +(BERT/GPT2/ViT/ResNet/LLaMA/Whisper) + +|SafeTensors loader |Done |`+██████████+` 100% + +|Model Metadata |Done |`+████████░░+` 80% (bundle save/load) + +|Resource-aware dispatch |Done |`+██████████+` 100% +|=== + +==== Compile & Optimization + +[cols=",,",options="header",] +|=== +|Component |Status |Progress +|Backend dispatch |Done |`+██████████+` 100% +|SmartBackend (per-op) |Done |`+██████████+` 100% +|Mixed precision |Done |`+████████░░+` 80% (loss scaling) +|fold_batchnorm |Done |`+██████████+` 100% +|fold_constants |Done |`+██████████+` 100% +|dead code elimination |Done |`+██████████+` 100% +|aggressive opt pass |Done |`+██████████+` 100% +|=== + +==== Infrastructure + +[cols=",,",options="header",] +|=== +|Component |Status |Progress +|CI/CD (21 workflows) |Good |`+████████░░+` 80% +|Tests (283 passing) |Good |`+██████████+` 100% +|Benchmarks |Done |`+██████████+` 100% +|Documentation (wiki) |Done |`+██████████+` 100% +|RSR Compliance |Done |`+██████████+` 100% +|Bot directives (8) |Done |`+██████████+` 100% +|Contractiles (5) |Done |`+██████████+` 100% +|SCM files (5) |Done |`+██████████+` 100% +|=== + +=== Key Dependencies + +[cols=",,",options="header",] +|=== +|Dependency |Purpose |Required +|Julia >= 1.10 |Runtime |Yes +|LinearAlgebra |Matrix operations |Yes +|SHA |Proof certificate hashing |Yes +|JSON |Metadata serialization |Yes +|CUDA.jl |NVIDIA GPU acceleration |Optional +|AMDGPU.jl |AMD GPU acceleration |Optional +|Metal.jl |Apple GPU acceleration |Optional +|PyCall.jl |PyTorch interop |Optional +|Zig toolchain |Zig backend compilation |Optional +|Z3/CVC5 |SMT solver for @prove |Optional +|=== + +=== Overall: ~98% complete + +*Strongest areas:* Core layers, activations, reversible computing +(CouplingLayer/ActNorm/Inv1x1Conv/RevBlock/NormalizingFlow with custom +Zygote adjoints), Zig kernel implementations (sole native backend, 36 +exports, 395KB .so, SIMD + 4-thread dispatch), SmartBackend per-op +dispatch, SIMD-optimized Zig kernels (GELU 3x, RMSNorm 7x, sigmoid +2.9x), multi-threaded element-wise ops (>64K threshold), SMTLib, +coprocessor dispatch infrastructure (9 backends with setup guides and +hardware detection), compile optimizations (incl. mixed precision with +loss scaling), certificates, HuggingFace (7 architectures + +SafeTensors), RSR compliance (SPDX on all files), GPU extensions (full +coverage), autograd (Zygote), @prove (heuristic+SMT), proof export (real +tactics), backend-aware dispatch (LayerNorm/RMSNorm route through +backends), model save/load (binary + metadata bundle), external +benchmarks (Axiom vs Flux vs PyTorch), 283 tests passing *Weakest +areas:* Coprocessor skeletons (20% — need real hardware for end-to-end +integration) + +=== Ecosystem Context + +Axiom.jl is the flagship package in `+julia-ecosystem+` (part of +`+developer-ecosystem+` monorepo). 13 sibling COMPUTE packages share the +same backend abstraction: Cladistics.jl, BowtieRisk.jl, Cliometrics.jl, +KnotTheory.jl, HackenbushGames.jl, QuantumCircuit.jl, SMTLib.jl, +PolyglotFormalisms.jl, Causals.jl, SiliconCore.jl, LowLevel.jl, +ZeroProb.jl, ProvenCrypto.jl. diff --git a/TOPOLOGY.md b/TOPOLOGY.md deleted file mode 100644 index 7e00ab5..0000000 --- a/TOPOLOGY.md +++ /dev/null @@ -1,238 +0,0 @@ - -# Axiom.jl - System Architecture - -``` - Axiom.jl - Provably Correct Machine Learning - ============================================ - - User API Layer - +-----------------------------------------------------------------+ - | @axiom @ensure @prove* Sequential/Chain/Pipeline | - | Dense Conv2d BatchNorm LayerNorm MaxPool Dropout ReLU | - | CouplingLayer ActNorm Inv1x1Conv RevBlock NormFlow | - | train!() compile() verify() from_pytorch() | - +-----------------------------------------------------------------+ - | | | | - v v v v - +----------+ +-----------+ +-----------+ +-----------+ - | DSL & | | Training | | Verifi- | | Integra- | - | Macros | | Loop | | cation | | tions | - |----------| |-----------| |-----------| |-----------| - | axiom_ | | optimiz- | | proper- | | hugging- | - | macro | | ers.jl | | ties.jl | | face.jl | - | ensure | | loss.jl | | checker | | pytorch | - | prove* | | train.jl | | certifi- | | ext | - | pipeline | | gradient* | | cates.jl | | | - +----------+ +-----------+ | serial- | +-----------+ - | ize.jl | - | proof_ | - | export | - +-----------+ - | - +-----------------------------+-----------------------------+ - | | | - v v v - +-----------+ +-----------+ +-----------+ - | SMTLib.jl | | Lean 4 | | Coq / | - | (bundled) | | Export* | | Isabelle* | - |-----------| +-----------+ +-----------+ - | z3, cvc5 | - | yices, | - | mathsat | - +-----------+ - - Backend Abstraction Layer (15 backends incl. SmartBackend) - +-----------------------------------------------------------------+ - | abstract.jl - AbstractBackend / set_backend! / compile() | - | SmartBackend (per-op dispatch) / MixedPrecision / self-healing | - +-----------------------------------------------------------------+ - | | | - v v v - +-----------+ +-----------+ +-----------+ - | Julia | | Zig | | GPU | - | Backend | | Backend | | Backends | - |-----------| |-----------| |-----------| - | (default) | | zig/ | | CUDA | - | reference | | axiom | | ROCm | - | impl | | .zig | | Metal | - | | | SIMD+MT | | | - +-----------+ +-----------+ +-----------+ - | - Coprocessor Backends (self-healing fallback) | - +-----------------------------------------------------------------+ - | TPU | NPU | DSP | PPU | Math | FPGA | VPU | QPU | Crypto | - |-----------------------------------------------------------------| - | Environment-based detection (AXIOM_*_AVAILABLE) | - | Strict mode: AXIOM_*_REQUIRED=1 prevents fallback | - | Self-healing: graceful degradation to JuliaBackend | - +-----------------------------------------------------------------+ - - * = disabled, stub, or placeholder -``` - -## Completion Dashboard - -### Core Framework -| Component | Status | Progress | -|------------------------|--------|--------------------------------| -| Type System (Tensor) | Done | `██████████` 100% | -| Layer Definitions | Done | `██████████` 100% | -| Activation Functions | Done | `██████████` 100% | -| Optimizers (SGD/Adam) | Done | `██████████` 100% | -| Loss Functions | Done | `██████████` 100% | -| Training Loop | Done | `██████████` 90% | -| Model Save/Load | Done | `██████████` 100% (binary) | -| Autograd (Zygote) | Done | `██████████` 100% | -| Data Utilities | Done | `██████████` 100% | -| Model Containers | Done | `██████████` 100% | - -### Reversible Computing -| Component | Status | Progress | -|------------------------|--------|--------------------------------| -| CouplingLayer (affine) | Done | `██████████` 100% | -| ActNorm (data-dep init)| Done | `██████████` 100% | -| Invertible1x1Conv (LU) | Done | `██████████` 100% | -| RevBlock (reversible) | Done | `██████████` 100% | -| InvertibleSequential | Done | `██████████` 100% | -| NormalizingFlow | Done | `██████████` 100% | -| Custom Zygote adjoints | Done | `██████████` 100% | -| Roundtrip verification | Done | `██████████` 100% | - -### DSL & Macros -| Component | Status | Progress | -|------------------------|--------|--------------------------------| -| @axiom macro | Done | `██████████` 100% | -| @ensure macro | Done | `██████████` 100% | -| @prove macro | Done | `██████████` 100% | -| Pipeline DSL | Done | `██████████` 100% | - -### Verification System -| Component | Status | Progress | -|------------------------|--------|--------------------------------| -| Property Checking | Done | `██████████` 100% | -| Proof Certificates | Done | `██████████` 100% (JSON+text) | -| Serialization | Done | `██████████` 100% | -| SMTLib.jl (bundled) | Done | `████████░░` 80% | -| Lean 4 Export | Done | `████████░░` 80% (real tactics) | -| Coq Export | Done | `████████░░` 80% (real tactics) | -| Isabelle Export | Done | `████████░░` 80% (real tactics) | -| Proof Import | Done | `██████████` 100% | - -### Backends - Julia (Reference) -| Component | Status | Progress | -|------------------------|--------|--------------------------------| -| matmul | Done | `██████████` 100% | -| conv2d | Done | `██████████` 100% | -| activations (all) | Done | `██████████` 100% | -| batchnorm / layernorm | Done | `██████████` 100% | -| pooling (max/avg/glob) | Done | `██████████` 100% | -| dropout / flatten | Done | `██████████` 100% | - -### Backends - Zig (sole native backend, 320KB .so) -| Component | Status | Progress | -|------------------------|--------|--------------------------------| -| matmul (SIMD tiled) | Done | `██████████` 100% | -| activations (15 funcs) | Done | `██████████` 100% | -| conv2d + depthwise | Done | `██████████` 100% | -| pooling (max/avg/glob) | Done | `██████████` 100% | -| norm (batch/layer/rms) | Done | `██████████` 100% | -| flash attention | Done | `██████████` 100% | -| rotary embeddings | Done | `██████████` 100% | -| Julia-side ccall wiring| Done | `██████████` 100% (17 ops) | -| Compiled .so artifact | Done | `██████████` 100% (320KB) | -| FFI exports (32 syms) | Done | `██████████` 100% | -| SIMD GELU/sigmoid/tanh | Done | `██████████` 100% (3x speedup) | -| Multi-threaded dispatch| Done | `██████████` 100% (4 threads) | - -### Backends - GPU Extensions -| Component | Status | Progress | -|------------------------|--------|--------------------------------| -| CUDA: matmul | Done | `██████████` 100% | -| CUDA: relu | Done | `██████████` 100% | -| CUDA: softmax | Done | `██████████` 100% | -| CUDA: conv2d | Done | `██████████` 100% | -| CUDA: batchnorm | Done | `██████████` 100% | -| CUDA: pooling | Done | `██████████` 100% | -| ROCm: matmul/relu/soft | Done | `██████████` 100% | -| ROCm: conv2d/norm/pool | Done | `██████████` 100% | -| Metal: matmul/relu/soft| Done | `██████████` 100% | -| Metal: conv2d/norm/pool| Done | `██████████` 100% | - -### Backends - Coprocessor Dispatch -| Component | Status | Progress | -|------------------------|--------|--------------------------------| -| Backend type hierarchy | Done | `██████████` 100% | -| Env-based detection | Done | `██████████` 100% | -| Self-healing fallback | Done | `██████████` 100% | -| Strict mode / required | Done | `██████████` 100% | -| Runtime diagnostics | Done | `██████████` 100% | -| Capability reporting | Done | `██████████` 100% | -| TPU extension skeleton | Skel | `██░░░░░░░░` 20% | -| NPU extension skeleton | Skel | `██░░░░░░░░` 20% | -| DSP extension skeleton | Skel | `██░░░░░░░░` 20% | -| PPU extension skeleton | Skel | `██░░░░░░░░` 20% | -| Math extension skeleton| Skel | `██░░░░░░░░` 20% | -| FPGA extension skeleton| Skel | `██░░░░░░░░` 20% | -| VPU extension skeleton | Skel | `██░░░░░░░░` 20% | -| QPU extension skeleton | Skel | `██░░░░░░░░` 20% | -| Crypto ext. skeleton | Skel | `██░░░░░░░░` 20% | - -### Integrations -| Component | Status | Progress | -|------------------------|--------|--------------------------------| -| PyTorch import/export | Done | `██████████` 90% | -| HuggingFace framework | Done | `████████░░` 80% | -| HF model converters | Done | `████████░░` 80% (BERT/GPT2/ViT/ResNet/LLaMA/Whisper) | -| SafeTensors loader | Done | `██████████` 100% | -| Model Metadata | Done | `████████░░` 80% (bundle save/load) | -| Resource-aware dispatch| Done | `██████████` 100% | - -### Compile & Optimization -| Component | Status | Progress | -|------------------------|--------|--------------------------------| -| Backend dispatch | Done | `██████████` 100% | -| SmartBackend (per-op) | Done | `██████████` 100% | -| Mixed precision | Done | `████████░░` 80% (loss scaling) | -| fold_batchnorm | Done | `██████████` 100% | -| fold_constants | Done | `██████████` 100% | -| dead code elimination | Done | `██████████` 100% | -| aggressive opt pass | Done | `██████████` 100% | - -### Infrastructure -| Component | Status | Progress | -|------------------------|--------|--------------------------------| -| CI/CD (21 workflows) | Good | `████████░░` 80% | -| Tests (283 passing) | Good | `██████████` 100% | -| Benchmarks | Done | `██████████` 100% | -| Documentation (wiki) | Done | `██████████` 100% | -| RSR Compliance | Done | `██████████` 100% | -| Bot directives (8) | Done | `██████████` 100% | -| Contractiles (5) | Done | `██████████` 100% | -| SCM files (5) | Done | `██████████` 100% | - -## Key Dependencies - -| Dependency | Purpose | Required | -|----------------|----------------------------|----------| -| Julia >= 1.10 | Runtime | Yes | -| LinearAlgebra | Matrix operations | Yes | -| SHA | Proof certificate hashing | Yes | -| JSON | Metadata serialization | Yes | -| CUDA.jl | NVIDIA GPU acceleration | Optional | -| AMDGPU.jl | AMD GPU acceleration | Optional | -| Metal.jl | Apple GPU acceleration | Optional | -| PyCall.jl | PyTorch interop | Optional | -| Zig toolchain | Zig backend compilation | Optional | -| Z3/CVC5 | SMT solver for @prove | Optional | - -## Overall: ~98% complete - -**Strongest areas:** Core layers, activations, reversible computing (CouplingLayer/ActNorm/Inv1x1Conv/RevBlock/NormalizingFlow with custom Zygote adjoints), Zig kernel implementations (sole native backend, 36 exports, 395KB .so, SIMD + 4-thread dispatch), SmartBackend per-op dispatch, SIMD-optimized Zig kernels (GELU 3x, RMSNorm 7x, sigmoid 2.9x), multi-threaded element-wise ops (>64K threshold), SMTLib, coprocessor dispatch infrastructure (9 backends with setup guides and hardware detection), compile optimizations (incl. mixed precision with loss scaling), certificates, HuggingFace (7 architectures + SafeTensors), RSR compliance (SPDX on all files), GPU extensions (full coverage), autograd (Zygote), @prove (heuristic+SMT), proof export (real tactics), backend-aware dispatch (LayerNorm/RMSNorm route through backends), model save/load (binary + metadata bundle), external benchmarks (Axiom vs Flux vs PyTorch), 283 tests passing -**Weakest areas:** Coprocessor skeletons (20% — need real hardware for end-to-end integration) - -## Ecosystem Context - -Axiom.jl is the flagship package in `julia-ecosystem` (part of `developer-ecosystem` monorepo). -13 sibling COMPUTE packages share the same backend abstraction: Cladistics.jl, BowtieRisk.jl, -Cliometrics.jl, KnotTheory.jl, HackenbushGames.jl, QuantumCircuit.jl, SMTLib.jl, -PolyglotFormalisms.jl, Causals.jl, SiliconCore.jl, LowLevel.jl, ZeroProb.jl, ProvenCrypto.jl. diff --git a/benchmark/results_2026-02-20_framework-comparison.md b/benchmark/results_2026-02-20_framework-comparison.adoc similarity index 62% rename from benchmark/results_2026-02-20_framework-comparison.md rename to benchmark/results_2026-02-20_framework-comparison.adoc index 187a087..2e755e8 100644 --- a/benchmark/results_2026-02-20_framework-comparison.md +++ b/benchmark/results_2026-02-20_framework-comparison.adoc @@ -1,17 +1,18 @@ -# Axiom.jl External Framework Comparison — 2026-02-20 +== Axiom.jl External Framework Comparison — 2026-02-20 -## System -- **CPU**: Intel (i915 + Quadro M2000M laptop) -- **OS**: Fedora 43 Atomic (Linux 6.18.10) -- **Julia**: 1.12.5 -- **PyTorch**: 2.10.0+cpu (ATen/MKL) -- **Flux.jl**: 0.16+ (NNlib backend) -- **Axiom.jl**: 1.0.0 (SmartBackend: Zig 213KB + Julia/BLAS) -- **Method**: 50 iterations, 3 warmup, median timing, CPU-only +=== System -## Raw Timings (microseconds) +* *CPU*: Intel (i915 + Quadro M2000M laptop) +* *OS*: Fedora 43 Atomic (Linux 6.18.10) +* *Julia*: 1.12.5 +* *PyTorch*: 2.10.0+cpu (ATen/MKL) +* *Flux.jl*: 0.16+ (NNlib backend) +* *Axiom.jl*: 1.0.0 (SmartBackend: Zig 213KB + Julia/BLAS) +* *Method*: 50 iterations, 3 warmup, median timing, CPU-only -``` +=== Raw Timings (microseconds) + +.... ┌─────────────┬──────────────┬───────────────┬───────────────┬───────────────┬───────────────┐ │ Operation │ Size │ Axiom Smart │ Axiom Julia │ Flux.jl (μs) │ PyTorch (μs) │ ├─────────────┼──────────────┼───────────────┼───────────────┼───────────────┼───────────────┤ @@ -41,11 +42,11 @@ │ batchnorm │ 64×256 │ 84.5 │ 87.8 │ 8.1 │ 56.2 │ │ batchnorm │ 128×512 │ 357.9 │ 205.4 │ 28.2 │ 67.4 │ └─────────────┴──────────────┴───────────────┴───────────────┴───────────────┴───────────────┘ -``` +.... -## Speedup vs PyTorch (>1.0x = faster than PyTorch) +=== Speedup vs PyTorch (>1.0x = faster than PyTorch) -``` +.... ┌─────────────┬──────────────┬───────────────┬───────────────┬───────────────┐ │ Operation │ Size │ Axiom Smart │ Axiom Julia │ Flux.jl │ ├─────────────┼──────────────┼───────────────┼───────────────┼───────────────┤ @@ -75,81 +76,94 @@ │ batchnorm │ 64×256 │ 0.67x │ 0.64x │ 6.95x │ │ batchnorm │ 128×512 │ 0.19x │ 0.33x │ 2.39x │ └─────────────┴──────────────┴───────────────┴───────────────┴───────────────┘ -``` - -## Aggregate - -| Framework | Geometric Mean | Arithmetic Mean | Wins vs PyTorch | -|----------------|---------------|-----------------|-----------------| -| Axiom Smart | 0.73x | 3.57x | 11/25 | -| Axiom Julia | 0.52x | 2.12x | 11/25 (different ops) | -| Flux.jl | 0.82x | 4.57x | 11/25 | - -> All three Julia frameworks win small-batch operations (lower dispatch overhead than Python). -> PyTorch dominates medium-to-large element-wise operations (MKL VML + OpenMP threading). - -## Analysis - -### Where Axiom SmartBackend Wins vs PyTorch -- **Small inputs (1K elements)**: 1.3–30x faster — zero Python overhead, no tensor metadata -- **RMSNorm (all sizes)**: 2–30x faster — Zig SIMD inner loop has less dispatch overhead than PyTorch's nn.RMSNorm -- **LayerNorm (small)**: 3.3x faster — Zig SIMD at 32×128 -- **BatchNorm (small)**: 6.6x faster at 32×64 - -### Where PyTorch Wins -- **Sigmoid/GELU/Softmax at ≥100K**: 5–25x faster — PyTorch uses Intel MKL VML (Vector Math Library) which provides multi-threaded, AVX-512/AVX2 optimized transcendental functions (`exp`, `tanh`). Our Zig SIMD is single-threaded AVX-256. -- **Large LayerNorm** (64×768, 128×1024): 3–6x faster — same MKL advantage -- **Large softmax**: 25x faster at 128×50257 — MKL softmax kernel is heavily optimized - -### SmartBackend Impact -SmartBackend improves Axiom's geomean from **0.52x → 0.73x** vs PyTorch (40% improvement). -Key wins from Zig dispatch: -- GELU 1K: 16.3μs → 5.5μs (3x, routes to Zig SIMD) -- Sigmoid 1M: 11061μs → 5068μs (2.2x, routes to Zig SIMD) -- RMSNorm: 460μs → 72μs (6.4x, routes to Zig SIMD) -- LayerNorm: 397μs → 153μs (2.6x, routes to Zig) - -### Axiom vs Flux.jl -Axiom SmartBackend beats Flux on: -- **Sigmoid** (all sizes): Zig SIMD vs Flux broadcasting -- **GELU** (1K, 1M): Zig SIMD vectorization -- **LayerNorm** (64×768): Zig dispatch -- **Softmax** (small): Zig vectorized - -Flux beats Axiom on: -- **BatchNorm**: NNlib has highly optimized batched normalization -- **ReLU** (100K): NNlib fused kernel -- **RMSNorm**: Manual broadcast is surprisingly fast in Flux - -### Root Cause: Why PyTorch is Faster at Scale - -PyTorch's ATen C++ library uses: -1. **Intel MKL VML** — vectorized math functions (`vsSigmoid`, `vsTanh`, `vsExp`) with AVX-512, multi-threaded -2. **OpenMP threading** — automatic parallelism across CPU cores -3. **In-place operations** — fewer memory allocations -4. **Fused kernels** — compound operations like GELU don't create intermediates - -Our Zig kernels are: -1. Single-threaded (uses only one core) -2. AVX-256 only (8-wide `@Vector(8, f32)`) -3. Separate allocation per output - -### Recommendations for Axiom v1.0 - -1. **Threading**: Add `@threadlocal` or Zig thread pool for element-wise ops at ≥100K elements -2. **AVX-512**: Detect and use `@Vector(16, f32)` when available -3. **In-place variants**: Add `backend_sigmoid!()` etc. to avoid allocation -4. **Fused kernels**: Implement `gelu_and_multiply`, `layernorm_and_residual` -5. **Softmax**: The 128×50257 case needs multi-threaded reduction - -### Honest Assessment - -Axiom.jl at v1.0 is **competitive with PyTorch for small-to-medium workloads** and -**RMSNorm/LayerNorm are faster at all sizes**. For large element-wise operations, -PyTorch's MKL integration gives it a 5–25x advantage that can only be closed with -threading and wider SIMD. This is expected — PyTorch has had thousands of -engineer-years of optimization. - -**The differentiator is not raw speed — it's provable correctness.** -No other framework offers `@ensure`, `@prove`, and proof certificates alongside -competitive kernel performance. +.... + +=== Aggregate + +[width="100%",cols="25%,23%,26%,26%",options="header",] +|=== +|Framework |Geometric Mean |Arithmetic Mean |Wins vs PyTorch +|Axiom Smart |0.73x |3.57x |11/25 +|Axiom Julia |0.52x |2.12x |11/25 (different ops) +|Flux.jl |0.82x |4.57x |11/25 +|=== + +____ +All three Julia frameworks win small-batch operations (lower dispatch +overhead than Python). PyTorch dominates medium-to-large element-wise +operations (MKL VML + OpenMP threading). +____ + +=== Analysis + +==== Where Axiom SmartBackend Wins vs PyTorch + +* *Small inputs (1K elements)*: 1.3–30x faster — zero Python overhead, +no tensor metadata +* *RMSNorm (all sizes)*: 2–30x faster — Zig SIMD inner loop has less +dispatch overhead than PyTorch’s nn.RMSNorm +* *LayerNorm (small)*: 3.3x faster — Zig SIMD at 32×128 +* *BatchNorm (small)*: 6.6x faster at 32×64 + +==== Where PyTorch Wins + +* *Sigmoid/GELU/Softmax at ≥100K*: 5–25x faster — PyTorch uses Intel MKL +VML (Vector Math Library) which provides multi-threaded, AVX-512/AVX2 +optimized transcendental functions (`+exp+`, `+tanh+`). Our Zig SIMD is +single-threaded AVX-256. +* *Large LayerNorm* (64×768, 128×1024): 3–6x faster — same MKL advantage +* *Large softmax*: 25x faster at 128×50257 — MKL softmax kernel is +heavily optimized + +==== SmartBackend Impact + +SmartBackend improves Axiom’s geomean from *0.52x → 0.73x* vs PyTorch +(40% improvement). Key wins from Zig dispatch: - GELU 1K: 16.3μs → 5.5μs +(3x, routes to Zig SIMD) - Sigmoid 1M: 11061μs → 5068μs (2.2x, routes to +Zig SIMD) - RMSNorm: 460μs → 72μs (6.4x, routes to Zig SIMD) - +LayerNorm: 397μs → 153μs (2.6x, routes to Zig) + +==== Axiom vs Flux.jl + +Axiom SmartBackend beats Flux on: - *Sigmoid* (all sizes): Zig SIMD vs +Flux broadcasting - *GELU* (1K, 1M): Zig SIMD vectorization - +*LayerNorm* (64×768): Zig dispatch - *Softmax* (small): Zig vectorized + +Flux beats Axiom on: - *BatchNorm*: NNlib has highly optimized batched +normalization - *ReLU* (100K): NNlib fused kernel - *RMSNorm*: Manual +broadcast is surprisingly fast in Flux + +==== Root Cause: Why PyTorch is Faster at Scale + +PyTorch’s ATen C++ library uses: 1. *Intel MKL VML* — vectorized math +functions (`+vsSigmoid+`, `+vsTanh+`, `+vsExp+`) with AVX-512, +multi-threaded 2. *OpenMP threading* — automatic parallelism across CPU +cores 3. *In-place operations* — fewer memory allocations 4. *Fused +kernels* — compound operations like GELU don’t create intermediates + +Our Zig kernels are: 1. Single-threaded (uses only one core) 2. AVX-256 +only (8-wide `+@Vector(8, f32)+`) 3. Separate allocation per output + +==== Recommendations for Axiom v1.0 + +[arabic] +. *Threading*: Add `+@threadlocal+` or Zig thread pool for element-wise +ops at ≥100K elements +. *AVX-512*: Detect and use `+@Vector(16, f32)+` when available +. *In-place variants*: Add `+backend_sigmoid!()+` etc. to avoid +allocation +. *Fused kernels*: Implement `+gelu_and_multiply+`, +`+layernorm_and_residual+` +. *Softmax*: The 128×50257 case needs multi-threaded reduction + +==== Honest Assessment + +Axiom.jl at v1.0 is *competitive with PyTorch for small-to-medium +workloads* and *RMSNorm/LayerNorm are faster at all sizes*. For large +element-wise operations, PyTorch’s MKL integration gives it a 5–25x +advantage that can only be closed with threading and wider SIMD. This is +expected — PyTorch has had thousands of engineer-years of optimization. + +*The differentiator is not raw speed — it’s provable correctness.* No +other framework offers `+@ensure+`, `+@prove+`, and proof certificates +alongside competitive kernel performance. diff --git a/benchmark/results_2026-02-20_julia-rust-zig.md b/benchmark/results_2026-02-20_julia-rust-zig.adoc similarity index 62% rename from benchmark/results_2026-02-20_julia-rust-zig.md rename to benchmark/results_2026-02-20_julia-rust-zig.adoc index ac54a56..6cac4ee 100644 --- a/benchmark/results_2026-02-20_julia-rust-zig.md +++ b/benchmark/results_2026-02-20_julia-rust-zig.adoc @@ -1,22 +1,26 @@ -# Axiom.jl Benchmark Results — 2026-02-20 +== Axiom.jl Benchmark Results — 2026-02-20 -## System -- **CPU**: Intel (i915 + Quadro M2000M laptop) -- **OS**: Fedora 43 Atomic (Linux 6.18.10) -- **Julia**: 1.11+ -- **Zig**: 0.15.2 (ReleaseFast) -- **Rust**: nightly (release) -- **Method**: 50 iterations, 3 warmup, median timing +=== System -## Binary Sizes -| Backend | Size | -|---------|------| -| Rust | 1990 KB | -| Zig | 213 KB | +* *CPU*: Intel (i915 + Quadro M2000M laptop) +* *OS*: Fedora 43 Atomic (Linux 6.18.10) +* *Julia*: 1.11+ +* *Zig*: 0.15.2 (ReleaseFast) +* *Rust*: nightly (release) +* *Method*: 50 iterations, 3 warmup, median timing -## Results (Post-SIMD Optimization) +=== Binary Sizes -``` +[cols=",",options="header",] +|=== +|Backend |Size +|Rust |1990 KB +|Zig |213 KB +|=== + +=== Results (Post-SIMD Optimization) + +.... ┌─────────────┬──────────────┬───────────────┬───────────────┬───────────────┬─────────────┬─────────────┐ │ Operation │ Size │ Julia (μs) │ Rust (μs) │ Zig (μs) │ Rust vs Jul │ Zig vs Jul │ ├─────────────┼──────────────┼───────────────┼───────────────┼───────────────┼─────────────┼─────────────┤ @@ -46,55 +50,70 @@ │ batchnorm │ 64×256 │ 46.0 │ 117.7 │ 53.6 │ 0.39x │ 0.86x │ │ batchnorm │ 128×512 │ 197.1 │ 596.4 │ 346.5 │ 0.33x │ 0.57x │ └─────────────┴──────────────┴───────────────┴───────────────┴───────────────┴─────────────┴─────────────┘ -``` - -## Aggregate - -| Backend | Geometric Mean | Arithmetic Mean | -|---------|---------------|-----------------| -| Rust | 0.49x | 0.86x | -| Zig | 1.01x | 1.99x | - -> Values >1.0x mean native backend is faster than Julia. - -## Analysis - -### Zig Wins (dispatch-worthy) -- **RMSNorm**: 6.5–7.3x faster — SIMD-optimized inner loop dominates -- **GELU**: 3.0–3.5x faster — SIMD `@exp` vectorization (was 0.55x before SIMD!) -- **Sigmoid**: 1.1–2.9x faster — SIMD `@exp` path -- **LayerNorm**: 1.2–2.6x faster — consistent advantage at all sizes -- **Softmax (small/medium)**: 1.0–1.4x faster - -### Julia Wins (keep on BLAS) -- **MatMul**: 7–50x faster — Julia calls OpenBLAS/MKL; native backends use hand-written tiled matmul -- **BatchNorm**: 1.2–1.8x faster at large sizes — row-major conversion overhead in FFI path -- **ReLU**: near-parity but FFI overhead makes Julia preferable - -### GELU SIMD Optimization Impact -The biggest win of this session — GELU went from Julia's worst Zig dispatch to its best: - -| Size | Before SIMD | After SIMD | Improvement | -|------|------------|------------|-------------| -| 1K | 0.52x | 3.10x | **6.0x** | -| 100K | 0.57x | 3.45x | **6.1x** | -| 1M | 0.55x | 2.96x | **5.4x** | - -Root cause: scalar `math.tanh()` loop replaced with SIMD `@exp` vectorization -using identity `tanh(z) = 1 - 2/(exp(2z) + 1)`. - -### Zig vs Rust -Zig beats Rust on every single benchmark: -- 9.3x smaller binary (213KB vs 1990KB) -- Faster compilation (seconds vs minutes) -- First-class SIMD (no crate dependencies) -- RMSNorm: Zig 7.3x vs Rust 1.7x (Zig 4.3x faster than Rust) -- GELU: Zig 3.5x vs Rust 1.1x (Zig 3.2x faster than Rust) - -### SmartBackend Dispatch Table (implemented) -1. **MatMul**: Julia/BLAS — native backends cannot compete -2. **GELU**: Zig — 3.0–3.5x faster after SIMD optimization -3. **RMSNorm/LayerNorm/Sigmoid**: Zig by default -4. **Softmax**: Zig for small batches (<50K classes), Julia for large -5. **BatchNorm/ReLU**: Julia — FFI overhead negates kernel advantage -6. **Conv2d**: Julia — BLAS-based +.... + +=== Aggregate + +[cols=",,",options="header",] +|=== +|Backend |Geometric Mean |Arithmetic Mean +|Rust |0.49x |0.86x +|Zig |1.01x |1.99x +|=== + +____ +Values >1.0x mean native backend is faster than Julia. +____ + +=== Analysis + +==== Zig Wins (dispatch-worthy) + +* *RMSNorm*: 6.5–7.3x faster — SIMD-optimized inner loop dominates +* *GELU*: 3.0–3.5x faster — SIMD `+@exp+` vectorization (was 0.55x +before SIMD!) +* *Sigmoid*: 1.1–2.9x faster — SIMD `+@exp+` path +* *LayerNorm*: 1.2–2.6x faster — consistent advantage at all sizes +* *Softmax (small/medium)*: 1.0–1.4x faster + +==== Julia Wins (keep on BLAS) + +* *MatMul*: 7–50x faster — Julia calls OpenBLAS/MKL; native backends use +hand-written tiled matmul +* *BatchNorm*: 1.2–1.8x faster at large sizes — row-major conversion +overhead in FFI path +* *ReLU*: near-parity but FFI overhead makes Julia preferable + +==== GELU SIMD Optimization Impact + +The biggest win of this session — GELU went from Julia’s worst Zig +dispatch to its best: + +[cols=",,,",options="header",] +|=== +|Size |Before SIMD |After SIMD |Improvement +|1K |0.52x |3.10x |*6.0x* +|100K |0.57x |3.45x |*6.1x* +|1M |0.55x |2.96x |*5.4x* +|=== + +Root cause: scalar `+math.tanh()+` loop replaced with SIMD `+@exp+` +vectorization using identity `+tanh(z) = 1 - 2/(exp(2z) + 1)+`. + +==== Zig vs Rust + +Zig beats Rust on every single benchmark: - 9.3x smaller binary (213KB +vs 1990KB) - Faster compilation (seconds vs minutes) - First-class SIMD +(no crate dependencies) - RMSNorm: Zig 7.3x vs Rust 1.7x (Zig 4.3x +faster than Rust) - GELU: Zig 3.5x vs Rust 1.1x (Zig 3.2x faster than +Rust) + +==== SmartBackend Dispatch Table (implemented) + +[arabic] +. *MatMul*: Julia/BLAS — native backends cannot compete +. *GELU*: Zig — 3.0–3.5x faster after SIMD optimization +. *RMSNorm/LayerNorm/Sigmoid*: Zig by default +. *Softmax*: Zig for small batches (<50K classes), Julia for large +. *BatchNorm/ReLU*: Julia — FFI overhead negates kernel advantage +. *Conv2d*: Julia — BLAS-based diff --git a/crypto/README.adoc b/crypto/README.adoc new file mode 100644 index 0000000..7c75a88 --- /dev/null +++ b/crypto/README.adoc @@ -0,0 +1,127 @@ +== axiom_crypto + +Hybrid *Ed448 + Dilithium5 (ML-DSA-87)* signing primitives for Axiom.jl +verification certificates, exposed as a C-ABI `+cdylib+` for `+ccall+` +from Julia. This is the estate Trustfile hybrid signature scheme: a +classical signature (Ed448 / EdDSA over Curve448, RFC 8032) plus a +post-quantum signature (Dilithium5 / ML-DSA-87, FIPS 204), both required +to pass. + +No hand-rolled cryptography: Ed448 goes through the system libcrypto +(OpenSSL 3.x) via the vetted https://docs.rs/openssl[`+openssl+`] crate; +Dilithium5 goes through the vetted +https://docs.rs/pqcrypto-dilithium[`+pqcrypto-dilithium+`] crate +(PQClean reference implementation). + +This mirrors the algorithm choice used by `+opsm_ex/native/opsm_pq_nif+` +(the Elixir/BEAM reference implementation in +`+odds-and-sods-package-manager+`), but is a fresh, dependency-free (of +that project) Rust `+cdylib+` — Axiom.jl does not depend on Elixir/BEAM. + +=== Build + +[source,sh] +---- +cd crypto +cargo build --release +cargo test +---- + +Or via the repo `+Justfile+`: `+just build-crypto+` (from the Axiom.jl +root). + +Output: `+crypto/target/release/libaxiom_crypto.so+` (Linux) / +`+.dylib+` (macOS) / `+.dll+` (Windows). `+crypto/target/+` is +git-ignored; the compiled shared library is a build artifact, not +source. + +=== Private key custody — NEVER commit private keys + +This crate never reads or writes key material to disk on its own. Keys +are either: + +* generated in-memory for tests / examples (`+*_keypair+` functions), or +* generated and held out-of-band by an HSM or an offline signing +process, with only the *public* keys embedded in a certificate. + +No `+.pem+`/`+.key+` file produced by a real signing key should ever +enter this repository. See `+ROADMAP.adoc+` for the custody story. + +=== C ABI + +Every exported function is `+extern "C"+`, `+#[no_mangle]+`. Convention: + +* *Fixed-size outputs* (public/secret keys, Ed448 signatures) are +written into a caller-allocated buffer. The required size is given by a +paired `+axiom_crypto_*_len()+` getter — call it first, allocate that +many bytes, then pass the buffer pointer. +* *Variable/bounded-size outputs* (Dilithium5 signatures) are written +into a caller-allocated buffer sized by +`+axiom_crypto_dilithium5_signature_maxlen()+`; the actual length +written is returned through an out-parameter +`+sig_len_out: *mut usize+`. +* *Every function returns `+i32+`.* For keypair/sign functions: `+0+` = +OK, negative = error (`+AXIOM_CRYPTO_ERR_NULL_PTR = -1+`, +`+AXIOM_CRYPTO_ERR_BAD_LENGTH = -2+`, +`+AXIOM_CRYPTO_ERR_CRYPTO_FAILURE = -3+`). For verify functions: `+1+` = +signature valid, `+0+` = signature invalid, negative = the call itself +could not be carried out (distinct from "`ran and failed`" — a bad +pointer is not the same claim as "`this certificate is forged`"). +* *No alloc+free pairs.* All buffers are caller-owned; there is no +`+axiom_crypto_free+`. This keeps the Julia side to plain `+ccall+` + +`+Vector{UInt8}+` with no foreign-pointer finalizer needed. + +==== Length getters + +[cols=",",options="header",] +|=== +|Function |Returns +|`+axiom_crypto_ed448_public_key_len() -> usize+` |57 +|`+axiom_crypto_ed448_secret_key_len() -> usize+` |57 +|`+axiom_crypto_ed448_signature_len() -> usize+` |114 +|`+axiom_crypto_dilithium5_public_key_len() -> usize+` |2592 +|`+axiom_crypto_dilithium5_secret_key_len() -> usize+` |4896 +|`+axiom_crypto_dilithium5_signature_maxlen() -> usize+` |4627 +|=== + +==== Ed448 + +[source,c] +---- +int32_t axiom_crypto_ed448_keypair(uint8_t *pk_out, uint8_t *sk_out); + +int32_t axiom_crypto_ed448_sign( + const uint8_t *msg_ptr, size_t msg_len, + const uint8_t *sk_ptr, + uint8_t *sig_out); + +int32_t axiom_crypto_ed448_verify( + const uint8_t *msg_ptr, size_t msg_len, + const uint8_t *sig_ptr, + const uint8_t *pk_ptr); // returns 1/0/negative, see above +---- + +==== Dilithium5 (ML-DSA-87) + +[source,c] +---- +int32_t axiom_crypto_dilithium5_keypair(uint8_t *pk_out, uint8_t *sk_out); + +int32_t axiom_crypto_dilithium5_sign( + const uint8_t *msg_ptr, size_t msg_len, + const uint8_t *sk_ptr, + uint8_t *sig_out, size_t *sig_len_out); + +int32_t axiom_crypto_dilithium5_verify( + const uint8_t *msg_ptr, size_t msg_len, + const uint8_t *sig_ptr, size_t sig_len, + const uint8_t *pk_ptr); // returns 1/0/negative, see above +---- + +=== Julia usage + +See `+src/verification/signing.jl+` in the Axiom.jl root — it loads this +library via `+Libdl+`, exposes `+generate_hybrid_keypair()+`, +`+hybrid_sign(content, keys)+`, and +`+hybrid_verify(content, sig, pubkeys)+`, and degrades gracefully (clear +error, not a crash) when the shared library has not been built. diff --git a/crypto/README.md b/crypto/README.md deleted file mode 100644 index e94a0f3..0000000 --- a/crypto/README.md +++ /dev/null @@ -1,119 +0,0 @@ - -# axiom_crypto - -Hybrid **Ed448 + Dilithium5 (ML-DSA-87)** signing primitives for Axiom.jl -verification certificates, exposed as a C-ABI `cdylib` for `ccall` from -Julia. This is the estate Trustfile hybrid signature scheme: a classical -signature (Ed448 / EdDSA over Curve448, RFC 8032) plus a post-quantum -signature (Dilithium5 / ML-DSA-87, FIPS 204), both required to pass. - -No hand-rolled cryptography: Ed448 goes through the system libcrypto -(OpenSSL 3.x) via the vetted [`openssl`](https://docs.rs/openssl) crate; -Dilithium5 goes through the vetted -[`pqcrypto-dilithium`](https://docs.rs/pqcrypto-dilithium) crate (PQClean -reference implementation). - -This mirrors the algorithm choice used by `opsm_ex/native/opsm_pq_nif` (the -Elixir/BEAM reference implementation in `odds-and-sods-package-manager`), but -is a fresh, dependency-free (of that project) Rust `cdylib` — Axiom.jl does -not depend on Elixir/BEAM. - -## Build - -```sh -cd crypto -cargo build --release -cargo test -``` - -Or via the repo `Justfile`: `just build-crypto` (from the Axiom.jl root). - -Output: `crypto/target/release/libaxiom_crypto.so` (Linux) / -`.dylib` (macOS) / `.dll` (Windows). `crypto/target/` is git-ignored; the -compiled shared library is a build artifact, not source. - -## Private key custody — NEVER commit private keys - -This crate never reads or writes key material to disk on its own. Keys are -either: - -- generated in-memory for tests / examples (`*_keypair` functions), or -- generated and held out-of-band by an HSM or an offline signing process, - with only the **public** keys embedded in a certificate. - -No `.pem`/`.key` file produced by a real signing key should ever enter this -repository. See `ROADMAP.adoc` for the custody story. - -## C ABI - -Every exported function is `extern "C"`, `#[no_mangle]`. Convention: - -- **Fixed-size outputs** (public/secret keys, Ed448 signatures) are written - into a caller-allocated buffer. The required size is given by a paired - `axiom_crypto_*_len()` getter — call it first, allocate that many bytes, - then pass the buffer pointer. -- **Variable/bounded-size outputs** (Dilithium5 signatures) are written into - a caller-allocated buffer sized by `axiom_crypto_dilithium5_signature_maxlen()`; - the actual length written is returned through an out-parameter - `sig_len_out: *mut usize`. -- **Every function returns `i32`.** For keypair/sign functions: `0` = OK, - negative = error (`AXIOM_CRYPTO_ERR_NULL_PTR = -1`, - `AXIOM_CRYPTO_ERR_BAD_LENGTH = -2`, `AXIOM_CRYPTO_ERR_CRYPTO_FAILURE = -3`). - For verify functions: `1` = signature valid, `0` = signature invalid, - negative = the call itself could not be carried out (distinct from "ran - and failed" — a bad pointer is not the same claim as "this certificate is - forged"). -- **No alloc+free pairs.** All buffers are caller-owned; there is no - `axiom_crypto_free`. This keeps the Julia side to plain `ccall` + - `Vector{UInt8}` with no foreign-pointer finalizer needed. - -### Length getters - -| Function | Returns | -|---|---| -| `axiom_crypto_ed448_public_key_len() -> usize` | 57 | -| `axiom_crypto_ed448_secret_key_len() -> usize` | 57 | -| `axiom_crypto_ed448_signature_len() -> usize` | 114 | -| `axiom_crypto_dilithium5_public_key_len() -> usize` | 2592 | -| `axiom_crypto_dilithium5_secret_key_len() -> usize` | 4896 | -| `axiom_crypto_dilithium5_signature_maxlen() -> usize` | 4627 | - -### Ed448 - -```c -int32_t axiom_crypto_ed448_keypair(uint8_t *pk_out, uint8_t *sk_out); - -int32_t axiom_crypto_ed448_sign( - const uint8_t *msg_ptr, size_t msg_len, - const uint8_t *sk_ptr, - uint8_t *sig_out); - -int32_t axiom_crypto_ed448_verify( - const uint8_t *msg_ptr, size_t msg_len, - const uint8_t *sig_ptr, - const uint8_t *pk_ptr); // returns 1/0/negative, see above -``` - -### Dilithium5 (ML-DSA-87) - -```c -int32_t axiom_crypto_dilithium5_keypair(uint8_t *pk_out, uint8_t *sk_out); - -int32_t axiom_crypto_dilithium5_sign( - const uint8_t *msg_ptr, size_t msg_len, - const uint8_t *sk_ptr, - uint8_t *sig_out, size_t *sig_len_out); - -int32_t axiom_crypto_dilithium5_verify( - const uint8_t *msg_ptr, size_t msg_len, - const uint8_t *sig_ptr, size_t sig_len, - const uint8_t *pk_ptr); // returns 1/0/negative, see above -``` - -## Julia usage - -See `src/verification/signing.jl` in the Axiom.jl root — it loads this -library via `Libdl`, exposes `generate_hybrid_keypair()`, -`hybrid_sign(content, keys)`, and `hybrid_verify(content, sig, pubkeys)`, -and degrades gracefully (clear error, not a crash) when the shared library -has not been built. diff --git a/docs/berrywiki/ABI.adoc b/docs/berrywiki/ABI.adoc new file mode 100644 index 0000000..41b0ab8 --- /dev/null +++ b/docs/berrywiki/ABI.adoc @@ -0,0 +1,10 @@ +== ABI + +Stable Idris2-facing and Zig FFI layout rules. + +Axiom keeps the mathematical API and proof-oriented contracts while +delegating supported tensor primitives through the shared accelerator +ABI. + +See [[Home]] for the project boundary and the repository +machine-readable state for exact fields. diff --git a/docs/berrywiki/ABI.md b/docs/berrywiki/ABI.md deleted file mode 100644 index 875f754..0000000 --- a/docs/berrywiki/ABI.md +++ /dev/null @@ -1,18 +0,0 @@ - - -# ABI - -Stable Idris2-facing and Zig FFI layout rules. - -Axiom keeps the mathematical API and proof-oriented contracts while delegating supported tensor primitives through the shared accelerator ABI. - -See [[Home]] for the project boundary and the repository machine-readable state for exact fields. diff --git a/docs/berrywiki/Architecture.adoc b/docs/berrywiki/Architecture.adoc new file mode 100644 index 0000000..e3a1dc9 --- /dev/null +++ b/docs/berrywiki/Architecture.adoc @@ -0,0 +1,10 @@ +== Architecture + +Boundaries, ownership, and data flow. + +Axiom keeps the mathematical API and proof-oriented contracts while +delegating supported tensor primitives through the shared accelerator +ABI. + +See [[Home]] for the project boundary and the repository +machine-readable state for exact fields. diff --git a/docs/berrywiki/Architecture.md b/docs/berrywiki/Architecture.md deleted file mode 100644 index 0962e50..0000000 --- a/docs/berrywiki/Architecture.md +++ /dev/null @@ -1,18 +0,0 @@ - - -# Architecture - -Boundaries, ownership, and data flow. - -Axiom keeps the mathematical API and proof-oriented contracts while delegating supported tensor primitives through the shared accelerator ABI. - -See [[Home]] for the project boundary and the repository machine-readable state for exact fields. diff --git a/docs/berrywiki/Axiom-Kernels.adoc b/docs/berrywiki/Axiom-Kernels.adoc new file mode 100644 index 0000000..6aa3a66 --- /dev/null +++ b/docs/berrywiki/Axiom-Kernels.adoc @@ -0,0 +1,10 @@ +== Axiom-Kernels + +Axiom-derived pointwise, binary, and attention coverage. + +Axiom keeps the mathematical API and proof-oriented contracts while +delegating supported tensor primitives through the shared accelerator +ABI. + +See [[Home]] for the project boundary and the repository +machine-readable state for exact fields. diff --git a/docs/berrywiki/Axiom-Kernels.md b/docs/berrywiki/Axiom-Kernels.md deleted file mode 100644 index 99071ba..0000000 --- a/docs/berrywiki/Axiom-Kernels.md +++ /dev/null @@ -1,18 +0,0 @@ - - -# Axiom-Kernels - -Axiom-derived pointwise, binary, and attention coverage. - -Axiom keeps the mathematical API and proof-oriented contracts while delegating supported tensor primitives through the shared accelerator ABI. - -See [[Home]] for the project boundary and the repository machine-readable state for exact fields. diff --git a/docs/berrywiki/Backends.adoc b/docs/berrywiki/Backends.adoc new file mode 100644 index 0000000..7fdac66 --- /dev/null +++ b/docs/berrywiki/Backends.adoc @@ -0,0 +1,10 @@ +== Backends + +Backend/provider registration and selection. + +Axiom keeps the mathematical API and proof-oriented contracts while +delegating supported tensor primitives through the shared accelerator +ABI. + +See [[Home]] for the project boundary and the repository +machine-readable state for exact fields. diff --git a/docs/berrywiki/Backends.md b/docs/berrywiki/Backends.md deleted file mode 100644 index ad90156..0000000 --- a/docs/berrywiki/Backends.md +++ /dev/null @@ -1,18 +0,0 @@ - - -# Backends - -Backend/provider registration and selection. - -Axiom keeps the mathematical API and proof-oriented contracts while delegating supported tensor primitives through the shared accelerator ABI. - -See [[Home]] for the project boundary and the repository machine-readable state for exact fields. diff --git a/docs/berrywiki/Evidence.adoc b/docs/berrywiki/Evidence.adoc new file mode 100644 index 0000000..c301502 --- /dev/null +++ b/docs/berrywiki/Evidence.adoc @@ -0,0 +1,10 @@ +== Evidence + +Capability and execution evidence requirements. + +Axiom keeps the mathematical API and proof-oriented contracts while +delegating supported tensor primitives through the shared accelerator +ABI. + +See [[Home]] for the project boundary and the repository +machine-readable state for exact fields. diff --git a/docs/berrywiki/Evidence.md b/docs/berrywiki/Evidence.md deleted file mode 100644 index 1174805..0000000 --- a/docs/berrywiki/Evidence.md +++ /dev/null @@ -1,18 +0,0 @@ - - -# Evidence - -Capability and execution evidence requirements. - -Axiom keeps the mathematical API and proof-oriented contracts while delegating supported tensor primitives through the shared accelerator ABI. - -See [[Home]] for the project boundary and the repository machine-readable state for exact fields. diff --git a/docs/berrywiki/Home.adoc b/docs/berrywiki/Home.adoc new file mode 100644 index 0000000..f5a0953 --- /dev/null +++ b/docs/berrywiki/Home.adoc @@ -0,0 +1,10 @@ +== Axiom.jl + +Julia proof-oriented tensor API with Zig FFI kernels. + +Axiom keeps the mathematical API and proof-oriented contracts while +delegating supported tensor primitives through the shared accelerator +ABI. + +This BerryWiki notebook is the human-facing index; the repository’s +machine-readable state file is authoritative for automation. diff --git a/docs/berrywiki/Home.md b/docs/berrywiki/Home.md deleted file mode 100644 index 3e1247a..0000000 --- a/docs/berrywiki/Home.md +++ /dev/null @@ -1,19 +0,0 @@ - - -# Axiom.jl - -Julia proof-oriented tensor API with Zig FFI kernels. - -Axiom keeps the mathematical API and proof-oriented contracts while delegating supported tensor primitives through the shared accelerator ABI. - -This BerryWiki notebook is the human-facing index; the repository's machine-readable state file is authoritative for automation. - diff --git a/docs/berrywiki/Kernels.adoc b/docs/berrywiki/Kernels.adoc new file mode 100644 index 0000000..4b781f0 --- /dev/null +++ b/docs/berrywiki/Kernels.adoc @@ -0,0 +1,10 @@ +== Kernels + +Kernel families, layouts, and numerical contracts. + +Axiom keeps the mathematical API and proof-oriented contracts while +delegating supported tensor primitives through the shared accelerator +ABI. + +See [[Home]] for the project boundary and the repository +machine-readable state for exact fields. diff --git a/docs/berrywiki/Kernels.md b/docs/berrywiki/Kernels.md deleted file mode 100644 index a99af25..0000000 --- a/docs/berrywiki/Kernels.md +++ /dev/null @@ -1,18 +0,0 @@ - - -# Kernels - -Kernel families, layouts, and numerical contracts. - -Axiom keeps the mathematical API and proof-oriented contracts while delegating supported tensor primitives through the shared accelerator ABI. - -See [[Home]] for the project boundary and the repository machine-readable state for exact fields. diff --git a/docs/berrywiki/Machine-Index.adoc b/docs/berrywiki/Machine-Index.adoc new file mode 100644 index 0000000..c3934c7 --- /dev/null +++ b/docs/berrywiki/Machine-Index.adoc @@ -0,0 +1,10 @@ +== Machine-Index + +Machine-readable inventory and automation entry point. + +Axiom keeps the mathematical API and proof-oriented contracts while +delegating supported tensor primitives through the shared accelerator +ABI. + +See [[Home]] for the project boundary and the repository +machine-readable state for exact fields. diff --git a/docs/berrywiki/Machine-Index.md b/docs/berrywiki/Machine-Index.md deleted file mode 100644 index 052f526..0000000 --- a/docs/berrywiki/Machine-Index.md +++ /dev/null @@ -1,18 +0,0 @@ - - -# Machine-Index - -Machine-readable inventory and automation entry point. - -Axiom keeps the mathematical API and proof-oriented contracts while delegating supported tensor primitives through the shared accelerator ABI. - -See [[Home]] for the project boundary and the repository machine-readable state for exact fields. diff --git a/docs/berrywiki/Operations.adoc b/docs/berrywiki/Operations.adoc new file mode 100644 index 0000000..db7bcdb --- /dev/null +++ b/docs/berrywiki/Operations.adoc @@ -0,0 +1,10 @@ +== Operations + +Canonical operation names and request semantics. + +Axiom keeps the mathematical API and proof-oriented contracts while +delegating supported tensor primitives through the shared accelerator +ABI. + +See [[Home]] for the project boundary and the repository +machine-readable state for exact fields. diff --git a/docs/berrywiki/Operations.md b/docs/berrywiki/Operations.md deleted file mode 100644 index 46acb64..0000000 --- a/docs/berrywiki/Operations.md +++ /dev/null @@ -1,18 +0,0 @@ - - -# Operations - -Canonical operation names and request semantics. - -Axiom keeps the mathematical API and proof-oriented contracts while delegating supported tensor primitives through the shared accelerator ABI. - -See [[Home]] for the project boundary and the repository machine-readable state for exact fields. diff --git a/docs/berrywiki/Performance.adoc b/docs/berrywiki/Performance.adoc new file mode 100644 index 0000000..adc7f04 --- /dev/null +++ b/docs/berrywiki/Performance.adoc @@ -0,0 +1,10 @@ +== Performance + +Benchmarking, determinism, and tuning guidance. + +Axiom keeps the mathematical API and proof-oriented contracts while +delegating supported tensor primitives through the shared accelerator +ABI. + +See [[Home]] for the project boundary and the repository +machine-readable state for exact fields. diff --git a/docs/berrywiki/Performance.md b/docs/berrywiki/Performance.md deleted file mode 100644 index 8d5d193..0000000 --- a/docs/berrywiki/Performance.md +++ /dev/null @@ -1,18 +0,0 @@ - - -# Performance - -Benchmarking, determinism, and tuning guidance. - -Axiom keeps the mathematical API and proof-oriented contracts while delegating supported tensor primitives through the shared accelerator ABI. - -See [[Home]] for the project boundary and the repository machine-readable state for exact fields. diff --git a/docs/berrywiki/Roadmap.adoc b/docs/berrywiki/Roadmap.adoc new file mode 100644 index 0000000..7e6fe3c --- /dev/null +++ b/docs/berrywiki/Roadmap.adoc @@ -0,0 +1,10 @@ +== Roadmap + +Near-term implementation and admission milestones. + +Axiom keeps the mathematical API and proof-oriented contracts while +delegating supported tensor primitives through the shared accelerator +ABI. + +See [[Home]] for the project boundary and the repository +machine-readable state for exact fields. diff --git a/docs/berrywiki/Roadmap.md b/docs/berrywiki/Roadmap.md deleted file mode 100644 index 495c399..0000000 --- a/docs/berrywiki/Roadmap.md +++ /dev/null @@ -1,18 +0,0 @@ - - -# Roadmap - -Near-term implementation and admission milestones. - -Axiom keeps the mathematical API and proof-oriented contracts while delegating supported tensor primitives through the shared accelerator ABI. - -See [[Home]] for the project boundary and the repository machine-readable state for exact fields. diff --git a/docs/berrywiki/Runtime.adoc b/docs/berrywiki/Runtime.adoc new file mode 100644 index 0000000..09147cb --- /dev/null +++ b/docs/berrywiki/Runtime.adoc @@ -0,0 +1,10 @@ +== Runtime + +Lifecycle, loading, and failure terminality. + +Axiom keeps the mathematical API and proof-oriented contracts while +delegating supported tensor primitives through the shared accelerator +ABI. + +See [[Home]] for the project boundary and the repository +machine-readable state for exact fields. diff --git a/docs/berrywiki/Runtime.md b/docs/berrywiki/Runtime.md deleted file mode 100644 index 2cd5b1a..0000000 --- a/docs/berrywiki/Runtime.md +++ /dev/null @@ -1,18 +0,0 @@ - - -# Runtime - -Lifecycle, loading, and failure terminality. - -Axiom keeps the mathematical API and proof-oriented contracts while delegating supported tensor primitives through the shared accelerator ABI. - -See [[Home]] for the project boundary and the repository machine-readable state for exact fields. diff --git a/docs/berrywiki/Security.adoc b/docs/berrywiki/Security.adoc new file mode 100644 index 0000000..0151fab --- /dev/null +++ b/docs/berrywiki/Security.adoc @@ -0,0 +1,10 @@ +== Security + +Trust boundaries, validation, and unsafe inputs. + +Axiom keeps the mathematical API and proof-oriented contracts while +delegating supported tensor primitives through the shared accelerator +ABI. + +See [[Home]] for the project boundary and the repository +machine-readable state for exact fields. diff --git a/docs/berrywiki/Security.md b/docs/berrywiki/Security.md deleted file mode 100644 index 2deada8..0000000 --- a/docs/berrywiki/Security.md +++ /dev/null @@ -1,18 +0,0 @@ - - -# Security - -Trust boundaries, validation, and unsafe inputs. - -Axiom keeps the mathematical API and proof-oriented contracts while delegating supported tensor primitives through the shared accelerator ABI. - -See [[Home]] for the project boundary and the repository machine-readable state for exact fields. diff --git a/docs/berrywiki/Simulation.adoc b/docs/berrywiki/Simulation.adoc new file mode 100644 index 0000000..9adb1bd --- /dev/null +++ b/docs/berrywiki/Simulation.adoc @@ -0,0 +1,10 @@ +== Simulation + +Rules for simulation, refusal, and conformance claims. + +Axiom keeps the mathematical API and proof-oriented contracts while +delegating supported tensor primitives through the shared accelerator +ABI. + +See [[Home]] for the project boundary and the repository +machine-readable state for exact fields. diff --git a/docs/berrywiki/Simulation.md b/docs/berrywiki/Simulation.md deleted file mode 100644 index 1c0f14b..0000000 --- a/docs/berrywiki/Simulation.md +++ /dev/null @@ -1,18 +0,0 @@ - - -# Simulation - -Rules for simulation, refusal, and conformance claims. - -Axiom keeps the mathematical API and proof-oriented contracts while delegating supported tensor primitives through the shared accelerator ABI. - -See [[Home]] for the project boundary and the repository machine-readable state for exact fields. diff --git a/docs/berrywiki/Testing.adoc b/docs/berrywiki/Testing.adoc new file mode 100644 index 0000000..0ab5484 --- /dev/null +++ b/docs/berrywiki/Testing.adoc @@ -0,0 +1,10 @@ +== Testing + +Local tests, integration tests, and acceptance gates. + +Axiom keeps the mathematical API and proof-oriented contracts while +delegating supported tensor primitives through the shared accelerator +ABI. + +See [[Home]] for the project boundary and the repository +machine-readable state for exact fields. diff --git a/docs/berrywiki/Testing.md b/docs/berrywiki/Testing.md deleted file mode 100644 index 82f00fe..0000000 --- a/docs/berrywiki/Testing.md +++ /dev/null @@ -1,18 +0,0 @@ - - -# Testing - -Local tests, integration tests, and acceptance gates. - -Axiom keeps the mathematical API and proof-oriented contracts while delegating supported tensor primitives through the shared accelerator ABI. - -See [[Home]] for the project boundary and the repository machine-readable state for exact fields. diff --git a/docs/berrywiki/UMS-Integration.adoc b/docs/berrywiki/UMS-Integration.adoc new file mode 100644 index 0000000..8ac756c --- /dev/null +++ b/docs/berrywiki/UMS-Integration.adoc @@ -0,0 +1,10 @@ +== UMS-Integration + +How the universal model space contract is consumed. + +Axiom keeps the mathematical API and proof-oriented contracts while +delegating supported tensor primitives through the shared accelerator +ABI. + +See [[Home]] for the project boundary and the repository +machine-readable state for exact fields. diff --git a/docs/berrywiki/UMS-Integration.md b/docs/berrywiki/UMS-Integration.md deleted file mode 100644 index eb3a234..0000000 --- a/docs/berrywiki/UMS-Integration.md +++ /dev/null @@ -1,18 +0,0 @@ - - -# UMS-Integration - -How the universal model space contract is consumed. - -Axiom keeps the mathematical API and proof-oriented contracts while delegating supported tensor primitives through the shared accelerator ABI. - -See [[Home]] for the project boundary and the repository machine-readable state for exact fields. diff --git a/docs/berrywiki/_Sidebar.adoc b/docs/berrywiki/_Sidebar.adoc new file mode 100644 index 0000000..3ae2c87 --- /dev/null +++ b/docs/berrywiki/_Sidebar.adoc @@ -0,0 +1,18 @@ +== Notebook + +* link:Home[Axiom.jl] +* Architecture +* Operations +* Backends +* Kernels +* Evidence +* ABI +* UMS-Integration +* Simulation +* Axiom-Kernels +* Runtime +* Testing +* Security +* Performance +* Roadmap +* Machine-Index diff --git a/docs/berrywiki/_Sidebar.md b/docs/berrywiki/_Sidebar.md deleted file mode 100644 index f79b327..0000000 --- a/docs/berrywiki/_Sidebar.md +++ /dev/null @@ -1,18 +0,0 @@ -# Notebook - -- [Axiom.jl](Home) -- [Architecture](Architecture) -- [Operations](Operations) -- [Backends](Backends) -- [Kernels](Kernels) -- [Evidence](Evidence) -- [ABI](ABI) -- [UMS-Integration](UMS-Integration) -- [Simulation](Simulation) -- [Axiom-Kernels](Axiom-Kernels) -- [Runtime](Runtime) -- [Testing](Testing) -- [Security](Security) -- [Performance](Performance) -- [Roadmap](Roadmap) -- [Machine-Index](Machine-Index) diff --git a/docs/design-diary/ULTRAPLAN.adoc b/docs/design-diary/ULTRAPLAN.adoc index cded6a7..72c8856 100644 --- a/docs/design-diary/ULTRAPLAN.adoc +++ b/docs/design-diary/ULTRAPLAN.adoc @@ -98,7 +98,7 @@ See `GAP-REGISTER.md` for the machine-readable form. Severity ∈ . *[high/system]* No RegistryCI/AutoMerge/TagBot/CompatHelper; only test is Idris2 string-match (asserts a nonexistent README.adoc) → add RegistryCI. . *[high/compliance]* `NOTICE` falsely claims PMPL-1.0 → **FLAG-ONLY to owner** (no auto-edit). . *[medium/adaptive]* No semver/AutoMerge guideline; compat lower-bounds only → write policy + enforce. -. *[medium/perfective]* Doc-map drift (claims README.adoc/deno.json/flake.nix; STATE 0% vs shipped v1.0.0) → reconcile. +. *[medium/perfective]* Doc-map drift (claims README.adoc/deno.json/flake.guix; STATE 0% vs shipped v1.0.0) → reconcile. . *[medium/perfective]* No julianiser↔registry integration docs → document the pipeline. . *[low/corrective]* stapeln/guix copy-paste; copilot `npx` (self-banned); duplicate `secrets:inherit`; malformed curl → fix/exempt. . *[low/perfective]* GOVERNANCE references `docs/decisions/` that doesn't exist → create ADR dir. diff --git a/docs/src/api-core.md b/docs/src/api-core.adoc similarity index 68% rename from docs/src/api-core.md rename to docs/src/api-core.adoc index 8dd61a9..6439bae 100644 --- a/docs/src/api-core.md +++ b/docs/src/api-core.adoc @@ -1,13 +1,9 @@ - - -# Tensors & Layers +== Tensors & Layers Core tensor types, shapes, and neural network layers. -```@autodocs +[source,@autodocs] +---- Modules = [Axiom] Public = true Private = false @@ -23,4 +19,4 @@ Pages = [ "layers/pooling.jl", "layers/invertible.jl", ] -``` +---- diff --git a/docs/src/api-serving.md b/docs/src/api-serving.adoc similarity index 70% rename from docs/src/api-serving.md rename to docs/src/api-serving.adoc index 9447497..1328254 100644 --- a/docs/src/api-serving.md +++ b/docs/src/api-serving.adoc @@ -1,14 +1,10 @@ - - -# Backends, Serving & Interop +== Backends, Serving & Interop Accelerator backend abstraction (CPU/Zig/GPU/coprocessor), model serving (REST/GraphQL/gRPC), PyTorch/ONNX interop, and model metadata/packaging. -```@autodocs +[source,@autodocs] +---- Modules = [Axiom] Public = true Private = false @@ -22,4 +18,4 @@ Pages = [ "model_metadata.jl", "model_packaging.jl", ] -``` +---- diff --git a/docs/src/api-training.md b/docs/src/api-training.adoc similarity index 54% rename from docs/src/api-training.md rename to docs/src/api-training.adoc index a6f880f..2a857d5 100644 --- a/docs/src/api-training.md +++ b/docs/src/api-training.adoc @@ -1,14 +1,11 @@ - +== Training & Automatic Differentiation -# Training & Automatic Differentiation +Optimizers, loss functions, the training loop, automatic +differentiation, and the `+@axiom+` / `+@ensure+` / `+@prove+` +declarative DSL. -Optimizers, loss functions, the training loop, automatic differentiation, -and the `@axiom` / `@ensure` / `@prove` declarative DSL. - -```@autodocs +[source,@autodocs] +---- Modules = [Axiom] Public = true Private = false @@ -26,4 +23,4 @@ Pages = [ "utils/data.jl", "utils/initialization.jl", ] -``` +---- diff --git a/docs/src/api-verification.md b/docs/src/api-verification.adoc similarity index 66% rename from docs/src/api-verification.md rename to docs/src/api-verification.adoc index 78e3cdc..4a16981 100644 --- a/docs/src/api-verification.md +++ b/docs/src/api-verification.adoc @@ -1,15 +1,11 @@ - - -# Verification & Certification +== Verification & Certification Formal property specification, checking, certificate generation and -serialization, hybrid Ed448+Dilithium5 signing, and proof-assistant export -(Lean/Coq/Isabelle). +serialization, hybrid Ed448+Dilithium5 signing, and proof-assistant +export (Lean/Coq/Isabelle). -```@autodocs +[source,@autodocs] +---- Modules = [Axiom] Public = true Private = false @@ -22,4 +18,4 @@ Pages = [ "verification/verification.jl", "proof_export.jl", ] -``` +---- diff --git a/docs/src/index.adoc b/docs/src/index.adoc new file mode 100644 index 0000000..0397e6d --- /dev/null +++ b/docs/src/index.adoc @@ -0,0 +1,29 @@ +== Axiom.jl + +Axiom.jl: Toward Provably Correct Machine Learning (proofs in progress). + +This site is generated by +https://github.com/JuliaDocs/Documenter.jl[Documenter.jl] from the +docstrings in `+src/+`. See `+README.md+` for a narrative introduction, +usage examples, and the honest prior-art comparison, and +`+REGISTRY-READINESS.md+` for the current state of the quality gates. + +The API reference is split across a few pages (grouped by source-file +area rather than crammed onto one page) because a single-page +`+@autodocs+` dump of Axiom’s full public surface exceeds Documenter’s +HTML `+size_threshold+` sanity check: + +* link:@ref[Tensors & Layers] – core types, layer constructors, +activations +* link:@ref[Training & Automatic Differentiation] – optimizers, losses, +autograd, the `+@axiom+`/`+@ensure+`/`+@prove+` DSL +* link:@ref[Verification & Certification] – properties, certificates, +proof export, hybrid signing +* link:@ref[Backends, Serving & Interop] – accelerator backends, +model serving APIs, PyTorch/ONNX interop, packaging + +=== Full API index + +[source,@index] +---- +---- diff --git a/docs/src/index.md b/docs/src/index.md deleted file mode 100644 index 73a6d6f..0000000 --- a/docs/src/index.md +++ /dev/null @@ -1,28 +0,0 @@ - - -# Axiom.jl - -Axiom.jl: Toward Provably Correct Machine Learning (proofs in progress). - -This site is generated by [Documenter.jl](https://github.com/JuliaDocs/Documenter.jl) -from the docstrings in `src/`. See `README.md` for a narrative introduction, -usage examples, and the honest prior-art comparison, and -`REGISTRY-READINESS.md` for the current state of the quality gates. - -The API reference is split across a few pages (grouped by source-file area -rather than crammed onto one page) because a single-page `@autodocs` dump -of Axiom's full public surface exceeds Documenter's HTML -`size_threshold` sanity check: - -- [Tensors & Layers](@ref) -- core types, layer constructors, activations -- [Training & Automatic Differentiation](@ref) -- optimizers, losses, autograd, the `@axiom`/`@ensure`/`@prove` DSL -- [Verification & Certification](@ref) -- properties, certificates, proof export, hybrid signing -- [Backends, Serving & Interop](@ref) -- accelerator backends, model serving APIs, PyTorch/ONNX interop, packaging - -## Full API index - -```@index -``` diff --git a/llm-warmup-dev.adoc b/llm-warmup-dev.adoc new file mode 100644 index 0000000..3d9f9c2 --- /dev/null +++ b/llm-warmup-dev.adoc @@ -0,0 +1,19 @@ +== LLM Warmup — Axiom.jl (Developer) + +=== What is Axiom.jl? + +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 39bc2f0..0000000 --- a/llm-warmup-dev.md +++ /dev/null @@ -1,16 +0,0 @@ -# LLM Warmup — Axiom.jl (Developer) - -## What is Axiom.jl? -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..ffab2e3 --- /dev/null +++ b/llm-warmup-user.adoc @@ -0,0 +1,19 @@ +== LLM Warmup — Axiom.jl (User) + +=== What is Axiom.jl? + +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 f646b25..0000000 --- a/llm-warmup-user.md +++ /dev/null @@ -1,16 +0,0 @@ -# LLM Warmup — Axiom.jl (User) - -## What is Axiom.jl? -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/packages/SMTLib.jl/README.md b/packages/SMTLib.jl/README.adoc similarity index 59% rename from packages/SMTLib.jl/README.md rename to packages/SMTLib.jl/README.adoc index 6a4e7d8..ea1768f 100644 --- a/packages/SMTLib.jl/README.md +++ b/packages/SMTLib.jl/README.adoc @@ -1,24 +1,29 @@ -# SMTLib.jl +== SMTLib.jl A lightweight Julia interface to SMT solvers via SMT-LIB2 format. -> **Standalone Package**: This package is designed to be published independently. -> Currently bundled with [Axiom.jl](https://github.com/hyperpolymath/axiom.jl) at `packages/SMTLib.jl`. -> To publish separately, copy this directory to a new repository. +____ +*Standalone Package*: This package is designed to be published +independently. Currently bundled with +https://github.com/hyperpolymath/axiom.jl[Axiom.jl] at +`+packages/SMTLib.jl+`. To publish separately, copy this directory to a +new repository. +____ -## Features +=== Features -- **Auto-detection** of installed SMT solvers (Z3, CVC5, Yices, MathSAT) -- **Julia expression to SMT-LIB2** conversion -- **Multiple logics**: QF_LIA, QF_LRA, QF_NRA, QF_BV, arrays, and more -- **Model parsing** and counterexample extraction -- **Timeout support** -- **Incremental solving** with push/pop semantics -- **Zero dependencies** - pure Julia +* *Auto-detection* of installed SMT solvers (Z3, CVC5, Yices, MathSAT) +* *Julia expression to SMT-LIB2* conversion +* *Multiple logics*: QF_LIA, QF_LRA, QF_NRA, QF_BV, arrays, and more +* *Model parsing* and counterexample extraction +* *Timeout support* +* *Incremental solving* with push/pop semantics +* *Zero dependencies* - pure Julia -## Installation +=== Installation -```julia +[source,julia] +---- using Pkg # From Axiom.jl monorepo @@ -26,13 +31,14 @@ Pkg.develop(path="packages/SMTLib.jl") # Or from standalone repo (when published) # Pkg.add(url="https://github.com/hyperpolymath/SMTLib.jl") -``` +---- -### Prerequisites +==== Prerequisites Install at least one SMT solver: -```bash +[source,bash] +---- # Z3 (recommended) brew install z3 # macOS apt install z3 # Ubuntu/Debian @@ -41,11 +47,12 @@ pacman -S z3 # Arch # CVC5 brew install cvc5 apt install cvc5 -``` +---- -## Quick Start +=== Quick Start -```julia +[source,julia] +---- using SMTLib # Simple satisfiability check @@ -64,11 +71,12 @@ if result.status == :sat println("x = ", result.model[:x]) println("y = ", result.model[:y]) end -``` +---- -### Using the @smt Macro +==== Using the @smt Macro -```julia +[source,julia] +---- result = @smt logic=:QF_LIA begin x::Int y::Int @@ -79,57 +87,71 @@ end println(result.status) # :sat println(result.model) # Dict(:x => 5, :y => 5) -``` +---- -### Proving Properties +==== Proving Properties -```julia +[source,julia] +---- # Prove that x^2 >= 0 for all real x # (Returns true if proven) proven = prove(:(x * x >= 0), logic=:QF_NRA) -``` +---- -## Supported Logics +=== Supported Logics -| Logic | Description | -|-------|-------------| -| `QF_LIA` | Quantifier-free linear integer arithmetic | -| `QF_LRA` | Quantifier-free linear real arithmetic | -| `QF_NIA` | Quantifier-free nonlinear integer arithmetic | -| `QF_NRA` | Quantifier-free nonlinear real arithmetic | -| `QF_BV` | Quantifier-free bitvectors | -| `QF_AUFLIA` | Arrays, uninterpreted functions, linear integer arithmetic | -| `ALL` | All supported theories | +[width="100%",cols="35%,65%",options="header",] +|=== +|Logic |Description +|`+QF_LIA+` |Quantifier-free linear integer arithmetic -## API Reference +|`+QF_LRA+` |Quantifier-free linear real arithmetic -### Solver Discovery +|`+QF_NIA+` |Quantifier-free nonlinear integer arithmetic -```julia +|`+QF_NRA+` |Quantifier-free nonlinear real arithmetic + +|`+QF_BV+` |Quantifier-free bitvectors + +|`+QF_AUFLIA+` |Arrays, uninterpreted functions, linear integer +arithmetic + +|`+ALL+` |All supported theories +|=== + +=== API Reference + +==== Solver Discovery + +[source,julia] +---- available_solvers() # List all detected solvers find_solver() # Get first available solver find_solver(:z3) # Get specific solver -``` +---- -### Context Management +==== Context Management -```julia +[source,julia] +---- ctx = SMTContext(logic=:QF_LIA, timeout_ms=30000) declare(ctx, :x, Int) # Declare variable assert!(ctx, expr) # Add assertion check_sat(ctx) # Check satisfiability reset!(ctx) # Clear context -``` +---- -### SMT-LIB Conversion +==== SMT-LIB Conversion -```julia +[source,julia] +---- to_smtlib(:(x + y == 10)) # "(= (+ x y) 10)" -``` +---- -### Types +==== Types -```julia +[source,julia] +---- # Built-in types Int, Float64, Bool @@ -138,13 +160,14 @@ BitVec{32} # 32-bit bitvector # Arrays SMTArray{Int, Int} # Array from Int to Int -``` +---- -## Examples +=== Examples -### Sudoku Solver +==== Sudoku Solver -```julia +[source,julia] +---- function solve_sudoku(grid) ctx = SMTContext(logic=:QF_LIA) @@ -160,11 +183,12 @@ function solve_sudoku(grid) result = check_sat(ctx) # Extract solution from result.model end -``` +---- -### Verification +==== Verification -```julia +[source,julia] +---- # Verify array bounds check is sufficient ctx = SMTContext(logic=:QF_LIA) @@ -182,12 +206,13 @@ assert!(ctx, :(i < 0 || i >= n)) result = check_sat(ctx) @assert result.status == :unsat # Proven safe! -``` +---- -## License +=== License MIT License - see LICENSE file. -## Acknowledgments +=== Acknowledgments -Extracted from [Axiom.jl](https://github.com/hyperpolymath/axiom.jl), a provably correct ML framework. +Extracted from https://github.com/hyperpolymath/axiom.jl[Axiom.jl], a +provably correct ML framework. diff --git a/templates/README.adoc b/templates/README.adoc new file mode 100644 index 0000000..ae0f4ff --- /dev/null +++ b/templates/README.adoc @@ -0,0 +1,211 @@ +== Axiom.jl Model Zoo Templates + +Verification-ready model templates with formal properties and metadata. + +=== Quick Start + +==== Computer Vision + +[source,julia] +---- +using Axiom + +# ResNet50 for image classification +model, metadata = resnet50_verified(pretrained=true) + +# Verify properties +@prove ∀x ∈ ImageNet. is_finite(model(x)) + +# Inference +predictions = model(load_image("cat.jpg")) +---- + +==== Natural Language Processing + +[source,julia] +---- +using Axiom + +# Transformer encoder +model, metadata = transformer_encoder_verified( + vocab_size=50000, + d_model=768, + n_heads=12 +) + +# Verify attention properties +@prove ∀x. sum(attention_weights(model, x), dims=2) ≈ 1.0 + +# Inference +embeddings = model(tokenize("Hello world")) +---- + +=== Available Templates + +==== Computer Vision + +[width="100%",cols="16%,13%,26%,45%",options="header",] +|=== +|Model |Task |Parameters |Verification Claims +|ResNet50 |Image Classification |25.6M |Lipschitz, finite outputs, +probability bounds + +|MobileNetV2 |Mobile CV |3.5M |Efficient inference, quantization-ready + +|EfficientNet-B0 |Compound Scaling |5.3M |Accuracy-efficiency tradeoffs + +|Vision Transformer (ViT) |Image Classification |86M |Attention +normalization, patch embedding +|=== + +==== Natural Language Processing + +[width="100%",cols="16%,13%,26%,45%",options="header",] +|=== +|Model |Task |Parameters |Verification Claims +|Transformer Encoder |Sequence Modeling |Custom |Attention normalized, +stable embeddings + +|BERT-Base |Masked LM |110M |Token prediction bounds, attention sparsity + +|GPT-2 Small |Autoregressive LM |117M |Causality preserved, generation +stability + +|T5-Small |Seq2Seq |60M |Encoder-decoder alignment +|=== + +=== Model Structure + +Each template provides: + +[arabic] +. *Verified Architecture* - Built with `+@axiom+` macro for shape +checking +. *Metadata* - Complete `+ModelMetadata+` with provenance +. *Verification Claims* - Formal properties verified with `+@prove+` +. *Pretrained Weights* - Optional pretrained checkpoints +. *Documentation* - Usage examples and property specifications + +=== Creating Custom Templates + +==== Basic Template Structure + +[source,julia] +---- +function my_model_verified(; pretrained=false, num_classes=10) + # Define architecture + model = @axiom begin + # ... layers ... + end + + # Load weights if pretrained + if pretrained + load_weights!(model, "path/to/weights.jld2") + end + + # Create metadata + metadata = create_metadata( + model, + name="MyModel", + architecture="Custom", + task="classification", + # ... other fields ... + ) + + # Add verification claims + verify_and_claim!( + metadata, + "Property name", + "Formal specification" + ) + + # Save metadata + save_metadata(metadata, "my_model_metadata.json") + + return model, metadata +end +---- + +==== Verification Best Practices + +[arabic] +. *Start with basic properties*: +* No NaN/Inf propagation +* Output bounds (for probabilities, etc.) +* Input-output relationship preservation +. *Add domain-specific properties*: +* CV: Lipschitz continuity, spatial invariance +* NLP: Attention normalization, causality +. *Test verification overhead*: +* Profile verification time +* Consider caching verified properties +* Use sampling for large input spaces +. *Document limitations*: +* Approximations made +* Assumptions about input distribution +* Verification scope (training vs inference) + +=== Extending Templates + +==== Adding New Architecture + +[arabic] +. Create file in `+templates/{cv,nlp}/my_architecture.jl+` +. Implement `+my_architecture_verified()+` function +. Add verification claims appropriate to architecture +. Create metadata with complete provenance +. Add tests in `+test/templates/+` +. Document in this README + +==== Adding Pretrained Weights + +Weights should be: - Stored in standard format (JLD2, BSON, or +HuggingFace compatible) - Include checksum (SHA256) - Provide download +script or registry link - Include training configuration and metrics + +==== Verification Properties + +Common properties to verify: + +*Stability:* - No NaN/Inf propagation - Bounded gradients (Lipschitz) - +Numerical precision limits + +*Correctness:* - Output shape matches specification - Probability +distributions (sum to 1, non-negative) - Attention weights normalized + +*Robustness:* - Bounded perturbation resistance - Adversarial input +handling - Out-of-distribution detection + +*Performance:* - Inference time bounds - Memory usage limits - Batch +processing guarantees + +=== Integration with HuggingFace + +Import pretrained models from HuggingFace Hub: + +[source,julia] +---- +using Axiom + +# Import with automatic verification +model, metadata = from_pretrained( + "bert-base-uncased", + verify=true, # Verify after import + architecture="transformer" +) + +# Verification results in metadata +for claim in metadata.verification_claims + println("$(claim.property): $(claim.verified ? "✓" : "✗")") +end +---- + +=== See Also + +* link:../src/model_metadata.jl[Model Metadata Schema] +* link:../src/integrations/huggingface.jl[HuggingFace Integration] +* link:../docs/wiki/Verification.md[Verification Guide] +* https://github.com/hyperpolymath/Axiom.jl/issues/15[Issue #15 - +Verified Model Zoo] +* https://github.com/hyperpolymath/Axiom.jl/issues/16[Issue #16 - Model +Metadata] diff --git a/templates/README.md b/templates/README.md deleted file mode 100644 index 8cb9e03..0000000 --- a/templates/README.md +++ /dev/null @@ -1,200 +0,0 @@ -# Axiom.jl Model Zoo Templates - -Verification-ready model templates with formal properties and metadata. - -## Quick Start - -### Computer Vision - -```julia -using Axiom - -# ResNet50 for image classification -model, metadata = resnet50_verified(pretrained=true) - -# Verify properties -@prove ∀x ∈ ImageNet. is_finite(model(x)) - -# Inference -predictions = model(load_image("cat.jpg")) -``` - -### Natural Language Processing - -```julia -using Axiom - -# Transformer encoder -model, metadata = transformer_encoder_verified( - vocab_size=50000, - d_model=768, - n_heads=12 -) - -# Verify attention properties -@prove ∀x. sum(attention_weights(model, x), dims=2) ≈ 1.0 - -# Inference -embeddings = model(tokenize("Hello world")) -``` - -## Available Templates - -### Computer Vision - -| Model | Task | Parameters | Verification Claims | -|-------|------|------------|---------------------| -| ResNet50 | Image Classification | 25.6M | Lipschitz, finite outputs, probability bounds | -| MobileNetV2 | Mobile CV | 3.5M | Efficient inference, quantization-ready | -| EfficientNet-B0 | Compound Scaling | 5.3M | Accuracy-efficiency tradeoffs | -| Vision Transformer (ViT) | Image Classification | 86M | Attention normalization, patch embedding | - -### Natural Language Processing - -| Model | Task | Parameters | Verification Claims | -|-------|------|------------|---------------------| -| Transformer Encoder | Sequence Modeling | Custom | Attention normalized, stable embeddings | -| BERT-Base | Masked LM | 110M | Token prediction bounds, attention sparsity | -| GPT-2 Small | Autoregressive LM | 117M | Causality preserved, generation stability | -| T5-Small | Seq2Seq | 60M | Encoder-decoder alignment | - -## Model Structure - -Each template provides: - -1. **Verified Architecture** - Built with `@axiom` macro for shape checking -2. **Metadata** - Complete `ModelMetadata` with provenance -3. **Verification Claims** - Formal properties verified with `@prove` -4. **Pretrained Weights** - Optional pretrained checkpoints -5. **Documentation** - Usage examples and property specifications - -## Creating Custom Templates - -### Basic Template Structure - -```julia -function my_model_verified(; pretrained=false, num_classes=10) - # Define architecture - model = @axiom begin - # ... layers ... - end - - # Load weights if pretrained - if pretrained - load_weights!(model, "path/to/weights.jld2") - end - - # Create metadata - metadata = create_metadata( - model, - name="MyModel", - architecture="Custom", - task="classification", - # ... other fields ... - ) - - # Add verification claims - verify_and_claim!( - metadata, - "Property name", - "Formal specification" - ) - - # Save metadata - save_metadata(metadata, "my_model_metadata.json") - - return model, metadata -end -``` - -### Verification Best Practices - -1. **Start with basic properties**: - - No NaN/Inf propagation - - Output bounds (for probabilities, etc.) - - Input-output relationship preservation - -2. **Add domain-specific properties**: - - CV: Lipschitz continuity, spatial invariance - - NLP: Attention normalization, causality - -3. **Test verification overhead**: - - Profile verification time - - Consider caching verified properties - - Use sampling for large input spaces - -4. **Document limitations**: - - Approximations made - - Assumptions about input distribution - - Verification scope (training vs inference) - -## Extending Templates - -### Adding New Architecture - -1. Create file in `templates/{cv,nlp}/my_architecture.jl` -2. Implement `my_architecture_verified()` function -3. Add verification claims appropriate to architecture -4. Create metadata with complete provenance -5. Add tests in `test/templates/` -6. Document in this README - -### Adding Pretrained Weights - -Weights should be: -- Stored in standard format (JLD2, BSON, or HuggingFace compatible) -- Include checksum (SHA256) -- Provide download script or registry link -- Include training configuration and metrics - -### Verification Properties - -Common properties to verify: - -**Stability:** -- No NaN/Inf propagation -- Bounded gradients (Lipschitz) -- Numerical precision limits - -**Correctness:** -- Output shape matches specification -- Probability distributions (sum to 1, non-negative) -- Attention weights normalized - -**Robustness:** -- Bounded perturbation resistance -- Adversarial input handling -- Out-of-distribution detection - -**Performance:** -- Inference time bounds -- Memory usage limits -- Batch processing guarantees - -## Integration with HuggingFace - -Import pretrained models from HuggingFace Hub: - -```julia -using Axiom - -# Import with automatic verification -model, metadata = from_pretrained( - "bert-base-uncased", - verify=true, # Verify after import - architecture="transformer" -) - -# Verification results in metadata -for claim in metadata.verification_claims - println("$(claim.property): $(claim.verified ? "✓" : "✗")") -end -``` - -## See Also - -- [Model Metadata Schema](../src/model_metadata.jl) -- [HuggingFace Integration](../src/integrations/huggingface.jl) -- [Verification Guide](../docs/wiki/Verification.md) -- [Issue #15 - Verified Model Zoo](https://github.com/hyperpolymath/Axiom.jl/issues/15) -- [Issue #16 - Model Metadata](https://github.com/hyperpolymath/Axiom.jl/issues/16)