The Principia Machina/TPC-PY/tpc sr9.py: Difference between revisions

Latest revision as of 02:11, 30 September 2026

# -*- coding: utf-8 -*-
"""
TPC-PY --- SR9 C-test harness (TPC step 2, increment 3)
=======================================================
Discharges the SR9 part of TPS 4.5.3 OWED C-08: "the mechanical
implementation of ... SR9; the synthetic record suite for C1, C2, C4".
(SR3, SR4, SR8 were increment 1, tpc_strike.py.) Standard library only;
Python 3.7+; Windows/Linux.

WHAT IS CHECKED (TPS 4.5.2; check-class matrix row 17, MECHANICAL when
the entry is executable; on failure CAC refuses certification):
  C1  the entry never ranks a record failing SR1 above one passing it;
  C2  within a regime, adding an ASSUMPTION never improves rank, except
      in a declared limiting case naming its DOMAIN, applied only there;
  C4  the entry does not let an M contradiction strike an L derivation.
  Plus the TPS 4.5.3 gate: the TMS declares k, STEP CONVENTION and N_x.
  C3 and C5 are INSPECTION (row 18) and are not here.

EXECUTABLE ENTRY INTERFACE (what the harness runs):
  key(rid, records, tfk)            -> tuple; lexicographic; lower = closer
  resolve(id1, id2, records, tfk)   -> "STRIKE:<id>" | "AUDIT" |
                                       "GAP:<id>" | "DOMAIN:<id>"
  limiting                          -> list of DOMAIN strings where a C2
                                       exemption is declared
  A UWC declares an executable local yardstick in the closed grammar of
  the TMS zone schema (D100.1); tpc_yardstick compiles it into this
  interface, and every check below accepts that entry tuple in place of a
  fixture name.

FIXTURES. ENTRIES holds one compliant entry (the strike skeleton itself)
and deliberately broken entries, each violating exactly one check, so the
corpus proves the harness catches what it must (a check that accepts what
it should reject is a soundness defect).

LIMIT. A pass on a finite synthetic suite is evidence, not proof: an entry
can still violate C1/C2/C4 on records the suite lacks. This is the design
TPS 4.5.2 specifies (MECHANICAL on a synthetic record suite); C3/C5 stay
INSPECTION.

SYNTHETIC RECORD FIELDS: regime ("L"|"M"), assumptions [ids], cites [ids],
steps (int), domain (str), sr1_fail (bool; given, since SR1 detection
needs a derivation oracle and is not a TPC function).
"""

import tpc_strike as S

TPC_SR9_VERSION = "0.1.1"     # proposed PATCH with TPC-PY 0.2.0 (C-MS-5: TPC-PHP copies before it adds the fresh assumption)
_FRESH = "~FRESH~"   # prefix for the assumption added by the C2 transform


def _a(rid, records, tfk):
    return S.a_of_r(rid, records, tfk)


def _sr1(r):
    return 1 if r["sr1_fail"] else 0


# ---- key builders (total functions of record fields) ---------------------
def _key_skeleton(rid, records, tfk):
    """Skeleton (i)+(iii): SR1-failing records sort after all passing ones
    (struck without ranking); then d(r) = (a(r), s(r))."""
    r = records[rid]
    return (_sr1(r), _a(rid, records, tfk), int(r["steps"]))


def _key_naive(rid, records, tfk):
    """Broken for C1: plain d(r), ignoring SR1 status."""
    r = records[rid]
    return (_a(rid, records, tfk), int(r["steps"]))


def _key_more_is_better(rid, records, tfk):
    """Broken for C2: more assumptions rank closer."""
    r = records[rid]
    return (_sr1(r), -_a(rid, records, tfk), int(r["steps"]))


def _key_invert_in(domain):
    """Inverts the assumption count inside one DOMAIN only (a limiting case)."""
    def key(rid, records, tfk):
        r = records[rid]
        a = _a(rid, records, tfk)
        return (_sr1(r), -a if r["domain"] == domain else a, int(r["steps"]))
    return key


# ---- resolvers -----------------------------------------------------------
def _sr5(key, id1, id2, records, tfk):
    k1, k2 = key(id1, records, tfk), key(id2, records, tfk)
    if k1 < k2:
        return "STRIKE:" + id2
    if k2 < k1:
        return "STRIKE:" + id1
    return "AUDIT"


def _resolve_regime_aware(key):
    """SR7 for an L-M pair (never strike the L derivation: named GAP when
    a(L) > 0, DOMAIN finding when a(L) = 0); SR5 on the key otherwise."""
    def resolve(id1, id2, records, tfk):
        r1, r2 = records[id1], records[id2]
        if r1["regime"] != r2["regime"]:
            lid = id1 if r1["regime"] == "L" else id2
            return ("GAP:" if _a(lid, records, tfk) > 0 else "DOMAIN:") + lid
        return _sr5(key, id1, id2, records, tfk)
    return resolve


