"""CAIN-A75-005 offline verifier (rules embedded verbatim). CAIN-A75-005 research-provenance rules. Standard library only, no CAIN imports: embedded verbatim in the offline verifier. A multi-agent research programme is a ledger of agents (with the operator each one belongs to) and claims. Each claim has an author agent, a kind (CONJECTURE, LEMMA, THEOREM, CONSTRUCTION), dependencies on other claims, evidence and reviews. The rules compute what the ledger actually establishes and compare it with what the programme says: graph dependencies exist and form no cycle; every author is a registered agent evidence CONSTRUCTION evidence is RE-CHECKED EXACTLY here for the supported families: sidon_set a set A in [1, N] whose pairwise sums a + b (a <= b) are all distinct, |A| = claimed size ramsey_graph a graph on n vertices with no clique of size s and no independent set of size t formal_proof evidence is EXTERNAL: its checker and artifact hash are recorded, not re-checked here none nothing to check status ESTABLISHED own evidence re-checks exactly and every dependency is ESTABLISHED EXTERNAL relies on an external formal proof (itself or a dependency), nothing refuted CONDITIONAL depends (directly or not) on a CONJECTURE or on a claim without evidence REFUTED its construction fails the exact check, or it depends on a REFUTED claim reviews a review counts as independent only if the reviewer is a registered agent with a different operator than the author, and the review's claim_sha256 matches the claim as it is now (no stale reviews) honesty every claim the programme's summary lists as "established" must compute to ESTABLISHED; every THEOREM / CONSTRUCTION listed as established needs at least one independent, current review Verdict: CONSISTENT, or INCONSISTENT with every failing check named. Malformed input is INCONSISTENT. Exact checks are bounded (sidon N <= 100000 and |A| <= 400; ramsey n <= 22 and s, t <= 6) so a review always ends. """ from __future__ import annotations import hashlib import json import math import re from itertools import combinations KINDS = {"CONJECTURE", "LEMMA", "THEOREM", "CONSTRUCTION"} _ID = re.compile(r"^[A-Za-z0-9_.:\-]{1,80}$") _HEX = re.compile(r"^[0-9a-f]{64}$") class Bad(ValueError): pass def claim_hash(cl): body = {k: v for k, v in cl.items() if k != "reviews"} return hashlib.sha256(json.dumps(body, sort_keys=True, separators=(",", ":"), ensure_ascii=True).encode()).hexdigest() def _int(v, what, lo=0, hi=10 ** 9): if isinstance(v, bool) or not isinstance(v, int) or not (lo <= v <= hi): raise Bad(f"{what} must be an integer in [{lo}, {hi}]") return v def check_sidon(obj): N = _int(obj.get("N"), "sidon.N", 1, 100_000) A = obj.get("set") if not isinstance(A, list) or not (1 <= len(A) <= 400): raise Bad("sidon.set must be a list of 1-400 integers") A = [_int(a, "sidon element", 1, N) for a in A] if len(set(A)) != len(A): return False, "elements repeat" sums = set() for i, a in enumerate(A): for b in A[i:]: s = a + b if s in sums: return False, f"two pairs share the sum {s}" sums.add(s) size = obj.get("claimed_size") if size != len(A): return False, f"claimed size {size!r} but the set has {len(A)} elements" return True, f"{len(A)} elements in [1, {N}], all {len(sums)} pairwise sums distinct" def check_ramsey(obj): n = _int(obj.get("n"), "ramsey.n", 2, 22) s, t = _int(obj.get("s"), "ramsey.s", 2, 6), _int(obj.get("t"), "ramsey.t", 2, 6) E = obj.get("edges") if not isinstance(E, list): raise Bad("ramsey.edges must be a list of [u, v] pairs") adj = [[False] * n for _ in range(n)] for e in E: if not (isinstance(e, list) and len(e) == 2): raise Bad("an edge is [u, v]") u, v = _int(e[0], "vertex", 0, n - 1), _int(e[1], "vertex", 0, n - 1) if u == v: raise Bad("no self-loops") adj[u][v] = adj[v][u] = True for S in combinations(range(n), s): if all(adj[a][b] for a, b in combinations(S, 2)): return False, f"clique of size {s}: {list(S)}" for T in combinations(range(n), t): if not any(adj[a][b] for a, b in combinations(T, 2)): return False, f"independent set of size {t}: {list(T)}" return True, f"graph on {n} vertices: no K{s} and no independent {t}-set (so R({s},{t}) > {n})" CHECKERS = {"sidon_set": check_sidon, "ramsey_graph": check_ramsey} def evaluate(ledger): checks, summary = [], {"status": {}, "construction_checks": {}} def c(cid, ok, detail=""): checks.append({"id": cid, "ok": bool(ok), "detail": detail}) return ok try: if not isinstance(ledger, dict) or ledger.get("schema") != "cain42.a75.research.ledger.v1": raise Bad("not a cain42.a75.research.ledger.v1 ledger") agents = ledger.get("agents") claims = ledger.get("claims") if not isinstance(agents, list) or not isinstance(claims, list) or not claims or len(claims) > 500: raise Bad("agents and claims (1-500) must be lists") A = {} for a in agents: if not isinstance(a, dict) or not isinstance(a.get("id"), str) or not _ID.match(a["id"]) or not isinstance(a.get("operator"), str): raise Bad("an agent needs an id and an operator") A[a["id"]] = a["operator"] C = {} for cl in claims: if not isinstance(cl, dict) or not isinstance(cl.get("id"), str) or not _ID.match(cl["id"]): raise Bad("a claim needs an id") if cl["id"] in C: raise Bad(f"duplicate claim id {cl['id']}") if cl.get("kind") not in KINDS: raise Bad(f"{cl['id']}: kind must be one of {sorted(KINDS)}") C[cl["id"]] = cl for cid, cl in C.items(): c(f"{cid}.author_registered", cl.get("author") in A, f"author {cl.get('author')!r}") deps = cl.get("depends_on", []) c(f"{cid}.dependencies_exist", isinstance(deps, list) and all(d in C for d in deps), f"depends on {deps}") # cycles state = {} def visit(x, stack): if state.get(x) == 1: return True if state.get(x) == 2: return False state[x] = 1 for d in (C[x].get("depends_on") or []): if d in C and visit(d, stack): return True state[x] = 2 return False cyc = sorted(x for x in C if visit(x, []) or state.get(x) == 1) c("graph.acyclic", not any(state.get(x) == 1 for x in C), "no claim depends on itself" if not cyc else f"cycle through {cyc}") # own evidence own = {} for cid, cl in C.items(): ev = cl.get("evidence") if isinstance(cl.get("evidence"), dict) else {"type": "none"} t = ev.get("type") if t == "construction": fam = ev.get("family") if fam not in CHECKERS: c(f"{cid}.construction_family", False, f"family {fam!r} has no exact checker here") own[cid] = "UNCHECKABLE" continue ok, why = CHECKERS[fam](ev.get("object") if isinstance(ev.get("object"), dict) else {}) summary["construction_checks"][cid] = why own[cid] = "OK" if ok else "FAILED" elif t == "formal_proof": c(f"{cid}.formal_proof_recorded", isinstance(ev.get("checker"), str) and isinstance(ev.get("artifact_sha256"), str) and bool(_HEX.match(ev["artifact_sha256"])), "an external proof records its checker and the SHA-256 of the proof artifact") own[cid] = "EXTERNAL" else: own[cid] = "NONE" if cl["kind"] == "CONSTRUCTION": c(f"{cid}.construction_has_construction", t == "construction", "a CONSTRUCTION must carry the object") # status through the graph (memoised; acyclic was checked above, guard anyway) memo = {} def status(x, depth=0): if x in memo: return memo[x] if depth > 600 or x not in C: return "CONDITIONAL" cl = C[x] deps = [status(d, depth + 1) for d in (cl.get("depends_on") or []) if d in C] if own[x] == "FAILED" or "REFUTED" in deps: s = "REFUTED" elif cl["kind"] == "CONJECTURE" or own[x] in ("NONE", "UNCHECKABLE") or "CONDITIONAL" in deps: s = "CONDITIONAL" elif own[x] == "EXTERNAL" or "EXTERNAL" in deps: s = "EXTERNAL" else: s = "ESTABLISHED" memo[x] = s return s if not any(state.get(x) == 1 for x in C): for x in C: summary["status"][x] = status(x) # reviews indep = {} for cid, cl in C.items(): h = claim_hash(cl) n = 0 for r in cl.get("reviews") or []: if not isinstance(r, dict): continue rv = r.get("by") current = r.get("claim_sha256") == h independent = rv in A and A.get(rv) != A.get(cl.get("author")) and rv != cl.get("author") if r.get("verdict") == "accept" and current and independent: n += 1 indep[cid] = n # honesty: what the programme says vs what the ledger establishes said = ledger.get("summary", {}).get("established") if isinstance(ledger.get("summary"), dict) else None if not isinstance(said, list): raise Bad("summary.established must be a list of claim ids") for cid in said: st = summary["status"].get(cid, "UNKNOWN") c(f"summary.{cid}.is_established", st == "ESTABLISHED", f"the programme calls it established; the ledger gives {st}") if cid in C and C[cid]["kind"] in ("THEOREM", "CONSTRUCTION"): c(f"summary.{cid}.independently_reviewed", indep.get(cid, 0) >= 1, f"{indep.get(cid, 0)} independent, current accepting review(s)") summary["independent_reviews"] = indep except Bad as e: checks.append({"id": "input.well_formed", "ok": False, "detail": str(e)}) return "INCONSISTENT", checks, summary except Exception as e: # noqa: BLE001 checks.append({"id": "input.error", "ok": False, "detail": f"{type(e).__name__}: {e}"[:200]}) return "INCONSISTENT", checks, summary return ("CONSISTENT" if all(x["ok"] for x in checks) else "INCONSISTENT"), checks, summary # ---------------------------------------------------------------------------- offline verifier (no CAIN imports) # Every name below is prefixed _kit_verifier_ / _b64 / _hl / _json / _sys so it cannot shadow a name in the rules above. import base64 as _b64, hashlib as _hl, json as _json, sys as _sys _KIT_VERIFIER_GENESIS = _hl.sha256(b"cain42.a75.research.genesis").hexdigest() def _kit_verifier_canon(o): return _json.dumps(o, sort_keys=True, separators=(",", ":"), ensure_ascii=True).encode() def _kit_verifier_sha(o): return _hl.sha256(_kit_verifier_canon(o)).hexdigest() def _kit_verifier_main(argv): from cryptography.hazmat.primitives.asymmetric.ed25519 import Ed25519PublicKey if len(argv) < 2: print("usage: verify_offline.py run.json --pinned-key BASE64"); return 2 run = _json.load(open(argv[1])) pin = argv[argv.index("--pinned-key") + 1] if "--pinned-key" in argv else None problems, prev, recs = [], _KIT_VERIFIER_GENESIS, run.get("records") or [] for i, r in enumerate(recs): body = {k: v for k, v in r.items() if k not in ("record_hash", "signature_b64")} if _kit_verifier_sha(body) != r.get("record_hash"): problems.append(f"record {i}: record_hash does not match") if body.get("subject_sha256") != _kit_verifier_sha(body.get("subject")): problems.append(f"record {i}: subject_sha256 does not match") if pin and r.get("public_key_b64") != pin: problems.append(f"record {i}: different key than the pinned one") try: Ed25519PublicKey.from_public_bytes(_b64.b64decode(pin or r.get("public_key_b64"))).verify( _b64.b64decode(r.get("signature_b64", "")), str(r.get("record_hash")).encode()) except Exception: problems.append(f"record {i}: signature does not verify") if r.get("prev_record_hash") != prev: problems.append(f"record {i}: chain link broken") v, checks, _ = evaluate(r.get("subject")) if v != r.get("verdict") or checks != r.get("checks"): problems.append(f"record {i}: re-running the rules gives {v}, the record says {r.get('verdict')}") prev = r.get("record_hash") if run.get("run_hash") != _kit_verifier_sha([r.get("record_hash") for r in recs]): problems.append("run_hash does not match") for p in problems: print(" -", p) if not pin: print("WARNING: no --pinned-key given; the signature was checked against the key inside the file") print("VERDICT:", "VERIFIED" if not problems else "TAMPERED OR INVALID", f"(CAIN-A75-005, {len(recs)} record(s), verdicts {run.get('verdicts')})") return 0 if not problems else 1 if __name__ == "__main__": _sys.exit(_kit_verifier_main(_sys.argv))