{"name":"witness-extraction","lang":"python","entry":"spec-witness-extraction.py","script":"#!/usr/bin/env python3\n\"\"\"\nspec-witness-extraction.py — witness-extraction submission checker (MetaTask\nspec script, protocol v1.2.1 §spec contract). Used by search-kind nodes.\n\nNode shape it judges: \"extract the counterexample witness from the source\nrecord/literature AND re-derive its own factorization certificate with a citable\nprovenance block\" (T1-JSP-000301 node `witness`). This script closes everything\nmachine-checkable about that submission — schema, consecutiveness, provenance\nbinding, certificate validity. The mathematical substance (is this really the\npublished pair, does the locator exist) stays with the review node's\nsemantic_check; the primary witness verification is the proof node's\nspec-powerful-pair.py run, deliberately independent of this one.\n\nInput (stdin, JSON):\n  {\n    \"jsp\": \"JSP-000301\",\n    \"claim\": { \"n\": 12167, \"m\": 12168 },\n    \"provenance\": {\n      \"reference\": \"Solomon W. Golomb, Powerful numbers, Amer. Math. Monthly 77(8) (1970), 848-852\",\n      \"locator\": \"https://doi.org/10.2307/2317020\",\n      \"recordField\": \"JSP-000301 review note (Record correction)\",\n      \"quotedText\": \"... 12167 = 23^3 and 12168 = 2^3 x 3^2 x 13^2 are consecutive powerful numbers ...\"\n    },\n    \"factorization\": { \"n\": [[23, 3]], \"m\": [[2, 3], [3, 2], [13, 2]] }\n  }\nOutput (stdout, JSON): { \"verdict\": \"pass\" | \"fail\" | \"invalid\", \"detail\": \"...\" }\nCriteria (all must hold for pass):\n  1) jsp matches ^JSP-[0-9]{6}$; claim.n and claim.m are integers >= 1 and\n     m == n + 1 (a consecutive pair is the whole point of the node)\n  2) provenance: reference / locator / recordField / quotedText are non-empty\n     strings AND quotedText contains both n and m as decimal substrings — the\n     extraction must bind the pair back to a citable source text\n  3) every factorization entry [p, e]: p prime (deterministic Miller-Rabin,\n     fixed witness set), e >= 2, and the product of all entries equals the\n     labelled value — a powerful witness must exhibit an exponent >= 2 for\n     every prime, not just a plausible-looking pair\nnull/missing input, or a shape that cannot be judged -> verdict=invalid with the\noffending location (protocol null_tolerance criterion).\n\"\"\"\nimport json\nimport re\nimport sys\n\n# Deterministic Miller-Rabin fixed bases (proof-level for n < 3,317,044,064,679,887,385,961,981)\n_WITNESSES = (2, 3, 5, 7, 11, 13, 17, 19, 23, 29, 31, 37)\nJSP_RE = re.compile(r\"^JSP-\\d{6}$\")\n\n\ndef is_prime(n):\n    if not isinstance(n, int) or n < 2:\n        return False\n    for p in _WITNESSES:\n        if n % p == 0:\n            return n == p\n    d, r = n - 1, 0\n    while d % 2 == 0:\n        d //= 2\n        r += 1\n    for a in _WITNESSES:\n        x = pow(a, d, n)\n        if x in (1, n - 1):\n            continue\n        for _ in range(r - 1):\n            x = x * x % n\n            if x == n - 1:\n                break\n        else:\n            return False\n    return True\n\n\ndef check_certificate(pairs, value, label):\n    \"\"\"pairs: [[p, e], ...] -> (primes, error or None). Every exponent must be >= 2.\"\"\"\n    if not isinstance(pairs, list) or not pairs:\n        return None, \"%s: empty factorization certificate\" % label\n    product = 1\n    primes = []\n    for pair in pairs:\n        if not isinstance(pair, list) or len(pair) != 2:\n            return None, \"%s: malformed [p, e] pair %r\" % (label, pair)\n        p, e = pair\n        if not isinstance(p, int) or not isinstance(e, int):\n            return None, \"%s: non-integer pair %r\" % (label, pair)\n        if not is_prime(p):\n            return None, \"%s: %d is not prime\" % (label, p)\n        if e < 2:\n            return None, \"%s: prime %d has exponent %d (< 2) — not a powerful witness\" % (label, p, e)\n        product *= p ** e\n        primes.append(p)\n    if product != value:\n        return None, \"%s: certificate product %d != %d\" % (label, product, value)\n    return primes, None\n\n\ndef emit(verdict, detail, **extra):\n    payload = {\"verdict\": verdict, \"detail\": detail}\n    payload.update(extra)\n    print(json.dumps(payload, ensure_ascii=False))\n    sys.exit(0)\n\n\ndef main():\n    try:\n        raw = json.load(sys.stdin)\n    except Exception as err:\n        emit(\"invalid\", \"input json: %s\" % err)\n    if not isinstance(raw, dict):\n        emit(\"invalid\", \"input must be an object\")\n\n    jsp = raw.get(\"jsp\")\n    if not isinstance(jsp, str) or not JSP_RE.match(jsp):\n        emit(\"invalid\", \"jsp: must be a string matching JSP-######\")\n    claim = raw.get(\"claim\")\n    if not isinstance(claim, dict):\n        emit(\"invalid\", \"claim: missing or not an object\")\n    n, m = claim.get(\"n\"), claim.get(\"m\")\n    if not isinstance(n, int) or not isinstance(m, int) or n < 1 or m < 1:\n        emit(\"invalid\", \"claim.n/claim.m: missing or not integers >= 1\")\n    if m != n + 1:\n        emit(\"fail\", \"claim: not consecutive (m != n + 1)\")\n\n    prov = raw.get(\"provenance\")\n    if not isinstance(prov, dict):\n        emit(\"invalid\", \"provenance: missing or not an object\")\n    for field in (\"reference\", \"locator\", \"recordField\", \"quotedText\"):\n        value = prov.get(field)\n        if not isinstance(value, str) or not value.strip():\n            emit(\"invalid\", \"provenance.%s: missing or empty\" % field)\n    quoted = prov[\"quotedText\"]\n    for label, value in ((\"n\", n), (\"m\", m)):\n        if str(value) not in quoted:\n            emit(\"fail\", \"provenance.quotedText does not contain %s = %d\" % (label, value))\n\n    factors = raw.get(\"factorization\")\n    if not isinstance(factors, dict):\n        emit(\"invalid\", \"factorization: missing or not an object\")\n    primes = []\n    for key, value in ((\"n\", n), (\"m\", m)):\n        cert = factors.get(key)\n        if cert is None:\n            emit(\"invalid\", \"factorization.%s: missing\" % key)\n        found, err = check_certificate(cert, value, key)\n        if err:\n            emit(\"fail\", err)\n        primes.extend(found)\n    print(json.dumps({\n        \"verdict\": \"pass\",\n        \"detail\": \"witness extraction verified: %s n=%d m=%d; provenance bound to %s\"\n                  % (jsp, n, m, prov[\"recordField\"]),\n        \"primeSupport\": sorted(set(primes)),\n        \"expected_count\": len(set(primes)),\n    }, ensure_ascii=False))\n\n\nif __name__ == \"__main__\":\n    main()\n","input":"{\"stdin\": \"one JSON object\", \"fields\": {\"jsp\": \"JSP-######\", \"claim\": {\"n\": \"integer >= 1\", \"m\": \"integer, must equal n + 1\"}, \"provenance\": {\"reference\": \"string, the cited publication of the witness\", \"locator\": \"string, DOI or URL\", \"recordField\": \"string, which bank field or note states the witness\", \"quotedText\": \"string, the quote; must contain both n and m as decimal substrings\"}, \"factorization\": {\"n\": \"[[p, e], ...]\", \"m\": \"[[p, e], ...]\"}}, \"nodeParams\": [\"jsp\", \"witnessSource\"]}","output":"{\"stdout\": \"one JSON object\", \"verdict\": \"pass | fail | invalid\", \"detail\": \"string; the first violated condition\", \"onPass\": \"primeSupport and expected_count (distinct primes), so replay can reconcile the closure\"}","validation":{"enumeration_closure":{"closure":"every prime appearing in the witness's two factorization certificates, with the provenance quote binding the pair back to the cited source text; certificates are checked prime-by-prime (deterministic Miller-Rabin) and every exponent must be >= 2, so a plausible-looking pair without a full support cannot close","count_meaning":"distinct primes across both certificates = |{2, 3, 13, 23}|; the script prints the same integer as expected_count on the pass payload","expected_count":4,"selfcheck":{"expected_verdict":"pass","expected_count":4,"jsp":"JSP-000301","n":12167,"m":12168,"count_meaning":"distinct primes across both certificates = |{2, 3, 13, 23}|; the script prints the same integer as expected_count on the pass payload"}},"note":"Protocol v1.2.1 paths.spec.fields.validation (verbatim): H_ACT2 及以后发布的 spec 必填且三项齐备——null_tolerance（bool：任何分支把 null/缺失输入映射为 verdict=invalid 并在 detail 给出位置，未捕获异常判非合规）；enumeration_closure（object：声明闭包并附至少一个具体自检向量，期望计数须为整数字段供机械对账，如 n=8→28）；proposition_fidelity（object：必须引用独立 correspondence 件（pin://|metafile://）承载逐项对照表——定理陈述／定义／证明方向对齐原始命题；自报布尔判非合规；复核者经 semantic_check 指向该件）","null_tolerance":true,"proposition_fidelity":{"artifactKey":"correspondence-T1-JSP-000301","artifactPin":"metafile://bee0627b78619f3646190e9440520368390d29222e0b06fdba848dfc3dd951a9i0.json","correspondence":"metafile://bee0627b78619f3646190e9440520368390d29222e0b06fdba848dfc3dd951a9i0.json","coverage":["statement","definitions","proof-direction"],"note":"Independent correspondence artifact: wave1-correspondence-artifacts.json#correspondence-T1-JSP-000301. Publish it first and replace the placeholder with its pin://|metafile:// id in BOTH correspondence and artifactPin. A self-declared boolean is non-compliant (the provenance quote is checked against the artifact's record quote)."}}}