chore(lean4): bump toolchain v4.12.0 -> v4.34.1 (P0-3)

[hyperpolymath]

ULTRAPLAN P0-3 — Lean toolchain v4.12.0 → v4.34.1 (D9: latest stable on 2026-10-02).

Build matrix (every lib built explicitly with lake build <lib>; baseline from a clean git archive of 4401867)

Lib	v4.12.0 (main)	v4.34.1 before fix	v4.34.1 after
FilesystemModel, FileOperations, FilesystemComposition, FilesystemEquivalence, Extraction, CrashConsistency, model_oracle	✅	✅	✅
PathTraversal	✅	1 error	✅
SymlinkOperations	1 error	1 error	✅
CopyMoveOperations	16 errors	16	16
RMOOperations	5 errors	8	8
FileContentOperations	5 errors	3	3
PermissionOperations	4 errors	4	4

Changes

• lean-toolchain → leanprover/lean4:v4.34.1; rust-cli.yml --default-toolchain to match (the only build-relevant v4.12 pin; lean-verification.yml reads lean-toolchain).
• PathTraversal.lean:102 — List.dropLast_append_of_ne_nil lost its explicit list argument. The only real v4.34 regression; the theorem statement is unchanged.
• SymlinkOperations.lean:61 — trailing /-- Summary -/ doc comment with no declaration was a parse error on v4.12.0 too, so its 3 theorems never checked; now a plain comment, and they check.
• lakefile header: last verified v4.34.1, and it now names the four libs that do not build instead of implying the package builds.

Theorems (grep) 111 → 111 · sorry 0 → 0 · no axiom · no set_option escapes · default targets unchanged.

⚠ Status correction this PR surfaces (not fixed here)

46 of the 111 theorems live in four libs that have never built: CopyMoveOperations (11), RMOOperations (14), FileContentOperations (13), PermissionOperations (8). Under the five-status taxonomy they are DESIGNED, not PROVEN. CI never noticed because it builds only the default target, Extraction and model_oracle. CopyMove opens namespaces that do not exist (Valence.Filesystem, Valence.FileOps), and RMO cites a lemma that does not exist (deleteFile_preserves_other_paths). Repairing them is real proof work → Phase 1 (V1) / P1-0 claims ledger. Same for CLAUDE.md's "101 theorems" (grep: 111).

Logs: llm-coding-configs/claude/20261002-vsh-lean434/ on the dev machine (v412-*, before-*, after-*).

Stacked on top: P0-4 (oracle no-skip-as-pass).

🤖 Generated with Claude Code

https://claude.ai/code/session_01VxcAoyMQe7CjQwCKL18Mm4

[coderabbitai]

Navigate logical layers of code changes, visualize relationships, and explore their blast radius.

Note

Currently processing new changes in this PR. This may take a few minutes, please wait...

⚙️ Run configuration

Configuration used: Organization UI

Review profile: ASSERTIVE

Plan: Advanced

Run ID: 8b4bb799-c62f-43ec-8b92-5a891c971448

📥 Commits

Reviewing files that changed from the base of the PR and between 4401867 and 996b7b7.

📒 Files selected for processing (5)

• .github/workflows/rust-cli.yml
• proofs/lean4/PathTraversal.lean
• proofs/lean4/SymlinkOperations.lean
• proofs/lean4/lakefile.lean
• proofs/lean4/lean-toolchain

 ___________________________________________________________
< Ultimately, we're all just debugging someone else's code. >
 -----------------------------------------------------------
  \
   \   \
        \ /\
        ( )
      .( o ).

• Autopilot · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

Autopilot is currently an internal CodeRabbit preview.

---

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands.}

[github-actions]

🔍 Hypatia Security Scan

Findings: 120 issues detected

Severity	Count
🔴 Critical	9
🟠 High	28
🟡 Medium	83

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Job `triage` in label-triage.yml has no `timeout-minutes:` declaration. Default is 6 hours — a stuck codeload fetch or runner hang can burn budget. Add `timeout-minutes: 10` (or proportional).",
    "type": "missing_timeout_minutes",
    "file": ".github/workflows/label-triage.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium",
    "recipe_id": "recipe-add-workflow-timeout-minutes",
    "job": "triage"
  },
  {
    "reason": "Job `sync` in labels.yml has no `timeout-minutes:` declaration. Default is 6 hours — a stuck codeload fetch or runner hang can burn budget. Add `timeout-minutes: 10` (or proportional).",
    "type": "missing_timeout_minutes",
    "file": ".github/workflows/labels.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium",
    "recipe_id": "recipe-add-workflow-timeout-minutes",
    "job": "sync"
  },
  {
    "line": 38,
    "reason": "job in .github/workflows/labels.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/labels.yml",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium"
  },
  {
    "line": 44,
    "reason": "job in .github/workflows/push-email-notify.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/push-email-notify.yml",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium"
  },
  {
    "line": 46,
    "reason": "job in .github/workflows/cflite_batch.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/cflite_batch.yml",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium"
  },
  {
    "line": 45,
    "reason": "job in .github/workflows/cflite_pr.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/cflite_pr.yml",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium"
  },
  {
    "line": 20,
    "reason": "job in .github/workflows/instant-sync.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/instant-sync.yml",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium"
  },
  {
    "line": 83,
    "reason": "job in .github/workflows/hypatia-scan.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/hypatia-scan.yml",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium"
  },
  {
    "line": 52,
    "reason": "job in .github/workflows/label-triage.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/label-triage.yml",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium"
  },
  {
    "line": 88,
    "reason": "workflow .github/workflows/compilation_tests.yml:88 step `Run ignored tests (stress)` swallows non-zero exit via `continue-on-error: true` — failures will be masked",
    "type": "RE005",
    "file": ".github/workflows/compilation_tests.yml",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence