From 996b7b7e4a5bb259acd9f0f9a5e85f9fa2a515ca Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Fri, 2 Oct 2026 13:06:13 +0100 Subject: [PATCH 1/2] chore(lean4): bump toolchain v4.12.0 -> v4.34.1 - lean-toolchain: leanprover/lean4:v4.34.1 - PathTraversal: List.dropLast_append_of_ne_nil no longer takes the list as an explicit argument; pass only the non-empty proof. This is the only v4.34 regression. - SymlinkOperations: trailing `/-- Summary -/` doc comment had no declaration to attach to (parse error on v4.12.0 too); make it a plain block comment. No proof changed. - rust-cli.yml lean4 job: elan --default-toolchain v4.34.1. - lakefile header: last verified v4.34.1 (2026-10-02), and list which libs build. FileContentOperations, RMOOperations, CopyMoveOperations and PermissionOperations fail on v4.12.0 as well (measured from a clean `git archive HEAD` build) and are not touched here. Theorem count 111 -> 111, sorry 0 -> 0, no axioms. Co-Authored-By: Claude Opus 5.5 --- .github/workflows/rust-cli.yml | 2 +- proofs/lean4/PathTraversal.lean | 2 +- proofs/lean4/SymlinkOperations.lean | 2 +- proofs/lean4/lakefile.lean | 8 +++++++- proofs/lean4/lean-toolchain | 2 +- 5 files changed, 11 insertions(+), 5 deletions(-) diff --git a/.github/workflows/rust-cli.yml b/.github/workflows/rust-cli.yml index 46863943..51e3b5f9 100644 --- a/.github/workflows/rust-cli.yml +++ b/.github/workflows/rust-cli.yml @@ -75,7 +75,7 @@ jobs: # verify its SHA-256, then execute it — no `curl | sh`. curl -sSfL https://raw.githubusercontent.com/leanprover/elan/v3.1.1/elan-init.sh -o elan-init.sh echo "f5d473c923c093759ae3839073bec2a58e82cb8bc0e4083930e76090da75b310 elan-init.sh" | sha256sum -c - - sh elan-init.sh -y --default-toolchain leanprover/lean4:v4.12.0 + sh elan-init.sh -y --default-toolchain leanprover/lean4:v4.34.1 rm -f elan-init.sh echo "$HOME/.elan/bin" >> $GITHUB_PATH diff --git a/proofs/lean4/PathTraversal.lean b/proofs/lean4/PathTraversal.lean index fcf4122f..25c90a64 100644 --- a/proofs/lean4/PathTraversal.lean +++ b/proofs/lean4/PathTraversal.lean @@ -99,7 +99,7 @@ theorem isPrefix_dropLast -- (since t :: ts is non-empty), so xs is still a prefix. refine ⟨(t :: ts).dropLast, ?_⟩ subst htail - rw [List.dropLast_append_of_ne_nil _ (List.cons_ne_nil t ts)] + rw [List.dropLast_append_of_ne_nil (List.cons_ne_nil t ts)] -- --------------------------------------------------------------------- -- Per-step invariant diff --git a/proofs/lean4/SymlinkOperations.lean b/proofs/lean4/SymlinkOperations.lean index c42fdd4f..f8635620 100644 --- a/proofs/lean4/SymlinkOperations.lean +++ b/proofs/lean4/SymlinkOperations.lean @@ -58,7 +58,7 @@ theorem symlink_unlink_reversible (p : Path) (fs : Filesystem) exact ⟨node, hfs⟩ · simp [h] -/-- Summary: +/- Summary: ✓ Symlink creation and removal operations ✓ Preconditions for safe symlink creation ✓ Reversibility: unlink(symlink(p, fs)) = fs diff --git a/proofs/lean4/lakefile.lean b/proofs/lean4/lakefile.lean index 7aaca912..a6b9b5d7 100644 --- a/proofs/lean4/lakefile.lean +++ b/proofs/lean4/lakefile.lean @@ -1,7 +1,13 @@ -- SPDX-License-Identifier: MPL-2.0 -- Valence Shell — Lean 4 Proof Package -- --- Last verified working: Lean 4 v4.12.0 (2026-03-10) +-- Last verified working: Lean 4 v4.34.1 (2026-10-02) +-- Builds clean: FilesystemModel, FileOperations, FilesystemComposition, +-- FilesystemEquivalence, SymlinkOperations, Extraction, CrashConsistency, +-- PathTraversal, model_oracle. +-- Do NOT build (already broken on v4.12.0, not port regressions): +-- FileContentOperations, RMOOperations, CopyMoveOperations, +-- PermissionOperations. -- Toolchain pinned in: lean-toolchain -- CI workflow: .github/workflows/lean-verification.yml -- .github/workflows/rust-cli.yml (lean4 job) diff --git a/proofs/lean4/lean-toolchain b/proofs/lean4/lean-toolchain index 89985206..ba8ebf2d 100644 --- a/proofs/lean4/lean-toolchain +++ b/proofs/lean4/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.12.0 +leanprover/lean4:v4.34.1 From d8e475bccf894bc19993218b0cb195f051fd651c Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Fri, 2 Oct 2026 13:10:46 +0100 Subject: [PATCH 2/2] fix(test): model oracle test fails instead of skipping as a pass The differential correspondence test returned early ("SKIP") when the Lean model_oracle binary was missing, so a plain `cargo test` reported it as passed with zero probes checked. A VSH_MODEL_ORACLE pointing at a non-file silently fell back to the default path. - Mark the test #[ignore] with a reason; plain `cargo test` now shows it as ignored, not passed. - When run (--ignored), a missing oracle panics; an invalid VSH_MODEL_ORACLE panics instead of falling back. - Assert sequences_run > 0 alongside checked_probes > 0 and print both. - lean-verification.yml and `just test-correspondence-model` pass --ignored. Verified: cargo test 786 passed / 0 failed / 15 ignored; with the oracle built on Lean v4.34.1, 1218 probes agreed across 196 non-empty sequences (of 200); VSH_MODEL_ORACLE=/nonexistent and a missing default oracle both fail with exit 101. Co-Authored-By: Claude Opus 5.5 --- .github/workflows/lean-verification.yml | 2 +- Justfile | 5 +- .../tests/model_oracle_correspondence.rs | 71 ++++++++++++------- 3 files changed, 48 insertions(+), 30 deletions(-) diff --git a/.github/workflows/lean-verification.yml b/.github/workflows/lean-verification.yml index 69ad23cf..fea15e58 100644 --- a/.github/workflows/lean-verification.yml +++ b/.github/workflows/lean-verification.yml @@ -117,7 +117,7 @@ jobs: - name: Differential correspondence (proven Lean model vs Rust impl) run: | cd impl/rust-cli - cargo test --test model_oracle_correspondence -- --nocapture + cargo test --test model_oracle_correspondence -- --ignored --nocapture - name: Report Rust binary size run: | diff --git a/Justfile b/Justfile index de2799f4..c801fac3 100644 --- a/Justfile +++ b/Justfile @@ -51,9 +51,10 @@ build-model-oracle: @echo "✓ model oracle -> proofs/lean4/.lake/build/bin/model_oracle" # Run the differential correspondence test (proven Lean model vs Rust impl). -# Builds the oracle first so the test does not skip. +# Builds the oracle first; the test is #[ignore]d so it needs --ignored, and +# fails (never skips) if the oracle is missing. test-correspondence-model: build-model-oracle - cd impl/rust-cli && cargo test --test model_oracle_correspondence -- --nocapture + cd impl/rust-cli && cargo test --test model_oracle_correspondence -- --ignored --nocapture # Build Agda proofs build-agda: diff --git a/impl/rust-cli/tests/model_oracle_correspondence.rs b/impl/rust-cli/tests/model_oracle_correspondence.rs index f448c8a5..aadbaee4 100644 --- a/impl/rust-cli/tests/model_oracle_correspondence.rs +++ b/impl/rust-cli/tests/model_oracle_correspondence.rs @@ -14,10 +14,14 @@ //! Any disagreement is a genuine correspondence divergence between the proven //! model and the runtime — the thing a mechanized correspondence is meant to catch. //! -//! Gating: if the oracle binary is not built, the test SKIPS (prints how to build -//! it) rather than failing, so `cargo test` stays green without a Lean toolchain. +//! Gating: the test is `#[ignore]`d, so a plain `cargo test` (no Lean toolchain) +//! reports it as IGNORED rather than passing it. Run it explicitly with +//! `--ignored`; when run, a missing or invalid oracle is a hard FAILURE, never a +//! silent skip-as-pass. //! Build it with: cd proofs/lean4 && lake build model_oracle //! or: just build-model-oracle +//! Run it with: cargo test --test model_oracle_correspondence -- --ignored +//! or: just test-correspondence-model use std::collections::BTreeMap; use std::io::Write; @@ -57,25 +61,33 @@ impl Rng { } } -/// Locate the compiled Lean model oracle. Env override wins; otherwise the -/// default lake build path relative to this crate. -fn locate_oracle() -> Option { - if let Ok(p) = std::env::var("VSH_MODEL_ORACLE") { +/// Locate the compiled Lean model oracle, panicking if it cannot be found. +/// +/// If `VSH_MODEL_ORACLE` is set it must name an existing file: an invalid value +/// panics instead of silently falling back to the default path, so a typo can +/// never cause a different (or no) oracle to be used. Otherwise the default lake +/// build path relative to this crate is used, and its absence also panics. +fn locate_oracle() -> PathBuf { + if let Some(p) = std::env::var_os("VSH_MODEL_ORACLE") { let pb = PathBuf::from(p); - if pb.is_file() { - return Some(pb); - } + assert!( + pb.is_file(), + "VSH_MODEL_ORACLE is set to {pb:?}, which is not a file. Unset it to \ + use the default lake build path, or point it at a built model_oracle." + ); + return pb; } // impl/rust-cli/tests -> repo root -> proofs/lean4/.lake/build/bin/model_oracle let manifest = PathBuf::from(env!("CARGO_MANIFEST_DIR")); - let candidate = manifest - .join("../../proofs/lean4/.lake/build/bin/model_oracle") - .canonicalize() - .ok()?; - if candidate.is_file() { - Some(candidate) - } else { - None + let default = manifest.join("../../proofs/lean4/.lake/build/bin/model_oracle"); + match default.canonicalize() { + Ok(candidate) if candidate.is_file() => candidate, + _ => panic!( + "Lean model oracle not found at {default:?}.\n\ + Build it with: cd proofs/lean4 && lake build model_oracle\n\ + or: just build-model-oracle\n\ + or set VSH_MODEL_ORACLE=/path/to/model_oracle" + ), } } @@ -236,22 +248,20 @@ fn rust_kind(root: &std::path::Path, rel: &str) -> &'static str { } } +/// Differential test: apply generated precondition-respecting op sequences to +/// the real Rust implementation and to the compiled Lean model oracle, and assert +/// both agree on the node type at every touched path. Ignored by default because +/// it needs the Lean oracle; when run, a missing oracle fails the test. #[test] +#[ignore = "needs Lean model_oracle — build with `just build-model-oracle`, run with --ignored"] fn rust_matches_proven_lean_model() { - let Some(oracle) = locate_oracle() else { - eprintln!( - "SKIP model_oracle_correspondence: Lean model oracle not built.\n\ - Build it with: cd proofs/lean4 && lake build model_oracle\n\ - or: just build-model-oracle\n\ - or set VSH_MODEL_ORACLE=/path/to/model_oracle" - ); - return; - }; + let oracle = locate_oracle(); const SEQUENCES: usize = 200; const MAX_OPS: usize = 14; let mut rng = Rng::new(20260717u64); let mut checked_probes = 0usize; + let mut sequences_run = 0usize; for seq in 0..SEQUENCES { let (ops, probes) = gen_sequence(&mut rng, MAX_OPS); @@ -279,6 +289,8 @@ fn rust_matches_proven_lean_model() { }); } + sequences_run += 1; + // Ask the proven model for the same probes. let model = oracle_query(&oracle, &ops, &probes); assert_eq!( @@ -306,11 +318,16 @@ fn rust_matches_proven_lean_model() { } } + assert!( + sequences_run > 0, + "no sequences were run — generator produced only empty sequences" + ); assert!( checked_probes > 0, "no probes were checked — generator produced only empty sequences" ); eprintln!( - "model_oracle_correspondence: {checked_probes} probes agreed across {SEQUENCES} sequences" + "model_oracle_correspondence: {checked_probes} probes agreed across \ + {sequences_run} non-empty sequences (of {SEQUENCES} generated)" ); }