Integrate THOTH STEM workspace and Platinum-scoped proof kernels

.github/workflows/gaussian-proof-gate.yml

@@ -9,6 +9,34 @@ permissions:
   contents: read
 
 jobs:
+  spark-platinum-components:
+    name: SPARK Platinum functional kernels
+    runs-on: ubuntu-24.04
+    timeout-minutes: 30
+    steps:
+      - name: Check out exact revision
+        uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4
+
+      - name: Install GNAT, GPRbuild, and GNATprove
+        uses: alire-project/alr-install@b99b8c21417c79c307905439def2718bc393b94a # v2.0.1
+        with:
+          crates: gnat_native=16.1.0 gprbuild=26.0.1 gnatprove=16.1.0
+
+      - name: Enforce bidirectional requirements and whole-surface closure
+        run: |
+          python3 -B tools/check_assurance_traceability.py
+          python3 -B -m unittest tests.assurance_traceability_test -v
+
+      - name: Prove the total interval decision kernel
+        run: |
+          proofs/spark/hellgate_interval/prove.sh
+          python3 -B -m unittest tests.codex_plugin.test_spark_interval -v
+
+      - name: Prove and exhaustively refine the claim policy kernel
+        run: |
+          proofs/spark/claim_policy/prove.sh
+          python3 -B -m unittest tests.claim_policy_conformance_test -v
+
   lean-proof-and-axioms:
     name: Gaussian/range source closures and axiom audits
     runs-on: ubuntu-24.04

.github/workflows/jackal-codex-plugin.yml

@@ -10,8 +10,78 @@ permissions:
 
 env:
   PYTHONDONTWRITEBYTECODE: "1"
+  MPMATH_WHEEL_URL: https://files.pythonhosted.org/packages/43/e3/7d92a15f894aa0c9c4b49b8ee9ac9850d6e63b03c9c32c0367a13ae62209/mpmath-1.3.0-py3-none-any.whl
+  MPMATH_WHEEL_SHA256: a0b2b9fe80bbcd81a6647ff13108738cfb482d481d826cc0e02f5b35e5c88d2c
+  MPMATH_WHEEL_SIZE: "536198"
 
 jobs:
+  linux-aarch64-plugin:
+    name: Linux aarch64 plugin gates
+    runs-on: ubuntu-24.04-arm
+    timeout-minutes: 20
+    steps:
+      - name: Check out exact revision
+        uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4
+        with:
+          fetch-depth: 0
+          persist-credentials: false
+
+      - name: Require the supported host and fixed Python prerequisite
+        run: |
+          test "$(uname -s)" = Linux
+          test "$(uname -m)" = aarch64
+          test -x /usr/bin/python3
+          /usr/bin/python3 -c 'import sys; assert sys.version_info >= (3, 10)'
+
+      - name: Require the host atomic no-replace rename primitive
+        run: |
+          /usr/bin/python3 -c '
+          import ctypes
+          libc = ctypes.CDLL(None, use_errno=True)
+          assert callable(getattr(libc, "renameat2", None)), "glibc renameat2 is required"
+          '
+
+      - name: Verify canonical capability and documentation contracts
+        run: |
+          /usr/bin/python3 -B tools/capability_drift_gate.py
+          /usr/bin/python3 -B -m unittest \
+            tests.capability_inventory_test \
+            tests.capability_drift_gate_test -v
+
+      - name: Fetch exact untrusted HELLGATE oracle dependency
+        run: |
+          wheel="$RUNNER_TEMP/mpmath-1.3.0-py3-none-any.whl"
+          curl --proto '=https' --tlsv1.2 --fail --location --silent --show-error \
+            --max-filesize "$MPMATH_WHEEL_SIZE" --output "$wheel" "$MPMATH_WHEEL_URL"
+          test "$(wc -c < "$wheel" | tr -d '[:space:]')" = "$MPMATH_WHEEL_SIZE"
+          /usr/bin/python3 - "$wheel" "$MPMATH_WHEEL_SHA256" <<'PY'
+          import hashlib
+          import pathlib
+          import sys
+          actual = hashlib.sha256(pathlib.Path(sys.argv[1]).read_bytes()).hexdigest()
+          if actual != sys.argv[2]:
+              raise SystemExit("mpmath wheel digest mismatch")
+          PY
+
+      - name: Run complete Codex plugin unit suite
+        env:
+          PYTHONPATH: ${{ runner.temp }}/mpmath-1.3.0-py3-none-any.whl
+        run: /usr/bin/python3 -B -m unittest discover -s tests/codex_plugin -v
+
+      - name: Verify exact plugin identity
+        run: /usr/bin/python3 -B plugins/jackel/scripts/verify_plugin.py
+
+      - name: Portable launcher starts and refuses for the documented reason
+        run: |
+          cd plugins/jackel
+          set +e
+          output=$(/bin/sh scripts/launch_mcp.sh provision --check 2>&1)
+          status=$?
+          set -e
+          printf '%s\n' "$output"
+          test "$status" -eq 1
+          printf '%s\n' "$output" | grep -q "pinned runtime is not installed"
+
   macos-arm64-plugin:
     name: macOS arm64 plugin gates
     runs-on: macos-14
