feat: import LeanSAT LRAT (#5074)

This PR imports LeanSAT's LRAT module as step 4/~6 (step 7 could go
after I did some refactorings to import this) of the LeanSAT
upstreaming. It is the last large component, after this only the LRAT
parser and the reflection tactic that hooks everything up to the meta
level remains. In particular it is the last component that contains
notable proofs, yay!

Again a few remarks:
1. Why is this not in `Std`? I'm not quite sure whether it should be
there. At the current level of code/proof quality we can certainly not
import the checker itself into `Std` but maybe having the data type as
well as the trimming algorithm there might be of interested? I'm hoping
that as we refactor the checker in the future its quality will be high
enough to be also put into `Std`. At this point we would have a full AIG
-> CNF -> LRAT verification pipeline in `Std` for everyone to use. One
additional blocker in this is that we cannot provide the parsers for the
format in `Std` as of today because `Parsec` is still in `Lean` so that
would also have to change.
2. There do exist two abstraction levels to make sure we can swap out
the LRAT implementation at any time:
- The public interface is just all files in the top level `LRAT`
directory. It basically only contains the LRAT format itself, the
checker + soundness proof and the trimming algorithm. As long as we
don't need to change their API (which we shouldn't have to I think) we
can always swap out the entire `Internal` directory without breaking
anything else in LeanSAT.
- The `Internal` module itself contains another layer of abstraction in
the form of the `Formula` class. This allows us to swap out the most
complex component in `Internal` as well, without having to touch any of
the infrastructure that is built around it either.
3. I mostly performed stylistic cleanups on the `Internal` module. In my
experience over upgrading to many nightlies during the course of LeanSAT
development, I have gotten these proofs cleaned up to the point, where
they only break if we change the `List` or `Array` proof API
significantly. Given that we are currently in the process of stabilizing
it I'm hoping that these proofs do not have to be touched anymore unless
we do something crazy. All of the custom theory that the LRAT component
developed around various basic data types has been upstreamed into Lean
over the course of various other PRs.
4. If there are some simple tricks that we can pull off to increase the
code / proof quality in `Internal` and in particular `Internal.Formula`
(this module is not for the light-hearted Lean reviewer) I'm all for it.
Otherwise the best course of action to provide LeanSAT to our users soon
would probably be to merge it as is and do a cut + rewrite at one of the
two interface points described above.

src/Lean/Elab/Tactic/BVDecide.lean

@@ -5,6 +5,7 @@ Authors: Henrik Böving
 -/
 prelude
 import Lean.Elab.Tactic.BVDecide.Bitblast
+import Lean.Elab.Tactic.BVDecide.LRAT
 
 /-!
 This directory implements the `bv_decide` tactic as a verified bitblaster with subterm sharing.

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

@@ -0,0 +1,14 @@
+/-
+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.LRAT.Actions
+import Lean.Elab.Tactic.BVDecide.LRAT.Checker
+import Lean.Elab.Tactic.BVDecide.LRAT.Trim
+
+/-!
+This directory contains the implementation of the LRAT certificate checking and the LRAT trimming
+algorithm.
+-/

src/Lean/Elab/Tactic/BVDecide/LRAT/Actions.lean

