Skip to content

Commit 5f0f289

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
feat(spark): introduce SPARK/Ada axiom-policy enforcement layer
Ports the enforce_policy decision logic from axiom_tracker.rs into a formally-verified Ada/SPARK layer (GNATprove discharges the soundness and precision invariants automatically from the loop invariants): Soundness — any Reject-level usage → Policy_Rejected output Precision — no Reject-level usage → never Policy_Rejected output Architecture (Idris2 ABI → SPARK/Ada → Zig C-ABI shim → Rust): src/abi/EchidnaABI/AxiomTracker.idr — Idris2 ABI spec + proofs src/ada/spark/{axiom_types,axiom_policy,axiom_c_bridge}.ads/.adb src/ada/spark/echidna_spark.gpr — GPRbuild project src/zig/ffi/axiom_spark_bridge.zig — Zig C-ABI re-export src/rust/ffi/spark_axiom.rs — Rust extern "C" bindings src/rust/verification/axiom_tracker.rs — crosscheck method added Wiring: Cargo.toml — `spark` feature flag build.rs — links libechidna_spark + libechidna_spark_zig Justfile — build-spark-ada / prove-spark / spark-all recipes "Rust" here means Rust/SPARK per estate convention. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
1 parent eed105c commit 5f0f289

15 files changed

Lines changed: 1190 additions & 4 deletions

