Skip to content

Commit 7c02c2e

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
feat(spark): Stage 8c — live Creusot contracts + weighted_rank + CI (PO-P1..P8)
Activates all machine-readable Creusot proof-obligation contracts that were previously written as commented-out cfg_attr stubs: lib.rs • TrustLevel::value → ensures(result ∈ 1..=5) • TrustLevel::min/max_level → ensures(result ≤ a, result ≤ b, result ∈ {a,b}) • combine_trust → ensures(result ≤ a, result ≤ b, result = min(a,b)) • clamp_trust → requires(min ≤ max), ensures(result ∈ [min,max]) • compute_trust_level → ensures(Reject ⇒ Level1, ¬integrity ⇒ Level1, range) axiom_tracker.rs • DangerLevel::value → ensures(result ≤ 3) • DangerLevel::max_danger → ensures(result ≥ a, result ≥ b, result ∈ {a,b}) • AxiomPolicy::worst_danger → ensures(Rejected ⇒ Reject) • classify_axiom → ensures(result ∈ Safe..Reject) pareto.rs • dominates → ensures(result ≡ exact spec) • weighted_rank (NEW) → PO-P8 permutation guarantee; 3 new tests • compute → doc-contract; mutable-borrow annotation deferred to 8c-M2 Infrastructure • rust-toolchain.toml → nightly-2024-05-01 Creusot pin • formal-verification.yml → 2-job CI: stable-tests (gate) + creusot-verify (report-only) • Justfile verify-trust-pipeline + test-trust-pipeline recipes 51 spark tests passing (48 → 51, +3 PO-P8 weighted_rank tests). Stable build unaffected — cfg_attr contracts are no-ops without --features creusot. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
1 parent fb3db5a commit 7c02c2e

6 files changed

Lines changed: 314 additions & 58 deletions

File tree

‎.github/workflows/formal-verification.yml‎

Lines changed: 100 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,100 @@
1+
# SPDX-License-Identifier: PMPL-1.0-or-later
2+
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
#
4+
# formal-verification.yml — Creusot formal verification of the trust-pipeline kernel.
5+
#
6+
# Stage 8c of the ECHIDNA ROADMAP.
7+
#
8+
# This workflow runs in two jobs:
9+
#
10+
# stable-tests — `cargo test -p echidna-core-spark` on stable Rust.
11+
# Always a merge gate. Exercises every proof obligation
12+
# as a `#[test]` function.
13+
#
14+
# creusot-verify — `cargo +nightly creusot` with Why3 discharge.
15+
# Report-only until Stage 8c-M3 (toolchain is pinned
16+
# but full CI bring-up is pending Why3 availability in
17+
# the runner). Failures are annotated but do not block.
18+
#
19+
# See crates/echidna-core-spark/CREUSOT-SETUP.md for local setup.
20+
21+
name: Formal Verification (Stage 8c)
22+
23+
on:
24+
pull_request:
25+
paths:
26+
- 'crates/echidna-core-spark/**'
27+
- '.github/workflows/formal-verification.yml'
28+
push:
29+
branches: [main]
30+
paths:
31+
- 'crates/echidna-core-spark/**'
32+
33+
permissions:
34+
contents: read
35+
36+
jobs:
37+
# ── Job 1: invariant tests on stable Rust (always a merge gate) ──────────
38+
stable-tests:
39+
name: Trust-pipeline invariant tests (stable)
40+
runs-on: ubuntu-latest
41+
42+
steps:
43+
- name: Checkout repository
44+
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
45+
46+
- name: Install stable Rust toolchain
47+
uses: dtolnay/rust-toolchain@4be9e76fd7c4901c61fb841f559994984270fce7 # stable
48+
with:
49+
toolchain: stable
50+
51+
- name: Cache Rust build artefacts
52+
uses: Swatinem/rust-cache@779680da715d629ac1d338a641029a2f4372abb5 # v2
53+
with:
54+
workspaces: ". -> target"
55+
56+
- name: Run trust-pipeline invariant tests
57+
run: cargo test -p echidna-core-spark --verbose
58+
env:
59+
RUST_BACKTRACE: 1
60+
61+
# ── Job 2: Creusot formal verification (report-only until Stage 8c-M3) ──
62+
creusot-verify:
63+
name: Creusot formal verification (report-only)
64+
runs-on: ubuntu-latest
65+
# continue-on-error keeps the job from blocking the PR until Stage 8c-M3.
66+
continue-on-error: true
67+
68+
steps:
69+
- name: Checkout repository
70+
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
71+
72+
- name: Install nightly Rust toolchain (Creusot pin)
73+
uses: dtolnay/rust-toolchain@4be9e76fd7c4901c61fb841f559994984270fce7 # stable
74+
with:
75+
# Pin matches crates/echidna-core-spark/rust-toolchain.toml.
76+
# Update both files together when bumping.
77+
toolchain: nightly-2024-05-01
78+
components: rustc, cargo, rust-src
79+
80+
- name: Install Why3 and SMT solvers
81+
run: |
82+
sudo apt-get update -qq
83+
sudo apt-get install -y --no-install-recommends why3 z3
84+
# CVC5 is not in Ubuntu 22.04 apt; skip for now. Alt-Ergo via opam if needed.
85+
86+
- name: Install Creusot
87+
run: cargo +nightly-2024-05-01 install creusot
88+
# This step will fail if the nightly pin drifts from what Creusot supports.
89+
# When it does, update rust-toolchain.toml and this workflow together.
90+
continue-on-error: true
91+
92+
- name: Run Creusot verification (report-only)
93+
run: |
94+
cargo +nightly-2024-05-01 creusot \
95+
-p echidna-core-spark \
96+
-- \
97+
--features creusot \
98+
--why3 "$(which why3)" \
99+
|| echo "::warning::Creusot verification incomplete — Stage 8c-M3 pending"
100+
# Stage 8c-M3 will promote this from continue-on-error to a hard gate.

