Jump to content

The Principia Machina/TPC-PY/gen zone corpus.py

From The Invariance Itself
# -*- coding: utf-8 -*-
"""Generator for tpc/vectors/zone_corpus.json (TPC step 2, increment 4; schema
0.4.0 from increment 8, the D108.1 declared form; schema 0.5.0 from D176.1 and
D177.1: ROLE on LAW, ROLE INPUT on DOF, the TPK PARAMETERS part with
D_VARIABLES, STRUCTURE_CHECK in the TMS PARAMETERS, and T1's D-variable rules; S33:
a LAW restating the motion of a FIXed DOF, the toy's FREE_Z, carries ROLE CONSTRAINT).
Validator, dimension and successor expectations are HAND-DERIVED and written
literally below; the generator refuses to write the corpus if the module
disagrees with any of them. Digest cases carry their preimage; 'expect' is
SHA-256 of it (auditable with an external sha256sum). The minimal-TMS
preimage is hand-built and compared byte for byte. 0.5.2 (C-MS-5): the
decode/ cases tell a JSON {} from a JSON [] as both residences now read
them. The corpus is written with LF line ends on every platform (S65).
Run: cd tpc && python3 gen_zone_corpus.py (Windows: py gen_zone_corpus.py)."""
import copy, hashlib, json, os, sys
sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
import tpc_zone as Z
import tpc_strike as S

# ---- the toy TFK: a mass on a linear spring, motion confined to z = 0 --------
TPK = {
  "DOF": [
    {"NAME": "x", "DIMENSION": "L1"},
    {"NAME": "v", "DIMENSION": "L1 T-1"},
    {"NAME": "z", "DIMENSION": "L1"}],
  "CONSTANT": [
    {"NAME": "m", "DIMENSION": "M1"},
    {"NAME": "k_s", "DIMENSION": "M1 T-2"},
    {"NAME": "x_max", "DIMENSION": "L1", "VALUE": "0.05", "UNIT": "m", "UNCERTAINTY": "0.001"}],
  "LAW": [
    {"NAME": "N2", "STATEMENT": "m dv/dt = -k_s x", "REFS": ["m", "v", "k_s", "x"], "ROLE": "EOM(v)"},
    {"NAME": "KIN", "STATEMENT": "dx/dt = v", "REFS": ["x", "v"], "ROLE": "EOM(x)"},
    {"NAME": "FREE_Z", "STATEMENT": "d2z/dt2 = 0", "REFS": ["z"], "ROLE": "CONSTRAINT"}],
  "ASSUMPTION": [
    {"NAME": "A_lin", "PROPOSITION": "the restoring force is linear in x (Hooke r\u00e9gime)", "REFS": ["x"]}],
  "CONSTRAINT": [
    {"NAME": "C_NOZ", "TARGET": "z", "ACTION": "FIX", "VALUE": "0", "UNIT": "m", "STATEMENT": "motion confined to z = 0"}],
  "BOUNDARY": [
    {"NAME": "B_small", "PREDICATE": "|x| < x_max", "REFS": ["x", "x_max"]}],
}
TRM = {
  "HEADER": {
    "ENVIRONMENT_INVENTORY": [
      {"ENVIRONMENT_QUANTITY": "position", "DIMENSION": "L1"},
      {"ENVIRONMENT_QUANTITY": "velocity", "DIMENSION": "L1 T-1"},
      {"ENVIRONMENT_QUANTITY": "height", "DIMENSION": "L1"}],
    "SIGNATURE": [
      {"NAME": "time_derivative", "OVER": ["x", "v"], "IMAGE": "d/dt maps position to velocity"}],
    "TRANSFORMATIONS": [
      {"NAME": "time_translation", "STATEMENT": "t -> t + t0"}]},
  "ENTRIES": [
    {"NAME": "E_x", "DOF": "x", "DOMAIN": "|x| < x_max", "ENVIRONMENT_QUANTITY": "position",
     "IDENTIFICATION": "x is the displacement from equilibrium along the spring axis",
     "FALSIFIER": "a measured restoring force not proportional to x inside the domain",
     "FALSIFIER_CLASS": "F3", "BEARS": ["N2", "KIN"], "DIMENSION": "L1"},
    {"NAME": "E_v", "DOF": "v", "DOMAIN": "|x| < x_max", "ENVIRONMENT_QUANTITY": "velocity",
     "IDENTIFICATION": "v is the time derivative of x",
     "FALSIFIER": "a measured velocity differing from dx/dt beyond uncertainty",
     "FALSIFIER_CLASS": "F2", "BEARS": ["KIN"], "DIMENSION": "L1 T-1"},
    {"NAME": "E_z", "DOF": "z", "DOMAIN": "always", "ENVIRONMENT_QUANTITY": "height",
     "IDENTIFICATION": "z is the height above the track",
     "FALSIFIER": "any measured z different from 0",
     "FALSIFIER_CLASS": "F3", "BEARS": ["FREE_Z", "C_NOZ"], "DIMENSION": "L1"}],
}
TMS = {
  "PARAMETERS": {
    "STEP_CONVENTION": "one application of an inference rule or algebraic identity is one step",
    "K": "2", "N_X": 2, "S_MAX": 10},
  "CONSTANTS": [{"NAME": "w_a", "VALUE": "1"}, {"NAME": "w_s", "VALUE": "0.5"}],
  "YARDSTICKS": [{"NAME": "combined_distance", "KEY": ["SR1", "WSUM:w_a*A;w_s*S", "S"], "LIMITING": []}],
}
TFK = {"TPK": TPK, "TrM": TRM, "TMS": TMS}


def rev(x):
    """Reverse every list that is not a sequence field, recursively; reverse
    dict key order. Order-insensitive content must survive this unchanged."""
    if isinstance(x, dict):
        return {k: (x[k] if k in Z.SEQ_FIELDS else rev(x[k])) for k in reversed(list(x))}
    if isinstance(x, list):
        return [rev(e) for e in reversed(x)]
    return x


cases = []
def case(cid, fn, inp, expect, **extra):
    c = {"id": cid, "fn": fn, "input": inp}
    c.update(extra)
    c["expect"] = expect
    cases.append(c)

# ---- 1. canonical DIMENSION ---------------------------------------------------
for s, e in [("1", "true"), ("L1 M1 T-2", "true"), ("TH1", "true"), ("T1 TH1", "true"),
             ("L-1 TH1", "true"), ("M1 L1", "false"), ("L0", "false"), ("L1  T-1", "false"),
             ("L+1", "false"), ("L1 L2", "false"), ("", "false"), ("l1", "false")]:
    case("dim/is_canonical/" + (s if s else "empty").replace(" ", "_"),
         "is_canonical_dimension", {"s": s}, e)
for exps, e in [({"M": 1, "L": 2, "T": -2}, "L2 M1 T-2"), ({}, "1"), ({"L": 0}, "1"),
                ({"TH": 1, "L": -1}, "L-1 TH1"), ({"J": 1, "N": -1, "I": 2}, "I2 N-1 J1")]:
    case("dim/canon/" + (",".join("%s%d" % (b, exps[b]) for b in sorted(exps)) or "none"),
         "canon_dimension", {"exps": exps}, e)

# ---- 2. validators: the toy passes, hand-derived negatives fail ---------------
case("t1/toy-passes", "t1_well_formed", {"tpk": TPK}, "[true,[]]")
case("trm/toy-passes", "trm_well_formed", {"trm": TRM, "tpk": TPK}, "[true,[]]")
case("tms/toy-passes", "tms_well_formed", {"tms": TMS}, "[true,[]]")

TPK_BAD1 = {
  "DOF": [{"NAME": "x", "DIMENSION": "L1"}, {"NAME": "x", "DIMENSION": "M1 Q1"}],
  "LAW": [{"NAME": "N", "STATEMENT": "N relates x and q", "REFS": ["x", "q", "N"], "ROLE": "CONSTITUTIVE"}],
  "CONSTRAINT": [{"NAME": "C", "TARGET": "N", "ACTION": "FIX", "STATEMENT": "fix N"}],
  "CONSTANT": [{"NAME": "m", "DIMENSION": "M1", "VALUE": "1.5"}],
  "BOGUS": [],
}
case("t1/bad-structure", "t1_well_formed", {"tpk": TPK_BAD1},
     "[false,[CONSTANT:m: VALUE requires UNIT,CONSTRAINT:C: FIX requires UNIT,CONSTRAINT:C: FIX requires VALUE,"
     "CONSTRAINT:C: TARGET N is not a DOF,DOF:x: DIMENSION M1 Q1 is not a dimension,"
     "LAW:N: REFS q does not resolve,LAW:N: cites itself,TPK: duplicate name x,"
     "TPK: unknown kind BOGUS]]")

TPK_BAD2 = copy.deepcopy(TPK)
TPK_BAD2["ASSUMPTION"][0]["REFS"] = ["N2"]
TPK_BAD2["CONSTRAINT"][0]["ACTION"] = "REMOVE"
TPK_BAD2["CONSTANT"][2]["UNCERTAINTY"] = "-0.1"
TPK_BAD2["LAW"][1]["STATE"] = "OPEN"
TPK_BAD2["LAW"][1]["COMMENT"] = "x"
TPK_BAD2["LAW"][2]["REFS"] = "z"
TPK_BAD2["BOUNDARY"][0]["REFS"] = ["x", "x", "x_max"]
case("t1/bad-fields", "t1_well_formed", {"tpk": TPK_BAD2},
     "[false,[ASSUMPTION:A_lin: REFS N2 is a LAW, not a DOF or CONSTANT,"
     "BOUNDARY:B_small: field REFS has duplicate entries,"
     "CONSTANT:x_max: UNCERTAINTY -0.1 is negative,"
     "CONSTRAINT:C_NOZ: REMOVE forbids UNIT,CONSTRAINT:C_NOZ: REMOVE forbids VALUE,"
     "LAW:FREE_Z: field REFS has the wrong type,"
     "LAW:KIN: mutable field STATE is not permitted in the TFK,LAW:KIN: unknown field COMMENT]]")

TRM_BAD1 = {"HEADER": copy.deepcopy(TRM["HEADER"]), "ENTRIES": [
    {"NAME": "E1", "DOF": "w", "DOMAIN": " ", "ENVIRONMENT_QUANTITY": "speed",
     "IDENTIFICATION": "w is a speed", "FALSIFIER": "none offered", "FALSIFIER_CLASS": "F0",
     "BEARS": ["N2", "x"], "DIMENSION": "L1 T-1", "STATE": "PROPOSED"}]}
case("trm/bad-entry", "trm_well_formed", {"trm": TRM_BAD1, "tpk": TPK},
     "[false,[ENTRY:E1: BEARS x is not a TPK LAW or CONSTRAINT,ENTRY:E1: DOF w is not a TPK DOF,"
     "ENTRY:E1: DOMAIN is empty,"
     "ENTRY:E1: ENVIRONMENT_QUANTITY speed is not in the ENVIRONMENT INVENTORY,"
     "ENTRY:E1: FALSIFIER_CLASS F0 is inadmissible,"
     "ENTRY:E1: mutable field STATE is not permitted in the TFK]]")

TRM_BAD2 = {"HEADER": {
    "ENVIRONMENT_INVENTORY": [{"ENVIRONMENT_QUANTITY": "position", "DIMENSION": "L1"},
                              {"ENVIRONMENT_QUANTITY": "position", "DIMENSION": "T-1 L"}],
    "SIGNATURE": [{"NAME": "time_derivative", "OVER": ["x", "m"], "IMAGE": "d/dt"}]},
  "ENTRIES": []}
case("trm/bad-header", "trm_well_formed", {"trm": TRM_BAD2, "tpk": TPK},
     "[false,[ENV:position: DIMENSION T-1 L is not a dimension,"
     "SIGNATURE:time_derivative: OVER m is not a TPK DOF,"
     "TrM HEADER: missing part TRANSFORMATIONS,TrM: duplicate environment quantity position]]")

