Verify Crab's inferred invariants with Lean

CMakeLists.txt

@@ -57,6 +57,7 @@ add_executable(crabber
   src/crabir_builder.cpp
   src/analyzer.cpp
   src/json_export.cpp
+  src/lean_verify.cpp
   src/domains/boxes_domain.cpp
   src/domains/dis_interval_domain.cpp    
   src/domains/interval_domain.cpp
@@ -68,6 +69,44 @@ add_executable(crabber
   src/domains/zones_domain.cpp
 )
 target_link_libraries(crabber PRIVATE ${CRAB_LIBS})
+
+# --verify-with-lean: after the analysis, ask the Lean development in lean/ to
+# prove the exported invariants sound.
+#
+# Configure-time rather than a runtime flag, for two reasons. It means the
+# option exists only in a build that can actually honour it -- in particular the
+# wasm build, which has no toolchain to call, does not carry code for a
+# capability a browser cannot have. And it removes any need to discover lake or
+# the project directory at run time.
+set(LAKE_EXECUTABLE "" CACHE FILEPATH
+    "Path to lake. Enables crabber's --verify-with-lean option.")
+
+if (LAKE_EXECUTABLE)
+  if (NOT EXISTS "${LAKE_EXECUTABLE}")
+    message(FATAL_ERROR "LAKE_EXECUTABLE does not exist: ${LAKE_EXECUTABLE}")
+  endif()
+
+  # Build the Lean library as part of the normal build. Knowing where lake lives
+  # is not the same as the library having been built, and a crabber that can
+  # find lake but meets missing .olean files reports a confusing failure that
+  # looks nothing like a proof not going through.
+  add_custom_target(lean_library ALL
+    COMMAND "${LAKE_EXECUTABLE}" build
+    WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}/lean"
+    COMMENT "Building the Lean verification library")
+  add_dependencies(crabber lean_library)
+
+  target_compile_definitions(crabber PRIVATE
+    CRABBER_WITH_LEAN=1
+    CRABBER_LAKE="${LAKE_EXECUTABLE}"
+    CRABBER_LEAN_PROJECT="${CMAKE_CURRENT_SOURCE_DIR}/lean")
+
+  message(STATUS "Lean verification enabled: ${LAKE_EXECUTABLE}")
+else ()
+  message(STATUS "Lean verification disabled "
+                 "(set -DLAKE_EXECUTABLE=$(which lake) to enable)")
+endif()
+
 install(TARGETS crabber DESTINATION bin)
 install(DIRECTORY include/crabber DESTINATION include)
 

README.md

