feat: basic instances for ULift and PLift

Some missing easy lemmas.

.github/workflows/restart-on-label.yml

@@ -14,8 +14,9 @@ jobs:
         # (unfortunately cannot search by PR number, only base branch,
         # and that is't even unique given PRs from forks, but the risk
         # of confusion is low and the danger is mild)
-        run_id=$(gh run list -e pull_request -b "$head_ref" --workflow 'CI' --limit 1 \
-          --limit 1 --json databaseId --jq '.[0].databaseId')
+        echo "Trying to find a run with branch $head_ref and commit $head_sha"
+        run_id="$(gh run list -e pull_request -b "$head_ref" -c "$head_sha" \
+          --workflow 'CI' --limit 1 --json databaseId --jq '.[0].databaseId')"
         echo "Run id: ${run_id}"
         gh run view "$run_id"
         echo "Cancelling (just in case)"
@@ -29,5 +30,6 @@ jobs:
       shell: bash
       env:
         head_ref: ${{ github.head_ref }}
+        head_sha: ${{ github.event.pull_request.head.sha }}
         GH_TOKEN: ${{ github.token }}
         GH_REPO: ${{ github.repository }}

src/Init/Data.lean

@@ -37,3 +37,5 @@ import Init.Data.Cast
 import Init.Data.Sum
 import Init.Data.BEq
 import Init.Data.Subtype
+import Init.Data.ULift
+import Init.Data.PLift

src/Init/Data/List/Find.lean

@@ -34,7 +34,7 @@ theorem find?_some : ∀ {l}, find? p l = some a → p a
     · exact H ▸ h
     · exact find?_some H
 
-@[simp] theorem mem_of_find?_eq_some : ∀ {l}, find? p l = some a → a ∈ l
+theorem mem_of_find?_eq_some : ∀ {l}, find? p l = some a → a ∈ l
   | b :: l, H => by
     by_cases h : p b <;> simp [find?, h] at H
     · exact H ▸ .head _

src/Init/Data/List/Sort/Basic.lean

@@ -30,8 +30,8 @@ def merge (le : α → α → Bool) : List α → List α → List α
     else
       y :: merge le (x :: xs) ys
 
-@[simp] theorem merge_nil_left (ys : List α) : merge le [] ys = ys := by simp [merge]
-@[simp] theorem merge_nil_right (xs : List α) : merge le xs [] = xs := by
+@[simp] theorem nil_merge (ys : List α) : merge le [] ys = ys := by simp [merge]
+@[simp] theorem merge_right (xs : List α) : merge le xs [] = xs := by
   induction xs with
   | nil => simp [merge]
   | cons x xs ih => simp [merge, ih]

src/Init/Data/List/Sort/Lemmas.lean

@@ -215,6 +215,10 @@ theorem merge_perm_append : ∀ {xs ys : List α}, merge le xs ys ~ xs ++ ys
 
 /-! ### mergeSort -/
 
+@[simp] theorem mergeSort_nil : [].mergeSort r = [] := by rw [List.mergeSort]
+
+@[simp] theorem mergeSort_singleton (a : α) : [a].mergeSort r = [a] := by rw [List.mergeSort]
+
 variable (le) in
 theorem mergeSort_perm : ∀ (l : List α), mergeSort le l ~ l
   | [] => by simp [mergeSort]
@@ -228,6 +232,9 @@ theorem mergeSort_perm : ∀ (l : List α), mergeSort le l ~ l
         (Perm.of_eq (splitInTwo_fst_append_splitInTwo_snd _)))
 termination_by l => l.length
 
+@[simp] theorem mergeSort_length (l : List α) : (mergeSort le l).length = l.length :=
+  (mergeSort_perm le l).length_eq
+
 @[simp] theorem mem_mergeSort {a : α} {l : List α} : a ∈ mergeSort le l ↔ a ∈ l :=
   (mergeSort_perm le l).mem_iff
 

src/Init/Data/List/Sublist.lean

@@ -68,12 +68,12 @@ instance : Trans (Membership.mem : α → List α → Prop) Subset Membership.me
 instance : Trans (Subset : List α → List α → Prop) Subset Subset :=
   ⟨Subset.trans⟩
 
-@[simp] theorem subset_cons_self (a : α) (l : List α) : l ⊆ a :: l := fun _ => Mem.tail _
+theorem subset_cons_self (a : α) (l : List α) : l ⊆ a :: l := fun _ => Mem.tail _
 
 theorem subset_of_cons_subset {a : α} {l₁ l₂ : List α} : a :: l₁ ⊆ l₂ → l₁ ⊆ l₂ :=
   fun s _ i => s (mem_cons_of_mem _ i)
 
