Axiom flagship hardening — P1 soundness holes (WIP) (#46)

## 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 `NoNaN` static "proof" (critical)
`checker.jl::has_safe_operations()` returned a bare `true`, so every
`NoNaN` request on the static path was reported `:proven` regardless of
the model's operations. A sound static `NoNaN` proof also requires a
finite-input guarantee that cannot be established statically, so `NoNaN`
now routes to empirical checking and `has_safe_operations` makes no
false claim.

### G01 — falsely-labelled certificate "signature" (critical; relabel)
`certificates.jl` emitted `algorithm: "SHA256-HMAC"` over an **unkeyed**
`SHA-256` digest — 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 tested `opsm` PQ
crypto) are the tracked follow-up.

### Regression guard
Added `test/verification/soundness_tests.jl` to 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 pass**

## Scope / tracked follow-ups
Remaining Axiom P1: real hybrid signing (G01 auth layer), proof-import
theorem-presence check (G03), `@prove` honest 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.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>

Author: hyperpolymath

src/verification/certificates.jl

@@ -1,7 +1,11 @@
 # SPDX-License-Identifier: MPL-2.0
 # Axiom.jl Verification Certificates
 #
-# Cryptographically signed certificates proving model properties.
+# Tamper-evidence certificates for model properties. The certificate carries a
+# SHA-256 content digest over its public fields — this detects accidental or
+# naive tampering but is NOT a keyed/authenticating signature (anyone can
+# recompute the digest). Authenticating hybrid Ed448+Dilithium5 signatures (per
+# the estate Trustfile) are tracked in ROADMAP.adoc.
 
 using SHA
 
@@ -117,7 +121,12 @@ function compute_data_hash(data)
 end
 
 """
-Sign a certificate (simplified - production would use proper PKI).
+Attach a tamper-evidence digest to a certificate.
+
+NOTE: this computes an unkeyed SHA-256 content digest, NOT a keyed or asymmetric
+signature — it detects naive tampering but does not authenticate authorship (a
+forger can recompute the digest). Authenticating hybrid Ed448+Dilithium5
+signatures are planned; see ROADMAP.adoc.
 """
 function sign_certificate(cert::Certificate)
     # Concatenate certificate fields
@@ -209,7 +218,13 @@ function _save_certificate_json(cert::Certificate, path::String)
         ),
         "signature" => Dict(
             "value" => cert.signature,
-            "algorithm" => "SHA256-HMAC"
+            "algorithm" => "SHA-256",
+            "kind" => "content-digest",
+            "authenticated" => false,
+            "note" => "Unkeyed SHA-256 digest over public certificate fields: " *
+                      "detects naive tampering but does NOT authenticate authorship " *
+                      "(a forger can recompute it). Authenticating hybrid " *
+                      "Ed448+Dilithium5 signatures are planned; see ROADMAP.adoc."
         )
     )
 

src/verification/checker.jl

@@ -276,12 +276,12 @@ function try_static_verify(prop::Property, model)
         end
     end
 
-    if prop isa NoNaN
-        # Check for NaN-producing operations
-        if has_safe_operations(model)
-            return :proven
-        end
-    end
+    # NoNaN is intentionally NOT statically proven here. A sound static NoNaN
+    # proof needs BOTH structural operation-safety (see `has_safe_operations`)
+    # AND a finite-input guarantee, and inputs cannot be constrained statically.
+    # Returning :proven from structure alone was a soundness hole (every model
+    # was vacuously "proven" NaN-safe), so NoNaN routes to empirical checking.
+    # Planned input-range analysis (see ROADMAP.adoc) would enable a sound proof.
 
     :unknown
 end