TMS_BAD1 = {
  "PARAMETERS": {"STEP_CONVENTION": "x", "K": "0", "N_X": 1, "IC2_POLICY": "MAYBE"},
  "CONSTANTS": [{"NAME": "w", "VALUE": "abc"}],
  "YARDSTICKS": [{"NAME": "Y", "KEY": ["A", "SR1", "WSUM:q*A", "BAD"], "LIMITING": []}],
}
case("tms/bad-params-and-key", "tms_well_formed", {"tms": TMS_BAD1},
     "[false,[CONSTANT:w: VALUE abc is not a decimal,"
     "PARAMETERS: IC2_POLICY MAYBE is not GAP or REJECT,PARAMETERS: K 0 is not a positive decimal in double range,"
     "PARAMETERS: N_X must be at least 2,PARAMETERS: missing field S_MAX,"
     "YARDSTICK:Y: KEY must begin with SR1,YARDSTICK:Y: SR1 may appear only as the first term,"
     "YARDSTICK:Y: constant q is not a TMS constant,YARDSTICK:Y: term BAD is not well-formed]]")

TMS_BAD2 = copy.deepcopy(TMS)
TMS_BAD2["YARDSTICKS"].append({"NAME": "Z", "KEY": ["SR1", "A"], "LIMITING": [
    {"DOMAIN": "d1", "KEY": ["SR1", "NEG:A"]}, {"DOMAIN": "d1", "KEY": ["A"]}]})
case("tms/bad-limiting", "tms_well_formed", {"tms": TMS_BAD2},
     "[false,[YARDSTICK:Z LIMITING d1: KEY must begin with SR1,"
     "YARDSTICK:Z: duplicate limiting DOMAIN d1]]")

TPK_BAD3 = {"DOF": [{"NAME": "x y", "DIMENSION": "L1"}],
            "LAW": [{"NAME": "?", "STATEMENT": "s", "REFS": ["x y"], "ROLE": "CONSTITUTIVE"}],
            "ASSUMPTION": "not a list", "BOUNDARY": [42]}
case("t1/bad-names-and-shapes", "t1_well_formed", {"tpk": TPK_BAD3},
     "[false,[DOF:x y: NAME x y is not an identifier,LAW:?: NAME ? is not an identifier,"
     "TPK kind ASSUMPTION is not a list,TPK kind BOUNDARY: entry is not an object]]")
case("t1/zone-not-object", "t1_well_formed", {"tpk": "x"}, "[false,[TPK: zone is not an object]]")
case("trm/bad-shapes", "trm_well_formed", {"trm": {"HEADER": "x", "ENTRIES": "y", "EXTRA": 1}, "tpk": TPK},
     "[false,[TrM ENTRIES is not a list,TrM: HEADER is not an object,TrM: unknown part EXTRA]]")
case("dim/is_canonical/trailing-newline", "is_canonical_dimension", {"s": "L1\n"}, "false")
for kv, e in [("1e-400", "[false,[PARAMETERS: K 1e-400 is not a positive decimal in double range]]"),
              ("1e400", "[false,[PARAMETERS: K 1e400 is not a positive decimal in double range]]"),
              ("2\n", "[false,[PARAMETERS: K 2\n is not a decimal]]"),
              ("1e-300", "[true,[]]")]:
    t = copy.deepcopy(TMS); t["PARAMETERS"]["K"] = kv
    case("tms/k-" + kv.replace("\n", "NL"), "tms_well_formed", {"tms": t}, e)
t = copy.deepcopy(TMS)
t["YARDSTICKS"].append({"NAME": "Z", "KEY": ["SR1"], "LIMITING": [
    {"DOMAIN": "r\u00e9gime", "KEY": ["SR1"]}, {"DOMAIN": "re\u0301gime", "KEY": ["SR1", "A"]},
    {"DOMAIN": " ", "KEY": ["SR1"]}]})
case("tms/limiting-nfc-duplicate-and-empty", "tms_well_formed", {"tms": t},
     "[false,[YARDSTICK:Z LIMITING  : DOMAIN is empty,YARDSTICK:Z: duplicate limiting DOMAIN r\u00e9gime]]")

t = copy.deepcopy(TRM); t["ENTRIES"][0]["DOMAIN"] = "\u00a0\t"
case("trm/nbsp-domain-is-blank", "trm_well_formed", {"trm": t, "tpk": TPK},
     "[false,[ENTRY:E_x: DOMAIN is empty]]")
t = copy.deepcopy(TMS); t["PARAMETERS"]["STEP_CONVENTION"] = "\u3000"
case("tms/ideographic-space-step-convention-is-blank", "tms_well_formed", {"tms": t},
     "[false,[PARAMETERS: STEP_CONVENTION is empty]]")
t = copy.deepcopy(TMS); t["PARAMETERS"]["STEP_CONVENTION"] = "\u200b"
case("tms/zero-width-space-is-refused", "tms_well_formed", {"tms": t},
     "[false,[PARAMETERS: field STEP_CONVENTION contains disallowed character U+200B]]",
     note="U+200B is general category Cf: refused as invisible text (tpm_zone_schemas 0.2.0 section 6)")

# ---- 2b. normalization functions and the yardstick grammar ------------------
for s_, e in [("1", "1"), ("L1 T-1", "L1 T-1"), ("T-1 L1", "L1 T-1"), ("L1 L-1", "1"), ("L0", "1"),
              ("M1 L1 M1", "L1 M2"), ("L01", "L1"), ("TH-2 J1 T3", "T3 TH-2 J1"), ("L", "null"),
              ("L1  T-1", "null"), ("L12345", "null"), ("", "null"), ("1 L1", "null"),
              ("L1\n", "null"), ("Q1", "null")]:
    case("dim/normalize/" + (s_.replace(" ", "_").replace("\n", "NL") or "empty"),
         "normalize_dimension", {"s": s_}, e)
for s_, e in [("0.05", "5e-2"), ("0.050", "5e-2"), ("5e-2", "5e-2"), ("1500", "15e2"), ("-0", "0"),
              ("0.0", "0"), ("2", "2"), ("2.0", "2"), ("6.02214076e23", "602214076e15"),
              ("007.10", "71e-1"), ("-1.5E+3", "-15e2"), ("1e-400", "1e-400"), ("10", "1e1"),
              (".5", "null"), ("5.", "null"), ("1e12345", "null"), ("0.5\n", "null"), ("+1", "null"),
              ("1,5", "null"), ("", "null")]:
    case("dec/canon/" + (s_.replace("\n", "NL") or "empty"), "canon_decimal", {"s": s_}, e)
for t_, e in [("SR1", "SR1"), ("WSUM:w_s*S;w_a*A", "WSUM:w_a*A;w_s*S"), ("NEG:NEG:A", "A"),
              ("NEG:NEG:NEG:S", "NEG:S"), ("NEG:WSUM:b*S;a*A", "NEG:WSUM:a*A;b*S"),
              ("WSUM:a*FIELD:z;b*A", "WSUM:b*A;a*FIELD:z"), ("WSUM:a*A;b*A", "WSUM:a*A;b*A"),
              ("FIELD:dof_count", "FIELD:dof_count")]:
    case("term/canon/" + t_, "canonical_term", {"t": t_}, e)

t = copy.deepcopy(TMS)
t["CONSTANTS"] += [{"NAME": "w_neg", "VALUE": "-1"}, {"NAME": "w_zero", "VALUE": "0.0"}]
t["YARDSTICKS"] = [
    {"NAME": "Y1", "KEY": ["SR1", "NEG:A", "S"], "LIMITING": []},
    {"NAME": "Y2", "KEY": ["SR1", "WSUM:w_neg*A;w_s*S"], "LIMITING": []},
    {"NAME": "Y3", "KEY": ["SR1", "WSUM:w_zero*A", "A"],
     "LIMITING": [{"DOMAIN": "|x| << x_max", "KEY": ["SR1", "NEG:A"]}]},
    {"NAME": "Y4", "KEY": ["SR1", "WSUM:w_s*A;w_s*A"], "LIMITING": []},
    {"NAME": "Y5", "KEY": ["SR1", "NEG:SR1"], "LIMITING": []},
    {"NAME": "Y6", "KEY": ["SR1", "FIELD:1bad"], "LIMITING": []},
    {"NAME": "Y7", "KEY": ["SR1", "S", "NEG:NEG:A"], "LIMITING": []},
    {"NAME": "Y8", "KEY": ["SR1", "S", "NEG:NEG:NEG:A"], "LIMITING": []}]
case("tms/yardstick-grammar-and-static-c2", "tms_well_formed", {"tms": t},
     "[false,[YARDSTICK:Y1: KEY ranks a record higher when an assumption is added (SR9 C2),"
     "YARDSTICK:Y2: KEY ranks a record higher when an assumption is added (SR9 C2),"
     "YARDSTICK:Y4: term WSUM:w_s*A;w_s*A is not well-formed,"
     "YARDSTICK:Y5: SR1 may appear only as the first term,"
     "YARDSTICK:Y6: term FIELD:1bad is not well-formed,"
     "YARDSTICK:Y8: KEY ranks a record higher when an assumption is added (SR9 C2)]]",
     note=("Y3: the first A-moving term is the plain A, since w_zero is 0; its limiting KEY "
           "inverts A inside its declared DOMAIN and is exempt from C2 there. Y7: NEG:NEG:A is A."))

# ---- 2c. text safety (tpm_zone_schemas 0.2.0 section 6) ---------------------
def with_(zone, path, value):
    z = copy.deepcopy(zone); o = z
    for k in path[:-1]:
        o = o[k]
    o[path[-1]] = value
    return z
case("text/bidi-override-in-statement", "t1_well_formed",
     {"tpk": with_(TPK, ["LAW", 0, "STATEMENT"], "m dv/dt = -k_s x \u202e")},
     "[false,[LAW:N2: field STATEMENT contains disallowed character U+202E]]")
case("text/tag-character-in-proposition", "t1_well_formed",
     {"tpk": with_(TPK, ["ASSUMPTION", 0, "PROPOSITION"], "linear\U000E0041\U000E0042 force")},
     "[false,[ASSUMPTION:A_lin: field PROPOSITION contains disallowed character U+E0041]]")
case("text/nul-in-falsifier", "trm_well_formed",
     {"trm": with_(TRM, ["ENTRIES", 0, "FALSIFIER"], "a\u0000b"), "tpk": TPK},
     "[false,[ENTRY:E_x: field FALSIFIER contains disallowed character U+0000]]")
case("text/private-use-in-image", "trm_well_formed",
     {"trm": with_(TRM, ["HEADER", "SIGNATURE", 0, "IMAGE"], "d/dt \ue000"), "tpk": TPK},
     "[false,[SIGNATURE:time_derivative: field IMAGE contains disallowed character U+E000]]")
case("text/line-separator-in-step-convention", "tms_well_formed",
     {"tms": with_(TMS, ["PARAMETERS", "STEP_CONVENTION"], "one rule\u2028one step")},
     "[false,[PARAMETERS: field STEP_CONVENTION contains disallowed character U+2028]]")
t = copy.deepcopy(TMS)
t["YARDSTICKS"].append({"NAME": "Z", "KEY": ["SR1"], "LIMITING": [{"DOMAIN": "\ufffe", "KEY": ["SR1"]}]})
case("text/noncharacter-escaped-in-message", "tms_well_formed", {"tms": t},
     "[false,[YARDSTICK:Z LIMITING <U+FFFE>: field DOMAIN contains disallowed character U+FFFE]]",
     note="the tag echoes the DOMAIN; the message shows the code point, never the character")
t = copy.deepcopy(TRM); t["ENTRIES"][1]["NOTE\u202e"] = "x"
case("text/unknown-field-name-escaped", "trm_well_formed", {"trm": t, "tpk": TPK},
     "[false,[ENTRY:E_v: unknown field NOTE<U+202E>]]")
case("term/canon/deep-neg-5000", "canonical_term", {"t": "NEG:" * 5000 + "A"}, "A",
     note="counted, not recursed: no input depth exhausts the stack")
case("term/canon/deep-neg-5001", "canonical_term", {"t": "NEG:" * 5001 + "A"}, "NEG:A")
case("tms/deep-neg-key-static-c2", "tms_well_formed",
     {"tms": with_(TMS, ["YARDSTICKS", 0, "KEY"], ["SR1", "NEG:" * 5001 + "A"])},
     "[false,[YARDSTICK:combined_distance: KEY ranks a record higher when an assumption is added (SR9 C2)]]")
