From a2a810566321eca4ac223b4781b049003e85062a Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 1 Jul 2026 07:51:31 +0000 Subject: [PATCH] =?UTF-8?q?feat(flagship):=20estate=20tooling=20=E2=80=94?= =?UTF-8?q?=20Aqua/JET/Documenter/test-gate=20+=20k9/panic-attack/RSR=20(t?= =?UTF-8?q?ier-2)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Makes Axiom.jl demonstrably best-practice (tier-2; G07, G08, G13, G14, G15, G16). Quality/testing: - Aqua.test_all(Axiom): all 11 checks pass with ZERO overrides. Fixed a real unbound-type-param bug in LayerNorm/InstanceNorm/GroupNorm inner constructors; removed the stale JSON3 dep (its only consumer, dead huggingface.jl, is not included in the module). (G07) - JET.test_package(Axiom; target_modules=(Axiom,)): zero Axiom-rooted errors, no allowlist. (G07) - Full [compat] closure incl. all six weakdeps + stdlibs + extras; widened Zygote 0.6 -> 0.6,0.7 (resolves to 0.7.11; suite unchanged). (G08) - Documenter docs/make.jl builds with doctests (explicit GitHub remote for the proxy env; API split into 4 pages under Documenter's HTML size limit). (G13) - julia-test.yml CI gate builds the crypto cdylib BEFORE Pkg.test, so the hybrid-signing tests actually run in CI (they had been silently @test_skip'd); matrix 1.10 + 1 + nightly(continue-on-error); no on.*.paths. Compliance/gates: - k9iser.toml (safety-tier fv) over Project.toml / axiom-abi.ipkg / crypto. (G15) - static-analysis-gate.yml (panic-attack assail, fail-on-critical) + Justfile assail recipe fixed (panic-attacker -> panic-attack). First assail: 0 critical, 2 high (legit crypto/FFI unsafe boundary, tracked for P5 audit). (G14) - estate-rules.yml (correctly bans V-lang, NOT Zig) + RSR files: docs/legal/ EXHIBIT-A/B, docs/governance/*, .machine_readable/policies/*. (G16) Verified: Pkg.test 709/709 (697 + 11 Aqua + 1 JET); docs build clean; Pkg.resolve clean; no licence/key files touched; SPDX on all new files. Residual: dead huggingface.jl (stale dep removed; deletion is tier-3); assail residuals audited in P5. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01UPFC9YQ7g9gc3VnRox42Q1 --- .github/workflows/Documentation.yml | 43 ++++ .github/workflows/estate-rules.yml | 80 +++++++ .github/workflows/julia-test.yml | 106 +++++++++ .github/workflows/static-analysis-gate.yml | 223 ++++++++++++++++++ .../policies/MAINTENANCE-AXES.a2ml | 61 +++++ .../policies/MAINTENANCE-CHECKLIST.a2ml | 161 +++++++++++++ .../SOFTWARE-DEVELOPMENT-APPROACH.a2ml | 65 +++++ Justfile | 4 +- Project.toml | 26 +- REGISTRY-READINESS.md | 44 +++- docs/Project.toml | 8 + docs/governance/MAINTENANCE-CHECKLIST.adoc | 202 ++++++++++++++++ .../SOFTWARE-DEVELOPMENT-APPROACH.adoc | 86 +++++++ docs/legal/EXHIBIT-A-ETHICAL-USE.txt | 34 +++ docs/legal/EXHIBIT-B-QUANTUM-SAFE.txt | 163 +++++++++++++ docs/make.jl | 60 +++++ docs/src/api-core.md | 26 ++ docs/src/api-serving.md | 25 ++ docs/src/api-training.md | 29 +++ docs/src/api-verification.md | 25 ++ docs/src/index.md | 28 +++ k9iser.toml | 88 +++++++ src/layers/normalization.jl | 47 ++++ test/aqua.jl | 38 +++ test/jet.jl | 43 ++++ test/runtests.jl | 4 + 26 files changed, 1709 insertions(+), 10 deletions(-) create mode 100644 .github/workflows/Documentation.yml create mode 100644 .github/workflows/estate-rules.yml create mode 100644 .github/workflows/julia-test.yml create mode 100644 .github/workflows/static-analysis-gate.yml create mode 100644 .machine_readable/policies/MAINTENANCE-AXES.a2ml create mode 100644 .machine_readable/policies/MAINTENANCE-CHECKLIST.a2ml create mode 100644 .machine_readable/policies/SOFTWARE-DEVELOPMENT-APPROACH.a2ml create mode 100644 docs/Project.toml create mode 100644 docs/governance/MAINTENANCE-CHECKLIST.adoc create mode 100644 docs/governance/SOFTWARE-DEVELOPMENT-APPROACH.adoc create mode 100644 docs/legal/EXHIBIT-A-ETHICAL-USE.txt create mode 100644 docs/legal/EXHIBIT-B-QUANTUM-SAFE.txt create mode 100644 docs/make.jl create mode 100644 docs/src/api-core.md create mode 100644 docs/src/api-serving.md create mode 100644 docs/src/api-training.md create mode 100644 docs/src/api-verification.md create mode 100644 docs/src/index.md create mode 100644 k9iser.toml create mode 100644 test/aqua.jl create mode 100644 test/jet.jl diff --git a/.github/workflows/Documentation.yml b/.github/workflows/Documentation.yml new file mode 100644 index 0000000..2d9c09e --- /dev/null +++ b/.github/workflows/Documentation.yml @@ -0,0 +1,43 @@ +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell (hyperpolymath) + +# Documenter build + (main-branch only) GitHub Pages deploy (G13). +# +# Per the estate required-check rule: no `on.*.paths` filter -- this +# workflow always runs so it is never stuck "Expected" on unrelated PRs. + +name: Documentation + +permissions: + contents: read + pages: write + id-token: write + +on: + push: + branches: [main] + pull_request: + branches: [main] + +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true + +jobs: + build: + name: Build docs (Documenter, with doctests) + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4 + + - uses: julia-actions/setup-julia@4c0cb0fce8556fdb04a90347310e5db8b1f98fb9 # v2 + with: + version: '1.10' + + - uses: julia-actions/cache@e33b4bfa0ea7cd9caedd7cb82b0e36956ef40285 # v2 + + - name: Build documentation (doctest=true) + env: + GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} + DOCUMENTER_KEY: ${{ secrets.DOCUMENTER_KEY }} + run: julia --project=docs docs/make.jl diff --git a/.github/workflows/estate-rules.yml b/.github/workflows/estate-rules.yml new file mode 100644 index 0000000..17b10bd --- /dev/null +++ b/.github/workflows/estate-rules.yml @@ -0,0 +1,80 @@ +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Axiom.jl Contributors +# +# Estate Rules — enforces hyperpolymath estate-wide conventions relevant to a +# Julia numerics package: no-Python (banned estate-wide, replacement is +# Julia/Rust/AffineScript), AsciiDoc-by-default under docs/ (excluding the +# docs/wiki/ GitHub-wiki mirror, which is legitimately Markdown because +# GitHub's wiki renderer consumes .md, not .adoc), and no V-lang (vlang.io) +# references — NOT a ban on Zig. Zig is the current estate default for +# APIs/FFI/gateways (hyperpolymath/standards CLAUDE.md, "Estate default +# 2026-05-28"), and Axiom.jl legitimately ships a Zig compute layer +# (zig/, ffi/zig/); a same-named check adapted from an older template +# repo had inverted this (banning the string "zig" itself, seemingly from a +# botched V-lang-ban rename) — do not repeat that mistake here. +# +# Checks are inlined (no external scripts/ dependency) because this repo's +# .github/workflows/ ownership does not include a scripts/ directory of its +# own for these checks. +name: Estate Rules +on: + push: + branches: [main] + pull_request: +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true +permissions: + contents: read +jobs: + estate-rules: + runs-on: ubuntu-latest + timeout-minutes: 15 + steps: + - name: Checkout + uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + + - name: No Python anywhere (estate-banned; Julia/Rust/AffineScript only) + run: | + HITS=$(find . -type f \( -name '*.py' -o -name '*.pyi' \) \ + -not -path './crypto/target/*' \ + -not -path './.git/*' \ + 2>/dev/null || true) + if [ -n "$HITS" ]; then + echo "::error::Python files found — Python is fully banned estate-wide:" + echo "$HITS" + exit 1 + fi + echo "PASS: no Python files found" + + - name: AsciiDoc by default under docs/ (excluding docs/wiki/ GitHub-wiki mirror) + run: | + HITS=$(find docs -name '*.md' -type f -not -path 'docs/wiki/*' 2>/dev/null || true) + if [ -n "$HITS" ]; then + echo "::error::.md files found under docs/ outside the docs/wiki/ mirror (estate rule: AsciiDoc by default):" + echo "$HITS" + exit 1 + fi + echo "PASS: no disallowed .md files under docs/ (docs/wiki/ is the GitHub-wiki Markdown mirror, exempt by design)" + + - name: No V-lang references (Zig is the estate default — do not confuse the two) + run: | + # V-lang (vlang.io) was banned 2026-04-10, superseded by Zig. This + # check must NOT match "zig" — Zig is the estate default for + # APIs/FFI/gateways and Axiom.jl ships a legitimate Zig compute + # layer under zig/ and ffi/zig/. + PATTERNS='vlang|v-lang|V-lang|asdf-vlang' + HITS=$(grep -rniE "$PATTERNS" . \ + --exclude-dir=.git \ + --exclude-dir=node_modules \ + --exclude-dir=target \ + --include='*.jl' --include='*.rs' --include='*.toml' \ + --include='*.zig' --include='*.idr' --include='*.adoc' \ + --include='*.a2ml' --include='Justfile' \ + 2>/dev/null || true) + if [ -n "$HITS" ]; then + echo "::error::V-lang reference(s) found (estate rule: V-lang is banned, replaced by Zig):" + echo "$HITS" + exit 1 + fi + echo "PASS: no V-lang references found" diff --git a/.github/workflows/julia-test.yml b/.github/workflows/julia-test.yml new file mode 100644 index 0000000..1af4a54 --- /dev/null +++ b/.github/workflows/julia-test.yml @@ -0,0 +1,106 @@ +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell (hyperpolymath) + +# Julia test gate (required check). +# +# `ci.yml`'s `julia-compat` job runs `Pkg.test()` but never builds the +# hybrid Ed448+Dilithium5 crypto cdylib (crypto/), so +# `test/verification/hybrid_signing_tests.jl` always takes the +# `@test_skip` branch there and the real signing path is never exercised +# in CI. This workflow builds the crypto shim first so those tests +# actually run, and also runs the new Aqua/JET quality-gate testsets +# (test/aqua.jl, test/jet.jl). +# +# Per the estate required-check rule: no `on.*.paths` filter on a required +# gate -- a path-filtered required workflow that never triggers is +# reported as permanently "Expected" and blocks merges. This workflow +# always runs. + +name: Julia Test Gate + +permissions: + contents: read + +on: + push: + branches: [main, develop] + pull_request: + branches: [main] + schedule: + - cron: '0 0 * * 0' + +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true + +env: + JULIA_NUM_THREADS: 2 + +jobs: + test: + name: Julia ${{ matrix.julia-version }} (crypto-enabled) - ubuntu-latest + runs-on: ubuntu-latest + strategy: + fail-fast: false + matrix: + # 1.10 is the LTS floor declared in Project.toml's `[compat] julia`; + # '1' resolves to the current stable release. + julia-version: ['1.10', '1'] + + steps: + - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4 + + - name: Install Rust toolchain + uses: dtolnay/rust-toolchain@efa25f7f19611383d5b0ccf2d1c8914531636bf9 # stable + + - name: Cache Cargo (crypto shim) + uses: actions/cache@668228422ae6a00e4ad889ee87cd7109ec5666a7 # v5.0.4 + with: + path: | + ~/.cargo/registry + ~/.cargo/git + crypto/target + key: ${{ runner.os }}-cargo-crypto-${{ hashFiles('crypto/Cargo.lock') }} + + - name: Build hybrid-signing crypto cdylib + run: cd crypto && cargo build --release + + - uses: julia-actions/setup-julia@4c0cb0fce8556fdb04a90347310e5db8b1f98fb9 # v2 + with: + version: ${{ matrix.julia-version }} + + - uses: julia-actions/cache@e33b4bfa0ea7cd9caedd7cb82b0e36956ef40285 # v2 + + - name: Instantiate / Build / Precompile / Test + run: julia --project=. -e 'using Pkg; Pkg.instantiate(); Pkg.build(); Pkg.precompile(); Pkg.test()' + + test-nightly: + name: Julia nightly (crypto-enabled) - ubuntu-latest + runs-on: ubuntu-latest + continue-on-error: true + steps: + - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4 + + - name: Install Rust toolchain + uses: dtolnay/rust-toolchain@efa25f7f19611383d5b0ccf2d1c8914531636bf9 # stable + + - name: Cache Cargo (crypto shim) + uses: actions/cache@668228422ae6a00e4ad889ee87cd7109ec5666a7 # v5.0.4 + with: + path: | + ~/.cargo/registry + ~/.cargo/git + crypto/target + key: ${{ runner.os }}-cargo-crypto-${{ hashFiles('crypto/Cargo.lock') }} + + - name: Build hybrid-signing crypto cdylib + run: cd crypto && cargo build --release + + - uses: julia-actions/setup-julia@4c0cb0fce8556fdb04a90347310e5db8b1f98fb9 # v2 + with: + version: nightly + + - uses: julia-actions/cache@e33b4bfa0ea7cd9caedd7cb82b0e36956ef40285 # v2 + + - name: Instantiate / Build / Precompile / Test + run: julia --project=. -e 'using Pkg; Pkg.instantiate(); Pkg.build(); Pkg.precompile(); Pkg.test()' diff --git a/.github/workflows/static-analysis-gate.yml b/.github/workflows/static-analysis-gate.yml new file mode 100644 index 0000000..d77156a --- /dev/null +++ b/.github/workflows/static-analysis-gate.yml @@ -0,0 +1,223 @@ +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Axiom.jl Contributors +# +# Static Analysis Gate — panic-attack `assail` over the whole repo, blocking +# on Critical/High findings. This is a candidate REQUIRED status check, so it +# deliberately carries NO `on.*.paths` filter: a path-filtered required +# workflow that never triggers is reported by GitHub as permanently +# "Expected", which leaves unrelated PRs `mergeable_state: blocked` forever +# (see hyperpolymath/boj-server CLAUDE.md, "CI / Required Status Checks"). +# Instead, a lightweight always-run `changes` job gates the heavy job via +# `if:`, which still counts as a passing required check when skipped. +name: Static Analysis Gate +on: + push: + branches: [main, master] + pull_request: +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true +permissions: + contents: read +jobs: + # --------------------------------------------------------------------------- + # Job 0: changes — always runs, cheap. Decides whether the heavy scan is + # needed. Fail-safe default is run=true (never silently skips on an error). + # --------------------------------------------------------------------------- + changes: + name: Detect relevant changes + runs-on: ubuntu-latest + timeout-minutes: 5 + outputs: + run: ${{ steps.detect.outputs.run }} + steps: + - name: Checkout repository + uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + with: + fetch-depth: 0 + - name: Decide whether to run the gate + id: detect + run: | + # Fail safe: default to running the gate. + RUN="true" + if [ "${{ github.event_name }}" = "pull_request" ]; then + BASE="${{ github.event.pull_request.base.sha }}" + if [ -n "$BASE" ] && git diff --quiet "$BASE"...HEAD 2>/dev/null; then + RUN="false" + fi + fi + echo "run=$RUN" >> "$GITHUB_OUTPUT" + + # --------------------------------------------------------------------------- + # Job 1: panic-attack assail + # --------------------------------------------------------------------------- + panic-attack-assail: + name: panic-attack assail + needs: changes + if: needs.changes.outputs.run == 'true' + runs-on: ubuntu-latest + timeout-minutes: 15 + steps: + - name: Checkout repository + uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + with: + fetch-depth: 0 + - name: Install panic-attack (if available) + id: install + run: | + # Try to fetch the latest release binary from the org. Tool renamed + # 2026-02-08: panic-attacker -> panic-attack (binary + repo + subcommand). + PA_URL="https://github.com/hyperpolymath/panic-attack/releases/latest/download/panic-attack-linux-x86_64" + if curl -fsSL --head "$PA_URL" >/dev/null 2>&1; then + curl -fsSL -o /usr/local/bin/panic-attack "$PA_URL" + chmod +x /usr/local/bin/panic-attack + echo "installed=true" >> "$GITHUB_OUTPUT" + else + echo "::notice::panic-attack binary not available — skipping assail" + echo "installed=false" >> "$GITHUB_OUTPUT" + fi + - name: Run panic-attack assail + id: assail + if: steps.install.outputs.installed == 'true' + run: | + set +e + panic-attack assail . --output panic-attack-findings.json --output-format json --headless + PA_EXIT=$? + set -e + + if [ ! -s panic-attack-findings.json ] || ! jq empty panic-attack-findings.json 2>/dev/null; then + echo '{"weak_points":[]}' > panic-attack-findings.json + fi + + # Parse finding counts by severity (schema: {"weak_points":[{"severity":...}]}) + TOTAL=$(jq '.weak_points | length' panic-attack-findings.json 2>/dev/null || echo 0) + CRITICAL=$(jq '[.weak_points[] | select(.severity == "Critical")] | length' panic-attack-findings.json 2>/dev/null || echo 0) + HIGH=$(jq '[.weak_points[] | select(.severity == "High")] | length' panic-attack-findings.json 2>/dev/null || echo 0) + MEDIUM=$(jq '[.weak_points[] | select(.severity == "Medium")] | length' panic-attack-findings.json 2>/dev/null || echo 0) + LOW=$(jq '[.weak_points[] | select(.severity == "Low")] | length' panic-attack-findings.json 2>/dev/null || echo 0) + + echo "total=$TOTAL" >> "$GITHUB_OUTPUT" + echo "critical=$CRITICAL" >> "$GITHUB_OUTPUT" + echo "high=$HIGH" >> "$GITHUB_OUTPUT" + echo "medium=$MEDIUM" >> "$GITHUB_OUTPUT" + echo "low=$LOW" >> "$GITHUB_OUTPUT" + echo "exit_code=$PA_EXIT" >> "$GITHUB_OUTPUT" + - name: Write step summary + if: steps.install.outputs.installed == 'true' + run: | + cat <> "$GITHUB_STEP_SUMMARY" + ## panic-attack assail Results + + | Severity | Count | + |----------|-------| + | Critical | ${{ steps.assail.outputs.critical }} | + | High | ${{ steps.assail.outputs.high }} | + | Medium | ${{ steps.assail.outputs.medium }} | + | Low | ${{ steps.assail.outputs.low }} | + | **Total**| ${{ steps.assail.outputs.total }} | + + Known-legitimate residuals (audited, not yet suppressed via + \`audits/assail-classifications.a2ml\`): + - \`crypto/src/lib.rs\` UnsafeCode (FFI cdylib boundary — Ed448 + + Dilithium5/ML-DSA-87 signing shim, see \`crypto/README.md\`). + - \`src/verification/signing.jl\` / \`src/backends/zig_ffi.jl\` + UnsafeFFI (\`ccall\` into the same cdylib / the Zig compute layer). + EOF + - name: Create stub findings (when panic-attack unavailable) + if: steps.install.outputs.installed != 'true' + run: | + echo '{"weak_points":[]}' > panic-attack-findings.json + echo "## panic-attack assail" >> "$GITHUB_STEP_SUMMARY" + echo "" >> "$GITHUB_STEP_SUMMARY" + echo "Skipped: panic-attack not available in this environment." >> "$GITHUB_STEP_SUMMARY" + - name: Upload panic-attack findings + uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2 + with: + name: panic-attack-findings + path: panic-attack-findings.json + retention-days: 90 + - name: Fail on Critical or High findings + if: steps.install.outputs.installed == 'true' && (steps.assail.outputs.critical > 0 || steps.assail.outputs.high > 0) + run: | + echo "::error::panic-attack found ${{ steps.assail.outputs.critical }} critical and ${{ steps.assail.outputs.high }} high issue(s) — blocking merge" + echo "::error::If a finding is a known-legitimate residual (e.g. the crypto/ FFI shim), triage and record it via audits/assail-classifications.a2ml — do not bypass this gate." + exit 1 + + # --------------------------------------------------------------------------- + # Job 2: patch-bridge triage (crypto/Cargo.lock CVE contextual assessment) + # --------------------------------------------------------------------------- + patch-bridge-triage: + name: Patch Bridge CVE triage (crypto/) + needs: changes + if: needs.changes.outputs.run == 'true' + runs-on: ubuntu-latest + timeout-minutes: 15 + steps: + - name: Checkout repository + uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + with: + fetch-depth: 0 + - name: Install panic-attack (if available) + id: install + run: | + PA_URL="https://github.com/hyperpolymath/panic-attack/releases/latest/download/panic-attack-linux-x86_64" + if curl -fsSL --head "$PA_URL" >/dev/null 2>&1; then + curl -fsSL -o /usr/local/bin/panic-attack "$PA_URL" + chmod +x /usr/local/bin/panic-attack + echo "installed=true" >> "$GITHUB_OUTPUT" + else + echo "::notice::panic-attack binary not available — skipping Patch Bridge" + echo "installed=false" >> "$GITHUB_OUTPUT" + fi + - name: Run Patch Bridge triage against crypto/ + id: triage + if: steps.install.outputs.installed == 'true' + run: | + set +e + panic-attack bridge triage crypto --output bridge-report.json --offline + PB_EXIT=$? + set -e + + if [ ! -s bridge-report.json ] || ! jq empty bridge-report.json 2>/dev/null; then + echo '{"cves":[],"mitigated":0,"unmitigable":0,"concatenative":0,"informational":0}' > bridge-report.json + fi + + UNMITIGABLE=$(jq '.unmitigable // 0' bridge-report.json) + MITIGATED=$(jq '.mitigated // 0' bridge-report.json) + INFORMATIONAL=$(jq '.informational // 0' bridge-report.json) + + echo "unmitigable=$UNMITIGABLE" >> "$GITHUB_OUTPUT" + echo "mitigated=$MITIGATED" >> "$GITHUB_OUTPUT" + echo "informational=$INFORMATIONAL" >> "$GITHUB_OUTPUT" + - name: Write step summary + if: steps.install.outputs.installed == 'true' + run: | + cat <> "$GITHUB_STEP_SUMMARY" + ## Patch Bridge CVE Triage (crypto/) + + | Classification | Count | + |----------------|-------| + | Unmitigable | ${{ steps.triage.outputs.unmitigable }} | + | Mitigated | ${{ steps.triage.outputs.mitigated }} | + | Informational | ${{ steps.triage.outputs.informational }} | + EOF + - name: Create stub report (when unavailable) + if: steps.install.outputs.installed != 'true' + run: | + echo '{"cves":[],"mitigated":0,"unmitigable":0,"concatenative":0,"informational":0}' > bridge-report.json + echo "## Patch Bridge CVE Triage (crypto/)" >> "$GITHUB_STEP_SUMMARY" + echo "" >> "$GITHUB_STEP_SUMMARY" + echo "Skipped: panic-attack not available in this environment." >> "$GITHUB_STEP_SUMMARY" + - name: Upload bridge report + uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2 + with: + name: bridge-report + path: bridge-report.json + retention-days: 90 + - name: Warn on unmitigable CVEs + if: steps.install.outputs.installed == 'true' && steps.triage.outputs.unmitigable > 0 + run: | + echo "::warning::Patch Bridge found ${{ steps.triage.outputs.unmitigable }} unmitigable CVE(s) in crypto/ — review required" + # Warning only, not blocking — this is a cryptographic dependency, + # so an unmitigable finding needs a human architectural decision, + # not an automatic merge block. diff --git a/.machine_readable/policies/MAINTENANCE-AXES.a2ml b/.machine_readable/policies/MAINTENANCE-AXES.a2ml new file mode 100644 index 0000000..b76ae75 --- /dev/null +++ b/.machine_readable/policies/MAINTENANCE-AXES.a2ml @@ -0,0 +1,61 @@ +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Axiom.jl Contributors +# +# Canonical maintenance governance model — Axiom.jl + +[metadata] +version = "1.0.0" +last-updated = "2026-07-01" +scope = "repo" +repo = "Axiom.jl" + +[discovery] +human-entrypoints = [ + "README.md", + "ROADMAP.adoc", + "docs/governance/MAINTENANCE-CHECKLIST.adoc", + "docs/governance/SOFTWARE-DEVELOPMENT-APPROACH.adoc", +] +machine-entrypoints = [ + ".machine_readable/policies/MAINTENANCE-AXES.a2ml", + ".machine_readable/policies/MAINTENANCE-CHECKLIST.a2ml", + ".machine_readable/policies/SOFTWARE-DEVELOPMENT-APPROACH.a2ml", + ".machine_readable/6a2/META.a2ml", + ".machine_readable/bot_directives/README.adoc", +] +bots = ["hypatia", "gitbot-fleet", "repo visitors"] + +[axes] +axis-1 = "must > intend > like" +axis-2 = "corrective > adaptive > perfective" +axis-3 = "systems > compliance > effects" +execution-order = "axis-1 > axis-2 > axis-3" + +[axis-1-scoping] +required = true +sources = "README, ROADMAP.adoc, REGISTRY-READINESS.md, TEST-NEEDS.md, CI/security workflows" +markers = "TODO/FIXME/XXX/HACK/STUB/PARTIAL" +idris-unsound-markers = "believe_me/assert_total (src/Abi/*.idr, packages/SMTLib.jl/src/abi/*.idr)" +output = "scoped work assembly in must/intend/like buckets" + +[axis-2-maintenance] +corrective-first = true +adaptive-second = true +adaptive-focus = "scope changes, stale references, obsolete work culling" +perfective-third = true +perfective-source = "honest state from axis-1 after corrective/adaptive updates" + +[axis-3-audit] +systems-check = true +compliance-check = true +effects-check = true +compliance-focus = "seams/compromises/exception register and anti-drift — notably the crypto/ FFI cdylib boundary and the Idris2 ABI seam (src/Abi/, axiom-abi.ipkg)" +compliance-tooling = "panic-attack" +effects-tooling = "benchmark/ directory (framework_comparison.jl, threaded_benchmark.jl, gpu_performance_baseline.json)" +effects-evidence = "benchmark/results_*.md snapshots and maintainer status review" + +[axiom-specific-surfaces] +formal-abi = ".machine_readable-adjacent: axiom-abi.ipkg (Idris2), typechecked via idris2-abi-check in CI" +compute-layer = "zig/ (matmul, attention, norm, activations, pool, threading, conv, bench) + ffi/zig/ FFI bridge" +crypto-shim = "crypto/ (Rust cdylib axiom_crypto) — hybrid Ed448 + Dilithium5/ML-DSA-87 certificate signing" +gpu-extensions = "ext/AxiomCUDAExt.jl, AxiomAMDGPUExt.jl, AxiomMetalExt.jl (weakdeps-gated)" diff --git a/.machine_readable/policies/MAINTENANCE-CHECKLIST.a2ml b/.machine_readable/policies/MAINTENANCE-CHECKLIST.a2ml new file mode 100644 index 0000000..dd0a9be --- /dev/null +++ b/.machine_readable/policies/MAINTENANCE-CHECKLIST.a2ml @@ -0,0 +1,161 @@ +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Axiom.jl Contributors +# +# Maintenance baseline (machine-readable canonical) — Axiom.jl + +[metadata] +version = "1.0.0" +last-updated = "2026-07-01" +scope = "repo" +repo = "Axiom.jl" +source-human = "docs/governance/MAINTENANCE-CHECKLIST.adoc" +companion-human = "docs/governance/SOFTWARE-DEVELOPMENT-APPROACH.adoc" +companion-machine = ".machine_readable/policies/SOFTWARE-DEVELOPMENT-APPROACH.a2ml" + +[policy] +single-source = true +notes = "Use this file as canonical machine policy and keep docs/governance/MAINTENANCE-CHECKLIST.adoc synchronized." + +[maintenance-axes] +scoping-first = true +execution-order = ["scoping", "axis-1", "axis-2", "axis-3"] +axis-1 = "must > intend > like" +axis-2 = "corrective > adaptive > perfective" +axis-3 = "systems > compliance > effects" + +[scoping] +inputs_required = [ + "README", + "ROADMAP.adoc", + "REGISTRY-READINESS.md", + "TEST-NEEDS.md", + "ci-and-security-workflows", +] + +marker_scan_required = [ + "TODO", + "FIXME", + "XXX", + "HACK", + "STUB", + "PARTIAL", +] + +idris_unsound_scan_required = [ + "believe_me", + "assert_total", +] + +scope_assembly_buckets = ["must", "intend", "like"] + +[axis-2-maintenance-rules] +corrective-first = true +adaptive-second = true +adaptive_examples = [ + "scope-change reconciliation", + "stale-reference removal", + "obsolete-work culling", +] +perfective-third = true +perfective_source = "axis-1 honest state after corrective/adaptive updates" + +[axis-3-audit-rules] +systems-check = true +documentation-honesty-check = true +safety-security-accounted-check = true +effects-review-check = true +benchmark-evidence-required = true +maintainer-dialogue-review-required = true +compliance-seams-check = true +exception-register-required = true +exception-bounded-scope-required = true +policy-drift-contamination-check = true +compliance-tooling = "panic-attack" +effects-tooling = "benchmark/ (framework_comparison.jl, gpu_performance_baseline.json, threaded_benchmark.jl)" + +[generic-cleanup-finish-off] +root-cleanup-required = true +stale-work-cull-required = true +docs-parity-required = true +machine-human-sync-required = true +compliance-finish-off-required = true +effects-finish-off-required = true +release-prep-summary-required = true +next-actions-required = ["corrective", "adaptive", "perfective"] + +[must] +root_control_files = [ + ".editorconfig", + "guix.scm", + "setup.sh", + "Justfile", + "Mustfile", +] + +ownership_files = [ + "MAINTAINERS.adoc", +] + +machine_readable_required = [ + ".machine_readable/anchors/ANCHOR.a2ml", + ".machine_readable/contractiles/", + ".machine_readable/bot_directives/", + ".machine_readable/policies/", +] + +contractiles_required = [ + ".machine_readable/contractiles/Mustfile.a2ml", + ".machine_readable/contractiles/Trustfile.a2ml", + ".machine_readable/contractiles/Intentfile.a2ml", +] + +security_required = [ + ".well-known/security.txt", + ".github/workflows/hypatia-scan.yml", + ".github/workflows/secret-scanner.yml", + ".github/workflows/static-analysis-gate.yml", +] + +quality_gate_required = [ + "format", + "lint", + "unit-tests (test/runtests.jl)", + "property-tests (test/property_test.jl)", + "e2e-tests (test/e2e_test.jl)", + "bench-smoke (benchmark/threaded_benchmark.jl)", + "docs-check", + "security-scan (hypatia-scan.yml, secret-scanner.yml, static-analysis-gate.yml)", +] + +abi_ffi_policy = [ + "ABI Idris2 in src/Abi/*.idr (Types.idr, Layout.idr, Foreign.idr), typechecked via axiom-abi.ipkg", + "FFI Zig in zig/src/*.zig + ffi/zig/src/main.zig", + "Crypto FFI Rust cdylib in crypto/src/lib.rs (axiom_crypto), loaded via Libdl/ccall", +] + +[should] +docs_primary_format = "adoc (docs/governance/, docs/legal/, docs/compliance/); docs/wiki/ remains Markdown as the GitHub-wiki mirror" +docs_structure = [ + "docs/legal", + "docs/governance", + "docs/compliance", + "docs/accessibility", + "docs/design-diary", + "docs/wiki", +] + +root_minimization = true +well_known_metadata = true +roadmap_honesty_with_dates = true +ci_doc_format_policy = true + +[could] +generate_human_from_machine = true +mode_aware_bots = ["corrective", "adaptive", "perfective", "audit"] +exception_registry = "audits/assail-classifications.a2ml (planned, not yet authored — P5 phase per panic-attack CLAUDE.md User-Classification Registry)" + +[latest-execution-record] +date = "2026-07-01" +repo = "Axiom.jl" +branch = "claude/axiom-jl-registry-infra-kr7t4a" +notes = "Tier-2 compliance gates added: k9iser.toml, static-analysis-gate.yml, estate-rules.yml, docs/legal/{EXHIBIT-A,EXHIBIT-B}, docs/governance/{MAINTENANCE-CHECKLIST,SOFTWARE-DEVELOPMENT-APPROACH}.adoc, .machine_readable/policies/*. panic-attack assail run: 18 weak points (0 Critical, 2 High, 16 Medium), see docs/governance/MAINTENANCE-CHECKLIST.adoc Sec 'Latest Assail Baseline' for the full breakdown. No suppressions authored in this pass (P5 triage phase is separate)." diff --git a/.machine_readable/policies/SOFTWARE-DEVELOPMENT-APPROACH.a2ml b/.machine_readable/policies/SOFTWARE-DEVELOPMENT-APPROACH.a2ml new file mode 100644 index 0000000..7218cf1 --- /dev/null +++ b/.machine_readable/policies/SOFTWARE-DEVELOPMENT-APPROACH.a2ml @@ -0,0 +1,65 @@ +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Axiom.jl Contributors +# +# General software development approach (machine-readable) — Axiom.jl + +[metadata] +version = "1.0.0" +last-updated = "2026-07-01" +scope = "repo" +repo = "Axiom.jl" +source-human = "docs/governance/SOFTWARE-DEVELOPMENT-APPROACH.adoc" + +[execution] +order = ["axis-1", "axis-2", "axis-3"] + +[axis-1] +name = "scope" +priority = "must > intend > like" +inputs = [ + "README", + "ROADMAP.adoc", + "REGISTRY-READINESS.md", + "ci-and-security-workflows", +] +marker-scan = ["TODO", "FIXME", "XXX", "HACK", "STUB", "PARTIAL"] +idris-unsound-scan = ["believe_me", "assert_total"] +idris-unsound-scan-paths = ["src/Abi/", "packages/SMTLib.jl/src/abi/", "ffi/idris/"] +output = "scoped-work-assembly" + +[axis-2] +name = "maintenance" +priority = "corrective > adaptive > perfective" +corrective = "defect/regression/safety/security fixes" +adaptive = "scope reconciliation, stale-reference removal, obsolete-work culling" +perfective = "improve quality/clarity/performance only from the honest Axis 1 state" + +[axis-3] +name = "audit" +priority = "systems > compliance > effects" +systems = "required mechanisms exist and are operating (CI workflows, k9iser.toml, Justfile recipes)" +compliance = "seams/compromises/exceptions are explicit, bounded, and do not drift — the crypto/ FFI cdylib boundary and the Idris2 ABI seam are the two load-bearing seams in this repo" +effects = "benchmark and operational impact evidence is captured and reviewed (benchmark/ directory)" +compliance-tooling = "panic-attack" +effects-tooling = "benchmark/framework_comparison.jl, benchmark/threaded_benchmark.jl, benchmark/gpu_performance_baseline.json" + +[cleanup-finish-off] +root-cleanup = true +stale-work-cull = true +docs-sync-human-machine = true +compliance-audit = true +effects-audit = true +release-summary = ["must", "should", "could"] +next-actions = ["corrective", "adaptive", "perfective"] + +[collaboration] +maintainer-dialogue-required = true +dialogue-topics = ["what changed", "why", "remaining risks"] + +[axiom-specific] +formal-verification-tier = "fv" +load-bearing-seams = [ + "src/Abi/{Types,Layout,Foreign}.idr <-> axiom-abi.ipkg (Idris2 ABI, typechecked in CI: idris2-abi-check)", + "zig/src/*.zig <-> src/backends/zig_ffi.jl (Zig compute layer FFI)", + "crypto/src/lib.rs <-> src/verification/signing.jl (Rust cdylib, hybrid Ed448 + Dilithium5/ML-DSA-87 signing)", +] diff --git a/Justfile b/Justfile index 1846804..d33599e 100644 --- a/Justfile +++ b/Justfile @@ -86,9 +86,9 @@ status: @echo "Zig backend:" @test -f zig/zig-out/lib/libaxiom_zig.so && echo " Built" || echo " Not built (run: just build-zig)" -# Run panic-attacker pre-commit scan +# Run panic-attack pre-commit scan (renamed 2026-02-08: panic-attacker -> panic-attack) assail: - @command -v panic-attack >/dev/null 2>&1 && panic-attack assail . || echo "panic-attack not found — install from https://github.com/hyperpolymath/panic-attacker" + @command -v panic-attack >/dev/null 2>&1 && panic-attack assail . || echo "panic-attack not found — install from https://github.com/hyperpolymath/panic-attack" # ═══════════════════════════════════════════════════════════════════════════════ # ONBOARDING & DIAGNOSTICS diff --git a/Project.toml b/Project.toml index 1b93fd3..9000c24 100644 --- a/Project.toml +++ b/Project.toml @@ -8,7 +8,6 @@ authors = ["Jonathan D.A. Jewell "] Dates = "ade2ca70-3891-5945-98fb-dc099432e06a" HTTP = "cd3eb016-35fb-5094-929b-558a96fad6f3" JSON = "682c06a0-de6a-54ab-a142-c8b1cf79cde6" -JSON3 = "0f8b85d8-7281-11e9-16c2-39a750bddbf1" Libdl = "8f399da3-3557-5675-b5ff-fb832c97cbdb" LinearAlgebra = "37e2e46d-f89d-539d-b4ee-838fcccc9c8e" Random = "9a3f8284-a2c9-5f02-9a11-845980a1fd5c" @@ -33,16 +32,35 @@ AxiomPyTorchExt = "PyCall" AxiomSMTExt = "SMTLib" [compat] +AMDGPU = "1, 2" +Aqua = "0.8" +CUDA = "5, 6" Dates = "1" HTTP = "1.10.19" +JET = "0.9, 0.10" JSON = "0.21, 1" -JSON3 = "1.14.3" +KernelAbstractions = "0.9" +Libdl = "1" +LinearAlgebra = "1" +Metal = "1" +PyCall = "1" +Random = "1" SHA = "0.7, 1" -Zygote = "0.6" +Serialization = "1" +# SMTLib is the estate-internal package (packages/SMTLib.jl, uuid +# 7d3f9a2c-...) resolvable only inside this monorepo via the workspace/dev +# path -- it is not (yet) registered in General. The bound below tracks its +# own Project.toml version (currently 0.1.0) rather than a registry range. +SMTLib = "0.1" +Statistics = "1" +Test = "1" +Zygote = "0.6, 0.7" julia = "1.10" [extras] +Aqua = "4c88cf16-eb10-579e-8560-4a9242c79595" +JET = "c3a54625-cd67-489e-a8e7-0a5a0ff4e31b" Test = "8dfed614-e22c-5e08-85e1-65c5234f0b40" [targets] -test = ["Test"] +test = ["Aqua", "JET", "Test"] diff --git a/REGISTRY-READINESS.md b/REGISTRY-READINESS.md index c30446e..8d9d364 100644 --- a/REGISTRY-READINESS.md +++ b/REGISTRY-READINESS.md @@ -42,10 +42,46 @@ package submissions. The only thing that rebuilds that trust is honesty. - [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: unbound-params / undefined-exports / - project-extras pass; stale-deps **now clean** (orphaned - `src/integrations/huggingface.jl` + its sole-consumer dep `JSON3` - removed — they were unreachable dead code) +- [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 diff --git a/docs/Project.toml b/docs/Project.toml new file mode 100644 index 0000000..2afaa0a --- /dev/null +++ b/docs/Project.toml @@ -0,0 +1,8 @@ +# SPDX-License-Identifier: MPL-2.0 +[deps] +Axiom = "bbd403f8-dcc5-405a-84eb-8de9d358675c" +Documenter = "e30172f5-a6a5-5a46-863b-614d45cd2de4" + +[compat] +Documenter = "1" +julia = "1.10" diff --git a/docs/governance/MAINTENANCE-CHECKLIST.adoc b/docs/governance/MAINTENANCE-CHECKLIST.adoc new file mode 100644 index 0000000..ab1f551 --- /dev/null +++ b/docs/governance/MAINTENANCE-CHECKLIST.adoc @@ -0,0 +1,202 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2026 Axiom.jl Contributors += Maintenance Checklist — Axiom.jl +:toc: left +:toclevels: 2 + +Repeatable maintenance runbook for Axiom.jl. + +Companion policy: + +* `.machine_readable/policies/MAINTENANCE-CHECKLIST.a2ml` (machine-readable, canonical) +* `docs/governance/SOFTWARE-DEVELOPMENT-APPROACH.adoc` (human-readable) +* `.machine_readable/policies/SOFTWARE-DEVELOPMENT-APPROACH.a2ml` (machine-readable) + +== Three-Axis Default Model + +* Axis 1 (scope priority, runs first): `must > intend > like` +* Axis 2 (maintenance priority): `corrective > adaptive > perfective` +* Axis 3 (audit priority): `systems > compliance > effects` +* Perfective items are derived from Axis 1 honest state (not started independently). + +== Axis 1 — Scoping Pass (Mandatory) + +Before Axis 2/3 execution, assemble a scoped worklist from evidence: + +* Read and reconcile: `README.md`, `ROADMAP.adoc`, `REGISTRY-READINESS.md`, `TEST-NEEDS.md`, and current CI/security workflow definitions under `.github/workflows/`. +* Scan for unfinished markers: `TODO`, `FIXME`, `XXX`, `HACK`, `STUB`, `PARTIAL`. +* Scan Idris2 unsoundness markers in `src/Abi/*.idr`, `packages/SMTLib.jl/src/abi/*.idr`, and `ffi/idris/*.idr`: `believe_me`, `assert_total`. +* Identify declared intent vs. actual implementation (docs-honesty check) — e.g. does `ROADMAP.adoc` still list the hybrid Ed448+Dilithium5 signing as a TODO after `crypto/` shipped it? +* Produce a scope-assembly artefact with prioritized entries under `must` / `intend` / `like`. + +== Axis 2 — Maintenance Execution Rules + +* Corrective first: fix breakage, defects, regressions, safety issues (e.g. a broken `ccall` signature into `crypto/` or `zig/`). +* Adaptive second: reconcile changed scope, remove stale references, cull no-longer-relevant work. +* Perfective third: only from the current honest state established by Axis 1 and updated by corrective/adaptive actions. + +== Axis 3 — Audit Rules + +* Verify systems are in place and actually operating: CI workflows run green, `k9iser.toml` constraints are satisfiable, Justfile recipes work. +* Verify documentation explains the real/current state (not aspirational-only), including documented exceptions. +* Verify safety and security controls are present, active, and evidenced — notably the two load-bearing seams in this repo: +** The Idris2 ABI (`src/Abi/`, `axiom-abi.ipkg`), typechecked in CI (`idris2-abi-check`). +** The `crypto/` Rust cdylib FFI boundary (hybrid Ed448 + Dilithium5/ML-DSA-87 signing), loaded via `Libdl`/`ccall` from `src/verification/signing.jl`. +* Verify observed effects/impacts are captured and reviewed: +** benchmark execution and recorded results (`benchmark/results_*.md`, `benchmark/gpu_performance_baseline.json`) +** explicit maintainer dialogue/status review on what changed, why, and next risks +* Audit compliance seams/compromises explicitly: +** policy exceptions are recorded with rationale, scope, and expiry/review +** exception does not silently broaden into general policy drift +** run `panic-attack assail` as the compliance-audit scanner (see `.github/workflows/static-analysis-gate.yml`) + +== Panic/Safety/Security Pass + +* Run `just assail` (wraps `panic-attack assail .`). +* Triage findings by severity: Critical/High block, Medium/Low get scheduled. +* Fix High first, then Medium. +* Re-run until acceptable. + +[source,bash] +---- +panic-attack assail /path/to/Axiom.jl --output /tmp/axiom-assail.json --verbose +jq -r '.weak_points | length' /tmp/axiom-assail.json +jq -r '.weak_points[] | "\(.severity)|\(.category)|\(.file)"' /tmp/axiom-assail.json +---- + +=== Latest Assail Baseline (2026-07-01) + +Ground-truthed by actually running the tool (not a status-doc claim): + +[cols="1,1,3"] +|=== +| Severity | Count | Notes + +| Critical +| 0 +| None found. + +| High +| 2 +| `UnsafeCode` in `crypto/src/lib.rs` (21 `unsafe` blocks — the C-ABI `extern "C"` surface itself, expected for a cdylib boundary); `ProofDrift` in `test/verification/proof_export_tests.jl` (a `# sorry`/`# TODO: prove`-style proof-substitute comment). + +| Medium +| 16 +| Mostly `ProofDrift` (12× type-only `@test x isa Y` assertions across `test/` and `packages/SMTLib.jl/test/`, which stand in for unwritten formal theorems), 2× `UnsafeFFI` (`ccall` sites in `src/verification/signing.jl` and `src/backends/zig_ffi.jl` — the same FFI boundary as the High UnsafeCode finding, viewed from the Julia side), 2× `InputBoundary` (`JSON3.read`/`JSON.parse` without `try`/`catch` in `src/verification/serialization.jl` and its test), 1× `MutationGap` (`test/ci/backend_parity.jl` has only type-only assertions). + +| Low +| 0 +| None found. +|=== + +**Known-legitimate residuals** (audited but not yet formally suppressed — that +suppression step is a separate P5 phase, see `panic-attack`'s +User-Classification Registry convention): the `crypto/` `UnsafeCode` finding +and both `UnsafeFFI` findings are the expected shape of a Rust-cdylib + +Zig-compute-layer FFI boundary loaded via `ccall`. They are flagged here for +future audit-file authorship (`audits/assail-classifications.a2ml`), not +suppressed in this pass. + +Full JSON report from this run: `/tmp/axiom-assail.json` (not committed — +regenerate via `just assail` or the command above). + +== Language-Specific Validation + +=== Julia + +* Format/lint (project convention). +* `julia --project=. -e 'using Pkg; Pkg.test()'` (unit + property + e2e suites under `test/`). +* Benchmark smoke: `benchmark/threaded_benchmark.jl`. + +=== Rust (crypto/) + +[source,bash] +---- +cd crypto +cargo fmt --all --check +cargo clippy --all-targets -- -D warnings +cargo test +---- + +=== Zig (zig/, ffi/zig/) + +[source,bash] +---- +cd zig && zig build test +cd ffi/zig && zig build test +---- + +=== Idris2 (src/Abi/) + +[source,bash] +---- +idris2 --typecheck axiom-abi.ipkg +---- + +== Final QA and Release Hygiene + +* Re-run full relevant checks one final time. +* Confirm no unintended file changes. +* Commit scoped changes with a clear message. +* Push and capture the commit SHA. + +== Maintenance Report Template + +Copy this block per maintenance run: + +[source,text] +---- +Repo: Axiom.jl +Branch: +Start UTC: +End UTC: + +Scope: +- Corrective: +- Adaptive: +- Perfective: + +Checks Run: +- TODO/FIXME scan: +- panic-attack assail: +- Julia/Rust/Zig/Idris2 checks: +- Benchmark checks: + +Findings: +- Critical: +- High: +- Medium: +- Low: + +Fixes Applied: +1. +2. + +Validation Results: +- Tests: +- Benchmarks: +- panic-attack rerun: + +Artifacts: +- assail report: +- benchmark output: + +Commit(s): +- SHA: + +Remaining Risks / Follow-ups: +1. +2. +---- + +== AI Execution Integrity Contract + +Use this when delegating maintenance to any AI agent working on this repo. + +* Do not claim any step is complete unless it actually ran. +* Do not silently skip checklist items — state SKIPPED plus the exact reason. +* For every check, provide evidence: command executed, pass/fail/warn, key output summary, artifact/log path. +* If a command fails, stop claiming success and report the failure clearly. +* After each fix, re-run the relevant failing check and report the rerun result. +* Never mark "all done" while any fail/warn remains unexplained. +* Fail closed: if evidence is missing for any checklist item, treat that item as NOT DONE. diff --git a/docs/governance/SOFTWARE-DEVELOPMENT-APPROACH.adoc b/docs/governance/SOFTWARE-DEVELOPMENT-APPROACH.adoc new file mode 100644 index 0000000..2d3a2f0 --- /dev/null +++ b/docs/governance/SOFTWARE-DEVELOPMENT-APPROACH.adoc @@ -0,0 +1,86 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2026 Axiom.jl Contributors += Software Development Approach — Axiom.jl +:toc: left +:toclevels: 2 + +This is the operating policy for software development on Axiom.jl, a Julia +ML/numerics framework with a Zig compute layer, an Idris2-specified ABI, and +a Rust cdylib crypto shim implementing hybrid post-quantum certificate +signing. + +Machine-readable companion: `.machine_readable/policies/SOFTWARE-DEVELOPMENT-APPROACH.a2ml`. + +== Core Sequence + +Always run work in this order: + +. Scope first (Axis 1) +. Maintenance second (Axis 2) +. Audit third (Axis 3) + +== Axis Definitions + +=== Axis 1: Scope + +Priority order: `must > intend > like` + +Axis 1 output is a scoped assembly of work based on: + +* `README.md`, `ROADMAP.adoc`, `REGISTRY-READINESS.md`, `TEST-NEEDS.md`, CI/security workflow definitions +* marker scans (`TODO`, `FIXME`, `XXX`, `HACK`, `STUB`, `PARTIAL`) +* Idris2 unsoundness scan against `src/Abi/*.idr`, `packages/SMTLib.jl/src/abi/*.idr`, `ffi/idris/*.idr` (`believe_me`, `assert_total`) +* docs-honesty check (intent vs. actual implementation) — Axiom.jl's `ROADMAP.adoc` has previously drifted from shipped reality (e.g. the hybrid signing capability landing before the roadmap was updated); re-check this on every pass + +=== Axis 2: Maintenance + +Priority order: `corrective > adaptive > perfective` + +* Corrective: fix defects, regressions, breakage, security/safety failures — including breakage at either FFI seam (`crypto/`, `zig/`) or the Idris2 ABI seam (`src/Abi/`) +* Adaptive: reconcile scope changes, remove stale references, cull obsolete work +* Perfective: improve quality/clarity/performance only from the honest Axis 1 state + +=== Axis 3: Audit + +Priority order: `systems > compliance > effects` + +* Systems: required mechanisms exist and are operating — CI workflows (`.github/workflows/`), `k9iser.toml` constraints, `Justfile` recipes (`just assail`, `just build-crypto`, `just build-zig`) +* Compliance: seams/compromises/exceptions are explicit, bounded, and do not drift. Axiom.jl's two load-bearing seams are: +** the Idris2 ABI (`src/Abi/{Types,Layout,Foreign}.idr` <-> `axiom-abi.ipkg`, typechecked in CI via `idris2-abi-check`) +** the `crypto/` Rust cdylib FFI boundary (hybrid Ed448 + Dilithium5/ML-DSA-87 signing, `crypto/src/lib.rs` <-> `src/verification/signing.jl`) +* Effects: benchmark and operational impact evidence is captured and reviewed (`benchmark/` — `framework_comparison.jl`, `threaded_benchmark.jl`, `gpu_performance_baseline.json`, dated `results_*.md` snapshots) + +Compliance scanner baseline: `panic-attack` (see `.github/workflows/static-analysis-gate.yml` and `docs/governance/MAINTENANCE-CHECKLIST.adoc` for the latest ground-truthed finding counts). + +== Generic Cleanup And Finish-Off + +At cycle end: + +* reduce root clutter to required control/entry files +* archive/remove stale or superseded work +* synchronize human and machine docs (`docs/governance/*.adoc` <-> `.machine_readable/policies/*.a2ml`) +* run compliance and effects audits with evidence capture +* produce Must/Should/Could summary and immediate next-actions list + +== Collaboration Rule + +Effects review must include explicit maintainer dialogue: + +* what changed +* why it changed +* what risks remain + +== Formal-Verification Tier + +Axiom.jl runs at safety-tier `fv` (formal verification) in `k9iser.toml`, +distinct from a plain numerics package, because it carries: + +* a genuine Idris2 ABI specification (not just documentation) that is + typechecked in CI; +* a genuine post-quantum cryptographic signing implementation + (`crypto/`), not a placeholder or a policy aspiration — see + `docs/legal/EXHIBIT-B-QUANTUM-SAFE.txt`. + +Both surfaces widen the attack surface (FFI boundaries, `unsafe` blocks) in +ways that are expected and audited, not accidental — see the Latest Assail +Baseline in `docs/governance/MAINTENANCE-CHECKLIST.adoc`. diff --git a/docs/legal/EXHIBIT-A-ETHICAL-USE.txt b/docs/legal/EXHIBIT-A-ETHICAL-USE.txt new file mode 100644 index 0000000..518b35c --- /dev/null +++ b/docs/legal/EXHIBIT-A-ETHICAL-USE.txt @@ -0,0 +1,34 @@ +SPDX-License-Identifier: MPL-2.0 + +================================================================================ +EXHIBIT A — SOURCE CODE FORM LICENSE NOTICE +Mozilla Public License Version 2.0 +Axiom.jl +================================================================================ + + This Source Code Form is subject to the terms of the Mozilla Public + License, v. 2.0. If a copy of the MPL was not distributed with this + file, You can obtain one at https://mozilla.org/MPL/2.0/. + +If it is not possible or desirable to put the notice in a particular file, +then You may include the notice in a location (such as a LICENSE file) where +a recipient would be likely to look for such a notice. + +You may add additional accurate notices of copyright ownership. + +Axiom.jl is dual-licensed at the artefact level, per REUSE conventions: + + - Source code (Julia, Rust, Zig, Idris2) is MPL-2.0. This covers `src/`, + `ext/`, `crypto/`, `zig/`, `ffi/`, `packages/SMTLib.jl/`, `scripts/`, + `test/`, `benchmark/`, and the axiom-abi.ipkg / Justfile / Mustfile + build definitions. + - Prose documentation (this exhibit's sibling `.adoc` files under `docs/`, + and Markdown files that are the GitHub-wiki mirror under `docs/wiki/`) + is CC-BY-SA-4.0 unless a file's own SPDX header states otherwise. + +Full license texts are at `LICENSE` (root) and `LICENSES/MPL-2.0.txt`, +`LICENSES/CC-BY-SA-4.0.txt`. + +================================================================================ +END OF EXHIBIT A +================================================================================ diff --git a/docs/legal/EXHIBIT-B-QUANTUM-SAFE.txt b/docs/legal/EXHIBIT-B-QUANTUM-SAFE.txt new file mode 100644 index 0000000..a8aa678 --- /dev/null +++ b/docs/legal/EXHIBIT-B-QUANTUM-SAFE.txt @@ -0,0 +1,163 @@ +SPDX-License-Identifier: MPL-2.0 + +================================================================================ +QUANTUM-SAFE PROVENANCE SPECIFICATION +Axiom.jl — Exhibit B +================================================================================ + +0. STATUS — THIS IS NOT ASPIRATIONAL + + Unlike the generic RSR template version of this exhibit, this repository + SHIPS a real, working implementation of the scheme described below: the + `crypto/` crate (`axiom_crypto`, a Rust `cdylib` loaded from Julia via + `ccall`/`Libdl`, see `src/verification/signing.jl` and + `crypto/README.md`). The hybrid Ed448 + Dilithium5 (ML-DSA-87) signing + path is real code with real tests, not a policy placeholder. + +1. PURPOSE + + This exhibit specifies the cryptographic algorithms and procedures Axiom.jl + uses for quantum-safe provenance of verification certificates. It is a + standalone, licence-agnostic specification: it imposes no licence terms + of its own and may be referenced by software under any licence (this + repository is MPL-2.0 for code, CC-BY-SA-4.0 for prose). + +2. ALGORITHMS ACTUALLY IN USE (this repository) + + 2.1. Digital Signatures — Hybrid scheme, both required to pass + - Ed448 (RFC 8032, EdDSA over Curve448) — the classical half. + Implemented via the system libcrypto (OpenSSL 3.x) through the + vetted Rust `openssl` crate. No hand-rolled elliptic-curve code. + - Dilithium5 / ML-DSA-87 (FIPS 204) — the post-quantum half. + Implemented via the vetted Rust `pqcrypto-dilithium` crate + (PQClean reference implementation). No hand-rolled lattice code. + - Both signatures are required to verify (`hybrid_verify`); this + mirrors the "hybrid signatures encouraged during transition" + guidance in §6 below, but Axiom.jl treats the PQ half as + mandatory rather than optional, given the FFI-boundary and + certificate-authenticity stakes involved. + + 2.2. Key sizes (from `crypto/README.md`, C ABI length getters) + - Ed448 public key: 57 bytes; secret key: 57 bytes; signature: + 114 bytes. + - Dilithium5 (ML-DSA-87) public key: 2592 bytes; secret key: 4896 + bytes; signature: up to 4627 bytes (variable-length, bounded). + + 2.3. Hash Functions + - SHA-256, via Julia's `SHA` stdlib, for the default (non-PQ) + certificate content digest (`src/verification/certificates.jl`, + `authenticated=false` mode — the always-on baseline). + - The hybrid PQ signature path (§2.1) signs over this same + certificate content; it does not replace the digest, it adds an + opt-in authenticating signature layer on top of it. + + 2.4. Algorithms considered but NOT currently implemented here + - ML-KEM (FIPS 203) key encapsulation: not needed — Axiom.jl signs + certificates, it does not encrypt provenance metadata for + transport. + - SLH-DSA (FIPS 205) / FALCON: not implemented. Dilithium5 was + selected to match the estate Trustfile hybrid scheme used + elsewhere (see `opsm_ex/native/opsm_pq_nif`, the Elixir/BEAM + reference implementation this crate's algorithm choice mirrors, + per `crypto/README.md`). A future revision MAY add SLH-DSA as a + third factor; this is not committed. + +3. PROVENANCE METADATA FORMAT (certificate fields, this implementation) + + 3.1. Required Fields (see `src/verification/certificates.jl` / + `src/verification/signing.jl`) + - content-hash: SHA-256 digest of the certificate content + (always present, even when `authenticated=false`). + - hybrid-signature: present only when the opt-in authenticating + path is used — pairs `(ed448_signature, dilithium5_signature)`, + both over the same message. + - public keys: Ed448 and Dilithium5 PUBLIC keys only, hex-encoded + (`hybrid_signature_to_dict`). Private keys are never serialized + by this crate — see §5. + + 3.2. Optional Fields + - parent-hash / witnesses / context-notes are not currently + modelled in the certificate schema; this is a documented gap, + not a silent omission — see `ROADMAP.adoc` for the key-custody + and certificate-schema roadmap. + +4. SIGNATURE PROCEDURE (as implemented) + + 4.1. Signing (`axiom_crypto_ed448_sign` / `axiom_crypto_dilithium5_sign`, + both `extern "C"` / `#[no_mangle]`, called from Julia via `ccall`) + a. Compute the certificate content (SHA-256 digest already present + from the default, non-PQ path). + b. Sign the same message independently with Ed448 and Dilithium5. + c. Attach both signatures to the certificate + (`hybrid_signature_to_dict`). + d. `panic = "abort"` is set in `crypto/Cargo.toml` as a defence-in- + depth backstop: every exported function is written to catch + errors internally and return a status code (`i32`; 0 = OK, + negative = error) rather than unwind, because unwinding across + the C ABI / `ccall` boundary is undefined behaviour. + + 4.2. Verification (`axiom_crypto_ed448_verify` / + `axiom_crypto_dilithium5_verify`) + a. Extract both signatures and both public keys from the + certificate. + b. Verify Ed448 first, then Dilithium5 (or vice versa) — BOTH must + return valid (`1`) for the hybrid signature to be accepted. + c. Verify the content hash matches the actual certificate content. + d. A negative return value from either verify call means the call + itself could not be carried out (bad pointer, bad length) — + distinct from "ran and returned invalid" (a forged/tampered + certificate). Callers must not conflate the two. + +5. KEY MANAGEMENT (as implemented — read before assuming HSM integration) + + 5.1. This crate NEVER reads or writes private key material to disk on + its own. Keys are either: + - generated in-memory for tests/examples only + (`*_keypair` functions in `crypto/src/lib.rs`), or + - generated and held out-of-band by an HSM or an offline signing + process, with only the PUBLIC keys ever embedded in a + certificate (see `crypto/README.md`, "Private key custody"). + No `.pem`/`.key` file produced by a real signing key may ever enter + this repository. This is an enforced convention, not aspirational + guidance — `crypto/.gitignore` and the review process are the + current controls; formal HSM integration is tracked in + `ROADMAP.adoc`, not yet implemented. + + 5.2. Key rotation policy: not yet automated in this repository. Treat + rotation as a manual, out-of-band operational procedure until + `ROADMAP.adoc`'s custody story is implemented. + +6. TRANSITION PERIOD + + 6.1. Axiom.jl's DEFAULT certificate path (`generate_certificate`, + `authenticated=false`) remains a SHA-256 content digest with no + signature at all — this is the baseline, unconditionally available + without the `crypto/` cdylib being built. + 6.2. The hybrid Ed448 + Dilithium5 path (§2.1) is opt-in, on top of the + default digest, and — unlike the generic RSR guidance that treats + hybrid signing as merely "encouraged" — Axiom.jl requires BOTH + halves to verify once the opt-in path is engaged; there is no + "classical-signature-only" mode in this implementation. + 6.3. Pure-PQ-only (dropping the Ed448 half) is not implemented and not + currently planned — the hybrid pairing is the estate Trustfile + convention this crate follows. + +7. COMPLIANCE + + Quantum-safe signing is OPTIONAL at the certificate-generation call site + (`authenticated=false` remains the default), but once a certificate + carries a hybrid signature, both the Ed448 and Dilithium5 signatures + MUST verify for the certificate to be accepted as authenticated; a + hybrid signature must never be partially stripped (e.g. keeping only + the classical half) from a distribution that carries it. + + FFI/UnsafeCode residual: `crypto/src/lib.rs`'s `unsafe` blocks (the C-ABI + `extern "C"` surface itself) and the `ccall` sites in + `src/verification/signing.jl` / `src/backends/zig_ffi.jl` are expected, + legitimate residuals of this design — see the `panic-attack assail` + findings referenced in `docs/governance/MAINTENANCE-CHECKLIST.adoc` and, + once written, `audits/assail-classifications.a2ml`. + +================================================================================ +END OF EXHIBIT B +================================================================================ diff --git a/docs/make.jl b/docs/make.jl new file mode 100644 index 0000000..a39adbd --- /dev/null +++ b/docs/make.jl @@ -0,0 +1,60 @@ +# SPDX-License-Identifier: MPL-2.0 +# Documenter build script (G13). +# +# Run locally with: julia --project=docs docs/make.jl +# +# `docs/Project.toml` lists Axiom itself as a dep so it resolves inside the +# docs environment, but it is not registered -- `Pkg.develop` below points +# it at this checkout (the parent of `docs/`) rather than requiring a +# registry entry. This must run before `using Axiom`. + +using Pkg +Pkg.develop(Pkg.PackageSpec(path = joinpath(@__DIR__, ".."))) + +using Documenter +using Axiom + +DocMeta.setdocmeta!(Axiom, :DocTestSetup, :(using Axiom); recursive = true) + +# Deploying to GitHub Pages requires `GITHUB_TOKEN`/`DOCUMENTER_KEY` and a +# real CI environment (git remote, `GITHUB_ACTIONS`, etc.). Guard it so a +# local `julia --project=docs docs/make.jl` build/doctest run always +# succeeds even outside CI: `deploydocs` is skipped unless we can detect +# we're actually running inside GitHub Actions on this repo. +const IS_CI = get(ENV, "GITHUB_ACTIONS", "false") == "true" + +makedocs(; + modules = [Axiom], + sitename = "Axiom.jl", + authors = "Jonathan D.A. Jewell ", + doctest = true, + checkdocs = :none, + # Explicit `repo` (rather than relying on Documenter's git-remote + # auto-detection): in sandboxed/CI checkouts `origin` may point at a + # proxy/mirror URL rather than a real `github.com` remote, which makes + # `interpret_repo_and_remotes` error out before `makedocs` can run at + # all. A `Remotes.GitHub` object fully specifies the remote (unlike a + # bare template string, which only silences the *link-construction* + # error but leaves the navbar-link URL undeterminable), so the local + # build/doctest run works regardless of what `git remote -v` shows. + repo = Remotes.GitHub("hyperpolymath", "Axiom.jl"), + format = Documenter.HTML(; + prettyurls = IS_CI, + edit_link = "main", + ), + pages = [ + "Home" => "index.md", + "Tensors & Layers" => "api-core.md", + "Training & Automatic Differentiation" => "api-training.md", + "Verification & Certification" => "api-verification.md", + "Backends, Serving & Interop" => "api-serving.md", + ], + warnonly = [:missing_docs, :cross_references], +) + +if IS_CI + deploydocs(; + repo = "github.com/hyperpolymath/Axiom.jl.git", + devbranch = "main", + ) +end diff --git a/docs/src/api-core.md b/docs/src/api-core.md new file mode 100644 index 0000000..8dd61a9 --- /dev/null +++ b/docs/src/api-core.md @@ -0,0 +1,26 @@ + + +# Tensors & Layers + +Core tensor types, shapes, and neural network layers. + +```@autodocs +Modules = [Axiom] +Public = true +Private = false +Pages = [ + "types/tensor.jl", + "types/shapes.jl", + "types/math.jl", + "layers/abstract.jl", + "layers/dense.jl", + "layers/conv.jl", + "layers/activations.jl", + "layers/normalization.jl", + "layers/pooling.jl", + "layers/invertible.jl", +] +``` diff --git a/docs/src/api-serving.md b/docs/src/api-serving.md new file mode 100644 index 0000000..9447497 --- /dev/null +++ b/docs/src/api-serving.md @@ -0,0 +1,25 @@ + + +# Backends, Serving & Interop + +Accelerator backend abstraction (CPU/Zig/GPU/coprocessor), model serving +(REST/GraphQL/gRPC), PyTorch/ONNX interop, and model metadata/packaging. + +```@autodocs +Modules = [Axiom] +Public = true +Private = false +Pages = [ + "backends/abstract.jl", + "backends/julia_backend.jl", + "backends/gpu_hooks.jl", + "backends/zig_ffi.jl", + "serving/api.jl", + "integrations/interop.jl", + "model_metadata.jl", + "model_packaging.jl", +] +``` diff --git a/docs/src/api-training.md b/docs/src/api-training.md new file mode 100644 index 0000000..a6f880f --- /dev/null +++ b/docs/src/api-training.md @@ -0,0 +1,29 @@ + + +# Training & Automatic Differentiation + +Optimizers, loss functions, the training loop, automatic differentiation, +and the `@axiom` / `@ensure` / `@prove` declarative DSL. + +```@autodocs +Modules = [Axiom] +Public = true +Private = false +Pages = [ + "dsl/axiom_macro.jl", + "dsl/ensure.jl", + "dsl/prove.jl", + "dsl/pipeline.jl", + "autograd/gradient.jl", + "autograd/tape.jl", + "autograd/invertible_rules.jl", + "training/optimizers.jl", + "training/loss.jl", + "training/train.jl", + "utils/data.jl", + "utils/initialization.jl", +] +``` diff --git a/docs/src/api-verification.md b/docs/src/api-verification.md new file mode 100644 index 0000000..78e3cdc --- /dev/null +++ b/docs/src/api-verification.md @@ -0,0 +1,25 @@ + + +# Verification & Certification + +Formal property specification, checking, certificate generation and +serialization, hybrid Ed448+Dilithium5 signing, and proof-assistant export +(Lean/Coq/Isabelle). + +```@autodocs +Modules = [Axiom] +Public = true +Private = false +Pages = [ + "verification/properties.jl", + "verification/checker.jl", + "verification/certificates.jl", + "verification/serialization.jl", + "verification/signing.jl", + "verification/verification.jl", + "proof_export.jl", +] +``` diff --git a/docs/src/index.md b/docs/src/index.md new file mode 100644 index 0000000..73a6d6f --- /dev/null +++ b/docs/src/index.md @@ -0,0 +1,28 @@ + + +# 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/k9iser.toml b/k9iser.toml new file mode 100644 index 0000000..fdaee02 --- /dev/null +++ b/k9iser.toml @@ -0,0 +1,88 @@ +# SPDX-License-Identifier: MPL-2.0 +# k9iser manifest — wrap configs into self-validating K9 contracts +# +# Axiom.jl: Julia ML/numerics framework with a Zig compute layer +# (zig/, ffi/zig/), a formally-specified Idris2 ABI (src/Abi/, +# axiom-abi.ipkg), and a Rust cdylib crypto shim (crypto/) implementing the +# estate hybrid Trustfile scheme (Ed448 classical + Dilithium5/ML-DSA-87 +# post-quantum certificate signing, FIPS 204). Safety-tier "fv" (formal +# verification) — this repo carries a real formal-ABI surface plus a genuine +# cryptographic attack surface (FFI boundary + PQ signing), not just +# numerics; both must be held to formal-verification-adjacent scrutiny. + +[project] +name = "Axiom.jl" +safety-tier = "fv" # formal-verification tier — Idris2 ABI + PQ crypto surface + +# ── Project.toml — Julia package manifest ──────────────────────────────────── + +[[configs]] +name = "julia-package-manifest" +source = "Project.toml" +format = "toml" +must = [ + "name == 'Axiom'", + "uuid is set", + "license == 'MPL-2.0'", + "authors is non-empty", + "version is set", + "compat.julia is set", # minimum Julia version pinned + "no dependency on PyCall unless behind [weakdeps]", # Python interop is opt-in only, never a hard dep + "extensions.AxiomCUDAExt implies weakdeps.CUDA is set", + "extensions.AxiomAMDGPUExt implies weakdeps.AMDGPU is set", + "extensions.AxiomMetalExt implies weakdeps.Metal is set", + "extensions.AxiomSMTExt implies weakdeps.SMTLib is set", +] +trust = ["signed-by: ci-pipeline"] +dust = ["remove: unused weakdeps/extensions pairs"] +intend = ["production-ready", "registry-ready"] + +# ── axiom-abi.ipkg — Idris2 formal ABI package ──────────────────────────────── + +[[configs]] +name = "idris2-abi" +source = "axiom-abi.ipkg" +format = "ipkg" +must = [ + "package == 'axiom-abi'", + "sourcedir == 'src'", + "modules contains 'Abi.Types'", + "modules contains 'Abi.Layout'", + "modules contains 'Abi.Foreign'", + "depends contains 'base'", + "no module uses 'believe_me'", # unsoundness marker — banned in the ABI surface + "no module uses 'assert_total' without a documented termination proof", + "typechecks-in-ci == true", # axiom-abi.ipkg must be gated by idris2 --typecheck, not just authored +] +trust = ["signed-by: ci-pipeline", "typechecked-by: idris2-abi-check"] +dust = ["remove: unreferenced Abi modules"] +intend = ["formally-verified-abi", "zero-unsoundness-markers"] + +# ── crypto/Cargo.toml — Rust PQ-crypto cdylib shim ─────────────────────────── + +[[configs]] +name = "crypto-shim-manifest" +source = "crypto/Cargo.toml" +format = "toml" +must = [ + "package.name == 'axiom_crypto'", + "package.edition == '2021'", + "package.license == 'MPL-2.0'", + "package.publish == false", # cdylib is a build artifact consumed via ccall, never published to crates.io + "lib.crate-type contains 'cdylib'", + "dependencies.openssl is set", # Ed448 classical signature via vetted system libcrypto + "dependencies.pqcrypto-dilithium is set", # Dilithium5 / ML-DSA-87 post-quantum signature via PQClean reference impl + "no dependency on md5", # MD5 banned for security-relevant crate + "no dependency on sha1", # SHA-1 banned for security-relevant crate + "no hand-rolled cryptographic primitives", # both algorithms MUST come from vetted crates, never reimplemented + "profile.release.panic == 'abort'", # unwinding across the C-ABI/ccall boundary is UB — abort is the defence-in-depth backstop + "private keys never read/written to disk by this crate", # key custody stays out-of-band (HSM / offline signing per ROADMAP.adoc) +] +trust = ["signed-by: ci-pipeline"] +dust = ["remove: unused pqcrypto feature flags"] +intend = ["production-ready", "quantum-safe", "ffi-boundary-sealed"] + +[validation] +strict = true +auto-fix = false +report-format = "text" diff --git a/src/layers/normalization.jl b/src/layers/normalization.jl index d86ad84..9829f05 100644 --- a/src/layers/normalization.jl +++ b/src/layers/normalization.jl @@ -87,6 +87,22 @@ mutable struct LayerNorm{T, S} <: AbstractLayer normalized_shape::S eps::Float32 elementwise_affine::Bool + + # Explicit inner constructor (Aqua G07): both `γ` and `β` are + # `Union{_, Nothing}`-typed, so Julia's auto-generated default + # positional constructor leaves `T` unbound (passing `nothing` for + # both pins no concrete `T`). This constructor takes `T`/`S` from the + # `{T, S}` type application itself, so `T`/`S` are always bound + # regardless of whether `γ`/`β` are `nothing`. + function LayerNorm{T, S}( + γ::Union{Array{T}, Nothing}, + β::Union{Array{T}, Nothing}, + normalized_shape::S, + eps::Float32, + elementwise_affine::Bool, + ) where {T, S} + new{T, S}(γ, β, normalized_shape, eps, elementwise_affine) + end end function LayerNorm( @@ -168,6 +184,21 @@ mutable struct InstanceNorm{T} <: AbstractLayer eps::Float32 affine::Bool num_features::Int + + # Explicit inner constructor (Aqua G07): see LayerNorm's constructor + # comment above -- `γ`/`β` being `Union{_, Nothing}` leaves `T` + # unbound in the auto-generated default constructor. Taking `T` from + # the `{T}` type application keeps it bound even when both are + # `nothing` (affine=false). + function InstanceNorm{T}( + γ::Union{Vector{T}, Nothing}, + β::Union{Vector{T}, Nothing}, + eps::Float32, + affine::Bool, + num_features::Int, + ) where T + new{T}(γ, β, eps, affine, num_features) + end end function InstanceNorm( @@ -228,6 +259,22 @@ mutable struct GroupNorm{T} <: AbstractLayer num_channels::Int eps::Float32 affine::Bool + + # Explicit inner constructor (Aqua G07): see LayerNorm's constructor + # comment above -- `γ`/`β` being `Union{_, Nothing}` leaves `T` + # unbound in the auto-generated default constructor. Taking `T` from + # the `{T}` type application keeps it bound even when both are + # `nothing` (affine=false). + function GroupNorm{T}( + γ::Union{Vector{T}, Nothing}, + β::Union{Vector{T}, Nothing}, + num_groups::Int, + num_channels::Int, + eps::Float32, + affine::Bool, + ) where T + new{T}(γ, β, num_groups, num_channels, eps, affine) + end end function GroupNorm( diff --git a/test/aqua.jl b/test/aqua.jl new file mode 100644 index 0000000..3f30754 --- /dev/null +++ b/test/aqua.jl @@ -0,0 +1,38 @@ +# SPDX-License-Identifier: MPL-2.0 +# Aqua.jl quality-gate testset (G07). +# +# Aqua checks: method ambiguities, unbound type parameters, undefined +# exports, stale/missing deps, [compat] bounds (including `julia`), type +# piracy, and persistent tasks. Axiom passes every one of these with NO +# overrides required -- see the two fixes below that made this possible: +# +# 1. Unbound type parameters (real bug, fixed at the source): `LayerNorm`, +# `InstanceNorm`, and `GroupNorm` each had a `T` (and `S`) type +# parameter that only appeared in `Union{_, Nothing}`-typed fields +# (`γ`/`β` are `nothing` when `affine=false`). Julia's default +# auto-generated positional constructor for those structs therefore +# left `T`/`S` unbound from the perspective of `Test.detect_unbound_args` +# (a `nothing` argument pins no concrete type). Fixed in +# `src/layers/normalization.jl` by adding an explicit inner constructor +# per struct that takes `T`/`S` from the `{T}`/`{T, S}` type +# application itself, so they stay bound even when both fields are +# `nothing`. `BatchNorm` was never affected: its `running_mean`/ +# `running_var` fields are non-nullable `Vector{T}`, so `T` was always +# pinned by those. +# 2. Stale dependency (`JSON3`, removed from `Project.toml`): its only +# consumer, `src/integrations/huggingface.jl`, is not `include()`d from +# `src/Axiom.jl` (dead/orphaned code, unreachable from the module), so +# the dependency was genuinely unused by anything Aqua can see. +# +# `Aqua.test_piracies` also passes without a `treat_as_own` override: +# Axiom extends `size`/`sum`/etc. only via methods that dispatch on +# Axiom's OWN `Tensor`/`DynamicTensor` types, which Aqua's own heuristic +# already recognises as ordinary (non-piratic) dispatch. + +using Test +using Aqua +using Axiom + +@testset "Aqua quality gate" begin + Aqua.test_all(Axiom) +end diff --git a/test/jet.jl b/test/jet.jl new file mode 100644 index 0000000..ce93325 --- /dev/null +++ b/test/jet.jl @@ -0,0 +1,43 @@ +# SPDX-License-Identifier: MPL-2.0 +# JET.jl static-analysis testset (G07). +# +# `JET.report_package`/`test_package` walk the whole dependency graph by +# default: an unscoped `report_package(Axiom)` currently reports 66 +# "possible errors", essentially all of them rooted in transitive deps +# Axiom does not control (JSON/StructUtils conversion fallbacks, +# LinearAlgebra QR internals, Zygote/ZygoteRules adjoint kwcall plumbing, +# Base.Broadcast internals, ...). We scope the report to Axiom's own code +# via JET's native `target_modules` config (see `JET.configured_reports` / +# `JET.LastFrameModule` in JETBase.jl): this is a documented, JET-native +# scoping mechanism, not a hand-rolled file-path filter. +# +# Verified empirically (not just by reading JET's source) that this +# scoping is not blanket-hiding genuine Axiom-side bugs: with +# `target_modules = (Axiom,)`, `report_package(Axiom)` returns exactly +# ZERO reports, including the two candidates that looked at first glance +# like they might be Axiom-origin: +# - `transform_pipeline`/`is_pipeline_expr` in src/dsl/axiom_macro.jl: +# JET's unscoped run flags a `Symbol has no field args` error whose +# OWN innermost frame is `Base.getproperty`/`Base.getfield`, reached +# because `is_pipeline_expr(expr::Union{Expr,Symbol})` can't prove to +# JET that the `expr isa Expr &&` short-circuit in the caller already +# excludes `Symbol` before `.args` is accessed -- unreachable at +# runtime, and its root cause is a Base call, not an Axiom one. +# - `prove_property` in src/dsl/prove.jl calling `Axiom.smt_proof(...)`: +# `smt_proof` is an extension stub (`function smt_proof end`) only +# implemented by `AxiomSMTExt` when the `SMTLib` weakdep is loaded; +# `report_package` analyzes bare `Axiom` without loading extensions, +# so it structurally can't see that method. The call site itself is +# guarded by `Base.get_extension(Axiom, :AxiomSMTExt) !== nothing`, +# so it is never reached unless the method exists. +# Any *new* Axiom-origin JET finding will still fail this test -- this +# comment documents why the count is 0 today, not an allowlist of +# suppressed findings. + +using Test +using JET +using Axiom + +@testset "JET static analysis gate" begin + JET.test_package(Axiom; target_modules = (Axiom,), toplevel_logger = nothing) +end diff --git a/test/runtests.jl b/test/runtests.jl index ac9dba8..87ecb00 100644 --- a/test/runtests.jl +++ b/test/runtests.jl @@ -761,6 +761,10 @@ with open(args.output, "w", encoding="utf-8") as f: include("e2e_test.jl") include("property_test.jl") + # Quality gates (G07): static/dynamic analysis of Axiom's own code. + include("aqua.jl") + include("jet.jl") + end println("\nAll tests passed!")