@@ -316,11 +316,18 @@ function has_bounded_output(model, low, high)
 end
 
 """
-Check if model uses only NaN-safe operations.
+Whether `model` uses only NaN/Inf-safe operations. This is a NECESSARY but not
+SUFFICIENT condition for NaN-freedom (finite inputs are also required and cannot
+be established statically), so it must never be used on its own to claim a
+NoNaN proof — see `try_static_verify`.
+
+A real structural graph analysis is planned (see ROADMAP.adoc). Until it lands
+this makes NO safety claim and returns `false`, so NoNaN is checked empirically
+rather than via a vacuous static "proof". (Previously this returned `true`
+unconditionally — a soundness hole that reported every model as NaN-safe.)
 """
 function has_safe_operations(model)
-    # Simplified check - real implementation would analyze graph
-    true
+    false
 end
 
 """

test/runtests.jl

@@ -751,6 +751,9 @@ with open(args.output, "w", encoding="utf-8") as f:
     include("verification/serialization_tests.jl")
     include("verification/proof_export_tests.jl")
 
+    # Soundness regression tests (P1 holes must never silently reopen)
+    include("verification/soundness_tests.jl")
+
     # CRG Grade C tests
     include("e2e_test.jl")
     include("property_test.jl")

test/verification/soundness_tests.jl

@@ -0,0 +1,55 @@
+# SPDX-License-Identifier: MPL-2.0
+# Soundness regression tests — guard against reintroducing the P1 soundness holes:
+#   G02: vacuous NoNaN static "proof" (has_safe_operations == true)
+#   G01: certificate falsely labelling an unkeyed digest as "SHA256-HMAC"
+# These run inside the main suite so the holes cannot silently reopen.
+
+using Test
+using Axiom
+using JSON
+
+@testset "Soundness (P1 holes)" begin
+    model = Sequential(Dense(10, 5, relu), Dense(5, 3), Softmax())
+
+    @testset "NoNaN is not a vacuous static proof (G02)" begin
+        # Structure alone cannot soundly prove NoNaN (a finite-input guarantee is
+        # also required), so the static path must return :unknown, never :proven.
+        @test Axiom.try_static_verify(NoNaN(), model) === :unknown
+        # The unconditional `true` is gone; the honest predicate makes no claim.
+        @test Axiom.has_safe_operations(model) === false
+        # Regression: genuinely-sound static proofs still work.
+        @test Axiom.try_static_verify(ValidProbabilities(), model) === :proven
+        # NoNaN still verifies empirically on well-behaved data (fallback path).
+        x = Tensor(randn(Float32, 4, 10))
+        res = verify(model; properties = [NoNaN()], data = [(x, nothing)])
+        @test res.passed
+    end
+
+    @testset "Certificate does not falsely claim a keyed signature (G01)" begin
+        x = Tensor(randn(Float32, 2, 10))
+        result = verify(model; properties = [ValidProbabilities(), FiniteOutput()], data = [(x, nothing)])
+        cert = generate_certificate(model, result; model_name = "soundness-ci")
+
+        path = tempname() * ".json"
+        save_certificate(cert, path; format = :json)
+        try
+            content = read(path, String)
+            # The false "SHA256-HMAC" label (unkeyed digest sold as HMAC) is gone.
+            @test !occursin("SHA256-HMAC", content)
+            parsed = JSON.parsefile(path)
+            @test parsed["signature"]["authenticated"] == false
+            @test parsed["signature"]["kind"] == "content-digest"
+        finally
+            rm(path; force = true)
+        end
+
+        # Tamper-evidence: an altered digest is rejected. (A forger who recomputes
+        # the digest still passes — the documented limit of a content digest;
+        # authenticating Ed448+Dilithium5 signatures are tracked in ROADMAP.adoc.)
+        @test verify_certificate(cert)
+        forged = Axiom.Certificate(cert.model_hash, cert.model_name, cert.properties,
+            cert.verification_mode, cert.test_data_hash, cert.proof_type,
+            cert.created_at, cert.axiom_version, cert.verifier_id, "deadbeef")
+        @test !verify_certificate(forged)
+    end
+end