t = copy.deepcopy(TMS); t["PARAMETERS"]["N_X"] = 1000001; t["PARAMETERS"]["S_MAX"] = 1000001
case("tms/int-cap", "tms_well_formed", {"tms": t},
     "[false,[PARAMETERS: N_X must be at most 1000000,PARAMETERS: S_MAX must be at most 1000000]]")
t = copy.deepcopy(TMS); t["PARAMETERS"]["N_X"] = 1000000; t["PARAMETERS"]["S_MAX"] = 1000000
case("tms/int-cap-edge-accepted", "tms_well_formed", {"tms": t}, "[true,[]]")
for fl, e in [("F0", "[false,[PARAMETERS: PROMOTION_FLOOR F0 is not F1, F2 or F3]]"),
              ("F1", "[true,[]]"), ("F3", "[true,[]]"), ("f2", "[false,[PARAMETERS: PROMOTION_FLOOR f2 is not F1, F2 or F3]]")]:
    case("tms/promotion-floor-" + fl, "tms_well_formed",
         {"tms": with_(TMS, ["PARAMETERS", "PROMOTION_FLOOR"], fl)}, e)

# ---- 2d. units at zone entry (schema 0.3.0; D103.1, D104.1) ------------------
def tpk_with(path, value):
    return with_(TPK, path, value)
case("t1/unit-not-a-unit", "t1_well_formed", {"tpk": tpk_with(["CONSTANT", 2, "UNIT"], "furlong")},
     "[false,[CONSTANT:x_max: UNIT furlong: furlong is not a unit symbol]]")
case("t1/unit-wrong-dimension", "t1_well_formed", {"tpk": tpk_with(["CONSTANT", 2, "UNIT"], "cm2")},
     "[false,[CONSTANT:x_max: UNIT cm2 has dimension L2, not L1]]")
case("t1/unit-refused-celsius", "t1_well_formed", {"tpk": tpk_with(["CONSTANT", 2, "UNIT"], "degC")},
     "[false,[CONSTANT:x_max: UNIT degC: degC is refused, an offset scale, not a ratio]]")
case("t1/unit-prefixed-accepted", "t1_well_formed", {"tpk": tpk_with(["CONSTANT", 2, "UNIT"], "cm")},
     "[true,[]]")
case("t1/unit-bidi-control", "t1_well_formed", {"tpk": tpk_with(["CONSTANT", 2, "UNIT"], "m\u202e")},
     "[false,[CONSTANT:x_max: UNIT m<U+202E> is not a unit,"
     "CONSTANT:x_max: field UNIT contains disallowed character U+202E]]")
case("t1/fix-requires-unit", "t1_well_formed",
     {"tpk": dict(TPK, CONSTRAINT=[{k: v for k, v in TPK["CONSTRAINT"][0].items() if k != "UNIT"}])},
     "[false,[CONSTRAINT:C_NOZ: FIX requires UNIT]]")
case("t1/fix-unit-wrong-dimension", "t1_well_formed", {"tpk": tpk_with(["CONSTRAINT", 0, "UNIT"], "s")},
     "[false,[CONSTRAINT:C_NOZ: UNIT s has dimension T1, not L1 of TARGET z]]")
t = copy.deepcopy(TPK)
t["DOF"].append({"NAME": "theta", "DIMENSION": "1"})
t["CONSTANT"].append({"NAME": "theta_0", "DIMENSION": "1", "VALUE": "0.1", "UNIT": "rad"})
t["CONSTRAINT"].append({"NAME": "C_TH", "TARGET": "theta", "ACTION": "FIX", "VALUE": "5", "UNIT": "deg",
                        "STATEMENT": "theta held at 5 degrees"})
case("t1/angle-is-dimensionless", "t1_well_formed", {"tpk": t}, "[true,[]]",
     note="rad and deg are commensurable with DIMENSION 1 (the SI treats angle as one)")

# ---- 2e. the declared form at zone entry (schema 0.4.0; D108.1, increment 8) -------
TPK_F = copy.deepcopy(TPK)
TPK_F["DOF"].append({"NAME": "t", "DIMENSION": "T1"})
TPK_F["LAW"] = [
    {"NAME": "N2", "STATEMENT": "m dv/dt = -k_s x", "REFS": ["m", "v", "k_s", "x", "t"], "ROLE": "EOM(v)",
     "EQUATION": "m * D(v, t) = -k_s * x"},
    {"NAME": "KIN", "STATEMENT": "dx/dt = v", "REFS": ["x", "v", "t"], "ROLE": "EOM(x)", "EQUATION": "D(x, t) = v"},
    {"NAME": "FREE_Z", "STATEMENT": "d2z/dt2 = 0", "REFS": ["z", "t"], "ROLE": "CONSTRAINT", "EQUATION": "D(z, t, 2) = 0"}]
TPK_F["BOUNDARY"] = [{"NAME": "B_small", "PREDICATE": "|x| < x_max", "REFS": ["x", "x_max"], "CONDITION": "abs(x) < x_max"}]
TRM_F = copy.deepcopy(TRM)
TRM_F["HEADER"]["ENVIRONMENT_INVENTORY"].append({"ENVIRONMENT_QUANTITY": "time", "DIMENSION": "T1"})
TRM_F["HEADER"]["SIGNATURE"] = [{"NAME": "time_derivative", "OVER": ["x", "v", "t"], "IMAGE": "d/dt maps position to velocity",
                                 "FORM": "D(x, t) = v", "IMAGE_FORM": "D(position, time) = velocity"}]
TRM_F["ENTRIES"].append({"NAME": "E_t", "DOF": "t", "DOMAIN": "always", "ENVIRONMENT_QUANTITY": "time",
                         "IDENTIFICATION": "t is the laboratory clock reading",
                         "FALSIFIER": "two laboratory clocks that disagree beyond their stated uncertainty",
                         "FALSIFIER_CLASS": "F3", "BEARS": [], "DIMENSION": "T1"})
TFK_F = {"TPK": TPK_F, "TrM": TRM_F, "TMS": TMS}
case("t1/forms-pass", "t1_well_formed", {"tpk": TPK_F}, "[true,[]]",
     note="the spring with its forms: EQUATION on every LAW, CONDITION on the BOUNDARY, a DOF t of T1 (S3)")
case("trm/forms-pass", "trm_well_formed", {"trm": TRM_F, "tpk": TPK_F}, "[true,[]]")
case("t1/equation-does-not-parse", "t1_well_formed", {"tpk": with_(TPK_F, ["LAW", 0, "EQUATION"], "m * D(v, t) =")},
     "[false,[LAW:N2: EQUATION does not parse: unexpected end]]")
case("t1/equation-names-nonmember", "t1_well_formed", {"tpk": with_(TPK_F, ["LAW", 1, "REFS"], ["x", "v"])},
     "[false,[LAW:KIN: EQUATION names t, which is not in REFS]]")
case("t1/refs-member-unnamed", "t1_well_formed", {"tpk": with_(TPK_F, ["LAW", 0, "REFS"], ["m", "v", "k_s", "x", "t", "z"])},
     "[false,[LAW:N2: REFS z is not named in EQUATION]]")
case("t1/condition-names-nonmember", "t1_well_formed", {"tpk": with_(TPK_F, ["BOUNDARY", 0, "REFS"], ["x"])},
     "[false,[BOUNDARY:B_small: CONDITION names x_max, which is not in REFS]]")
case("t1/condition-does-not-parse", "t1_well_formed", {"tpk": with_(TPK_F, ["BOUNDARY", 0, "CONDITION"], "|x| < x_max")},
     "[false,[BOUNDARY:B_small: CONDITION does not parse: unexpected character | at 1]]")
case("t1/equation-hidden-character", "t1_well_formed", {"tpk": with_(TPK_F, ["LAW", 0, "EQUATION"], "m * D(v, t) = -k_s * x\u202e")},
     "[false,[LAW:N2: EQUATION does not parse: unexpected character <U+202E> at 23,"
     "LAW:N2: field EQUATION contains disallowed character U+202E]]")
case("t1/equation-wrong-type", "t1_well_formed", {"tpk": with_(TPK_F, ["LAW", 0, "EQUATION"], 7)},
     "[false,[LAW:N2: field EQUATION has the wrong type]]")
case("t1/equation-on-boundary-unknown", "t1_well_formed", {"tpk": with_(TPK_F, ["BOUNDARY", 0, "EQUATION"], "x = 0")},
     "[false,[BOUNDARY:B_small: unknown field EQUATION]]")
case("t1/condition-on-law-unknown", "t1_well_formed", {"tpk": with_(TPK_F, ["LAW", 0, "CONDITION"], "x < 0")},
     "[false,[LAW:N2: unknown field CONDITION]]")
t = copy.deepcopy(TRM_F); del t["HEADER"]["SIGNATURE"][0]["IMAGE_FORM"]
case("trm/form-requires-image-form", "trm_well_formed", {"trm": t, "tpk": TPK_F},
     "[false,[SIGNATURE:time_derivative: FORM requires IMAGE_FORM]]")
t = copy.deepcopy(TRM_F); del t["HEADER"]["SIGNATURE"][0]["FORM"]
case("trm/image-form-requires-form", "trm_well_formed", {"trm": t, "tpk": TPK_F},
     "[false,[SIGNATURE:time_derivative: IMAGE_FORM requires FORM]]")
case("trm/form-names-nonmember", "trm_well_formed", {"trm": with_(TRM_F, ["HEADER", "SIGNATURE", 0, "OVER"], ["x", "v"]), "tpk": TPK_F},
     "[false,[SIGNATURE:time_derivative: FORM names t, which is not in OVER]]")
case("trm/over-member-unnamed", "trm_well_formed", {"trm": with_(TRM_F, ["HEADER", "SIGNATURE", 0, "OVER"], ["x", "v", "t", "z"]), "tpk": TPK_F},
     "[false,[SIGNATURE:time_derivative: OVER z is not named in FORM]]")
case("trm/image-form-names-non-quantity", "trm_well_formed",
     {"trm": with_(TRM_F, ["HEADER", "SIGNATURE", 0, "IMAGE_FORM"], "D(position, time) = speed"), "tpk": TPK_F},
     "[false,[SIGNATURE:time_derivative: IMAGE_FORM names speed, which is not in the ENVIRONMENT INVENTORY]]")
case("trm/form-does-not-parse", "trm_well_formed", {"trm": with_(TRM_F, ["HEADER", "SIGNATURE", 0, "FORM"], "D(x, t) = v ="), "tpk": TPK_F},
     "[false,[SIGNATURE:time_derivative: FORM does not parse: unexpected token = at 13]]")

# ---- 3. the hand-built preimages (schema 0.5.0) -------------------------------
TMS_MIN = {"PARAMETERS": {"STEP_CONVENTION": "x", "K": "2", "N_X": 2, "S_MAX": 1},
           "CONSTANTS": [], "YARDSTICKS": []}
HAND = ("l4:sTMS6:s0.5.0141:l11:sPARAMETERS122:l16:sSTEP_CONVENTION2:sx2:sK2:s24:sN_X2:i26:sS_MAX"
        "2:i111:sIC2_POLICY4:sGAP16:sPROMOTION_FLOOR3:sF216:sSTRUCTURE_CHECK3:sON"
        "17:l10:sCONSTANTS1:l18:l11:sYARDSTICKS1:l")
assert len(HAND) == 201
case("preimage/tms-minimal-hand-built", "zone_preimage", {"zone": "TMS", "value": TMS_MIN}, HAND,
     note="schema 0.5.0: STRUCTURE_CHECK enters after PROMOTION_FLOOR; absent, it serializes as ON")
case("digest/tms-minimal", "d_tms", {"tms": TMS_MIN},
     hashlib.sha256(HAND.encode("ascii")).hexdigest(), preimage=HAND)
TMS_MIN2 = copy.deepcopy(TMS_MIN); TMS_MIN2["PARAMETERS"]["K"] = "20e-1"
case("preimage/tms-minimal-K-respelled", "zone_preimage", {"zone": "TMS", "value": TMS_MIN2}, HAND,
     note="K 20e-1 normalizes to 2: the same hand-built preimage")