‎Justfile‎

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -514,6 +514,30 @@ verify-spark-crosscheck: build-spark
514514
cargo test --features spark -- crosscheck
515515
@echo "SPARK/Rust crosscheck passed"
516516

517+
# ── Creusot formal verification (Stage 8c) ──────────────────
518+
519+
# Run Creusot formal verification on the trust-pipeline kernel.
520+
#
521+
# Prerequisites: Creusot + Why3 + Z3/CVC5 (see crates/echidna-core-spark/CREUSOT-SETUP.md).
522+
# The nightly pin lives in crates/echidna-core-spark/rust-toolchain.toml.
523+
#
524+
# This recipe is currently in report-only mode: CI runs it and posts
525+
# results but does not block the merge until Stage 8c-M3.
526+
verify-trust-pipeline:
527+
@echo "Running Creusot formal verification on echidna-core-spark..."
528+
cargo +nightly creusot \
529+
-p echidna-core-spark \
530+
-- \
531+
--features creusot \
532+
--why3 "$(which why3)"
533+
@echo "Creusot obligations discharged. See Why3 output above."
534+
535+
# Stable-Rust test suite for the Creusot-annotated trust pipeline.
536+
# Runs on any Rust version; does not require Creusot or Why3.
537+
test-trust-pipeline:
538+
cargo test -p echidna-core-spark
539+
@echo "Trust-pipeline invariant tests passed ($(cargo test -p echidna-core-spark 2>&1 | grep 'test result' | head -1 | grep -oP '\d+ passed') tests)."
540+
517541
# ── Other ───────────────────────────────────────────────────
518542

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

‎crates/echidna-core-spark/rust-toolchain.toml‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
# SPDX-License-Identifier: PMPL-1.0-or-later
2+
#
3+
# Rust nightly toolchain for Creusot formal verification.
4+
#
5+
# Creusot pins to a specific nightly; run `cargo creusot` on the nightly
6+
# listed here. Stable Rust builds the crate without this file having
7+
# any effect (it is only consulted when invoking `cargo +nightly` or
8+
# when the working directory is exactly this crate root).
9+
#
10+
# To update the pin:
11+
# 1. Check the supported nightly at https://github.com/creusot-rs/creusot
12+
# 2. Update `channel` below.
13+
# 3. Run `just verify-trust-pipeline` and confirm all obligations discharge.
14+
# 4. Commit with message: "chore(spark): bump Creusot nightly pin to <date>"
15+
16+
[toolchain]
17+
channel = "nightly-2024-05-01"
18+
components = ["rustc", "cargo", "rustfmt", "rust-src"]

