From 67af0a3c0a68fead0997b9a408b6569f538db0b3 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 1 Jun 2026 13:35:37 +0100 Subject: [PATCH] =?UTF-8?q?fix(ci):=20make=20set-e=20safe=20counter=20incr?= =?UTF-8?q?ements=20+=20correct=20lean4=E2=86=92lean=20prover=20name?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two foundational CI/CD reds on main fixed at source: 1. `scripts/validate-correspondence.sh` — every counter `((var++))` returns exit-code 1 when `var=0` (the post-increment yields the pre-value, which is treated as a falsy arithmetic result). Combined with `set -euo pipefail` this caused the script to exit at the very first PASS line. Replaced all `((var++))` with `var=$((var + 1))` which always returns 0. Verified locally: now reports 18 PASS / 0 WARN / 0 FAIL / 100% confidence, replacing the previous instant exit-1 after a single PASS. 2. `scripts/validate-with-echidna.sh` — same `((var++))` bug AND it passed `--prover lean4` to the echidna CLI, which only accepts `--prover lean` (see `src/rust/provers/mod.rs:660-678` in hyperpolymath/echidna: matches on `"lean"` for `ProverKind::Lean`; `"lean4"` returns `"Unknown prover: lean4"`). Verified against echidna source — the four Lean 4 verify_file calls now route to the correct prover. Affected workflows that should now go green on main: - Correspondence Validation (`.github/workflows/validation.yml`) - ECHIDNA Validation (`.github/workflows/echidna-validation.yml`) Refs valence-shell audit 2026-06-01 (mirror of verisimdb #77-#83 shape). Co-Authored-By: Claude Opus 4.7 (1M context) --- scripts/validate-correspondence.sh | 32 +++++++++++++++--------------- scripts/validate-with-echidna.sh | 24 +++++++++++----------- 2 files changed, 28 insertions(+), 28 deletions(-) diff --git a/scripts/validate-correspondence.sh b/scripts/validate-correspondence.sh index 63e07695..f6386f79 100755 --- a/scripts/validate-correspondence.sh +++ b/scripts/validate-correspondence.sh @@ -37,32 +37,32 @@ check_file_reference() { # Check Lean file exists if [ ! -f "$lean_file" ]; then echo -e "${RED}FAIL${NC} - Lean file not found: $lean_file" - ((fail_count++)) + fail_count=$((fail_count + 1)) return 1 fi # Check Rust file exists if [ ! -f "$rust_file" ]; then echo -e "${RED}FAIL${NC} - Rust file not found: $rust_file" - ((fail_count++)) + fail_count=$((fail_count + 1)) return 1 fi # Check correspondence doc mentions both if ! grep -q "$(basename "$lean_file")" "$CORRESPONDENCE_DOC" 2>/dev/null; then echo -e "${YELLOW}WARN${NC} - Lean file not documented in correspondence" - ((warn_count++)) + warn_count=$((warn_count + 1)) return 0 fi if ! grep -q "$(basename "$rust_file")" "$CORRESPONDENCE_DOC" 2>/dev/null; then echo -e "${YELLOW}WARN${NC} - Rust file not documented in correspondence" - ((warn_count++)) + warn_count=$((warn_count + 1)) return 0 fi echo -e "${GREEN}PASS${NC}" - ((pass_count++)) + pass_count=$((pass_count + 1)) } # Function to check property test coverage @@ -74,15 +74,15 @@ check_property_test_coverage() { if grep -q "$test_pattern" "$IMPL_DIR/tests/property_tests.rs" 2>/dev/null; then echo -e "${GREEN}PASS${NC}" - ((pass_count++)) + pass_count=$((pass_count + 1)) return 0 elif grep -q "$test_pattern" "$IMPL_DIR/tests/property_correspondence_tests.rs" 2>/dev/null; then echo -e "${GREEN}PASS${NC}" - ((pass_count++)) + pass_count=$((pass_count + 1)) return 0 else echo -e "${YELLOW}WARN${NC} - No property test found" - ((warn_count++)) + warn_count=$((warn_count + 1)) return 0 fi } @@ -111,12 +111,12 @@ echo echo "4. Conditional Operations (Phase 6 M14)" if [ -f "$IMPL_DIR/src/test_command.rs" ]; then echo -e " test/[ implementation... ${GREEN}PASS${NC}" - ((pass_count++)) + pass_count=$((pass_count + 1)) check_property_test_coverage "test -f" "prop_test_f_file_detection" check_property_test_coverage "test -d" "prop_test_d_directory_detection" else echo -e " test/[ implementation... ${RED}FAIL${NC}" - ((fail_count++)) + fail_count=$((fail_count + 1)) fi echo @@ -124,12 +124,12 @@ echo echo "5. Logical Operators (Phase 6 M14)" if grep -q "LogicalOp" "$IMPL_DIR/src/parser.rs" 2>/dev/null; then echo -e " &&/|| implementation... ${GREEN}PASS${NC}" - ((pass_count++)) + pass_count=$((pass_count + 1)) check_property_test_coverage "logical AND" "prop_logical_and_short_circuit" check_property_test_coverage "logical OR" "prop_logical_or_short_circuit" else echo -e " &&/|| implementation... ${RED}FAIL${NC}" - ((fail_count++)) + fail_count=$((fail_count + 1)) fi echo @@ -137,11 +137,11 @@ echo echo "6. Quote Processing (Phase 6 M13)" if [ -f "$IMPL_DIR/src/quotes.rs" ]; then echo -e " Quote module... ${GREEN}PASS${NC}" - ((pass_count++)) + pass_count=$((pass_count + 1)) check_property_test_coverage "quote processing" "prop_quote_prevents_glob" else echo -e " Quote module... ${RED}FAIL${NC}" - ((fail_count++)) + fail_count=$((fail_count + 1)) fi echo @@ -149,11 +149,11 @@ echo echo "7. Glob Expansion (Phase 6 M12)" if [ -f "$IMPL_DIR/src/glob.rs" ]; then echo -e " Glob module... ${GREEN}PASS${NC}" - ((pass_count++)) + pass_count=$((pass_count + 1)) check_property_test_coverage "glob expansion" "prop_glob_deterministic" else echo -e " Glob module... ${RED}FAIL${NC}" - ((fail_count++)) + fail_count=$((fail_count + 1)) fi echo diff --git a/scripts/validate-with-echidna.sh b/scripts/validate-with-echidna.sh index af66dffb..0922e350 100755 --- a/scripts/validate-with-echidna.sh +++ b/scripts/validate-with-echidna.sh @@ -48,7 +48,7 @@ verify_file() { if [ ! -f "$REPO_ROOT/$file" ]; then echo "[SKIP] $label — file not found: $file" - ((SKIPPED++)) + SKIPPED=$((SKIPPED + 1)) return 0 fi @@ -56,28 +56,28 @@ verify_file() { local output output=$("$ECHIDNA" verify "$REPO_ROOT/$file" --prover "$prover" --timeout 120 $VERBOSE $FORMAT_FLAG 2>&1) && { echo -e "\r[PASS] $label" - ((PASSED++)) + PASSED=$((PASSED + 1)) } || { # Distinguish prover-not-found from actual verification failure if echo "$output" | grep -qi "not found\|not installed\|not available\|no such\|cannot find"; then echo -e "\r[SKIP] $label (prover '$prover' not available)" - ((SKIPPED++)) + SKIPPED=$((SKIPPED + 1)) else echo -e "\r[FAIL] $label" if [ -n "$VERBOSE" ]; then echo " $output" | head -3 fi - ((FAILED++)) + FAILED=$((FAILED + 1)) fi } } # ─── Step 1: Verify Lean 4 proofs (primary source of truth) ─── echo "── Step 1: Lean 4 Proofs ──" -verify_file "Lean 4: FilesystemModel" "proofs/lean4/FilesystemModel.lean" "lean4" -verify_file "Lean 4: FileOperations" "proofs/lean4/FileOperations.lean" "lean4" -verify_file "Lean 4: FilesystemComposition" "proofs/lean4/FilesystemComposition.lean" "lean4" -verify_file "Lean 4: FilesystemEquivalence" "proofs/lean4/FilesystemEquivalence.lean" "lean4" +verify_file "Lean 4: FilesystemModel" "proofs/lean4/FilesystemModel.lean" "lean" +verify_file "Lean 4: FileOperations" "proofs/lean4/FileOperations.lean" "lean" +verify_file "Lean 4: FilesystemComposition" "proofs/lean4/FilesystemComposition.lean" "lean" +verify_file "Lean 4: FilesystemEquivalence" "proofs/lean4/FilesystemEquivalence.lean" "lean" echo "" # ─── Step 2: Verify Coq proofs ─── @@ -123,19 +123,19 @@ echo "── Step 7: Rust Correspondence Tests ──" echo -n "[....] cargo test --test correspondence_tests" if (cd "$REPO_ROOT/impl/rust-cli" && cargo test --test correspondence_tests 2>/dev/null); then echo -e "\r[PASS] cargo test --test correspondence_tests (28 tests)" - ((PASSED++)) + PASSED=$((PASSED + 1)) else echo -e "\r[FAIL] cargo test --test correspondence_tests" - ((FAILED++)) + FAILED=$((FAILED + 1)) fi echo -n "[....] cargo test --test property_tests" if (cd "$REPO_ROOT/impl/rust-cli" && cargo test --test property_tests 2>/dev/null); then echo -e "\r[PASS] cargo test --test property_tests (28 tests)" - ((PASSED++)) + PASSED=$((PASSED + 1)) else echo -e "\r[FAIL] cargo test --test property_tests" - ((FAILED++)) + FAILED=$((FAILED + 1)) fi echo ""