TMS_MIN3 = copy.deepcopy(TMS_MIN); TMS_MIN3["PARAMETERS"]["IC2_POLICY"] = "GAP"
case("preimage/tms-minimal-IC2-explicit-GAP", "zone_preimage", {"zone": "TMS", "value": TMS_MIN3}, HAND,
     note="an absent IC2_POLICY serializes as GAP (TPS 2.3.7): the same hand-built preimage")
TMS_MIN4 = copy.deepcopy(TMS_MIN); TMS_MIN4["PARAMETERS"]["PROMOTION_FLOOR"] = "F2"
case("preimage/tms-minimal-PROMOTION-FLOOR-explicit-F2", "zone_preimage", {"zone": "TMS", "value": TMS_MIN4}, HAND,
     note="an absent PROMOTION_FLOOR serializes as F2 (D92.1): the same hand-built preimage")
TMS_MIN5 = copy.deepcopy(TMS_MIN); TMS_MIN5["PARAMETERS"]["STRUCTURE_CHECK"] = "ON"
case("preimage/tms-minimal-STRUCTURE-CHECK-explicit-ON", "zone_preimage", {"zone": "TMS", "value": TMS_MIN5}, HAND,
     note="an absent STRUCTURE_CHECK serializes as ON (D176.1): the same hand-built preimage")
case("digest/tms-minimal-STRUCTURE-CHECK-explicit-ON", "d_tms", {"tms": TMS_MIN5},
     hashlib.sha256(HAND.encode("ascii")).hexdigest(), preimage=HAND,
     note="declaring the default and saying nothing give one digest")
HAND_OFF = ("l4:sTMS6:s0.5.0142:l11:sPARAMETERS123:l16:sSTEP_CONVENTION2:sx2:sK2:s24:sN_X2:i26:sS_MAX"
            "2:i111:sIC2_POLICY4:sGAP16:sPROMOTION_FLOOR3:sF216:sSTRUCTURE_CHECK4:sOFF"
            "17:l10:sCONSTANTS1:l18:l11:sYARDSTICKS1:l")
assert len(HAND_OFF) == 202
TMS_MIN6 = copy.deepcopy(TMS_MIN); TMS_MIN6["PARAMETERS"]["STRUCTURE_CHECK"] = "OFF"
case("preimage/tms-minimal-STRUCTURE-CHECK-OFF-hand-built", "zone_preimage", {"zone": "TMS", "value": TMS_MIN6}, HAND_OFF)
case("digest/tms-minimal-STRUCTURE-CHECK-OFF", "d_tms", {"tms": TMS_MIN6},
     hashlib.sha256(HAND_OFF.encode("ascii")).hexdigest(), preimage=HAND_OFF)
# the TPK: PARAMETERS ahead of the six kinds; absent, it serializes as D_VARIABLES ONE
TPK_MIN = {"DOF": [{"NAME": "x", "DIMENSION": "L1"}]}
HAND_TPK = ("l4:sTPK6:s0.5.040:l11:sPARAMETERS22:l12:sD_VARIABLES4:sONE"
            "44:l4:sDOF34:l30:l5:sNAME2:sx10:sDIMENSION3:sL1"
            "15:l9:sCONSTANT1:l10:l4:sLAW1:l18:l11:sASSUMPTION1:l18:l11:sCONSTRAINT1:l15:l9:sBOUNDARY1:l")
assert len(HAND_TPK) == 196
case("t1/tpk-minimal-passes", "t1_well_formed", {"tpk": TPK_MIN}, "[true,[]]",
     note="the hand-built TPK below passes T1, so its digest is defined")
case("preimage/tpk-minimal-hand-built", "zone_preimage", {"zone": "TPK", "value": TPK_MIN}, HAND_TPK,
     note="schema 0.5.0: the PARAMETERS part enters ahead of the six kinds; absent, it serializes as D_VARIABLES ONE")
case("digest/tpk-minimal", "d_tpk", {"tpk": TPK_MIN},
     hashlib.sha256(HAND_TPK.encode("ascii")).hexdigest(), preimage=HAND_TPK)
for cid, pm in [("empty", {}), ("explicit-ONE", {"D_VARIABLES": "ONE"})]:
    t = copy.deepcopy(TPK_MIN); t["PARAMETERS"] = pm
    t = {"PARAMETERS": t.pop("PARAMETERS"), "DOF": t["DOF"]}
    case("preimage/tpk-minimal-PARAMETERS-" + cid, "zone_preimage", {"zone": "TPK", "value": t}, HAND_TPK,
         note="an absent PARAMETERS or an absent D_VARIABLES serializes as ONE (D177.1): the same hand-built preimage")
    case("digest/tpk-minimal-PARAMETERS-" + cid, "d_tpk", {"tpk": t},
         hashlib.sha256(HAND_TPK.encode("ascii")).hexdigest(), preimage=HAND_TPK)
HAND_TPK_SEV = ("l4:sTPK6:s0.5.044:l11:sPARAMETERS26:l12:sD_VARIABLES8:sSEVERAL"
                "44:l4:sDOF34:l30:l5:sNAME2:sx10:sDIMENSION3:sL1"
                "15:l9:sCONSTANT1:l10:l4:sLAW1:l18:l11:sASSUMPTION1:l18:l11:sCONSTRAINT1:l15:l9:sBOUNDARY1:l")
assert len(HAND_TPK_SEV) == 200
t = {"PARAMETERS": {"D_VARIABLES": "SEVERAL"}, "DOF": copy.deepcopy(TPK_MIN["DOF"])}
case("preimage/tpk-minimal-SEVERAL-hand-built", "zone_preimage", {"zone": "TPK", "value": t}, HAND_TPK_SEV)
case("digest/tpk-minimal-SEVERAL", "d_tpk", {"tpk": t},
     hashlib.sha256(HAND_TPK_SEV.encode("ascii")).hexdigest(), preimage=HAND_TPK_SEV)

# ---- 4. the toy's digests, each with its preimage -----------------------------
pre = {"TPK": Z.preimage_tpk(TPK).decode("utf-8"),
       "TrM": Z.preimage_trm(TRM).decode("utf-8"),
       "TMS": Z.preimage_tms(TMS).decode("utf-8")}
for zone, fn, key, val in [("TPK", "d_tpk", "tpk", TPK), ("TrM", "d_trm", "trm", TRM),
                           ("TMS", "d_tms", "tms", TMS)]:
    case("preimage/toy-" + zone, "zone_preimage", {"zone": zone, "value": val}, pre[zone])
    case("digest/toy-" + zone, fn, {key: val},
         hashlib.sha256(pre[zone].encode("utf-8")).hexdigest(), preimage=pre[zone])
assert pre["TPK"].startswith("l4:sTPK6:s0.5.040:l11:sPARAMETERS22:l12:sD_VARIABLES4:sONE")
assert "5:sREFS19:l4:sk_s2:sm2:sv2:sx5:sROLE7:sEOM(v)" in pre["TPK"]          # ROLE after REFS (schema 0.5.0)
assert "16:sPROMOTION_FLOOR3:sF216:sSTRUCTURE_CHECK3:sON" in pre["TMS"]           # absent STRUCTURE_CHECK is ON
dz = [hashlib.sha256(pre[z].encode("utf-8")).hexdigest() for z in ("TPK", "TrM", "TMS")]
case("digest/toy-TFK", "d_tfk_of", {"tfk": TFK}, S.canon(Z.G.combine_digests(dz)),
     note="combine_digests of the three toy zone digests above (D97.1)")

# ---- 4b. the spring with its forms: preimages carry the canonical spelling (S10) ----
pre_f = {"TPK": Z.preimage_tpk(TPK_F).decode("utf-8"), "TrM": Z.preimage_trm(TRM_F).decode("utf-8")}
assert "9:sEQUATION16:sm*D(v,t)=-k_s*x" in pre_f["TPK"] and "10:sCONDITION13:sabs(x)<x_max" in pre_f["TPK"]
assert "5:sFORM9:sD(x,t)=v11:sIMAGE_FORM26:sD(position,time)=velocity" in pre_f["TrM"]
assert "5:sROLE7:sEOM(v)9:sEQUATION16:sm*D(v,t)=-k_s*x" in pre_f["TPK"]      # ROLE between REFS and EQUATION
case("preimage/spring-forms-TPK", "zone_preimage", {"zone": "TPK", "value": TPK_F}, pre_f["TPK"],
     note="ROLE enters after REFS; EQUATION and CONDITION after it in their canonical spelling")
case("digest/spring-forms-TPK", "d_tpk", {"tpk": TPK_F}, hashlib.sha256(pre_f["TPK"].encode("utf-8")).hexdigest(),
     preimage=pre_f["TPK"])
case("preimage/spring-forms-TrM", "zone_preimage", {"zone": "TrM", "value": TRM_F}, pre_f["TrM"],
     note="FORM and IMAGE_FORM enter after IMAGE in their canonical spelling")
case("digest/spring-forms-TrM", "d_trm", {"trm": TRM_F}, hashlib.sha256(pre_f["TrM"].encode("utf-8")).hexdigest(),
     preimage=pre_f["TrM"])
dzf = [hashlib.sha256(pre_f["TPK"].encode("utf-8")).hexdigest(), hashlib.sha256(pre_f["TrM"].encode("utf-8")).hexdigest(),
       hashlib.sha256(Z.preimage_tms(TMS)).hexdigest()]
case("digest/spring-forms-TFK", "d_tfk_of", {"tfk": TFK_F}, S.canon(Z.G.combine_digests(dzf)),
     note="the tutorial's spring with its forms and ROLEs under schema 0.5.0")

# ---- 5. order- and normalization-insensitivity; successor classes -------------
TFK_REV = rev(TFK)
case("invariance/reordered-TPK-same-digest", "d_tpk", {"tpk": TFK_REV["TPK"]}, dz[0])
case("invariance/reordered-TrM-same-digest", "d_trm", {"trm": TFK_REV["TrM"]}, dz[1])
case("invariance/reordered-TMS-same-digest", "d_tms", {"tms": TFK_REV["TMS"]}, dz[2])
TPK_NFD = copy.deepcopy(TPK)
TPK_NFD["ASSUMPTION"][0]["PROPOSITION"] = "the restoring force is linear in x (Hooke re\u0301gime)"
assert TPK_NFD != TPK
case("invariance/NFD-text-same-digest", "d_tpk", {"tpk": TPK_NFD}, dz[0])

def succ(cid, b, e):
    case("successor/" + cid, "classify_successor", {"a": TFK, "b": b}, e)
succ("reordered", TFK_REV, "IDENTICAL")
succ("nfd", {"TPK": TPK_NFD, "TrM": TRM, "TMS": TMS}, "IDENTICAL")
b = copy.deepcopy(TFK); b["TrM"]["ENTRIES"][1]["FALSIFIER_CLASS"] = "F3"
succ("falsifier-class-changed", b, "CORRESPONDENCE_CHANGED")
b = copy.deepcopy(TFK); b["TrM"]["HEADER"]["TRANSFORMATIONS"][0]["STATEMENT"] = "t -> t + t0, t0 real"
succ("header-changed", b, "CORRESPONDENCE_CHANGED")
b = copy.deepcopy(TFK); b["TMS"]["PARAMETERS"]["K"] = "3"
succ("k-changed", b, "YARDSTICK_ONLY")
b = copy.deepcopy(TFK); b["TMS"]["PARAMETERS"]["IC2_POLICY"] = "REJECT"
succ("ic2-tightened-to-reject", b, "YARDSTICK_ONLY")
b = copy.deepcopy(TFK); b["TMS"]["PARAMETERS"]["PROMOTION_FLOOR"] = "F3"
succ("promotion-floor-raised", b, "YARDSTICK_ONLY")
b = copy.deepcopy(TFK); b["TMS"]["PARAMETERS"]["PROMOTION_FLOOR"] = "F2"
succ("promotion-floor-explicit-default", b, "IDENTICAL")
a = copy.deepcopy(TFK); a["TPK"]["LAW"][1]["STATEMENT"] = "dx/dt\n= v"
b = copy.deepcopy(TFK); b["TPK"]["LAW"][1]["STATEMENT"] = "dx/dt\r\n= v"
case("successor/crlf-is-lf", "classify_successor", {"a": a, "b": b}, "IDENTICAL")
b = copy.deepcopy(TFK); b["TPK"]["LAW"][1]["STATEMENT"] = "dx/dt\r= v"
case("successor/lone-cr-is-lf", "classify_successor", {"a": a, "b": b}, "IDENTICAL")
case("t1/crlf-and-tab-are-accepted", "t1_well_formed",
     {"tpk": dict(copy.deepcopy(TPK), LAW=[dict(TPK["LAW"][0], STATEMENT="m dv/dt\r\n\t= -k_s x")] + TPK["LAW"][1:])},
     "[true,[]]")
