WIP: saw-core-lean — SAWCore→Lean 4 backend

.github/ci.sh

@@ -179,6 +179,15 @@ bundle_files() {
   cp intTests/jars/galois.jar dist/lib
   cp -r deps/cryptol/lib/* dist/lib
   cp -r examples/* dist/examples
+
+  # saw-core-lean replay assets. The bindist binary's compiled-in
+  # Cabal datadir is never installed, so these trees must ship for
+  # `offline_lean_replay` to work from the tarball; shipping them
+  # checkout-shaped makes the unpacked root a valid SAW_LEAN_ROOT,
+  # which must be writable (replay builds inside it). Derived from
+  # git, not a hand list. Details: saw-core-lean/README.md.
+  git archive --format=tar HEAD -- saw-core-lean/lean saw-core-lean/replay \
+    | (cd dist && tar x)
 }
 
 sign() {

.github/workflows/ci.yml

@@ -11,7 +11,10 @@ on:
     tags:
       - "v?[0-9]+.[0-9]+"
       - "v?[0-9]+.[0-9]+.[0-9]+"
-    branches: [master, "release-**"]
+    # saw-core-lean is the Lean backend's integration branch: it is
+    # long-lived and merged into rather than PR'd per change, so it
+    # needs a push trigger of its own to get CI coverage.
+    branches: [master, "release-**", saw-core-lean]
   pull_request:
   schedule:
     - cron: "0 10 * * *" # 10am UTC -> 2/3am PST
@@ -202,6 +205,8 @@ jobs:
             cryptol-saw-core-tests
             crux-mir-comp-tests
             saw-core-rocq-tests
+            saw-core-lean-smoketest
+            saw-core-lean-tests
           dest: dist-tests
 
       # In the next 2 steps, we upload to different names depending on whether
@@ -751,6 +756,38 @@ jobs:
           java-version: "8"
           java-package: jdk
 
+      - name: Install Lean toolchain for lake-driven tests
+        if: "(matrix.suite == 'integration-tests' || matrix.suite == 'saw-core-lean-tests') && runner.os != 'Windows'"
+        shell: bash
+        run: |
+          # Install elan + the toolchain pinned in saw-core-lean/lean/lean-toolchain.
+          # This puts 'lake' / 'lean' on PATH for both Lean-using test paths:
+          #
+          #   - integration-tests: legacy otherTests/saw-core-lean/{negative,saw-boundary,proofs}/ harnesses
+          #     (lean-negative-test.sh, lean-proof-test.sh, test-lean.sh).
+          #
+          #   - saw-core-lean-tests: otherTests/saw-core-lean/test.sh, which
+          #     drives drivers/*, differential/*, obligations/*, saw-boundary/*,
+          #     proofs/*, and negative/* through the support harnesses.
+          #
+          # Phase A audit (2026-05-04): the Lean test harnesses FAIL LOUDLY
+          # when lake is missing, instead of silently skipping. So this
+          # install step is mandatory for both suites — without it the
+          # tests are red. Windows currently lacks the install (handled
+          # via `continue-on-error: true` for integration-tests on Windows,
+          # and saw-core-lean-tests is ubuntu-only by default); see #134
+          # for the follow-up to install elan on Windows or filter
+          # test_lean_* tests off Windows deliberately.
+          # Audit H-1 (2026-05-06): `saw-core-lean-tests` was previously
+          # gated only on integration-tests, leaving the suite either red
+          # on every CI push or silently inheriting elan from elsewhere.
+          curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
+            | sh -s -- -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
+          export PATH="$HOME/.elan/bin:$PATH"
+          # Trigger toolchain download by reading the lean-toolchain file.
+          ( cd saw-core-lean/lean && lake env lean --version )
+
       - uses: actions/cache/restore@v4
         name: Restore SMT solver result cache
         if: "matrix.suite == 'integration-tests'"
@@ -774,6 +811,28 @@ jobs:
           export PATH="$PWD/bin:$PWD/dist/bin:$PATH"
           dist-tests/${{ matrix.suite }}
 
+      # Verify the saw-lean-example demo end-to-end: rerun saw on
+      # demo.saw, then lake-build the proof/ project that consumes
+      # its emitted output. The example is a release demo
+      # (examples/saw-lean/), so silent rot here would be visible
+      # to users following the documentation. Only runs in the
+      # saw-core-lean-tests matrix because earlier jobs may not
+      # have elan/saw on PATH together.
+      - name: saw-lean-example demo
+        if: "matrix.suite == 'saw-core-lean-tests' && runner.os != 'Windows'"
+        shell: bash
+        run: |
+          export PATH="$PWD/bin:$PWD/dist/bin:$HOME/.elan/bin:$PATH"
+          # demo.saw's replay steps need the asset root: the
+          # extracted binary's compiled-in datadir is never installed.
+          export SAW_LEAN_ROOT="$PWD"
+          cd examples/saw-lean
+          saw demo.saw
+          # Build the committed Emitted copies. Refreshing them
+          # from out/ is tracked in saw-core-lean/TODO.md.
+          cd proof
+          lake build
+
       - uses: actions/cache/save@v4
         name: Save SMT solver result cache
         if: "matrix.suite == 'integration-tests'"

.gitignore

@@ -15,7 +15,20 @@ stack.yaml
 .ghc.environment*
 dist-newstyle
 cabal.project.freeze
+build.log
 *~
 *#
 .#*
 saw-core-rocq/rocq/.Makefile.rocq.d
+
+# Lean backend (saw-core-lean): build artifacts, per-test staging
+# (tests clean their own intTestsProbe/ subdirs), and local
+# AI-session bookkeeping. Deliberately NO blanket scratch-dir rules
+# (.tmp-*/ etc.) — scratch should show up in git status and get
+# dealt with, not accumulate invisibly.
+.lake/
+*.olean
+*.ilean
+saw-core-lean/lean/intTestsProbe/
+otherTests/saw-core-lean/.tier-selftest/
+.claude/

