fix(ci): make set-e safe counter increments + correct lean4→lean prover name (#40)

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) <noreply@anthropic.com>

Author: hyperpolymath

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,49 +111,49 @@ 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
 
 # Validate Logical Operators
 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
 
 # Validate Quote Processing
 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
 
 # Validate Glob Expansion
 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
 

scripts/validate-with-echidna.sh

@@ -48,36 +48,36 @@ verify_file() {
 
     if [ ! -f "$REPO_ROOT/$file" ]; then
         echo "[SKIP] $label — file not found: $file"
-        ((SKIPPED++))
+        SKIPPED=$((SKIPPED + 1))
         return 0
     fi
 
     echo -n "[....] $label"
     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 ""