Repair Lean proof suite + make Echo Types a structural typesystem gate

.gitattributes

@@ -17,6 +17,13 @@
 *.v text eol=lf
 *.zig text eol=lf
 
+# Julia-the-Viper source + conformance corpus. These are parsed byte-exactly by
+# the test suite, so pin LF: the cross-platform CI matrix must read identical
+# bytes on a Windows checkout (otherwise CRLF would change parser/whitespace
+# behaviour and fail conformance tests only on Windows).
+*.jtv text eol=lf
+*.pata text eol=lf
+
 # Configuration
 *.toml text eol=lf
 *.json text eol=lf

.github/workflows/cflite_batch.yml

@@ -7,6 +7,7 @@ permissions: read-all
 jobs:
   BatchFuzzing:
     runs-on: ubuntu-latest
+    timeout-minutes: 60
     strategy:
       fail-fast: false
       matrix:

.github/workflows/cflite_pr.yml

@@ -9,6 +9,7 @@ permissions: read-all
 jobs:
   PR:
     runs-on: ubuntu-latest
+    timeout-minutes: 20
     strategy:
       fail-fast: false
       matrix:

.github/workflows/codeql.yml

@@ -23,6 +23,7 @@ permissions:
 jobs:
   analyze:
     runs-on: ubuntu-latest
+    timeout-minutes: 30
     permissions:
       contents: read
       security-events: write

.github/workflows/coverage.yml

@@ -17,8 +17,11 @@ permissions:
 jobs:
   coverage:
     name: Code coverage
+    # No `if: hashFiles('Cargo.toml') != ''` guard — `hashFiles()` is invalid in
+    # a job-level `if:` and startup-fails the whole workflow (see rust-ci.yml).
+    # This repo always has a Cargo workspace.
     runs-on: ubuntu-latest
-    if: hashFiles('Cargo.toml') != ''
+    timeout-minutes: 45
 
     steps:
       - name: Checkout repository
@@ -64,7 +67,7 @@ jobs:
 
       - name: Upload HTML report as artifact
         if: always()
-        uses: actions/upload-artifact@v4
+        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4
         with:
           name: coverage-report
           path: coverage/

.github/workflows/deno.yml

@@ -21,6 +21,7 @@ permissions:
 jobs:
   test:
     runs-on: ubuntu-latest
+    timeout-minutes: 15
 
     steps:
       - name: Setup repo

.github/workflows/dogfood-gate.yml

@@ -22,6 +22,7 @@ jobs:
   a2ml-validate:
     name: Validate A2ML manifests
     runs-on: ubuntu-latest
+    timeout-minutes: 20
 
     steps:
       - name: Checkout repository
@@ -66,6 +67,7 @@ jobs:
   k9-validate:
     name: Validate K9 contracts
     runs-on: ubuntu-latest
+    timeout-minutes: 20
 
     steps:
       - name: Checkout repository
@@ -115,6 +117,7 @@ jobs:
   empty-lint:
     name: Empty-linter (invisible characters)
     runs-on: ubuntu-latest
+    timeout-minutes: 20
 
     steps:
       - name: Checkout repository
@@ -179,6 +182,7 @@ jobs:
   groove-check:
     name: Groove manifest check
     runs-on: ubuntu-latest
+    timeout-minutes: 20
 
     steps:
       - name: Checkout repository
@@ -237,6 +241,7 @@ jobs:
   dogfood-summary:
     name: Dogfooding compliance summary
     runs-on: ubuntu-latest
+    timeout-minutes: 20
     needs: [a2ml-validate, k9-validate, empty-lint, groove-check]
     if: always()
 

.github/workflows/generator-generic-ossf-slsa3-publish.yml

@@ -22,6 +22,7 @@ permissions: read-all
 jobs:
   build:
     runs-on: ubuntu-latest
+    timeout-minutes: 20
     outputs:
       digests: ${{ steps.hash.outputs.digests }}
 

.github/workflows/jekyll-gh-pages.yml

@@ -26,6 +26,7 @@ jobs:
   # Build job
   build:
     runs-on: ubuntu-latest
