From 8a82e9796c9382c1c76d46461fa9cd9fdc891046 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 3 Jun 2026 17:38:43 +0000 Subject: [PATCH 1/4] proof(lean): repair JtvEcho + JtvExtended; wire JtvExtended into lake build MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The Lean 4 proof suite (jtv_proofs/) did not compile under the pinned v4.12.0 toolchain, and the apex module JtvExtended.lean was orphaned — absent from lakefile.lean, so `lake build` never checked it, despite verification/PROOF-CAPABILITY-MATRIX.adoc listing it as `verified`. Fixes: * JtvEcho.neg_injective: after `intro a b h`, `h` keeps its un-beta-reduced form `(fun n => -n) a = (fun n => -n) b`, so `rw [h]` could not match the goal `- -a = - -b`. Coerce `h` to its beta-reduced form (defeq) and close with `omega`. * JtvExtended.lean (never compiled against v4.12.0): - replace the Mathlib-only `ring` with `omega` (Lean core has no Mathlib here); - add the missing `omega` discharges to `sub_eq_add_neg` and `simplify_add_neg_self`; - drop the redundant `omega` after a closing `simp` in `neg_subexpr_size_lt` (use `simp only … ; omega`); - convert four dangling `/-- … -/` doc comments (attached to no declaration) to plain `/- … -/` block comments — these were hard parse errors that cascaded spurious failures downstream; - `DataSandbox.noStateMod`: replace the invalid term `(eval e σ; σ)` with `(eval e σ, σ).2 = σ` (Data eval is a read-only function); - `data_is_sandboxed`: `theorem` → `def` (DataSandbox is a Type, a record of proofs, not a Prop); - `dead_code_elim`: spell the congruence hypothesis with explicit `semanticEquiv` (the `≃` infix mis-parses in that higher-order position); - `groundEquivDecidable`: rebuild on the real value `evalDataExpr _ State.empty` (the previous `have v := …` lost the definitional link, leaving the iff unprovable). * lakefile.lean: add `lean_lib JtvExtended` and include it in the `JtvAll` default target so the apex module is verified by `lake build` and the proof-regression workflow. `lake build` is green from a clean tree (all 10 targets, cold); the sorry/admit/axiom-free invariant holds across all eight libraries. https://claude.ai/code/session_01BJmfoz1ZS1Pejy9LLMY742 --- jtv_proofs/JtvEcho.lean | 8 ++++-- jtv_proofs/JtvExtended.lean | 57 +++++++++++++++++++++++-------------- jtv_proofs/lakefile.lean | 9 +++++- 3 files changed, 49 insertions(+), 25 deletions(-) diff --git a/jtv_proofs/JtvEcho.lean b/jtv_proofs/JtvEcho.lean index f251650..655f98f 100644 --- a/jtv_proofs/JtvEcho.lean +++ b/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 diff --git a/jtv_proofs/JtvExtended.lean b/jtv_proofs/JtvExtended.lean index bf54605..44b27f0 100644 --- a/jtv_proofs/JtvExtended.lean +++ b/jtv_proofs/JtvExtended.lean @@ -44,8 +44,8 @@ theorem add_right_cancel (a b c : DataExpr) (σ : State) theorem neg_add_distrib (a b : DataExpr) (σ : State) : evalDataExpr (DataExpr.neg (DataExpr.add a b)) σ = evalDataExpr (DataExpr.add (DataExpr.neg a) (DataExpr.neg b)) σ := by - simp [evalDataExpr] - ring + simp only [evalDataExpr] + omega /-- **Theorem (Subtraction via Addition)**: @@ -54,7 +54,8 @@ theorem neg_add_distrib (a b : DataExpr) (σ : State) : theorem sub_eq_add_neg (a b : DataExpr) (σ : State) : evalDataExpr a σ - evalDataExpr b σ = evalDataExpr (DataExpr.add a (DataExpr.neg b)) σ := by - simp [evalDataExpr] + simp only [evalDataExpr] + omega -- ============================================================================ -- SECTION 2: EXPRESSION SIZE AND COMPLEXITY @@ -83,12 +84,13 @@ theorem subexpr_size_lt (e₁ e₂ : DataExpr) : theorem neg_subexpr_size_lt (e : DataExpr) : e.size < (DataExpr.neg e).size := by - simp [DataExpr.size] + simp only [DataExpr.size] omega -/-- +/- **Theorem (Evaluation Steps Bounded by Size)**: The number of evaluation steps is O(size(e)). + (Meta-theorem about the operational semantics; not formalized here.) -/ -- This is a meta-theorem about the operational semantics @@ -171,10 +173,13 @@ theorem semEquiv_neg_cong (e₁ e₂ : DataExpr) (h : e₁ ≃ e₂) : **Theorem (Dead Code Elimination)**: Replacing a subexpression with an equivalent one preserves semantics. -/ +-- Stated with explicit `semanticEquiv` rather than the `≃` notation: in this +-- higher-order position (a congruence hypothesis `hctx`) the infix notation's +-- precedence interacts badly with the `→`, so we spell it out. theorem dead_code_elim (context : DataExpr → DataExpr) (e e' : DataExpr) - (h : e ≃ e') - (hctx : ∀ a b, a ≃ b → context a ≃ context b) : - context e ≃ context e' := + (h : semanticEquiv e e') + (hctx : ∀ (a b : DataExpr), semanticEquiv a b → semanticEquiv (context a) (context b)) : + semanticEquiv (context e) (context e') := hctx e e' h /-- @@ -199,7 +204,8 @@ theorem simplify_zero_add (e : DataExpr) : theorem simplify_add_neg_self (e : DataExpr) : DataExpr.add e (DataExpr.neg e) ≃ DataExpr.zero := by intro σ - simp [evalDataExpr, DataExpr.zero] + simp only [evalDataExpr, DataExpr.zero] + omega /-- **Theorem (Algebraic Simplification: -(-x) = x)**: @@ -220,9 +226,10 @@ theorem simplify_neg_neg (e : DataExpr) : def dependsOn (e : DataExpr) (x : String) : Prop := x ∈ e.freeVars -/-- +/- **Theorem (Dependency Transitivity)**: If a term depends on x and x depends on y, the expression depends on y. + (Requires tracking through state transformations; not formalized here.) -/ -- This requires tracking through state transformations @@ -264,9 +271,10 @@ theorem rev_totality (op : RevOp) (σ : State) : -- SECTION 8: TYPE THEORY METATHEOREMS -- ============================================================================ -/-- +/- **Theorem (Type Preservation for Reduction)**: If Γ ⊢ e : τ and e → e', then Γ ⊢ e' : τ. + (See JtvTypes.lean for the typing rules; not re-derived here.) -/ -- See JtvTypes.lean for the typing rules @@ -312,12 +320,17 @@ theorem control_data_noninterference (e : DataExpr) (s : ControlStmt) (σ : Stat 4. Access external resources -/ structure DataSandbox where - noStateMod : ∀ e σ, (evalDataExpr e σ; σ) = σ + -- Evaluating a Data expression returns a value while leaving the state + -- untouched: pairing the result with the input state, the state component + -- is exactly the input state (Data evaluation is a read-only function). + noStateMod : ∀ (e : DataExpr) (σ : State), (evalDataExpr e σ, σ).2 = σ noIO : True -- No I/O constructs in DataExpr terminates : ∀ e σ, ∃ v, evalDataExpr e σ = v noExternal : True -- No external access constructs -theorem data_is_sandboxed : DataSandbox := { +-- `DataSandbox` is a record of (proof) properties — a `Type`, not a `Prop` — +-- so this evidence bundle is a `def`, not a `theorem`. +def data_is_sandboxed : DataSandbox := { noStateMod := fun _ _ => rfl, noIO := trivial, terminates := dataExpr_totality, @@ -336,9 +349,10 @@ theorem eval_functorial (e₁ e₂ : DataExpr) (σ : State) : evalDataExpr (DataExpr.add e₁ e₂) σ = evalDataExpr e₁ σ + evalDataExpr e₂ σ := rfl -/-- +/- **Theorem (Natural Transformation)**: State transformation is natural with respect to evaluation. + (For closed expressions, evaluation is independent of state; not formalized here.) -/ -- For closed expressions, evaluation is independent of state @@ -358,19 +372,18 @@ instance : DecidableEq DataExpr := inferInstance -/ def groundEquivDecidable (e₁ e₂ : DataExpr) (h₁ : e₁.freeVars = []) (h₂ : e₂.freeVars = []) : - Decidable (e₁ ≃ e₂) := by - -- Ground terms have constant values - have v₁ := evalDataExpr e₁ State.empty - have v₂ := evalDataExpr e₂ State.empty - exact decidable_of_iff (v₁ = v₂) (by + Decidable (e₁ ≃ e₂) := + -- Ground terms have a single value (their evaluation in any state, here the + -- empty state). For closed expressions, semantic equivalence reduces to + -- equality of those values — and `Int` equality is decidable. + decidable_of_iff (evalDataExpr e₁ State.empty = evalDataExpr e₂ State.empty) (by constructor · intro h σ have eq₁ := closed_context_independent e₁ σ State.empty h₁ have eq₂ := closed_context_independent e₂ σ State.empty h₂ - simp [eq₁, eq₂, h] + rw [eq₁, eq₂]; exact h · intro h - exact h State.empty - ) + exact h State.empty) -- ============================================================================ -- SECTION 12: SUMMARY OF VERIFIED PROPERTIES diff --git a/jtv_proofs/lakefile.lean b/jtv_proofs/lakefile.lean index ba190ad..ec04024 100644 --- a/jtv_proofs/lakefile.lean +++ b/jtv_proofs/lakefile.lean @@ -34,7 +34,14 @@ lean_lib JtvEcho where -- (aligns with the echo-types Agda library / EchoTypes.jl) roots := #[`JtvEcho] +lean_lib JtvExtended where + -- Extended metatheory: algebraic cancellation/distribution, expression + -- size/complexity, semantic-equivalence congruences, optimization + -- correctness, decidability, reversibility composition, and the Data + -- sandboxing bundle. Imports every other library (the apex module). + roots := #[`JtvExtended] + -- Build all proofs @[default_target] lean_lib JtvAll where - roots := #[`JtvCore, `JtvTheorems, `JtvOperational, `JtvTypes, `JtvSecurity, `JtvEcho] + roots := #[`JtvCore, `JtvTheorems, `JtvOperational, `JtvTypes, `JtvSecurity, `JtvEcho, `JtvExtended] From ebc37b95e432c515f0497c7cff627908df3d2010 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 3 Jun 2026 17:46:53 +0000 Subject: [PATCH 2/4] feat(typechecker): make Echo Types a structural, uniform gate on reversibility MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Echo Types were modelled in `crates/jtv-core/src/echo.rs` and gated only the `reverse { … }` form, with one pre-existing bug and one gap: * The Echo admissibility check ran AFTER per-statement type inference, so an unbound/ill-typed variable masked the Echo violation behind a type error. This is why `test_reverse_block_rejects_breaking_echo` was *failing* on the baseline: `reverse { x += x }` (x unbound) errored as `UndefinedVariable` rather than the asserted `EchoViolation`. Echo classification is purely structural (does the target appear in the expression?), so the gate now runs FIRST and the violation is reported regardless of type bindings. * `ControlStmt::ReversibleBlock` (the v2 `reversible { … } -> tok` form, which records a reversal log later inverted by `reverse tok`) skipped the Echo gate entirely. It now enforces the same Safe-only admissibility rule — an irreversible body (e.g. `y += y`) can't produce a soundly-invertible log. Changes: * typechecker.rs: gate both `ReverseBlock` and `ReversibleBlock` on `check_echo_admissible`, checked structurally and before type inference; correct the stale doc comment (the policy is Safe-only — `EchoNeutral` and `EchoBreaking` are both rejected, not just `EchoBreaking`). * Add `test_reversible_block_{rejects_breaking,accepts_safe}_echo` mirroring the reverse-block tests. * PROOF-CAPABILITY-MATRIX.adoc: record that the gate covers both reversibility forms and is structural/first. `cargo test -p jtv-core` is now fully green (97 lib + all integration suites); the previously-failing reverse-block Echo test passes. The Lean model (`jtv_proofs/JtvEcho.lean`, `blockEcho_admissible`) is unchanged and remains the source of truth for this gate. https://claude.ai/code/session_01BJmfoz1ZS1Pejy9LLMY742 --- crates/jtv-core/src/typechecker.rs | 64 +++++++++++++++++++++-- verification/PROOF-CAPABILITY-MATRIX.adoc | 7 ++- 2 files changed, 65 insertions(+), 6 deletions(-) diff --git a/crates/jtv-core/src/typechecker.rs b/crates/jtv-core/src/typechecker.rs index c9905e4..30ccdc5 100644 --- a/crates/jtv-core/src/typechecker.rs +++ b/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#" diff --git a/verification/PROOF-CAPABILITY-MATRIX.adoc b/verification/PROOF-CAPABILITY-MATRIX.adoc index 3faa736..13d1ec2 100644 --- a/verification/PROOF-CAPABILITY-MATRIX.adoc +++ b/verification/PROOF-CAPABILITY-MATRIX.adoc @@ -87,12 +87,17 @@ induction. Corrected as part of the Phase-1 doc-truthing pass. | `Echo.join` (absorbing `breaking`, unit `safe`) | `Echo::join` | `Echo.admissible` | `Echo::admissible_in_reverse` | `Echo.le` (`a ⊔ b = b`) | `Echo::leq` -| `blockEcho` / `blockEcho_admissible` | `classify_stmts` + reverse-block gate +| `blockEcho` / `blockEcho_admissible` | `classify_stmts` + reverse/reversible-block gate | `Fibre f y := { x // f x = y }` | (value-level; effect classes implemented) |=== The Rust gate (`TypeChecker::check_echo_admissible`) raises `JtvError::EchoViolation` exactly when `blockEcho_admissible` returns `false`. +It runs on *both* reversibility forms — `reverse { … }` (`ReverseBlock`) and +`reversible { … } -> tok` (`ReversibleBlock`) — and is checked *structurally* +and *before* the per-statement type inference, so a structurally +irreversible block (e.g. the self-referential `x += x`) is reported as an +Echo violation regardless of the variables' type bindings. *Authority:* `JtvEcho.lean` is authoritative for JtV implementation semantics; the `echo-types` Agda library is the conceptual source/reference. The Agda↔Lean From b72fbf56af68f06b8d873e3d6a94788ca2ac6947 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 3 Jun 2026 17:56:30 +0000 Subject: [PATCH 3/4] ci(workflows): SHA-pin coverage upload-artifact + add timeout-minutes MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Clears the failing `governance / Workflow security linter` check and the Hypatia `missing_timeout_minutes` / `unpinned_action` (medium) findings — all on workflow files this branch had not otherwise touched. * coverage.yml: pin `actions/upload-artifact@v4` to its commit SHA (`ea165f8d65b6e75b540449e92b4886f43607fa02`), matching the repo's existing pin-everything convention. This is the one finding that actually failed the security linter. * Add `timeout-minutes` to every normal (`runs-on`) job that lacked one: cflite_batch (60, ≥ its 1800s fuzz budget), cflite_pr (20), codeql (30), coverage (45), deno (15), dogfood-gate (20 ×5), the SLSA generator's build job (20), jekyll-gh-pages (20 ×2), language-policy (15 ×2), rust-ci (30 ×2). Deliberately NOT changed (would be unsound or out of this scope): * Jobs that *call* reusable workflows (governance, mirror, hypatia-scan, scorecard, and the SLSA provenance job) — `timeout-minutes` is not valid on a reusable-workflow-call job, so adding it would break them. * proof-regression.yml already sets per-job timeouts. * The `download_then_run` (toolchain `curl | sh`) and the `governance-reusable.yml@main` ref are higher-effort / possibly intentional; left for a dedicated governance pass. Verified: the linter's own checks pass locally (no unpinned actions; SPDX + permissions present on all workflows) and every workflow still parses as valid YAML. https://claude.ai/code/session_01BJmfoz1ZS1Pejy9LLMY742 --- .github/workflows/cflite_batch.yml | 1 + .github/workflows/cflite_pr.yml | 1 + .github/workflows/codeql.yml | 1 + .github/workflows/coverage.yml | 3 ++- .github/workflows/deno.yml | 1 + .github/workflows/dogfood-gate.yml | 5 +++++ .github/workflows/generator-generic-ossf-slsa3-publish.yml | 1 + .github/workflows/jekyll-gh-pages.yml | 2 ++ .github/workflows/language-policy.yml | 2 ++ .github/workflows/rust-ci.yml | 2 ++ 10 files changed, 18 insertions(+), 1 deletion(-) diff --git a/.github/workflows/cflite_batch.yml b/.github/workflows/cflite_batch.yml index 0757e57..340f417 100644 --- a/.github/workflows/cflite_batch.yml +++ b/.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: diff --git a/.github/workflows/cflite_pr.yml b/.github/workflows/cflite_pr.yml index e194056..40964e8 100644 --- a/.github/workflows/cflite_pr.yml +++ b/.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: diff --git a/.github/workflows/codeql.yml b/.github/workflows/codeql.yml index 9e32d15..94ba8ff 100644 --- a/.github/workflows/codeql.yml +++ b/.github/workflows/codeql.yml @@ -23,6 +23,7 @@ permissions: jobs: analyze: runs-on: ubuntu-latest + timeout-minutes: 30 permissions: contents: read security-events: write diff --git a/.github/workflows/coverage.yml b/.github/workflows/coverage.yml index f8c06ca..66181dc 100644 --- a/.github/workflows/coverage.yml +++ b/.github/workflows/coverage.yml @@ -18,6 +18,7 @@ jobs: coverage: name: Code coverage runs-on: ubuntu-latest + timeout-minutes: 45 if: hashFiles('Cargo.toml') != '' steps: @@ -64,7 +65,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/ diff --git a/.github/workflows/deno.yml b/.github/workflows/deno.yml index 911ea36..e133317 100644 --- a/.github/workflows/deno.yml +++ b/.github/workflows/deno.yml @@ -21,6 +21,7 @@ permissions: jobs: test: runs-on: ubuntu-latest + timeout-minutes: 15 steps: - name: Setup repo diff --git a/.github/workflows/dogfood-gate.yml b/.github/workflows/dogfood-gate.yml index a9f5c7c..309c766 100644 --- a/.github/workflows/dogfood-gate.yml +++ b/.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() diff --git a/.github/workflows/generator-generic-ossf-slsa3-publish.yml b/.github/workflows/generator-generic-ossf-slsa3-publish.yml index f515746..79dec84 100644 --- a/.github/workflows/generator-generic-ossf-slsa3-publish.yml +++ b/.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 }} diff --git a/.github/workflows/jekyll-gh-pages.yml b/.github/workflows/jekyll-gh-pages.yml index 919efac..609731a 100644 --- a/.github/workflows/jekyll-gh-pages.yml +++ b/.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 diff --git a/.github/workflows/language-policy.yml b/.github/workflows/language-policy.yml index d5b3940..a7a0108 100644 --- a/.github/workflows/language-policy.yml +++ b/.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 diff --git a/.github/workflows/rust-ci.yml b/.github/workflows/rust-ci.yml index 8e9f59b..8250df1 100644 --- a/.github/workflows/rust-ci.yml +++ b/.github/workflows/rust-ci.yml @@ -19,6 +19,7 @@ jobs: check: name: Check (${{ matrix.os }}) runs-on: ${{ matrix.os }} + timeout-minutes: 30 if: hashFiles('Cargo.toml') != '' strategy: fail-fast: false @@ -49,6 +50,7 @@ jobs: test: name: Test (${{ matrix.os }}) runs-on: ${{ matrix.os }} + timeout-minutes: 30 needs: check if: hashFiles('Cargo.toml') != '' strategy: From 5631ffd41742cfcdd1ff8cd4d7f09ee51fba8e00 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 3 Jun 2026 21:39:27 +0000 Subject: [PATCH 4/4] ci: fix root cause of chronically-failing Rust CI + Coverage (startup failure) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `rust-ci.yml` and `coverage.yml` gated their jobs with `if: hashFiles('Cargo.toml') != ''` at the JOB level. `hashFiles()` is not a valid function in a job-level `if:`, so GitHub rejected the whole workflow at validation time: Unrecognized function: 'hashFiles'. Located at position 1 within expression: hashFiles('Cargo.toml') != '' The result was a *startup failure with zero jobs scheduled* — so Rust CI (build / fmt / clippy / test, 3-OS matrix) and Coverage have not actually run on any push since at least 2026-05-27. Every `Rust CI` run on `main` is a 0-job `failure`. (This is the exact gotcha already documented in proof-regression.yml, which guards in a post-checkout step instead.) Fixes, at root: * Remove the invalid job-level guards from both workflows (this repo is unconditionally a Cargo workspace, so no guard is needed) and add a comment so the broken pattern is not reintroduced. * `echo.rs`: clear the one `clippy::cloned_ref_to_slice_refs` lint (`&[safe.clone()]` → `std::slice::from_ref(&safe)`) that `clippy -D warnings` flags — previously invisible because the `check` job never ran. * `.gitattributes`: pin `*.jtv` / `*.pata` to `eol=lf`. The conformance corpus (57 `.jtv` files) is parsed byte-exactly; pinning LF keeps the Windows leg of the now-live matrix reading identical bytes (CRLF would otherwise fail conformance tests only on Windows). Verified locally (Linux): `cargo fmt --all --check`, `cargo check --all-targets`, `cargo clippy --all-targets -- -D warnings`, and `cargo test --all-targets` all pass; the workflows parse as valid YAML and still satisfy the governance linter (SHA-pinned actions, SPDX, permissions). https://claude.ai/code/session_01BJmfoz1ZS1Pejy9LLMY742 --- .gitattributes | 7 +++++++ .github/workflows/coverage.yml | 4 +++- .github/workflows/rust-ci.yml | 11 ++++++++--- crates/jtv-core/src/echo.rs | 2 +- 4 files changed, 19 insertions(+), 5 deletions(-) diff --git a/.gitattributes b/.gitattributes index e50db6f..129917e 100644 --- a/.gitattributes +++ b/.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 diff --git a/.github/workflows/coverage.yml b/.github/workflows/coverage.yml index 66181dc..2bdb401 100644 --- a/.github/workflows/coverage.yml +++ b/.github/workflows/coverage.yml @@ -17,9 +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 timeout-minutes: 45 - if: hashFiles('Cargo.toml') != '' steps: - name: Checkout repository diff --git a/.github/workflows/rust-ci.yml b/.github/workflows/rust-ci.yml index 8250df1..15c3756 100644 --- a/.github/workflows/rust-ci.yml +++ b/.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: @@ -20,7 +27,6 @@ jobs: name: Check (${{ matrix.os }}) runs-on: ${{ matrix.os }} timeout-minutes: 30 - if: hashFiles('Cargo.toml') != '' strategy: fail-fast: false matrix: @@ -52,7 +58,6 @@ jobs: runs-on: ${{ matrix.os }} timeout-minutes: 30 needs: check - if: hashFiles('Cargo.toml') != '' strategy: fail-fast: false matrix: diff --git a/crates/jtv-core/src/echo.rs b/crates/jtv-core/src/echo.rs index e79760e..fa36fd3 100644 --- a/crates/jtv-core/src/echo.rs +++ b/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); } }