Integrate THOTH STEM workspace and Platinum-scoped proof kernels - #19
Merged
Conversation
Extends the JACKAL runtime and its Codex plugin to Linux aarch64 alongside the existing macOS arm64 support, non-destructively — the macOS release identity (MANIFEST.sha256, proof identities, compat floor) stays byte-clean and every macOS code path falls through unchanged. Re-pin (formal lanes on Linux): - release/tools/repin_linux.py derives a per-host release/MANIFEST.<host>.sha256 that rebinds only the compiled-binary rows, the proof-identity rows, and the compiler pin from live bytes; all other rows are copied verbatim from the macOS manifest. - Host-suffixed Linux proof identities, a Linux compat floor, and a Linux lean-admission-audit are generated from the locally built Lean checkers. - release_validate.py, gaussian_release.py, int_cert_release.py, formal_receipt.py and lean_admission_audit.py prefer host-suffixed evidence and fall back to the pinned macOS records. - The ten jackal-*-release wrappers select the per-host manifest and identity. All ten formal lanes emit status=formal-bounded with re-verified receipts. Provisioner (install the Linux runtime): - release/build_package_linux.sh builds jackal-v1.7.3-linux-aarch64.tar.gz, passing full identity + semantic validation (plugin identity_match, formal smokes, receipt replays). The atomic no-replace publish uses renameat2 (RENAME_NOREPLACE) on Linux. - provision_runtime.py: SUPPORTED_HOSTS + RELEASE_PINS gain linux-aarch64; resolve_host/release_pin/rename_exclusive_for_host select per host; provision() binds the host release pin; byte caps fit the largest runtime; a POSIX launch_mcp.sh joins launch_mcp.zsh with a byte-identical probe. - mcp/server.py locator + package-metadata checks use effective_release_pins. - A ubuntu-24.04-arm CI job runs the plugin gates on Linux. Note: the domain-pack protocol-v1 verifier host-gates to macOS in pinned shared source, so its staged QA is skipped for a local build (JACKAL_LOCAL_BUILD=1); the ~4 domain-pack/program tools fail closed on Linux, and the archival v1.7.0 lane stays macOS bytes. 37/41 tools work on Linux, including every formal-bounded lane. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The domain-pack protocol-v1 verifier (tools/domain_pack_verify.py) hard-gated
to Darwin/arm64, so the four domain-pack/decision tools (jackal_decision_rank,
jackal_decision_rank_v2, jackal_test_exists, jackal_claim_cites_test) refused
on Linux with "requires Apple Silicon macOS". This admits Linux/aarch64 to
that verifier and propagates the resulting digest change consistently.
- domain_pack_verify.py: validate_host() gains a SUPPORTED_HOSTS set
({Darwin/arm64, Linux/aarch64}); the emitted report's host field now
reflects the real host instead of a hardcoded "darwin-arm64". macOS behavior
is unchanged.
- domain_packs/registry_v1.json: pack_verifier_sha256 rebound to the edited
verifier, registry_digest_sha256 recomputed over the canonical body.
- The domain_pack_verifier + domain_pack_registry rows are updated in BOTH
release/MANIFEST.sha256 and release/MANIFEST.linux-aarch64.sha256 (the
verifier and registry are shared, platform-neutral source), and
capability_inventory_v1.json + the plugin identity manifest are regenerated.
- build_package_linux.sh: the JACKAL_LOCAL_BUILD domain-pack QA skip is
removed; the staged domain-pack verification now runs unconditionally and
passes on Linux.
- provision_runtime.py: linux-aarch64 release pin updated for the rebuilt
package (sha 15803b7e, 177404787 bytes).
Verified through the provisioner-installed runtime: all 41 tools are
host-clean — exact/checked/estimated/bounded/formal-bounded lanes compute,
decision_rank and test_exists return exact/structural-exact, and the
claim/verify/program tools reach real input validation with no host refusal.
The codex_plugin suite, drift gate, capability inventory, plugin identity, and
repin_linux --check all pass; the program-evidence verifier's 12/15 pass on
Linux matches pristine (the 3 failures are pre-existing shallow-clone
fixtures, not from this change).
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The Linux package previously shipped one macOS binary — jackal_cert_check_v170, the archival v1.7.0 range-replay checker, pulled from the Apple release archive. It could not execute on Linux, so the archival replay lane was a dead file. This rebuilds it native and re-pins the archival chain, so the Omarchy (Linux aarch64) edition carries zero macOS bytes: all five binaries are native ELF. - The v1.7.0 range checker is rebuilt from the v1.7.0 tag's Lean source against the same Lean 4.32 / Mathlib v4.32 toolchain (native ELF, sha d515cdc2). It ACCEPTs a valid enclosure and REJECTs a tampered one, verified in the installed runtime. - A native archival v1 proof identity (schema jackal-range-proof-identity-v1, binding the native checker bytes) is generated at the v1.7.0 tag and shipped as release/evidence/range_proof_identity.linux-aarch64.json. - Host-aware archival pins: formal_receipt.py resolves both the archival range checker sha and the archival identity file sha per host (native on Linux via release/evidence/archival_range_checker.linux-aarch64, macOS bytes as the fallback); the Linux compat floor and manifest carry the native shas; repin_linux.py rebinds the archival-range-checker and archival-range-proof rows. - build_package_linux.sh no longer downloads the Apple v1.7.0 archive: it copies the native archival checker and the platform-neutral archival coverage inventory from JACKAL_ARCHIVAL_DIR, verifying both against their pins. Verified: the built package and installed runtime contain zero Mach-O binaries; full identity + semantic validation passes (including the archival identity / checker consistency checks); plugin identity_match=true; all 41 tools and every formal lane work. macOS release identity (MANIFEST.sha256, the macOS archival identity, macOS compat floor) is untouched — the host-aware fallbacks keep the macOS edition on its original bytes. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Adds ("Linux","x86_64") to SUPPORTED_HOSTS with a null RELEASE_PIN so the host
is recognized and provisioning refuses "no published release asset for host
linux-x86_64" until a native x86_64 package is built and OBSERVED on x86_64
hardware (planned bare-metal iMac Pro). No x86_64 function is claimed. The
aarch64/x86_64 arch-substitution refusal follows from the per-host pin/directory
binding. Plugin identity regenerated for the changed provisioner.
Part of the Omarchy JACKAL native-product mission: architecture gate for a
versioned Linux product with architecture-specific native artifacts, not an
aarch64-only fork.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…ded sign-off) Under the architect's 2026-08-23 bounded sign-off: admit a native Linux aarch64 Z3 4.15.4 as a separate architecture-qualified program-evidence trust anchor. The guest's system Z3 4.16.0 is NOT admitted. - Z3 4.15.4 pinned from official source (archive dae52625, tree 0e4123f4, version verified), independently double-built byte-identical (b6fcd93b) in two isolated directories under a recorded deterministic recipe; native aarch64 ELF, no dependency on the guest 4.16.0. - tools/anubis_program_verify.py: host-aware _approved_z3_for_host() selects the Darwin anchor (preserved EXACTLY) or the Linux aarch64 anchor (b6fcd93b), enforcing exact digest + semver 4.15.4 + no-symlink + owner/mode + single-snapshot identity. The inventory-safe-v1 policy body is byte-frozen (POLICY_SHA256 1b94350a unchanged); no verification semantics, residual, or refusal is loosened. - Negative controls verified: Linux 4.16.0 refused (z3-identity-mismatch), symlink/one-byte-tamper/world-writable refused, pristine restores (A->B->A). - The approved Z3 is shipped in the package (jackal_z3_v4154) and pinned in the Linux manifest (approved-z3-linux-aarch64); build_package_linux.sh copies it from JACKAL_Z3_DIR; repin_linux appends the anchor row. - jackal_anubis_verify_program + verify_program_receipt now PASS from the installed package with all six residuals open and the artifact never executed. The shared verifier hash change updates the anubis_program_verifier row in both manifests and the capability inventory (authorized; macOS proof/checker/floor and the inventory-safe-v1 policy body remain byte-identical to baseline). jackal_anubis_check_program remains BLOCKED on the SEPARATE approved-check-compiler anchor, which this Z3 sign-off does not authorize. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…4 stack The Omarchy edition's binaries (anubis, jackal-native, Lean checkers, archival checker, Z3 4.15.4, package) are all built from source and not committed. This captures the complete reproduction recipe, known-good digests, and the pending check-compiler trust-surface sign-off in one place so the stack is durable. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Resolve the check-compiler sign-off for jackal_anubis_check_program on
Linux/aarch64 via the architect's clean-source route, without reusing the
historical macOS anchor (0d6a8f89) and without weakening inventory-safe-v1.
- tools/anubis_program_verify.py: point the architecture-qualified check
compiler anchor at the reproducible clean-source build
7cdafb30... (supersedes the pre-emitter d8c7d38b...). macOS anchor,
both Z3 anchors, host-aware selection, and the frozen inventory-safe-v1
policy body (1b94350a...) are untouched.
- release/evidence/approved_check_compiler.linux-aarch64: pin marker.
- release/tools/repin_linux.py: append the approved-check-compiler-<host> row.
- release/build_package_linux.sh: ship the digest-checked check compiler and
emit its manifest row.
- release/MANIFEST{,.linux-aarch64}.sha256: rebind the verifier row to
cafbd257... and the linux check-compiler row to 7cdafb30...
- release/capability_inventory_v1.json: regenerate (verifier pin cafbd257...).
- plugins/jackel/scripts/provision_runtime.py + PLUGIN_IDENTITY.sha256:
repin the self-consistent Linux package (0b239bc7...).
Verified end-to-end through the unmodified verifier and the real hermes
plugin on a clean-install runtime: verified-program-evidence, 4 obligations
independently RUP-replayed + approved-Z3-unsat; all negative controls fail
closed; 41/41 tools present; drift gate + plugin identity + 12/12 adversarial
A->B->A pass.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01KBajXqAr1zojERZGTTxY2n
…x/aarch64
The MCP server validated the installed runtime tree against the module-level
SHA256SUMS_SHA256 constant, which is the macOS release value. On Linux/aarch64
the runtime's SHA256SUMS is the host tree, so both startup checks refused
("pinned runtime validation refused", then "private runtime snapshot creation
refused") and the server never started.
Resolve it the same way the metadata check already resolves the package sha:
expose sha256sums_sha256 from effective_release_pins() (host-aware) and use it
in both server startup calls (validate_runtime + create_runtime_snapshot)
instead of the macOS module constant. macOS behaviour is unchanged — its host
pin equals the module constant.
Verified: `claude mcp list` -> jackal ✔ Connected; initialize + tools/list over
a persistent pipe returns all 41 tools; tools/call round-trips.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01KBajXqAr1zojERZGTTxY2n
…k compiler Record the architect's sign-off designating the clean-source Linux/aarch64 Anubis check compiler (7cdafb30...) as the approved check compiler for jackal_anubis_check_program on Linux/aarch64. Unlike the historical macOS candidate (0d6a8f89, "caller-pinned candidate; architect sign-off required", source irrecoverable), this is a committed clean-source, reproducibly double-built (byte-identical), architecture-qualified identity verified end-to-end through the unmodified frozen verifier and the real plugin. Scope is Linux/aarch64 only: the macOS candidate is not reused and the inventory-safe-v1 policy body stays byte-frozen (1b94350a). macOS and both Z3 anchors are untouched. Standalone authority evidence (mirrors the macOS dogfood record; not manifest-pinned). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KBajXqAr1zojERZGTTxY2n
The architect sign-off for jackal_anubis_check_program on Linux/aarch64 was granted+recorded 2026-08-24 (SIGNOFF_linux_aarch64.json, verifier anchor 7cdafb30, VERDICT.txt/STATUS.json=ARCHITECT_SIGNED_OFF) and independently re-verified today (verified-program-evidence, 4 proofs, receipt 81d6477e). The 'Pending trust-surface sign-offs' section was stale; mark it RESOLVED. Product verdict stays _V111_PENDING (gated on the future sealed 49-tool package, not this round). No verifier acceptance broadened; anchors untouched. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… changes Adversarial pre-push review (multi-agent) + emitter stress-test across the real program space surfaced test/inventory drift from this cycle's host-aware and re-pin changes. No production behaviour changes here; the signed-off check compiler (7cdafb30) is untouched. - release/capability_inventory_v1.json: regenerate to pick up the host-aware mcp/server.py sha (the drift gate + `capability_inventory --check` now pass). - tests/codex_plugin/test_mcp_adapter.py: the two fake provisioners now expose sha256sums_sha256 from effective_release_pins(), matching the real host-aware contract the server startup path now uses (validate_runtime + create_runtime_snapshot). Fixes 4 errors + 1 failure. - tests/codex_plugin/test_runtime_provisioner.py: update the host-guard tests to the actually-supported set (Darwin/arm64, Linux/aarch64, and the Linux/x86_64 declared gate with a None pin), still refusing genuinely foreign hosts. The old "darwin-only" assertions predated the Linux host support already on this branch. - tests/anubis_program_verifier_test.py: the dangling-out_root check test now patches the host-aware anchor helper (_approved_check_compiler_sha256_for_host) so it passes on Linux/aarch64, where the macOS constant is not consulted. Verified: full tests/codex_plugin suite (235) green on Linux; capability inventory --check + drift gate green; emitter stress-tested across 10 real programs (0 canonical-id mismatches at up to 46 functions; every refusal a legitimate fail-safe contract/budget boundary); emitter analysis output is byte-deterministic (only the native artifact sha varies, a pre-existing codegen property, faithfully recorded). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KBajXqAr1zojERZGTTxY2n
… compiler 6c3ae920
Owner (khephri.labs@proton.me) authorized adopting the host-honesty fix into the
signed check compiler. Re-pins the SOURCE-OF-TRUTH trust surface from 7cdafb30 to
6c3ae920 (= anubis-lang 0ad40aaf: 6aa6fd92 v3-emitter + host-honest `anubis doctor`,
main.rs only), double-built byte-identical, proven a drop-in (program-evidence for
verified_loop.anb is byte-identical to 7cdafb30 after scrubbing volatile fields).
Re-pinned (host-aware; Darwin 0d6a8f89 + Z3 anchors + inventory-safe-v1 body 1b94350a
untouched):
- tools/anubis_program_verify.py APPROVED_CHECK_COMPILER_LINUX_AARCH64_SHA256
- release/evidence/approved_check_compiler.linux-aarch64 (marker)
- release/MANIFEST.linux-aarch64.sha256 (approved-check-compiler row via repin_linux)
- release/build_package_linux.sh APPROVED_CC_SHA256 (next package build)
- release/evidence/anubis_program_dogfood_linux_aarch64_v1.json (designation; the
v1.7.3 tarball's shipped_check_compiler stays 7cdafb30 — honest as-shipped)
- OMARCHY_BUILD.md
Incidental: repin_linux also rebound MANIFEST `compiler_pin` c6affa8c -> 2704f083, the
now-doctor-honest language anubis at ~/.local/bin/anubis (jackal-native re-builds with it
at V111). Consistent with adopting the doctor-honest toolchain.
Verification (this box): direct frozen verifier -> verified-program-evidence, 4 proofs
(receipt 46c7b357) for 6c3ae920; REFUSES 7cdafb30 (compiler-not-approved). Gate-green:
235/235 codex_plugin tests (1 skip), plugin_identity=verified, CAPABILITY_DRIFT_PASS,
repin_linux --check MATCH.
Deployment: source-ahead-of-deployment by design. The provisioned v1.7.3 runtime + MCP
surface + hermes bundle still verify the deployed 7cdafb30 and re-provision to 6c3ae920
at the V111 repackage (which regenerates the hermes bundle identity). Not pushed.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
# Conflicts: # plugins/jackel/.codex-plugin/plugin.json # plugins/jackel/PLUGIN_IDENTITY.sha256 # plugins/jackel/skills/jackel/SKILL.md # tools/capability_drift_gate.py
|
Important
This repository does not receive automatic reviews because it has fewer than 10 stars. ⚙️ Run configurationConfiguration used: defaults Review profile: CHILL Plan: Pro Plus Run ID: Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
added 5 commits
August 29, 2026 01:30
Owner
Author
Final current-head evidence auditExact head audited: Hosted evidence
Local current-head evidence
Companion Omarchy release
Assurance boundary“Platinum” is intentionally component-scoped to the two declared SPARK kernels and their allocated finite-domain requirements. This does not establish universal correctness of the complete JACKAL/THOTH product, Python/QML/JavaScript/shell code, compilers, source-to-native refinement, operating system, hardware, sensors, or physical models. HELLGATE |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Outcome
This adds THOTH as an integrated JACKAL subsystem, expands the Codex wrapper with linked STEM/CAS/graphing/measurement/aerospace surfaces, and introduces two narrowly scoped SPARK Platinum components. It preserves the sealed v1.7.3 runtime inventory and all existing JACKAL status, refusal, ceiling, and non-claim semantics.
Main changes
Fresh local verification
Claim boundary
The Platinum claim is component-scoped only to the declared SPARK kernels and their allocated finite-domain requirements. It does not establish universal correctness of Python, QML, JavaScript, shell, Linux, compiler/runtime refinement, hardware, sensor authenticity, physical aerospace models, or the whole JACKAL product. HELLGATE E0 remains
bounded, notformal-bounded; the certificate does not prove moments, perturbation derivatives, BdG stability, or all challenge parts.The current Hermes source-tree selftest deliberately reports
SKIPPED-manifest-pendingfor unreleased development bytes. Success-path tests assemble a self-consistent package-local manifest, while the published release manifest remains immutable. macOS-only spacecraft publication/package gates are left to their owning macOS workflow and are not weakened to pass on Linux.