def _resolve_ignores_regime(key):
    """Broken for C4: SR5 on the key for every pair, L-M included."""
    def resolve(id1, id2, records, tfk):
        return _sr5(key, id1, id2, records, tfk)
    return resolve


_K_LIM = _key_invert_in("LIM")
_K_OTHER = _key_invert_in("OTHER")

ENTRIES = {
    # name: (key, resolve, declared limiting-case DOMAINs)
    "skeleton":            (_key_skeleton, _resolve_regime_aware(_key_skeleton), []),
    "naive_d":             (_key_naive, _resolve_regime_aware(_key_naive), []),
    "more_is_better":      (_key_more_is_better, _resolve_regime_aware(_key_more_is_better), []),
    "ignores_regime":      (_key_skeleton, _resolve_ignores_regime(_key_skeleton), []),
    "limiting_declared":   (_K_LIM, _resolve_regime_aware(_K_LIM), ["LIM"]),
    "limiting_undeclared": (_K_LIM, _resolve_regime_aware(_K_LIM), []),
    "limiting_leak":       (_K_OTHER, _resolve_regime_aware(_K_OTHER), ["LIM"]),
}


def _entry(entry):
    """A fixture by name, or an entry tuple (key, resolve, limiting) built
    elsewhere, such as a declared TMS yardstick (tpc_yardstick)."""
    if isinstance(entry, tuple):
        return entry
    if entry not in ENTRIES:
        raise KeyError("sr9: unknown entry %r" % entry)
    return ENTRIES[entry]


def _suite(suite):
    return suite["records"], list(suite.get("tfk_assumptions", []))


# ---- the checks ----------------------------------------------------------
def sr9_c1(entry, suite):
    """C1. Witnesses "F>P": SR1-failing F ranked strictly above passing P.
    Returns [pass, sorted witnesses]."""
    key, _, _ = _entry(entry)
    recs, tfk = _suite(suite)
    fails = sorted(i for i, r in recs.items() if r["sr1_fail"])
    passes = sorted(i for i, r in recs.items() if not r["sr1_fail"])
    w = []
    for f in fails:
        kf = key(f, recs, tfk)
        for p in passes:
            if kf < key(p, recs, tfk):
                w.append(f + ">" + p)
    w.sort()
    return [not w, w]


def sr9_c2(entry, suite):
    """C2. For each record r, r+ = r with one fresh assumption (same regime).
    A violation is key(r+) < key(r) outside a declared limiting DOMAIN; the
    same inside one is recorded as exempt. Returns [pass, violations, exempt]."""
    key, _, limiting = _entry(entry)
    recs, tfk = _suite(suite)
    viol, exempt = [], []
    for rid in sorted(recs):
        plus = dict(recs[rid])
        plus["assumptions"] = list(plus.get("assumptions", [])) + [_FRESH + rid]
        recs2 = dict(recs)
        recs2[rid + "+"] = plus
        if key(rid + "+", recs2, tfk) < key(rid, recs2, tfk):
            (exempt if recs[rid]["domain"] in limiting else viol).append(rid)
    viol.sort()
    exempt.sort()
    return [not viol, viol, exempt]


def sr9_c4(entry, suite):
    """C4. For each listed L-M contradiction, resolve in both orders; a
    violation is any outcome striking the L record. Returns
    [pass, sorted "L|M" witnesses]."""
    _, resolve, _ = _entry(entry)
    recs, tfk = _suite(suite)
    viol = []
    for a, b in suite.get("contradictions", []):
        if recs[a]["regime"] == recs[b]["regime"]:
            continue                                  # C4 concerns M-vs-L only
        lid, mid = (a, b) if recs[a]["regime"] == "L" else (b, a)
        outcomes = {resolve(lid, mid, recs, tfk), resolve(mid, lid, recs, tfk)}
        if ("STRIKE:" + lid) in outcomes:
            viol.append(lid + "|" + mid)
    viol.sort()
    return [not viol, viol]


def sr9_harness(entry, suite):
    """Summary for the CAC gate: [C1 pass, C2 pass, C4 pass, total violations]."""
    c1, c2, c4 = sr9_c1(entry, suite), sr9_c2(entry, suite), sr9_c4(entry, suite)
    return [c1[0], c2[0], c4[0], len(c1[1]) + len(c2[1]) + len(c4[1])]


def tms_params_ok(params):
    """TPS 4.5.3: CAC refuses a TMS that does not declare k (SR3), STEP
    CONVENTION (SR4) or N_x (SR6). k > 0; STEP CONVENTION a non-empty
    string; N_x an integer >= 2. Returns [pass, missing-or-invalid names]."""
    missing = []
    k = params.get("k")
    if isinstance(k, bool) or not isinstance(k, (int, float)) or not k > 0:
        missing.append("k")
    sc = params.get("step_convention")
    if not isinstance(sc, str) or not sc.strip():
        missing.append("step_convention")
    nx = params.get("n_x")
    if isinstance(nx, bool) or not isinstance(nx, int) or nx < 2:
        missing.append("n_x")
    return [not missing, missing]