+    timeout-minutes: 20
     steps:
       - name: Checkout
         uses: actions/checkout@b4ffde65f46336ab88eb53be808477a3936bae11 # v4
@@ -45,6 +46,7 @@ jobs:
       name: github-pages
       url: ${{ steps.deployment.outputs.page_url }}
     runs-on: ubuntu-latest
+    timeout-minutes: 20
     needs: build
     steps:
       - name: Deploy to GitHub Pages

.github/workflows/language-policy.yml

@@ -22,6 +22,7 @@ jobs:
   check-banned-languages:
     name: Check for Banned Languages
     runs-on: ubuntu-latest
+    timeout-minutes: 15
     steps:
       - name: Checkout
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4
@@ -150,6 +151,7 @@ jobs:
   check-required-files:
     name: Check Required Files
     runs-on: ubuntu-latest
+    timeout-minutes: 15
     steps:
       - name: Checkout
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4

.github/workflows/rust-ci.yml

@@ -3,7 +3,14 @@
 #
 # rust-ci.yml — Cargo build, test, clippy, and fmt for Rust projects.
 # Cross-platform matrix: Linux, macOS, Windows.
-# Only runs if Cargo.toml exists in the repo root.
+#
+# NOTE: do NOT gate these jobs with `if: hashFiles('Cargo.toml') != ''`.
+# `hashFiles()` is not valid in a job-level `if:` — GitHub rejects the whole
+# workflow at validation time (startup failure: "Unrecognized function:
+# 'hashFiles'", zero jobs scheduled), which silently disabled Rust CI here.
+# This repo is unconditionally a Cargo workspace, so no guard is needed. (Same
+# lesson is recorded in proof-regression.yml, which guards in a post-checkout
+# step instead.)
 name: Rust CI
 
 on:
@@ -19,7 +26,7 @@ jobs:
   check:
     name: Check (${{ matrix.os }})
     runs-on: ${{ matrix.os }}
-    if: hashFiles('Cargo.toml') != ''
+    timeout-minutes: 30
     strategy:
       fail-fast: false
       matrix:
@@ -49,8 +56,8 @@ jobs:
   test:
     name: Test (${{ matrix.os }})
     runs-on: ${{ matrix.os }}
+    timeout-minutes: 30
     needs: check
-    if: hashFiles('Cargo.toml') != ''
     strategy:
       fail-fast: false
       matrix:

crates/jtv-core/src/echo.rs

@@ -201,7 +201,7 @@ mod tests {
         let safe = ReversibleStmt::AddAssign("x".to_string(), DataExpr::Number(Number::Int(5)));
         let breaking =
             ReversibleStmt::AddAssign("y".to_string(), DataExpr::Identifier("y".to_string()));
-        assert_eq!(classify_stmts(&[safe.clone()]), Echo::Safe);
+        assert_eq!(classify_stmts(std::slice::from_ref(&safe)), Echo::Safe);
         assert_eq!(classify_stmts(&[safe.clone(), breaking]), Echo::Breaking);
     }
 }

crates/jtv-core/src/typechecker.rs

@@ -369,13 +369,27 @@ impl TypeChecker {
                 Ok(())
             }
             ControlStmt::ReverseBlock(block) => {
+                // Echo admissibility is a *structural* property of the block
+                // (does any statement destroy information, e.g. `x += x`?),
+                // independent of the variables' type bindings — so gate on it
+                // FIRST, then type-check the individual statements. Doing it the
+                // other way round let an unbound/ill-typed variable mask the
+                // Echo violation behind a type error.
+                self.check_echo_admissible(&block.body)?;
                 for stmt in &block.body {
                     self.check_reversible_stmt(stmt)?;
                 }
-                self.check_echo_admissible(&block.body)?;
                 Ok(())
             }
             ControlStmt::ReversibleBlock(rb) => {
+                // The forward pass records a reversal log that a later
+                // `reverse tok` inverts, so the body must satisfy the SAME Echo
+                // admissibility rule as a `reverse` block — otherwise the
+                // recorded log cannot be soundly inverted. Checked structurally
+                // and FIRST (like `ReverseBlock`); previously this arm skipped
+                // the Echo gate entirely, leaving the `reversible` form
+                // un-checked.
+                self.check_echo_admissible(&rb.body)?;
                 for stmt in &rb.body {
                     self.check_reversible_stmt(stmt)?;
                 }
@@ -401,10 +415,14 @@ impl TypeChecker {
         }
     }
 
