David F Glidden
ecf5f95b0a
Kernel v1.1 §7 realised. Five defects injected into CONTROL-A as RECORDED
TRANSFORMATIONS, each with unit target, exact find/replace, what is
undemonstrated, and why no mechanical check can catch it.
THE RESULT THAT MATTERS: the twin passes EVERY mechanical check. Tiling, §3.1
tagging completeness, §3.2 Q-resolution, §3.3 heading screen, A-prohibition —
59/59 units, 100% sound, zero quarantined. It carries five load-bearing claims
that do not hold.
So the pair is the cleanest demonstration yet of the class the steward asked
about: two documents, one sound and one defective, are MECHANICALLY
INDISTINGUISHABLE. Both report 100%. The difference is visible only by reading.
That is not a flaw in the instruments — it is the design. A defect a check could
catch would not be testing the reader.
THE FIVE, each a distinct failure mode:
D1 SCOPE-WIDENING — asserts this file has a 'stated review date'; the quoted
clause is triggered by one and nothing establishes it
D2 UNDEFINED-TERM — imports 'limit of the system' and an obligation to report
limits; neither is in the axiom set or the quotations
D3 PREMISE-WEAKENED — drains the premise of the content the conclusion needs,
leaving both premise and conclusion standing
D4 SUPPORT-DELETED — removes the fifth quotation entirely and keeps the three
claims that rested on it, rewriting the lead so nothing dangles
D5 CIRCULAR — makes a premise rest on the conclusion it is a step toward
D1 and D2 are the two defects I found in my OWN draft 2 of CONTROL-A and removed.
Reintroducing them deliberately is the only honest use for them, and it means at
least two of the five are defects a careful author actually made.
GROUND TRUTH BY LEDGER. twin.py gates it bidirectionally: forward(control) == twin
AND inverse(twin) == control, both byte-exact. Forward alone would pass a ledger
that OMITS an edit, since the omitted edit is simply carried in the twin file —
which is exactly how laundering would enter. The inverse is what makes the ledger
complete rather than merely non-empty.
test_twin.py shows the gate FAILING in both laundering directions: a twin quietly
altered beyond the ledger, and a ledger recording an edit the twin does not
contain. Fixtures derived from the property, not from the code.
The tags file for the twin contains five deliberate falsehoods, marked and named,
because that is what a defective document's own tagging would say. The ledger and
the tag file disagree on purpose; the ledger governs.
Not run. The Fool has seen neither document.
109 lines
3.8 KiB
Python
Executable File
109 lines
3.8 KiB
Python
Executable File
#!/usr/bin/env python3
|
|
"""
|
|
Positive control for the defect-twin ledger gate.
|
|
|
|
The gate's whole claim is that the ledger is COMPLETE — that every difference
|
|
between control and twin is written down. A gate only ever shown passing has
|
|
demonstrated nothing, so it is shown here failing on a twin carrying an edit the
|
|
ledger does not record. That is the laundering case, and it is the only case the
|
|
gate exists for.
|
|
|
|
Fixtures are derived from the PROPERTY ("what would make 'the ledger is complete'
|
|
false?") rather than from the code, per the discrimination principle.
|
|
|
|
Usage: ./test_twin.py
|
|
"""
|
|
|
|
from __future__ import annotations
|
|
|
|
import json
|
|
import sys
|
|
from pathlib import Path
|
|
|
|
HERE = Path(__file__).resolve().parent
|
|
sys.path.insert(0, str(HERE))
|
|
from twin import apply_forward, apply_inverse, load_ledger # noqa: E402
|
|
|
|
CONTROL = HERE / "CONTROL-A-flagging-and-modifying.md"
|
|
TWIN = HERE / "CONTROL-B-flagging-and-modifying-defective.md"
|
|
LEDGER = HERE / "twin-ledger.json"
|
|
|
|
failures: list[str] = []
|
|
|
|
|
|
def check(name: str, got, want, detail: str = "") -> None:
|
|
if got != want:
|
|
failures.append(f"{name}: expected {want!r}, got {got!r}. {detail}")
|
|
print(f" FAIL {name}")
|
|
else:
|
|
print(f" ok {name}")
|
|
|
|
|
|
for p in (CONTROL, TWIN, LEDGER):
|
|
if not p.is_file():
|
|
failures.append(f"missing artifact: {p.name}")
|
|
|
|
if not failures:
|
|
control = CONTROL.read_text(encoding="utf-8")
|
|
twin = TWIN.read_text(encoding="utf-8")
|
|
ledger = load_ledger(LEDGER)
|
|
|
|
print("Round trip on the real pair:")
|
|
check("forward reproduces the twin", apply_forward(control, ledger), twin)
|
|
check("inverse reproduces the control", apply_inverse(twin, ledger), control)
|
|
|
|
print("\nPositive control — an UNLOGGED edit must be caught:")
|
|
# The laundering case: a twin quietly altered beyond what the ledger records.
|
|
laundered = twin.replace(
|
|
"What opens is the report.", "What opens is the report, and nothing else."
|
|
)
|
|
check("laundered twin actually differs", laundered != twin, True)
|
|
check(
|
|
"forward gate DETECTS the unlogged edit",
|
|
apply_forward(control, ledger) != laundered,
|
|
True,
|
|
"a ledger that cannot detect an unlogged edit establishes no ground truth",
|
|
)
|
|
check(
|
|
"inverse gate DETECTS it too",
|
|
apply_inverse(laundered, ledger) != control,
|
|
True,
|
|
)
|
|
|
|
print("\nPositive control — a ledger entry for an edit NOT made must be caught:")
|
|
phantom = json.loads(LEDGER.read_text(encoding="utf-8"))
|
|
phantom["defects"].append({
|
|
"id": "PHANTOM", "type": "TEST", "target": "", "undemonstrated": "",
|
|
"why_invisible_to_checks": "",
|
|
"edits": [{"find": "What opens is the report.",
|
|
"replace": "What opens is the report, obviously."}],
|
|
})
|
|
check(
|
|
"forward gate DETECTS a recorded edit absent from the twin",
|
|
apply_forward(control, phantom) != twin,
|
|
True,
|
|
)
|
|
|
|
print("\nEvery defect must be uniquely locatable:")
|
|
for d in ledger["defects"]:
|
|
for i, e in enumerate(d["edits"]):
|
|
check(f"{d['id']}[{i}] find is unique in control",
|
|
control.count(e["find"]), 1)
|
|
check(f"{d['id']}[{i}] replace is unique in twin",
|
|
twin.count(e["replace"]), 1)
|
|
|
|
print("\nEvery defect carries the record a grader needs:")
|
|
for d in ledger["defects"]:
|
|
check(f"{d['id']} states what is undemonstrated",
|
|
bool(d.get("undemonstrated", "").strip()), True)
|
|
check(f"{d['id']} states why no check catches it",
|
|
bool(d.get("why_invisible_to_checks", "").strip()), True)
|
|
|
|
if failures:
|
|
print(f"\nINSTRUMENT NOT VERIFIED — {len(failures)} failure(s):")
|
|
for f in failures:
|
|
print(f" - {f}")
|
|
sys.exit(1)
|
|
|
|
print("\nLedger gate verified, and shown failing on both laundering directions.")
|