@@ -37,7 +107,24 @@ jobs:
             tests.capability_inventory_test \
             tests.capability_drift_gate_test -v
 
+      - name: Fetch exact untrusted HELLGATE oracle dependency
+        run: |
+          wheel="$RUNNER_TEMP/mpmath-1.3.0-py3-none-any.whl"
+          curl --proto '=https' --tlsv1.2 --fail --location --silent --show-error \
+            --max-filesize "$MPMATH_WHEEL_SIZE" --output "$wheel" "$MPMATH_WHEEL_URL"
+          test "$(wc -c < "$wheel" | tr -d '[:space:]')" = "$MPMATH_WHEEL_SIZE"
+          /opt/homebrew/bin/python3 - "$wheel" "$MPMATH_WHEEL_SHA256" <<'PY'
+          import hashlib
+          import pathlib
+          import sys
+          actual = hashlib.sha256(pathlib.Path(sys.argv[1]).read_bytes()).hexdigest()
+          if actual != sys.argv[2]:
+              raise SystemExit("mpmath wheel digest mismatch")
+          PY
+
       - name: Run complete Codex plugin unit suite
+        env:
+          PYTHONPATH: ${{ runner.temp }}/mpmath-1.3.0-py3-none-any.whl
         run: /opt/homebrew/bin/python3 -B -m unittest discover -s tests/codex_plugin -v
 
       - name: Verify exact plugin identity

OMARCHY_BUILD.md