@@ -279,3 +279,139 @@ TestResult run_program(std::istream &is,
 
 ```
 
+# Verifying the analysis with Lean #
+
+Abstract interpretation is sound *by construction*: the theory guarantees that
+the computed invariants over-approximate the reachable states — provided the
+domains, their transfer functions, and the fixpoint engine are implemented
+correctly. That proviso carries most of the weight. An abstract domain is
+thousands of lines of C++, and a bug in a join, a widening, or a single transfer
+function yields an invariant that is unsound while looking entirely ordinary.
+Soundness in theory says nothing about *this* run of *this* implementation.
+
+`--verify-with-lean` checks that run. Crabber exports the analyzed CFG together
+with the inferred invariants as JSON, and a Lean 4 development in
+[`lean/`](lean/) reads that document and tries to prove the results sound — so
+an implementation bug surfaces as a failed proof rather than as a wrong answer
+nobody notices.
+
+``` bash
+crabber samples/test-1.crabir -d int --verify-with-lean
+```
+
+``` 
+### LEAN VERIFICATION ###
+could not verify  foo : omega could not prove the goal:
+proved            bar : invariants sound, all assertions proved
+```
+
+Enabled at configure time:
+
+``` bash
+cmake -DLAKE_EXECUTABLE=$(which lake) ../
+```
+
+## What "proved" means ##
+
+For that CFG, Lean's kernel has accepted a proof of two things:
+
+- every state the program can reach at a block satisfies the invariant Crab
+  printed for that block, under the concrete semantics of CrabIR;
+- no execution can reach an assertion whose condition is false.
+
+Crucially, **nothing about Crab is modelled**. The fixpoint engine, widening,
+and the abstract domains are not formalized — only Crab's *output* is checked,
+per program. That is what makes the result independent of which domain produced
+it, and what keeps the proof effort bounded.
+
+## Which CFGs are checked ##
+
+A file may hold several CFGs, and only the **roots of the call graph** — those
+nothing calls — are checked. A CFG that is called is reported as `not checked`
+rather than passed over silently.
+
+The reason is that a callee's invariants are not properties of the callee. Crab's
+top-down inter-procedural analysis derives them from the call sites, so in
+
+```
+main() { ... inc(7) ... }      inc(a) { ... }
+```
+
+Crab may infer `a >= 5` at `inc`'s entry — true only because of how `main` calls
+it. The theorem Lean proves quantifies over *every* initial state, which is a
+strictly stronger claim than Crab made. Checking `inc` in isolation would ask a
+question Crab never answered, and fail for a reason that says nothing about the
+analysis.
+
+Verifying the conditional claim Crab actually made needs the calling context
+modelled, which is future work. Until then the check stays where the two
+questions coincide.
+
+## Which statements are modelled ##
+
+The Lean semantics covers the integer core and the whole boolean fragment:
+
+| Modelled | |
+|---|---|
+| `assign`, `havoc`, `assume`, `assert` | Integers are unbounded `Int`, not machine words — measured against the analyser, `x:i8 := 127; x := x+1` yields 128. An `assert` is check-then-assume. |
+| `bool_assign_cst`, `bool_assign_var`, `bool_binop`, `bool_assume`, `bool_assert`, `bool_select` | Booleans live in their own store, as `Bool` rather than as 0/1 integers. Crab exports boolean facts as `b = 1`; the reader turns those back into boolean claims. |
+
+| Not modelled — refused by name, so a CFG using one is reported `not attempted` | |
+|---|---|
+| `binop`, `select`, `cast` | Multiplication and division of variables are outside what `omega` decides, and Crab's four division operators differ in rounding. `cast` is why `samples/test-6.crabir` cannot be checked despite being a boolean program; `samples/test-bool-1.crabir` is the cast-free equivalent. |
+| `callsite` | Needs a call rule and the interprocedural summaries — see above. |
+| the four array statements, and the reference/region family | Need select/store reasoning in the assertion language. |
+
+Nothing is ever silently skipped: dropping a statement would weaken every proof
+obligation in its block, so an unmodelled construct fails the read and names
+itself in the report.
+
+## What is trusted, and what is not ##
+
+The point of the exercise is that the list of trusted things is short and
+explicit.
+
+| Trusted — a bug here could certify a false invariant | |
+|---|---|
+| The Lean model of CrabIR's semantics | The substantive one. It *is* the claim about what a CrabIR program means; nothing can prove it right. |
+| The exporter | Crab's rendering of an abstract state as linear constraints, and crabber's JSON around it. |
+| The JSON reader on the Lean side | Mitigated: it writes what it read back out and compares against the input, so a dropped statement or misread coefficient is reported rather than believed. |
+| Crabber's own report | Printing "proved" only says crabber ran Lean and Lean agreed. To rely on it, run `lake build` in `lean/` yourself. |
+
+| Not trusted — proved, or checked by the kernel | |
+|---|---|
+| The verification conditions and the weakest-precondition calculus | Proved sound once, for all programs. |
+| The soundness meta-theorem and assertion safety | Proved once. |
+| Every per-program proof | Found by tactics, then checked by Lean's kernel. A tactic can fail to find a proof; it cannot produce a wrong one. |
+
+## Reading a negative result ##
+
+`could not verify` is a statement about the proof attempt, **not** about Crab.
+It may mean the invariant is genuinely not inductive — or only that the proof
+search was too weak, or that the program contains an assertion Crab itself could
+not establish. The check is sound but incomplete, and its output is worded to
+keep that distinction visible.
+
+When the arithmetic is what ran out, the report also shows the assignment it
+could not rule out, in the program's own variables:
+
+```
+could not verify  octagons : omega could not prove the goal
+  cannot rule out : 101 ≤ y ≤ 200
+```
+
+That is **not** a counterexample to the invariant — the state may well be
+unreachable. It says where the reasoning stopped, which is usually the quickest
+way to see whether a fact is missing or the invariant is genuinely too weak.
+
+To investigate further, keep the intermediate files and ask for Lean's full
+output:
+
+``` bash
+crabber samples/test-2.crabir --verify-with-lean --lean-keep-temp --lean-show-output
+```
+
+This reports the exported JSON, the generated Lean file, and the exact command
+that re-runs it. That file is all Lean was given, so it can be opened in an
+editor, its tactics taken apart, and the failing goal inspected directly.
+

include/crabber/lean_verify.hpp

@@ -0,0 +1,135 @@
+#pragma once
+/**
+ * Ask the Lean development to prove the exported invariants sound.
+ *
+ * `--print-invariants-to-json` writes a document holding the analyzed CFG and,
+ * for every block, the invariant Crab inferred for it. That document is the
+ * only thing that crosses between the two sides: this code writes it, Lean
+ * reads it, and nothing about the program travels any other way.
+ *
+ * What happens per CFG is that a two-line Lean file is written,
+ *
+ *     crab_program "<absolute path to the document>" cfg "<name>"
+ *     crab_verify
+ *
+ * and checked with `lake env lean`. The first line reads the document while the
+ * file is being elaborated and installs the program and the invariants as Lean
+ * data; the second generates the proof obligations and discharges them. Success
+ * means Lean's kernel accepted a proof that every reachable state satisfies the
+ * invariant Crab printed for its block, and that no assertion can fail.
+ *
+ * What this does *not* do is make crabber's report trustworthy on its own.
+ * Printing "proved" only says Lean was run and agreed; a bug here could print
+ * it without running anything. The claim rests on the Lean development, and
+ * anyone who wants to rely on it should run `lake build` themselves.
+ *
+ * Nor is a failure evidence that Crab is wrong. Lean's arithmetic may simply be
+ * too weak, the program may use constructs the Lean semantics does not model,
+ * or an assertion may be one Crab itself could not prove. The verdicts below
+ * keep those apart, and the wording of each is chosen so that a negative result
+ * never reads as a claim about Crab.
+ *
+ * Available only when the build was configured with a path to `lake` (see
+ * `LAKE_EXECUTABLE` in CMakeLists.txt). Without it `leanAvailable()` is false
+ * and the option reports how to enable it.
+ */
+
+#include <string>
+#include <vector>
+
+namespace crabber {
+
+class CrabIrBuilder;
+
+struct LeanVerifyOpts {
+  /** Run the check after the analysis. */
+  bool enabled = false;
+  /**
+   * Elaboration budget, as Lean heartbeats rather than seconds.
+   *
+   * A wall-clock timeout would make the outcome depend on how loaded the
+   * machine is, so the same program could verify on one run and "fail" on the
+   * next. Heartbeats are deterministic, and exhausting them is reported by Lean
+   * as an ordinary diagnostic, which is why `Exhausted` can be told apart from
+   * a proof that genuinely did not go through.
+   */
+  unsigned heartbeats = 400000;
+  /**
+   * Keep the exported JSON and the generated Lean file, and report where they
+   * are.
+   *
+   * This is the whole debugging story for a CFG that does not go through. The
+   * two files are exactly what Lean saw, so re-running the printed command
+   * reproduces the failure with nothing in between -- and the Lean file can
+   * then be edited, its tactics taken apart, and the failing goal inspected in
+   * an editor.
+   */
+  bool keep_temp = false;
+  /** Print Lean's complete output for a CFG that was not proved. */
+  bool show_output = false;
+};
+
+enum class LeanVerdict {
+  /** Lean proved the invariants sound and every assertion unfailable. */
+  Proved,
+  /** The program uses a construct the Lean semantics does not model. */
+  OutOfScope,
+  /** Lean did not find a proof. Not a claim that Crab is wrong. */
+  Unproved,
+  /** The elaboration budget ran out before Lean finished. */
+  Exhausted,
+  /**
+   * Not a root of the call graph, so not checked.
+   *
+   * Reported rather than passed over in silence: a CFG present in the file and
+   * absent from the results would otherwise look like an oversight.
+   */
+  Skipped,
+};
+
+struct LeanResult {
+  std::string cfg_name;
+  LeanVerdict verdict;
+  /** Lean's own first line of output, kept for the unproved cases. */
+  std::string detail;
+  /** Everything Lean printed. Empty when it printed nothing. */
+  std::string output;
+  /**
+   * The counterexample the arithmetic decision procedure reported, if it did,
+   * rewritten in terms of the program's own variables.
+   *
+   * Not a counterexample to the invariant: it describes an assignment the proof
+   * search could not rule out, which may well be unreachable. It is a pointer to
+   * where the reasoning ran out, and usually the fastest way to see whether the
+   * gap is a missing fact or a genuinely weak invariant.
+   */
+  std::string counterexample;
+  /** Where the generated Lean file was left, when it was kept. */
+  std::string lean_file;
+};
+
+/** Whether this build can call Lean at all. */
+bool leanAvailable();
+
+/** The Lean development this build was configured against. */
+std::string leanProjectDir();
+
+/** The command that re-runs one kept Lean file by hand. */
+std::string leanReproduceCommand(const std::string &leanFile);
+
+/** Why not, when it cannot -- suitable for showing to a user. */
+std::string leanUnavailableReason();
+
+/**
+ * Check every CFG in `jsonPath`, which must be a document written by
+ * `--print-invariants-to-json`. One result per CFG, in the order the call graph
+ * gives them.
+ */
+std::vector<LeanResult> verifyWithLean(const std::string &jsonPath,
+                                       const CrabIrBuilder &crabIR,
+                                       const LeanVerifyOpts &opts);
+
+/** One line describing a result, for the report. */
+std::string describe(const LeanResult &r);
+
+} // namespace crabber

lean/.gitignore

@@ -0,0 +1,10 @@
+# Lake build artifacts: .olean/.ilean/.c outputs, and any fetched dependencies
+# under .lake/packages. Entirely regenerated by `lake build`.
+/.lake/
+
+# Scratch analyses, written here when sweeping crabber over the samples:
+#   crabber <file>.crabir -d <domain> --print-invariants-to-json lean/exports/<file>.json
+# Regenerable, and committing them would only invite drift from the exporter.
+# The one document a build actually needs is a fixture, and lives next to the
+# sample that reads it, under CrabberJson/Samples/.
+/exports/