b = copy.deepcopy(TFK); b["TMS"]["YARDSTICKS"][0]["KEY"] = ["SR1", "S", "WSUM:w_a*A;w_s*S"]
succ("key-order-changed", b, "YARDSTICK_ONLY")
b = copy.deepcopy(TFK); b["TMS"]["YARDSTICKS"][0]["KEY"] = ["SR1", "WSUM:w_s*S;w_a*A", "NEG:NEG:S"]
succ("key-terms-respelled", b, "IDENTICAL")
b = copy.deepcopy(TFK); b["TPK"]["CONSTANT"][2]["VALUE"] = "5e-2"
b["TPK"]["CONSTANT"][2]["UNCERTAINTY"] = "0.0010"
b["TPK"]["CONSTRAINT"][0]["VALUE"] = "-0.0"
b["TMS"]["PARAMETERS"]["K"] = "2.0"; b["TMS"]["CONSTANTS"][1]["VALUE"] = "5E-1"
succ("decimals-respelled", b, "IDENTICAL")
b = copy.deepcopy(TFK); b["TPK"]["DOF"][1]["DIMENSION"] = "T-1 L1"
b["TPK"]["CONSTANT"][1]["DIMENSION"] = "T-1 M1 T-1 L0"
succ("tpk-dimensions-respelled", b, "IDENTICAL")
b = copy.deepcopy(TFK); b["TrM"]["ENTRIES"][1]["DIMENSION"] = "T-1 L1"
b["TrM"]["HEADER"]["ENVIRONMENT_INVENTORY"][1]["DIMENSION"] = "L2 T-1 L-1"
succ("trm-dimensions-respelled", b, "IDENTICAL")
b = copy.deepcopy(TFK); b["TPK"]["LAW"][1]["STATEMENT"] = "dx/dt = v + 0"
succ("law-statement-changed", b, "KERNEL_CHANGED")
b = copy.deepcopy(TFK); b["TPK"]["DOF"][1]["DIMENSION"] = "L1 T-2"
b["TrM"]["ENTRIES"][1]["DIMENSION"] = "L1 T-2"
succ("kernel-and-correspondence-changed", b, "KERNEL_CHANGED")
a = copy.deepcopy(TFK)
a["TMS"]["YARDSTICKS"][0]["LIMITING"] = [{"DOMAIN": "b_dom", "KEY": ["SR1", "NEG:A"]},
                                        {"DOMAIN": "a_dom", "KEY": ["SR1", "S"]}]
b = copy.deepcopy(a); b["TMS"]["YARDSTICKS"][0]["LIMITING"].reverse()
case("successor/limiting-reordered", "classify_successor", {"a": a, "b": b}, "IDENTICAL")
a = copy.deepcopy(TFK); a["TPK"]["CONSTANT"][1].update({"VALUE": "40", "UNIT": "kg s-2"})
b = copy.deepcopy(TFK); b["TPK"]["CONSTANT"][1].update({"VALUE": "40", "UNIT": "s-2 kg1"})
case("successor/unit-respelled", "classify_successor", {"a": a, "b": b}, "IDENTICAL",
     note="the preimage carries the canonical spelling kg s-2 (D104.1)")
b = copy.deepcopy(TFK); b["TPK"]["CONSTANT"][2].update({"VALUE": "5", "UNIT": "cm", "UNCERTAINTY": "0.1"})
succ("same-quantity-other-unit", b, "KERNEL_CHANGED")
b = copy.deepcopy(TFK); b["TPK"]["CONSTRAINT"][0]["UNIT"] = "mm"
succ("fix-unit-changed", b, "KERNEL_CHANGED")
a = copy.deepcopy(TFK_F)
b = copy.deepcopy(TFK_F); b["TPK"]["LAW"][0]["EQUATION"] = "m*D(v,t,1)=((-k_s*x))"
b["TPK"]["BOUNDARY"][0]["CONDITION"] = "(abs((x))<x_max)"
b["TrM"]["HEADER"]["SIGNATURE"][0]["FORM"] = "D( x , t ) = ( v )"
case("successor/forms-respelled", "classify_successor", {"a": a, "b": b}, "IDENTICAL",
     note="whitespace, D(x,t,1) and redundant enclosing parentheses: one canonical spelling (S10)")
b = copy.deepcopy(TFK_F); b["TPK"]["LAW"][0]["EQUATION"] = "D(v, t) * m = -k_s * x"
case("successor/form-operands-reordered", "classify_successor", {"a": a, "b": b}, "KERNEL_CHANGED",
     note="only spelling is canonical: m*D(v,t) and D(v,t)*m are different statements")
b = copy.deepcopy(TFK_F); del b["TPK"]["LAW"][1]["EQUATION"]
case("successor/form-removed", "classify_successor", {"a": a, "b": b}, "KERNEL_CHANGED")
b = copy.deepcopy(TFK_F); b["TrM"]["HEADER"]["SIGNATURE"][0]["IMAGE_FORM"] = "D(position,time)=(velocity)"
case("successor/image-form-respelled", "classify_successor", {"a": a, "b": b}, "IDENTICAL")
b = copy.deepcopy(TFK_F); del b["TrM"]["HEADER"]["SIGNATURE"][0]["FORM"]; del b["TrM"]["HEADER"]["SIGNATURE"][0]["IMAGE_FORM"]
case("successor/signature-form-removed", "classify_successor", {"a": a, "b": b}, "CORRESPONDENCE_CHANGED")
case("successor/schema-0.4.0-toy-under-0.5.0", "d_tfk_of", {"tfk": TFK}, S.canon(Z.G.combine_digests(dz)),
     note=("the toy without forms under schema 0.5.0, its LAWs carrying ROLE: its D(TFK) under 0.4.0 (no ROLE) was "
           "09a229d76bbf580abe7d7c10985fc804ef842f733a331f2a14fc92c12d664798, under 0.3.0 "
           "3e92bae72f437acac87d3f6a0683978cf629e61df17bed2ceb5e9da3c8c352b1; the version tag moves every zone digest"))

# ---- 2f. S15: a DIMENSION whose canonical form leaves the grammar (tpc_zone 0.4.1) ----
# D99: anything that does not parse is refused, never altered; D103: an exponent has
# at most four digits. Repeated bases add (TPS 2.5.12); a sum outside -9999..9999 would
# canonicalize to a token the grammar refuses ("L9999 L1" -> "L10000"), so the
# DIMENSION is refused: "DIMENSION <D>: an exponent is out of range", in the form of
# tpc_units' "UNIT <U>: an exponent is out of range". The bound is on the canonical
# form: sums that return inside it are accepted. Hand-derived.
for s_, e in [("L9999", "L9999"), ("L-9999", "L-9999"), ("L9999_L1", "null"), ("L9999_L9999", "null"),
              ("L-9999_L-1", "null"), ("L5000_L4999", "L9999"), ("L9999_L-1_L1", "L9999"),
              ("L9999_L9999_L-9999", "L9999"), ("T9999_TH9999_TH1", "null"),
              ("M1_M-1_L9999_L1_L-1", "L9999"), ("L9999_L1_Q1", "null")]:
    case("dim/normalize/s15-" + s_, "normalize_dimension", {"s": s_.replace("_", " ")}, e)
for s_, e in [("L9999", "true"), ("L-9999", "true"), ("L10000", "false"), ("L-10000", "false"),
              ("L1 T-10000", "false")]:
    case("dim/is_canonical/s15-" + s_.replace(" ", "_"), "is_canonical_dimension", {"s": s_}, e,
         **({"note": "tpc_zone 0.4.0 answered true: its canonical token had no digit bound"}
            if e == "false" else {}))
case("t1/s15-dof-dimension-out-of-range", "t1_well_formed", {"tpk": tpk_with(["DOF", 0, "DIMENSION"], "L9999 L1")},
     "[false,[DOF:x: DIMENSION L9999 L1: an exponent is out of range]]",
     note="tpc_zone 0.4.0 admitted it as L10000, a DIMENSION its own grammar refuses")
case("t1/s15-dof-dimension-sum-at-bound", "t1_well_formed", {"tpk": tpk_with(["DOF", 0, "DIMENSION"], "L5000 L-4999")},
     "[true,[]]", note="the sum is L1: accepted, spelled L1")
case("t1/s15-constant-with-unit", "t1_well_formed", {"tpk": tpk_with(["CONSTANT", 2, "DIMENSION"], "L9999 L1")},
     "[false,[CONSTANT:x_max: DIMENSION L9999 L1: an exponent is out of range]]",
     note="the UNIT check stays silent on a DIMENSION that does not parse")
case("t1/s15-fix-target", "t1_well_formed", {"tpk": tpk_with(["DOF", 2, "DIMENSION"], "L-9999 L-1")},
     "[false,[DOF:z: DIMENSION L-9999 L-1: an exponent is out of range]]")
case("t1/s15-bad-token-first", "t1_well_formed", {"tpk": tpk_with(["DOF", 0, "DIMENSION"], "L9999 L1 Q1")},
     "[false,[DOF:x: DIMENSION L9999 L1 Q1 is not a dimension]]", note="a token that does not parse is reported as before")
t = copy.deepcopy(TRM); t["HEADER"]["ENVIRONMENT_INVENTORY"][0]["DIMENSION"] = "L9999 L1"
case("trm/s15-env-dimension-out-of-range", "trm_well_formed", {"trm": t, "tpk": TPK},
     "[false,[ENV:position: DIMENSION L9999 L1: an exponent is out of range]]")
t = copy.deepcopy(TRM); t["ENTRIES"][0]["DIMENSION"] = "T9999 TH9999 TH1"
case("trm/s15-entry-dimension-out-of-range", "trm_well_formed", {"trm": t, "tpk": TPK},
     "[false,[ENTRY:E_x: DIMENSION T9999 TH9999 TH1: an exponent is out of range]]")
t = copy.deepcopy(TPK); t["DOF"][0]["DIMENSION"] = "L5000 L-4999"
case("invariance/s15-dimension-sum-within-bound-same-digest", "d_tpk", {"tpk": t}, dz[0],
     note="an admitted respelling keeps the toy's D(TPK)")
succ("s15-dimension-sum-within-bound", {"TPK": t, "TrM": TRM, "TMS": TMS}, "IDENTICAL")


# ---- 2g. schema 0.5.0 (D176.1, D177.1; tpc_zone 0.5.0, proposed) -------------------------
# ROLE on LAW, required: EOM(<NAME>), CONSTRAINT, CONSTITUTIVE, INVARIANT or DEFINITION,
# spelled exactly so; in EOM(<NAME>) the NAME must be a DOF of the TPK (T1). Every other
# consistency of a ROLE is the structure check's finding, not T1's (S31). ROLE on DOF,
# optional: INPUT only. The TPK PARAMETERS part, optional, ahead of the six kinds: its one
# field D_VARIABLES, ONE or SEVERAL; absent means ONE. STRUCTURE_CHECK in the TMS
# PARAMETERS, optional, ON or OFF; absent means ON. T1's D-variable rules (D177.1): the
# second argument s of every D in the TPK's forms is a DOF and the TARGET of no CONSTRAINT;
# under ONE every D uses one s. Every expectation hand-derived.
def law_role(tpk, name, role):
    t = copy.deepcopy(tpk)
    for l in t["LAW"]:
        if l["NAME"] == name:
            if role is None:
                del l["ROLE"]
            else:
                l["ROLE"] = role
    return t

