Repository navigation
Axiom flagship hardening — P1 soundness holes (WIP) - #46
Merged
Merged
Conversation
… false cert signature label) Holes-first pass from the Axiom flagship audit. - checker.jl: has_safe_operations() returned bare `true`, so every NoNaN request on the static path was vacuously reported :proven. A sound static NoNaN proof needs a finite-input guarantee that cannot be established statically, so NoNaN now routes to empirical checking and has_safe_operations makes no false claim. (G02) - certificates.jl: the JSON output hardcoded algorithm="SHA256-HMAC" over an unkeyed SHA-256 digest -- forgeable, and falsely presented as authenticated. Relabelled honestly (algorithm SHA-256, kind content-digest, authenticated=false, explanatory note); docstrings corrected. Authenticating hybrid Ed448+Dilithium5 signatures tracked for follow-up. (G01, relabel) - Added test/verification/soundness_tests.jl to the main suite so neither hole can silently reopen. Verified: full suite 651/651 pass; certificate_integrity CI file 6/6 pass. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01UPFC9YQ7g9gc3VnRox42Q1
hyperpolymath
marked this pull request as ready for review
July 1, 2026 02:57
hyperpolymath
added a commit
that referenced
this pull request
Jul 1, 2026
… diary (#47) ## Summary Follow-up to the merged #46 (which closed the first two P1 soundness holes). This branch was **restarted from the post-merge `main`** — it does not re-stack the squashed pilot. It closes three "proof honesty" gaps and captures the initiative's decision record in-repo. ### G03 — proof-assistant import verification was fake (high) `proof_export.jl` judged a Lean/Coq/Isabelle proof "complete" merely for **lacking** `sorry`/`Admitted`/`oops` — so an empty file, or `theorem foo : True := trivial`, passed as verified. Now a proof must contain **at least one substantive** (non-vacuous, non-boilerplate) theorem/lemma statement; empty/trivial proofs report `:incomplete`. *(Fixing this exposed two pre-existing test fixtures that were themselves vacuous `:= trivial` proofs — updated to substantive statements.)* ### G04 — `@prove` overclaim (high) `dsl/prove.jl` (+ `docs/wiki/Verification.md`) documented `@prove` as "symbolic execution" / "formal verification", but it is a **substring match on the printed AST**. Relabelled honestly (experimental heuristic; **not** symbolic execution or a theorem prover; real proving is the SMT/Idris2 path). No behaviour change — every remaining mention is now an explicit negation. ### G05 — Idris2 ABI is a disconnected demo (high; honest relabel) `src/Abi/*.idr` declare a generic surface that does **not** match the ~36 real `axiom_*` zig exports used by `src/backends/zig_ffi.jl`. Labelled as an **illustrative scaffold** (not a proof of the production FFI boundary) in each file + `ABI-FFI-README.md`, pointed at the real boundary (`zig/` + `zig_ffi.jl`), and flagged the **orphan `ffi/zig/` tree (zero `axiom_*` exports)** as a KNOWN ISSUE. Full ABI↔zig connection is tracked follow-up (Idris2 is CI-only here). ### Design record captured online `docs/design-diary/PEPYS-DESIGN-DIARY.adoc` (the running "Samuel Pepys" decision log) and `docs/design-diary/ULTRAPLAN.adoc` (executive summary, 41-item gap register, phased plan, decision forks, estate wiring, risks). ## Verification (independent re-run, not self-graded) - `Pkg.test()` on the rebased base → **670 / 670 pass** (651 + 19 new G03 assertions). - Grep confirms no affirmative "symbolic execution" / "formal verification" claim remains attached to `@prove`. ## Residuals (tracked) Real hybrid **Ed448+Dilithium5** certificate signing (G01 auth layer, reusing `opsm`'s `pqcrypto` crates), full Idris2-ABI↔zig connection (G05), plus the broader flagship work (Aqua/JET/Documenter, RegistryCI, panic-attack gate, RSR completeness, doc reconciliation). 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01UPFC9YQ7g9gc3VnRox42Q1 --- _Generated by [Claude Code](https://claude.ai/code/session_01UPFC9YQ7g9gc3VnRox42Q1)_ --------- Co-authored-by: Claude <noreply@anthropic.com>
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
2 participants
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.
Summary
First hardening pass toward making Axiom.jl the estate Julia flagship and measuring-stick. Opened as a draft to accumulate the holes-first fixes from a full ground-truthed audit (soundness → doc reconciliation → estate tooling). This commit closes two confirmed P1 soundness holes.
G02 — vacuous
NoNaNstatic "proof" (critical)checker.jl::has_safe_operations()returned a baretrue, so everyNoNaNrequest on the static path was reported:provenregardless of the model's operations. A sound staticNoNaNproof also requires a finite-input guarantee that cannot be established statically, soNoNaNnow routes to empirical checking andhas_safe_operationsmakes no false claim.G01 — falsely-labelled certificate "signature" (critical; relabel)
certificates.jlemittedalgorithm: "SHA256-HMAC"over an unkeyedSHA-256digest — forgeable and misleadingly presented as authenticated. Relabelled honestly:algorithm: SHA-256,kind: content-digest,authenticated: false, plus an explanatory note; docstrings corrected. Authenticating hybrid Ed448+Dilithium5 signatures (matching the estate Trustfile and the testedopsmPQ crypto) are the tracked follow-up.Regression guard
Added
test/verification/soundness_tests.jlto the main suite so neither hole can silently reopen.Verification (ran the tools; no self-grading)
Pkg.test()— 651 / 651 pass (642 prior + 9 new soundness assertions)test/ci/certificate_integrity.jl— 6 / 6 passScope / tracked follow-ups
Remaining Axiom P1: real hybrid signing (G01 auth layer), proof-import theorem-presence check (G03),
@provehonest relabel (G04), Idris2 ABI ↔ zig-export reconciliation (G05). Broader flagship work: doc reconciliation, Aqua/JET/Documenter, RegistryCI, panic-attack static-analysis gate, RSR completeness. Registry and julianiser critical fixes land on their own branches.🤖 Generated with Claude Code
https://claude.ai/code/session_01UPFC9YQ7g9gc3VnRox42Q1
Generated by Claude Code