@@ -0,0 +1,86 @@
+# Omarchy JACKAL — full native rebuild recipe (Linux aarch64)
+
+Every binary in the Omarchy edition is built from source on this host; none are
+committed (they are large and reproducible). This is the complete recipe to
+rebuild the whole stack from a fresh clone. Times are approximate on 8 cores.
+
+Prerequisites (system): `pacman -S z3 cmake` (z3 is *supporting only*, not the
+program-evidence anchor), `cargo`/`rustc` (stable), `elan` (Lean), `python3`.
+
+## 1. Anubis compiler  (~2 min)
+    cd ~/Projects/anubis-lang
+    cargo build --release -p anubis --no-default-features   # skip the Apple `prove` feature
+    install -m755 target/release/anubis ~/.local/bin/anubis
+
+## 2. Lean checkers (current)  (~40 min incl. Mathlib cache)
+    cd ~/Projects/jackal/proofs/lean
+    export PATH="$HOME/.elan/bin:$PATH"
+    lake exe cache get                                       # prebuilt Mathlib oleans — do NOT compile Mathlib
+    lake build jackal_cert_check jackal_gaussian_check jackal_int_cert_check jackal_parse_dump
+    # -> proofs/lean/.lake/build/bin/{jackal_cert_check,jackal_gaussian_check,jackal_int_cert_check}
+
+## 3. jackal-native (engine)  (~1 min; needs Z3 for its contract obligations)
+    cd ~/Projects/jackal
+    ANUBIS_BIN=~/.local/bin/anubis anubis build jackal_calc.anb --out /tmp/jn
+    cp /tmp/jn/anubis_out ./jackal-native
+
+## 4. Archival v1.7.0 checker (native)  (~40 min in a v1.7.0 worktree)
+    git worktree add /tmp/j170 v1.7.0
+    cd /tmp/j170/proofs/lean && export PATH="$HOME/.elan/bin:$PATH"
+    lake exe cache get && lake build jackal_cert_check
+    mkdir -p ~/jackal-omarchy-archival
+    cp .lake/build/bin/jackal_cert_check ~/jackal-omarchy-archival/jackal_cert_check_v170   # expect sha d515cdc2
+    git -C ~/Projects/jackal show v1.7.0:release/coverage/formal_coverage_inventory.json \
+        > ~/jackal-omarchy-archival/formal_coverage_inventory_v170.json                     # expect sha 18ff7b1d
+    git worktree remove /tmp/j170 --force
+
+## 5. Approved Z3 4.15.4 (double-build, byte-reproducible)  (~6 min)
+    # recipe: ~/omarchy-jackal-completion/z3build/build_recipe.sh (deterministic:
+    # SOURCE_DATE_EPOCH, -ffile-prefix-map, Release, static, --build-id=none)
+    URL=https://github.com/Z3Prover/z3/archive/refs/tags/z3-4.15.4.tar.gz  # archive sha dae52625
+    # build TWICE in isolated dirs; both MUST equal sha b6fcd93b (else STOP: not reproducible)
+    install -m700 <build>/z3 ~/.local/share/JACKAL/z3/linux-aarch64/jackal_z3_v4154
+
+## 6. Regenerate host evidence + manifest  (seconds)
+    export PATH="$HOME/.elan/bin:$PATH"
+    # host-suffixed proof identities, compat floor, lean audit, archival identity/marker,
+    # approved_z3 marker — see the *.linux-aarch64* files under release/evidence, release/compat.
+    JACKAL_ANUBIS_COMPILER_PATH=~/.local/bin/anubis python3 -B release/tools/repin_linux.py --write
+    python3 -B tools/capability_inventory.py --write
+    python3 -B tools/capability_drift_gate.py --write-plugin-identity
+
+## 7. Build the package  (~1 min)
+    JACKAL_ANUBIS_COMPILER_PATH=~/.local/bin/anubis JACKAL_DIST=~/jackal-dist-linux \
+    JACKAL_ARCHIVAL_DIR=~/jackal-omarchy-archival \
+    JACKAL_Z3_DIR=~/.local/share/JACKAL/z3/linux-aarch64 \
+      sh release/build_package_linux.sh --build
+    # then update the linux-aarch64 pin block in plugins/jackel/scripts/provision_runtime.py
+    # with the printed tarball sha256/size + SHA256SUMS sha + extracted size.
+
+## 8. Install
+    /bin/sh plugins/jackel/scripts/launch_mcp.sh provision --tarball \
+      ~/jackal-dist-linux/jackal-v1.7.3-linux-aarch64.tar.gz
+    omarchy-jackal doctor            # FUNCTIONAL from live probes
+
+## Known-good digests
+    anubis compiler   c6affa8c…   jackal-native       (rebuild)   cert_check     89e4e42d…
+    gaussian_check    1f21c6b2…   int_cert_check      f2e26f50…   v170 archival  d515cdc2…
+    approved Z3 4.15.4 b6fcd93b…  inventory-safe-v1 policy (frozen) 1b94350a…
+
+## Trust-surface sign-offs
+    - jackal_anubis_check_program: RESOLVED 2026-08-24 — architect (khephri.labs@proton.me)
+      designated the clean-source Linux/aarch64 anubis CHECK COMPILER sha256
+      6c3ae920… (double-built byte-identical, from anubis-lang commit 0ad40aaf =
+      6aa6fd92 + host-honest doctor; supersedes 7cdafb30 which lacked the doctor fix,
+      recipe §1). Scope: Linux/aarch64 only; macOS 0d6a8f89 not reused;
+      inventory-safe-v1 policy body byte-frozen (1b94350a). Verifier anchor is
+      host-aware (Darwin=0d6a8f89 preserved). Independently re-verified 2026-08-24
+      (verified-program-evidence, 4 proofs, receipt 46c7b357… (D2)). Records:
+      release/evidence/anubis_program_dogfood_linux_aarch64_v1.json and
+      ~/omarchy-jackal-completion/evidence/compiler/SIGNOFF_linux_aarch64.json;
+      finding ~/omarchy-jackal-completion/evidence/I_check_compiler_finding.json
+      = RESOLVED_ARCHITECT_SIGNED_OFF.
+    - Note: the overall product verdict stays _V111_PENDING — gated on the FUTURE
+      sealed 49-tool package (AWAITING_SEALED_V111_PACKAGE), NOT on this
+      check-compiler round, which is independently resolved. Linux x86_64
+      execution remains gate-declared/unobserved (separate item).

README.md

@@ -75,6 +75,11 @@ Qalculate!, Soulver and SpeedCrunch. JACKAL does **not** claim parity with a gen
 arbitrary-precision-float engine, or interactive graphing system. Its differentiated implemented
 surface is claim-aware and measurement-aware computation.
 
