{"name":"jsp82-pow2-cycle-hunt-verifier","lang":"python3","entry":"spec-jsp82.py","script":"#!/usr/bin/env python3\n\"\"\"JSP-000082 verifier — \"does every graph of minimum degree >= 3 contain a cycle\nwhose length is a power of 2?\" hunt campaign.\n\nInput  (protocol spec contract):\n  argv[1] = submission directory containing the result JSON (find.json | result.json\n            | the single *.json in that directory), OR the result JSON on stdin.\nOutput:\n  one JSON object on stdout: {\"verdict\": \"pass\"|\"fail\"|\"invalid\", \"reason\": str}\n  exit 0 iff verdict == \"pass\".\n\nAccepted submission forms (see correspondence pin):\n  A) {\"type\":\"witness\",\"n\":N,\"edges\":[[u,v],...]}\n     pass iff, recomputed from scratch: simple graph, min degree >= 3,\n     and no cycle whose length is in {4,8,16,32,...} <= N (lengths 1 and 2 are\n     impossible in a simple graph, so the first admissible length is 4).\n  B) {\"type\":\"negative\",\"from\":A,\"to\":B,\"script_python\":\"<source>\",\"method\":\"...\"}\n     pass iff the verifier can rerun the submitted pure-python3 search script on a\n     sampled sub-interval and the rerun reports no counterexample. The rerun is a\n     sample, not a full replay: the full-range claim stays with the reviewers.\n\nTest-only option: --pow2-only L restricts the power-of-two length set to {L}; it\nexists so the pass branch can be self-tested (see validation block) and must not\nbe used by the harness.\n\"\"\"\nimport json\nimport os\nimport re\nimport subprocess\nimport sys\nimport tempfile\n\nPOW2_MAX_LEN = 4096\n\n\ndef emit(verdict, reason):\n    print(json.dumps({\"verdict\": verdict, \"reason\": reason}, ensure_ascii=False))\n    sys.exit(0 if verdict == \"pass\" else 1)\n\n\ndef load_result():\n    args = [a for a in sys.argv[1:] if not a.startswith(\"--\")]\n    if args:\n        path = args[0]\n        if os.path.isfile(path):\n            try:\n                return json.load(open(path, encoding=\"utf-8\"))\n            except Exception as e:  # noqa: BLE001\n                emit(\"invalid\", \"unparseable submission file: %s\" % e)\n        if os.path.isdir(path):\n            for name in (\"find.json\", \"result.json\"):\n                f = os.path.join(path, name)\n                if os.path.isfile(f):\n                    try:\n                        return json.load(open(f, encoding=\"utf-8\"))\n                    except Exception as e:  # noqa: BLE001\n                        emit(\"invalid\", \"unparseable %s: %s\" % (name, e))\n            cands = sorted(f for f in os.listdir(path) if f.endswith(\".json\"))\n            if len(cands) == 1:\n                try:\n                    return json.load(open(os.path.join(path, cands[0]), encoding=\"utf-8\"))\n                except Exception as e:  # noqa: BLE001\n                    emit(\"invalid\", \"unparseable %s: %s\" % (cands[0], e))\n            emit(\"invalid\", \"no result JSON found in submission directory\")\n    raw = sys.stdin.read()\n    if not raw.strip():\n        emit(\"invalid\", \"no submission path and empty stdin\")\n    try:\n        return json.loads(raw)\n    except Exception as e:  # noqa: BLE001\n        emit(\"invalid\", \"unparseable stdin JSON: %s\" % e)\n\n\ndef pow2_lengths(n, only=None):\n    if only:\n        return [only] if only <= n else []\n    out, L = [], 4\n    while L <= min(n, POW2_MAX_LEN):\n        out.append(L)\n        L *= 2\n    return out\n\n\ndef build_adj(n, edges):\n    adj = [set() for _ in range(n)]\n    for e in edges:\n        if not (isinstance(e, (list, tuple)) and len(e) == 2):\n            emit(\"invalid\", \"edge is not a pair: %r\" % (e,))\n        u, v = e\n        if not (isinstance(u, int) and isinstance(v, int)):\n            emit(\"invalid\", \"non-integer edge endpoint: %r\" % (e,))\n        if u == v:\n            emit(\"invalid\", \"self-loop at %d\" % u)\n        if not (0 <= u < n and 0 <= v < n):\n            emit(\"invalid\", \"edge out of range: %r\" % (e,))\n        if v in adj[u]:\n            emit(\"invalid\", \"duplicate edge: %r\" % (e,))\n        adj[u].add(v)\n        adj[v].add(u)\n    return adj\n\n\ndef has_cycle_of_length(adj, L):\n    \"\"\"Return a vertex list of a simple cycle of length exactly L, else None.\"\"\"\n    n = len(adj)\n    if L < 3 or L > n:\n        return None\n\n    def dfs(start, v, path, seen):\n        if len(path) == L:\n            return path if start in adj[v] else None\n        for w in sorted(adj[v]):\n            if w < start or w in seen:\n                continue\n            seen.add(w)\n            path.append(w)\n            got = dfs(start, w, path, seen)\n            if got:\n                return got\n            path.pop()\n            seen.discard(w)\n        return None\n\n    for s in range(n):\n        got = dfs(s, s, [s], {s})\n        if got:\n            return got\n    return None\n\n\ndef check_witness(d, only=None):\n    n = d.get(\"n\")\n    edges = d.get(\"edges\")\n    if not isinstance(n, int) or n < 4:\n        emit(\"invalid\", \"field n must be an integer >= 4\")\n    if n > 40:\n        emit(\"invalid\", \"n=%d exceeds the mechanical verifier limit (40); state the limit in the submission\" % n)\n    if not isinstance(edges, list):\n        emit(\"invalid\", \"field edges must be a list of pairs\")\n    adj = build_adj(n, edges)\n    deg = [len(a) for a in adj]\n    low = [i for i, x in enumerate(deg) if x < 3]\n    if low:\n        emit(\"fail\", \"minimum degree violated at vertices %s (degrees %s)\" % (low[:8], [deg[i] for i in low[:8]]))\n    test = pow2_lengths(n, only)\n    if not test:\n        emit(\"fail\", \"n=%d admits no admissible power-of-two cycle length\" % n)\n    for L in test:\n        cyc = has_cycle_of_length(adj, L)\n        if cyc:\n            emit(\"fail\", \"graph has a cycle of length %d (a power of two): %s\" % (L, cyc))\n    return \"recomputed from scratch: n=%d, %d edges, min degree %d, no cycle of length in %s\" % (\n        n, len(edges), min(deg), test)\n\n\ndef check_negative(d):\n    src = d.get(\"script_python\")\n    a, b = d.get(\"from\"), d.get(\"to\")\n    if not isinstance(src, str) or not src.strip():\n        emit(\"invalid\", \"field script_python (self-contained python3 source) is required for a negative record\")\n    if not (isinstance(a, int) and isinstance(b, int)) or b <= a:\n        emit(\"invalid\", \"fields from/to must be integers with from < to\")\n    hi = min(b, a + 2000)\n    with tempfile.TemporaryDirectory() as td:\n        p = os.path.join(td, \"search.py\")\n        open(p, \"w\", encoding=\"utf-8\").write(src)\n        try:\n            r = subprocess.run([sys.executable, p, str(a), str(hi)], capture_output=True, text=True, timeout=300)\n        except subprocess.TimeoutExpired:\n            emit(\"fail\", \"sampled rerun timed out over [%d,%d]\" % (a, hi))\n    if r.returncode != 0:\n        emit(\"fail\", \"sampled rerun exited %d: %s\" % (r.returncode, (r.stderr or \"\")[-400:]))\n    out = (r.stdout or \"\").strip()\n    if not out:\n        emit(\"invalid\", \"sampled rerun produced no output; the script must print a JSON line\")\n    line = out.splitlines()[-1]\n    try:\n        j = json.loads(line)\n    except Exception:  # noqa: BLE001\n        m = re.search(r'\\{.*\\}', out, re.S)\n        if not m:\n            emit(\"invalid\", \"sampled rerun output is not JSON: %s\" % out[-200:])\n        try:\n            j = json.loads(m.group(0))\n        except Exception:  # noqa: BLE001\n            emit(\"invalid\", \"sampled rerun output is not JSON: %s\" % out[-200:])\n    ce = j.get(\"counterexamples\")\n    if ce is None and \"found\" in j:\n        ce = j[\"found\"] if isinstance(j[\"found\"], list) else []\n    if ce:\n        emit(\"fail\", \"sampled rerun FOUND a counterexample the record suppressed: %s\" % json.dumps(ce)[:300])\n    return \"sampled rerun clean over [%d,%d]; full-range claim remains with the reviewers\" % (a, hi)\n\n\ndef main():\n    only = None\n    for a in sys.argv[1:]:\n        m = re.match(r\"--pow2-only=(\\d+)$\", a)\n        if m:\n            only = int(m.group(1))\n    d = load_result()\n    if not isinstance(d, dict):\n        emit(\"invalid\", \"submission must be a JSON object\")\n    t = d.get(\"type\")\n    if t == \"witness\":\n        emit(\"pass\", check_witness(d, only))\n    if t == \"negative\":\n        emit(\"pass\", check_negative(d))\n    emit(\"invalid\", \"unknown or missing type: %r (expected 'witness' or 'negative')\" % (t,))\n\n\nif __name__ == \"__main__\":\n    main()\n","input":"argv[1] = submission directory containing find.json (or result.json / the single *.json), or the same JSON on stdin. Forms: {type:witness,n,edges} | {type:negative,from,to,script_python}","output":"single-line JSON {verdict: pass|fail|invalid, reason}; exit 0 iff pass","validation":{"null_tolerance":true,"enumeration_closure":{"closure":"for a witness, the complete cycle-length set {4,8,16,32,...} n [4,N] is enumerated by the verifier from scratch (so the verdict is a function of every admissible length, not a subset); for a negative record the replayed domain is the sampled sub-interval [A, min(B,A+2000)] of the declared [A,B]","count_meaning":"number of harness self-check fixtures executed pre-publish","selfCheckCount":9,"selfChecks":["Petersen graph (3-regular, girth 5) -> fail, hits cycle of length 8 [0,1,2,3,4,9,7,5]","Petersen with length set restricted to {4} (test-only switch) -> pass: exercises the pass branch","C5 -> fail: minimum degree violated (degrees [2,2,2,2,2])","K4 -> fail, hits cycle of length 4 [0,1,2,3]","self-loop edge -> invalid","duplicate edge -> invalid","unknown type -> invalid","negative with honest script -> pass (sampled rerun clean over [4,2004])","negative with script that finds a counterexample -> fail (suppressed counterexample surfaced)"]},"proposition_fidelity":{"artifact":"pin://d0a9b29d121588c93fc227aa4ace87c66bc83e2b6f0df5204bf3d582272385d2i0","note":"the correspondence pin records the official question verbatim, the admissible power-of-two length set, both submission forms and the honest negative-claim clause; the script was checked against that text fixture by fixture"}}}