-theorem subset_cons_of_subset (a : α) {l₁ l₂ : List α} : l₁ ⊆ l₂ → l₁ ⊆ a :: l₂ :=
+@[simp] theorem subset_cons_of_subset (a : α) {l₁ l₂ : List α} : l₁ ⊆ l₂ → l₁ ⊆ a :: l₂ :=
   fun s _ i => .tail _ (s i)
 
 theorem cons_subset_cons {l₁ l₂ : List α} (a : α) (s : l₁ ⊆ l₂) : a :: l₁ ⊆ a :: l₂ :=
@@ -100,14 +100,14 @@ theorem filterMap_subset {l₁ l₂ : List α} (f : α → Option β) (H : l₁
   rintro ⟨a, h, w⟩
   exact ⟨a, H h, w⟩
 
-@[simp] theorem subset_append_left (l₁ l₂ : List α) : l₁ ⊆ l₁ ++ l₂ := fun _ => mem_append_left _
+theorem subset_append_left (l₁ l₂ : List α) : l₁ ⊆ l₁ ++ l₂ := fun _ => mem_append_left _
 
-@[simp] theorem subset_append_right (l₁ l₂ : List α) : l₂ ⊆ l₁ ++ l₂ := fun _ => mem_append_right _
+theorem subset_append_right (l₁ l₂ : List α) : l₂ ⊆ l₁ ++ l₂ := fun _ => mem_append_right _
 
-theorem subset_append_of_subset_left (l₂ : List α) : l ⊆ l₁ → l ⊆ l₁ ++ l₂ :=
+@[simp] theorem subset_append_of_subset_left (l₂ : List α) : l ⊆ l₁ → l ⊆ l₁ ++ l₂ :=
 fun s => Subset.trans s <| subset_append_left _ _
 
-theorem subset_append_of_subset_right (l₁ : List α) : l ⊆ l₂ → l ⊆ l₁ ++ l₂ :=
+@[simp] theorem subset_append_of_subset_right (l₁ : List α) : l ⊆ l₂ → l ⊆ l₁ ++ l₂ :=
 fun s => Subset.trans s <| subset_append_right _ _
 
 @[simp] theorem append_subset {l₁ l₂ l : List α} :
@@ -155,7 +155,9 @@ theorem Sublist.trans {l₁ l₂ l₃ : List α} (h₁ : l₁ <+ l₂) (h₂ : l
 
 instance : Trans (@Sublist α) Sublist Sublist := ⟨Sublist.trans⟩
 
-@[simp] theorem sublist_cons_self (a : α) (l : List α) : l <+ a :: l := (Sublist.refl l).cons _
+attribute [simp] Sublist.cons
+
+theorem sublist_cons_self (a : α) (l : List α) : l <+ a :: l := (Sublist.refl l).cons _
 
 theorem sublist_of_cons_sublist : a :: l₁ <+ l₂ → l₁ <+ l₂ :=
   (sublist_cons_self a l₁).trans
@@ -286,11 +288,11 @@ theorem sublist_filter_iff {l₁ : List α} {p : α → Bool} :
     l₁ <+ l₂.filter p ↔ ∃ l', l' <+ l₂ ∧ l₁ = l'.filter p := by
   simp only [← filterMap_eq_filter, sublist_filterMap_iff]
 
-@[simp] theorem sublist_append_left : ∀ l₁ l₂ : List α, l₁ <+ l₁ ++ l₂
+theorem sublist_append_left : ∀ l₁ l₂ : List α, l₁ <+ l₁ ++ l₂
   | [], _ => nil_sublist _
   | _ :: l₁, l₂ => (sublist_append_left l₁ l₂).cons₂ _
 
-@[simp] theorem sublist_append_right : ∀ l₁ l₂ : List α, l₂ <+ l₁ ++ l₂
+theorem sublist_append_right : ∀ l₁ l₂ : List α, l₂ <+ l₁ ++ l₂
   | [], _ => Sublist.refl _
   | _ :: l₁, l₂ => (sublist_append_right l₁ l₂).cons _
 
@@ -299,10 +301,10 @@ theorem sublist_filter_iff {l₁ : List α} {p : α → Bool} :
   obtain ⟨_, _, rfl⟩ := append_of_mem h
   exact ((nil_sublist _).cons₂ _).trans (sublist_append_right ..)
 
-theorem sublist_append_of_sublist_left (s : l <+ l₁) : l <+ l₁ ++ l₂ :=
+@[simp] theorem sublist_append_of_sublist_left (s : l <+ l₁) : l <+ l₁ ++ l₂ :=
   s.trans <| sublist_append_left ..
 
-theorem sublist_append_of_sublist_right (s : l <+ l₂) : l <+ l₁ ++ l₂ :=
+@[simp] theorem sublist_append_of_sublist_right (s : l <+ l₂) : l <+ l₁ ++ l₂ :=
   s.trans <| sublist_append_right ..
 
 @[simp] theorem append_sublist_append_left : ∀ l, l ++ l₁ <+ l ++ l₂ ↔ l₁ <+ l₂

src/Init/Data/Option/Lemmas.lean

@@ -261,7 +261,7 @@ theorem liftOrGet_eq_or_eq {f : α → α → α} (h : ∀ a b, f a b = a ∨ f
 @[simp] theorem getD_map (f : α → β) (x : α) (o : Option α) :
   (o.map f).getD (f x) = f (getD o x) := by cases o <;> rfl
 
-section
+section choice
 
 attribute [local instance] Classical.propDecidable
 
@@ -277,7 +277,7 @@ theorem choice_eq {α : Type _} [Subsingleton α] (a : α) : choice α = some a
 theorem choice_isSome_iff_nonempty {α : Type _} : (choice α).isSome ↔ Nonempty α :=
   ⟨fun h => ⟨(choice α).get h⟩, fun h => by simp only [choice, dif_pos h, isSome_some]⟩
 
-end
+end choice
 
 @[simp] theorem toList_some (a : α) : (a : Option α).toList = [a] := rfl
 
@@ -333,3 +333,43 @@ theorem or_of_isSome {o o' : Option α} (h : o.isSome) : o.or o' = o := by
 theorem or_of_isNone {o o' : Option α} (h : o.isNone) : o.or o' = o' := by
   match o, h with
   | none, _ => simp
+
+section ite
+
+@[simp] theorem isSome_dite {p : Prop} [Decidable p] {b : p → β} :
+    (if h : p then some (b h) else none).isSome = true ↔ p := by
+  split <;> simpa
+@[simp] theorem isSome_ite {p : Prop} [Decidable p] :
+    (if p then some b else none).isSome = true ↔ p := by
+  split <;> simpa
+@[simp] theorem isSome_dite' {p : Prop} [Decidable p] {b : ¬ p → β} :
+    (if h : p then none else some (b h)).isSome = true ↔ ¬ p := by
+  split <;> simpa
+@[simp] theorem isSome_ite' {p : Prop} [Decidable p] :
+    (if p then none else some b).isSome = true ↔ ¬ p := by
+  split <;> simpa
+
+@[simp] theorem get_dite {p : Prop} [Decidable p] (b : p → β) (w) :
+    (if h : p then some (b h) else none).get w = b (by simpa using w) := by
+  split
+  · simp
+  · exfalso
+    simp at w
+    contradiction
+@[simp] theorem get_ite {p : Prop} [Decidable p] (h) :
+    (if p then some b else none).get h = b := by
+  simpa using get_dite (p := p) (fun _ => b) (by simpa using h)
+@[simp] theorem get_dite' {p : Prop} [Decidable p] (b : ¬ p → β) (w) :
+    (if h : p then none else some (b h)).get w = b (by simpa using w) := by
+  split
+  · exfalso
+    simp at w
+    contradiction
+  · simp
+@[simp] theorem get_ite' {p : Prop} [Decidable p] (h) :
+    (if p then none else some b).get h = b := by
+  simpa using get_dite' (p := p) (fun _ => b) (by simpa using h)
+
+end ite
+
+end Option

src/Init/Data/PLift.lean

@@ -0,0 +1,12 @@
+/-
+Copyright (c) 2024 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Core
+
+deriving instance DecidableEq for PLift
+
+instance [Subsingleton α] : Subsingleton (PLift α) where
+  allEq := fun ⟨a⟩ ⟨b⟩ => congrArg PLift.up (Subsingleton.elim a b)

src/Init/Data/String/Basic.lean

@@ -558,7 +558,7 @@ structure Iterator where
   `Iterator.next` when `Iterator.atEnd` is true. If the position is not valid, then the
   current character is `(default : Char)`, similar to `String.get` on an invalid position. -/
   i : Pos
-  deriving DecidableEq
+  deriving DecidableEq, Inhabited
 
 /-- Creates an iterator at the beginning of a string. -/
 def mkIterator (s : String) : Iterator :=

src/Init/Data/ULift.lean

@@ -0,0 +1,12 @@
+/-
+Copyright (c) 2024 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Core
+
+deriving instance DecidableEq for ULift
+
+instance [Subsingleton α] : Subsingleton (ULift α) where
+  allEq := fun ⟨a⟩ ⟨b⟩ => congrArg ULift.up (Subsingleton.elim a b)

src/Lean/Data/Parsec/Basic.lean

@@ -84,6 +84,10 @@ def eof : Parsec ι Unit := fun it =>
   else
     .success it ()
 
+@[inline]
+def eof? : Parsec ι Bool := fun it =>
+  .success it (!Input.hasNext it)
+
 @[specialize]
 partial def manyCore (p : Parsec ι α) (acc : Array α) : Parsec ι <| Array α :=
   tryCatch p (manyCore p <| acc.push ·) (fun _ => pure acc)

src/Lean/Data/Parsec/ByteArray.lean

@@ -62,6 +62,35 @@ def digit : Parser Char := attempt do
   let b ← any
   if '0'.toUInt8 ≤ b ∧ b ≤ '9'.toUInt8 then return Char.ofUInt8 b else fail s!"digit expected"
 
+@[inline]
+private def digitToNat (b : UInt8) : Nat := (b - '0'.toUInt8).toNat
+
+@[inline]
+private partial def digitsCore (acc : Nat) : Parser Nat := fun it =>
+  /-
+  With this design instead of combinators we can avoid allocating and branching over .success values
+  all of the time.
+  -/
+  let ⟨res, it⟩ := go it acc
+  .success it res
+where
+  go (it : ByteArray.Iterator) (acc : Nat) : Nat × ByteArray.Iterator :=
+    if it.hasNext then
+      let candidate := it.curr
+      if '0'.toUInt8 ≤ candidate ∧ candidate ≤ '9'.toUInt8 then
+        let digit := digitToNat candidate
+        let acc := acc * 10 + digit
+        go it.next acc
+      else
+        (acc, it)
+    else
+      (acc, it)
+
+@[inline]
+def digits : Parser Nat := do
+  let d ← digit
+  digitsCore (digitToNat d.toUInt8)
+
 @[inline]
 def hexDigit : Parser Char := attempt do
   let b ← any

src/Lean/Data/Parsec/String.lean

@@ -46,6 +46,35 @@ def digit : Parser Char := attempt do
   let c ← any
   if '0' ≤ c ∧ c ≤ '9' then return c else fail s!"digit expected"
 
+@[inline]
+private def digitToNat (b : Char) : Nat := b.toNat - '0'.toNat
+
+@[inline]
+private partial def digitsCore (acc : Nat) : Parser Nat := fun it =>
+  /-
+  With this design instead of combinators we can avoid allocating and branching over .success values
+  all of the time.
+  -/
+  let ⟨res, it⟩ := go it acc
+  .success it res
+where
+  go (it : String.Iterator) (acc : Nat) : (Nat × String.Iterator) :=
+    if it.hasNext then
+      let candidate := it.curr
+      if '0' ≤ candidate ∧ candidate ≤ '9' then
+        let digit := digitToNat candidate
+        let acc := acc * 10 + digit
+        go it.next acc
+      else
+        (acc, it)
+    else
+      (acc, it)
+
+@[inline]
+def digits : Parser Nat := do
+  let d ← digit
+  digitsCore (digitToNat d)
+
 @[inline]
 def hexDigit : Parser Char := attempt do
   let c ← any

src/Lean/Elab/Tactic/BVDecide.lean

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

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

@@ -0,0 +1,163 @@
+/-
+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.Parser
+import Lean.CoreM
+import Lean.Data.Parsec
+
+/-!
+This module implements the logic to call CaDiCal (or CLI interface compatible SAT solvers) and
+extract an LRAT UNSAT proof or a model from its output.
+-/
+
+namespace Lean.Elab.Tactic.BVDecide
+
+namespace External
+
+/--
+The result of calling a SAT solver.
+-/
+inductive SolverResult where
+  /--
+  The solver returned SAT with some literal assignment.
+  -/
+  | sat (assignment : Array (Bool × Nat))
+  /--
+  The solver returned UNSAT.
+  -/
+  | unsat
+
+namespace ModelParser
+
+open Lean.Parsec
+open Lean.Parsec.ByteArray
+
+def parsePartialAssignment : Parser (Bool × (Array (Bool × Nat))) := do
+  skipByteChar 'v'
+  let idents ← many (attempt wsLit)
+  let idents := idents.map (fun i => if i > 0 then (true, i.natAbs) else (false, i.natAbs))
+  Parsec.tryCatch
+    (skipString " 0")
+    (csuccess := fun _ => pure (true, idents))
+    (cerror := fun _ => do
+      skipByteChar '\n'
+      return (false, idents)
+    )
+where
+  @[inline]
+  wsLit : Parser Int := do
+    skipByteChar ' '
+    LRAT.Parser.Text.parseLit
+
+partial def parseLines : Parser (Array (Bool × Nat)) :=
+  go #[]
+where
+  go (acc : Array (Bool × Nat)) : Parser (Array (Bool × Nat)) := do
+    let (terminal?, additionalAssignment) ← parsePartialAssignment
+    let acc := acc ++ additionalAssignment
+    if terminal? then
+      return acc
+    else
+      go acc
+
+@[inline]
+def parseHeader : Parser Unit := do
+  skipString "s SATISFIABLE\n"
+
+/--
+Parse the witness format of a SAT solver. The rough grammar for this is:
+line = "v" (" " lit)*\n
+terminal_line = "v" (" " lit)* (" " 0)\n
+witness = "s SATISFIABLE\n" line+ terminal_line
+-/
+def parse : Parser (Array (Bool × Nat)) := do
+  parseHeader
+  parseLines
+
+end ModelParser
+
+open Lean (CoreM)
+
+/--
+Run a process with `args` until it terminates or the cancellation token in `CoreM` tells us to abort.
+-/
+partial def runInterruptible (args : IO.Process.SpawnArgs) : CoreM 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 }
+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
+      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 }
+      | 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
+    else
+      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) :
+    CoreM SolverResult := do
+  let cmd := solverPath
+  let 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.
+  ]
+
+  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
+    else
+      throwError s!"The external prover produced unexpected output:\n{stdout}"
+
+end External
+
+end Lean.Elab.Tactic.BVDecide

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

@@ -7,6 +7,7 @@ prelude
 import Lean.Elab.Tactic.BVDecide.LRAT.Actions
 import Lean.Elab.Tactic.BVDecide.LRAT.Checker
 import Lean.Elab.Tactic.BVDecide.LRAT.Trim
+import Lean.Elab.Tactic.BVDecide.LRAT.Parser
 
 /-!
 This directory contains the implementation of the LRAT certificate checking and the LRAT trimming

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

@@ -0,0 +1,425 @@
+/-
+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 Init.System.IO
+import Lean.Elab.Tactic.BVDecide.LRAT.Actions
+import Lean.Data.Parsec
+
+/-!
+This module implements parsers and serializers for both the binary and non-binary LRAT format.
+-/
+
+namespace Lean.Elab.Tactic.BVDecide
+
+namespace LRAT
+namespace Parser
+
+open Std.Sat
+open Lean.Elab.Tactic.BVDecide.LRAT (IntAction)
+
+private def getPivot (clause : Array Int) : Literal Nat :=
+  let pivotInt := clause[0]!
+  if pivotInt > 0 then
+    (pivotInt.natAbs, true)
+  else
+    (pivotInt.natAbs, false)
+
+
+open Lean.Parsec
+open Lean.Parsec.ByteArray
+
+namespace Text
+
+/-
+This implements a (corrected) version of the grammar presented in:
+https://www.cs.cmu.edu/~mheule/publications/lrat.pdf
+
+The production rules ⟨clause⟩ and ⟨rat⟩ in Fig. 3. would mandate to put two 0 after the new
+clause that the current proof step is producing, that is not the case.
+-/
+
+@[inline]
+def parsePos : Parser Nat := do
+  let ident ← digits
+  if ident == 0 then
+    fail "id was 0"
+  else
+    return ident
+
+@[inline]
+def parseNeg : Parser Int := do
+  skipByteChar '-'
+  let nat ← parsePos
+  return -nat
+
+@[inline]
+def parseId : Parser Nat := parsePos
+
+@[inline]
+def parseZero : Parser Unit := skipByteChar '0'
+
+def parseIdList : Parser (Array Nat) := do
+  many idWs
+where
+  @[inline]
+  idWs : Parser Nat := do
+    let ident ← attempt parseId
+    skipByteChar ' '
+    return ident
+
+def parseDelete : Parser IntAction := do
+  skipByteChar 'd'
+  skipByteChar ' '
+  let idList ← parseIdList
+  parseZero
+  return .del idList
+
+@[inline]
+def parseLit : Parser Int := do
+  if (← peek!) == '-'.toUInt8 then
+    parseNeg
+  else
+    Int.ofNat <$> parsePos
+
+def parseClause : Parser (Array Int) := do
+  let lits ← many litWs
+  parseZero
+  return lits
+where
+  @[inline]
+  litWs : Parser Int := do
+    let lit ← attempt parseLit
+    skipByteChar ' '
+    return lit
+
+def parseRes : Parser (Nat × Array Nat) := do
+  let lhs ← parseNeg
+  skipByteChar ' '
+  let idents ← parseIdList
+  return (lhs.natAbs, idents)
+
+def parseRat (ident : Nat) : Parser IntAction := do
+  let clause ← parseClause
+  skipByteChar ' '
+  let rupHints ← parseIdList
+  let ratHints ← many (attempt parseRes)
+  parseZero
+  match clause.size, ratHints.size with
+  | 0, 0 => return .addEmpty ident rupHints
+  | 0, _ => fail "There cannot be any ratHints for adding the empty clause"
+  | _, 0 => return .addRup ident clause rupHints
+  | _, _ => return .addRat ident clause (getPivot clause) rupHints ratHints
+
+def parseAction : Parser IntAction := do
+  let ident ← parseId
+  skipByteChar ' '
+  if (← peek!) == 'd'.toUInt8 then
+    parseDelete
+  else
+    parseRat ident
+
+partial def parseActions : Parser (Array IntAction) :=
+  go #[]
+where
+  go (actions : Array IntAction) : Parser (Array IntAction) := do
+    if (← peek!) == 'c'.toUInt8 then
+      let _ ← many (satisfy (· != '\n'.toUInt8))
+      skipByteChar '\n'
+      if ← eof? then
+        return actions
+      else
+        go actions
+    else
+      let action ← parseAction
+      skipByteChar '\n'
+      let actions := actions.push action
+      if ← eof? then
+        return actions
+      else
+        go actions
+
+end Text
+
+namespace Binary
+
+@[inline]
+def parseZero : Parser Unit := skipByte 0
+
+-- see: https://github.com/marijnheule/drat-trim?tab=readme-ov-file#binary-drat-format
+-- see: https://github.com/arminbiere/lrat-trim/blob/80f22c57fb2d74cb72210f5b334a1ffe2160a628/lrat-trim.c#L1579-L1595
+partial def parseLit : Parser Int := do
+  go 0 0
+where
+  go (uidx : UInt64) (shift : UInt64) : Parser Int := do
+    let uch ← any
+    if shift == 28 && ((uch &&& ~~~15) != 0) then
+      fail "Excessive literal"
+    else if uch == 0 then
+      fail "Invalid zero byte in literal"
+    else
+      let uidx := uidx ||| ((uch &&& 127).toUInt64 <<< shift)
+      if uch &&& 128 == 0 then
+        let idx := uidx >>> 1
+        if (1 &&& uidx) != 0 then
+          return (-(idx).toNat : Int)
+        else
+          return (idx.toNat : Int)
+      else
+        go uidx (shift + 7)
+
+@[inline]
+def parseNeg : Parser Nat := do
+  let lit ← parseLit
+  if lit < 0 then
+    return lit.natAbs
+  else
+    fail "parsed non negative lit where negative was expected"
+
+@[inline]
+def parsePos : Parser Nat := do
+  let lit ← parseLit
+  if lit > 0 then
+    return lit.natAbs
+  else
+    fail "parsed non positive lit where positive was expected"
+
+@[inline]
+def parseId : Parser Nat := parsePos
+
+@[specialize]
+partial def manyTillZero (parser : Parser α) : Parser (Array α) :=
+  go #[]
+where
+  @[specialize]
+  go (acc : Array α) : Parser (Array α) := do
+    if (← peek!) == 0 then
+      return acc
+    else
+      let elem ← parser
+      go <| acc.push elem
+
+@[specialize]
+partial def manyTillNegOrZero (parser : Parser α) : Parser (Array α) :=
+  go #[]
+where
+  @[specialize]
+  go (acc : Array α) : Parser (Array α) := do
+    let byte ← peek!
+    if (1 &&& byte != 0) || byte == 0 then
+      return acc
+    else
+      let elem ← parser
+      go <| acc.push elem
+
+@[inline]
+def parseIdList : Parser (Array Nat) :=
+  manyTillNegOrZero parseId
+
+@[inline]
+def parseClause : Parser (Array Int) := do
+  manyTillZero parseLit
+
+def parseRes : Parser (Nat × Array Nat) := do
+  let lhs ← parseNeg
+  let idents ← parseIdList
+  return (lhs, idents)
+
+@[inline]
+def parseRatHints : Parser (Array (Nat × Array Nat)) := do
+  manyTillZero parseRes
+
+def parseAction : Parser IntAction := do
+  let discr ← any
+  if discr == 'a'.toUInt8 then
+    parseAdd
+  else if discr == 'd'.toUInt8 then
+    parseDelete
+  else
+    fail s!"Expected a or d got: {discr}"
+where
+  parseAdd : Parser IntAction := do
+    let ident ← parseId
+    let clause ← parseClause
+    parseZero
+    let rupHints ← parseIdList
+    let ratHints ← parseRatHints
+    parseZero
+    match clause.size, ratHints.size with
+    | 0, 0 => return .addEmpty ident rupHints
+    | 0, _ => fail "There cannot be any ratHints for adding the empty clause"
+    | _, 0 => return .addRup ident clause rupHints
+    | _, _ => return .addRat ident clause (getPivot clause) rupHints ratHints
+
+  parseDelete : Parser IntAction := do
+    let idList ← parseIdList
+    parseZero
+    return .del idList
+
+def parseActions : Parser (Array IntAction) := do
+  let actions ← many parseAction
+  eof
+  return actions
+
+end Binary
+
+/--
+Based on the first byte parses the input either as a binary or non-binary LRAT.
+-/
+def parseActions : Parser (Array IntAction) := do
+  let byte ← peek!
+  if byte == 'a'.toUInt8 || byte == 'd'.toUInt8 then
+    Binary.parseActions
+  else
+    Text.parseActions
+
+end Parser
+
+/--
+Read and parse an LRAT proof from `path`. `path` may contain either the binary or the non-binary
+LRAT format.
+-/
+def loadLRATProof (path : System.FilePath) : IO (Array IntAction) := do
+  let proof ← IO.FS.readBinFile path
+  match Parser.parseActions.run proof with
+  | .ok actions => return actions
+  | .error err => throw <| .userError err
+
+/--
+Parse `proof` as an LRAT proof. `proof` may contain either the binary or the non-binary LRAT format.
+-/
+def parseLRATProof (proof : ByteArray) : Option (Array IntAction) :=
+  match Parser.parseActions.run proof with
+  | .ok actions => some actions
+  | .error .. => none
+
+/--
+Serialize `proof` into the non-binary LRAT format as a `String`.
+-/
+def lratProofToString (proof : Array IntAction) : String :=
+  proof.foldl (init := "") (· ++ serialize · ++ "\n")
+where
+  serialize (a : IntAction) : String :=
+    match a with
+    | .addEmpty id hints =>
+      s!"{id} 0 {serializeIdList hints}0"
+    | .addRup id c hints =>
+      s!"{id} {serializeClause c}0 {serializeIdList hints}0"
+    | .addRat id c _ rupHints ratHints =>
+      s!"{id} {serializeClause c}0 {serializeIdList rupHints}{serializeRatHints ratHints}0"
+    | .del ids =>
+      -- Note: 1 is not the actual step id but step ids don't matter for deletes
+      s!"1 d {serializeIdList ids}0"
+
+  serializeIdList (ids : Array Nat) : String :=
+    ids.foldl (init := "") (· ++ s!"{·} ")
+
+  serializeClause (clause : Array Int) : String :=
+    clause.foldl (init := "") (· ++ s!"{·} ")
+
+  serializeRatHint (hint : Nat × Array Nat) : String :=
+    s!"-{hint.fst} {serializeIdList hint.snd}"
+
+  serializeRatHints (hints : Array (Nat × Array Nat)) : String :=
+    hints.foldl (init := "") (· ++ serializeRatHint ·)
+
+/--
+Serialize `proof` into the binary LRAT format as a `ByteArray`.
+-/
+partial def lratProofToBinary (proof : Array IntAction) : ByteArray :=
+  -- we will definitely need at least 4 bytes per add step and almost exclusively produce add.
+  go 0 (ByteArray.mkEmpty (4 * proof.size))
+where
+  go (idx : Nat) (acc : ByteArray) : ByteArray :=
+    if h:idx < proof.size then
+      let acc :=
+        match proof[idx] with
+        | .addEmpty id hints =>
+          let acc := startAdd acc
+          let acc := addNat acc id
+          let acc := zeroByte acc
+          let acc := hints.foldl (init := acc) addNat
+          let acc := zeroByte acc
+          acc
+        | .addRup id c hints =>
+          let acc := startAdd acc
+          let acc := addNat acc id
+          let acc := c.foldl (init := acc) addInt
+          let acc := zeroByte acc
+          let acc := hints.foldl (init := acc) addNat
+          let acc := zeroByte acc
+          acc
+        | .addRat id c _ rupHints ratHints =>
+          let acc := startAdd acc
+          let acc := addNat acc id
+          let acc := c.foldl (init := acc) addInt
+          let acc := zeroByte acc
+          let acc := rupHints.foldl (init := acc) addNat
+          let ratHintFolder acc hint :=
+            let acc := addInt acc (-hint.fst)
+            let acc := hint.snd.foldl (init := acc) addNat
+            acc
+          let acc := ratHints.foldl (init := acc) ratHintFolder
+          let acc := zeroByte acc
+          acc
+        | .del ids =>
+          let acc := startDelete acc
+          let acc := ids.foldl (init := acc) addNat
+          let acc := zeroByte acc
+          acc
+      go (idx + 1) acc
+    else
+      acc
+
+  addInt (acc : ByteArray) (lit : Int) : ByteArray :=
+    let mapped :=
+      if lit > 0 then
+        2 * lit.natAbs
+      else
+        2 * lit.natAbs + 1
+    assert! mapped ≤ (2^64 - 1) -- our parser "only" supports 64 bit literals
+    let mapped := mapped.toUInt64
+    variableLengthEncode acc mapped
+
+  variableLengthEncode (acc : ByteArray) (lit : UInt64) : ByteArray :=
+    -- once the literal is 0 we don't need to add another byte.
+    if lit == 0 then
+      acc
+    else
+      let chunk :=
+        if lit > 127 then
+          (lit.toUInt8 &&& 127) ||| 128
+        else
+          lit.toUInt8 &&& 127
+      let acc := acc.push chunk
+      variableLengthEncode acc (lit >>> 7)
+
+  @[inline]
+  startAdd (acc : ByteArray) : ByteArray := acc.push 'a'.toUInt8
+
+  @[inline]
+  startDelete (acc : ByteArray) : ByteArray := acc.push 'd'.toUInt8
+
+  @[inline]
+  zeroByte (acc : ByteArray) : ByteArray := acc.push 0
+
+  @[inline]
+  addNat (acc : ByteArray) (n : Nat) : ByteArray := addInt acc n
+
+/--
+Dump `proof` into `path`, either in the binary or non-binary LRAT format, depending on `binaryProofs`.
+-/
+def dumpLRATProof (path : System.FilePath) (proof : Array IntAction) (binaryProofs : Bool) :
+    IO Unit := do
+  let out :=
+    if binaryProofs then
+      lratProofToBinary proof
+    else
+      lratProofToString proof |>.toUTF8
+  IO.FS.writeBinFile path out
+
+end LRAT
+
+end Lean.Elab.Tactic.BVDecide

tests/lean/run/lrat_roundtrip.lean

@@ -0,0 +1,25 @@
+import Lean.Elab.Tactic.BVDecide.LRAT.Parser
+
+open Lean.Elab.Tactic.BVDecide.LRAT
+
+-- This is a nonsensical LRAT proof, merely used for testing.
+def actions : Array IntAction := #[
+  .del #[1, 2, 3, 4],
+  .addRup 10000 #[111111111, -6] #[7, 8],
+  .addRat 10001 #[234234, 13] (234234, true) #[5, 9] #[(500, #[120, 170, 42])],
+  .addEmpty 10002 #[10000, 10001, 42]
+]
+
+/-- info: true -/
+#guard_msgs in
+#eval show IO _ from do
+  match Parser.parseActions.run (lratProofToString actions).toUTF8 with
+  | .ok parsed => return parsed == actions
+  | .error e => throw <| IO.userError e
+
+/-- info: true -/
+#guard_msgs in
+#eval show IO _ from do
+  match Parser.parseActions.run (lratProofToBinary actions) with
+  | .ok parsed => return parsed == actions
+  | .error e => throw <| IO.userError e