+For an honest path from research kernel to an externally reviewable engineering
+pilot, see [`docs/AEROSPACE_READINESS_GAP_LEDGER.md`](docs/AEROSPACE_READINESS_GAP_LEDGER.md).
+It separates implemented evidence from the qualification, refinement,
+independent-verification, safety, security, and operations work that remains.
+
 ## Why a calculator, in the age of frontier AI
 
 Language models are demonstrably unreliable at the arithmetic layer. OpenAI's own GSM8K

RESEARCH.md

@@ -5,7 +5,7 @@ This matrix uses official product pages as the baseline rather than review-site
 
 | Baseline | Observed strengths | JACKAL response |
 |---|---|---|
-| TI-Nspire CX II CAS | Linked algebraic/graphical/numeric views; CAS; matrices; regression, distributions, hypothesis tests; saved documents; programming and sensor data.[1] | Add matrices, numerical solvers, model cards, and reproducible fingerprints. A terminal Anubis program cannot honestly claim equivalent interactive graphing or CAS. |
+| TI-Nspire CX II CAS | Linked algebraic/graphical/numeric views; CAS; matrices; regression, distributions, hypothesis tests; saved documents; programming and sensor data.[1] | JACKAL now adds an identity-pinned evidence-aware CAS router and a professional PNG graph lane to the Codex surface, with exact rational x coordinates, estimated f64 y samples, explicit curve breaks on refusal, and reproducible wrapper fingerprints. It still does **not** claim TI-Nspire-equivalent linked interactive views, matrices, regression, sensor acquisition, or a general-purpose CAS. |
 | Qalculate! | "Arbitrary precision with both rational and floating point numbers"; exact/approximate forms; symbolic calculus; "propagation of uncertainty and interval arithmetic"; extensive units/constants; plotting.[2] | Add first-class measured quantities, propagated uncertainty, dimensional checks, numerical calculus, and explicit model limits. JACKAL now implements exact arbitrary-precision **integers** (`big-add/mul/pow/fact/ncr`) and exact **big rationals** (`rat`) in pure Anubis, plus outward-rounded **interval arithmetic** as a certified lane (`integrate-bound`/`range-bound`, refuse-on-doubt — with its f64/libm rounding model stated rather than implied); arbitrary-precision floats and general CAS remain outside the claimed surface. |
 | Soulver | Natural-language notepad; variables, line references, live updates, units, dates and scenario worksheets.[3] | Add human-readable calculation cards and Anubis-native audit narratives. JACKAL now has single-invocation worksheets with persistent variables (`worksheet "a = 5; b = a^2; a+b"`); a persistent reactive notebook with live updates is still not claimed. |
 | SpeedCrunch | Fast keyboard workflow; live results/history; custom functions/variables; "up to 50 digits of precision"; formula/constants library.[4] | Keep a scriptable CLI, add domain models and self-auditing output. JACKAL's `big-` integer lane is exact at any length within stated compute caps (verified against Python's arbitrary precision, e.g. 1000! at 2568 digits) — beyond 50 digits for integer work. Float work remains IEEE-754 f64: 50-digit float precision is still not claimed. |

assurance/README.md

@@ -0,0 +1,33 @@
+# JACKAL functional-proof baseline
+
+`requirements.json` is the machine-readable source for allocated functional
+requirements, component claims, and whole-surface closure status.
+
+The current universally quantified proofs apply to the total SPARK interval
+decision kernel and to the finite claim-assurance policy kernel over their
+complete declared input types. The claim-policy bridge also exhaustively checks
+the current producer and independent verifier registries against the proved
+SPARK truth table. The whole JACKAL product target is in progress. The closure
+matrix deliberately exposes every sealed
+runtime dependency family and every additive Codex tool group; it cannot become
+a whole-product claim until all discovered entries are `proved-universal` and
+all requirements are proved.
+
+Run:
+
+```sh
+python3 -B tools/check_assurance_traceability.py
+proofs/spark/hellgate_interval/prove.sh
+proofs/spark/claim_policy/prove.sh
+python3 -B -m unittest tests.claim_policy_conformance_test -v
+```
+
+The traceability gate rejects duplicate JSON keys, missing or one-way links,
+unknown public surface families, and premature whole-product claims. The proof
+gates reject missing tools, warnings, unproved or justified checks, skipped
+allocated units, and proof assumptions or annotations.
+
+SPARK Platinum is used only for SPARK components whose contracts fully cover
+their allocated functional requirements. Lean mathematical soundness, Anubis
+program evidence, independent checker replay, and empirical tests are recorded
+as different evidence forms rather than relabeled as SPARK Platinum.