# -*- coding: utf-8 -*-
"""
check_draft.py --- check a draft TFK on your own machine with TPC-PY
====================================================================
Advisory. TPX of record decides at the new-UWC gate; this tool runs
the same TPC functions ahead of it so an author sees every refusal before
submitting. Standard library only; Python 3.8+; written for Windows and
Linux. Run on Linux under Python 3.8.20, 3.10, 3.11, 3.12 and 3.13 over
the 11 examples and 86 research drafts, the output the same in each (K5,
2026-09-27); the Windows run is owed.
python3 check_draft.py my_draft.json (Windows: py check_draft.py ...)
The draft is one JSON object with up to three zones:
{"TPK": {...}, "TrM": {...}, "TMS": {...}}
Missing zones are reported and skipped. What it does, in the order TPX
does it (TPS 5.5; tpm_zone_schemas 0.3.0 with schema 0.5.0; tpm_units
0.2.0; tpm_kernel_tests 0.2.0; tpm_increment_8 0.1.0, the declared form;
D176.1 and D177.1, the ROLE fields, the TPK PARAMETERS part with
D_VARIABLES, the TMS switch STRUCTURE_CHECK and the D variable):
1. reads the file as UTF-8 and refuses what is not RFC 8259 JSON
(NaN, Infinity and -Infinity included), duplicate object keys (two
readers could otherwise disagree on which value counts) and nesting
deeper than MAX_DEPTH levels, before any TPC function runs;
2. runs T1 on the TPK (units included: every UNIT parses and has the
DIMENSION of what it measures; every EQUATION and CONDITION parses
and names exactly its REFS; every LAW's ROLE is in its grammar and
EOM(<NAME>) names a DOF; a DOF's ROLE is INPUT; D_VARIABLES is ONE
or SEVERAL; every D variable is a DOF that no CONSTRAINT targets, and
one only under ONE) and, if it passes, the kernel tests T2
(the syntactic part), T5, T4 (over every LAW with an EQUATION) and
T6 (over every BOUNDARY with a CONDITION); a law or boundary without
a form is listed as an inspection, never silently passed;
3. runs the structural check on the TrM against that TPK (a SIGNATURE's
FORM and IMAGE_FORM included) and, if both pass their structure, the
isomorphism checks IC1-IC4 and CODOMAIN, IC4 (a) syntactically where a
signature carries its forms, holding any untied DOF as a named gap;
4. runs the structural check on the TMS, then each yardstick of a
well-formed TMS through the SR9 harness (C1, C2, C4) on the
synthetic record suite;
5. if everything above passes, the final pass: T3 over the constraints
and over the laws with an EQUATION (the ground fragment at depth 1),
and IC2's disposition under the TMS's IC2_POLICY;
6. if the final pass admits the draft, prints the structure check of
its equations of motion (D176.1; tpc_eom): the EOM map (each DOF
with its label and the law the matching gives it, the index and
initial values of the determined part, the closed and invariant
laws), the findings each with its question for the declaring
authority, and the class the candidate certificate's STRUCTURE line
would carry. The map and the findings are shown whatever the TMS's
STRUCTURE_CHECK says (S26); the class line reads the switch, and
under OFF the gate lists nothing for the declaring authority. A
finding refuses nothing (D176.3), so it does not change the exit
status;
7. if the final pass admits the draft, prints D(TPK), D(TrM), D(TMS)
and D(TFK), and lists the checks that stay inspections for the
declaring authority.
Every problem is printed. Exit status 0 when all three zones are present
and every check passes (a named gap under IC2_POLICY GAP passes); 1 when a
zone is missing or a check refuses; 2 when the draft cannot be read or
cannot be checked to the end, and on a usage error. No input ends in a
traceback. The last line names the TPC-PY modules by their own versions: a
TPC-PY version exists only when the declaring authority declares one (TPS
5.11.9).
"""
import json
import os
import sys
HERE = os.path.dirname(os.path.abspath(__file__))
sys.path.insert(0, HERE)
import tpc_zone as Z # noqa: E402
import tpc_yardstick as Y # noqa: E402
import tpc_units as U # noqa: E402
import tpc_tests as K # noqa: E402
import tpc_form as F # noqa: E402
import tpc_eom as E # noqa: E402
CHECK_DRAFT_VERSION = "0.5.0" # proposed MINOR: the structure check after the final pass (D176.1, S26)
# The deepest draft the zone schemas admit nests 7 containers (the draft,
# TMS, YARDSTICKS, a yardstick, LIMITING, a limiting case, KEY); the
# examples reach 6. The loader refuses more before the JSON parser or any
# TPC function recurses into it.
MAX_DEPTH = 64
# What no mechanical body reads (tpm_kernel_tests 0.2.0 sections 2, 12;
# tpm_increment_8 0.1.0). The per-entry inspections a draft owes because an
# entry carries no form are printed beside the checks, from the draft itself.
OWED_INSPECTIONS = [
"T2 the semantic part: each ASSUMPTION states one claim (guide 3.6)",
"T3 over the assumptions, and over the laws beyond the ground fragment at depth 1, to depth S_MAX (guide 3.6)",
"T4, T6 and T3 over every law or boundary without a declared form, as listed beside the kernel tests (D108.1)",
"IC4 (a) that each SIGNATURE image holds in the environment, beyond the syntactic reading, and each borne law is expressible (guide 4.6)",
"IC5 falsifier invariance under the TRANSFORMATIONS (guide 4.6)",
"equivalence of environment quantities under the TRANSFORMATIONS (names are taken as written)",
"every STATEMENT, PROPOSITION, PREDICATE and IMAGE names only what its REFS or OVER list, and agrees with its declared form where one exists",
]
class DuplicateKey(ValueError):
pass
def _no_duplicates(pairs):
d = {}
for k, v in pairs:
if k in d:
raise DuplicateKey("duplicate key " + Z._show(k))
d[k] = v
return d
class NonJsonConstant(ValueError):
pass
def _no_constant(token):
"""json's parse_constant hook: RFC 8259 has no NaN, Infinity or
-Infinity, which Python's json module would otherwise accept."""
raise NonJsonConstant(token)
def _where(text, i):
"""The position as json reports it: line, column, char."""
return "line %d column %d (char %d)" % (text.count("\n", 0, i) + 1, i - text.rfind("\n", 0, i), i)
def _scan(text):
"""One linear pass over the raw text, outside strings: [the index of
the first bracket opened deeper than MAX_DEPTH, the index of the first
N or I]. Either is None when absent. Outside strings in text JSON has
read, an N or an I can only begin NaN or Infinity."""
depth, in_str, esc, const = 0, False, False, None
for i, ch in enumerate(text):
if in_str:
if esc:
esc = False
elif ch == "\\":
esc = True
elif ch == '"':
in_str = False
elif ch == '"':
in_str = True
elif ch == "[" or ch == "{":
depth += 1
if depth > MAX_DEPTH:
return [i, const]
elif ch == "]" or ch == "}":
depth -= 1
elif const is None and (ch == "N" or ch == "I"):
const = i - 1 if i > 0 and text[i - 1] == "-" else i
return [None, const]
def load_draft(path):
"""The draft as a dict, or raises ValueError with a readable reason.
utf-8-sig accepts the byte-order mark some Windows editors write. The
nesting bound is checked on the raw text, so the parser never recurses
past it; only the text before the first too-deep bracket is parsed,
and a problem found there is reported first, as the file's first."""
with open(path, "r", encoding="utf-8-sig") as f:
text = f.read()
deep, const = _scan(text)
try:
draft = json.loads(text if deep is None else text[:deep],
object_pairs_hook=_no_duplicates, parse_constant=_no_constant)
except NonJsonConstant as e:
raise ValueError("%s is not JSON (RFC 8259 has no NaN, Infinity or -Infinity)%s"
% (e, "" if const is None else ": " + _where(text, const)))
except json.JSONDecodeError as e:
if deep is None or e.pos < deep:
raise
except RecursionError:
raise ValueError("nesting deeper than the checker reads")
else:
if deep is not None: # a whole value, then a bracket: what json calls extra data
raise ValueError("Extra data: " + _where(text, deep))
if deep is not None:
raise ValueError("nesting deeper than the checker reads (more than %d levels): %s"
% (MAX_DEPTH, _where(text, deep)))
if not isinstance(draft, dict):
raise ValueError("the draft must be one JSON object")
return draft
def _count(n, word):
return "%d %s%s" % (n, word, "" if n == 1 else "s")
def _result(out, label, passed, probs):
if passed == "NO FORM":
out("%s NO FORM (by inspection)" % label)
return
out("%s %s" % (label, "PASS" if passed else "REFUSED, " + _count(len(probs), "problem")))
for p in probs:
out(" " + p)
def _structure(draft, out):
"""The structure check of the equations of motion, after the final pass
(D176.1; S26): the map and the findings whatever the switch says, then
the class, which reads the switch. Information: nothing here refuses."""
m = E.eom_map(draft)
if m[0] != "OK":
out("STRUCTURE not computed: " + m[1])
return
r = dict((row[0], row[1:]) for row in m[1])
dv = r["D_VARIABLES"][0]
out("STRUCTURE map (shown whatever STRUCTURE_CHECK says): analysis " + r["ANALYSIS"][0]
+ ("; D variable" + ("s " if len(dv) != 1 else " ") + ", ".join(dv) if dv else "; no D variable"))
for dof, label, law in r["MAP"][0]:
out(" %s: %s%s" % (dof, label, " (LAW " + law + ")" if law else ""))
if r["INDEX"][0] == "NONE":
out(" index and initial values: not computed")
else:
out(" index %s, initial values %s (the determined part; information)" % (r["INDEX"][0], r["INITIAL_VALUES"][0]))
if r["CLOSED"][0]:
out(" closed: " + ", ".join("%s (%s)" % (law, kind) for law, kind in r["CLOSED"][0]))
if r["INVARIANT"][0]:
out(" invariant, outside the matching: " + ", ".join(r["INVARIANT"][0]))
f = E.eom_findings(draft)
if f[0] != "OK":
out("STRUCTURE findings not computed: " + f[1])
return
c = E.eom_class(draft)
off = c[0] == "STRUCTURE" and len(c) > 2 and c[2] == ["CHECK OFF"]
head = "STRUCTURE findings" + (" (information: under STRUCTURE_CHECK OFF the gate lists none)" if off else "")
out(head + ": " + (str(len(f[1])) if f[1] else "none"))
for fd in f[1]:
out(" " + fd[0] + ": " + (fd[-1] + " (D variables " + ", ".join(fd[1]) + ")" if fd[0] == "PDE" else fd[-1]))
if c[0] != "STRUCTURE":
out("STRUCTURE class not computed: " + c[1])
elif len(c) == 2:
out("STRUCTURE " + c[1])
else:
out("STRUCTURE " + c[1] + ": " + ", ".join(c[2]))
def check(draft, out):
ok = all(z in draft for z in ("TPK", "TrM", "TMS"))
for k in sorted(draft):
if k not in ("TPK", "TrM", "TMS"):
out("DRAFT: unknown zone " + Z._show(k))
ok = False
tpk, trm, tms = draft.get("TPK"), draft.get("TrM"), draft.get("TMS")
t1_ok = kt_ok = trm_ok = ic_ok = tms_ok = False
# the Prime Kernel: T1, then T2 and T5
if "TPK" not in draft:
out("TPK MISSING (not checked)")
else:
kt = K.kernel_tests(tpk)
t1_ok = kt[1][0][1] is True
_result(out, "TPK ", t1_ok, kt[1][0][2])
if t1_ok:
for name, passed, probs in kt[1][1:]:
_result(out, " " + name, passed if passed == "NO FORM" else passed is True, probs)
for i in kt[2]:
out(" inspection " + i)
kt_ok = kt[0] is True
ok = ok and kt_ok
# the Translation Manifold: structure, then IC1-IC4 and CODOMAIN
if "TrM" not in draft:
out("TrM MISSING (not checked)")
else:
r = Z.trm_well_formed(trm, draft.get("TPK", {}))
trm_ok = r[0]
_result(out, "TrM ", trm_ok, r[1])
ok = ok and trm_ok
if trm_ok and not t1_ok:
out(" IC1-IC4 not run: the TPK " + ("does not pass T1" if "TPK" in draft else "is missing"))
elif trm_ok:
ic = K.ic_checks(trm, tpk)
if ic[0] == "REJECT":
_result(out, " IC1-IC4", False, ic[1])
elif ic[0] == "GAP":
out(" IC1-IC4 PASS with " + _count(len(ic[2]), "untied DOF")
+ ", held for the final pass")
elif ic[0] == "PASS":
out(" IC1-IC4 PASS")
else:
out(" IC1-IC4 not run: " + "; ".join(ic[1]))
if ic[0] == "REJECT" and ic[2]:
out(" and " + _count(len(ic[2]), "untied DOF") + ", held for the final pass")
for g in (ic[2] if ic[0] in ("REJECT", "GAP") else []):
out(" " + g)
if ic[0] != "NOT_RUN":
for u in F.ic4a_signature(trm, tpk)[2]:
out(" inspection " + u)
for sg in trm["HEADER"].get("SIGNATURE", []):
if "FORM" not in sg:
out(" inspection SIGNATURE:" + sg["NAME"] + ": no FORM; IC4 (a) by inspection")
ic_ok = ic[0] in ("PASS", "GAP")
ok = ok and ic_ok
# the Measure Set: structure, then each yardstick through SR9
if "TMS" not in draft:
out("TMS MISSING (not checked)")
else:
r = Z.tms_well_formed(tms)
tms_ok = r[0]
_result(out, "TMS ", tms_ok, r[1])
ok = ok and tms_ok
if tms_ok:
suite = json.load(open(os.path.join(HERE, "vectors", "sr9_corpus.json"), encoding="utf-8"))["cases"][0]["input"]["suite"]
for y in tms.get("YARDSTICKS", []):
r = Y.yardstick_checks(tms, y["NAME"], suite)
if r[0] != "OK":
out("YARDSTICK %s: REFUSED, %s" % (y["NAME"], r[1]))
ok = False
continue
c1, c2, c4 = r[1], r[2], r[3]
line = "YARDSTICK %s: C1 %s, C2 %s, C4 %s" % (
y["NAME"], "pass" if c1[0] else "FAIL", "pass" if c2[0] else "FAIL", "pass" if c4[0] else "FAIL")
if c2[2]:
line += "; exempt in a declared limiting DOMAIN: " + ", ".join(c2[2])
out(line)
for w in c1[1] + c2[1] + c4[1]:
out(" witness " + w)
ok = ok and c1[0] and c2[0] and c4[0]
# the final pass: T3 and IC2's disposition
if not all(z in draft for z in ("TPK", "TrM", "TMS")):
out("FINAL not run: a zone is missing")
elif not ok:
out("FINAL not run: it runs once every check above passes")
else:
fin = K.final_checks(draft)
if fin[0] == "PASS":
out("FINAL T3 (constraints and laws) and IC2 PASS")
elif fin[0] == "GAP":
out("FINAL T3 (constraints and laws) and IC2 PASS, admitted with " + _count(len(fin[2]), "named gap")
+ " (IC2_POLICY GAP)")
for g in fin[2]:
out(" " + g)
elif fin[0] == "REJECT":
_result(out, "FINAL T3 (constraints and laws) and IC2", False, fin[1])
else:
out("FINAL not run: " + "; ".join(fin[1]))
ok = fin[0] in ("PASS", "GAP")
if ok:
_structure(draft, out)
if ok:
out("")
out("D(TPK) " + Z.d_tpk(tpk))
out("D(TrM) " + Z.d_trm(trm))
out("D(TMS) " + Z.d_tms(tms))
out("D(TFK) " + Z.d_tfk_of(draft))
out("")
out("Inspections still owed to the declaring authority before declaring:")
for i in OWED_INSPECTIONS:
out(" - " + i)
out("")
out("Advisory result (TPC-PY: tpc_zone %s, tpc_units %s, tpc_tests %s, tpc_form %s, tpc_eom %s; schema %s). "
"TPX decides at the gate." % (Z.TPC_ZONE_VERSION, U.TPC_UNITS_VERSION, K.TPC_TESTS_VERSION, F.TPC_FORM_VERSION,
E.TPC_EOM_VERSION, Z.SCHEMA_VERSION))
return ok
def main(argv):
if hasattr(sys.stdout, "reconfigure"):
sys.stdout.reconfigure(errors="backslashreplace")
if len(argv) != 2:
print("usage: check_draft.py DRAFT.json")
return 2
try:
draft = load_draft(argv[1])
except (OSError, ValueError) as e:
print("DRAFT: cannot be read: " + str(e))
return 2
except MemoryError:
print("DRAFT: cannot be read: the file does not fit in memory")
return 2
try:
return 0 if check(draft, print) else 1
except RecursionError:
print("DRAFT: not checked to the end: a value nests deeper than TPC-PY's checks read"
" (RecursionError), such as a deeply nested EQUATION, CONDITION, FORM or IMAGE_FORM;"
" TPX decides at the gate")
return 2
except MemoryError:
print("DRAFT: not checked to the end: out of memory in the checks; TPX decides at the gate")
return 2
if __name__ == "__main__":
sys.exit(main(sys.argv))