ROLE_GRAMMAR = "is not EOM(<DOF>), CONSTRAINT, CONSTITUTIVE, INVARIANT or DEFINITION"
for role in ["CONSTRAINT", "CONSTITUTIVE", "INVARIANT", "DEFINITION", "EOM(z)", "EOM(x)", "EOM(t)"]:
    case("t1/s050-law-role-" + role, "t1_well_formed", {"tpk": law_role(TPK_F, "FREE_Z", role)}, "[true,[]]",
         **({"note": "EOM of the D variable, or of a second law's DOF, passes T1: any other consistency of a ROLE "
                     "is the structure check's finding (S31)"} if role in ("EOM(t)", "EOM(x)") else {}))
for cid, role in [("lower-eom", "eom(z)"), ("space-before-paren", "EOM (z)"), ("space-inside-left", "EOM( z)"),
                  ("space-inside-right", "EOM(z )"), ("unclosed", "EOM(z"), ("empty-name", "EOM()"),
                  ("name-not-identifier", "EOM(1z)"), ("two-names", "EOM(z,t)"), ("bare-EOM", "EOM"),
                  ("lower-word", "constraint"), ("mixed-case-word", "Constraint"), ("trailing-space", "CONSTRAINT "),
                  ("leading-space", " CONSTRAINT"), ("empty", ""), ("dof-role-on-law", "INPUT"),
                  ("trailing-newline", "EOM(z)\n"), ("brackets", "EOM[z]"), ("plural", "DEFINITIONS")]:
    case("t1/s050-law-role-refused-" + cid, "t1_well_formed", {"tpk": law_role(TPK_F, "FREE_Z", role)},
         "[false,[LAW:FREE_Z: ROLE " + role + " " + ROLE_GRAMMAR + "]]")
case("t1/s050-law-role-hidden-character", "t1_well_formed", {"tpk": law_role(TPK_F, "FREE_Z", "EOM(z)\u202e")},
     "[false,[LAW:FREE_Z: ROLE EOM(z)<U+202E> " + ROLE_GRAMMAR + ",LAW:FREE_Z: field ROLE contains disallowed character U+202E]]")
for cid, q, what in [("constant", "k_s", "k_s"), ("unresolved", "q", "q"), ("law", "KIN", "KIN"),
                     ("constraint", "C_NOZ", "C_NOZ"), ("environment-quantity", "position", "position"),
                     ("itself", "FREE_Z", "FREE_Z")]:
    case("t1/s050-law-role-eom-not-a-dof-" + cid, "t1_well_formed", {"tpk": law_role(TPK_F, "FREE_Z", "EOM(" + q + ")")},
         "[false,[LAW:FREE_Z: ROLE EOM(" + q + ") names " + what + ", which is not a DOF]]")
case("t1/s050-law-role-missing", "t1_well_formed", {"tpk": law_role(TPK_F, "FREE_Z", None)},
     "[false,[LAW:FREE_Z: missing field ROLE]]", note="ROLE is required on every LAW under schema 0.5.0")
case("t1/s050-law-role-missing-toy", "t1_well_formed", {"tpk": law_role(TPK, "KIN", None)},
     "[false,[LAW:KIN: missing field ROLE]]", note="a law without a form still carries a ROLE")
for cid, v in [("integer", 7), ("list", ["EOM(z)"]), ("null", None)]:
    t = law_role(TPK_F, "FREE_Z", "EOM(z)"); t["LAW"][2]["ROLE"] = v
    case("t1/s050-law-role-wrong-type-" + cid, "t1_well_formed", {"tpk": t}, "[false,[LAW:FREE_Z: field ROLE has the wrong type]]")

def dof_role(tpk, name, role):
    t = copy.deepcopy(tpk)
    for d in t["DOF"]:
        if d["NAME"] == name:
            d["ROLE"] = role
    return t

case("t1/s050-dof-role-INPUT", "t1_well_formed", {"tpk": dof_role(TPK_F, "x", "INPUT")}, "[true,[]]",
     note="an INPUT DOF named in EOM(x) passes T1: the structure check lists the ROLE MISMATCH (S31)")
for cid, role in [("lower", "input"), ("eom", "EOM(x)"), ("empty", ""), ("trailing-space", "INPUT "),
                  ("law-word", "CONSTRAINT"), ("plural", "INPUTS")]:
    case("t1/s050-dof-role-refused-" + cid, "t1_well_formed", {"tpk": dof_role(TPK_F, "x", role)},
         "[false,[DOF:x: ROLE " + role + " is not INPUT]]")
t = dof_role(TPK_F, "x", "INPUT"); t["DOF"][0]["ROLE"] = 1
case("t1/s050-dof-role-wrong-type", "t1_well_formed", {"tpk": t}, "[false,[DOF:x: field ROLE has the wrong type]]")

def tpk_params(tpk, pm):
    t = copy.deepcopy(tpk)
    out = {"PARAMETERS": pm}
    out.update(t)
    return out

for cid, pm in [("empty", {}), ("ONE", {"D_VARIABLES": "ONE"}), ("SEVERAL", {"D_VARIABLES": "SEVERAL"})]:
    case("t1/s050-parameters-" + cid, "t1_well_formed", {"tpk": tpk_params(TPK_F, pm)}, "[true,[]]")
for cid, dv in [("lower", "one"), ("TWO", "TWO"), ("empty", ""), ("trailing-space", "SEVERAL ")]:
    case("t1/s050-parameters-refused-" + cid, "t1_well_formed", {"tpk": tpk_params(TPK_F, {"D_VARIABLES": dv})},
         "[false,[TPK PARAMETERS: D_VARIABLES " + dv + " is not ONE or SEVERAL]]")
case("t1/s050-parameters-hidden-character", "t1_well_formed", {"tpk": tpk_params(TPK_F, {"D_VARIABLES": "ONE\u202e"})},
     "[false,[TPK PARAMETERS: D_VARIABLES ONE<U+202E> is not ONE or SEVERAL,"
     "TPK PARAMETERS: field D_VARIABLES contains disallowed character U+202E]]")
case("t1/s050-parameters-wrong-type", "t1_well_formed", {"tpk": tpk_params(TPK_F, {"D_VARIABLES": 2})},
     "[false,[TPK PARAMETERS: field D_VARIABLES has the wrong type]]")
case("t1/s050-parameters-unknown-field", "t1_well_formed",
     {"tpk": tpk_params(TPK_F, {"D_VARIABLES": "ONE", "STRUCTURE_CHECK": "ON"})},
     "[false,[TPK PARAMETERS: unknown field STRUCTURE_CHECK]]", note="STRUCTURE_CHECK is the TMS's, not the TPK's")
case("t1/s050-parameters-mutable-field", "t1_well_formed", {"tpk": tpk_params(TPK_F, {"STATE": "OPEN"})},
     "[false,[TPK PARAMETERS: mutable field STATE is not permitted in the TFK]]")
case("t1/s050-parameters-string", "t1_well_formed", {"tpk": tpk_params(TPK_F, "ONE")},
     "[false,[TPK: PARAMETERS is not an object]]")
case("t1/s050-parameters-list", "t1_well_formed", {"tpk": tpk_params(TPK_F, ["ONE"])},
     "[false,[TPK: PARAMETERS is not an object]]")
case("t1/s050-parameters-lower-part-unknown", "t1_well_formed",
     {"tpk": dict(copy.deepcopy(TPK_F), parameters={"D_VARIABLES": "ONE"})},
     "[false,[TPK: unknown kind parameters]]", note="the part's name is spelled exactly")

# T1's D-variable rules (D177.1): the spring uses t alone
TAU = copy.deepcopy(TPK_F)
TAU["DOF"].append({"NAME": "tau", "DIMENSION": "T1"})
TAU["LAW"][1]["EQUATION"] = "D(x, tau) = v"; TAU["LAW"][1]["REFS"] = ["x", "v", "tau"]
ONE_2 = ("TPK: D_VARIABLES is ONE (ONE when absent), but the forms use D variables "
         "t (LAW:FREE_Z, LAW:N2), tau (LAW:KIN)")
case("t1/s050-dvar-one-second-variable", "t1_well_formed", {"tpk": TAU}, "[false,[" + ONE_2 + "]]",
     note="absent PARAMETERS means ONE: a second distinct D variable is T1's refusal")
case("t1/s050-dvar-explicit-one-second-variable", "t1_well_formed",
     {"tpk": tpk_params(TAU, {"D_VARIABLES": "ONE"})}, "[false,[" + ONE_2 + "]]")
case("t1/s050-dvar-several-admits-second-variable", "t1_well_formed",
     {"tpk": tpk_params(TAU, {"D_VARIABLES": "SEVERAL"})}, "[true,[]]")
case("t1/s050-dvar-malformed-switch-no-count", "t1_well_formed", {"tpk": tpk_params(TAU, {"D_VARIABLES": "TWO"})},
     "[false,[TPK PARAMETERS: D_VARIABLES TWO is not ONE or SEVERAL]]",
     note="a D_VARIABLES that is neither ONE nor SEVERAL is refused as a field; the count rule is not applied under it")
t = copy.deepcopy(TPK_F); t["LAW"][1]["EQUATION"] = "D(x, m) = v"; t["LAW"][1]["REFS"] = ["x", "v", "m"]
case("t1/s050-dvar-constant", "t1_well_formed", {"tpk": tpk_params(t, {"D_VARIABLES": "SEVERAL"})},
     "[false,[LAW:KIN: EQUATION's D variable m is not a DOF]]",
     note="a CONSTANT is not a D variable (D177.1); T1's DIMENSION T1 requirement is removed")
case("t1/s050-dvar-constant-under-one", "t1_well_formed", {"tpk": t},
     "[false,[LAW:KIN: EQUATION's D variable m is not a DOF,"
     "TPK: D_VARIABLES is ONE (ONE when absent), but the forms use D variables m (LAW:KIN), t (LAW:FREE_Z, LAW:N2)]]")
t = copy.deepcopy(TPK_F); t["LAW"][1]["EQUATION"] = "D(x, q) = v"; t["LAW"][1]["REFS"] = ["x", "v", "q"]
case("t1/s050-dvar-unresolved", "t1_well_formed", {"tpk": tpk_params(t, {"D_VARIABLES": "SEVERAL"})},
     "[false,[LAW:KIN: EQUATION's D variable q is not a DOF,LAW:KIN: REFS q does not resolve]]")
t = copy.deepcopy(TPK_F); t["CONSTRAINT"].append({"NAME": "C_T", "TARGET": "t", "ACTION": "FIX", "VALUE": "0",
                                                  "UNIT": "s", "STATEMENT": "t = 0"})
case("t1/s050-dvar-fix-target", "t1_well_formed", {"tpk": t},
     "[false,[LAW:FREE_Z: EQUATION's D variable t is the TARGET of CONSTRAINT:C_T,"
     "LAW:KIN: EQUATION's D variable t is the TARGET of CONSTRAINT:C_T,"
     "LAW:N2: EQUATION's D variable t is the TARGET of CONSTRAINT:C_T]]",
     note="a FIXed clock is no D variable (D177.1)")
t = copy.deepcopy(TPK_F); t["CONSTRAINT"].append({"NAME": "C_TR", "TARGET": "t", "ACTION": "REMOVE", "STATEMENT": "no t"})
case("t1/s050-dvar-remove-target", "t1_well_formed", {"tpk": t},
     "[false,[LAW:FREE_Z: EQUATION's D variable t is the TARGET of CONSTRAINT:C_TR,"
     "LAW:KIN: EQUATION's D variable t is the TARGET of CONSTRAINT:C_TR,"
     "LAW:N2: EQUATION's D variable t is the TARGET of CONSTRAINT:C_TR]]")
t = copy.deepcopy(TPK_F); t["LAW"] = [l for l in t["LAW"] if l["NAME"] == "KIN"]
t["CONSTRAINT"] += [{"NAME": "C_T2", "TARGET": "t", "ACTION": "REMOVE", "STATEMENT": "no t"},
                    {"NAME": "C_T1", "TARGET": "t", "ACTION": "FIX", "VALUE": "0", "UNIT": "s", "STATEMENT": "t = 0"}]
