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/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..2bdb401 100644 --- a/.github/workflows/coverage.yml +++ b/.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/ 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..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: @@ -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: 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); } } 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/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] 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