# -*- coding: utf-8 -*-
"""
TPC-PY --- kernel tests T2, T3, T4, T5, T6 and the isomorphism checks
IC1-IC4 (TPC step 2, increments 7 and 8) --- SELECTED D106.1, D107.1,
D108.1; increment 8 at Option 1 of every slot (2026-09-24)
======================================================================
SELECTED 2026-09-22: D106.1 (the T2 syntactic rule below), D107.1 (the
inventory the TrM maps onto: the DOF less REMOVE targets), D108.1 (an
OPTIONAL declared expression form). INCREMENT 8 (2026-09-24): the form
exists (tpc_form): where a LAW carries EQUATION, T4's law half and T3 over
laws (the ground fragment) are MECHANICAL; where a BOUNDARY carries
CONDITION, T6's totality is; where a SIGNATURE carries FORM and
IMAGE_FORM, IC4 (a) is, syntactically; the names check is T1's. Where a
form is absent the part stays INSPECTION by H-DECL and is reported so,
never silently passed. Spec: tpm_kernel_tests 0.2.0 section 12,
tpm_increment_8 0.1.0. Standard library only; Python 3.8+; Windows/Linux.
WHAT IS MECHANICAL HERE, AND WHY (guide 3.6, 4.6; TPS 2.2.3, 2.3.7-2.3.15):
Under the D98 schema, statements, propositions and predicates are prose;
names, citations (REFS, TARGET), dimensions, units and classes are fields.
A check is mechanical exactly where it reads fields only.
T1 tpc_zone.t1_well_formed (increment 4). It also discharges T4's
constraint half (a FIX's UNIT against its TARGET's DIMENSION,
D104.1), T5 (a) (every REFS member resolves to a DOF or CONSTANT)
and T6's mechanical clause (a boundary names DOF and CONSTANTs only).
T2 the syntactic part: an ASSUMPTION's PROPOSITION is not a top-level
conjunction, list or joined pair of claims (D106.1).
The semantic part stays INSPECTION by the guide's classing.
T3 the executable fragment: CONSTRAINT entries. Two FIX of one TARGET
at different values, or a FIX and a REMOVE of one TARGET, are P and
not-P at depth 1 <= S_MAX. Over the laws, the ground fragment of
tpc_form.t3_laws where a LAW carries EQUATION; assumptions, and laws
without a form, stay INSPECTION.
T4 the law half, tpc_form.t4_homogeneity, where a LAW carries EQUATION;
a law without one stays INSPECTION and is listed.
T5 (b) a CONSTRAINT's TARGET is named by at least one LAW, else no law
leaves it free and the constraint is void; (c) every DOF is named by
at least one LAW, else it is idle.
T6 totality, tpc_form.t6_totality, where a BOUNDARY carries CONDITION;
a boundary without one stays INSPECTION and is listed.
IC1 every environment quantity is identified by some entry.
IC2 every DOF of the inventory the TrM maps onto is some entry's DOF;
a failure is a NAMED GAP, disposed of at the final pass by the
TMS's IC2_POLICY (GAP or REJECT), which TPX reads only then.
IC3 no DOF is identified with two inequivalent environment quantities,
and, the isomorphism being invertible (guide 4.5), no environment
quantity with two DOF.
IC4 (b) each entry's DIMENSION equals its DOF's and its environment
quantity's, canonically; (c) the necessary part: every DOF a law in
BEARS names, and the TARGET of every constraint in BEARS, is
identified by some entry. (a) the syntactic reading of
tpc_form.ic4a_signature where a SIGNATURE carries FORM and
IMAGE_FORM; the image holding in the environment stays INSPECTION.
IC5 is INSPECTION by the guide's classing.
EQUIVALENCE: TRANSFORMATIONS are prose, so the checks treat distinct
ENVIRONMENT_QUANTITY names as inequivalent. This errs toward rejection,
never acceptance; equivalence under a TRANSFORMATION stays INSPECTION.
THE INVENTORY (D107.1): the TrM maps onto the TPK's DOF less the
TARGETs of REMOVE constraints. A FIXed DOF stays in it: it is identified,
and its FIX may be borne by its entry. An entry on a REMOVEd DOF is
refused (CODOMAIN).
ORDER (guide L0.5, 4.7; TPS 5.5.2; D98.1): as the TPK is entered, T1, then
T2, T5, T4 and T6 (T1 failing stops the run); as the TrM is entered,
IC1-IC4, with IC2's gaps held; at the final pass, after the TMS, T3 over
the constraints and the laws, and IC2's disposition. Every function
returns canonical lists and never raises on malformed input.
"""
import tpc_zone as Z
import tpc_strike as S
import tpc_form as F
TPC_TESTS_VERSION = "0.2.1" # proposed PATCH with TPC-PY 0.2.0 (C-MS-5: TPC-PHP reads the JSON as written, a {} apart from a [])
# D106.1: the closed list of top-level joiners of claims.
T2_WORDS = ["and", "but", "whereas"]
T2_PHRASES = [["as", "well", "as"]]
T2_SYMBOLS = ["&", "∧"] # ampersand, LOGICAL AND
_OPEN = {"(": ")", "[": "]", "{": "}"}
_CLOSE = set(_OPEN.values())
_LIST_MARKS = set("-*+•") # hyphen, asterisk, plus, bullet
# ---- shared readers ------------------------------------------------------------
def _entries_of(zone, key):
if not Z._obj(zone):
return []
v = zone.get(key, [])
return [e for e in v if Z._obj(e)] if Z._list(v) else []
def _s(e, f):
v = e.get(f)
return v if isinstance(v, str) else None
def _set(e, f):
v = e.get(f)
if Z._list(v) and all(isinstance(x, str) for x in v):
return v
return []
def _dof_dims(tpk):
out = {}
for e in _entries_of(tpk, "DOF"):
n, d = _s(e, "NAME"), _s(e, "DIMENSION")
if n is not None and n not in out:
out[n] = Z.normalize_dimension(d) if d is not None else None
return out
def _law_refs(tpk):
out = set()
for e in _entries_of(tpk, "LAW"):
out.update(_set(e, "REFS"))
return out
def _removed(tpk):
"""{DOF name: sorted names of the REMOVE constraints that target it}."""
out = {}
for e in _entries_of(tpk, "CONSTRAINT"):
t, n = _s(e, "TARGET"), _s(e, "NAME")
if t is not None and n is not None and _s(e, "ACTION") == "REMOVE":
out.setdefault(t, []).append(n)
return {k: sorted(v) for k, v in out.items()}
# ---- T2, syntactic part (D106.1) -----------------------------------------------
def _top(chars):
"""top[i] is True where chars[i] lies outside every CLOSED bracket pair and
every CLOSED quotation. A pair counts only once its closer is found, so an
unclosed bracket or quotation hides nothing. A quotation opens only
outside brackets: an ASCII double quote closes at the next one; U+201C
closes at the next U+201D. Nested pairs are marked too."""
n = len(chars)
inside = [False] * n
stack = [] # (expected closer, index)
i = 0
while i < n:
ch = chars[i]
if not stack and ch in ('"', "“"):
closer = '"' if ch == '"' else "”"
j = i + 1
while j < n and chars[j] != closer:
j += 1
if j < n:
for k in range(i, j + 1):
inside[k] = True
i = j + 1
continue
elif ch in _OPEN:
stack.append((_OPEN[ch], i))
elif ch in _CLOSE and stack and stack[-1][0] == ch:
start = stack.pop()[1]
for k in range(start, i + 1):
inside[k] = True
i += 1
return [not x for x in inside]
def _strip_ws(chars):
a, b = 0, len(chars)
while a < b and chars[a] in Z._WS:
a += 1
while b > a and chars[b - 1] in Z._WS:
b -= 1
return chars[a:b]
def _strip_enclosing(chars):
"""Remove bracket pairs that enclose the whole text, repeatedly: a
proposition written "(A and B)" is still a top-level conjunction."""
chars = _strip_ws(chars)
while len(chars) >= 2 and chars[0] in _OPEN:
depth_zero_at = None
stack = []
for i, ch in enumerate(chars):
if ch in _OPEN:
stack.append(_OPEN[ch])
elif ch in _CLOSE and stack and stack[-1] == ch:
stack.pop()
if not stack:
depth_zero_at = i
break
if depth_zero_at != len(chars) - 1:
break
chars = _strip_ws(chars[1:-1])
return chars
def _is_word(ch):
return ("a" <= ch <= "z") or ("A" <= ch <= "Z") or ("0" <= ch <= "9") or ch == "_"
def t2_findings(prop):
"""The syntactic findings for one PROPOSITION string, sorted: each names
the joiner found at top level. [] when none."""
chars = _strip_enclosing(list(Z._text(prop)))
top = _top(chars)
found = set()
words = [] # (text, top) of maximal ASCII word runs
i, n = 0, len(chars)
while i < n:
if _is_word(chars[i]):
j = i
while j < n and _is_word(chars[j]):
j += 1
words.append(("".join(chars[i:j]).lower(), top[i]))
i = j
else:
i += 1
for k, (w, t) in enumerate(words):
if t and w in T2_WORDS:
found.add('joins claims with "' + w + '"')
for ph in T2_PHRASES:
seg = words[k:k + len(ph)]
if len(seg) == len(ph) and all(s[1] for s in seg) and [s[0] for s in seg] == ph:
found.add('joins claims with "' + " ".join(ph) + '"')
for i, ch in enumerate(chars):
if not top[i]:
continue
if ch in T2_SYMBOLS:
found.add("joins claims with " + ("U+2227" if ch == "∧" else '"&"'))
elif ch == ";":
found.add("has a semicolon")
elif ch in ".!?":
j = i + 1
while j < n and chars[j] in Z._WS:
j += 1
if j > i + 1 and j < n and "A" <= chars[j] <= "Z":
found.add("has more than one sentence")
elif ch == "\n":
j = i + 1
while j < n and chars[j] in (" ", "\t"):
j += 1
if j < n and chars[j] in _LIST_MARKS:
found.add("is a list")
elif j < n and "0" <= chars[j] <= "9":
k = j
while k < n and "0" <= chars[k] <= "9":
k += 1
if k < n and chars[k] in ".)":
found.add("is a list")
return sorted(found)
def t2_atomicity(tpk):
"""Kernel test T2, syntactic part: no ASSUMPTION's PROPOSITION is a
top-level conjunction, list or joined pair of claims. [pass, problems]."""
probs = []
for e in _entries_of(tpk, "ASSUMPTION"):
p = _s(e, "PROPOSITION")
if p is None or Z._first_bad(p) is not None:
continue # T1's to report
for f in t2_findings(p):
probs.append("ASSUMPTION:" + Z._name(e) + ": PROPOSITION " + f + " (T2)")
return Z._done(probs)
# ---- T3, the executable fragment -------------------------------------------------
def _fix_value(e):
v, u = e.get("VALUE"), e.get("UNIT")
if not (isinstance(v, str) and isinstance(u, str)):
return ["REFUSED", "not comparable"]
return _units().normalize_measurement(v, "0", u)
def _units():
import tpc_units
return tpc_units
def t3_consistency(tpk, tms):
"""Kernel test T3 over the executable fragment: the CONSTRAINT entries -
no TARGET is both removed and fixed, and no TARGET is fixed at two values
(compared in coherent SI through canon(), the 12-significant-digit form
TPC compares presented values in) - and, beside them, the ground fragment
over the laws that carry EQUATION (tpc_form.t3_laws). Depth 1, within any
S_MAX >= 1. [pass, problems]."""
probs = []
pm = tms.get("PARAMETERS") if Z._obj(tms) else None
sm = pm.get("S_MAX") if Z._obj(pm) else None
if not (isinstance(sm, int) and not isinstance(sm, bool) and sm >= 1):
return Z._done(["T3: S_MAX is not a declared depth of at least 1"])
by_target = {}
for e in _entries_of(tpk, "CONSTRAINT"):
t, n, a = _s(e, "TARGET"), _s(e, "NAME"), _s(e, "ACTION")
if t is None or n is None or a not in ("REMOVE", "FIX"):
continue
by_target.setdefault(t, []).append((n, a, e))
for t in sorted(by_target):
cs = sorted(by_target[t], key=lambda c: c[0])
for i in range(len(cs)):
for j in range(i + 1, len(cs)):
(n1, a1, e1), (n2, a2, e2) = cs[i], cs[j]
pair = "CONSTRAINT:" + n1 + " and CONSTRAINT:" + n2
if a1 != a2:
probs.append(pair + ": " + t + " is both removed and fixed (T3)")
elif a1 == "FIX":
r1, r2 = _fix_value(e1), _fix_value(e2)
if r1[0] != "OK" or r2[0] != "OK":
probs.append(pair + ": the two FIX values of " + t + " cannot be compared (T3)")
elif r1[4] != r2[4]:
probs.append(pair + ": the two FIX values of " + t
+ " cannot be compared: units of different kind: "
+ r1[4] + " and " + r2[4] + " (T3)")
elif S.canon(r1[1]) != S.canon(r2[1]):
probs.append(pair + ": " + t + " fixed at " + e1["VALUE"] + " " + e1["UNIT"]
+ " and at " + e2["VALUE"] + " " + e2["UNIT"] + " (T3)")
probs += F.t3_laws(tpk)[1]
return Z._done(probs)
# ---- T5 ---------------------------------------------------------------------------
def t5_dof_yield(tpk):
"""Kernel test T5 over the declared citations: (b) every CONSTRAINT's
TARGET is named by some LAW; (c) every DOF is named by some LAW. Part (a)
is T1's REFS resolution. [pass, problems]."""
probs = []
named = _law_refs(tpk)
dofs = _dof_dims(tpk)
for e in _entries_of(tpk, "CONSTRAINT"):
t = _s(e, "TARGET")
if t is not None and t in dofs and t not in named:
probs.append("CONSTRAINT:" + Z._name(e) + ": TARGET " + t
+ " is named by no LAW, so no law leaves it free (T5 b)")
for d in sorted(dofs):
if d not in named:
probs.append("DOF:" + d + ": named by no LAW (T5 c)")
return Z._done(probs)
def kernel_tests(tpk):
"""The kernel tests run as the TPK is entered, in order: T1, then T2, T5,
T4 and T6. A T1 failure stops the run (guide L0.5). T3 runs at the final
pass (D98.1). [pass, [[test, pass, problems], ...], inspections] with
"NOT_RUN" in place of pass for a test the run did not reach and "NO FORM"
for T4 when no LAW carries EQUATION and for T6 when no BOUNDARY carries
CONDITION; inspections lists every law and boundary whose form is absent,
so what stays INSPECTION is visible, never silently passed (12.3)."""
t1 = Z.t1_well_formed(tpk)
rows = [["T1", t1[0], t1[1]]]
if not t1[0]:
rows += [["T2", "NOT_RUN", []], ["T5", "NOT_RUN", []], ["T4", "NOT_RUN", []], ["T6", "NOT_RUN", []]]
return [False, rows, []]
t2, t5, t4, t6 = t2_atomicity(tpk), t5_dof_yield(tpk), F.t4_homogeneity(tpk), F.t6_totality(tpk)
laws, bnds = F.form_coverage(tpk)
all_laws = [Z._name(e) for e in _entries_of(tpk, "LAW")]
all_bnds = [Z._name(e) for e in _entries_of(tpk, "BOUNDARY")]
rows += [["T2", t2[0], t2[1]], ["T5", t5[0], t5[1]],
["T4", "NO FORM" if len(laws) == len(all_laws) else t4[0], t4[1]],
["T6", "NO FORM" if len(bnds) == len(all_bnds) else t6[0], t6[1]]]
insp = ["LAW:" + n + ": no EQUATION; T4 and T3 over this law by inspection" for n in laws]
insp += ["BOUNDARY:" + n + ": no CONDITION; T6 totality by inspection" for n in bnds]
return [t2[0] and t5[0] and t4[0] and t6[0], rows, sorted(insp)]
# ---- IC1-IC4 ----------------------------------------------------------------------
def _verdict(probs, gaps):
probs = sorted(set(Z._show(p) for p in probs))
gaps = sorted(set(gaps))
return ["REJECT" if probs else ("GAP" if gaps else "PASS"), probs, gaps]
def ic_checks(trm, tpk):
"""The four isomorphism checks as the TrM is entered (guide 4.6; TPS
2.3.7), over the inventory of D107.1; IC4 (a) syntactically where a
SIGNATURE carries FORM and IMAGE_FORM (tpc_form.ic4a_signature).
[verdict, problems, gaps]: REJECT on any problem; else GAP with the
untied DOF named; else PASS. NOT_RUN if the TPK fails T1 or the TrM is
not well-formed."""
if not Z.t1_well_formed(tpk)[0]:
return ["NOT_RUN", ["IC: the TPK does not pass T1"], []]
if not Z.trm_well_formed(trm, tpk)[0]:
return ["NOT_RUN", ["IC: the TrM is not well-formed"], []]
dofs = _dof_dims(tpk)
removed = _removed(tpk)
inventory = sorted(d for d in dofs if d not in removed)
env = {}
for e in _entries_of(trm.get("HEADER"), "ENVIRONMENT_INVENTORY"):
env[e["ENVIRONMENT_QUANTITY"]] = Z.normalize_dimension(e["DIMENSION"])
ents = sorted(_entries_of(trm, "ENTRIES"), key=lambda e: e["NAME"])
laws = {e["NAME"]: e for e in _entries_of(tpk, "LAW")}
cons = {e["NAME"]: e for e in _entries_of(tpk, "CONSTRAINT")}
probs, gaps = [], []
# CODOMAIN: an entry on a REMOVEd DOF maps outside the inventory.
for e in ents:
if e["DOF"] in removed:
probs.append("CODOMAIN: ENTRY:" + e["NAME"] + " identifies DOF " + e["DOF"]
+ ", which " + ", ".join("CONSTRAINT:" + c for c in removed[e["DOF"]])
+ " removes")
identified = set(e["DOF"] for e in ents if e["DOF"] not in removed)
# IC1 TOTAL
covered = set(e["ENVIRONMENT_QUANTITY"] for e in ents)
for q in sorted(env):
if q not in covered:
probs.append("IC1: environment quantity " + q + " is identified by no entry")
# IC2 SURJECTIVE: named gaps, disposed of at the final pass
for d in inventory:
if d not in identified:
gaps.append("IC2: DOF " + d + " is untied")
# IC3 INJECTIVE, both directions
by_dof, by_q = {}, {}
for e in ents:
by_dof.setdefault(e["DOF"], []).append(e)
by_q.setdefault(e["ENVIRONMENT_QUANTITY"], []).append(e)
for d in sorted(by_dof):
qs = sorted(set(e["ENVIRONMENT_QUANTITY"] for e in by_dof[d]))
if len(qs) > 1:
probs.append("IC3: DOF " + d + " is identified with inequivalent quantities "
+ ", ".join(qs) + " (" + ", ".join("ENTRY:" + e["NAME"] for e in by_dof[d]) + ")")
for q in sorted(by_q):
ds = sorted(set(e["DOF"] for e in by_q[q]))
if len(ds) > 1:
probs.append("IC3: environment quantity " + q + " is identified with DOF "
+ ", ".join(ds) + " (" + ", ".join("ENTRY:" + e["NAME"] for e in by_q[q]) + ")")
# IC4 (b) dimensions, (c) the necessary part of BEARS
for e in ents:
tag = "ENTRY:" + e["NAME"]
dim = Z.normalize_dimension(e["DIMENSION"])
dd = dofs.get(e["DOF"])
if dd is not None and dim != dd:
probs.append("IC4(b): " + tag + ": DIMENSION " + dim + " differs from DOF " + e["DOF"]
+ "'s " + dd)
qd = env.get(e["ENVIRONMENT_QUANTITY"])
if qd is not None and dim != qd:
probs.append("IC4(b): " + tag + ": DIMENSION " + dim + " differs from environment quantity "
+ e["ENVIRONMENT_QUANTITY"] + "'s " + qd)
for b in sorted(set(e["BEARS"])):
if b in laws:
for r in sorted(set(_set(laws[b], "REFS"))):
if r in dofs and r not in identified:
probs.append("IC4(c): " + tag + ": BEARS LAW:" + b + ", which names DOF " + r
+ " that no entry identifies")
elif b in cons:
t = _s(cons[b], "TARGET")
if t is not None and t not in identified:
probs.append("IC4(c): " + tag + ": BEARS CONSTRAINT:" + b + ", whose TARGET " + t
+ " no entry identifies")
probs += F.ic4a_signature(trm, tpk)[1]
return _verdict(probs, gaps)
# ---- the final pass ---------------------------------------------------------------
def final_checks(tfk):
"""At the final pass, after the TMS is entered (D98.1): T3 over the
constraints and the laws, and IC2's disposition under the TMS's
IC2_POLICY (TPS 2.3.7; GAP when absent). [verdict, problems, gaps];
NOT_RUN if a zone fails its checks."""
if not Z._obj(tfk):
return ["NOT_RUN", ["final pass: the TFK is not an object"], []]
tpk, trm, tms = tfk.get("TPK"), tfk.get("TrM"), tfk.get("TMS")
if not kernel_tests(tpk)[0]:
return ["NOT_RUN", ["final pass: the TPK does not pass T1, T2, T5, T4 and T6"], []]
if not Z.tms_well_formed(tms)[0]:
return ["NOT_RUN", ["final pass: the TMS is not well-formed"], []]
ic = ic_checks(trm, tpk)
if ic[0] in ("NOT_RUN", "REJECT"):
return ["NOT_RUN", ["final pass: the TrM does not pass IC1-IC4"], []]
probs = list(t3_consistency(tpk, tms)[1])
policy = tms["PARAMETERS"].get("IC2_POLICY", Z.IC2_DEFAULT)
if policy == "REJECT":
probs += [g + " and IC2_POLICY is REJECT" for g in ic[2]]
return _verdict(probs, ic[2])
