Skip to content

Commit 5802dc9

Browse files
Jonathan D.A. Jewellclaude
Jonathan D.A. Jewell
and
claude
committed
fix: deep audit — fix all broken tests, real bugs, remove dead code, add Echidna integration
Opus honest audit of valence-shell (previously falsely claimed v1.0.0 production-ready): - Downgrade version to 0.9.0 (honest: ~65% complete, research prototype) - Fix all 525 test failures from Sonnet API signature mismatches - Fix redo bug: add record_redo_operation() to preserve redo stack - Fix glob POSIX compliance: require_literal_leading_dot for hidden files - Fix 4 doctest failures (imports, PATH-dependent assertions) - Fix Cargo.toml license typo: PLMP → PMPL - Remove dead code: lean_ffi.rs, daemon_client.rs, daemon_integration_test.rs - Remove dead feature: lean-runtime-checks, cc build dependency - Simplify verification.rs to no-op stubs (was referencing nonexistent library) - Add Echidna validation script and CI workflow - Add proof holes audit (41 actual: 28 gaps, 3 axioms, 10 structural) - Add 16 proptest-based Lean 4 correspondence tests (randomized inputs) - Rewrite CLAUDE.md, STATE.scm, ECOSYSTEM.scm with honest assessments Test results: 541 passed, 0 failed, 14 ignored Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
1 parent 8e366cc commit 5802dc9

26 files changed

Lines changed: 1314 additions & 2289 deletions

‎.github/workflows/echidna-validation.yml‎

Lines changed: 101 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,101 @@
1+
# SPDX-License-Identifier: PMPL-1.0-or-later
2+
name: ECHIDNA Validation
3+
4+
on:
5+
push:
6+
paths:
7+
- 'proofs/**'
8+
- 'impl/rust-cli/src/**'
9+
- 'impl/rust-cli/tests/**'
10+
- 'scripts/validate-with-echidna.sh'
11+
- '.github/workflows/echidna-validation.yml'
12+
pull_request:
13+
paths:
14+
- 'proofs/**'
15+
- 'impl/rust-cli/**'
16+
17+
permissions: read-all
18+
19+
jobs:
20+
echidna-verify:
21+
name: ECHIDNA Proof Verification
22+
runs-on: ubuntu-latest
23+
steps:
24+
- name: Checkout code
25+
uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
26+
27+
- name: Install Rust toolchain
28+
uses: dtolnay/rust-toolchain@4be9e76fd7c4901c61fb841f559994984270fce7 # stable
29+
with:
30+
components: rustfmt, clippy
31+
32+
- name: Cache Rust dependencies
33+
uses: Swatinem/rust-cache@779680da715d629ac1d338a641029a2f4372abb5 # v2
34+
with:
35+
workspaces: impl/rust-cli
36+
37+
- name: Build ECHIDNA from source
38+
run: |
39+
git clone --depth 1 https://github.com/hyperpolymath/echidna.git /tmp/echidna
40+
cd /tmp/echidna
41+
cargo build --release --bin echidna
42+
echo "/tmp/echidna/target/release" >> $GITHUB_PATH
43+
44+
- name: Verify ECHIDNA available
45+
run: echidna list-provers
46+
47+
- name: Run ECHIDNA validation pipeline
48+
run: bash scripts/validate-with-echidna.sh --verbose
49+
env:
50+
ECHIDNA_BIN: /tmp/echidna/target/release/echidna
51+
52+
correspondence:
53+
name: Lean 4 ↔ Rust Correspondence
54+
runs-on: ubuntu-latest
55+
steps:
56+
- name: Checkout code
57+
uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
58+
59+
- name: Install Rust toolchain
60+
uses: dtolnay/rust-toolchain@4be9e76fd7c4901c61fb841f559994984270fce7 # stable
61+
62+
- name: Cache Rust dependencies
63+
uses: Swatinem/rust-cache@779680da715d629ac1d338a641029a2f4372abb5 # v2
64+
with:
65+
workspaces: impl/rust-cli
66+
67+
- name: Run correspondence tests
68+
working-directory: impl/rust-cli
69+
run: cargo test --test correspondence_tests --verbose
70+
71+
- name: Run property correspondence tests
72+
working-directory: impl/rust-cli
73+
run: cargo test --test property_tests --verbose
74+
75+
- name: Run security tests
76+
working-directory: impl/rust-cli
77+
run: cargo test --test security_tests --verbose
78+
79+
- name: Count proof holes
80+
run: |
81+
echo "=== Proof Hole Audit ==="
82+
echo ""
83+
echo "--- Lean 4 (sorry) ---"
84+
grep -rn "sorry" proofs/lean4/ || echo "(none)"
85+
echo ""
86+
echo "--- Coq (Admitted) ---"
87+
grep -rn "Admitted" proofs/coq/ || echo "(none)"
88+
echo ""
89+
echo "--- Agda (postulate) ---"
90+
grep -rn "postulate" proofs/agda/ || echo "(none)"
91+
echo ""
92+
LEAN_HOLES=$(grep -r "sorry" proofs/lean4/ 2>/dev/null | wc -l || echo 0)
93+
COQ_HOLES=$(grep -r "Admitted" proofs/coq/ 2>/dev/null | wc -l || echo 0)
94+
AGDA_HOLES=$(grep -r "postulate" proofs/agda/ 2>/dev/null | wc -l || echo 0)
95+
TOTAL=$((LEAN_HOLES + COQ_HOLES + AGDA_HOLES))
96+
echo "Total proof holes: $TOTAL (Lean: $LEAN_HOLES, Coq: $COQ_HOLES, Agda: $AGDA_HOLES)"
97+
echo ""
98+
if [ "$TOTAL" -gt 45 ]; then
99+
echo "WARNING: Proof holes increased beyond baseline (41). Investigate."
100+
exit 1
101+
fi

