Verify
For anyone who establishes an expensive fact once and then never re-checks it because re-checking feels expensive. Register the fact with the input files its derivation stood on; Verify keeps a content-hash certificate and re-checks it in a second. FRESH if the inputs are unchanged, STALE if one moved, DEAD if the ground is gone.
The honest edge
FRESH means the byte-truth inputs are unchanged, never that the fact is TRUE (⊢, not ⊨). It re-checks the ground you named — name too few inputs and a real dependency can move without tripping STALE. Byte-truth facts only; live facts (prices, who's CEO) can't be cheaply certified.
Run it
python3 verify.py --help
smoke_test.py (10/10)
Python stdlib only
The code — every file that ships
verify.py768 lineson GitHub →
#!/usr/bin/env python3
# SPDX-License-Identifier: MIT
"""
verify.py — the Verification System's one net-new primitive: a cheap re-check of
a learned fact, keyed on a kept certificate.
The idea (Kindling deliberate, S16.1613, verification-system line):
"Don't trust, verify" is cardinal — but verify CHEAPLY. Establishing a fact
X -> Y is expensive (~20 min). Re-checking that a claimed X -> Y still holds is
cheap (~1s) IF you kept the right certificate. That is the NP / certificate-
checking asymmetry, and the certificate is a CONTENT HASH of the derivation's
byte-truth inputs. A fact is FRESH iff its inputs still hash to what they
hashed when the certificate was kept; if an input moved, it is STALE and must
be re-derived; if the derivation's ground is gone (a required input missing) or
the fact was retired, it is DEAD.
This is content-addressed cache invalidation over a derivation DAG — the build-
cache primitive (Nix/Bazel/ccache), git's own Merkle tree, Certificate
Transparency — the primitive the floor already grew independently
(`git hash-object`, Amber blob-SHA fixity, the Loop-Line content-address) but
never generalized into a cheap fact-re-check. This is that generalization, and
nothing more (Constraint drive: a spine + one primitive + the taxonomy, no
engine).
THE HONEST CEILING (Wren's binding cut, deliberate C2):
The verdict is CERTIFICATE-FRESHNESS, NEVER TRUTH. `fresh` means the byte-truth
inputs the derivation stood on are UNCHANGED — it does NOT re-run the judgment
that made X -> Y true. The claim was judged true when it was ESTABLISHED; this
tool proves the ground under it has not moved. Calling `fresh` "true" is the
Cruise's "1,511 passing tests" lie one level up (Match != Prevention, borrowed
from Wobble RECALL). A verification cache is VISIBILITY, NOT IMMUNITY: it cannot
force re-derivation on a miss; the operator/floor stays the witness.
THE FORMAL LIMIT (deliberate C5, Shannon Corollary — named, not relabeled around):
Cheap verification holds ONLY for the byte-truth-derivable fact class — facts
whose input set is finite, content-addressable, and stable-when-nothing-changes.
Live/external facts ("current price", "who is CEO now") cannot be cheaply
certified — their input set is the world, which you cannot cheaply re-hash — and
route to the Customs House re-acquire path (fail-closed), NOT this cache. The
`provenance_class` field carries that split (C4: internal fails open to
re-derive; external fails closed).
Reuse map (C6 — composition, not duplication):
- `git hash-object` -> the content-address primitive (the certificate)
- the Lode's append-only fold -> the registry shape (verified.jsonl -> fold)
- the Loop-Line content-addr -> the re-check-on-pull mechanic
- Amber blob-SHA fixity -> snapshot certs
THE ASSUMPTION CELL (S16.1707, claim-grounding line — the family's second species):
A FACT is a claim whose ground you CHECKED and PINNED (the certificate = the
input hashes). An ASSUMPTION is a claim you are leaning on whose ground you have
NOT checked — you DEFERRED the check. Same claim; different grounding-state. They
are ONE register at two points of one lifecycle:
assume --(discharge: run the path, pin the inputs)--> verified (a fact)
verified --(an input moves)--> STALE --(re-derive)--> verified
(STALE is a fact fallen back to assumption-status: leaned-on, un-recertified.)
FORMAL GROUND (why this is not a bolt-on):
- Promotion assume->fact IS natural-deduction DISCHARGE: an assumption is an
undischarged hypothesis [A]; `discharge` closes it by pinning its ground.
Mechanized for free by the fold's latest-wins (a `verified` event with the
same fact_id supersedes the `assumed` one).
- A fact's verdict is derivability: `fresh` means the derivation still holds
on unchanged premises (|-), NEVER that the claim is true in the world (|=).
`fresh != true` IS `|- != |=`. The assumption razor is the same gap one
species over: `UNEXPIRED != true` — an assumption whose expiry has not
tripped is only NOT-YET-KNOWN-STALE, never verified.
- The species boundary is DECIDABILITY (Shannon Corollary). A fact's check is
a decidable, cheap hash-compare over a finite pinned input set. An
assumption's ground is NOT in that class yet (that is WHY it is deferred),
so its defeater is an EXPIRY CONDITION, not a hash-watch.
THE DECIDABLE-COLLAPSE RULE (the one that keeps this honest & minimal):
If your expiry condition is "when file X changes", that is BYTE-WATCHABLE —
it is a FACT, not an assumption: `register` it with X as an input. `assume`
is deliberately for the NON-byte-watchable case (a date, an external event, a
human judgement), and therefore takes NO --inputs. Its defeater cannot be
auto-checked, so `verify` on an assumption does NOT fake a freshness verdict —
it SURFACES the claim, its verification path, its expiry, and the razor, and
hands the judgement to the human (visibility, not immunity; Nyx: hope is not a
control, so the tool does not pretend to be one).
THE DECISION CELL (S16.1822, claim-grounding line — the family's THIRD species):
A FACT is a claim whose ground you CHECKED and PINNED (its input hashes). An
ASSUMPTION is a claim whose ground you DEFERRED. A DECISION is a claim of the
form "A beats B" whose ground is neither a set of input files nor a deferred
expiry — it is the set of PREMISES the choice rested on, and each premise is
itself a register entry (a fact-id or an assume-id). So a decision's certificate
is a COMPOSITE, and its grounding-state is DERIVED from its premises':
decide --decision-id D --claim "A beats B" --options "A;B;C" --chose A
--premises fact-1 assume-2 ... (premises = existing entry ids)
verify --fact-id D folds the premises' grounding-states:
FRESH iff every premise-FACT is FRESH ∧ no premise is a live assumption
STALE iff any premise-FACT moved (named — that is the defeater)
DEAD iff any premise was retired or is not on file (the ground is gone)
ASSUMED iff the decision rests on a live assumption (surfaced — you judge)
Trap 1 avoided — NO NEW ENGINE: `decided` is a third `kind` in the SAME
register, the SAME append-only log, the SAME latest-wins fold, composing the
fact + assumption cells. Not a decision engine; a third grounding-state.
Trap 2 avoided — the decision does NOT re-hash its premises' input files. It
DEFERS to each premise's OWN certificate (its `verify`), recursing for a nested
decision-premise. Hashing them directly would duplicate the fact cell and lose
an assumption-premise's human-judged defeater.
THE RAZOR, ONE LEVEL UP (the honest ceiling — get this exactly right):
decision-fresh != decision-still-right.
The premises holding does NOT mean A still beats B: a NEW option F could beat A
with no premise moving. `verify(decision)` checks PREMISE-STABILITY — it never
re-runs the choice. Same |- vs |= shape as the fact cell: premises-unchanged
(|-) is not conclusion-still-optimal (|=). Composed with the assumption razor:
a decision is only as grounded as its WEAKEST premise, and even all-fresh
premises do not re-decide the question.
Decidable-collapse analog: a decision whose premises are all byte-watchable
FACTS has a fully decidable re-check (verify each premise fact); one resting on
an ASSUMPTION inherits that assumption's human-judged defeater and SURFACES.
The use-case taxonomy (deliberate C3, the operator's explicit ask):
REGISTER a fact after an expensive, re-encounterable derivation (not everything)
ASSUME a claim you are leaning on but have NOT yet grounded (deferred check)
DECIDE record a choice "A beats B" + the premises it rested on (grounds keyed)
ASK (verify) before a load-bearing move / at check-before-build
DISCHARGE run an assumption's verification path, pin its inputs -> it becomes a fact
RE-DERIVE on stale or a cache miss
CALL DEAD (retire) when the DERIVATION is retired, not just an input moved
SUPERSEDE re-derive to a different value -> old cert superseded, not deleted
QUARANTINE external facts fail closed (provenance_class)
Verbs:
register --fact-id ID --claim "..." [--edge "X->Y"] --inputs f1 [f2 ...]
[--provenance internal|external]
assume --fact-id ID --claim "..." --path "how to discharge" --expiry "the defeater"
[--evidence "the weak signal leaned on"]
decide --decision-id ID --claim "A beats B" --options "A;B;C" --chose A
--premises f1 [f2 ...] (refs to existing entries)
verify --fact-id ID re-check (fact) / SURFACE (assumption) / FOLD (decision)
discharge --fact-id ID --inputs f1 [f2 ...] run the path, pin the ground -> a fact
retire --fact-id ID --reason "..." call it dead (Wren)
list the derived registry (pure fold, latest-wins)
fold --check fold-twice-identical invariant (the Lode contract)
A decision-id lives in the SAME keyspace as fact-ids (one register). Verify one
with `verify --fact-id <decision-id>` — there is no separate decision verify.
Exit codes (verify):
0 fresh — every input hash unchanged (a fact) / every premise fresh (a decision).
CERTIFICATE FRESH, not "true".
3 stale — at least one input hash / premise-fact moved -> re-derive
5 dead — a required input missing, a premise not on file, OR retired
4 unregistered — no certificate on file for that fact_id
6 assumed — the id is an ASSUMPTION (or a decision resting on a live assumption):
SURFACED with path + expiry + the razor (UNEXPIRED != true).
2 error / usage (includes a decision certificate that references itself — a cycle)
"""
import argparse
import hashlib
import json
import os
import subprocess
import sys
from datetime import datetime, timezone
# Standalone default: the store lives under the current working directory (like .git/).
# Override with VERIFY_REPO_ROOT to point the fact store somewhere else.
REPO_ROOT = os.getcwd()
FACTS_RELDIR = ".verify"
EVENTS_BASENAME = "verified.jsonl"
FRESH, STALE, DEAD, UNREGISTERED, ERROR = 0, 3, 5, 4, 2
ASSUMED = 6 # the assumption cell: the id is ungrounded — surfaced, not verified
# The decision cell (S16.1822) is a third grounding-state that REUSES these codes,
# no new taxonomy: a decision folds to FRESH/STALE/DEAD, or ASSUMED when it rests
# on a live assumption-premise. ERROR covers a self-referential (cyclic) certificate.
# ── The certificate primitive: content-address a byte-truth input ──────
def blob_sha(path):
"""The git blob SHA-1 of a file's bytes — the SAME primitive the floor uses
(`git hash-object`, Amber, the Loop-Line). Computed directly so the tool works
on any path with no subprocess and no git-checkout dependency, and returns the
identical value `git hash-object <path>` would. Returns None if the file is
absent from disk (the DEAD signal: the derivation's ground is gone)."""
if not os.path.isfile(path):
return None
with open(path, "rb") as fh:
data = fh.read()
header = b"blob " + str(len(data)).encode() + b"\0"
return hashlib.sha1(header + data).hexdigest()
def events_path(repo_root):
return os.path.join(repo_root, FACTS_RELDIR, EVENTS_BASENAME)
def read_events(repo_root):
"""Read the append-only event log (JSONL). Absent log = empty set (cold-safe)."""
p = events_path(repo_root)
if not os.path.isfile(p):
return []
events = []
with open(p, "r", encoding="utf-8") as fh:
for lineno, line in enumerate(fh, 1):
line = line.strip()
if not line:
continue
try:
ev = json.loads(line)
except json.JSONDecodeError as exc:
raise ValueError(f"{EVENTS_BASENAME}:{lineno}: bad JSON: {exc}")
events.append(ev)
return events
def append_event(repo_root, ev):
"""Append-only write (the Lode / Strike-Log contract: never rewrite a row)."""
p = events_path(repo_root)
os.makedirs(os.path.dirname(p), exist_ok=True)
existing = read_events(repo_root)
same_day = [e for e in existing if e.get("date") == ev["date"]]
ev["seq"] = 1 + max([e.get("seq", 0) for e in same_day], default=0)
with open(p, "a", encoding="utf-8") as fh:
fh.write(json.dumps(ev, sort_keys=True) + "\n")
return ev
# ── The pure fold: events -> the derived registry (latest-wins per fact) ──
def fold(events):
"""Pure, deterministic fold over the append-only log -> the registry projection.
Latest event per fact_id wins (register / retire). Folding the same events twice
yields a byte-identical projection (the Lode's fold-twice-identical contract)."""
order = sorted(range(len(events)), key=lambda i: (
events[i].get("date", ""), events[i].get("seq", 0), i))
latest = {}
for i in order:
ev = events[i]
fid = ev.get("fact_id")
if fid is None:
continue
latest[fid] = ev # last write wins in deterministic order
registry = []
for fid in sorted(latest):
registry.append(latest[fid])
return registry
def render_registry(registry):
"""Deterministic markdown-ish text render of the derived registry (for `list`)."""
lines = ["# The Verification Registry (derived — do not hand-edit)",
f"# facts: {len(registry)}", ""]
for rec in registry:
kind = rec.get("kind")
if kind == "retired":
state = "RETIRED (dead)"
elif kind == "assumed":
state = "ASSUMED (ungrounded)"
elif kind == "decided":
state = "DECIDED (premise-grounded)"
else:
state = rec.get("provenance_class", "internal")
lines.append(f"- {rec['fact_id']} [{state}]")
lines.append(f" claim: {rec.get('claim', '')}")
if rec.get("edge"):
lines.append(f" edge: {rec['edge']}")
if kind == "retired":
lines.append(f" retired: {rec.get('reason', '')}")
elif kind == "assumed":
lines.append(f" verification-path: {rec.get('verification_path', '')}")
lines.append(f" expiry (defeater): {rec.get('expiry', '')}")
if rec.get("evidence"):
lines.append(f" evidence: {rec['evidence']}")
elif kind == "decided":
opts = rec.get("options", [])
prem = rec.get("premises", [])
lines.append(f" chose: {rec.get('chose', '')} (of {', '.join(opts)})")
lines.append(f" premises: {len(prem)} entry-ref(s) — {', '.join(prem)}")
else:
lines.append(f" inputs: {len(rec.get('input_refs', []))} content-hashed @ {rec.get('established_at', '')}")
return "\n".join(lines) + "\n"
# ── The verbs ──────────────────────────────────────────────────────────
def cmd_register(args, repo_root):
inputs = args.inputs or []
if not inputs:
print("verify register: --inputs is required (a fact with no byte-truth "
"inputs has no certificate)", file=sys.stderr)
return ERROR
input_hashes = []
for ref in inputs:
h = blob_sha(ref if os.path.isabs(ref) else os.path.join(repo_root, ref))
if h is None:
print(f"verify register: input not found on disk: {ref}", file=sys.stderr)
return ERROR
input_hashes.append(h)
now = datetime.now(timezone.utc)
ev = {
"kind": "verified",
"fact_id": args.fact_id,
"claim": args.claim,
"edge": args.edge or "",
"input_refs": inputs,
"input_hashes": input_hashes,
"provenance_class": args.provenance,
"established_at": now.isoformat(timespec="seconds"),
"date": now.strftime("%d.%H%M"),
}
ev = append_event(repo_root, ev)
print(f"REGISTERED {args.fact_id} ({len(inputs)} input(s) content-hashed, "
f"provenance={args.provenance})")
print(f" certificate kept @ {ev['established_at']}")
print(f" NOTE: registers the CERTIFICATE (the ground), not a truth guarantee.")
return 0
def latest_for(events, fact_id):
recs = [e for e in events if e.get("fact_id") == fact_id]
if not recs:
return None
recs.sort(key=lambda e: (e.get("date", ""), e.get("seq", 0)))
return recs[-1]
# ── The certificate re-check core (shared by the fact + decision cells) ──
def fact_verdict(rec, repo_root):
"""For a kind=verified rec: re-check its kept certificate against disk.
Returns (code, moved, missing) — the ONE hash-compare both cmd_verify and a
decision's premise-fold call, so the two cells share a verdict, never fork one."""
refs = rec.get("input_refs", [])
kept = rec.get("input_hashes", [])
moved, missing = [], []
for ref, k in zip(refs, kept):
cur = blob_sha(ref if os.path.isabs(ref) else os.path.join(repo_root, ref))
if cur is None:
missing.append(ref)
elif cur != k:
moved.append(ref)
if missing:
return DEAD, moved, missing
if moved:
return STALE, moved, missing
return FRESH, moved, missing
def premise_state(events, repo_root, pid, seen):
"""Resolve ONE premise id to its grounding-state CODE — the decision cell's
Trap-2 discipline made mechanical: it DEFERS to the premise's OWN certificate
(never re-hashes the premise's files as the decision's inputs), recursing for a
nested decision-premise and guarding cycles. A premise not on file -> DEAD (the
ground is gone); retired -> DEAD; a live assumption -> ASSUMED; a fact -> its
fact_verdict; a decision -> its folded verdict."""
if pid in seen:
return ERROR # a self-referential (cyclic) decision certificate
rec = latest_for(events, pid)
if rec is None:
return DEAD
kind = rec.get("kind")
if kind == "retired":
return DEAD
if kind == "assumed":
return ASSUMED
if kind == "decided":
return decision_verdict(events, repo_root, rec, seen | {pid})[0]
return fact_verdict(rec, repo_root)[0]
def decision_verdict(events, repo_root, rec, seen):
"""Fold a decision's premises' grounding-states -> (code, breakdown).
The decision's ground is DERIVED from its premises', not hashed. Precedence:
DEAD > STALE > ASSUMED > FRESH (a gone premise is worse than a moved one is
worse than an un-grounded one); ERROR on a cycle. `breakdown` is [(pid, code)]."""
premises = rec.get("premises", [])
breakdown = [(pid, premise_state(events, repo_root, pid, seen)) for pid in premises]
codes = [c for _, c in breakdown]
if ERROR in codes:
return ERROR, breakdown
if not premises:
# a decision with no premises has no ground — treat as DEAD (defensive;
# `decide` refuses to author one, so this is only reachable via a hand-edit)
return DEAD, breakdown
for worst in (DEAD, STALE, ASSUMED):
if worst in codes:
return worst, breakdown
return FRESH, breakdown
def _code_word(code):
return {FRESH: "FRESH", STALE: "STALE", DEAD: "DEAD",
ASSUMED: "ASSUMED", ERROR: "CYCLE", UNREGISTERED: "UNREGISTERED"}.get(code, str(code))
_CODE_NAME = {FRESH: "fresh", STALE: "stale", DEAD: "dead",
UNREGISTERED: "unregistered", ASSUMED: "assumed", ERROR: "error"}
def _verify_json(args, repo_root, events, rec):
"""Machine-readable verdict on stdout (the CEILING still prints on stderr, so a
--json pipe stays clean). Reuses fact_verdict / decision_verdict, so the JSON
verdict and exit code are identical to the human path."""
out = {"fact_id": args.fact_id}
if rec is None:
out.update(verdict="unregistered", code=UNREGISTERED)
print(json.dumps(out, sort_keys=True)); return UNREGISTERED
kind = rec.get("kind")
if kind == "retired":
out.update(verdict="dead", code=DEAD, reason=rec.get("reason", ""))
print(json.dumps(out, sort_keys=True)); return DEAD
if kind == "assumed":
out.update(verdict="assumed", code=ASSUMED, claim=rec.get("claim", ""),
verification_path=rec.get("verification_path", ""),
expiry=rec.get("expiry", ""))
print(json.dumps(out, sort_keys=True)); return ASSUMED
if kind == "decided":
code, breakdown = decision_verdict(events, repo_root, rec, {args.fact_id})
out.update(verdict=_CODE_NAME.get(code, "error"), code=code,
chose=rec.get("chose", ""),
premises=[{"id": pid, "state": _CODE_NAME.get(c, "error")}
for pid, c in breakdown])
print(json.dumps(out, sort_keys=True)); return code
code, moved, missing = fact_verdict(rec, repo_root)
out.update(verdict=_CODE_NAME.get(code, "error"), code=code,
moved=moved, missing=missing,
provenance=rec.get("provenance_class", "internal"))
print(json.dumps(out, sort_keys=True)); return code
def cmd_verify(args, repo_root):
events = read_events(repo_root)
rec = latest_for(events, args.fact_id)
if getattr(args, "json", False):
return _verify_json(args, repo_root, events, rec)
if rec is None:
print(f"UNREGISTERED {args.fact_id} — no certificate on file. "
f"This is a cache MISS: re-derive the fact and register it.")
return UNREGISTERED
if rec.get("kind") == "retired":
print(f"DEAD {args.fact_id} — the derivation was retired "
f"({rec.get('reason', 'no reason given')}). Do not re-check a corpse.")
return DEAD
if rec.get("kind") == "assumed":
# An assumption has NO pinned inputs to hash — surfacing it is the whole
# point. Do NOT fake a freshness verdict on a human-judged defeater
# (Nyx: hope is not a control; the tool does not pretend to be one).
print(f"ASSUMED {args.fact_id} — this is an ASSUMPTION, not a fact. You are "
f"about to lean on UNGROUNDED ground.")
print(f" claim: {rec.get('claim', '')}")
print(f" verification-path (run this to DISCHARGE it -> fact): "
f"{rec.get('verification_path', '')}")
print(f" expiry (the defeater — YOU judge whether it has tripped): "
f"{rec.get('expiry', '')}")
if rec.get("evidence"):
print(f" evidence leaned on: {rec['evidence']}")
print(f" RAZOR: UNEXPIRED != true. An assumption whose expiry has not "
f"tripped is only NOT-YET-KNOWN-STALE — never verified.")
print(f" If the expiry is really 'a file changed', this is a FACT: "
f"register it with that file as an input instead.")
return ASSUMED
if rec.get("kind") == "decided":
# A decision's ground is its premises. Fold their grounding-states —
# DEFER to each premise's own certificate (Trap 2), never re-hash them.
code, breakdown = decision_verdict(events, repo_root, rec, {args.fact_id})
chose = rec.get("chose", "?")
claim = rec.get("claim", "")
if code == ERROR:
cyc = [p for p, c in breakdown if c == ERROR]
print(f"CYCLE {args.fact_id} — this decision certificate references "
f"itself (premise(s): {', '.join(cyc)}). A decision cannot ground "
f"itself; the certificate is malformed.")
return ERROR
# Name every premise in each failing class — the operator sees the whole
# ground, then the single worst verdict.
dead = [p for p, c in breakdown if c == DEAD]
stale = [p for p, c in breakdown if c == STALE]
assumed = [p for p, c in breakdown if c == ASSUMED]
if code == DEAD:
print(f"DEAD {args.fact_id} — the decision '{claim}' (chose {chose}) rests "
f"on premise(s) whose ground is GONE: {', '.join(dead)} "
f"(retired or not on file). The choice is no longer grounded.")
elif code == STALE:
print(f"STALE {args.fact_id} — the decision '{claim}' (chose {chose}) rests "
f"on premise-fact(s) that MOVED: {', '.join(stale)}. "
f"Re-derive the premise(s), then this decision may need re-deciding.")
elif code == ASSUMED:
print(f"ASSUMED {args.fact_id} — the decision '{claim}' (chose {chose}) rests "
f"on LIVE assumption(s): {', '.join(assumed)}. Its ground is only as "
f"grounded as those — YOU judge whether they still hold.")
else:
print(f"FRESH {args.fact_id} — the decision '{claim}' (chose {chose}): all "
f"{len(breakdown)} premise(s) still hold "
f"({', '.join(p for p, _ in breakdown)}).")
# THE RAZOR, one level up — printed on EVERY decision verdict (honest ceiling).
print(f" RAZOR: decision-fresh != decision-still-right. Premises holding does "
f"NOT mean {chose} still wins — a NEW option could beat it with no premise "
f"moving. This checks PREMISE-STABILITY, it never re-runs the choice.")
return code
code, moved, missing = fact_verdict(rec, repo_root)
if code == DEAD:
print(f"DEAD {args.fact_id} — required input(s) missing from disk: "
f"{', '.join(missing)}. The derivation's ground is gone.")
return DEAD
if code == STALE:
print(f"STALE {args.fact_id} — input(s) moved since the certificate was "
f"kept: {', '.join(moved)}. Re-derive and re-register.")
return STALE
refs = rec.get("input_refs", [])
prov = rec.get("provenance_class", "internal")
print(f"FRESH {args.fact_id} — certificate re-checks: all {len(refs)} input(s) "
f"unchanged since {rec.get('established_at', '?')} (provenance={prov}).")
print(f" Cheap re-check passed. This asserts the GROUND is unchanged, "
f"NOT that the claim was re-judged true.")
if rec.get("edge"):
print(f" provenance: {rec['edge']}")
return FRESH
def cmd_assume(args, repo_root):
"""Register an ASSUMPTION — a claim leaned on but NOT yet grounded. Takes no
--inputs by design: an assumption has no pinned ground (that is what makes it
an assumption). Its defeater is a human-judged expiry, not a hash-watch."""
now = datetime.now(timezone.utc)
ev = {
"kind": "assumed",
"fact_id": args.fact_id,
"claim": args.claim,
"verification_path": args.path,
"expiry": args.expiry,
"evidence": args.evidence or "",
"provenance_class": "internal",
"established_at": now.isoformat(timespec="seconds"),
"date": now.strftime("%d.%H%M"),
}
append_event(repo_root, ev)
print(f"ASSUMED {args.fact_id} — logged as an UNGROUNDED claim (deferred check).")
print(f" verification-path: {args.path}")
print(f" expiry (defeater): {args.expiry}")
print(f" NOTE: this is NOT a fact. `verify` will SURFACE it (exit 6), not "
f"certify it. Run `discharge` to promote it once the path is run.")
return 0
def cmd_discharge(args, repo_root):
"""Discharge an assumption -> a fact. Runs the verification path's RESULT: the
caller pins the byte-truth inputs the (now-run) derivation stood on, and we
append a `verified` event with the SAME fact_id. The fold's latest-wins makes
it a fact (natural-deduction discharge, mechanized). `verify` then returns FRESH."""
events = read_events(repo_root)
rec = latest_for(events, args.fact_id)
if rec is None:
print(f"verify discharge: {args.fact_id} is not on file — nothing to "
f"discharge (assume it first, or register it directly as a fact).",
file=sys.stderr)
return ERROR
if rec.get("kind") != "assumed":
print(f"verify discharge: {args.fact_id} is not an open assumption "
f"(kind={rec.get('kind')}). Discharge only promotes an assumption.",
file=sys.stderr)
return ERROR
inputs = args.inputs or []
if not inputs:
print("verify discharge: --inputs is required (discharge PINS the ground "
"the verification path stood on — that is the certificate).",
file=sys.stderr)
return ERROR
input_hashes = []
for ref in inputs:
h = blob_sha(ref if os.path.isabs(ref) else os.path.join(repo_root, ref))
if h is None:
print(f"verify discharge: input not found on disk: {ref}", file=sys.stderr)
return ERROR
input_hashes.append(h)
now = datetime.now(timezone.utc)
ev = {
"kind": "verified",
"fact_id": args.fact_id,
"claim": rec.get("claim", ""),
"edge": (args.edge or rec.get("verification_path", "")),
"input_refs": inputs,
"input_hashes": input_hashes,
"provenance_class": rec.get("provenance_class", "internal"),
"established_at": now.isoformat(timespec="seconds"),
"date": now.strftime("%d.%H%M"),
}
append_event(repo_root, ev)
print(f"DISCHARGED {args.fact_id} — assumption promoted to FACT "
f"({len(inputs)} input(s) now content-hashed). Natural-deduction "
f"discharge: the hypothesis is closed.")
print(f" `verify` now returns FRESH while the ground holds — and STALE the "
f"moment it moves (a fact can fall back to assumption-status).")
return 0
def cmd_decide(args, repo_root):
"""Record a DECISION — a choice 'A beats B' + the premises it rested on. The
premises are REFERENCES to existing register entries (fact-ids / assume-ids),
not fresh inputs (Trap 2): the decision's ground is COMPOSITE, and `verify`
defers to each premise's own certificate. A decision-id lives in the same
keyspace as fact-ids (one register)."""
options = [o.strip() for o in (args.options or "").replace(";", ",").split(",") if o.strip()]
if len(options) < 2:
print("verify decide: --options needs at least two choices (a decision is "
"'A beats B'); separate with ';' or ','.", file=sys.stderr)
return ERROR
if args.chose not in options:
print(f"verify decide: --chose {args.chose!r} is not among --options "
f"({', '.join(options)}). The chosen option must be one of the options.",
file=sys.stderr)
return ERROR
premises = args.premises or []
if not premises:
print("verify decide: --premises is required (a decision with no premises has "
"no ground). Reference the fact-ids / assume-ids the choice rested on.",
file=sys.stderr)
return ERROR
events = read_events(repo_root)
# A premise must already be on file — you cannot ground a decision on an entry
# that does not exist. This also structurally forecloses self/forward cycles
# (append-only + premises-must-exist), backstopped by the verify-time cycle guard.
missing = [p for p in premises if latest_for(events, p) is None]
if missing:
print(f"verify decide: premise(s) not on file: {', '.join(missing)}. Register "
f"or assume them first (a decision grounds on EXISTING entries).",
file=sys.stderr)
return ERROR
if args.decision_id in premises:
print(f"verify decide: a decision cannot list itself as a premise "
f"({args.decision_id}). A decision cannot ground itself.", file=sys.stderr)
return ERROR
now = datetime.now(timezone.utc)
ev = {
"kind": "decided",
"fact_id": args.decision_id, # one keyspace: a decision-id IS a fact-id
"claim": args.claim,
"options": options,
"chose": args.chose,
"premises": premises,
"provenance_class": "internal",
"established_at": now.isoformat(timespec="seconds"),
"date": now.strftime("%d.%H%M"),
}
append_event(repo_root, ev)
kinds = {p: latest_for(events, p).get("kind") for p in premises}
print(f"DECIDED {args.decision_id} — '{args.claim}' chose {args.chose} "
f"(of {', '.join(options)}), grounded on {len(premises)} premise(s):")
for p in premises:
print(f" {p} [{kinds[p]}]")
print(f" `verify --fact-id {args.decision_id}` folds these premises' grounding-"
f"states. RAZOR: decision-fresh != decision-still-right — it checks premise-"
f"stability, it never re-runs the choice.")
return 0
def cmd_retire(args, repo_root):
events = read_events(repo_root)
if latest_for(events, args.fact_id) is None:
print(f"verify retire: {args.fact_id} is not registered.", file=sys.stderr)
return ERROR
now = datetime.now(timezone.utc)
ev = {
"kind": "retired",
"fact_id": args.fact_id,
"reason": args.reason,
"date": now.strftime("%d.%H%M"),
"established_at": now.isoformat(timespec="seconds"),
}
append_event(repo_root, ev)
print(f"RETIRED {args.fact_id} — called dead ({args.reason}). "
f"verify now returns DEAD; the corpse is not re-checked.")
return 0
def cmd_list(args, repo_root):
registry = fold(read_events(repo_root))
sys.stdout.write(render_registry(registry))
return 0
def cmd_fold(args, repo_root):
events = read_events(repo_root)
once = render_registry(fold(events))
twice = render_registry(fold(events))
if once != twice:
print("FOLD CHECK FAILED — projection is not fold-twice-identical.", file=sys.stderr)
return STALE # exit 3, the projection-invariant breach code (Lode contract)
print(f"FOLD OK — {len(fold(events))} fact(s), fold-twice-identical.")
return 0
def build_parser():
p = argparse.ArgumentParser(prog="verify", description="The Verification System — cheap certificate re-check of a learned fact.")
sub = p.add_subparsers(dest="cmd", required=True)
r = sub.add_parser("register", help="register a fact's certificate (after an expensive, re-encounterable derivation)")
r.add_argument("--fact-id", required=True)
r.add_argument("--claim", required=True)
r.add_argument("--edge", default="", help="the derivation provenance, e.g. 'X -> Y'")
r.add_argument("--inputs", nargs="+", required=True, help="the byte-truth input paths the derivation consumed")
r.add_argument("--provenance", choices=["internal", "external"], default="internal")
a = sub.add_parser("assume", help="register an ungrounded claim (a deferred check); takes NO --inputs by design")
a.add_argument("--fact-id", required=True)
a.add_argument("--claim", required=True)
a.add_argument("--path", required=True, help="the verification path — how to discharge this to a fact")
a.add_argument("--expiry", required=True, help="the defeater — the condition under which this stops holding")
a.add_argument("--evidence", default="", help="the weak signal being leaned on (optional)")
v = sub.add_parser("verify", help="cheap re-check: fresh / stale / dead (or SURFACE an assumption)")
v.add_argument("--fact-id", required=True)
v.add_argument("--json", action="store_true", help="machine-readable verdict on stdout (pipeline source)")
d = sub.add_parser("discharge", help="run an assumption's path, pin its ground -> promote to a fact")
d.add_argument("--fact-id", required=True)
d.add_argument("--inputs", nargs="+", required=True, help="the byte-truth inputs the now-run derivation stood on")
d.add_argument("--edge", default="", help="the derivation provenance (defaults to the assumption's path)")
dc = sub.add_parser("decide", help="record a decision 'A beats B' + the premises it rested on (refs to existing entries)")
dc.add_argument("--decision-id", required=True, help="the decision's id (shares the fact-id keyspace)")
dc.add_argument("--claim", required=True, help="the choice, e.g. 'A beats B'")
dc.add_argument("--options", required=True, help="the options considered, ';'- or ','-separated, e.g. 'A;B;C'")
dc.add_argument("--chose", required=True, help="the option chosen (must be one of --options)")
dc.add_argument("--premises", nargs="+", required=True, help="the fact-ids / assume-ids the choice rested on")
t = sub.add_parser("retire", help="call the fact dead (the derivation is retired)")
t.add_argument("--fact-id", required=True)
t.add_argument("--reason", required=True)
sub.add_parser("list", help="the derived registry (pure fold, latest-wins)")
f = sub.add_parser("fold", help="fold-twice-identical invariant check")
f.add_argument("--check", action="store_true")
return p
def main(argv=None):
args = build_parser().parse_args(argv)
# THE HONEST CEILING — printed to stderr on EVERY run so the tool states its own
# limit out loud (and a --json stdout pipe stays clean). `fresh` is derivability,
# not truth: it proves the byte-truth ground is unchanged, never that the claim was
# re-judged true. |- != |=.
print("CEILING: verify reports certificate-FRESHNESS, never TRUTH. `fresh` means the "
"derivation's byte-truth inputs are unchanged since the certificate was kept, "
"NOT that the claim is true in the world. |- != |=.", file=sys.stderr)
repo_root = os.environ.get("VERIFY_REPO_ROOT", REPO_ROOT)
try:
return {
"register": cmd_register,
"assume": cmd_assume,
"decide": cmd_decide,
"verify": cmd_verify,
"discharge": cmd_discharge,
"retire": cmd_retire,
"list": cmd_list,
"fold": cmd_fold,
}[args.cmd](args, repo_root)
except ValueError as exc:
print(f"verify: {exc}", file=sys.stderr)
return ERROR
if __name__ == "__main__":
sys.exit(main())
allow.json134 lineson GitHub →
{
"sha256:758260898c5608b08ef0175ad818a15b163a8b4140e5096f8e6a791ebfc88a5a": [
"boolop Or->And @L307",
"boolop Or->And @L534",
"boolop Or->And @L583",
"compare Eq->NotEq @L224",
"compare Eq->NotEq @L262",
"compare Eq->NotEq @L277",
"compare Eq->NotEq @L472",
"const bool False->True @L437",
"const bool True->False @L227",
"const bool True->False @L410",
"const bool True->False @L414",
"const bool True->False @L419",
"const bool True->False @L426",
"const bool True->False @L431",
"const bool True->False @L697",
"const bool True->False @L700",
"const bool True->False @L701",
"const bool True->False @L703",
"const bool True->False @L707",
"const bool True->False @L708",
"const bool True->False @L709",
"const bool True->False @L710",
"const bool True->False @L714",
"const bool True->False @L718",
"const bool True->False @L719",
"const bool True->False @L723",
"const bool True->False @L724",
"const bool True->False @L725",
"const bool True->False @L726",
"const bool True->False @L727",
"const bool True->False @L730",
"const bool True->False @L731",
"const int 0->1 @L225",
"const int 0->1 @L238",
"const int 0->1 @L326",
"const int 0->1 @L545",
"const int 1->0 @L207",
"const int 1->0 @L225",
"const int 1->2 @L207",
"const int 1->2 @L225",
"drop Assign @L208",
"drop Assign @L225",
"drop Continue @L210",
"drop Continue @L244",
"drop Expr @L267",
"drop Expr @L269",
"drop Expr @L273",
"drop Expr @L274",
"drop Expr @L276",
"drop Expr @L283",
"drop Expr @L292",
"drop Expr @L299",
"drop Expr @L315",
"drop Expr @L317",
"drop Expr @L318",
"drop Expr @L326",
"drop Expr @L409",
"drop Expr @L410",
"drop Expr @L453",
"drop Expr @L454",
"drop Expr @L456",
"drop Expr @L459",
"drop Expr @L460",
"drop Expr @L462",
"drop Expr @L499",
"drop Expr @L516",
"drop Expr @L519",
"drop Expr @L540",
"drop Expr @L541",
"drop Expr @L542",
"drop Expr @L543",
"drop Expr @L556",
"drop Expr @L561",
"drop Expr @L567",
"drop Expr @L575",
"drop Expr @L577",
"drop Expr @L591",
"drop Expr @L594",
"drop Expr @L607",
"drop Expr @L611",
"drop Expr @L617",
"drop Expr @L627",
"drop Expr @L632",
"drop Expr @L649",
"drop Expr @L652",
"drop Expr @L653",
"drop Expr @L662",
"drop Expr @L673",
"drop Expr @L689",
"drop Expr @L691",
"drop Expr @L763",
"drop For @L572",
"drop For @L651",
"drop If @L209",
"drop If @L243",
"drop If @L268",
"drop If @L275",
"drop If @L291",
"drop If @L298",
"drop If @L362",
"drop If @L384",
"drop If @L408",
"drop If @L458",
"drop If @L518",
"drop If @L566",
"drop If @L574",
"drop If @L616",
"drop If @L631",
"drop If @L661",
"drop If @L688",
"drop Return @L294",
"drop Return @L300",
"drop Return @L319",
"drop Return @L363",
"drop Return @L387",
"drop Return @L395",
"drop Return @L410",
"drop Return @L520",
"drop Return @L545",
"drop Return @L570",
"drop Return @L576",
"drop Return @L596",
"drop Return @L620",
"drop Return @L634",
"drop Return @L656",
"drop Return @L663",
"drop Return @L675",
"drop Return @L681",
"drop Return @L690",
"drop Return @L692"
]
}
smoke_test.py629 lineson GitHub →
#!/usr/bin/env python3
# SPDX-License-Identifier: MIT
"""smoke_test.py — hermetic proof that verify.py holds the line. No network, no
state outside a tmpdir (VERIFY_REPO_ROOT points the fact store at it). Each
scenario runs verify.py as a subprocess and checks the exit code AND the verdict
text — the real CLI contract, mirroring the freshness claims:
1 a registered fact whose inputs are UNCHANGED re-checks FRESH (exit 0) <- the headline
2 an input that MOVED (bytes changed) makes the fact STALE (exit 3)
3 a required input MISSING from disk makes the fact DEAD (exit 5)
4 an unregistered id is UNREGISTERED — a cache miss, not a false FRESH (exit 4)
5 an assumption is SURFACED as ASSUMED, never faked FRESH (exit 6)
6 discharge runs an assumption's path and PROMOTES it to a fact -> FRESH
7 a retired fact is DEAD (exit 5) — do not re-check a corpse
8 --json emits a clean machine verdict on stdout, exit code matches the human path
9 the CEILING line is emitted on stderr on EVERY run (honest limits, out loud)
10 fold --check is fold-twice-identical (exit 0) — the registry is a pure fold
The suite exercises the verdict branches (compare / hash / kind dispatch) so a
mutation of the core logic flips a verdict and the suite catches it — that is
what gives it teeth under the gauntlet's Layer-5 mutation harness.
Run: python3 smoke_test.py (expect: 10/10 passed, exit 0)
Contract: exit 0 iff every scenario passes; non-zero on any fail (so the mutation
harness reads a killed mutant as non-zero).
"""
import json
import os
import subprocess
import sys
import tempfile
HERE = os.path.dirname(os.path.abspath(__file__))
VERIFY = os.path.join(HERE, "verify.py")
# Exit-code contract (mirrors verify.py; the suite asserts against these by value,
# staying hermetic — it never imports the tool it mutates under the harness).
FRESH, STALE, DEAD, UNREGISTERED, ERROR, ASSUMED = 0, 3, 5, 4, 2, 6
PASS = 0
FAIL = 0
def ok(msg):
global PASS
PASS += 1
print(f"ok {msg}")
def bad(msg, why):
global FAIL
FAIL += 1
print(f"FAIL {msg}: {why}")
def run(root, *argv):
"""Run verify.py with the fact store rooted at `root`; return (rc, out, err)."""
env = dict(os.environ, VERIFY_REPO_ROOT=root)
p = subprocess.run([sys.executable, VERIFY, *argv],
stdout=subprocess.PIPE, stderr=subprocess.PIPE,
text=True, env=env, cwd=root)
return p.returncode, p.stdout, p.stderr
def write(root, name, text):
with open(os.path.join(root, name), "w", encoding="utf-8") as f:
f.write(text)
def t1(d):
write(d, "in.txt", "v1")
run(d, "register", "--fact-id", "f1", "--claim", "X->Y", "--inputs", "in.txt")
rc, out, _ = run(d, "verify", "--fact-id", "f1")
if rc == 0 and "FRESH" in out:
ok("unchanged inputs re-check FRESH (exit 0)")
else:
bad("fresh", f"rc={rc} out=[{out.strip()}]")
def t2(d):
write(d, "in.txt", "v1")
run(d, "register", "--fact-id", "f2", "--claim", "c", "--inputs", "in.txt")
write(d, "in.txt", "v2-changed")
rc, out, _ = run(d, "verify", "--fact-id", "f2")
if rc == 3 and "STALE" in out:
ok("a moved input makes the fact STALE (exit 3)")
else:
bad("stale", f"expected rc=3 STALE, got rc={rc} out=[{out.strip()}]")
def t3(d):
write(d, "in.txt", "v1")
run(d, "register", "--fact-id", "f3", "--claim", "c", "--inputs", "in.txt")
os.remove(os.path.join(d, "in.txt"))
rc, out, _ = run(d, "verify", "--fact-id", "f3")
if rc == 5 and "DEAD" in out:
ok("a missing input makes the fact DEAD (exit 5)")
else:
bad("dead", f"expected rc=5 DEAD, got rc={rc} out=[{out.strip()}]")
def t4(d):
rc, out, _ = run(d, "verify", "--fact-id", "ghost")
if rc == 4 and "UNREGISTERED" in out:
ok("an unknown id is UNREGISTERED, never a false FRESH (exit 4)")
else:
bad("unregistered", f"expected rc=4, got rc={rc} out=[{out.strip()}]")
def t5(d):
run(d, "assume", "--fact-id", "a1", "--claim", "price current",
"--path", "re-fetch source", "--expiry", "2026-12-01")
rc, out, _ = run(d, "verify", "--fact-id", "a1")
if rc == 6 and "ASSUMED" in out:
ok("an assumption is SURFACED as ASSUMED, never faked FRESH (exit 6)")
else:
bad("assumed", f"expected rc=6 ASSUMED, got rc={rc} out=[{out.strip()}]")
def t6(d):
run(d, "assume", "--fact-id", "a2", "--claim", "c",
"--path", "run the derivation", "--expiry", "when src.txt changes")
write(d, "src.txt", "derived")
rc, _, _ = run(d, "discharge", "--fact-id", "a2", "--inputs", "src.txt")
if rc != 0:
bad("discharge", f"discharge rc={rc}")
return
rc2, out2, _ = run(d, "verify", "--fact-id", "a2")
if rc2 == 0 and "FRESH" in out2:
ok("discharge promotes an assumption to a FRESH fact")
else:
bad("discharge-promote", f"rc={rc2} out=[{out2.strip()}]")
def t7(d):
write(d, "in.txt", "v1")
run(d, "register", "--fact-id", "f7", "--claim", "c", "--inputs", "in.txt")
run(d, "retire", "--fact-id", "f7", "--reason", "derivation retired")
rc, out, _ = run(d, "verify", "--fact-id", "f7")
if rc == 5 and "DEAD" in out:
ok("a retired fact is DEAD, not re-checkable (exit 5)")
else:
bad("retire", f"expected rc=5 DEAD, got rc={rc} out=[{out.strip()}]")
def t8(d):
write(d, "in.txt", "v1")
run(d, "register", "--fact-id", "f8", "--claim", "c", "--inputs", "in.txt")
rc, out, err = run(d, "verify", "--fact-id", "f8", "--json")
try:
rec = json.loads(out)
except Exception as exc:
bad("json", f"stdout not clean JSON: {exc}; out=[{out.strip()}]")
return
if rc == 0 and rec.get("verdict") == "fresh" and rec.get("code") == 0:
ok("--json emits a clean machine verdict, exit code matches human path")
else:
bad("json-verdict", f"rc={rc} json={rec}")
def t9(d):
rc, out, err = run(d, "list")
if "CEILING:" in err and "|- != |=" in err:
ok("the CEILING line is emitted on stderr on every run")
else:
bad("ceiling", f"no CEILING on stderr; err=[{err.strip()}]")
def t10(d):
write(d, "in.txt", "v1")
run(d, "register", "--fact-id", "f10", "--claim", "c", "--inputs", "in.txt")
rc, out, _ = run(d, "fold", "--check")
if rc == 0:
ok("fold --check is fold-twice-identical (exit 0)")
else:
bad("fold", f"expected rc=0, got rc={rc} out=[{out.strip()}]")
# ── Hardening block (slot 04, gate 5): drive the paths the 10 headline cases
# leave un-exercised, so ast-level mutations of the core verdict logic flip an
# observable verdict and the suite catches them. The decision engine
# (decide / decision_verdict / premise_state), the --json path per record kind,
# the fold's latest-wins ordering, and the render/guard branches were the mutant
# survivors; each case below kills a cluster of them. verify.py is UNCHANGED —
# all teeth are added here (the 0fb3c694 content-hash pin holds). ──
def _reg(d, fid, val="v1", claim="c", name="in.txt"):
"""Register a fresh fact grounded on a written input file."""
write(d, name, val)
run(d, "register", "--fact-id", fid, "--claim", claim, "--inputs", name)
def _one_verdict(out):
"""The output must carry EXACTLY ONE verdict headline — a dropped `return` in a
verdict branch prints its word then falls through and prints a SECOND word, same
exit code. Counting verdict words catches that contradiction the exit code hides."""
words = ("FRESH", "STALE", "DEAD", "ASSUMED", "UNREGISTERED", "CYCLE")
return sum(out.count(w) for w in words) == 1
def t11_decide_fresh(d):
# A decision over two FRESH fact-premises folds to FRESH (exit 0), and names
# every premise. Kills: decision_verdict FRESH-fallthrough, the premise loop,
# cmd_verify decided-branch FRESH print, premise_state fact dispatch.
_reg(d, "p1", name="a.txt"); _reg(d, "p2", name="b.txt")
rc, out, _ = run(d, "decide", "--decision-id", "d1", "--claim", "A beats B",
"--options", "A,B", "--chose", "A", "--premises", "p1", "p2")
if rc != 0:
bad("decide-record", f"decide rc={rc} out=[{out.strip()}]"); return
rc, out, _ = run(d, "verify", "--fact-id", "d1")
if rc == 0 and "FRESH" in out and "p1" in out and "p2" in out and _one_verdict(out):
ok("a decision over fresh premises folds FRESH, naming every premise")
else:
bad("decide-fresh", f"rc={rc} out=[{out.strip()}]")
def t12_decide_stale_precedence(d):
# One premise MOVES -> the decision folds STALE (exit 3). Kills: the STALE
# precedence branch in decision_verdict, premise_state->fact_verdict STALE,
# the cmd_verify STALE-class naming (the `stale = [...]` comprehension).
_reg(d, "p1", name="a.txt"); _reg(d, "p2", val="orig", name="b.txt")
run(d, "decide", "--decision-id", "d2", "--claim", "c", "--options", "A;B",
"--chose", "A", "--premises", "p1", "p2")
write(d, "b.txt", "MOVED") # p2's ground moves
rc, out, _ = run(d, "verify", "--fact-id", "d2")
if rc == 3 and "STALE" in out and "p2" in out:
ok("a moved premise makes the decision STALE, naming the moved premise")
else:
bad("decide-stale", f"expected rc=3 STALE naming p2, got rc={rc} out=[{out.strip()}]")
def t13_decide_dead_beats_stale(d):
# DEAD outranks STALE: p2 moved (stale) AND p3 removed (dead) -> DEAD (exit 5).
# Kills: the DEAD-first precedence ordering in decision_verdict (drop/reorder
# of the `for worst in (DEAD, STALE, ASSUMED)` loop flips the verdict here).
_reg(d, "p1", name="a.txt"); _reg(d, "p2", val="o", name="b.txt")
_reg(d, "p3", name="c.txt")
run(d, "decide", "--decision-id", "d3", "--claim", "c", "--options", "A,B",
"--chose", "A", "--premises", "p1", "p2", "p3")
write(d, "b.txt", "MOVED") # p2 -> STALE
os.remove(os.path.join(d, "c.txt")) # p3 -> DEAD
rc, out, _ = run(d, "verify", "--fact-id", "d3")
if rc == 5 and "DEAD" in out and "p3" in out:
ok("DEAD outranks STALE in the decision fold (precedence order has teeth)")
else:
bad("decide-precedence", f"expected rc=5 DEAD, got rc={rc} out=[{out.strip()}]")
def t14_decide_assumed_premise(d):
# A decision resting on a LIVE assumption folds ASSUMED (exit 6). Kills:
# premise_state assumed-dispatch, the ASSUMED precedence branch, the assumed
# class-naming in cmd_verify.
_reg(d, "p1", name="a.txt")
run(d, "assume", "--fact-id", "asmp", "--claim", "leaned on",
"--path", "re-fetch", "--expiry", "2027-01-01")
run(d, "decide", "--decision-id", "d4", "--claim", "c", "--options", "A,B",
"--chose", "A", "--premises", "p1", "asmp")
rc, out, _ = run(d, "verify", "--fact-id", "d4")
if rc == 6 and "ASSUMED" in out and "asmp" in out:
ok("a decision on a live assumption folds ASSUMED, naming the assumption")
else:
bad("decide-assumed", f"expected rc=6 ASSUMED, got rc={rc} out=[{out.strip()}]")
def t15_decide_dead_on_retired_premise(d):
# A retired premise makes the decision DEAD (premise_state retired->DEAD).
_reg(d, "p1", name="a.txt")
run(d, "decide", "--decision-id", "d5", "--claim", "c", "--options", "A,B",
"--chose", "A", "--premises", "p1")
run(d, "retire", "--fact-id", "p1", "--reason", "premise retired")
rc, out, _ = run(d, "verify", "--fact-id", "d5")
if rc == 5 and "DEAD" in out:
ok("a retired premise makes the decision DEAD")
else:
bad("decide-retired-premise", f"expected rc=5 DEAD, got rc={rc} out=[{out.strip()}]")
def t16_decide_guards(d):
# Every cmd_decide validation guard returns ERROR (exit 2). Kills the guard
# cascade (len<2, chose-not-in-options, no-premises, missing-premise,
# self-premise) — each is a `drop If`/`compare` survivor otherwise.
_reg(d, "p1", name="a.txt")
checks = [
(["decide", "--decision-id", "g1", "--claim", "c", "--options", "A",
"--chose", "A", "--premises", "p1"], "one option"),
(["decide", "--decision-id", "g2", "--claim", "c", "--options", "A,B",
"--chose", "Z", "--premises", "p1"], "chose not in options"),
(["decide", "--decision-id", "g3", "--claim", "c", "--options", "A,B",
"--chose", "A"], "no premises"),
(["decide", "--decision-id", "g4", "--claim", "c", "--options", "A,B",
"--chose", "A", "--premises", "ghost"], "missing premise"),
(["decide", "--decision-id", "g5", "--claim", "c", "--options", "A,B",
"--chose", "A", "--premises", "g5"], "self premise"),
]
for argv, why in checks:
rc, _, _ = run(d, *argv)
if rc != ERROR:
bad("decide-guard", f"{why}: expected ERROR(2), got rc={rc}"); return
ok("every decide guard rejects with ERROR (option/chose/premise cascade)")
def t17_decide_cycle(d):
# A hand-edited self-referential decision certificate verifies as CYCLE
# (exit 2). decide REFUSES to author one, so we craft the event directly on
# the log to reach the verify-time cycle guard (premise_state `pid in seen`).
_reg(d, "p1", name="a.txt")
run(d, "decide", "--decision-id", "cyc", "--claim", "c", "--options", "A,B",
"--chose", "A", "--premises", "p1")
# append a decided event for `cyc` that lists itself as a premise (later seq wins)
ev = {"kind": "decided", "fact_id": "cyc", "claim": "c", "options": ["A", "B"],
"chose": "A", "premises": ["cyc"], "provenance_class": "internal",
"date": "31.2359", "seq": 99}
path = os.path.join(d, ".verify", "verified.jsonl")
with open(path, "a", encoding="utf-8") as fh:
fh.write(json.dumps(ev, sort_keys=True) + "\n")
rc, out, _ = run(d, "verify", "--fact-id", "cyc")
if rc == ERROR and "CYCLE" in out and _one_verdict(out):
ok("a self-referential decision certificate verifies as CYCLE (exit 2)")
else:
bad("decide-cycle", f"expected rc={ERROR} single-CYCLE, got rc={rc} out=[{out.strip()}]")
def t18_json_decided(d):
# --json on a decided record emits the folded verdict + a per-premise state
# breakdown, code matching the human path. Kills the _verify_json decided arm.
_reg(d, "p1", name="a.txt"); _reg(d, "p2", val="o", name="b.txt")
run(d, "decide", "--decision-id", "dj", "--claim", "c", "--options", "A,B",
"--chose", "A", "--premises", "p1", "p2")
write(d, "b.txt", "MOVED")
rc, out, _ = run(d, "verify", "--fact-id", "dj", "--json")
try:
rec = json.loads(out)
except Exception as exc:
bad("json-decided", f"stdout not JSON: {exc}"); return
prem = {p["id"]: p["state"] for p in rec.get("premises", [])}
if (rc == 3 and rec.get("verdict") == "stale" and rec.get("code") == 3
and prem.get("p2") == "stale" and prem.get("p1") == "fresh"):
ok("--json on a decision emits the fold + per-premise breakdown")
else:
bad("json-decided", f"rc={rc} json={rec}")
def t19_json_assumed_and_dead(d):
# --json arms for assumed and retired records (each its own _verify_json branch).
run(d, "assume", "--fact-id", "aj", "--claim", "cl", "--path", "p", "--expiry", "e")
rc, out, _ = run(d, "verify", "--fact-id", "aj", "--json")
rec = json.loads(out)
if not (rc == 6 and rec.get("verdict") == "assumed" and rec.get("claim") == "cl"):
bad("json-assumed", f"rc={rc} json={rec}"); return
_reg(d, "rj", name="r.txt")
run(d, "retire", "--fact-id", "rj", "--reason", "gone")
rc2, out2, _ = run(d, "verify", "--fact-id", "rj", "--json")
rec2 = json.loads(out2)
if rc2 == 5 and rec2.get("verdict") == "dead" and rec2.get("reason") == "gone":
ok("--json arms for assumed (with claim) and retired (with reason)")
else:
bad("json-dead", f"rc={rc2} json={rec2}")
def t20_fold_latest_wins(d):
# Re-registering a fact and then retiring it: the fold's latest-wins ordering
# must make the LATEST event authoritative (register->register->retire => DEAD).
# Kills fold ordering/dedup survivors and append_event's seq increment.
_reg(d, "ff", val="one", name="x.txt")
_reg(d, "ff", val="two", name="x.txt") # second register, same id
rc, out, _ = run(d, "verify", "--fact-id", "ff")
if not (rc == 0 and "FRESH" in out):
bad("fold-latest", f"after re-register expected FRESH, got rc={rc}"); return
run(d, "retire", "--fact-id", "ff", "--reason", "done")
rc2, out2, _ = run(d, "verify", "--fact-id", "ff")
if rc2 == 5 and "DEAD" in out2:
ok("fold latest-wins: register->register->retire resolves to DEAD")
else:
bad("fold-latest", f"after retire expected DEAD, got rc={rc2} out=[{out2.strip()}]")
def t21_list_render_kinds(d):
# `list` renders each record KIND with its distinguishing line. Kills the
# render_registry kind-dispatch branches (retired/assumed/decided/fact).
_reg(d, "rf", name="a.txt")
run(d, "assume", "--fact-id", "ra", "--claim", "cl", "--path", "p", "--expiry", "ex")
_reg(d, "rp", name="b.txt")
run(d, "decide", "--decision-id", "rd", "--claim", "dc", "--options", "A,B",
"--chose", "A", "--premises", "rp")
run(d, "retire", "--fact-id", "rf", "--reason", "gonzo")
rc, out, _ = run(d, "list")
need = ["RETIRED (dead)", "ASSUMED (ungrounded)", "DECIDED (premise-grounded)",
"gonzo", "chose:", "premises:"]
missing = [n for n in need if n not in out]
if rc == 0 and not missing:
ok("list renders every record kind with its distinguishing detail")
else:
bad("list-render", f"rc={rc} missing={missing}")
def t22_discharge_guards(d):
# discharge's error branches: not-on-file, not-an-assumption, no-inputs.
rc, _, _ = run(d, "discharge", "--fact-id", "nope", "--inputs", "x")
if rc != ERROR:
bad("discharge-missing", f"expected ERROR, got {rc}"); return
_reg(d, "realfact", name="a.txt")
rc2, _, _ = run(d, "discharge", "--fact-id", "realfact", "--inputs", "a.txt")
if rc2 != ERROR: # a fact is not an open assumption
bad("discharge-notassumed", f"expected ERROR, got {rc2}"); return
run(d, "assume", "--fact-id", "op", "--claim", "c", "--path", "p", "--expiry", "e")
rc3, _, _ = run(d, "discharge", "--fact-id", "op") # no --inputs
if rc3 == ERROR:
ok("discharge rejects: not-on-file, not-an-assumption, and no-inputs")
else:
bad("discharge-noinputs", f"expected ERROR, got {rc3}")
def t23_fold_check_json_parity(d):
# The --json exit code equals the human path across a fact's whole lifecycle,
# and fold --check stays green with a mixed registry. Guards _verify_json's
# fact arm (moved/missing fields) + the code==human invariant.
_reg(d, "lc", val="v1", name="a.txt")
rc_h, _, _ = run(d, "verify", "--fact-id", "lc")
rc_j, out_j, _ = run(d, "verify", "--fact-id", "lc", "--json")
if rc_h != rc_j or json.loads(out_j).get("code") != rc_h:
bad("json-parity", f"human={rc_h} json={rc_j}"); return
write(d, "a.txt", "moved")
rc_h2, _, _ = run(d, "verify", "--fact-id", "lc")
rc_j2, out_j2, _ = run(d, "verify", "--fact-id", "lc", "--json")
moved = json.loads(out_j2).get("moved", [])
if rc_h2 == rc_j2 == 3 and "a.txt" in moved:
ok("--json code tracks the human path and reports the moved input")
else:
bad("json-parity", f"h={rc_h2} j={rc_j2} moved={moved}")
def t24_nested_decision(d):
# premise_state's decided-branch: a decision grounded on ANOTHER decision.
# The inner decision folds first, its state propagates outward. Kills the
# premise_state `kind == "decided"` recursion (L369-370).
_reg(d, "leaf", val="o", name="a.txt")
run(d, "decide", "--decision-id", "inner", "--claim", "c", "--options", "A,B",
"--chose", "A", "--premises", "leaf")
run(d, "decide", "--decision-id", "outer", "--claim", "c", "--options", "A,B",
"--chose", "A", "--premises", "inner")
# fresh chain -> outer FRESH
rc, out, _ = run(d, "verify", "--fact-id", "outer")
if not (rc == 0 and "FRESH" in out):
bad("nested-fresh", f"expected FRESH, got rc={rc} out=[{out.strip()}]"); return
# move the leaf -> inner STALE -> outer must fold STALE through the nesting
write(d, "a.txt", "MOVED")
rc2, out2, _ = run(d, "verify", "--fact-id", "outer")
if rc2 == 3 and "STALE" in out2:
ok("a decision grounded on a decision folds the inner state outward")
else:
bad("nested-stale", f"expected STALE through nesting, got rc={rc2} out=[{out2.strip()}]")
def t25_bad_jsonl_raises(d):
# read_events must RAISE on a malformed log line (not silently skip / return
# a partial set). Kills read_events' try/except/raise (L208-214). The tool
# surfaces the parse failure as a non-zero exit, never a false FRESH.
_reg(d, "ok1", name="a.txt")
path = os.path.join(d, ".verify", "verified.jsonl")
with open(path, "a", encoding="utf-8") as fh:
fh.write("{ this is not valid json\n")
rc, out, err = run(d, "verify", "--fact-id", "ok1")
# a corrupt log is a hard error (exit 2), never a silent FRESH(0)
if rc != 0 and "FRESH" not in out:
ok("a malformed log line is surfaced as an error, never a false FRESH")
else:
bad("bad-jsonl", f"corrupt log gave rc={rc} out=[{out.strip()}]")
def t26_seq_ordering_manyevents(d):
# append_event's per-day seq increment orders same-day events for the fold.
# Register the same id THREE times in one run (same date) with different
# inputs; latest-wins must resolve to the LAST write's ground. If the seq
# increment is broken (const/drop mutant), a same-day tie could resolve to
# the wrong event and flip the verdict. Distinguishes the seq logic behaviorally.
write(d, "one.txt", "1"); run(d, "register", "--fact-id", "s", "--claim", "c", "--inputs", "one.txt")
write(d, "two.txt", "2"); run(d, "register", "--fact-id", "s", "--claim", "c", "--inputs", "two.txt")
write(d, "three.txt", "3"); run(d, "register", "--fact-id", "s", "--claim", "c", "--inputs", "three.txt")
# the live ground is three.txt; moving it must make s STALE, moving the others must NOT
write(d, "one.txt", "X"); write(d, "two.txt", "X")
rc, out, _ = run(d, "verify", "--fact-id", "s")
if not (rc == 0 and "FRESH" in out):
bad("seq-latest", f"latest event should be FRESH (moved only stale inputs), got rc={rc}"); return
write(d, "three.txt", "MOVED")
rc2, out2, _ = run(d, "verify", "--fact-id", "s")
if rc2 == 3 and "STALE" in out2:
ok("same-day seq ordering resolves latest-wins to the last write")
else:
bad("seq-latest", f"moving the latest input should be STALE, got rc={rc2} out=[{out2.strip()}]")
def _raw_append(d, ev):
# Craft an event directly onto the log, bypassing the CLI's seq-ordered
# writer, so file-order and (date,seq)-order can be made to DISAGREE. This
# is the only way to distinguish latest_for's sort from a file-order read
# (the CLI always writes in seq-order, so t26 cannot — see gate-5 triage).
path = os.path.join(d, ".verify", "verified.jsonl")
os.makedirs(os.path.dirname(path), exist_ok=True)
with open(path, "a", encoding="utf-8") as fh:
fh.write(json.dumps(ev, sort_keys=True) + "\n")
def t27_latest_for_sort_kills_fileorder(d):
# GATE-5 real gap: latest_for sorts recs by (date, seq) then takes [-1].
# Drop the .sort() and recs[-1] returns the file-order-last event instead of
# the true latest. Craft a log where the TRUE latest (higher seq) is written
# FIRST and an OLDER event (lower seq) is written LAST, with DIFFERENT kinds
# so the verdict's EXIT CODE distinguishes them. True-latest is `retired`
# (-> DEAD, exit 2); file-order-last is `verified` (-> would verify FRESH/STALE).
# true latest: retired, seq 5, written FIRST. (retired -> DEAD returns before
# any input-hash check, so the older event's inputs are irrelevant.)
_raw_append(d, {"kind": "retired", "fact_id": "x", "claim": "c",
"reason": "superseded", "date": "01.0000", "seq": 5})
# older: verified, seq 1, written LAST (file-order-last). No real inputs needed:
# if sort is intact this record is never reached; if sort is dropped, recs[-1]
# picks THIS (wrong) record and the verdict is no longer DEAD -> the mutant dies.
_raw_append(d, {"kind": "verified", "fact_id": "x", "claim": "c",
"inputs": {}, "established_at": "01.0000", "date": "01.0000", "seq": 1})
rc, out, _ = run(d, "verify", "--fact-id", "x")
# With sort: true latest (seq 5, retired) wins -> DEAD (exit 5).
if rc == 5 and "DEAD" in out and _one_verdict(out):
ok("latest_for resolves by (date,seq), not file order — true-latest retired -> DEAD")
else:
bad("latest-for-sort",
f"expected DEAD(2) from the higher-seq retired event, got rc={rc} out=[{out.strip()}]")
def t28_append_event_sameday_compare(d):
# GATE-5 real gap: append_event computes same_day by `e.get('date')==ev['date']`
# then seq = 1 + max(same-day seqs). Flip Eq->NotEq and the new event's seq is
# computed off the WRONG (other-day) events, so a real same-day sequence can
# collide/mis-order. Drive it through the CLI (which uses append_event) with two
# registers on the same date, then verify latest-wins still resolves correctly.
write(d, "a.txt", "1"); run(d, "register", "--fact-id", "y", "--claim", "c", "--inputs", "a.txt")
write(d, "b.txt", "2"); run(d, "register", "--fact-id", "y", "--claim", "c", "--inputs", "b.txt")
# latest (b.txt) is live; moving a.txt (older) must NOT make y stale
write(d, "a.txt", "MOVED")
rc, out, _ = run(d, "verify", "--fact-id", "y")
if not (rc == 0 and "FRESH" in out):
bad("append-sameday", f"older same-day input moved should stay FRESH, got rc={rc} out=[{out.strip()}]"); return
# moving the true latest (b.txt) MUST make it stale — proves seq ordered them right
write(d, "b.txt", "MOVED")
rc2, out2, _ = run(d, "verify", "--fact-id", "y")
if rc2 == 3 and "STALE" in out2:
ok("append_event same-day seq orders same-date events so latest-wins holds")
else:
bad("append-sameday", f"moving true-latest input should be STALE, got rc={rc2} out=[{out2.strip()}]")
def t29_fold_none_factid_guard(d):
# GATE-5 real gap: fold guards against a None fact_id. A raw log line missing
# fact_id must not crash `list` or mis-fold. Craft such a line, then run list.
write(d, "g.txt", "v1")
run(d, "register", "--fact-id", "real", "--claim", "c", "--inputs", "g.txt")
_raw_append(d, {"kind": "verified", "claim": "orphan-no-factid",
"date": "01.0001", "seq": 1}) # NO fact_id key
rc, out, err = run(d, "list")
# must not crash (exit 0/2 acceptable per contract), and the real fact must survive the fold
if rc in (0, 2) and "real" in out:
ok("fold survives a None/absent fact_id line without crashing or dropping real facts")
else:
bad("fold-none-factid", f"list should survive a factid-less line, got rc={rc} out=[{out.strip()}] err=[{err.strip()}]")
def t30_register_success_exit_zero(d):
# GATE-5 real gap: cmd_register ends `return 0` (success). Two mutants break it and
# BOTH pass the current suite because the headline REGISTERED still prints:
# (a) `const int 0->1 @L319` flips the success return to 1;
# (b) `drop Return @L228` drops append_event's `return ev`, so cmd_register does
# `ev = append_event(...)` -> ev is None -> the following ev['established_at']
# raises, and register exits non-zero.
# The success EXIT CODE is a hard consumer contract (0 = the certificate was written);
# a scripted caller that checks `verify register ... && ...` breaks silently on rc=1.
# Assert it directly.
write(d, "a.txt", "1")
rc, out, _ = run(d, "register", "--fact-id", "rz", "--claim", "c", "--inputs", "a.txt")
if rc == 0 and "REGISTERED" in out:
ok("register exits 0 on success (the write-succeeded contract, not just the headline)")
else:
bad("register-exit", f"register success must exit 0, got rc={rc} out=[{out.strip()[:80]}]")
def t31_retire_success_exit_zero(d):
# GATE-5 real gap: cmd_retire ends `return 0`. `const int 0->1 @L675` flips it to 1
# while still printing RETIRED, so the current suite (headline-only on retire) misses it.
# A retire that "succeeds" with rc=1 lies to `verify retire ... && verify verify ...`.
write(d, "a.txt", "1")
run(d, "register", "--fact-id", "rt", "--claim", "c", "--inputs", "a.txt")
rc, out, _ = run(d, "retire", "--fact-id", "rt", "--reason", "superseded")
if rc == 0 and "RETIRED" in out:
ok("retire exits 0 on success (the call-it-dead contract, not just the headline)")
else:
bad("retire-exit", f"retire success must exit 0, got rc={rc} out=[{out.strip()[:80]}]")
def t32_append_event_returns_written_record(d):
# GATE-5 real gap (the OTHER half of drop Return @L228): cmd_register reads fields off
# the RECORD append_event returns (ev['established_at'] for the "certificate kept @"
# line). If append_event returns None, that read fails. Assert the confirmation line
# that depends on the returned record is present AND register still exits 0 — this
# pins that append_event's return value is consumed, not just that it wrote a line.
write(d, "a.txt", "1")
rc, out, _ = run(d, "register", "--fact-id", "rr", "--claim", "c", "--inputs", "a.txt")
if rc == 0 and "certificate kept @" in out:
ok("register consumes append_event's returned record (certificate-kept confirmation prints)")
else:
bad("append-return", f"register must print the certificate-kept line from the returned record, got rc={rc} out=[{out.strip()[:80]}]")
HARDENING = (t11_decide_fresh, t12_decide_stale_precedence, t13_decide_dead_beats_stale,
t14_decide_assumed_premise, t15_decide_dead_on_retired_premise, t16_decide_guards,
t17_decide_cycle, t18_json_decided, t19_json_assumed_and_dead, t20_fold_latest_wins,
t21_list_render_kinds, t22_discharge_guards, t23_fold_check_json_parity,
t24_nested_decision, t25_bad_jsonl_raises, t26_seq_ordering_manyevents,
t27_latest_for_sort_kills_fileorder, t28_append_event_sameday_compare,
t29_fold_none_factid_guard, t30_register_success_exit_zero,
t31_retire_success_exit_zero, t32_append_event_returns_written_record)
def main():
for t in (t1, t2, t3, t4, t5, t6, t7, t8, t9, t10) + HARDENING:
with tempfile.TemporaryDirectory() as d:
t(d)
print()
print(f"{PASS}/{PASS + FAIL} passed")
return 0 if FAIL == 0 else 1
if __name__ == "__main__":
sys.exit(main())