CHANGES.md

@@ -6,6 +6,19 @@ This release supports [version
 
 ## New Features
 
+* `offline_lean` is now emission-only: it writes the Lean proof
+  obligation and leaves the goal UNSOLVED, so SAW never claims a goal
+  on the strength of an export (wrap in `fails` if the script should
+  continue). The new `offline_lean_replay` command is the discharge
+  path: it re-emits the goal, checks a user-completed Lean proof
+  against it, and on success admits the goal with recorded
+  `LeanReplayEvidence`. Setup, known limitations, and the trust model
+  are in `saw-core-lean/README.md`. As part of this, LLVM verification now runs every
+  verification condition's proof tactic before failing on unfinished
+  proofs, so multi-obligation `llvm_verify` runs with offline
+  exporters emit all obligation files in one pass (invalid proofs with
+  counterexamples still abort immediately).
+
 * Add new SAWScript commands `timeout_handle` and `timeout` for adding
   time limits to scripts.
 

Makefile

@@ -5,3 +5,62 @@ tmp/TAGS: | tmp
 
 tmp:
 	mkdir -p tmp
+
+# saw-core-lean comprehensive validation — the single CI gate.
+#
+# Required for ANY change touching the Lean backend (translator,
+# support library, soundness lockdowns, drivers, proofs, etc.).
+# Exits non-zero on the first failure.
+#
+# Coverage:
+#   (1) Tests       — Haskell-side translator invariants
+#                     (L-1..L-17 lockdowns) via the smoketest.
+#   (2) Synthesis   — SAW emission for every driver in
+#                     otherTests/saw-core-lean/drivers/ and
+#                     saw-boundary/, diffed against pinned .good.
+#   (3) Proofs      — Lean discharges every goal in
+#                     otherTests/saw-core-lean/proofs/, including
+#                     llvm_verify-emitted obligations.
+#   (4) Assurance   — Hand-rolled negative-attack probes pinning
+#                     axiom signatures (shape/), and the
+#                     CryptolToLean Lean support library compiles.
+#   (5) SAW broad   — General SAW integration tests (intTests/) to
+#                     catch regressions in non-Lean SAW
+#                     infrastructure that could affect the Lean
+#                     backend transitively (e.g. Cryptol parser,
+#                     scNormalize, Crucible).
+.PHONY: test-saw-core-lean
+test-saw-core-lean:
+	@echo "=== 1/5: build SAW with current translator ==="
+	cabal build exe:saw
+	@echo "=== 2/5: build CryptolToLean support library ==="
+	( cd saw-core-lean/lean && lake build )
+	@echo "=== 3/5: Haskell-side translator invariants (smoketest) ==="
+	cabal test saw-core-lean-smoketest
+	@echo "=== 4/5: Lean-side driver/proof/shape/saw-boundary ==="
+	cabal test saw-core-lean-tests
+	@echo "=== 5/5: SAW general integration tests ==="
+	cabal test integration-tests
+	@echo
+	@echo "=== ALL SAW-CORE-LEAN VALIDATIONS PASSED ==="
+
+# saw-core-lean focused semantic conformance gate.
+#
+# This is intentionally namespaced rather than a generic `conformance`
+# target: it is a SAW-Lean backend suite, not a whole-repository
+# conformance statement.
+.PHONY: test-saw-core-lean-conformance
+test-saw-core-lean-conformance:
+	@echo "=== build SAW with current translator ==="
+	cabal build exe:saw
+	@echo "=== saw-core-lean differential conformance ==="
+	$(MAKE) -C otherTests/saw-core-lean conformance
+
+# saw-core-lean proof/stress gap inventory.
+#
+# This is intentionally separate from the conformance gate: it reports
+# preserved proof gaps and stress probes that are not accepted proof-discharge
+# examples. It does not require a built saw binary.
+.PHONY: test-saw-core-lean-gaps
+test-saw-core-lean-gaps:
+	$(MAKE) -C otherTests/saw-core-lean gaps

README.md

@@ -26,6 +26,12 @@ There is also a longer
 [manual](https://github.com/GaloisInc/saw-script/blob/master/doc/pdfs/saw-user-manual.pdf)
 that describes the breadth of SAW's features.
 
+There is an experimental backend that discharges SAW proof
+obligations in the Lean 4 kernel instead of an SMT solver; it has its
+own documentation, including known soundness limitations you should
+read before relying on it. See
+[`saw-core-lean/README.md`](saw-core-lean/README.md).
+
 ## Precompiled Binaries
 
 Precompiled SAW binaries for a variety of platforms are available

build.sh

@@ -90,7 +90,9 @@ tgt_build() {
                 test-suite:integration-tests test-suite:saw-core-tests \
                 test-suite:crux-mir-comp-tests \
                 test-suite:cryptol-saw-core-tests \
-                test-suite:saw-core-rocq-tests
+                test-suite:saw-core-rocq-tests \
+                test-suite:saw-core-lean-smoketest \
+                test-suite:saw-core-lean-tests
 
     echo "rm -rf bin && mkdir bin"
     rm -rf bin && mkdir bin

doc/developer/developer.md

@@ -151,6 +151,13 @@ The following can be run with `cabal test`:
 - `saw-core-tests`
 - `cryptol-saw-core-tests`
 - `saw-core-rocq-tests`
+- `saw-core-lean-smoketest` (unit/regression tests for the Lean 4
+  backend; needs no `saw` binary)
+- `saw-core-lean-tests` (end-to-end SAW→Lean tests under
+  `otherTests/saw-core-lean`). Some Lean-backend soundness tests
+  also run as `intTests/test_lean_soundness_*` under
+  `integration-tests`. See `saw-core-lean/doc/contributing.md` for
+  what these cover and how to add to them.
 - `crux-mir-comp-tests`
 
 There is one other set of tests:

examples/saw-lean/.gitignore

@@ -0,0 +1 @@
+out/