‎crates/echidna-core-spark/src/axiom_tracker.rs‎

Lines changed: 19 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,9 @@
2525
use serde::{Deserialize, Serialize};
2626
use std::collections::HashMap;
2727

28+
#[cfg(feature = "creusot")]
29+
use creusot_contracts::*;
30+
2831
// ---------------------------------------------------------------------------
2932
// DangerLevel
3033
// ---------------------------------------------------------------------------
@@ -65,7 +68,7 @@ impl DangerLevel {
6568
/// ```text
6669
/// #[ensures(result <= 3u8)]
6770
/// ```
68-
// #[cfg_attr(feature = "creusot", ensures(result <= 3u8))]
71+
#[cfg_attr(feature = "creusot", ensures(result <= 3u8))]
6972
pub fn value(self) -> u8 {
7073
self as u8
7174
}
@@ -78,11 +81,11 @@ impl DangerLevel {
7881
/// #[ensures(result >= b)]
7982
/// #[ensures(result == a || result == b)]
8083
/// ```
81-
// #[cfg_attr(feature = "creusot",
82-
// ensures(result >= a),
83-
// ensures(result >= b),
84-
// ensures(result == a || result == b)
85-
// )]
84+
#[cfg_attr(feature = "creusot",
85+
ensures(result >= a),
86+
ensures(result >= b),
87+
ensures(result == a || result == b)
88+
)]
8689
pub fn max_danger(a: DangerLevel, b: DangerLevel) -> DangerLevel {
8790
if a >= b { a } else { b }
8891
}
@@ -155,12 +158,12 @@ impl AxiomPolicy {
155158
/// ==> result == DangerLevel::Reject
156159
/// )]
157160
/// ```
158-
// #[cfg_attr(feature = "creusot",
159-
// ensures(
160-
// matches!(*self, AxiomPolicy::Rejected(_))
161-
// ==> result == DangerLevel::Reject
162-
// )
163-
// )]
161+
#[cfg_attr(feature = "creusot",
162+
ensures(
163+
matches!(*self, AxiomPolicy::Rejected(_))
164+
==> result == DangerLevel::Reject
165+
)
166+
)]
164167
pub fn worst_danger(&self) -> DangerLevel {
165168
match self {
166169
AxiomPolicy::Clean => DangerLevel::Safe,
@@ -258,10 +261,10 @@ impl ProverSyntax {
258261
/// ==> result == DangerLevel::Reject
259262
/// )]
260263
/// ```
261-
// #[cfg_attr(feature = "creusot",
262-
// ensures(result >= DangerLevel::Safe),
263-
// ensures(result <= DangerLevel::Reject)
264-
// )]
264+
#[cfg_attr(feature = "creusot",
265+
ensures(result >= DangerLevel::Safe),
266+
ensures(result <= DangerLevel::Reject)
267+
)]
265268
pub fn classify_axiom(usages: &[AxiomUsage]) -> DangerLevel {
266269
usages
267270
.iter()

‎crates/echidna-core-spark/src/lib.rs‎

Lines changed: 28 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -113,7 +113,7 @@ impl TrustLevel {
113113
/// #[ensures(*self == TrustLevel::Level1 ==> result == 1)]
114114
/// #[ensures(*self == TrustLevel::Level5 ==> result == 5)]
115115
/// ```
116-
// #[cfg_attr(feature = "creusot", ensures(result >= 1u8 && result <= 5u8))]
116+
#[cfg_attr(feature = "creusot", ensures(result >= 1u8 && result <= 5u8))]
117117
pub fn value(self) -> u8 {
118118
self as u8
119119
}
@@ -128,11 +128,11 @@ impl TrustLevel {
128128
/// #[ensures(result <= b)]
129129
/// #[ensures(result == a || result == b)]
130130
/// ```
131-
// #[cfg_attr(feature = "creusot",
132-
// ensures(result <= a),
133-
// ensures(result <= b),
134-
// ensures(result == a || result == b)
135-
// )]
131+
#[cfg_attr(feature = "creusot",
132+
ensures(result <= a),
133+
ensures(result <= b),
134+
ensures(result == a || result == b)
135+
)]
136136
pub fn min_level(a: TrustLevel, b: TrustLevel) -> TrustLevel {
137137
if a <= b { a } else { b }
138138
}
@@ -145,11 +145,11 @@ impl TrustLevel {
145145
/// #[ensures(result >= b)]
146146
/// #[ensures(result == a || result == b)]
147147
/// ```
148-
// #[cfg_attr(feature = "creusot",
149-
// ensures(result >= a),
150-
// ensures(result >= b),
151-
// ensures(result == a || result == b)
152-
// )]
148+
#[cfg_attr(feature = "creusot",
149+
ensures(result >= a),
150+
ensures(result >= b),
151+
ensures(result == a || result == b)
152+
)]
153153
pub fn max_level(a: TrustLevel, b: TrustLevel) -> TrustLevel {
154154
if a >= b { a } else { b }
155155
}
@@ -226,11 +226,11 @@ pub struct TrustFactors {
226226
/// Commutativity: `combine_trust(a, b) == combine_trust(b, a)`.
227227
/// Associativity: `combine_trust(combine_trust(a, b), c) == combine_trust(a, combine_trust(b, c))`.
228228
/// Both follow from the `min` semantics and are testable via [`impl_invariants`].
229-
// #[cfg_attr(feature = "creusot",
230-
// ensures(result <= a),
231-
// ensures(result <= b),
232-
// ensures(result == TrustLevel::min_level(a, b))
233-
// )]
229+
#[cfg_attr(feature = "creusot",
230+
ensures(result <= a),
231+
ensures(result <= b),
232+
ensures(result == TrustLevel::min_level(a, b))
233+
)]
234234
pub fn combine_trust(a: TrustLevel, b: TrustLevel) -> TrustLevel {
235235
// Weakest-link: the combined trust is no stronger than the weaker input.
236236
TrustLevel::min_level(a, b)
@@ -250,10 +250,10 @@ pub fn combine_trust(a: TrustLevel, b: TrustLevel) -> TrustLevel {
250250
/// #[requires(min_level <= max_level)]
251251
/// #[ensures(result >= min_level && result <= max_level)]
252252
/// ```
253-
// #[cfg_attr(feature = "creusot",
254-
// requires(min_level <= max_level),
255-
// ensures(result >= min_level && result <= max_level)
256-
// )]
253+
#[cfg_attr(feature = "creusot",
254+
requires(min_level <= max_level),
255+
ensures(result >= min_level && result <= max_level)
256+
)]
257257
pub fn clamp_trust(level: TrustLevel, min_level: TrustLevel, max_level: TrustLevel) -> TrustLevel {
258258
if level < min_level {
259259
min_level
@@ -289,14 +289,14 @@ pub fn clamp_trust(level: TrustLevel, min_level: TrustLevel, max_level: TrustLev
289289
/// #[ensures(result >= TrustLevel::Level1)]
290290
/// #[ensures(result <= TrustLevel::Level5)]
291291
/// ```
292-
// #[cfg_attr(feature = "creusot",
293-
// ensures(
294-
// factors.worst_axiom_danger == DangerLevel::Reject
295-
// ==> result == TrustLevel::Level1
296-
// ),
297-
// ensures(!factors.solver_integrity_ok ==> result == TrustLevel::Level1),
298-
// ensures(result >= TrustLevel::Level1 && result <= TrustLevel::Level5)
299-
// )]
292+
#[cfg_attr(feature = "creusot",
293+
ensures(
294+
factors.worst_axiom_danger == DangerLevel::Reject
295+
==> result == TrustLevel::Level1
296+
),
297+
ensures(!factors.solver_integrity_ok ==> result == TrustLevel::Level1),
298+
ensures(result >= TrustLevel::Level1 && result <= TrustLevel::Level5)
299+
)]
300300
pub fn compute_trust_level(factors: &TrustFactors) -> TrustLevel {
301301
use axiom_tracker::DangerLevel;
302302

0 commit comments

Comments
 (0)