t["DOF"] = [d for d in t["DOF"] if d["NAME"] != "z"]; t["CONSTRAINT"] = t["CONSTRAINT"][1:]
t["LAW"].append({"NAME": "N2", "STATEMENT": "m dv/dt = -k_s x", "REFS": ["m", "v", "k_s", "x"], "ROLE": "EOM(v)"})
case("t1/s050-dvar-two-targets", "t1_well_formed", {"tpk": t},
     "[false,[LAW:KIN: EQUATION's D variable t is the TARGET of CONSTRAINT:C_T1,"
     "LAW:KIN: EQUATION's D variable t is the TARGET of CONSTRAINT:C_T2]]",
     note="each CONSTRAINT that targets the D variable is named; a law without a form uses no D variable")
# corner_fix_t (out/D/examples/corner_fix_t.json, ROLEs added): the clock FIXed at t = 0
CORNER_FIX_T = {
  "DOF": [{"NAME": "t", "DIMENSION": "T1"}, {"NAME": "x", "DIMENSION": "L1"}, {"NAME": "v", "DIMENSION": "L1 T-1"},
          {"NAME": "z", "DIMENSION": "L1"}],
  "CONSTANT": [{"NAME": "m", "DIMENSION": "M1"}, {"NAME": "k_s", "DIMENSION": "M1 T-2"},
               {"NAME": "x_max", "DIMENSION": "L1", "VALUE": "0.05", "UNIT": "m", "UNCERTAINTY": "0.001"}],
  "LAW": [{"NAME": "EOM_X", "STATEMENT": "m dv/dt = -k_s x", "REFS": ["m", "v", "k_s", "x", "t"], "ROLE": "EOM(v)",
           "EQUATION": "m * D(v, t) = -k_s * x"},
          {"NAME": "KIN", "STATEMENT": "dx/dt = v", "REFS": ["x", "v", "t"], "ROLE": "EOM(x)", "EQUATION": "D(x, t) = v"},
          {"NAME": "EOM_Z", "STATEMENT": "m d2z/dt2 = 0", "REFS": ["m", "z", "t"], "ROLE": "CONSTRAINT",
           "EQUATION": "m * D(z, t, 2) = 0"}],
  "ASSUMPTION": [{"NAME": "A_kpos", "PROPOSITION": "k_s is positive", "REFS": ["k_s"]},
                 {"NAME": "A_mpos", "PROPOSITION": "m is positive", "REFS": ["m"]}],
  "CONSTRAINT": [{"NAME": "C_NOZ", "TARGET": "z", "ACTION": "FIX", "VALUE": "0", "UNIT": "m",
                  "STATEMENT": "only motion on the spring axis is described: z = 0"},
                 {"NAME": "C_T", "TARGET": "t", "ACTION": "FIX", "VALUE": "0", "UNIT": "s", "STATEMENT": "t = 0"}],
  "BOUNDARY": [{"NAME": "B_small", "PREDICATE": "|x| < x_max", "REFS": ["x", "x_max"], "CONDITION": "abs(x) < x_max"}]}
case("t1/s050-dvar-corner-fix-t", "t1_well_formed", {"tpk": CORNER_FIX_T},
     "[false,[LAW:EOM_X: EQUATION's D variable t is the TARGET of CONSTRAINT:C_T,"
     "LAW:EOM_Z: EQUATION's D variable t is the TARGET of CONSTRAINT:C_T,"
     "LAW:KIN: EQUATION's D variable t is the TARGET of CONSTRAINT:C_T]]",
     note="out/D/examples/corner_fix_t.json with ROLEs added; T1 passed it under schema 0.4.0 (E-N7)")
# A21 (out/A/suite/A21_dimensionless_time.json, ROLEs added): the scaled time tau of DIMENSION 1
A21_TPK = {
  "DOF": [{"NAME": "X", "DIMENSION": "1"}, {"NAME": "V", "DIMENSION": "1"}, {"NAME": "tau", "DIMENSION": "1"}],
  "LAW": [{"NAME": "KIN", "STATEMENT": "dX/dtau = V", "REFS": ["X", "V", "tau"], "ROLE": "EOM(X)", "EQUATION": "D(X, tau) = V"},
          {"NAME": "N2", "STATEMENT": "dV/dtau = -X", "REFS": ["X", "V", "tau"], "ROLE": "EOM(V)", "EQUATION": "D(V, tau) = -X"}]}
case("t1/s050-dvar-scaled-time-A21", "t1_well_formed", {"tpk": A21_TPK}, "[true,[]]",
     note="out/A/suite/A21 with ROLEs added: the D variable is a DOF of DIMENSION 1, admitted (D177.1)")
t = copy.deepcopy(TPK_F); t["LAW"][1]["EQUATION"] = "D(x, t) ="
case("t1/s050-dvar-unparsed-form-uses-none", "t1_well_formed", {"tpk": tpk_params(t, {"D_VARIABLES": "ONE"})},
     "[false,[LAW:KIN: EQUATION does not parse: unexpected end]]",
     note="a form that does not parse uses no D variable; its refusal is reported once")
t = copy.deepcopy(TAU); t["LAW"][1]["EQUATION"] = "D(x, tau) = v\u202e"
case("t1/s050-dvar-hidden-form-uses-none", "t1_well_formed", {"tpk": t},
     "[false,[LAW:KIN: EQUATION does not parse: unexpected character <U+202E> at 14,"
     "LAW:KIN: field EQUATION contains disallowed character U+202E]]")
t = copy.deepcopy(TPK_F); t["DOF"][3]["ROLE"] = "INPUT"
case("t1/s050-dvar-input-dof", "t1_well_formed", {"tpk": t}, "[true,[]]",
     note="a D variable that carries ROLE INPUT passes T1")

# the TMS switch (D176.1)
for v in ["ON", "OFF"]:
    case("tms/s050-structure-check-" + v, "tms_well_formed", {"tms": with_(TMS, ["PARAMETERS", "STRUCTURE_CHECK"], v)}, "[true,[]]")
for cid, v in [("lower", "on"), ("YES", "YES"), ("empty", ""), ("trailing-space", "OFF ")]:
    case("tms/s050-structure-check-refused-" + cid, "tms_well_formed",
         {"tms": with_(TMS, ["PARAMETERS", "STRUCTURE_CHECK"], v)},
         "[false,[PARAMETERS: STRUCTURE_CHECK " + v + " is not ON or OFF]]")
case("tms/s050-structure-check-boolean", "tms_well_formed", {"tms": with_(TMS, ["PARAMETERS", "STRUCTURE_CHECK"], True)},
     "[false,[PARAMETERS: field STRUCTURE_CHECK has the wrong type]]")

# digests: defaults equal explicit values; the new fields enter D(TPK) and D(TMS)
for cid, pm in [("empty", {}), ("explicit-ONE", {"D_VARIABLES": "ONE"})]:
    case("invariance/s050-parameters-" + cid + "-same-digest", "d_tpk", {"tpk": tpk_params(TPK, pm)}, dz[0])
case("invariance/s050-structure-check-explicit-ON-same-digest", "d_tms",
     {"tms": with_(TMS, ["PARAMETERS", "STRUCTURE_CHECK"], "ON")}, dz[2])
succ("s050-parameters-explicit-ONE", {"TPK": tpk_params(TPK, {"D_VARIABLES": "ONE"}), "TrM": TRM, "TMS": TMS}, "IDENTICAL")
succ("s050-parameters-SEVERAL", {"TPK": tpk_params(TPK, {"D_VARIABLES": "SEVERAL"}), "TrM": TRM, "TMS": TMS},
     "KERNEL_CHANGED")
succ("s050-structure-check-explicit-ON", {"TPK": TPK, "TrM": TRM, "TMS": with_(TMS, ["PARAMETERS", "STRUCTURE_CHECK"], "ON")},
     "IDENTICAL")
succ("s050-structure-check-OFF", {"TPK": TPK, "TrM": TRM, "TMS": with_(TMS, ["PARAMETERS", "STRUCTURE_CHECK"], "OFF")},
     "YARDSTICK_ONLY")
succ("s050-law-role-changed", {"TPK": law_role(TPK, "FREE_Z", "EOM(z)"), "TrM": TRM, "TMS": TMS}, "KERNEL_CHANGED")
succ("s050-dof-role-INPUT-added", {"TPK": dof_role(TPK, "z", "INPUT"), "TrM": TRM, "TMS": TMS}, "KERNEL_CHANGED")
pre_in = Z.preimage_tpk(dof_role(TPK, "z", "INPUT")).decode("utf-8")
assert "45:l5:sNAME2:sz10:sDIMENSION3:sL15:sROLE6:sINPUT" in pre_in                    # ROLE after DIMENSION
case("preimage/s050-dof-role-INPUT", "zone_preimage", {"zone": "TPK", "value": dof_role(TPK, "z", "INPUT")}, pre_in,
     note="a DOF's ROLE enters after its DIMENSION; a DOF without ROLE serializes as under 0.4.0")


# ---- self-check against the module, then write ------------------------------
def nz(v):
    return "null" if v is None else v

# ---- 0.5.2 (C-MS-5; increment 11): a JSON {} and a JSON [] are told apart -------------
# TPC-PHP read zones as json_decode(..., true) arrays, where {} and [] decode alike and an
# object keyed "0".."n-1" reads as a list; from tpc_zone 0.5.1 both residences read the
# JSON as written. Expectations by hand from the validators' messages (t1_well_formed,
# trm_well_formed, tms_well_formed); every case is one an assoc-array reading answered
# otherwise, or a valid {} that must stay valid.
X_DOF = {"NAME": "x", "DIMENSION": "L1"}
case("decode/t1-tpk-list", "t1_well_formed", {"tpk": []}, "[false,[TPK: zone is not an object]]",
     note="a JSON [] is not a TPK (it read as an empty TPK and passed T1)")
case("decode/t1-tpk-empty-object", "t1_well_formed", {"tpk": {}}, "[true,[]]",
     note="a JSON {} is the empty TPK: every kind absent")
case("decode/t1-kind-object", "t1_well_formed", {"tpk": {"DOF": {}}}, "[false,[TPK kind DOF is not a list]]")
case("decode/t1-kind-zero-keyed", "t1_well_formed", {"tpk": {"DOF": {"0": X_DOF}}},
     "[false,[TPK kind DOF is not a list]]", note="an object keyed 0 is not a list")
case("decode/t1-entry-list", "t1_well_formed", {"tpk": {"DOF": [[]]}},
     "[false,[TPK kind DOF: entry is not an object]]")
case("decode/t1-entry-empty-object", "t1_well_formed", {"tpk": {"DOF": [{}]}},
     "[false,[DOF:?: missing field DIMENSION,DOF:?: missing field NAME]]")
case("decode/t1-parameters-list", "t1_well_formed", {"tpk": {"PARAMETERS": []}},
     "[false,[TPK: PARAMETERS is not an object]]")
case("decode/t1-parameters-empty-object", "t1_well_formed", {"tpk": {"PARAMETERS": {}}}, "[true,[]]",
     note="an empty PARAMETERS part is valid: D_VARIABLES is optional")
case("decode/t1-parameters-zero-keyed", "t1_well_formed", {"tpk": {"PARAMETERS": {"0": "ONE"}}},
     "[false,[TPK PARAMETERS: unknown field 0]]")
case("decode/t1-unknown-kind-zero", "t1_well_formed", {"tpk": {"0": [], "DOF": [X_DOF]}},
     "[false,[TPK: unknown kind 0]]", note="a key 0 beside named keys; the name is echoed as written")
LAW_OBJREFS = {"NAME": "L", "STATEMENT": "x is free", "REFS": {}, "ROLE": "DEFINITION"}
case("decode/t1-refs-object", "t1_well_formed", {"tpk": {"DOF": [X_DOF], "LAW": [LAW_OBJREFS]}},
     "[false,[LAW:L: field REFS has the wrong type]]", note="REFS {} is not a list of names")
case("decode/t1-refs-zero-keyed", "t1_well_formed",
     {"tpk": {"DOF": [X_DOF], "LAW": [dict(LAW_OBJREFS, REFS={"0": "x"})]}},
     "[false,[LAW:L: field REFS has the wrong type]]")