-    /// Enforce the Echo admissibility rule for a reverse block (spec v2 §9):
-    /// a reverse block is well-typed iff no constituent statement is
-    /// `EchoBreaking` (information-destroying). This is the type-checker
-    /// realisation of `blockEcho_admissible` in `jtv_proofs/JtvEcho.lean`.
+    /// Enforce the Echo admissibility rule for a `reverse` / `reversible`
+    /// block (spec v2 §9) under the **Safe-only** reversal policy: the block is
+    /// well-typed iff its aggregate echo is `EchoSafe` — i.e. every statement
+    /// is bijective (`+`/`-` with no self-reference). `EchoNeutral` (structured,
+    /// residue-retaining loss) and `EchoBreaking` (total erasure) are both
+    /// rejected, since neither is invertible by the implemented runtime. This
+    /// is the type-checker realisation of `blockEcho_admissible` in
+    /// `jtv_proofs/JtvEcho.lean`.
     fn check_echo_admissible(&self, body: &[ReversibleStmt]) -> Result<()> {
         let aggregate = echo::classify_stmts(body);
         if !aggregate.admissible_in_reverse() {
@@ -658,6 +676,42 @@ mod tests {
         assert!(checker.check_control_stmt(&stmt).is_ok());
     }
 
+    #[test]
+    fn test_reversible_block_rejects_breaking_echo() {
+        // A `reversible { … } -> tok` block records a reversal log; if any
+        // statement is information-destroying (EchoBreaking) the log cannot be
+        // inverted, so the type checker must reject it under the SAME Echo gate
+        // as a plain `reverse` block (spec v2 §9).
+        use crate::ast::*;
+        let mut checker = TypeChecker::new();
+        let block = ReversibleBlockStmt {
+            body: vec![ReversibleStmt::AddAssign(
+                "x".to_string(),
+                DataExpr::Identifier("x".to_string()),
+            )],
+            token_binding: Some("tok".to_string()),
+        };
+        let stmt = ControlStmt::ReversibleBlock(block);
+        let result = checker.check_control_stmt(&stmt);
+        assert!(matches!(result, Err(JtvError::EchoViolation(_))));
+    }
+
+    #[test]
+    fn test_reversible_block_accepts_safe_echo() {
+        use crate::ast::*;
+        let mut checker = TypeChecker::new();
+        checker.env.set_var("x".to_string(), Type::Int);
+        let block = ReversibleBlockStmt {
+            body: vec![ReversibleStmt::AddAssign(
+                "x".to_string(),
+                DataExpr::Number(Number::Int(5)),
+            )],
+            token_binding: Some("tok".to_string()),
+        };
+        let stmt = ControlStmt::ReversibleBlock(block);
+        assert!(checker.check_control_stmt(&stmt).is_ok());
+    }
+
     #[test]
     fn test_coercion() {
         let code = r#"

jtv_proofs/JtvEcho.lean

@@ -229,7 +229,11 @@ theorem residue_lossy :
     hence `safe` — the value-level justification for `reverse { x += v }`. -/
 theorem neg_injective : Injective (fun n : Int => -n) := by
   intro a b h
-  have : - -a = - -b := by rw [h]
-  simpa using this
+  -- `h : (fun n => -n) a = (fun n => -n) b`; the lambda applications are
+  -- definitionally `-a` / `-b`, so re-state `h` in beta-reduced form (the
+  -- defeq coercion does the beta step `rw` could not see) and finish with
+  -- linear integer reasoning.
+  have h' : -a = -b := h
+  omega
 
 end Jtv.Echo