Skip to the content.

Negative fixtures for the verification-ladder spec

These are the must-reject witnesses for ../../verification-ladder-spec.json (the declarable verification-ladder schema, #1210 / G2). The positive round-trip — the ladder ../verification-ladder.json plus the two decisions it produces, ../verification-ladder-decision-read.json (a low-risk read stops at rung 1) and ../verification-ladder-decision-write.json (a write climbs to rung 3) — shows the schema accepts a well-formed ladder and the decisions a walk over it yields. These five files make the acceptance criteria — “the verdict set is a closed, validatable vocabulary” and “the ladder is fail-closed by construction (an INDETERMINATE rung escalates, never silently allows)” — checkable rather than asserted. Each isolates exactly one defect so the rejection reason is unambiguous:

Fixture Validates against Defect Why the schema rejects it
ladder-fails-open.json Ladder (root) on_exhaustion: "allow" the fail-closed tail is pinned to const "deny" — a ladder cannot declare a fail-OPEN exhaustion; the recipe rule is structural
ladder-no-escalate.json Ladder (root) escalate_on omits indeterminate escalate_on MUST contains indeterminate — else an INDETERMINATE rung has nothing to trigger a climb and could be silently dropped
unknown-field.json Ladder (root) extra domain key the ladder is closed (additionalProperties: false) and domain-free; a host-specific knob cannot smuggle in
verdict-out-of-set.json $defs/Decision a path step’s verdict: "maybe" not in the closed Verdict set {allow, deny, indeterminate, defer} — out-of-set drift is refused at the boundary
indeterminate-final-verdict.json $defs/Decision final verdict: "indeterminate" the committed verdict is closed to {allow, deny} — an INDETERMINATE can never be the last word (a residual one folds to deny via on_exhaustion)

The round-trip, witnessed with no fak engine

Any off-the-shelf Draft 2020-12 validator runs this. The recipe below uses the jsonschema Python package (pip install jsonschema) — no fak engine, no network, no model. It does two things: (1) validates the four positive fixtures against their schema parts and rejects all five negatives, and (2) re-derives the smallest-sufficient rung from the declared ladder data and asserts each decision reached exactly that rung — so “a low-risk call stops at rung 1; a write climbs” is computed from the data, not just read off the fixture. Run it from the repo root; it exits non-zero if any expectation is unmet:

import json, sys
from jsonschema import Draft202012Validator

S = "docs/standards/verification-ladder-spec"
schema = json.load(open(f"{S}.json"))
F = "docs/standards/fixtures"

# The root validates a Ladder (the authored policy).
ladder_v = Draft202012Validator(schema)
# A Decision is an OUTPUT shape — validate decision fixtures against $defs/Decision.
decision_v = Draft202012Validator(
    {"$schema": schema["$schema"], "$defs": schema["$defs"], "$ref": "#/$defs/Decision"})

ok = True
def expect(name, valid, want_valid):
    global ok
    good = valid == want_valid
    ok = ok and good
    print(("PASS" if good else "FAIL"), name, "->", "accepted" if valid else "rejected")

def check(name, cond):
    global ok
    ok = ok and cond
    print(("PASS" if cond else "FAIL"), name)

# (1) schema validity: every positive validates, every negative is rejected
ladder   = json.load(open(f"{F}/verification-ladder.json"))
dec_read  = json.load(open(f"{F}/verification-ladder-decision-read.json"))
dec_write = json.load(open(f"{F}/verification-ladder-decision-write.json"))
expect("ladder (author)",          ladder_v.is_valid(ladder),     True)
expect("decision read (review)",   decision_v.is_valid(dec_read),  True)
expect("decision write (review)",  decision_v.is_valid(dec_write), True)
expect("ladder-fails-open",        ladder_v.is_valid(json.load(open(f"{F}/verification-ladder-invalid/ladder-fails-open.json"))),  False)
expect("ladder-no-escalate",       ladder_v.is_valid(json.load(open(f"{F}/verification-ladder-invalid/ladder-no-escalate.json"))), False)
expect("unknown-field",            ladder_v.is_valid(json.load(open(f"{F}/verification-ladder-invalid/unknown-field.json"))),       False)
expect("verdict-out-of-set",       decision_v.is_valid(json.load(open(f"{F}/verification-ladder-invalid/verdict-out-of-set.json"))),        False)
expect("indeterminate-final",      decision_v.is_valid(json.load(open(f"{F}/verification-ladder-invalid/indeterminate-final-verdict.json"))), False)

# (2) smallest-sufficient-rung selection, DERIVED from the declared ladder (AC#3).
# Risk is ordered; a rung "covers" a claim iff its max_risk is >= the claim's risk.
RISK = {"read": 0, "write": 1, "self_modify": 2}
covers = lambda max_risk, rc: RISK[max_risk] >= RISK[rc]
# The reuse/vDSO rung only decides a REPEATED call (a cache hit), so the smallest rung
# that can conclusively decide a NOVEL claim is the cheapest non-reuse rung that covers it.
conclusive = [r for r in ladder["rungs"] if r["cost"] != "reuse"]
first = min(r["id"] for r in conclusive)                                   # cheapest conclusive rung
select = lambda rc: min(r["id"] for r in conclusive if covers(r["max_risk"], rc))

# a low-risk READ stops at the cheapest conclusive rung; it never climbs
check("read selects rung 1",  select("read") == 1 == dec_read["rung_reached"])
check("read does not climb",   (select("read") != first) == dec_read["climbed"] == False)
# a WRITE cannot be allowed by a read-only rung -> it climbs to the require-witness rung
check("write selects rung 3", select("write") == 3 == dec_write["rung_reached"])
check("write climbs",          (select("write") != first) == dec_write["climbed"] == True)
check("riskier claim reaches a costlier rung",
      dec_write["rung_reached"] > dec_read["rung_reached"])

sys.exit(0 if ok else 1)

Expected output — the four positives accepted, all five negatives rejected, and the smallest-sufficient-rung selection re-derived and confirmed:

PASS ladder (author) -> accepted
PASS decision read (review) -> accepted
PASS decision write (review) -> accepted
PASS ladder-fails-open -> rejected
PASS ladder-no-escalate -> rejected
PASS unknown-field -> rejected
PASS verdict-out-of-set -> rejected
PASS indeterminate-final -> rejected
PASS read selects rung 1
PASS read does not climb
PASS write selects rung 3
PASS write climbs
PASS riskier claim reaches a costlier rung