HDR0 = {"ENVIRONMENT_INVENTORY": [], "SIGNATURE": [], "TRANSFORMATIONS": []}
case("decode/trm-list", "trm_well_formed", {"trm": [], "tpk": TPK_MIN}, "[false,[TrM: zone is not an object]]")
case("decode/trm-header-list", "trm_well_formed", {"trm": {"HEADER": [], "ENTRIES": []}, "tpk": TPK_MIN},
     "[false,[TrM: HEADER is not an object]]")
case("decode/trm-header-empty-object", "trm_well_formed", {"trm": {"HEADER": {}, "ENTRIES": []}, "tpk": TPK_MIN},
     "[false,[TrM HEADER: missing part ENVIRONMENT_INVENTORY,TrM HEADER: missing part SIGNATURE,"
     "TrM HEADER: missing part TRANSFORMATIONS]]")
case("decode/trm-entries-object", "trm_well_formed", {"trm": {"HEADER": HDR0, "ENTRIES": {}}, "tpk": TPK_MIN},
     "[false,[TrM ENTRIES is not a list]]")
case("decode/trm-inventory-zero-keyed", "trm_well_formed",
     {"trm": {"HEADER": dict(HDR0, ENVIRONMENT_INVENTORY={"0": {"ENVIRONMENT_QUANTITY": "position", "DIMENSION": "L1"}}),
              "ENTRIES": []}, "tpk": TPK_MIN},
     "[false,[TrM ENVIRONMENT_INVENTORY is not a list]]")
case("decode/trm-over-object", "trm_well_formed",
     {"trm": {"HEADER": dict(HDR0, SIGNATURE=[{"NAME": "s", "OVER": {}, "IMAGE": "i"}]), "ENTRIES": []},
      "tpk": TPK_MIN},
     "[false,[SIGNATURE:s: field OVER has the wrong type]]")
E_X = {"NAME": "E_x", "DOF": "x", "DOMAIN": "always", "ENVIRONMENT_QUANTITY": "position",
       "IDENTIFICATION": "x is the position", "FALSIFIER": "a measured position off x", "FALSIFIER_CLASS": "F2",
       "BEARS": [], "DIMENSION": "L1"}
TRM_X = {"HEADER": dict(HDR0, ENVIRONMENT_INVENTORY=[{"ENVIRONMENT_QUANTITY": "position", "DIMENSION": "L1"}]),
         "ENTRIES": [E_X]}
case("decode/trm-valid-x", "trm_well_formed", {"trm": TRM_X, "tpk": TPK_MIN}, "[true,[]]",
     note="the one-entry TrM the next case reads against a TPK whose DOF kind is not a list")
case("decode/trm-tpk-kind-zero-keyed", "trm_well_formed", {"trm": TRM_X, "tpk": {"DOF": {"0": X_DOF}}},
     "[false,[ENTRY:E_x: DOF x is not a TPK DOF]]",
     note="the TPK's DOF kind is not a list, so the TPK declares no DOF (it read as the list [x])")
TMS_M = {"PARAMETERS": {"STEP_CONVENTION": "x", "K": "2", "N_X": 2, "S_MAX": 1}}
case("decode/tms-valid-minimal", "tms_well_formed", {"tms": TMS_M}, "[true,[]]")
case("decode/tms-list", "tms_well_formed", {"tms": []}, "[false,[TMS: zone is not an object]]")
case("decode/tms-parameters-list", "tms_well_formed", {"tms": {"PARAMETERS": []}},
     "[false,[TMS: PARAMETERS is not an object]]")
case("decode/tms-parameters-empty-object", "tms_well_formed", {"tms": {"PARAMETERS": {}}},
     "[false,[PARAMETERS: missing field K,PARAMETERS: missing field N_X,PARAMETERS: missing field STEP_CONVENTION,"
     "PARAMETERS: missing field S_MAX]]")
case("decode/tms-parameters-zero-keyed", "tms_well_formed", {"tms": {"PARAMETERS": {"0": "x"}}},
     "[false,[PARAMETERS: missing field K,PARAMETERS: missing field N_X,PARAMETERS: missing field STEP_CONVENTION,"
     "PARAMETERS: missing field S_MAX,PARAMETERS: unknown field 0]]")
case("decode/tms-yardsticks-object", "tms_well_formed", {"tms": dict(TMS_M, YARDSTICKS={})},
     "[false,[TMS YARDSTICKS is not a list]]", note="it read as no yardstick and passed")
case("decode/tms-constants-zero-keyed", "tms_well_formed",
     {"tms": dict(TMS_M, CONSTANTS={"0": {"NAME": "w", "VALUE": "1"}})}, "[false,[TMS CONSTANTS is not a list]]")
Y1 = {"NAME": "y", "KEY": ["SR1"], "LIMITING": []}
case("decode/tms-yardstick-valid", "tms_well_formed", {"tms": dict(TMS_M, YARDSTICKS=[Y1])}, "[true,[]]")
case("decode/tms-limiting-object", "tms_well_formed", {"tms": dict(TMS_M, YARDSTICKS=[dict(Y1, LIMITING={})])},
     "[false,[YARDSTICK:y: field LIMITING has the wrong type]]")
case("decode/tms-limiting-entry-list", "tms_well_formed", {"tms": dict(TMS_M, YARDSTICKS=[dict(Y1, LIMITING=[[]])])},
     "[false,[YARDSTICK:y: field LIMITING has the wrong type]]", note="a limiting case [] is not an object")
case("decode/tms-limiting-entry-empty-object", "tms_well_formed",
     {"tms": dict(TMS_M, YARDSTICKS=[dict(Y1, LIMITING=[{}])])},
     "[false,[YARDSTICK:y LIMITING ?: missing field DOMAIN,YARDSTICK:y LIMITING ?: missing field KEY]]")
case("decode/tms-key-object", "tms_well_formed", {"tms": dict(TMS_M, YARDSTICKS=[dict(Y1, KEY={})])},
     "[false,[YARDSTICK:y: field KEY has the wrong type]]")
case("decode/digest-tpk-parameters-empty-object", "d_tpk", {"tpk": {"PARAMETERS": {}, "DOF": [X_DOF]}},
     hashlib.sha256(HAND_TPK.encode("ascii")).hexdigest(), preimage=HAND_TPK,
     note="a valid empty PARAMETERS object digests as the hand-built minimal TPK")
case("decode/preimage-tpk-empty-object", "zone_preimage", {"zone": "TPK", "value": {}},
     "l4:sTPK6:s0.5.040:l11:sPARAMETERS22:l12:sD_VARIABLES4:sONE10:l4:sDOF1:l15:l9:sCONSTANT1:l10:l4:sLAW1:l"
     "18:l11:sASSUMPTION1:l18:l11:sCONSTRAINT1:l15:l9:sBOUNDARY1:l",
     note="the empty TPK: PARAMETERS serialized with D_VARIABLES ONE and six empty kinds (hand-built)")


def dispatch(fn, i):
    if fn == "normalize_dimension": return nz(Z.normalize_dimension(i["s"]))
    if fn == "canon_decimal": return nz(Z.canon_decimal(i["s"]))
    if fn == "canonical_term": return Z.canonical_term(i["t"])
    if fn == "is_canonical_dimension": return Z.is_canonical_dimension(i["s"])
    if fn == "canon_dimension": return Z.canon_dimension(i["exps"])
    if fn == "t1_well_formed": return Z.t1_well_formed(i["tpk"])
    if fn == "trm_well_formed": return Z.trm_well_formed(i["trm"], i["tpk"])
    if fn == "tms_well_formed": return Z.tms_well_formed(i["tms"])
    if fn == "zone_preimage": return Z.zone_preimage(i["zone"], i["value"])
    if fn == "d_tpk": return Z.d_tpk(i["tpk"])
    if fn == "d_trm": return Z.d_trm(i["trm"])
    if fn == "d_tms": return Z.d_tms(i["tms"])
    if fn == "d_tfk_of": return Z.d_tfk_of(i["tfk"])
    if fn == "classify_successor": return Z.classify_successor(i["a"], i["b"])
    raise KeyError(fn)

bad = 0
for c in cases:
    got = S.canon(dispatch(c["fn"], c["input"]))
    if got != c["expect"]:
        bad += 1
        print("MISMATCH", c["id"], "\n  expect", c["expect"], "\n  got   ", got)
if bad:
    sys.exit("refusing to write: %d mismatches" % bad)

corpus = {
  "meta": {
    "name": "tpc_zone_corpus", "version": "0.5.2",
    "status": "SELECTED D92.1, D98.1, D99.1, D100.1; units D103.1, D104.1, D105.1 (2026-09-22); the D108.1 declared form at Option 1 of every slot (2026-09-24, increment 8); D176.1 and D177.1 (2026-09-26, schema 0.5.0); values VERIFIED",
    "conforms_tps": "0.1.0 revision 4 (zone schemas for TPS 2.2-2.4; per-zone digests TPS 2.5.9; successor classes TPS 2.1.5; T1 of guide 3.6); schema 0.5.0 per D176.1 and D177.1 as taken 2026-09-26 (TPS revision 6 text pending)",
    "module": "tpc_zone 0.5.1 (proposed with TPC-PY 0.2.0), schema 0.5.0 (tpc_units 0.1.1, tpc_form 0.2.1, with D177.1)",
    "note": ("Validator, dimension and successor expectations are hand-derived. Digest cases carry "
             "their preimage; expect = SHA-256(preimage), auditable with an external sha256sum. "
             "preimage/tms-minimal-hand-built was written by hand and matched byte for byte. The toy "
             "TFK is a mass on a linear spring with motion confined to z = 0 (C_NOZ carries UNIT m from "
             "schema 0.3.0); under schema 0.4.0 every zone digest moved once more, by the version tag; "
             "the spring with its forms adds a DOF t, an entry E_t and the declared forms (increment 8). "
             "Both are test fixtures, not physics under research. Both residences MUST reproduce every expect. "
             "0.4.1 (S15) adds, and changes no earlier case: a DIMENSION whose repeated bases sum past "
             "-9999..9999 is refused, its canonical form lying outside the grammar; the canonical token is "
             "bounded to four digits; no admitted zone's digest moves. "
             "0.5.0 (schema 0.5.0; D176.1, D177.1): ROLE on every LAW (required) and ROLE INPUT on a DOF "
             "(optional); the TPK PARAMETERS part with D_VARIABLES ONE or SEVERAL, ONE when absent and "
             "serialized ONE; STRUCTURE_CHECK in the TMS PARAMETERS, ON when absent and serialized ON; "
             "T1's D-variable rules. Every zone digest moved once, by the version tag and the new fields; "
             "every fixture LAW carries a ROLE chosen by its physics. "
             "0.5.1 (S33, 2026-09-26): a LAW restating the motion of a FIXed DOF (the toy's and the spring's "
             "FREE_Z, corner_fix_t's EOM_Z) carries ROLE CONSTRAINT, not EOM(z); the toy's and the spring's "
             "D(TPK) and D(TFK) move once more; successor/s050-law-role-changed now changes FREE_Z back to "
             "EOM(z). No other answer moves. "
             "0.5.2 (C-MS-5, increment 11, 2026-09-28): 34 decode/ cases, each a JSON {} where a list is "
             "read, a JSON [] where an object is read, an object keyed 0 read as a list, or a valid empty "
             "object; TPC-PHP now reads the JSON as written (tpc_zone 0.5.1). No earlier answer moves.")
  },
  "cases": cases
}
open(os.path.join(os.path.dirname(os.path.abspath(__file__)), "vectors", "zone_corpus.json"), "w", encoding="utf-8", newline="\n").write(
    json.dumps(corpus, indent=1, ensure_ascii=True) + "\n")
print("wrote", len(cases), "zone cases; all match hand-derived expectations")
print("D(TPK)", dz[0]); print("D(TrM)", dz[1]); print("D(TMS)", dz[2])
print("D(TFK)", Z.d_tfk_of(TFK))
print("spring with forms: D(TPK)", dzf[0]); print("D(TrM)", dzf[1]); print("D(TFK)", Z.d_tfk_of(TFK_F))