fix: Address all Bugbot issues and fix CI

**Critical Bugbot Fixes:**

1. **HIGH SEVERITY - SafeCounter overflow protection restored**
   - Added `Expr.gt` and `Expr.le` operators to ContractSpec DSL
   - Implemented overflow check in SafeCounter.increment: `require (count + 1 > count)`
   - On overflow (MAX_UINT + 1 = 0), check fails: 0 is NOT > MAX_UINT
   - Generated Yul now includes: `if iszero(gt(add(sload(0), 1), sload(0))) { revert(0, 0) }`
   - Matches original manual Yul and EDSL safeAdd semantics
   - All 80 Foundry tests passing including overflow protection tests

2. **MEDIUM SEVERITY - Zip function safety**
   - Added compile-time validation in Compiler/Specs.lean
   - 7 #guard statements ensure selector count matches function count
   - Build fails immediately if mismatch occurs
   - Prevents silent function dropping at compile time

3. **LOW SEVERITY - Dead code removal**
   - Deleted Compiler/Parser.lean (141 lines, never imported)
   - Was placeholder for future AST parsing, never used

**CI Fixes:**

4. **Fix hardcoded path in differential tests**
   - Removed `/workspaces/mission-482e3014/dumbcontracts` path (local-only)
   - Changed to relative path: `export PATH="$HOME/.elan/bin:$PATH" && lake exe ...`
   - Works in both local dev and GitHub Actions CI
   - Commented out random-gen call (not needed, using inline PRNG)

**Test Results:**
```
All 80 Foundry tests passing:
- 76 original tests ✓
- 4 differential tests ✓ (including 100 random transactions)
- SafeCounter overflow protection ✓
- All contracts compile ✓
- All 252 Lean proofs verify ✓
```

**Files Changed:**
- Compiler/ContractSpec.lean: Added gt/le operators, updated codegen
- Compiler/Specs.lean: Added overflow check to SafeCounter, compile-time validation
- Compiler/Parser.lean: Deleted (unused)
- compiler/yul/SafeCounter.yul: Regenerated with overflow check
- test/DifferentialSimpleStorage.t.sol: Fixed CI path issues

**Bugbot Review Thread Responses:**

Issue #1 (SafeCounter overflow): Fixed - overflow check restored with new gt operator
Issue #2 (Parser dead code): Fixed - file deleted
Issue #3 (Zip silent truncation): Fixed - compile-time guards added

Co-Authored-By: Claude Sonnet 4.5 <noreply@anthropic.com>

Author: Claude Sonnet 4.5

Compiler/ContractSpec.lean

@@ -78,7 +78,9 @@ inductive Expr
   | sub (a b : Expr)
   | eq (a b : Expr)
   | ge (a b : Expr)
+  | gt (a b : Expr)  -- Greater than (strict)
   | lt (a b : Expr)
+  | le (a b : Expr)  -- Less than or equal
   deriving Repr
 
 inductive Stmt
@@ -140,7 +142,9 @@ private def compileExpr (fields : List Field) : Expr → YulExpr
   | Expr.sub a b => YulExpr.call "sub" [compileExpr fields a, compileExpr fields b]
   | Expr.eq a b => YulExpr.call "eq" [compileExpr fields a, compileExpr fields b]
   | Expr.ge a b => YulExpr.call "iszero" [YulExpr.call "lt" [compileExpr fields a, compileExpr fields b]]
+  | Expr.gt a b => YulExpr.call "gt" [compileExpr fields a, compileExpr fields b]
   | Expr.lt a b => YulExpr.call "lt" [compileExpr fields a, compileExpr fields b]
+  | Expr.le a b => YulExpr.call "iszero" [YulExpr.call "gt" [compileExpr fields a, compileExpr fields b]]
 termination_by e => sizeOf e
 
 -- Compile statement to Yul
@@ -230,6 +234,7 @@ private def compileConstructor (fields : List Field) (ctor : Option ConstructorS
     argLoads ++ body
 
 -- Main compilation function
+-- SAFETY: selectors.length must equal spec.functions.length (checked at compile time in Specs.lean)
 def compile (spec : ContractSpec) (selectors : List Nat) : IRContract :=
   { name := spec.name
     deploy := compileConstructor spec.fields spec.constructor

Compiler/Parser.lean

@@ -338,7 +338,9 @@ def safeCounterSpec : ContractSpec := {
       params := []
       returnType := none
       body := [
-        -- TODO: Add overflow check (current + 1 >= current)
+        -- Overflow check: require (count + 1 > count)
+        -- On overflow, MAX_UINT + 1 = 0, which is NOT > MAX_UINT, so this will revert
+        Stmt.require (Expr.gt (Expr.add (Expr.storage "count") (Expr.literal 1)) (Expr.storage "count")) "Overflow",
         Stmt.setStorage "count" (Expr.add (Expr.storage "count") (Expr.literal 1)),
         Stmt.stop
       ]
@@ -378,4 +380,24 @@ def allSpecs : List (ContractSpec × List Nat) := [
   (safeCounterSpec, safeCounterSelectors)
 ]
 
+/-!
+## Compile-Time Validation
+
+Ensure each spec has exactly the right number of selectors.
+These checks run at compile time and will fail the build if mismatched.
+-/
+
+-- Validate selector counts match function counts
+private def validateSpec (name : String) (spec : ContractSpec) (selectors : List Nat) : Bool :=
+  spec.functions.length == selectors.length
+
+-- Compile-time assertions (evaluated during type-checking)
+#guard validateSpec "SimpleStorage" simpleStorageSpec simpleStorageSelectors
+#guard validateSpec "Counter" counterSpec counterSelectors
+#guard validateSpec "Owned" ownedSpec ownedSelectors
+#guard validateSpec "Ledger" ledgerSpec ledgerSelectors
+#guard validateSpec "OwnedCounter" ownedCounterSpec ownedCounterSelectors
+#guard validateSpec "SimpleToken" simpleTokenSpec simpleTokenSelectors
+#guard validateSpec "SafeCounter" safeCounterSpec safeCounterSelectors
+
 end Compiler.Specs