feat: import LeanSAT's tactic frontends

Co-authored-by: Markus Himmel <[email protected]>

.github/workflows/ci.yml

@@ -176,7 +176,7 @@ jobs:
                 "check-level": 2,
                 "CMAKE_PRESET": "debug",
                 // exclude seriously slow tests
-                "CTEST_OPTIONS": "-E 'interactivetest|leanpkgtest|laketest|benchtest'"
+                "CTEST_OPTIONS": "-E 'interactivetest|leanpkgtest|laketest|benchtest|bv_bitblast_stress'"
               },
               // TODO: suddenly started failing in CI
               /*{

CMakeLists.txt

@@ -30,31 +30,34 @@ if(NOT (DEFINED STAGE0_CMAKE_EXECUTABLE_SUFFIX))
     set(STAGE0_CMAKE_EXECUTABLE_SUFFIX "${CMAKE_EXECUTABLE_SUFFIX}")
 endif()
 
-# On CI Linux, we source cadical from Nix instead; see flake.nix
-find_program(CADICAL cadical)
-if(NOT CADICAL)
-  set(CADICAL_CXX c++)
-  find_program(CCACHE ccache)
-  if(CCACHE)
-    set(CADICAL_CXX "${CCACHE} ${CADICAL_CXX}")
-  endif()
-  # missing stdio locking API on Windows
-  if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
-    string(APPEND CADICAL_CXXFLAGS " -DNUNLOCKED")
+# Don't do anything with cadical on wasm
+if (NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
+  # On CI Linux, we source cadical from Nix instead; see flake.nix
+  find_program(CADICAL cadical)
+  if(NOT CADICAL)
+    set(CADICAL_CXX c++)
+    find_program(CCACHE ccache)
+    if(CCACHE)
+      set(CADICAL_CXX "${CCACHE} ${CADICAL_CXX}")
+    endif()
+    # missing stdio locking API on Windows
+    if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
+      string(APPEND CADICAL_CXXFLAGS " -DNUNLOCKED")
+    endif()
+    ExternalProject_add(cadical
+      PREFIX cadical
+      GIT_REPOSITORY https://github.com/arminbiere/cadical
+      GIT_TAG rel-1.9.5
+      CONFIGURE_COMMAND ""
+      # https://github.com/arminbiere/cadical/blob/master/BUILD.md#manual-build
+      BUILD_COMMAND $(MAKE) -f ${CMAKE_SOURCE_DIR}/src/cadical.mk CMAKE_EXECUTABLE_SUFFIX=${CMAKE_EXECUTABLE_SUFFIX} CXX=${CADICAL_CXX} CXXFLAGS=${CADICAL_CXXFLAGS}
+      BUILD_IN_SOURCE ON
+      INSTALL_COMMAND "")
+    set(CADICAL ${CMAKE_BINARY_DIR}/cadical/cadical${CMAKE_EXECUTABLE_SUFFIX} CACHE FILEPATH "path to cadical binary" FORCE)
+    set(EXTRA_DEPENDS "cadical")
   endif()
-  ExternalProject_add(cadical
-    PREFIX cadical
-    GIT_REPOSITORY https://github.com/arminbiere/cadical
-    GIT_TAG rel-1.9.5
-    CONFIGURE_COMMAND ""
-    # https://github.com/arminbiere/cadical/blob/master/BUILD.md#manual-build
-    BUILD_COMMAND $(MAKE) -f ${CMAKE_SOURCE_DIR}/src/cadical.mk CMAKE_EXECUTABLE_SUFFIX=${CMAKE_EXECUTABLE_SUFFIX} CXX=${CADICAL_CXX} CXXFLAGS=${CADICAL_CXXFLAGS}
-    BUILD_IN_SOURCE ON
-    INSTALL_COMMAND "")
-  set(CADICAL ${CMAKE_BINARY_DIR}/cadical/cadical${CMAKE_EXECUTABLE_SUFFIX} CACHE FILEPATH "path to cadical binary" FORCE)
-  set(EXTRA_DEPENDS "cadical")
+  list(APPEND CL_ARGS -DCADICAL=${CADICAL})
 endif()
-list(APPEND CL_ARGS -DCADICAL=${CADICAL})
 
 ExternalProject_add(stage0
   SOURCE_DIR "${LEAN_SOURCE_DIR}/stage0"

CODEOWNERS

@@ -43,3 +43,5 @@
 /src/Init/Guard.lean @digama0
 /src/Lean/Server/CodeActions/ @digama0
 /src/Std/ @TwoFX
+/src/Std/Tactic/BVDecide/ @hargoniX
+/src/Lean/Elab/Tactic/BVDecide/ @hargoniX

nix/bootstrap.nix

@@ -158,7 +158,7 @@ lib.warn "The Nix-based build is deprecated" rec {
       test = buildCMake {
         name = "lean-test-${desc}";
         realSrc = lib.sourceByRegex src [ "src.*" "tests.*" ];
-        buildInputs = [ gmp libuv perl git ];
+        buildInputs = [ gmp libuv perl git cadical ];
         preConfigure = ''
           cd src
         '';

src/CMakeLists.txt

@@ -535,6 +535,12 @@ else()
     OUTPUT_NAME leancpp)
 endif()
 
+if((${STAGE} GREATER 0) AND CADICAL)
+  add_custom_target(copy-cadical
+    COMMAND cmake -E copy_if_different "${CADICAL}" "${CMAKE_BINARY_DIR}/bin/cadical${CMAKE_EXECUTABLE_SUFFIX}")
+  add_dependencies(leancpp copy-cadical)
+endif()
+
 # MSYS2 bash usually handles Windows paths relatively well, but not when putting them in the PATH
 string(REGEX REPLACE "^([a-zA-Z]):" "/\\1" LEAN_BIN "${CMAKE_BINARY_DIR}/bin")
 
@@ -633,7 +639,7 @@ file(COPY ${LEAN_SOURCE_DIR}/bin/leanmake DESTINATION ${CMAKE_BINARY_DIR}/bin)
 
 install(DIRECTORY "${CMAKE_BINARY_DIR}/bin/" USE_SOURCE_PERMISSIONS DESTINATION bin)
 
-if (${STAGE} GREATER 0)
+if (${STAGE} GREATER 0 AND CADICAL)
   install(PROGRAMS "${CADICAL}" DESTINATION bin)
 endif()
 

src/Lean/Elab/Tactic/BVDecide.lean

@@ -6,9 +6,73 @@ Authors: Henrik Böving
 prelude
 import Lean.Elab.Tactic.BVDecide.LRAT
 import Lean.Elab.Tactic.BVDecide.External
+import Lean.Elab.Tactic.BVDecide.Frontend
 
 /-!
-This directory implements the `bv_decide` tactic as a verified bitblaster with subterm sharing.
-It makes use of proof by reflection and `ofReduceBool`, thus adding the Lean compiler to the trusted
-code base.
+This directory offers three different SAT tactics for proving goals involving `BitVec` and `Bool`:
+1. `bv_decide` takes the goal, hands it over to a SAT solver and verifies the generated LRAT
+   UNSAT proof to prove the goal.
+2. `bv_check file.lrat` can prove the same things as `bv_decide`. However instead of
+   dynamically handing the goal to a SAT solver to obtain an LRAT proof, the LRAT proof is read from
+   `file.lrat`. This allows users that do not have a SAT solver installed to verify proofs.
+3. `bv_decide?` offers a code action to turn a `bv_decide` invocation automatically into a
+   `bv_check` one.
+
+There are also some options to influence the behavior of `bv_decide` and friends:
+- `sat.solver`: the name of the SAT solver used by `bv_decide`. It goes through 3 steps to determine
+   which solver to use:
+   1. If sat.solver is set to something != "" it will use that.
+   2. If sat.solver is set to "" it will check if there is a cadical binary next to the executing
+      program. Usually that program is going to be `lean` itself and we do ship a `cadical` next to it.
+   3. If that does not succeed try to call `cadical` from PATH.
+- `sat.timeout`: The timeout for waiting for the SAT solver in seconds, default 10.
+- `sat.trimProofs`: Whether to run the trimming algorithm on LRAT proofs, default true.
+- `sat.binaryProofs`: Whether to use the binary LRAT proof format, default true.
+- `trace.Meta.Tactic.bv` and `trace.Meta.Tactic.sat` for inspecting the inner workings of `bv_decide`.
+- `debug.skipKernelTC`: may be set to true to disable actually checking the LRAT proof.
+  `bv_decide` will still run bitblasting + SAT solving so this option essentially trusts the SAT
+  solver.
+
+## Architecture
+`bv_decide` roughly runs through the following steps:
+1. Apply `false_or_by_contra` to start a proof by contradiction.
+2. Apply the `bv_normalize` and `seval` simp set to all hypotheses. This has two effects:
+    1. It applies a subset of the rewrite rules from [Bitwuzla](https://github.com/bitwuzla/bitwuzla)
+       for simplification of the expressions.
+    2. It turns all hypotheses that might be of interest for the remainder of the tactic into the form
+       `x = true` where `x` is a mixture of `Bool` and fixed width `BitVec` expressions.
+3. Use proof by reflection to reduce the proof to showing that an SMTLIB-syntax-like value that
+   represents the conjunction of all relevant assumptions is UNSAT.
+4. Use a verified bitblasting algorithm to turn that expression into an AIG.
+   The bitblasting algorithms are collected from various other bitblasters, including Bitwuzla and
+   Z3 and verified using Lean's `BitVec` theory.
+5. Turn the AIG into a CNF.
+6. Run CaDiCal on the CNF to obtain an LRAT proof that the CNF is UNSAT. If CaDiCal returns SAT
+   instead the tactic aborts here and presents a counterexample.
+7. Use an LRAT checker with a soundness proof in Lean to show that the LRAT proof is correct.
+8. Chain all the proofs so far to demonstrate that the original goal holds.
+
+## Axioms
+`bv_decide` makes use of proof by reflection and `ofReduceBool`, thus adding the Lean compiler to
+the trusted code base.
+
+
+## Adding a new primitive
+`bv_decide` knows two kinds of primitives:
+1. The ones that can be reduced to already existing ones.
+2. The ones that cannot.
+
+For the first kind the steps to adding them are very simple, go to `Std.Tactic.BVDecide.Normalize`
+and add the reduction lemma into the `bv_normalize` simp set. Don't forget to add a test!
+
+For the second kind more steps are involved:
+1. Add a new constructor to `BVExpr`/`BVPred`
+2. Add a bitblasting algorithm for the new constructor to `Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl`.
+3. Verify that algorithm in `Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas`.
+4. Integrate it with either the expression or predicate bitblaster and use the proof above to verify it.
+5. Add simplification lemmas for the primitive to `bv_normalize` in `Std.Tactic.BVDecide.Normalize`.
+   If there are mutliple ways to write the primitive (e.g. with TC based notation and without) you
+   should normalize for one notation here.
+6. Add the reflection code to `Lean.Elab.Tactic.BVDecide.Frontend.BVDecide`
+7. Add a test!
 -/

src/Lean/Elab/Tactic/BVDecide/External.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
 prelude
-import Lean.Elab.Tactic.BVDecide.LRAT.Parser
+import Std.Tactic.BVDecide.LRAT.Parser
 import Lean.CoreM
 import Std.Internal.Parsec
 
@@ -17,6 +17,8 @@ namespace Lean.Elab.Tactic.BVDecide
 
 namespace External
 
+open Std.Tactic.BVDecide
+
 /--
 The result of calling a SAT solver.
 -/
@@ -34,6 +36,7 @@ namespace ModelParser
 
 open Std.Internal.Parsec
 open Std.Internal.Parsec.ByteArray
+open LRAT.Parser.Text (skipNewline)
 
 def parsePartialAssignment : Parser (Bool × (Array (Bool × Nat))) := do
   skipByteChar 'v'
@@ -43,7 +46,7 @@ def parsePartialAssignment : Parser (Bool × (Array (Bool × Nat))) := do
     (skipString " 0")
     (csuccess := fun _ => pure (true, idents))
     (cerror := fun _ => do
-      skipByteChar '\n'
+      skipNewline
       return (false, idents)
     )
 where
@@ -65,7 +68,8 @@ where
 
 @[inline]
 def parseHeader : Parser Unit := do
-  skipString "s SATISFIABLE\n"
+  skipString "s SATISFIABLE"
+  skipNewline
 
 /--
 Parse the witness format of a SAT solver. The rough grammar for this is:
@@ -81,82 +85,107 @@ end ModelParser
 
 open Lean (CoreM)
 
+inductive TimedOut (α : Type u) where
+  | success (x : α)
+  | timeout
+
 /--
-Run a process with `args` until it terminates or the cancellation token in `CoreM` tells us to abort.
+Run a process with `args` until it terminates or the cancellation token in `CoreM` tells us to abort
+or `timeout` seconds have passed.
 -/
-partial def runInterruptible (args : IO.Process.SpawnArgs) : CoreM IO.Process.Output := do
+partial def runInterruptible (timeout : Nat) (args : IO.Process.SpawnArgs) :
+    CoreM (TimedOut IO.Process.Output) := do
   let child ← IO.Process.spawn { args with stdout := .piped, stderr := .piped, stdin := .null }
   let stdout ← IO.asTask child.stdout.readToEnd Task.Priority.dedicated
   let stderr ← IO.asTask child.stderr.readToEnd Task.Priority.dedicated
-  if let some tk := (← read).cancelTk? then
-    go child stdout stderr tk
-  else
-    let stdout ← IO.ofExcept stdout.get
-    let stderr ← IO.ofExcept stderr.get
-    let exitCode ← child.wait
-    return { exitCode := exitCode, stdout := stdout, stderr := stderr }
+  go (timeout * 1000) child stdout stderr
 where
-  go {cfg} (child : IO.Process.Child cfg) (stdout stderr : Task (Except IO.Error String))
-      (tk : IO.CancelToken) : CoreM IO.Process.Output := do
-    withInterruptCheck tk child.kill do
+  go {cfg} (budgetMs : Nat) (child : IO.Process.Child cfg) (stdout stderr : Task (Except IO.Error String)) :
+      CoreM (TimedOut IO.Process.Output) := do
+    let cleanup := killAndWait child
+    withTimeoutCheck budgetMs cleanup do
+    withInterruptCheck cleanup do
       match ← child.tryWait with
       | some exitCode =>
         let stdout ← IO.ofExcept stdout.get
         let stderr ← IO.ofExcept stderr.get
-        return { exitCode := exitCode, stdout := stdout, stderr := stderr }
+        return .success { exitCode := exitCode, stdout := stdout, stderr := stderr }
       | none =>
-        IO.sleep 50
-        go child stdout stderr tk
-
-  withInterruptCheck {α : Type} (tk : IO.CancelToken) (interrupted : CoreM Unit) (x : CoreM α) :
-      CoreM α := do
-    if ← tk.isSet then
-      interrupted
-      throw <| .internal Core.interruptExceptionId
+        let sleepMs : Nat := 50
+        IO.sleep sleepMs.toUInt32
+        go (budgetMs - sleepMs) child stdout stderr
+
+  killAndWait {cfg} (child : IO.Process.Child cfg) : IO Unit := do
+    child.kill
+    discard child.wait
+
+  withTimeoutCheck {α : Type} (budgetMs : Nat) (cleanup : CoreM Unit) (x : CoreM (TimedOut α)) :
+      CoreM (TimedOut α) := do
+    if budgetMs == 0 then
+      cleanup
+      return .timeout
     else
       x
 
+  withInterruptCheck {α : Type} (cleanup : CoreM Unit) (x : CoreM α) :
+      CoreM α := do
+    if let some tk := (← read).cancelTk? then
+      if ← tk.isSet then
+        cleanup
+        throw <| .internal Core.interruptExceptionId
+    x
+
 /--
 Call the SAT solver in `solverPath` with `problemPath` as CNF input and ask it to output an LRAT
 UNSAT proof (binary or non-binary depending on `binaryProofs`) into `proofOutput`. To avoid runaway
 solvers the solver is run with `timeout` in seconds as a maximum time limit to solve the problem.
 
 Note: This function currently assume that the solver has the same CLI as CaDiCal.
 -/
-def satQuery (solverPath : String) (problemPath : System.FilePath) (proofOutput : System.FilePath)
-    (timeout : Nat := 10) (binaryProofs : Bool := true) :
+def satQuery (solverPath : System.FilePath) (problemPath : System.FilePath) (proofOutput : System.FilePath)
+    (timeout : Nat) (binaryProofs : Bool) :
     CoreM SolverResult := do
-  let cmd := solverPath
-  let args := #[
+  let cmd := solverPath.toString
+  let mut args := #[
     problemPath.toString,
     proofOutput.toString,
-    "-t",
-    s!"{timeout}",
     "--lrat",
     s!"--binary={binaryProofs}",
     "--quiet",
-    "--unsat" -- This sets the magic parameters of cadical to optimize for UNSAT search.
+    /-
+    This sets the magic parameters of cadical to optimize for UNSAT search.
+    Given the fact that we are mostly interested in proving things and expect user goals to be
+    provable this is a fine value to set
+    -/
+    "--unsat",
+    /-
+    Bitwuzla sets this option and it does improve performance practically:
+    https://github.com/bitwuzla/bitwuzla/blob/0e81e616af4d4421729884f01928b194c3536c76/src/sat/cadical.cpp#L34
+    -/
+    "--shrink=0"
   ]
 
-  let out ← runInterruptible { cmd, args, stdin := .piped, stdout := .piped, stderr := .null }
-  if out.exitCode == 255 then
-    throwError s!"Failed to execute external prover:\n{out.stderr}"
-  else
-    let stdout := out.stdout
-    if stdout.startsWith "s UNSATISFIABLE" then
-      return .unsat
-    else if stdout.startsWith "s SATISFIABLE" then
-      match ModelParser.parse.run stdout.toUTF8 with
-      | .ok assignment =>
-        return .sat assignment
-      | .error err =>
-        throwError s!"Error {err} while parsing:\n{stdout}"
-    else if stdout.startsWith "c UNKNOWN" then
-      let mut err := "The SAT solver timed out while solving the problem."
-      err := err ++ "\nConsider increasing the timeout with `set_option sat.timeout <sec>`"
-      throwError err
+  -- We implement timeouting ourselves because cadicals -t option is not available on Windows.
+  let out? ← runInterruptible timeout { cmd, args, stdin := .piped, stdout := .piped, stderr := .null }
+  match out? with
+  | .timeout =>
+    let mut err := "The SAT solver timed out while solving the problem."
+    err := err ++ "\nConsider increasing the timeout with `set_option sat.timeout <sec>`"
+    throwError err
+  | .success { exitCode := exitCode, stdout := stdout, stderr := stderr} =>
+    if exitCode == 255 then
+      throwError s!"Failed to execute external prover:\n{stderr}"
     else
-      throwError s!"The external prover produced unexpected output:\n{stdout}"
+      if stdout.startsWith "s UNSATISFIABLE" then
+        return .unsat
+      else if stdout.startsWith "s SATISFIABLE" then
+        match ModelParser.parse.run stdout.toUTF8 with
+        | .ok assignment =>
+          return .sat assignment
+        | .error err =>
+          throwError s!"Error {err} while parsing:\n{stdout}"
+      else
+        throwError s!"The external prover produced unexpected output, stdout:\n{stdout}stderr:\n{stderr}"
 
 end External
 

src/Lean/Elab/Tactic/BVDecide/Frontend.lean

@@ -0,0 +1,19 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+prelude
+import Lean.Elab.Tactic.BVDecide.Frontend.Attr
+import Lean.Elab.Tactic.BVDecide.Frontend.BVCheck
+import Lean.Elab.Tactic.BVDecide.Frontend.BVDecide
+import Lean.Elab.Tactic.BVDecide.Frontend.BVTrace
+import Lean.Elab.Tactic.BVDecide.Frontend.LRAT
+import Lean.Elab.Tactic.BVDecide.Frontend.Normalize
+
+/-!
+This module provides the tactic frontends, consisting of:
+- `bv_decide`, the bitblasting based `BitVec` decision procedure itself.
+- `bv_check`, like `bv_decide` but the LRAT proof is provided as a file so no need to call a SAT solver.
+- `bv_decide?`, converts `bv_decide?` into `bv_check` calls.
+-/