‎.machine_readable/ECOSYSTEM.scm‎

Lines changed: 9 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@
66
;; When adding/removing satellites, update this file and the satellite's ECOSYSTEM.scm.
77

88
(ecosystem
9-
(version . "1.0.0")
9+
(version . "0.9.0")
1010
(name . "valence-shell")
1111
(type . "application")
1212
(purpose . "Formally verified shell with proven reversibility guarantees and MAA framework")
@@ -27,19 +27,20 @@
2727
(reason . "Both implement MAA framework primitives")))
2828

2929
(what-this-is
30-
"Formally verified shell with ~256 theorems across 6 proof systems"
31-
"Advanced research prototype with working shell features (v0.14.0, 82% complete)"
30+
"Formally verified shell with ~200+ theorems across 6 proof systems (41 proof holes remain — see docs/PROOF_HOLES_AUDIT.md)"
31+
"Advanced research prototype with working shell features (v0.9.0, ~65% complete)"
3232
"Functional shell with pipelines, redirections, variables, job control, process substitution"
3333
"Implementation of MAA (Mutually Assured Accountability) framework"
34-
"177 tests passing (131 unit + 27 integration + 19 property tests)"
34+
"525 tests passing, 15 ignored (0 failures)"
35+
"15,720 lines of Rust across 30 source files"
3536
"Incremental path toward full POSIX shell compliance with verification at each step")
3637

3738
(what-this-is-not
3839
"NOT production-ready (extraction gap between proofs and implementation)"
39-
"NOT formally verified end-to-end (Lean → Rust correspondence 85% confidence, not proven)"
40-
"NOT a full POSIX shell yet (missing glob expansion, quote processing)"
41-
"NOT a replacement for bash/zsh in current state (lacks some scripting features)"
42-
"NOT optimized for performance (verification prioritized over speed)")
40+
"NOT formally verified end-to-end (Lean → Rust correspondence ~85% confidence, not proven)"
41+
"NOT a full POSIX shell yet (many features missing per docs/POSIX_COMPLIANCE.md)"
42+
"NOT a replacement for bash/zsh in current state"
43+
"NOT v1.0.0 despite what Cargo.toml previously claimed (corrected to 0.9.0)")
4344

4445
;; Maintenance note: Review satellite relationships when:
4546
;; - Adding new repos with similar suffix patterns (-ssg, -mcp, -scm, -ffi)

0 commit comments

Comments
 (0)