@@ -0,0 +1,45 @@
+/-
+Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Josh Clune
+-/
+prelude
+import Std.Sat.CNF
+
+/-!
+This module contains the definition of the LRAT format (https://www.cs.utexas.edu/~marijn/publications/lrat.pdf)
+as a type `Action`, that is polymorphic over the variables used in the CNF. The type
+`IntAction := Action (Array Int) Nat` is the version that is used by the checker as input and should
+be considered the parsing target for LRAT proofs.
+-/
+
+namespace Lean.Elab.Tactic.BVDecide
+namespace LRAT
+
+open Std.Sat
+
+/-- `β` is for the type of a clause, `α` is for the type of variables -/
+inductive Action (β : Type u) (α : Type v)
+  | addEmpty (id : Nat) (rupHints : Array Nat)
+  | addRup (id : Nat) (c : β) (rupHints : Array Nat)
+  | addRat (id : Nat) (c : β) (pivot : Literal α) (rupHints : Array Nat) (ratHints : Array (Nat × Array (Nat)))
+  | del (ids : Array Nat)
+deriving Inhabited, BEq, Repr
+
+def Action.toString [ToString β] [ToString α] : Action β α → String
+  | .addEmpty id rup => s!"addEmpty (id: {id}) (hints: {rup})"
+  | .addRup id c rup => s!"addRup {c} (id : {id}) (hints: {rup})"
+  | .addRat id c l rup rat => s!"addRat {c} (id: {id}) (pivot: {l}) (rup hints: {rup}) (rat hints: {rat})"
+  | .del ids => s!"del {ids}"
+
+instance [ToString β] [ToString α] : ToString (Action β α) := ⟨Action.toString⟩
+
+/--
+`Action` where variables are (positive) `Nat`, clauses are arrays of `Int`, and ids are `Nat`.
+This Action type is meant to be a convenient target for parsing LRAT proofs.
+-/
+abbrev IntAction : Type := Action (Array Int) Nat
+
+
+end LRAT
+end Lean.Elab.Tactic.BVDecide

src/Lean/Elab/Tactic/BVDecide/LRAT/Checker.lean

@@ -0,0 +1,84 @@
+/-
+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.LRAT.Actions
+import Lean.Elab.Tactic.BVDecide.LRAT.Internal.Convert
+import Lean.Elab.Tactic.BVDecide.LRAT.Internal.LRATChecker
+import Lean.Elab.Tactic.BVDecide.LRAT.Internal.LRATCheckerSound
+import Std.Sat.CNF
+
+/-!
+This module contains the implementation of the LRAT checker as well as a proof that the given
+CNF is unsat if the checker succeeds.
+-/
+
+open Std.Sat
+
+namespace Lean.Elab.Tactic.BVDecide
+namespace LRAT
+
+open Lean.Elab.Tactic.BVDecide.LRAT.Internal in
+/--
+Check whether `lratProof` is a valid LRAT certificate for the unsatisfiability of `cnf`.
+-/
+def check (lratProof : Array IntAction) (cnf : CNF Nat) : Bool :=
+  let internalFormula := CNF.convertLRAT cnf
+  let lratProof := lratProof.toList
+  let lratProof := lratProof.map (intActionToDefaultClauseAction _)
+  let lratProof :=
+    lratProof.filterMap
+      (fun actOpt =>
+        match actOpt with
+        | none => none
+        | some (LRAT.Action.addEmpty id rupHints) => some (LRAT.Action.addEmpty id rupHints)
+        | some (LRAT.Action.addRup id c rupHints) => some (LRAT.Action.addRup id c rupHints)
+        | some (LRAT.Action.del ids) => some (LRAT.Action.del ids)
+        | some (LRAT.Action.addRat id c pivot rupHints ratHints) =>
+          if pivot ∈ Clause.toList c then
+            some (LRAT.Action.addRat id c pivot rupHints ratHints)
+          else
+            none
+      )
+  let checkerResult := lratChecker internalFormula lratProof
+  checkerResult = .success
+
+open Lean.Elab.Tactic.BVDecide.LRAT.Internal in
+/--
+If the `check` functions succeeds on `lratProof` and `cnf` then the `cnf` is unsatisfiable.
+-/
+theorem check_sound (lratProof : Array IntAction) (cnf : CNF Nat) :
+    check lratProof cnf → cnf.Unsat := by
+  intro h1
+  unfold check at h1
+  simp only [decide_eq_true_eq] at h1
+  have h2 :=
+    lratCheckerSound
+      _
+      (by apply CNF.convertLRAT_readyForRupAdd)
+      (by apply CNF.convertLRAT_readyForRatAdd)
+      _
+      (by
+        intro action h
+        simp only [Array.toList_eq, List.filterMap_map, List.mem_filterMap, Function.comp_apply] at h
+        rcases h with ⟨WellFormedActions, _, h2⟩
+        split at h2
+        . contradiction
+        . simp only [Option.some.injEq] at h2
+          simp [← h2, WellFormedAction]
+        . simp only [Option.some.injEq] at h2
+          simp [← h2, WellFormedAction]
+        . simp only [Option.some.injEq] at h2
+          simp [← h2, WellFormedAction]
+        . simp only [ite_some_none_eq_some] at h2
+          rcases h2 with ⟨hleft, hright⟩
+          simp [WellFormedAction, hleft, ← hright, Clause.limplies_iff_mem]
+      )
+      h1
+  apply CNF.unsat_of_convertLRAT_unsat
+  assumption
+
+end LRAT
+end Lean.Elab.Tactic.BVDecide

src/Lean/Elab/Tactic/BVDecide/LRAT/Internal.lean

@@ -0,0 +1,22 @@
+/-
+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.LRAT.Internal.Actions
+import Lean.Elab.Tactic.BVDecide.LRAT.Internal.Assignment
+import Lean.Elab.Tactic.BVDecide.LRAT.Internal.CNF
+import Lean.Elab.Tactic.BVDecide.LRAT.Internal.Formula
+import Lean.Elab.Tactic.BVDecide.LRAT.Internal.Entails
+import Lean.Elab.Tactic.BVDecide.LRAT.Internal.Assignment
+import Lean.Elab.Tactic.BVDecide.LRAT.Internal.Clause
+import Lean.Elab.Tactic.BVDecide.LRAT.Internal.LRATChecker
+import Lean.Elab.Tactic.BVDecide.LRAT.Internal.LRATCheckerSound
+import Lean.Elab.Tactic.BVDecide.LRAT.Internal.PosFin
+import Lean.Elab.Tactic.BVDecide.LRAT.Internal.Convert
+
+/-!
+This module contains the internals of the current LRAT checker implementation. It should not be
+considered part of the API of `bv_decide` and will be removed or largely refactored in the future.
+-/

src/Lean/Elab/Tactic/BVDecide/LRAT/Internal/Actions.lean

@@ -0,0 +1,97 @@
+/-
+Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Josh Clune
+-/
+prelude
+import Lean.Elab.Tactic.BVDecide.LRAT.Actions
+import Lean.Elab.Tactic.BVDecide.LRAT.Internal.Clause
+
+namespace Lean.Elab.Tactic.BVDecide
+
+namespace LRAT
+namespace Internal
+
+open Std.Sat
+
+/--
+`Action` where variables have type `PosFin n`, clauses are `DefaultClause`, and ids are `Nat`.
+This Action type is meant to be usable for verifying LRAT proofs that operate on default formulas.
+-/
+abbrev DefaultClauseAction (n : Nat) : Type := Action (DefaultClause n) (PosFin n)
+
+/--
+A predicate for Actions that ensures that the pivot of a clause is always included in the clause.
+In the LRAT format, the clause's pivot is always its first literal. However, from an interface
+perspective, it is awkward to require that all `Clause` implementations preserve the ordering of
+their literals. It is also awkward to have the pivot in the `addRat` action not included in the
+clause itself, since then the pivot would need to be readded to the clause when it is added to the
+formula. So to avoid imposing awkward constraints on the `Clause` interface, and to avoid requiring
+`Formula` implementations to add pivots to the clauses provided by the `addRat` action, we use this
+predicate to indicate that the pivot provided by the `addRat` action is indeed in the provided
+clause.
+-/
+def WellFormedAction [Clause α β] : Action β α → Prop
+  -- Note that `Limplies α p c` is equivalent to `p ∈ toList c` by `limplies_iff_mem` in CNF.lean
+  | .addRat _ c p _ _ => Limplies α p c
+  | _ => True
+
+def natLiteralToPosFinLiteral {n : Nat} (x : Literal Nat) (x_ne_zero : x.1 ≠ 0) : Option (Literal (PosFin n)) := do
+  if h : x.1 < n then
+    some (⟨x.1, ⟨Nat.zero_lt_of_ne_zero x_ne_zero, h⟩⟩, x.2)
+  else
+    none
+
+def intToLiteralPure {n : Nat} (x : Int) (x_ne_zero : x ≠ 0) : Option (Literal (PosFin n)) := do
+  if h : x.natAbs < n then
+    if x > 0 then
+      some (⟨x.natAbs, ⟨by omega, h⟩⟩, true)
+    else
+      some (⟨x.natAbs, ⟨by omega, h⟩⟩, false)
+  else
+    none
+
+/--
+Since `IntAction` is a convenient parsing target and `DefaultClauseAction` is a useful Action type
+for working with default clauses, an expected workflow pattern is to parse an external LRAT proof
+into a list of `IntAction`s, and then use this function to convert that list of `IntAction`s to
+`DefaultClauseAction`s.
+
+This function returns an `Option` type so that `none` can be returned if converting from the
+`IntAction` to `DefaultClauseAction` fails. This can occur if any of the literals in the `IntAction`
+are 0 or ≥ n.
+-/
+def intActionToDefaultClauseAction (n : Nat) : IntAction → Option (DefaultClauseAction n)
+  | .addEmpty cId rupHints => some <| .addEmpty cId rupHints
+  | .addRup cId c rupHints => do
+    let c : Array (Option (Literal (PosFin n))) :=
+      c.map (fun x => if h : x ≠ 0 then intToLiteralPure x h else none)
+    if c.contains none then
+      none
+    else
+      let c := c.filterMap id
+      match Clause.ofArray c with
+      | none => none
+      | some c => some <| .addRup cId c rupHints
+  | .addRat cId c pivot rupHints ratHints => do
+    if h : pivot.1 ≠ 0 then
+      let some pivot := natLiteralToPosFinLiteral pivot h
+        | none
+      let c : Array (Option (Literal (PosFin n))) :=
+        c.map (fun x => if h : x ≠ 0 then intToLiteralPure x h else none)
+      if c.contains none then
+        none
+      else
+        let c := c.filterMap id
+        match Clause.ofArray c with
+        | some c => some <| .addRat cId c pivot rupHints ratHints
+        | none => none
+    else
+      none
+  | .del ids => some <| .del ids
+
+
+end Internal
+end LRAT
+
+end Lean.Elab.Tactic.BVDecide