‎Cargo.toml‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -85,6 +85,7 @@ typed-wasm = { path = "crates/typed_wasm" }
8585
[features]
8686
default = []
8787
chapel = [] # Enable Chapel parallel proof search (requires Zig FFI library)
88+
spark = [] # Enable SPARK-verified axiom-policy (requires libechidna_spark from GPRbuild)
8889
verisim = [ # Enable VeriSimDB persistent proof storage (8-modality octads)
8990
"dep:ciborium",
9091
"dep:sha2",

‎Justfile‎

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -462,6 +462,39 @@ test-chapel-ffi:
462462
chapel-all: build-chapel-poc build-chapel-ffi test-chapel
463463
@echo "Chapel accelerator fully built and tested"
464464

465+
# ── SPARK axiom-policy layer ─────────────────────────────────
466+
467+
# Step 1: compile Ada/SPARK to static library (requires GNAT + GNATprove)
468+
build-spark-ada:
469+
gprbuild -P src/ada/spark/echidna_spark.gpr -j0
470+
@echo "SPARK library built at lib/spark/libechidna_spark.a"
471+
472+
# Step 2: run GNATprove to formally verify the SPARK contracts
473+
prove-spark:
474+
gnatprove -P src/ada/spark/echidna_spark.gpr --level=2 \
475+
--prover=z3,cvc5,altergo --timeout=30 --report=fail -j0
476+
@echo "GNATprove: all SPARK contracts discharged"
477+
478+
# Step 3: compile Zig bridge (links against libechidna_spark.a)
479+
build-spark-zig: build-spark-ada
480+
cd src/zig && zig build -Dspark=true -Doptimize=ReleaseSafe
481+
@echo "SPARK Zig bridge built at src/zig/zig-out/lib/libechidna_spark_zig.a"
482+
483+
# Step 4: build Rust with SPARK feature enabled
484+
build-spark: build-spark-zig
485+
cargo build --features spark
486+
@echo "Rust+SPARK build complete"
487+
488+
# Full SPARK pipeline: prove → build → test
489+
spark-all: prove-spark build-spark-zig
490+
cargo test --features spark -- spark
491+
@echo "SPARK layer: proved, built, tested"
492+
493+
# Cross-check: run both Rust and SPARK enforce_policy, assert agreement
494+
verify-spark-crosscheck: build-spark
495+
cargo test --features spark -- crosscheck
496+
@echo "SPARK/Rust crosscheck passed"
497+
465498
# ── Other ───────────────────────────────────────────────────
466499

467500
# [AUTO-GENERATED] Multi-arch / RISC-V target

‎build.rs‎

Lines changed: 47 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,56 @@
11
// SPDX-License-Identifier: PMPL-1.0-or-later
22
//! Build script for ECHIDNA
33
//!
4-
//! When the `chapel` feature is enabled, this links against the Zig-built
5-
//! Chapel FFI bridge library (libechidna_chapel_ffi).
4+
//! Chapel: Chapel (.chpl) → Zig bridge → Rust
5+
//! SPARK: Ada/SPARK (echidna_spark.gpr) → Zig bridge → Rust
66
//!
7-
//! Build order: Chapel (.chpl) → C headers → Zig (chapel_bridge.zig) → Rust (proof_search.rs)
7+
//! SPARK build order:
8+
//! 1. gprbuild -P src/ada/spark/echidna_spark.gpr
9+
//! 2. cd src/zig && zig build -Dspark
10+
//! 3. cargo build --features spark
811
912
fn main() {
10-
// Only link Chapel FFI when the feature is enabled
13+
// SPARK axiom-policy bridge (requires GPRbuild + Zig; see just spark-all)
14+
#[cfg(feature = "spark")]
15+
{
16+
let spark_zig_dir = std::path::PathBuf::from(env!("CARGO_MANIFEST_DIR"))
17+
.join("src")
18+
.join("zig")
19+
.join("zig-out")
20+
.join("lib");
21+
22+
let spark_ada_dir = std::path::PathBuf::from(env!("CARGO_MANIFEST_DIR"))
23+
.join("lib")
24+
.join("spark");
25+
26+
if spark_zig_dir.exists() {
27+
println!("cargo:rustc-link-search=native={}", spark_zig_dir.display());
28+
println!("cargo:rustc-link-lib=static=echidna_spark_zig");
29+
} else {
30+
println!(
31+
"cargo:warning=SPARK Zig bridge not found. \
32+
Build with: cd src/zig && zig build -Dspark"
33+
);
34+
}
35+
36+
if spark_ada_dir.exists() {
37+
println!("cargo:rustc-link-search=native={}", spark_ada_dir.display());
38+
println!("cargo:rustc-link-lib=static=echidna_spark");
39+
println!("cargo:rustc-link-lib=dylib=gnat");
40+
} else {
41+
println!(
42+
"cargo:warning=SPARK Ada library not found. \
43+
Build with: gprbuild -P src/ada/spark/echidna_spark.gpr"
44+
);
45+
}
46+
47+
println!("cargo:rustc-link-lib=dylib=c");
48+
println!("cargo:rerun-if-changed=src/ada/spark/axiom_policy.adb");
49+
println!("cargo:rerun-if-changed=src/ada/spark/axiom_policy.ads");
50+
println!("cargo:rerun-if-changed=src/zig/ffi/axiom_spark_bridge.zig");
51+
}
52+
53+
// Chapel parallel proof search bridge
1154
#[cfg(feature = "chapel")]
1255
{
1356
// Look for the Zig-built library in src/zig_ffi/zig-out/lib/

‎src/abi/EchidnaABI/AxiomTracker.idr‎

Lines changed: 174 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,174 @@
1+
-- SPDX-License-Identifier: PMPL-1.0-or-later
2+
-- Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
3+
--
4+
-- EchidnaABI.AxiomTracker
5+
--
6+
-- Idris2 ABI type specification for the axiom-policy enforcement layer.
7+
-- This file is the *formal specification* that the SPARK implementation
8+
-- (src/ada/spark/axiom_policy.ads/.adb) must conform to.
9+
--
10+
-- The key invariants stated here as dependent-type propositions are exactly
11+
-- what GNATprove discharges on the SPARK side. Both must agree.
12+
--
13+
-- NO believe_me — every proof is constructive (Refl, case analysis, or
14+
-- explicit witnesses).
15+
16+
module EchidnaABI.AxiomTracker
17+
18+
import EchidnaABI.Types -- ProverKind, Platform, etc.
19+
import Data.List
20+
import Data.So
21+
import Decidable.Equality
22+
23+
%default total
24+
25+
-- ════════════════════════════════════════════════════════════════════════════
26+
-- DangerLevel (mirrors src/rust/verification/axiom_tracker.rs)
27+
-- ════════════════════════════════════════════════════════════════════════════
28+
29+
||| The danger level assigned to an axiom usage.
30+
||| Total order: Safe < Noted < Warning < Reject.
31+
public export
32+
data DangerLevel
33+
= Safe -- standard library axiom; allowed unconditionally
34+
| Noted -- classical axiom in constructive system; noted but allowed
35+
| Warning -- incomplete proof marker (sorry, Admitted); warning issued
36+
| Reject -- known unsound construct; proof REJECTED
37+
38+
-- C-ABI wire encoding (u8 discriminant, matches Rust PartialOrd order)
39+
public export
40+
dangerToU8 : DangerLevel -> Bits8
41+
dangerToU8 Safe = 0
42+
dangerToU8 Noted = 1
43+
dangerToU8 Warning = 2
44+
dangerToU8 Reject = 3
45+
46+
public export
47+
u8ToDanger : Bits8 -> Maybe DangerLevel
48+
u8ToDanger 0 = Just Safe
49+
u8ToDanger 1 = Just Noted
50+
u8ToDanger 2 = Just Warning
51+
u8ToDanger 3 = Just Reject
52+
u8ToDanger _ = Nothing
53+
54+
||| Round-trip: decode . encode = id
55+
public export
56+
dangerRoundTrip : (d : DangerLevel) -> u8ToDanger (dangerToU8 d) = Just d
57+
dangerRoundTrip Safe = Refl
58+
dangerRoundTrip Noted = Refl
59+
dangerRoundTrip Warning = Refl
60+
dangerRoundTrip Reject = Refl
61+
62+
-- ════════════════════════════════════════════════════════════════════════════
63+
-- AxiomPolicy (mirrors Rust AxiomPolicy discriminant)
64+
-- ════════════════════════════════════════════════════════════════════════════
65+
66+
||| The policy verdict for a scanned proof.
67+
public export
68+
data AxiomPolicy
69+
= PolicyClean -- only Safe axioms; unconditionally accepted
70+
| PolicyClassical -- classical axioms noted; accepted with note
71+
| PolicyIncomplete -- sorry/Admitted found; accepted with warning
72+
| PolicyRejected -- unsound construct; REJECTED
73+
74+
-- C-ABI wire encoding (i32 discriminant)
75+
public export
76+
policyToI32 : AxiomPolicy -> Int32
77+
policyToI32 PolicyClean = 0
78+
policyToI32 PolicyClassical = 1
79+
policyToI32 PolicyIncomplete = 2
80+
policyToI32 PolicyRejected = 3
81+
82+
||| A proof is acceptable if and only if the policy is not PolicyRejected.
83+
public export
84+
isAcceptable : AxiomPolicy -> Bool
85+
isAcceptable PolicyRejected = False
86+
isAcceptable _ = True
87+
88+
-- ════════════════════════════════════════════════════════════════════════════
89+
-- The two central soundness invariants
90+
-- (These are what SPARK GNATprove formally verifies on the Ada side.)
91+
-- ════════════════════════════════════════════════════════════════════════════
92+
93+
||| Specification of enforcePolicySpec: the reference function that the
94+
||| SPARK implementation must replicate.
95+
|||
96+
||| This is NOT the live callable; it is the specification the bridge tests
97+
||| against via cross-check mode.
98+
public export
99+
enforcePolicySpec : List DangerLevel -> AxiomPolicy
100+
enforcePolicySpec usages =
101+
if any (== Reject) usages then PolicyRejected
102+
else if any (== Warning) usages then PolicyIncomplete
103+
else if any (== Noted) usages then PolicyClassical
104+
else PolicyClean
105+
106+
-- ────────────────────────────────────────────────────────────────────────────
107+
-- Invariant 1 (Soundness): Reject-in → PolicyRejected-out
108+
-- ────────────────────────────────────────────────────────────────────────────
109+
110+
||| Proof that if any usage is Reject, the spec returns PolicyRejected.
111+
public export
112+
soundness
113+
: (usages : List DangerLevel)
114+
-> Elem Reject usages
115+
-> enforcePolicySpec usages = PolicyRejected
116+
soundness usages prf =
117+
-- 'any (== Reject) usages' is True whenever Reject is an element
118+
rewrite anyRejectIsTrue usages prf in Refl
119+
where
120+
anyRejectIsTrue
121+
: (us : List DangerLevel)
122+
-> Elem Reject us
123+
-> any (== Reject) us = True
124+
anyRejectIsTrue (Reject :: _) Here = Refl
125+
anyRejectIsTrue (_ :: rest) (There p) = anyRejectIsTrue rest p
126+
anyRejectIsTrue [] p = absurd p
127+
128+
-- ────────────────────────────────────────────────────────────────────────────
129+
-- Invariant 2 (Precision): no Reject-in → not PolicyRejected-out
130+
-- ────────────────────────────────────────────────────────────────────────────
131+
132+
||| Proof that if no usage is Reject, the spec never returns PolicyRejected.
133+
public export
134+
precision
135+
: (usages : List DangerLevel)
136+
-> ((e : DangerLevel) -> Elem e usages -> Not (e = Reject))
137+
-> Not (enforcePolicySpec usages = PolicyRejected)
138+
precision usages noReject prf =
139+
-- If enforcePolicySpec returns PolicyRejected, then 'any (== Reject) usages'
140+
-- must have been True, so there is a Reject in the list — contradicting noReject.
141+
let anyFalse = noRejectMeansAnyFalse usages noReject
142+
in rewrite anyFalse in absurd prf
143+
where
144+
noRejectMeansAnyFalse
145+
: (us : List DangerLevel)
146+
-> ((e : DangerLevel) -> Elem e us -> Not (e = Reject))
147+
-> any (== Reject) us = False
148+
noRejectMeansAnyFalse [] _ = Refl
149+
noRejectMeansAnyFalse (x :: xs) noR =
150+
case decEq x Reject of
151+
Yes Refl => absurd (noR Reject Here Refl)
152+
No _ =>
153+
let rest = noRejectMeansAnyFalse xs (\e p => noR e (There p))
154+
in rewrite rest in Refl
155+
156+
-- ════════════════════════════════════════════════════════════════════════════
157+
-- ABI Layout declarations (for Zig/Rust bridge validation)
158+
-- ════════════════════════════════════════════════════════════════════════════
159+
160+
||| C function name exported by the SPARK/Ada layer (via Zig shim).
161+
public export
162+
sparkEnforcePolicySymbol : String
163+
sparkEnforcePolicySymbol = "echidna_spark_enforce_policy"
164+
165+
||| C function name for worst-danger query.
166+
public export
167+
sparkWorstDangerSymbol : String
168+
sparkWorstDangerSymbol = "echidna_spark_worst_danger"
169+
170+
||| Maximum array size accepted by the C bridge.
171+
||| Must match Axiom_Policy.Max_Usages in src/ada/spark/axiom_policy.ads.
172+
public export
173+
maxUsages : Nat
174+
maxUsages = 1024

0 commit comments

Comments
 (0)