test_glass.py

"""Regression suite for Glass.

Runs every example and every expected-failure case, prints a summary.
"""
from __future__ import annotations
import subprocess
import sys
import os

# Glass requires Python >= 3.10 (pyproject.toml). On an older interpreter the suite "runs" but
# every quartz (compile) gate dies on a `dict | None` annotation TypeError — 176 cryptic FAILs
# instead of one clear message. Fail fast and loudly instead (macOS /usr/bin/python3 is 3.9).
if sys.version_info < (3, 10):
    sys.exit(f"tests/test_glass.py: Python >= 3.10 required (running {sys.version.split()[0]}); "
             "try python3.12")

HERE = os.path.dirname(os.path.abspath(__file__))
ROOT = os.path.dirname(HERE)
GLASS = os.path.join(ROOT, "glass.py")
EX = os.path.join(ROOT, "examples")


def run(src: str) -> tuple[int, str, str]:
    p = subprocess.run(
        [sys.executable, GLASS, "/dev/stdin"],
        input=src, capture_output=True, text=True,
    )
    return p.returncode, p.stdout, p.stderr


def run_file(path: str) -> tuple[int, str, str]:
    p = subprocess.run(
        [sys.executable, GLASS, path], capture_output=True, text=True,
    )
    return p.returncode, p.stdout, p.stderr


# A heavy native `glass prove` gate occasionally HANGS in a resource-starved env — the documented
# under-load native-compile flake (a native subprocess deadlocks at 0% CPU). Without a timeout, the
# suite's subprocess.run would block FOREVER on that one gate, so the whole suite never completes.
# `_prove_run` bounds every prove gate: a hang past PROVE_TIMEOUT becomes a synthetic signal-like
# result (rc=137), which `_heavy_skipped` treats as an env-limited SKIP (CI green) — exactly as it
# already does for a signal-KILLED heavy prove. A genuine regression still returns a verdict in time
# and is evaluated normally; only a true hang is skipped (and logged — no silent cap). Legit heavy
# proves finish in well under a minute, so a multi-minute timeout fires only on a real stall.
PROVE_TIMEOUT = 600

def _prove_run(args, **kw):
    kw.setdefault("capture_output", True)
    kw.setdefault("text", True)
    kw.setdefault("cwd", ROOT)
    try:
        return subprocess.run(args, timeout=PROVE_TIMEOUT, **kw)
    except subprocess.TimeoutExpired:
        return subprocess.CompletedProcess(args, 137, stdout="", stderr=f"TIMEOUT >{PROVE_TIMEOUT}s (native prove hung — env-limited)")


# Examples that must succeed.
POSITIVE = [
    os.path.join(EX, "basic",    "hello.glass"),
    os.path.join(EX, "basic",    "fib.glass"),
    os.path.join(EX, "basic",    "list_ops.glass"),
    os.path.join(EX, "basic",    "option_result.glass"),
    os.path.join(EX, "basic",    "records.glass"),
    os.path.join(EX, "features", "generics.glass"),
    os.path.join(EX, "features", "crypto.glass"),
    os.path.join(EX, "features", "effects.glass"),
    os.path.join(EX, "features", "queries.glass"),
    os.path.join(EX, "features", "ai.glass"),
    os.path.join(EX, "features", "infer.glass"),
    os.path.join(EX, "selfhost", "parser.glass"),
    os.path.join(EX, "selfhost", "bootstrap.glass"),
    os.path.join(EX, "selfhost", "prism.glass"),
    os.path.join(EX, "selfhost", "typecheck.glass"),
    os.path.join(EX, "selfhost", "mini.glass"),
    os.path.join(EX, "showcase", "derive.glass"),
    os.path.join(EX, "showcase", "prover.glass"),
    os.path.join(EX, "showcase", "nash.glass"),
    os.path.join(EX, "showcase", "quantum.glass"),
    os.path.join(EX, "showcase", "golden.glass"),
    os.path.join(EX, "showcase", "harmonic.glass"),
    os.path.join(EX, "showcase", "geometry.glass"),
    os.path.join(EX, "showcase", "fractal.glass"),
    os.path.join(EX, "showcase", "spiral.glass"),
    os.path.join(EX, "showcase", "symmetry.glass"),
    os.path.join(EX, "showcase", "epistemic.glass"),
    os.path.join(EX, "showcase", "entanglement.glass"),
    os.path.join(EX, "showcase", "amplitude.glass"),
    os.path.join(EX, "showcase", "strategy.glass"),
    os.path.join(EX, "showcase", "worlds.glass"),
    os.path.join(EX, "showcase", "rational.glass"),
    os.path.join(EX, "showcase", "probability.glass"),
    os.path.join(EX, "showcase", "causal.glass"),
    os.path.join(EX, "showcase", "counterfactual.glass"),
    os.path.join(EX, "showcase", "identity.glass"),
    os.path.join(EX, "showcase", "observer.glass"),
    os.path.join(EX, "showcase", "simulation.glass"),
    os.path.join(EX, "showcase", "infoflow.glass"),
    os.path.join(EX, "showcase", "units.glass"),
    os.path.join(EX, "showcase", "conservation.glass"),
    os.path.join(EX, "showcase", "linear.glass"),
    os.path.join(EX, "features", "linear_ok.glass"),
    os.path.join(EX, "showcase", "refined_data.glass"),
    os.path.join(EX, "features", "imports.glass"),
    os.path.join(EX, "showcase", "refine.glass"),
    os.path.join(EX, "showcase", "compose.glass"),
    os.path.join(EX, "showcase", "imply.glass"),
    os.path.join(EX, "showcase", "regex.glass"),
    os.path.join(EX, "showcase", "json.glass"),
    os.path.join(EX, "showcase", "config.glass"),
    os.path.join(EX, "showcase", "markdown.glass"),
    os.path.join(EX, "features", "letstar.glass"),
    os.path.join(EX, "features", "letqmark.glass"),
    os.path.join(EX, "features", "letpat.glass"),
    os.path.join(EX, "features", "generic_fn.glass"),
    os.path.join(EX, "features", "generic_rec.glass"),
    os.path.join(EX, "features", "refine.glass"),
    os.path.join(EX, "features", "alpha_refine.glass"),
    os.path.join(EX, "features", "imply_refine.glass"),
    os.path.join(EX, "features", "runtime_refine.glass"),
    os.path.join(EX, "features", "curried_refine.glass"),
    os.path.join(EX, "features", "return_refine.glass"),
    os.path.join(EX, "features", "safe_div.glass"),
    os.path.join(EX, "features", "parens_after_let.glass"),
    os.path.join(EX, "features", "lambda_refine.glass"),
    os.path.join(EX, "features", "lambda_multi.glass"),
    os.path.join(EX, "features", "lambda_multi_refine.glass"),
    os.path.join(EX, "features", "and_or.glass"),
    os.path.join(EX, "features", "mod_refine.glass"),
    os.path.join(EX, "features", "not_refine.glass"),
    os.path.join(EX, "features", "xparam_refine.glass"),
    os.path.join(EX, "selfhost", "prism_lexer.glass"),
    os.path.join(EX, "selfhost", "quartz_min.glass"),
    os.path.join(EX, "selfhost", "build_pipeline.glass"),
    os.path.join(EX, "selfhost", "quartz_parser.glass"),
    os.path.join(EX, "selfhost", "selfcompile.glass"),
    os.path.join(EX, "stage3", "tinylang.glass"),
    os.path.join(EX, "stage3", "tinycalc.glass"),
    os.path.join(EX, "stage3", "midlang.glass"),
    os.path.join(EX, "stage3", "safecalc.glass"),
]

# (label, source, expected substring in stderr) — must fail with the right reason.
NEGATIVE = [
    # ---- v0.0.1 cases ----
    # ---- Tzimtzum: a concealed value can never escape to an observable position ----
    ("conceal cannot be revealed by arithmetic",
     'conceal(5) + 1',
     "Concealed"),
    ("conceal is opaque — no constructor, cannot be pattern-matched open",
     'match conceal(5) { Conceal(x) => x }',
     "unknown constructor"),
    ("fn return mismatch",
     'fn f(n: Int) : Int = "no"',
     "declared return Int, body is String"),

    ("heterogeneous list",
     'let xs : List<Int> = [1, 2, "three"]',
     "list elements differ"),

    ("bare spread outside list points to ++",
     'let x : Int = 1\n'
     'let y : List<Int> = ...x',
     "use '++'"),

    ("if branches differ",
     'let x : Int = if true then 1 else "x"',
     "if branches differ"),

    ("polymorphic builtin mismatch",
     'let xs : List<String> = ["a"]\n'
     'fn d(n: Int) : Int = n\n'
     'let bad : List<Int> = map(xs, d)',
     "arg type mismatch"),

    ("unbound identifier",
     'let x : Int = nope',
     "unbound identifier"),

    ("arity mismatch",
     'fn f(a: Int, b: Int) : Int = a + b\n'
     'let r : Int = f(1)',
     "arity mismatch"),

    # ---- v0.1 sum-type cases ----
    ("non-exhaustive match on Option",
     'fn f(o: Option<Int>) : Int = match o { Some(x) => x }',
     "non-exhaustive match on Option"),

    ("non-exhaustive match on Bool",
     'fn f(b: Bool) : Int = match b { true => 1 }',
     "non-exhaustive match"),

    ("non-exhaustive match on List",
     'fn f(xs: List<Int>) : Int = match xs { [] => 0 }',
     "non-exhaustive match on list"),

    # Nested-pattern exhaustiveness: a refutable SUB-pattern leaves cases
    # uncovered even when the outer shape looks total. These used to type-check
    # and then crash at runtime ("non-exhaustive match" RuntimeError).
    ("non-exhaustive: refutable list head",
     'fn f(xs: List<Int>) : Int = match xs { [] => 0; [1, ...t] => 9 }',
     "non-exhaustive match on list"),
    ("non-exhaustive: fixed-length list misses longer",
     'fn f(xs: List<Int>) : Int = match xs { [] => 0; [a, b] => a + b }',
     "non-exhaustive match on list"),
    ("non-exhaustive: refutable tuple component",
     'fn f(p: (Int, Int)) : Int = match p { (1, b) => b }',
     "non-exhaustive match on tuple"),
    ("non-exhaustive: refutable constructor argument",
     'type Box = Empty | Hold(Int)\n'
     'fn f(b: Box) : Int = match b { Empty => 0; Hold(1) => 9 }',
     "non-exhaustive match on Box"),

    ("ctor from wrong type",
     'fn f(o: Option<Int>) : Int = match o { Ok(x) => x ; None => 0 }',
     "Ok is from Result, but scrutinee is Option"),

    ("type-arity mismatch on annotation",
     'let bad : Option<Int, String> = None',
     "expects 1 arg"),

    ("unknown type in annotation",
     'let bad : Frobnicate<Int> = None',
     "unknown type"),

    ("ctor expects more fields",
     'let bad : Option<Int> = Some',
     # Some has no args here — it's the bare ctor as a value, which has fn type;
     # the annotation expects Option<Int>, not (Int) -> Option<Int>.
     "declared Option<Int>"),

    # ---- v0.2 cases ----
    ("head returns Option, not raw",
     'let xs : List<Int> = [1, 2, 3]\n'
     'let bad : Int = head(xs)',
     "declared Int, inferred Option<Int>"),

    ("Pair from prelude — type-arity check",
     'let bad : Pair<Int> = Pair(1, 2)',
     "expects 2 arg"),

    ("can't mix env types in Pair list",
     'let bad : List<Pair<String, Int>> = [Pair("a", 1), Pair("b", "wrong")]',
     "list elements differ"),

    # ---- v0.3 polymorphism soundness cases ----
    ("can't treat type param as Int inside body",
     'fn bad<A>(x: A) : A = let y : A = 42 in y',
     "let-in y: declared A, inferred Int"),

    ("can't return Int as type param A",
     'fn bad<A>(x: A) : A = 42',
     "declared return A, body is Int"),

    ("calling polymorphic fn with mismatched types",
     'fn id<T>(x: T) : T = x\n'
     'fn use_it(s: String) : Int = id(s)',
     "declared return Int"),

    ("type-arity on user-defined polymorphic fn",
     'fn id<T>(x: T) : T = x\n'
     'let bad : Int = id(1, 2)',
     "arity mismatch"),

    # ---- v0.4 refinement-type cases ----
    # v1.2: refinements with constant args are discharged statically.
    ("refinement violated at compile time (literal arg)",
     'fn d(a: Int, b: Int where (b != 0)) : Int = a / b\n'
     'let r : Int = d(10, 0)',
     "refinement violated at compile time"),

    # Runtime check still applies for non-constant arguments.
    ("refinement violated at runtime (dynamic arg)",
     'fn d(a: Int, b: Int where (b != 0)) : Int = a / b\n'
     'fn ident(n: Int) : Int = n\n'
     'let zero = ident(0)\n'
     'let r : Int = d(10, zero)',
     "refinement violated: b = 0"),

    # v4.24: curried multi-param case where the refinement is on the
    # SECOND param and the arg is a let-bound variable (not a literal).
    # Pinned down as a host-parity spec — prism's port mirrors this
    # error shape via its v4.24 VRefinedClos wrapper.
    ("refinement violated on second param at runtime (v4.24 host parity)",
     "fn safe_add(a: Int, b: Int where (b != 0)) : Int = a + b\n"
     "let zero : Int = 0\n"
     "let r : Int = safe_add(10, zero)",
     "refinement violated: b = 0"),

    # v4.25: return-type refinement violation. Host check has been in
    # place since v1.3; prism's port mirrors this shape — the
    # VRefinedClos wrapper carries the return type forward across
    # curried applies and checks against the final value on the last
    # apply.
    ("return refinement violated (multi-param, v4.25 host parity)",
     "fn diff(a: Int, b: Int) : Int where (result >= 0) = a - b\n"
     "let smaller : Int = 3\n"
     "let bigger : Int = 7\n"
     "let r : Int = diff(smaller, bigger)",
     "refinement violated: result = -4"),

    # Static discharge through arithmetic constant-folding.
    ("static discharge via subtraction fold",
     'fn f(n: Int where (n > 0)) : Int = n\n'
     'let r : Int = f(5 - 7)',
     "refinement violated at compile time"),

    # Static discharge through if-then-else folding.
    ("static discharge via if-fold",
     'fn f(n: Int where (n > 0)) : Int = n\n'
     'let r : Int = f(if true then 0 else 10)',
     "refinement violated at compile time"),

    # Return-type refinement violation at runtime (v1.3).
    ("return refinement violated at runtime",
     'fn negate(n: Int) : Int where (result >= 0) = 0 - n\n'
     'let r : Int = negate(5)',
     "refinement violated: result = -5 fails predicate"),

    # v1.4: implication discharges (result >= 5) does NOT imply (n > 5),
    # so the runtime check fires when at_least_five returns exactly 5.
    ("implication unsound: >= 5 should not imply > 5",
     'fn at_least_five(n: Int) : Int where (result >= 5) =\n'
     '  if n >= 5 then n else 5\n'
     'fn needs_above_five(n: Int where (n > 5)) : Int = n\n'
     'let r : Int = needs_above_five(at_least_five(0))',
     "refinement violated: n = 5 fails predicate (n > 5)"),

    ("refinement predicate must be Bool",
     'fn d(b: Int where (b + 1)) : Int = b',
     "must return Bool"),

    ("refinement predicate references unbound name",
     'fn d(b: Int where (q > 0)) : Int = b',
     "unbound identifier"),

    ("let refinement violated",
     'let x : Int where (x > 100) = 5',
     "refinement violated: x = 5"),

    # ---- v0.5 effect-tracking cases ----
    ("pure fn performing IO without declaring",
     'fn loud() : Int = let _ : String = print("oops") in 42',
     "fn loud performs effect(s) ['IO']"),

    ("fn declaring only IO but doing Random",
     'fn r() : Int !{IO} = random_int(0, 10)',
     "performs effect(s) ['Random']"),

    ("fn declaring only Random but doing IO",
     'fn s() : Int !{Random} = let _ : String = print("hi") in 0',
     "performs effect(s) ['IO']"),

    # ---- v0.7 effect polymorphism + Inference ----
    ("pure fn can't use map with effectful callback (caller must declare effects)",
     'fn loud(n: Int) : Int !{IO} =\n'
     '  let _ : String = print("x") in n\n'
     'fn pure_run() : List<Int> = map([1, 2], loud)',
     "performs effect(s) ['IO']"),

    ("undeclared !{Inference} is caught",
     'fn sneaky(s: String) : String = model_call("x: " ++ s)',
     "performs effect(s) ['Inference']"),

    ("fn declaring IO but body also does Inference is caught",
     'fn mixed(s: String) : String !{IO} =\n'
     '  let _ : String = print("doing it") in\n'
     '  model_call(s)',
     "performs effect(s) ['Inference']"),

    # A body that propagates TWO distinct abstract effect rows but declares
    # only one used to be accepted (extend_effects dropped the 2nd row var),
    # which let a fn that performs the 2nd effect be certified without it —
    # a soundness hole. The dropped row must now surface as undeclared.
    ("fn propagating a 2nd abstract effect row can't hide it under a 1-var decl",
     'fn twice<E, F>(p: () -> Int !{E}, q: () -> Int !{F}) : Int !{E} = p() + q()',
     "not declared in {E}"),

    # ---- v0.6 tuple cases ----
    ("tuple-arity mismatch in pattern",
     'let p : (Int, String) = (1, "x")\n'
     'fn f(p: (Int, String)) : Int = match p { (a, b, c) => a }',
     "tuple pattern arity mismatch"),

    ("tuple type-arity mismatch",
     'let p : (Int, String) = (1, 2)',
     "declared (Int, String), inferred (Int, Int)"),

    ("non-tuple destructured with tuple pattern",
     'fn f(n: Int) : Int = match n { (a, b) => a }',
     "tuple pattern against Int"),

    # Mutual recursion success: this would have failed before v0.6.
    # Tested via examples/queries.glass (bump <-> count_by_country) and
    # by being able to declare fns in source-independent order.

    # ---- v0.7 effect polymorphism + Inference ----
    ("pure fn can't use polymorphic map with Inference callback",
     'fn pure_batch(xs: List<String>) : List<String> =\n'
     '  map(xs, fn(s: String) -> model_call(s))',
     "performs effect(s) ['Inference']"),

    ("fn declaring only IO can't call a model",
     'fn io_only(s: String) : String !{IO} = model_call(s)',
     "performs effect(s) ['Inference']"),

    ("refinement violation on model output",
     'fn must_be_long(s: String) : String !{Inference} =\n'
     '  let r : String where (string_length(r) >= 1000) = model_call(s) in r\n'
     'let _ : String = must_be_long("hi")',
     "refinement violated"),

    # ---- v0.8 record cases ----
    ("record missing field",
     'type U = { id: Int, name: String }\n'
     'let u : U = U { id: 1 }',
     "missing field"),

    ("record extra field",
     'type U = { id: Int }\n'
     'let u : U = U { id: 1, extra: 5 }',
     "has no field"),

    ("record wrong field type",
     'type U = { id: Int, name: String }\n'
     'let u : U = U { id: "wrong", name: "Alice" }',
     "expected Int"),

    ("field access on non-record",
     'let n : Int = 5\n'
     'let x : Int = n.foo',
     "field access on non-record"),

    ("field access on unknown field",
     'type U = { id: Int }\n'
     'let u : U = U { id: 1 }\n'
     'let x : Int = u.bogus',
     "no field 'bogus'"),

    ("sum type used as record literal",
     'type Maybe = | Nope | Yep(Int)\n'
     'let m : Maybe = Maybe { Nope: 1 }',
     "use Maybe(...) for constructor call"),

    # ---- v0.8.1 string-ops cases ----
    ("substring with negative index",
     'let s : String = substring("hello", -1, 3)',
     "negative index"),

    ("substring with start > end",
     'let s : String = substring("hello", 4, 2)',
     "start > end"),

    # ---- v4.47: refined-param lambda rejection ----
    # The lambda's `where (x > 0)` runs at apply time. `let n = 0 - 3`
    # produces a non-literal so static discharge defers; the runtime
    # check then fires on n = -3 and the predicate fails.
    ("refined-param lambda rejects bad arg (v4.47)",
     "let n : Int = 0 - 3\n"
     "let r : Int = (fn(x: Int where (x > 0)) -> x * 2)(n)\n"
     "r\n",
     "refinement violated"),

    # ---- v4.48: refined SECOND param of a multi-arg lambda ----
    # First arg satisfies its refinement; the second fails. Pins
    # down that the per-param TyRefine check runs at each position,
    # not just the first.
    ("multi-arg refined lambda rejects 2nd arg (v4.48)",
     "let n : Int = 0\n"
     "let r : Int = (fn(a: Int where (a > 0), b: Int where (b > 0))"
     " -> a * b)(3, n)\n"
     "r\n",
     "b = 0 fails predicate"),

    # ---- v4.51: && / || type-checked as Bool, Bool → Bool ----
    # Non-Bool operands must be rejected with a clear shape error.
    ("&& rejects non-Bool operands (v4.51)",
     "let r : Bool = 1 && true\n",
     "expected Bool, Bool"),

    # ---- v4.53: % type-checked as Int, Int → Int ----
    ("% rejects non-Int operands (v4.53)",
     "let r : Int = true % 2\n",
     "expected Int, Int"),

    # ---- v4.54: ! requires a Bool operand ----
    ("! rejects non-Bool operand (v4.54)",
     "let r : Bool = !5\n",
     "expected Bool"),

    # ---- v4.56: cross-parameter refinement rejects bad input ----
    # hi=3, lo=10 → hi > lo is false. The check sees lo (earlier
    # param) and fires.
    ("cross-param refinement rejects bad input (v4.56)",
     "fn clamp(lo: Int, hi: Int where (hi > lo)) : Int = hi - lo\n"
     "let bad : Int = clamp(10, 3)\n"
     "bad\n",
     "refinement violated"),

    # ---- v4.66: conservation-law refinement rejects minting ----
    # The gate `after == before` (cross-param) fails when a transition
    # creates value (175 → 200), so non-conservative transitions are
    # rejected at the boundary.
    ("conservation refinement rejects minting (v4.66)",
     "fn checked(before: Int, after: Int where (after == before)) : Int"
     " = after\n"
     "let bad : Int = checked(175, 200)\n"
     "bad\n",
     "refinement violated"),

    # ---- v4.67: linear types — no cloning, no dropping ----
    # Using a linear resource twice is forbidden (no cloning).
    ("linear resource rejects cloning (v4.67)",
     "fn f() : Int = let lin x = 5 in x + x\n"
     "f()\n",
     "no cloning"),
    # Dropping a linear resource (never using it) is forbidden.
    ("linear resource rejects dropping (v4.67)",
     "fn f() : Int = let lin x = 5 in 99\n"
     "f()\n",
     "no dropping"),
    # Capturing a linear value in a closure can't guarantee single use.
    ("linear resource rejects lambda capture (v4.67)",
     "fn f() : Int = let lin x = 5 in (fn(y: Int) -> x + y)(3)\n"
     "f()\n",
     "captured in a lambda"),

    # ---- v4.69: field-level refinements rejected at construction ----
    # A negative value can't be packed into a Pos.
    ("refined ADT field rejects bad value (v4.69)",
     "type Pos = | Pos(n: Int where (n > 0))\n"
     "let bad = Pos(0 - 3)\n"
     "bad\n",
     "n = -3 fails predicate"),
    # Cross-field: hi must exceed lo; Range(10, 3) is rejected.
    ("cross-field refinement rejects bad range (v4.69)",
     "type Range = | Range(lo: Int, hi: Int where (hi > lo))\n"
     "let bad = Range(10, 3)\n"
     "bad\n",
     "hi = 3 fails predicate"),
]


def main() -> int:
    failures = 0

    print("== positive cases ==")
    for path in POSITIVE:
        rc, out, err = run_file(path)
        ok = (rc == 0)
        print(f"  {'OK ' if ok else 'FAIL'}  {os.path.basename(path)}")
        if not ok:
            print(f"        stderr: {err.strip()}")
            failures += 1

    print("== negative cases (must reject) ==")
    for label, src, needle in NEGATIVE:
        rc, out, err = run(src)
        ok = (rc != 0) and (needle in err)
        print(f"  {'OK ' if ok else 'FAIL'}  {label}")
        if not ok:
            print(f"        rc={rc}, expected substring {needle!r}")
            print(f"        stderr: {err.strip()}")
            failures += 1

    print("== inline regression cases ==")
    # (label, source, expected substring in stdout). Short programs that
    # pin down specific past bugs. Add a case when fixing a real bug.
    inline_positive = [
        # Tzimtzum: conceal a value, compute within concealment (cmap), prove a property
        # about it (concealed_in_range -> a PUBLIC Bool) — all without ever revealing it.
        ("Concealed<T>: provable-about, computable-within, never revealed",
         "fn add5(x: Int) : Int = x + 5\n"
         "let c : Concealed<Int> = cmap(conceal(20), add5)\n"
         "let ok : Bool = concealed_in_range(c, 24, 26)\n"
         "ok\n",
         "ok : Bool = true"),
        # Exhaustiveness must recognise coverage spread ACROSS arms via nested
        # patterns: the two Ok(...) arms together cover all of Box, so this is
        # total and must NOT be rejected (guards the recursive checker against
        # the over-strict per-arm version).
        ("nested cross-arm exhaustiveness accepted",
         "type Box = Empty | Hold(Int)\n"
         "fn f(r: Result<Box, String>) : Int =\n"
         "  match r { Ok(Hold(x)) => x; Ok(Empty) => 0; Err(m) => 0 - 1 }\n"
         "let out : Int = f(Ok(Hold(7)))\n"
         "out\n",
         "out : Int = 7"),
        # Interpreter integer arithmetic matches the compiled int64/C backend
        # (see eval_binop): / and % truncate toward zero (not Python floor),
        # + - * wrap at 64 bits, and a shift count is masked to 6 bits. Pins
        # the host side of the host<->compiled agreement on the exact inputs
        # where they used to diverge.
        ("neg division truncates toward zero",  "let r : Int = (0 - 7) / 2\nr\n",  "r : Int = -3"),
        ("neg modulo has dividend sign",        "let r : Int = (0 - 7) % 2\nr\n",  "r : Int = -1"),
        ("int64 overflow wraps (+)",            "let r : Int = 9223372036854775807 + 1\nr\n", "r : Int = -9223372036854775808"),
        ("shift count masked to 6 bits",        "let r : Int = bit_shl(1, 64)\nr\n", "r : Int = 1"),
        # v4.21: parser used to greedily eat an LPAREN-starting next line as
        # call-continuation. `let s = id("hello")\n(n, s)` mis-parsed to
        # `id("hello")(n, s)` and crashed with "not a function: String".
        # The column-1 + new-line rule in parse_postfix stops it.
        ("parens-after-let split (v4.21)",
         'fn id<A>(x: A) : A = x\n'
         'let n = id(42)\n'
         'let s = id("hello")\n'
         'let p = (n, s)\n'
         'p\n',
         "(42, hello)"),
        # v4.28: deep tail recursion. Without the trampoline-based TCE
        # added in v4.28, count_down(15000) blows Python's recursion
        # limit even with sys.setrecursionlimit(20000). The test verifies
        # both correctness and unbounded-depth tolerance. We use 25000 to
        # exceed any reasonable Python limit so the test FAILS if TCE is
        # ever accidentally removed.
        ("deep tail recursion via TCE (v4.28)",
         "fn count_down(n: Int) : Int =\n"
         "  if n == 0 then 0 else count_down(n - 1)\n"
         "let result : Int = count_down(25000)\n"
         "result\n",
         "result : Int = 0"),
        # v4.28: tail-recursive sum_to with explicit accumulator. The
        # arithmetic check pins down the *value* — confirms that env
        # bindings (acc) flow correctly through the trampoline.
        ("tail-recursive accumulator via TCE (v4.28)",
         "fn sum_to(n: Int, acc: Int) : Int =\n"
         "  if n == 0 then acc else sum_to(n - 1, acc + n)\n"
         "let result : Int = sum_to(50000, 0)\n"
         "result\n",
         "result : Int = 1250025000"),
        # v4.23: prism runtime refinement check fires when static discharge
        # defers. The host already enforces runtime checks (since v0.4); this
        # test runs the same program through host to pin down the shape of the
        # error message that prism's port mirrors. The prism-side check is
        # exercised end-to-end when prism.glass runs in the POSITIVE list —
        # its demo chain reads runtime_refine_bad.glass and prints the same
        # message, which surfaces in prism's stdout (not its exit code).
        ("runtime refinement check (v4.23 host parity)",
         "fn positive_double(n: Int where (n > 0)) : Int = n * 2\n"
         "let x : Int = 21\n"
         "let r : Int = positive_double(x)\n"
         "r\n",
         "r : Int = 42"),
        # v4.21 drift catch: AGENT.md §5 claimed sequential top-level lets
        # using the same generic fn at different types fail to type-check.
        # They don't — the symptom in §5's repro was the parens-after-let
        # parser bug above. Pin both invariants down with a test.
        ("sequential generic-fn instantiation (v4.21)",
         'fn id<A>(x: A) : A = x\n'
         'let n = id(42)\n'
         'let s = id("hello")\n'
         'let b = id(true)\n'
         'b\n',
         ": Bool = true"),
        # v4.47: refined-param lambdas. Before v4.47 the host's
        # parse_lambda called parse_params without accept_refinement,
        # so `fn(x: Int where (x > 0)) -> ...` failed at the `where`
        # token. Now the parser accepts the refinement and the
        # existing apply_fn TyRefine path checks the predicate at
        # call time. Positive case: 5 > 0 holds, body returns 10.
        ("refined-param lambda accepts (v4.47)",
         "let r : Int = (fn(x: Int where (x > 0)) -> x * 2)(5)\n"
         "r\n",
         "r : Int = 10"),
        # v4.47 capture-aware variant: the lambda closes over `k`
        # AND has a refined param. Confirms ELamR (prism) / refined
        # Lambda (host) interoperates with closures, not just bare
        # arithmetic — refinement check runs before capture lookup.
        ("refined-param lambda with capture (v4.47)",
         "let k : Int = 100\n"
         "let r : Int = (fn(x: Int where (x > 0)) -> x + k)(7)\n"
         "r\n",
         "r : Int = 107"),
        # v4.48: multi-param lambdas. Three-arg variant pins down
        # that the right-fold builds the chain correctly across more
        # than two params (a common edge of "did I get the
        # recursion-base-case right?").
        ("three-arg lambda applied inline (v4.48)",
         "let r : Int = (fn(a: Int, b: Int, c: Int) -> a + b + c)(1, 2, 3)\n"
         "r\n",
         "r : Int = 6"),
        # v4.51: `&&` and `||` lex, parse, typecheck, evaluate. The
        # bigger language win for v4.51 is that boolean combinators
        # become legal in refinement predicates — pinning down basic
        # eval here means the predicate machinery has solid ground.
        ("&& and || basic truth tables (v4.51)",
         "let a : Bool = true && false\n"
         "let b : Bool = true || false\n"
         "let c : Bool = (3 > 0) && (3 < 100)\n"
         "let r : Bool = (a == false) && b && c\n"
         "r\n",
         "r : Bool = true"),
        # v4.51 precedence pin-down: `&&` binds tighter than `||`.
        # `false || true && false` must parse as
        # `false || (true && false)` = `false || false` = false.
        # If precedence were inverted it would be
        # `(false || true) && false` = `true && false` = false (same
        # answer by luck) — so we need a discriminating case:
        # `true && false || true` parses as `(true && false) || true`
        # = `false || true` = true. Flipped would be
        # `true && (false || true)` = `true && true` = true (same).
        # The actually discriminating shape:
        ("&& binds tighter than || (v4.51)",
         "let r : Bool = false || true && false\n"
         "r\n",
         "r : Bool = false"),
        # v4.51 range refinement at runtime. `n > 0 && n < 100` is
        # the canonical interval refinement; before this release a
        # single-comparison was the only valid shape.
        ("range refinement via && (v4.51)",
         "fn middling(n: Int where (n > 0 && n < 100)) : Int = n + 1\n"
         "let r : Int = middling(50)\n"
         "r\n",
         "r : Int = 51"),
        # v4.51 short-circuit semantics: the rhs of `&&` is NOT
        # evaluated when lhs is false. We probe this by putting an
        # expression that WOULD raise (refinement violation) on the
        # rhs, then verify the program completes successfully.
        ("&& short-circuits on false lhs (v4.51)",
         "fn pos(n: Int where (n > 0)) : Int = n\n"
         "let n : Int = 0\n"
         "let r : Bool = (n > 0) && (pos(n) > 0)\n"
         "r\n",
         "r : Bool = false"),
        # v4.53: modulo as a basic arithmetic operator. Same precedence
        # as `*` and `/`, so `1 + 17 % 5` parses as `1 + (17 % 5) = 3`.
        ("basic modulo + precedence (v4.53)",
         "let r : Int = 1 + 17 % 5\n"
         "r\n",
         "r : Int = 3"),
        # v4.53: parity refinement. The canonical use of `%` in
        # predicate position — `n % 2 == 0` enforces evenness.
        ("parity refinement holds (v4.53)",
         "fn even_only(n: Int where (n % 2 == 0)) : Int = n + 1\n"
         "let r : Int = even_only(10)\n"
         "r\n",
         "r : Int = 11"),
        # v4.54: unary NOT. Basic truth + double-negation + applied to
        # a comparison. `!(3 > 5)` is true.
        ("unary NOT basics (v4.54)",
         "let a : Bool = !true\n"
         "let b : Bool = !!false\n"
         "let r : Bool = (a == false) && (b == false) && !(3 > 5)\n"
         "r\n",
         "r : Bool = true"),
        # v4.54: NOT in a refinement predicate. `!(n == 0)` is the
        # "anything but zero" guard; 5 satisfies it so 100/5 = 20.
        ("NOT refinement holds (v4.54)",
         "fn nonzero(n: Int where (!(n == 0))) : Int = 100 / n\n"
         "let r : Int = nonzero(5)\n"
         "r\n",
         "r : Int = 20"),
        # v4.55: arithmetic inside a refinement predicate. The host
        # always handled this (full eval); v4.55 brings Quartz to
        # parity. Pinned here so host + Quartz agree on the shape.
        ("arithmetic in refinement predicate (v4.55)",
         "fn f(n: Int where (n * n >= 1 && n + 1 > 0)) : Int = n\n"
         "let r : Int = f(7)\n"
         "r\n",
         "r : Int = 7"),
        # v4.56: cross-parameter refinement in the host. `hi > lo`
        # references the earlier param; host binds-and-checks in order
        # so `lo` is bound when `hi`'s check runs. clamp(3,10) = 7.
        ("cross-parameter refinement holds (v4.56)",
         "fn clamp(lo: Int, hi: Int where (hi > lo)) : Int = hi - lo\n"
         "let r : Int = clamp(3, 10)\n"
         "r\n",
         "r : Int = 7"),
        # v4.48 composes with v4.47: two-arg lambda where BOTH params
        # are refined. The host's apply_fn checks each TyRefine at
        # call time; prism's port mirrors via two stacked VRefinedClos
        # wrappers. 3 > 0 and 4 > 0 hold, body returns 12.
        ("two-arg refined lambda (v4.48)",
         "let r : Int = (fn(a: Int where (a > 0), b: Int where (b > 0))"
         " -> a * b)(3, 4)\n"
         "r\n",
         "r : Int = 12"),
        # v4.57: quantum-inspired measurement (showcase/quantum.glass).
        # Weighted collapse via cumulative buckets + `seed % total`.
        # Over seeds 0..99 a 9:1 superposition collapses to |0> exactly
        # 90 times — measurement frequency tracks the weights, and the
        # whole thing is pure (seed threaded explicitly).
        ("quantum measurement tracks weights (v4.57)",
         "type Amp = | Amp(String, Int)\n"
         "fn tw(xs: List<Amp>) : Int =\n"
         "  fold(xs, 0, fn(a: Int, x: Amp) -> match x { Amp(_, w) => a + w })\n"
         "fn pick(xs: List<Amp>, r: Int) : String =\n"
         "  match xs { [] => \"_\";"
         " [Amp(l, w), ...rest] => if r < w then l else pick(rest, r - w) }\n"
         "fn measure(xs: List<Amp>, seed: Int where (seed >= 0)) : String =\n"
         "  pick(xs, seed % tw(xs))\n"
         "let bias = [Amp(\"|0>\", 9), Amp(\"|1>\", 1)]\n"
         "let hits : Int =\n"
         "  fold(range(0, 100), 0, fn(a: Int, s: Int) ->\n"
         "    if measure(bias, s) == \"|0>\" then a + 1 else a)\n"
         "hits\n",
         "hits : Int = 90"),
        # v4.58 (Proportion & Form bundle): the golden fingerprint.
        # |a² − a·b − b²| = 1 holds EXACTLY for consecutive Fibonacci
        # pairs — here (34, 21) gives residue +1, the φ convergent test.
        ("golden-ratio residue is +1 for Fibonacci pair (v4.58)",
         "fn residue(a: Int, b: Int) : Int = a * a - a * b - b * b\n"
         "let r : Int = residue(34, 21)\n"
         "r\n",
         "r : Int = 1"),
        # v4.58: Euler's formula as the polyhedron refinement. The
        # cross-param gate accepts the dodecahedron (20−30+12 = 2) and
        # the body returns V+E+F.
        ("Euler polyhedron gate accepts dodecahedron (v4.58)",
         "fn make_poly(v: Int, e: Int, f: Int where (v - e + f == 2)) : Int"
         " = v + e + f\n"
         "let r : Int = make_poly(20, 30, 12)\n"
         "r\n",
         "r : Int = 62"),
        # v4.58: harmonic consonance via gcd-reduction. 6:4 reduces to
        # 3:2 (perfect fifth) — reduced denominator 2 <= 4, consonant.
        ("harmonic ratio reduces to perfect fifth (v4.58)",
         "fn gcd(a: Int, b: Int) : Int = if b == 0 then a else gcd(b, a % b)\n"
         "let rd : Int = 4 / gcd(6, 4)\n"
         "rd\n",
         "rd : Int = 2"),
        # v4.59 (Self-Similarity & Spirals): the fractal self-similarity
        # gate. Sierpinski triples each depth, so 27 is a valid successor
        # of 9 under branch 3 (cross-param refinement next == prev * 3).
        ("fractal self-similarity gate (v4.59)",
         "fn next_level(prev: Int, branch: Int,"
         " next: Int where (next == prev * branch)) : Int = next\n"
         "let r : Int = next_level(9, 3, 27)\n"
         "r\n",
         "r : Int = 27"),
        # v4.59: the golden-spiral peel is exact in Int —
        # F(n+1) − F(n) = F(n-1). For F(6)=8, F(5)=5: 8 − 5 = 3 = F(4).
        # The Σ-Fibonacci identity F(1)+…+F(n) = F(n+2) − 1 gives 20 at
        # n=6, pinned via the closed form.
        ("golden spiral Fibonacci-sum identity (v4.59)",
         "fn fib(n: Int) : Int = if n < 2 then n else fib(n - 1) + fib(n - 2)\n"
         "let r : Int = fib(8) - 1\n"   # F(8)-1 = 21-1 = 20 = sum F(1..6)
         "r\n",
         "r : Int = 20"),
        # v4.60 (Epistemic-games + symmetry): D₄ is non-abelian — the
        # dihedral group law makes r1·s0 ≠ s0·r1. Composing a quarter
        # turn with a reflection in each order gives different elements
        # (s3 vs s1 in our encoding), so their rotation indices differ.
        ("D4 group is non-abelian (v4.60)",
         "fn mod4(n: Int) : Int = ((n % 4) + 4) % 4\n"
         "fn compose_k(k1: Int, f1: Bool, k2: Int, f2: Bool) : Int =\n"
         "  mod4((if f2 then 0 - k1 else k1) + k2)\n"
         "let rs : Int = compose_k(1, false, 0, true)\n"   # r1 then s0
         "let sr : Int = compose_k(0, true, 1, false)\n"   # s0 then r1
         "let r : Bool = rs != sr\n"
         "r\n",
         "r : Bool = true"),
        # v4.60: epistemic knowledge — a child KNOWS their own state iff
        # all indistinguishable live worlds agree on it. In the muddy
        # world (M,M) with only {(M,M)} live, the single world fixes the
        # value, so the child knows (returns the mud value 1).
        ("epistemic: knowledge from a singleton world set (v4.60)",
         "type World = | W(Int, Int)\n"
         "fn mud(c: Int, w: World) : Int ="
         " match w { W(a, b) => if c == 1 then a else b }\n"
         "fn knows(c: Int, w: World, live: List<World>) : Bool =\n"
         "  fold(live, true, fn(acc: Bool, x: World) ->"
         " acc && mud(c, x) == mud(c, w))\n"
         "let r : Bool = knows(1, W(1, 1), [W(1, 1)])\n"
         "r\n",
         "r : Bool = true"),
        # v4.61 (Quantum II): destructive interference. Two paths with
        # opposite-phase amplitudes (+1 and −1) sum to amplitude 0, so
        # the quantum probability |Σ aₖ|² = 0 — the outcome is
        # impossible despite each path being individually possible. The
        # classical sum Σ|aₖ|² would be 2. This is the dark fringe.
        ("destructive interference cancels (v4.61)",
         "type Cx = | Cx(Int, Int)\n"
         "fn cadd(a: Cx, b: Cx) : Cx ="
         " match a { Cx(ar, ai) => match b { Cx(br, bi) =>"
         " Cx(ar + br, ai + bi) } }\n"
         "fn norm2(z: Cx) : Int = match z { Cx(re, im) => re * re + im * im }\n"
         "fn qprob(ps: List<Cx>) : Int ="
         " norm2(fold(ps, Cx(0, 0), fn(a: Cx, p: Cx) -> cadd(a, p)))\n"
         "let r : Int = qprob([Cx(1, 0), Cx(0 - 1, 0)])\n"
         "r\n",
         "r : Int = 0"),
        # v4.61: entanglement — in the Bell state |00>+|11> (weights
        # 1,0,0,1), measuring q1=0 leaves only the 00 branch, so q2 is
        # determined to 0 (the conditional weight for q2=1 is zero).
        ("entanglement pins the partner qubit (v4.61)",
         "type Joint = | Joint(Int, Int, Int, Int)\n"
         "fn cond01(j: Joint) : Int ="   # q2=1 weight given q1=0
         " match j { Joint(w00, w01, w10, w11) => w01 }\n"
         "let bell = Joint(1, 0, 0, 1)\n"
         "let r : Int = cond01(bell)\n"   # 0 ⇒ q2=1 impossible ⇒ q2 pinned to 0
         "r\n",
         "r : Int = 0"),
        # v4.62 (Strategy & Worlds): the Prisoner's Dilemma tragedy —
        # (Cooperate,Cooperate)=(3,3) Pareto-dominates the forced
        # equilibrium (Defect,Defect)=(1,1): both better off, yet
        # dominance forces the worse outcome.
        ("Prisoner's Dilemma: equilibrium is Pareto-dominated (v4.62)",
         "fn pareto_dom(a1: Int, a2: Int, b1: Int, b2: Int) : Bool =\n"
         "  a1 >= b1 && a2 >= b2 && (a1 > b1 || a2 > b2)\n"
         "let r : Bool = pareto_dom(3, 3, 1, 1)\n"
         "r\n",
         "r : Bool = true"),
        # v4.62: multi-world branching. Three coin flips multiply into
        # 2³ = 8 worlds (the list-monad bind unions every branch); the
        # head-counts form the binomial row 1,3,3,1.
        ("multi-world branching: 3 flips = 8 worlds (v4.62)",
         "type World = | World(List<Int>)\n"
         "fn wof(w: World) : List<Int> = match w { World(xs) => xs }\n"
         "fn pure(x: Int) : World = World([x])\n"
         "fn wbind(w: World, f: (Int) -> World) : World =\n"
         "  World(fold(wof(w), [], fn(acc: List<Int>, x: Int) ->"
         " acc ++ wof(f(x))))\n"
         "let flip = World([0, 1])\n"
         "let three = wbind(flip, fn(a: Int) ->"
         " wbind(flip, fn(b: Int) -> wbind(flip, fn(c: Int) ->"
         " pure(a + b + c))))\n"
         "let r : Int = len(wof(three))\n"
         "r\n",
         "r : Int = 8"),
        # v4.63 (Rationals & Probability): exact fraction arithmetic.
        # 1/3 + 1/6 reduces to exactly 1/2 — no rounding. The result is
        # gcd-normalized, so num=1, den=2; we pin the numerator.
        ("exact rational 1/3 + 1/6 = 1/2 (v4.63)",
         "type Rat = | Rat(Int, Int)\n"
         "fn gcd(a: Int, b: Int) : Int = if b == 0 then a else gcd(b, a % b)\n"
         "fn rat(n: Int, d: Int) : Int = n / gcd(n, d)\n"  # numerator of reduced n/d
         "let total : Int = 1 * 6 + 1 * 3\n"   # 1/3 + 1/6 = (6+3)/18 = 9/18
         "let r : Int = rat(total, 18)\n"      # 9/18 → numerator 1
         "r\n",
         "r : Int = 1"),
        # v4.63: Gini/collision uncertainty is exact and rational. For a
        # fair coin [1/2,1/2]:  1 − (1/4 + 1/4) = 1/2. We compute it over
        # a common denominator (4): numerator of 1 − 2/4 = 2, over 4.
        ("Gini uncertainty of fair coin = 1/2 (v4.63)",
         "let sum_sq_num : Int = 1 + 1\n"   # (1/2)²+(1/2)² = 1/4+1/4 = 2/4
         "let u_num : Int = 4 - sum_sq_num\n"   # 1 − 2/4 = (4-2)/4 = 2/4 = 1/2
         "u_num\n",
         "u_num : Int = 2"),
        # v4.64 (Time & Causality): the do-operator. Intervening
        # do(rain := false) recomputes wet = rain ∨ sprinkler from the
        # structural equation — with sprinkler off, the grass is dry.
        # This is intervention, not observation: the equation re-runs.
        ("counterfactual intervention dries the grass (v4.64)",
         "fn wet(rain: Bool, sprinkler: Bool) : Bool = rain || sprinkler\n"
         "let actual : Bool = wet(true, false)\n"    # actually wet
         "let cf : Bool = wet(false, false)\n"       # do(rain:=false)
         "let r : Bool = actual && !cf\n"            # was wet, would be dry
         "r\n",
         "r : Bool = true"),
        # v4.64: Ship of Theseus. After replacing all 4 planks, the
        # original [1,2,3,4] and final [5,6,7,8] differ in every
        # position — diff_count = 4, so strictly NOT the same (yet each
        # step changed only one plank: continuous).
        ("Ship of Theseus shares no original part (v4.64)",
         "fn diff(a: List<Int>, b: List<Int>) : Int =\n"
         "  match a { [] => 0; [x, ...xs] => match b { [] => 0;"
         " [y, ...ys] => (if x == y then 0 else 1) + diff(xs, ys) } }\n"
         "let r : Int = diff([1, 2, 3, 4], [5, 6, 7, 8])\n"
         "r\n",
         "r : Int = 4"),
        # v4.65 (Information & Observation): nested simulation depth.
        # Sim(Sim(Add(3, Sim(4)))) is three realities deep, while the
        # value (7) is level-independent.
        ("nested simulation depth (v4.65)",
         "type Expr = | Lit(Int) | Add(Expr, Expr) | Sim(Expr)\n"
         "fn depth(e: Expr) : Int =\n"
         "  match e { Lit(_) => 0;"
         " Add(a, b) => let da = depth(a) in let db = depth(b) in"
         " (if da > db then da else db);"
         " Sim(inner) => 1 + depth(inner) }\n"
         "let r : Int = depth(Sim(Sim(Add(Lit(3), Sim(Lit(4))))))\n"
         "r\n",
         "r : Int = 3"),
        # v4.65: information-flow taint. Joining a public value with a
        # secret one yields secret (Secret dominates the lattice), so
        # the result is NOT publishable — non-interference by the join.
        ("info-flow taint blocks publish (v4.65)",
         "type Label = | Public | Secret\n"
         "fn join(a: Label, b: Label) : Bool =\n"   # returns is_public of join
         "  match a { Secret => false;"
         " Public => match b { Public => true; Secret => false } }\n"
         "let publishable : Bool = join(Public, Secret)\n"
         "publishable\n",
         "publishable : Bool = false"),
        # v4.66 (Physical types): dimensional analysis. distance/time
        # subtracts dimension vectors, so (1,0,0) ÷ (0,1,0) = (1,−1,0),
        # a velocity. We pin the time exponent of the result = −1.
        ("dimensional division yields velocity (v4.66)",
         "type Dim = | Dim(Int, Int, Int)\n"
         "fn dsub(a: Dim, b: Dim) : Dim =\n"
         "  match a { Dim(l1, t1, m1) => match b { Dim(l2, t2, m2) =>"
         " Dim(l1 - l2, t1 - t2, m1 - m2) } }\n"
         "fn time_exp(d: Dim) : Int = match d { Dim(_, t, _) => t }\n"
         "let v : Dim = dsub(Dim(1, 0, 0), Dim(0, 1, 0))\n"
         "let r : Int = time_exp(v)\n"
         "r\n",
         "r : Int = -1"),
        # v4.67 (Tier-3): linear types. A `let lin` resource consumed
        # exactly once type-checks and runs. Path-aware: using it once
        # in each if-branch is one use per execution path.
        ("linear resource used once (v4.67)",
         "fn f(b: Bool) : Int =\n"
         "  let lin x = 5 in if b then x + 1 else x + 2\n"
         "let r : Int = f(true)\n"
         "r\n",
         "r : Int = 6"),
        # v4.67: `lin` is a CONTEXTUAL keyword — a variable literally
        # named `lin` still works (it's only special as `let lin <id>`).
        ("lin is a usable identifier (v4.67)",
         "fn f() : Int = let lin = 7 in lin + 1\n"
         "let r : Int = f()\n"
         "r\n",
         "r : Int = 8"),
        # v4.69: field-level refinement. A constructor field carries its
        # own invariant; Pos(5) packs fine, and the value is positive by
        # construction so pos_value just reads it back.
        ("refined ADT field accepts valid value (v4.69)",
         "type Pos = | Pos(n: Int where (n > 0))\n"
         "fn pos_value(x: Pos) : Int = match x { Pos(n) => n }\n"
         "let r : Int = pos_value(Pos(42))\n"
         "r\n",
         "r : Int = 42"),
        # v4.69: cross-FIELD refinement — `hi` references earlier field
        # `lo`. Range(3,10) is well-formed; span is 7.
        ("cross-field refinement accepts ordered range (v4.69)",
         "type Range = | Range(lo: Int, hi: Int where (hi > lo))\n"
         "fn span(r: Range) : Int = match r { Range(lo, hi) => hi - lo }\n"
         "let r : Int = span(Range(3, 10))\n"
         "r\n",
         "r : Int = 7"),
        ("list spread: leading + trailing (...a ++ ...b)",
         "let a : List<Int> = [1, 2]\n"
         "let b : List<Int> = [3, 4]\n"
         "let r : List<Int> = [...a, ...b]\n"
         "r\n",
         "r : List<Int> = [1, 2, 3, 4]"),
        ("list spread: middle element (...a, x, ...b)",
         "let a : List<Int> = [1, 2]\n"
         "let b : List<Int> = [4, 5]\n"
         "let r : List<Int> = [...a, 3, ...b]\n"
         "r\n",
         "r : List<Int> = [1, 2, 3, 4, 5]"),
        ("list spread: tail form (a, ...b)",
         "let b : List<Int> = [2, 3]\n"
         "let r : List<Int> = [1, ...b]\n"
         "r\n",
         "r : List<Int> = [1, 2, 3]"),
    ]
    for label, src, needle in inline_positive:
        rc, out, err = run(src)
        ok = (rc == 0) and (needle in out)
        print(f"  {'OK ' if ok else 'FAIL'}  {label}")
        if not ok:
            print(f"        expected substring {needle!r}")
            print(f"        rc={rc}, stdout: {out.strip()[-200:]}")
            print(f"        stderr: {err.strip()[-200:]}")
            failures += 1

    print("== prism runtime-check end-to-end (v4.23) ==")
    # Run prism.glass and confirm BOTH the positive and negative
    # refinement runtime-check demo lines surface in stdout. This is the
    # only test that exercises prism's own check_refine_runtime — the
    # host-level inline test above pins down the SHAPE of the message;
    # this one pins down that prism's port produces it.
    prism_rc, prism_out, prism_err = run_file(
        os.path.join(EX, "selfhost", "prism.glass")
    )
    prism_checks = [
        ("prism runtime check accepts (v4.23)",
         "examples/features/runtime_refine.glass ==> 42 : Int"),
        ("prism runtime check rejects (v4.23)",
         "examples/features/runtime_refine_bad.glass ==> "
         "refinement violated at runtime: n = 0 fails predicate"),
        # v4.24: refinement on the SECOND param of a curried top-level fn.
        # Pre-v4.24 prism silently let bad values through here because the
        # check only fired on the first param. The VRefinedClos wrapper
        # carries the remaining formals past the first apply so subsequent
        # applies still see their refinements.
        ("prism general list spread (self-host parity)",
         "examples/features/spread_general.glass ==> "
         "[0, 1, 2, 3, 4, 5, 1, 2, 4, 5] : List<Int>"),
        ("prism curried-refine accepts (v4.24)",
         "examples/features/curried_refine.glass ==> 15 : Int"),
        ("prism curried-refine rejects (v4.24)",
         "examples/features/curried_refine_bad.glass ==> "
         "refinement violated at runtime: b = 0 fails predicate"),
        # v4.25: prism return-type refinement runtime check end-to-end.
        # Positive case prints the tuple; negative case prints the
        # violation message for `result = -4`.
        ("prism return-refine accepts (v4.25)",
         "examples/features/return_refine.glass ==> (7, 7) : (Int, Int)"),
        ("prism return-refine rejects (v4.25)",
         "examples/features/return_refine_bad.glass ==> "
         "refinement violated at runtime: result = -4 fails predicate"),
        # v4.26: prism's lexer/parser/eval gain `/`. Textbook
        # safe_div(a, b: Int where (b != 0)) now runs end-to-end in
        # prism; the runtime refinement check carries the divide-by-zero
        # invariant.
        ("prism safe_div with division (v4.26)",
         "examples/features/safe_div.glass ==> (25, 20) : (Int, Int)"),
        # v4.27: parens-after-let parser fix in prism. Bare `(r1, r2)`
        # at column 1 after `let r2 = ...` used to be chained as a call;
        # now it parses as a separate top-level tuple expression.
        ("prism parens-after-let split (v4.27)",
         "examples/features/parens_after_let.glass ==> (3, 7) : (Int, Int)"),
        # v4.47: refined-param lambda runtime checks. The parser now
        # accepts `where (pred)` after a lambda's typed param, and the
        # ELamR -> VRefinedClos path enforces the predicate on every
        # apply. Positive case returns 10; negative case prints the
        # standard "refinement violated at runtime" message via the
        # demo loop.
        ("prism lambda-refine accepts (v4.47)",
         "examples/features/lambda_refine.glass ==> 10 : Int"),
        ("prism lambda-refine rejects (v4.47)",
         "examples/features/lambda_refine_bad.glass ==> "
         "refinement violated at runtime: x = -3 fails predicate"),
        # v4.48: multi-parameter lambdas in prism. Pre-v4.48 the
        # parser bailed at the first comma in a lambda param list, so
        # `fn(a, b) -> ...` never reached eval. The new parse_fn
        # parses a comma-separated list and right-folds it into a
        # nested ELam/ELamR chain — same shape as the host's curried
        # top-level fn encoding.
        ("prism multi-arg lambda (v4.48)",
         "examples/features/lambda_multi.glass ==> 7 : Int"),
        # v4.48 composes with v4.47: each param's refinement runs at
        # its own apply step via the VRefinedClos wrapper from v4.24.
        # 3 > 0 and 4 > 0 both hold, so the call returns 12.
        ("prism multi-arg refined lambda (v4.48)",
         "examples/features/lambda_multi_refine.glass ==> 12 : Int"),
        # v4.52: `&&` and `||` end-to-end through prism. v4.51 deferred
        # prism's update; this is the closing case. Tokenizer recognizes
        # `&&` / `||`, parser layers parse_or → parse_and → parse_compare
        # with C-style precedence, infer rejects non-Bool operands, eval
        # short-circuits. The interval refinement holds (50 in (0,100))
        # so middling returns 51.
        ("prism && / || end-to-end via interval refinement (v4.52)",
         "examples/features/and_or.glass ==> 51 : Int"),
        # v4.53: modulo end-to-end through prism. TPercent token,
        # EMod variant, parse_mul_rest arm, infer/eval/eval_pred/
        # alpha/equal arms — five sites mirroring EMul/EDiv. Parity
        # refinement `n % 2 == 0` is the canonical divisibility shape.
        # 10 is even, so even_only(10) returns 11.
        ("prism modulo end-to-end via parity refinement (v4.53)",
         "examples/features/mod_refine.glass ==> 11 : Int"),
        # v4.54: unary NOT end-to-end through prism. New parse_unary
        # layer above parse_mul, EUNot variant, infer/eval/eval_pred/
        # alpha/equal arms. `!(n == 0)` refinement holds for 5, so
        # nonzero(5) = 100 / 5 = 20.
        ("prism unary NOT end-to-end via refinement (v4.54)",
         "examples/features/not_refine.glass ==> 20 : Int"),
        # v4.68: linear types ported to prism — prism self-hosts the
        # path-aware exactly-once check. A resource used once compiles;
        # a clone is rejected at parse time. Glass checking Glass's own
        # substructural discipline.
        ("prism linear resource accepts single use (v4.68)",
         "examples/features/linear_ok.glass ==> 50 : Int"),
        ("prism linear resource rejects cloning (v4.68)",
         "examples/features/linear_clone.glass ==> "
         "linear variable token used 2 times (no cloning)"),
        # v4.56: cross-parameter refinement through prism. The arg-env
        # threaded through VRefinedClos lets `hi > lo` resolve `lo`.
        # clamp(3, 10) = 7.
        ("prism cross-param refinement accepts (v4.56)",
         "examples/features/xparam_refine.glass ==> 7 : Int"),
        # And the bad case fires LOUDLY (not the pre-v4.56 silent skip
        # on unbound `lo`): clamp(10, 3) violates hi > lo.
        ("prism cross-param refinement rejects (v4.56)",
         "examples/features/xparam_refine_bad.glass ==> "
         "refinement violated at runtime: hi = 3 fails predicate"),
    ]
    for label, needle in prism_checks:
        ok = (prism_rc == 0) and (needle in prism_out)
        print(f"  {'OK ' if ok else 'FAIL'}  {label}")
        if not ok:
            print(f"        expected substring {needle!r}")
            print(f"        rc={prism_rc}")
            print(f"        stdout tail: {prism_out.strip()[-300:]}")
            print(f"        stderr tail: {prism_err.strip()[-300:]}")
            failures += 1

    print("== REPL session cases ==")
    repl_cases = [
        ("simple expression",
         "1 + 1\n:quit\n", ": Int = 2"),
        ("let binding then use",
         "let x = 42\nx + 1\n:quit\n", ": Int = 43"),
        ("multi-line fn definition",
         "fn fact(n: Int) : Int =\n"
         "  if n < 2 then 1\n"
         "  else n * fact(n - 1)\n"
         "fact(5)\n:quit\n", ": Int = 120"),
        (":type command",
         ":type 42 + 1\n:quit\n", "42 + 1 : Int"),
        ("error recovery",
         "undefined_x\n1 + 1\n:quit\n", ": Int = 2"),
        (":reset clears state",
         "let x = 5\n:reset\nx\n:quit\n", "unbound"),
    ]
    for label, src, needle in repl_cases:
        p = subprocess.run(
            [sys.executable, GLASS],
            input=src, capture_output=True, text=True,
        )
        ok = (needle in p.stdout)
        print(f"  {'OK ' if ok else 'FAIL'}  {label}")
        if not ok:
            print(f"        expected substring {needle!r}")
            print(f"        stdout: {p.stdout.strip()[-200:]}")
            failures += 1

    print("== statement-binding guard ==")
    # The FS transcript digest MUST depend on the statement (a different claimed
    # R or reordered gates -> a different seed). Pin it so the binding can never
    # silently regress to a no-op — the exact failure mode of the v5.46.1
    # grinding bug, which lived in an untested path. Digest-only, interpreter, ~secs.
    rc, out, err = run_file(os.path.join(EX, "prove", "prove_source_goldilocks_bind_test.glass"))
    bind_ok = (rc == 0) and ("BIND-GUARD PASS" in out)
    print(f"  {'OK ' if bind_ok else 'FAIL'}  FS digest binds circuit + claimed R")
    if not bind_ok:
        print(f"        rc={rc}; expected 'BIND-GUARD PASS' in stdout")
        if err.strip():
            print(f"        stderr: {err.strip()[-200:]}")
        failures += 1

    print("== baby-bear prove guard ==")
    # The baby-bear prove bridge (prove_source_adt_zk.glass) is an
    # interpreter-only path the POSITIVE list and the bootstrap fixpoint don't
    # exercise — so a v5.55.0 exhaustiveness tightening silently broke it (a
    # match on the imported 2-constructor TypeDecl handled only one ctor and
    # was no longer accepted as total). Pin an end-to-end ACCEPT so the bridge
    # stays type-checkable and sound. ~seconds, interpreter, --fast self-check.
    import tempfile
    with tempfile.NamedTemporaryFile("w", suffix=".glass", delete=False) as _tf:
        _tf.write("fn f(a: Int) : Int = a * a + 1\nf(inp)\n")
        _bb_path = _tf.name
    _bb = subprocess.run(
        [sys.executable, GLASS, "prove", "--baby-bear", "--fast", _bb_path, "inp=5"],
        capture_output=True, text=True,
    )
    os.unlink(_bb_path)
    bb_ok = (_bb.returncode == 0) and ("ACCEPT" in _bb.stdout) and ("26" in _bb.stdout)
    print(f"  {'OK ' if bb_ok else 'FAIL'}  baby-bear prove f(5)=26 ACCEPT (bridge exhaustiveness/soundness)")
    if not bb_ok:
        print(f"        rc={_bb.returncode}; expected ACCEPT + result 26")
        if _bb.stderr.strip():
            print(f"        stderr: {_bb.stderr.strip()[-200:]}")
        failures += 1

    # The baby-bear bridge lowered every UNSUPPORTED operator (comparisons,
    # / %, strings, records) to a SILENT 0 — so `glass prove --baby-bear` on
    # `a < b` certified `result: 0 ACCEPT`, a FALSE statement with a valid
    # proof (the silent-wrong-certification class). It must now REFUSE loudly,
    # never silently prove a wrong value. (The default Goldilocks path already
    # refused comparisons since v5.52; this brings the toy path to parity.)
    with tempfile.NamedTemporaryFile("w", suffix=".glass", delete=False) as _tf:
        _tf.write("fn lt(a: Int, b: Int) : Bool = a < b\nlt(a, b)\n")
        _cmp_path = _tf.name
    _cmp = subprocess.run(
        [sys.executable, GLASS, "prove", "--baby-bear", "--fast", _cmp_path, "a=3", "b=5"],
        capture_output=True, text=True,
    )
    os.unlink(_cmp_path)
    cmp_ok = (_cmp.returncode != 0) and ("ACCEPT" not in _cmp.stdout) and ("REFUSED" in _cmp.stderr)
    print(f"  {'OK ' if cmp_ok else 'FAIL'}  baby-bear refuses comparisons (no silent wrong-cert)")
    if not cmp_ok:
        print(f"        rc={_cmp.returncode}; expected nonzero + REFUSED, no ACCEPT")
        print(f"        stdout: {_cmp.stdout.strip()[-150:]}  stderr: {_cmp.stderr.strip()[-150:]}")
        failures += 1

    # Heavy Goldilocks native proves: all 3 gates now RUN to completion on the GitHub runner (and macOS,
    # and a linux/amd64 container) — confirmed 426/426 with real ACCEPT/REJECT verdicts. The Linux
    # blockers were cleared in sequence: quartz GC compile (v5.91, no >7.6GB malloc-leak OOM), 512MB run
    # stack (v5.92, no deep-recursion SIGSEGV), and v5.93's run_native.sh `grep -m1` fix — the last one
    # was the runner-specific cause: run_native inlined prism via `grep|head -1`, and on hosts that
    # IGNORE SIGPIPE (GitHub runners) head closing the pipe made grep fail EPIPE (exit 2) under
    # `pipefail`+`set -e`, aborting run_native BEFORE the compile (rc=2, no binary) → the gate skipped.
    # _heavy_skipped() now stands only as a FALLBACK: a future resource-starved env that signal-kills a
    # heavy prove (rc>=128) skips that one gate (CI green) while a real logic regression (rc<128) still
    # produces a verdict and is evaluated normally. See reference_build_portability memory.
    def _heavy_skipped(proc, label):
        if proc.returncode >= 128:
            print(f"  OK   {label}  (SKIPPED: native heavy-prove killed by signal rc={proc.returncode} — env-limited)")
            return True
        return False

    # Dead-branch PREDICATION (v5.88): cgen builds BOTH if-arms, so a divide-by-zero in a DEAD arm
    # (`if a==a then a else a%b`, b=0) used to poison the circuit. The division gadget now predicates
    # its `r < b` check on an in-circuit `b!=0` bit, so the dead `a%0` is vacuously satisfiable and the
    # live result PROVES — `result: 7, ACCEPT` (was ABSTAIN). Goldilocks native path (~15s).
    _db_path = os.path.join(EX, "prove", "deadbranch_div.glass")
    _db = _prove_run([sys.executable, GLASS, "prove", _db_path, "a=7", "b=0"],
                         capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_db, "dead-branch predication: dead a%0 proves the live result (7, ACCEPT)"):
        db_ok = (_db.returncode == 0) and ("ACCEPT" in _db.stdout) and ("result:  7" in _db.stdout)
        print(f"  {'OK ' if db_ok else 'FAIL'}  dead-branch predication: dead a%0 proves the live result (7, ACCEPT)")
        if not db_ok:
            print(f"        rc={_db.returncode}  out: {_db.stdout.strip()[-150:]}  err: {_db.stderr.strip()[-150:]}")
            failures += 1
    # Soundness companion: a LIVE divide-by-zero (b=0 on the TAKEN path) must STILL ABSTAIN — the
    # predication only relaxes DEAD arms; seval short-circuits to the taken path and refuses b==0.
    with tempfile.NamedTemporaryFile("w", suffix=".glass", delete=False) as _lf:
        _lf.write("a % b\n"); _live_path = _lf.name
    _lv = _prove_run([sys.executable, GLASS, "prove", _live_path, "a=7", "b=0"],
                         capture_output=True, text=True, cwd=ROOT)
    os.unlink(_live_path)
    lv_ok = (_lv.returncode != 0) and ("ABSTAIN" in (_lv.stdout + _lv.stderr)) and ("ACCEPT" not in _lv.stdout)
    print(f"  {'OK ' if lv_ok else 'FAIL'}  live divide-by-zero still ABSTAINs (predication relaxes only dead arms)")
    if not lv_ok:
        print(f"        rc={_lv.returncode}  out: {_lv.stdout.strip()[-150:]}  err: {_lv.stderr.strip()[-150:]}")
        failures += 1
    # WRONG-CLAIM REJECT for the divmod path (v5.89, audit-recommended): the v5.88 soundness rests on
    # the proven R being the circuit's OWN divmod output (build_claim_m pins output==claimedR). This
    # proves a FALSE division claim is REJECTed: `a/b` with a=17,b=5 claiming 4 (true is 3) -> verify_b3
    # REJECT — the prover cannot forge a verifying proof of a wrong quotient. (Goldilocks native, ~55s.)
    with tempfile.NamedTemporaryFile("w", suffix=".glass", delete=False) as _wf:
        _wf.write("a / b\n"); _wc_path = _wf.name
    _wc = _prove_run([sys.executable, GLASS, "prove", "--claim", "4", _wc_path, "a=17", "b=5"],
                         capture_output=True, text=True, cwd=ROOT)
    os.unlink(_wc_path)
    if not _heavy_skipped(_wc, "wrong divmod claim REJECTs (claim 17/5=4; true is 3 — no proof of a false quotient)"):
        # v5.133 exit-code contract: a REJECT exits 2 (0=ACCEPT, 1=ABSTAIN, 2=REJECT, 3=DIVERGENCE),
        # so scripts can branch on the verdict without parsing — pinned here on the REJECT path.
        wc_ok = ("proof:   REJECT" in _wc.stdout) and ("proof:   ACCEPT" not in _wc.stdout) and (_wc.returncode == 2)
        print(f"  {'OK ' if wc_ok else 'FAIL'}  wrong divmod claim REJECTs (claim 17/5=4; true is 3 — no proof of a false quotient)")
        if not wc_ok:
            print(f"        rc={_wc.returncode}  out: {_wc.stdout.strip()[-200:]}  err: {_wc.stderr.strip()[-150:]}")
            failures += 1

    # FORGED-PROVER divmod soundness (v5.131, the forgery-resistance audit's one finding): in the
    # b==0 sub-circuit (a dead-branch divide-by-zero) the quotient q is ADVICE. Before v5.131 it was
    # a FREE [0,2^32) value — a malicious prover binary hinting q=7 produced an internally-consistent
    # witness (identity a == 0*7 + r holds with r=a; the range bits decompose 7) that verify_b3
    # ACCEPTed (verified on the pre-fix bridge), exactly the freedom an a/0 forgery would ride on any
    # future path where the b==0 quotient goes live. The isz*q == 0 pin makes the b==0 witness UNIQUE
    # (q=0, r=a). This gate IS that malicious prover: a copy of the bridge with the q-hint forged to 7
    # (GLASS_BRIDGE_DIR points the CLI at it); every downstream wire recomputes consistently, so the
    # ONLY violated constraint is the pin — the proof must REJECT. (Goldilocks native, ~15s.)
    import shutil as _sh_fg
    _fg_line = "let qi : Int = if bi <= 0 then 0 else ai / bi"
    with open(os.path.join(EX, "prove", "prove_source_goldilocks_zk.glass")) as _bf:
        _bridge_src = _bf.read()
    if _fg_line not in _bridge_src:
        print("  FAIL  forged prover (q-hint=7 in the b==0 sub-circuit) REJECTs — the q-hint line moved in the bridge; update this gate")
        failures += 1
    else:
        _fg_dir = tempfile.mkdtemp()
        try:
            with open(os.path.join(_fg_dir, "prove_source_goldilocks_zk.glass"), "w") as _ff:
                _ff.write(_bridge_src.replace(_fg_line, _fg_line.replace("then 0", "then 7")))
            _fenv = dict(os.environ); _fenv["GLASS_BRIDGE_DIR"] = _fg_dir
            _fg = _prove_run([sys.executable, GLASS, "prove", _db_path, "a=7", "b=0"],
                             capture_output=True, text=True, cwd=ROOT, env=_fenv)
            if not _heavy_skipped(_fg, "forged prover (q-hint=7 in the b==0 sub-circuit) REJECTs — divmod advice is PINNED, not free"):
                fg_ok = ("proof:   REJECT" in _fg.stdout) and ("proof:   ACCEPT" not in _fg.stdout)
                print(f"  {'OK ' if fg_ok else 'FAIL'}  forged prover (q-hint=7 in the b==0 sub-circuit) REJECTs — divmod advice is PINNED, not free")
                if not fg_ok:
                    print(f"        rc={_fg.returncode}  out: {_fg.stdout.strip()[-200:]}  err: {_fg.stderr.strip()[-150:]}")
                    failures += 1
        finally:
            _sh_fg.rmtree(_fg_dir, ignore_errors=True)

    # CAPTURE-AVOIDING INLINING (v5.132): inline_fn used to bind call arguments as a sequential ELet
    # nest, so an argument referencing an EARLIER parameter's NAME was captured by the just-bound
    # parameter — `gcd(b, a % b)` computed b % b, and the circuit attested gcd(48,18)=18 while the
    # source computes 6 (a STARK-valid wrong lowering, caught ONLY by the Third Witness). The minimal
    # shape: top(a,b) calls g(b, a-b) — the `a` in `a-b` must be the CALLER's a (10), not the bound
    # first parameter (3). Truth: g(3, 7) = 307; the captured lowering proved 300. (~30s native.)
    with tempfile.NamedTemporaryFile("w", suffix=".glass", delete=False) as _cpf:
        _cpf.write("fn g(a: Int, b: Int) : Int = a * 100 + b\n"
                   "fn top(a: Int, b: Int) : Int = g(b, a - b)\n\ntop(x, y)\n")
        _cp_path = _cpf.name
    _cp = _prove_run([sys.executable, GLASS, "prove", "--cross-check", _cp_path, "x=10", "y=3"],
                     capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_cp, "capture-avoiding inlining: g(b, a-b) binds the CALLER's a (307, Third Witness AGREES)"):
        cp_ok = (_cp.returncode == 0) and ("result:  307" in _cp.stdout) and ("THIRD LINEAGE AGREES" in _cp.stdout)
        print(f"  {'OK ' if cp_ok else 'FAIL'}  capture-avoiding inlining: g(b, a-b) binds the CALLER's a (307, Third Witness AGREES)")
        if not cp_ok:
            print(f"        rc={_cp.returncode}  out: {_cp.stdout.strip()[-200:]}  err: {_cp.stderr.strip()[-150:]}")
            failures += 1

    # ...and the COUNTERFACTUAL + the loud Third Witness (v5.132): a bridge copy with tmpn regressed
    # to the identity reproduces the OLD capturing lowering exactly (the param "temp" aliases itself),
    # so the same program proves the WRONG 300 and the Third Witness must flag DIVERGENCE — and a
    # detected divergence is now a HARD FAILURE: `glass prove --cross-check` exits 3, not 0. This gate
    # pins both: the divergence detection and its exit code. (~30s native.)
    _cl_old = 'fn tmpn(p: String) : String = "q9p_" ++ p'
    with open(os.path.join(EX, "prove", "prove_source_goldilocks_zk.glass")) as _bf2:
        _bridge_src2 = _bf2.read()
    if _cl_old not in _bridge_src2:
        print("  FAIL  regressed-capture bridge DIVERGEs with exit code 3 — tmpn moved in the bridge; update this gate")
        failures += 1
    else:
        _cl_dir = tempfile.mkdtemp()
        try:
            with open(os.path.join(_cl_dir, "prove_source_goldilocks_zk.glass"), "w") as _cf:
                _cf.write(_bridge_src2.replace(_cl_old, "fn tmpn(p: String) : String = p"))
            _clenv = dict(os.environ); _clenv["GLASS_BRIDGE_DIR"] = _cl_dir
            _cl = _prove_run([sys.executable, GLASS, "prove", "--cross-check", _cp_path, "x=10", "y=3"],
                             capture_output=True, text=True, cwd=ROOT, env=_clenv)
            if not _heavy_skipped(_cl, "regressed-capture bridge: Third Witness flags DIVERGENCE and exits 3 (a divergence is loud)"):
                cl_ok = (_cl.returncode == 3) and ("DIVERGENCE" in _cl.stdout) and ("THIRD LINEAGE AGREES" not in _cl.stdout)
                print(f"  {'OK ' if cl_ok else 'FAIL'}  regressed-capture bridge: Third Witness flags DIVERGENCE and exits 3 (a divergence is loud)")
                if not cl_ok:
                    print(f"        rc={_cl.returncode}  out: {_cl.stdout.strip()[-200:]}  err: {_cl.stderr.strip()[-150:]}")
                    failures += 1
        finally:
            _sh_fg.rmtree(_cl_dir, ignore_errors=True)
    os.unlink(_cp_path)

    # Higher-order proving (v5.87): the seval guard resolves function-valued parameters via fenv
    # (mirroring unroll), so a higher-order program — `map(inc, xs)` — is GUARDED and PROVEN instead
    # of spuriously refused (it ABSTAINed before, because seval couldn't resolve the `f` callee that
    # unroll+cgen handle). Goldilocks native path (~30s); proves the result and ACCEPTs.
    _ho_path = os.path.join(EX, "prove", "map_prove.glass")
    _ho = _prove_run([sys.executable, GLASS, "prove", _ho_path, "inp=5"],
                         capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_ho, "higher-order proving: map(inc, [5,2,3]) sum = 13 ACCEPT (no spurious refusal)"):
        ho_ok = (_ho.returncode == 0) and ("ACCEPT" in _ho.stdout) and ("result:  13" in _ho.stdout)
        print(f"  {'OK ' if ho_ok else 'FAIL'}  higher-order proving: map(inc, [5,2,3]) sum = 13 ACCEPT (no spurious refusal)")
        if not ho_ok:
            print(f"        rc={_ho.returncode}  out: {_ho.stdout.strip()[-200:]}  err: {_ho.stderr.strip()[-150:]}")
            failures += 1

    # Signed comparison (v5.94): slt/sle/sgt/sge prove ordering over SIGNED integers in
    # [-2^31, 2^31) — negatives included. They desugar to the existing unsigned range gadget
    # via a monotonic +2^31 offset (no new gate, no verifier change), and a negative input is
    # now bound CANONICALLY (gin: p-|v|, not the non-canonical two's-complement limbs glit4(-5)
    # would give). slt(-5, 3) -> result 1, ACCEPT. Goldilocks native path (~30s).
    _sc_path = os.path.join(EX, "prove", "signed_cmp.glass")
    _sc = _prove_run([sys.executable, GLASS, "prove", _sc_path, "a=-5", "b=3"],
                         capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_sc, "signed comparison: slt(-5, 3) = 1 ACCEPT (negatives, canonical binding)"):
        sc_ok = (_sc.returncode == 0) and ("ACCEPT" in _sc.stdout) and ("result:  1" in _sc.stdout)
        print(f"  {'OK ' if sc_ok else 'FAIL'}  signed comparison: slt(-5, 3) = 1 ACCEPT (negatives, canonical binding)")
        if not sc_ok:
            print(f"        rc={_sc.returncode}  out: {_sc.stdout.strip()[-200:]}  err: {_sc.stderr.strip()[-150:]}")
            failures += 1

    # ...and a FALSE signed-comparison claim must REJECT: slt(-5, 3) is 1 (true), so claiming 0
    # is unsatisfiable — the independent verify_b3 proves no false signed ordering. Goldilocks native.
    _scf = _prove_run([sys.executable, GLASS, "prove", _sc_path, "a=-5", "b=3", "--claim", "0"],
                          capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_scf, "wrong signed-comparison claim REJECTs (slt(-5,3)=1; claim 0 is false)"):
        scf_ok = ("proof:   REJECT" in _scf.stdout) and ("proof:   ACCEPT" not in _scf.stdout)
        print(f"  {'OK ' if scf_ok else 'FAIL'}  wrong signed-comparison claim REJECTs (slt(-5,3)=1; claim 0 is false)")
        if not scf_ok:
            print(f"        rc={_scf.returncode}  out: {_scf.stdout.strip()[-200:]}  err: {_scf.stderr.strip()[-150:]}")
            failures += 1

    # Signed band membership (v5.95): the ZK range-membership pattern — prove a private value t is
    # within a signed band [-40, 125] without revealing it. Exercises a compound `sge(t,-40) && sle(t,125)`
    # AND the canonical NEGATIVE-LITERAL lowering fixed in v5.95 (a `-40` literal previously lowered via
    # the non-canonical glit(-40)=[-40] to a WRONG comparison — sge(20,-40) proved 0 instead of 1, a
    # silent wrong result the Third Witness flagged as a source<->circuit DIVERGENCE). Now EInt(n<0) binds
    # canonically (gin), so the band proves the right verdict. t=20 is in band -> result 1 ACCEPT; if the
    # negative-literal fix regressed, sge(20,-40) would be 0 and this gate would see result 0. Goldilocks native.
    _sb_path = os.path.join(EX, "prove", "signed_band.glass")
    _sb = _prove_run([sys.executable, GLASS, "prove", _sb_path, "t=20"],
                         capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_sb, "signed band: -40 <= 20 <= 125 proves 1 ACCEPT (negative literal lowers canonically)"):
        sb_ok = (_sb.returncode == 0) and ("ACCEPT" in _sb.stdout) and ("result:  1" in _sb.stdout)
        print(f"  {'OK ' if sb_ok else 'FAIL'}  signed band: -40 <= 20 <= 125 proves 1 ACCEPT (negative literal lowers canonically)")
        if not sb_ok:
            print(f"        rc={_sb.returncode}  out: {_sb.stdout.strip()[-200:]}  err: {_sb.stderr.strip()[-150:]}")
            failures += 1

    # Signed division/modulo (v5.96): sdiv/smod prove C99 truncated division (q toward zero, r with
    # the dividend's sign) over signed [-2^31, 2^31). The +2^31 offset that makes signed COMPARISON
    # free does NOT compose for division, so sdiv/smod are built by SIGN-MAGNITUDE — but soundly, by
    # composing already-lowered primitives (slt for the proven canonical sign, if/then/else for
    # magnitude+post-negate, the unsigned divmod_build core), NOT a sign-bit gadget (an adversarial
    # design failed exactly there; the Third Witness catches such a wrong lowering). The result is the
    # canonical field element p-|r| for negatives; --cross-check confirms the signed value. Goldilocks
    # native (~2x divmod). ACCEPT: sdiv(-17,5) = -3 with witness3 AGREEing on the signed -3.
    _sd_path = os.path.join(EX, "prove", "signed_div.glass")
    _sd = _prove_run([sys.executable, GLASS, "prove", _sd_path, "a=-17", "b=5", "--cross-check"],
                         capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_sd, "signed division: sdiv(-17,5) = -3 ACCEPT (C99 trunc; Third Witness confirms -3)"):
        sd_ok = (_sd.returncode == 0) and ("ACCEPT" in _sd.stdout) and ("result:  -3" in _sd.stdout) and ("f(inputs) = -3" in _sd.stdout) and ("DIVERGENCE" not in _sd.stdout)
        print(f"  {'OK ' if sd_ok else 'FAIL'}  signed division: sdiv(-17,5) = -3 ACCEPT (C99 trunc; Third Witness confirms -3)")
        if not sd_ok:
            print(f"        rc={_sd.returncode}  out: {_sd.stdout.strip()[-220:]}  err: {_sd.stderr.strip()[-150:]}")
            failures += 1

    # ...and a FALSE signed-division claim must REJECT: sdiv(-17,5) is -3 (canonical p-3); claiming 3
    # is unsatisfiable, so the independent verify_b3 REJECTs (no proof of a wrong signed quotient).
    _sdf = _prove_run([sys.executable, GLASS, "prove", _sd_path, "a=-17", "b=5", "--claim", "3"],
                          capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_sdf, "wrong signed-division claim REJECTs (sdiv(-17,5)=-3; claim 3 is false)"):
        sdf_ok = ("proof:   REJECT" in _sdf.stdout) and ("proof:   ACCEPT" not in _sdf.stdout)
        print(f"  {'OK ' if sdf_ok else 'FAIL'}  wrong signed-division claim REJECTs (sdiv(-17,5)=-3; claim 3 is false)")
        if not sdf_ok:
            print(f"        rc={_sdf.returncode}  out: {_sdf.stdout.strip()[-200:]}  err: {_sdf.stderr.strip()[-150:]}")
            failures += 1

    # Signed utility intrinsics (v5.100): sabs(x)=|x|, smin/smax — composed from the proven slt + if
    # (no new gadget). The zero-knowledge PRIVATE-DISTANCE pattern sabs(a-b): prove |a-b| between two
    # private values without revealing either. sabs(3-17) = 14, witness3-confirmed. Goldilocks native.
    _pd = _prove_run([sys.executable, GLASS, "prove", os.path.join(EX, "prove", "private_distance.glass"),
                          "a=3", "b=17", "--cross-check"], capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_pd, "private distance: sabs(3 - 17) = 14 ACCEPT (|a-b| without revealing a,b)"):
        pd_ok = (_pd.returncode == 0) and ("ACCEPT" in _pd.stdout) and ("result:  14" in _pd.stdout) and ("THIRD LINEAGE AGREES" in _pd.stdout)
        print(f"  {'OK ' if pd_ok else 'FAIL'}  private distance: sabs(3 - 17) = 14 ACCEPT (|a-b| without revealing a,b)")
        if not pd_ok:
            print(f"        rc={_pd.returncode}  out: {_pd.stdout.strip()[-220:]}  err: {_pd.stderr.strip()[-150:]}")
            failures += 1

    # Strings in zero-knowledge (v5.101): a string lowers as a MULTI-WIRE value — one codepoint
    # wire per character — reusing the ADT/tuple layout; `++` is structural concat, `==` the
    # per-codepoint is-zero gadget AND-folded, `substring` a static wire slice. No new gate type,
    # no verify_b3 change. The headline: a PRIVATE string predicate in ZK. Prove a private API key
    # has the public prefix "sk-live-" without revealing the key: substring(key,0,8)=="sk-live-"
    # -> 1 ACCEPT, and the Third Witness (glass.py, independent of the bridge) AGREES. Goldilocks native.
    _sp_path = os.path.join(EX, "prove", "private_prefix.glass")
    _sp = _prove_run([sys.executable, GLASS, "prove", _sp_path, 'key=sk-live-9f3a2c7e1b', "--cross-check"],
                         capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_sp, "strings in ZK: private key prefix substring(key,0,8)=='sk-live-' -> 1 ACCEPT (key hidden)"):
        sp_ok = (_sp.returncode == 0) and ("ACCEPT" in _sp.stdout) and ("result:  1" in _sp.stdout) and ("THIRD LINEAGE AGREES" in _sp.stdout)
        print(f"  {'OK ' if sp_ok else 'FAIL'}  strings in ZK: private key prefix substring(key,0,8)=='sk-live-' -> 1 ACCEPT (key hidden)")
        if not sp_ok:
            print(f"        rc={_sp.returncode}  out: {_sp.stdout.strip()[-220:]}  err: {_sp.stderr.strip()[-150:]}")
            failures += 1
    # Discrimination: a NON-matching prefix must prove 0 (not always-1) — the per-codepoint equality
    # actually compares. A test key -> result 0, ACCEPT, witness3 AGREES.
    _spt = _prove_run([sys.executable, GLASS, "prove", _sp_path, 'key=sk-test-0000000000', "--cross-check"],
                          capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_spt, "strings in ZK: non-matching prefix proves 0 (per-codepoint compare discriminates)"):
        spt_ok = (_spt.returncode == 0) and ("result:  0" in _spt.stdout) and ("THIRD LINEAGE AGREES" in _spt.stdout)
        print(f"  {'OK ' if spt_ok else 'FAIL'}  strings in ZK: non-matching prefix proves 0 (per-codepoint compare discriminates)")
        if not spt_ok:
            print(f"        rc={_spt.returncode}  out: {_spt.stdout.strip()[-220:]}  err: {_spt.stderr.strip()[-150:]}")
            failures += 1
    # Soundness: a FALSE string-predicate claim must REJECT. is_live(live key) is 1 (true), so
    # claiming 0 is unsatisfiable — the independent verify_b3 proves no false string predicate.
    _spf = _prove_run([sys.executable, GLASS, "prove", "--claim", "0", _sp_path, 'key=sk-live-9f3a2c7e1b'],
                          capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_spf, "strings in ZK: false string-predicate claim REJECTs (is_live=1; claim 0 is false)"):
        spf_ok = ("proof:   REJECT" in _spf.stdout) and ("proof:   ACCEPT" not in _spf.stdout)
        print(f"  {'OK ' if spf_ok else 'FAIL'}  strings in ZK: false string-predicate claim REJECTs (is_live=1; claim 0 is false)")
        if not spf_ok:
            print(f"        rc={_spf.returncode}  out: {_spf.stdout.strip()[-220:]}  err: {_spf.stderr.strip()[-150:]}")
            failures += 1
    # Computed-but-static substring bound + string_length: prove a PRIVATE email is at the org domain
    # without revealing it — substring(email, string_length(email)-14, string_length(email))=="@setonhill.edu"
    # -> 1 ACCEPT, witness3 AGREES (string_length is the build-time wire count; the slice offset folds to a constant).
    _se_path = os.path.join(EX, "prove", "private_email.glass")
    _se = _prove_run([sys.executable, GLASS, "prove", _se_path, 'email=ekhaklin@setonhill.edu', "--cross-check"],
                         capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_se, "strings in ZK: private email org-domain suffix -> 1 ACCEPT (string_length + substring)"):
        se_ok = (_se.returncode == 0) and ("ACCEPT" in _se.stdout) and ("result:  1" in _se.stdout) and ("THIRD LINEAGE AGREES" in _se.stdout)
        print(f"  {'OK ' if se_ok else 'FAIL'}  strings in ZK: private email org-domain suffix -> 1 ACCEPT (string_length + substring)")
        if not se_ok:
            print(f"        rc={_se.returncode}  out: {_se.stdout.strip()[-220:]}  err: {_se.stderr.strip()[-150:]}")
            failures += 1

    # String `match` / PStr (v5.102): a string-literal pattern selects via the v5.101 multi-wire
    # per-codepoint equality gadget — provable allowlist membership / dispatch over a PRIVATE string.
    # `match cmd { "deploy" => 1; "rollback" => 2; "status" => 3; _ => 0 }`: cmd="deploy" -> 1 ACCEPT,
    # witness3 AGREES (the command stays a private witness). Goldilocks native path.
    _al_path = os.path.join(EX, "prove", "private_allowlist.glass")
    _al = _prove_run([sys.executable, GLASS, "prove", _al_path, 'cmd=deploy', "--cross-check"],
                         capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_al, "string match: private cmd 'deploy' -> action 1 ACCEPT (allowlist dispatch, cmd hidden)"):
        al_ok = (_al.returncode == 0) and ("result:  1" in _al.stdout) and ("ACCEPT" in _al.stdout) and ("THIRD LINEAGE AGREES" in _al.stdout)
        print(f"  {'OK ' if al_ok else 'FAIL'}  string match: private cmd 'deploy' -> action 1 ACCEPT (allowlist dispatch, cmd hidden)")
        if not al_ok:
            print(f"        rc={_al.returncode}  out: {_al.stdout.strip()[-220:]}  err: {_al.stderr.strip()[-150:]}")
            failures += 1
    # Non-member falls through `_` to 0 (the per-codepoint compare discriminates; no string matches it).
    _aln = _prove_run([sys.executable, GLASS, "prove", _al_path, 'cmd=hack', "--cross-check"],
                          capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_aln, "string match: non-member cmd 'hack' -> 0 (falls through _; no arm matches)"):
        aln_ok = (_aln.returncode == 0) and ("result:  0" in _aln.stdout) and ("THIRD LINEAGE AGREES" in _aln.stdout)
        print(f"  {'OK ' if aln_ok else 'FAIL'}  string match: non-member cmd 'hack' -> 0 (falls through _; no arm matches)")
        if not aln_ok:
            print(f"        rc={_aln.returncode}  out: {_aln.stdout.strip()[-220:]}  err: {_aln.stderr.strip()[-150:]}")
            failures += 1
    # Soundness: a false dispatch claim REJECTs. action("deploy") is 1, so claiming 2 is unsatisfiable.
    _alf = _prove_run([sys.executable, GLASS, "prove", "--claim", "2", _al_path, 'cmd=deploy'],
                          capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_alf, "string match: false dispatch claim REJECTs (action 'deploy'=1; claim 2 is false)"):
        alf_ok = ("proof:   REJECT" in _alf.stdout) and ("proof:   ACCEPT" not in _alf.stdout)
        print(f"  {'OK ' if alf_ok else 'FAIL'}  string match: false dispatch claim REJECTs (action 'deploy'=1; claim 2 is false)")
        if not alf_ok:
            print(f"        rc={_alf.returncode}  out: {_alf.stdout.strip()[-220:]}  err: {_alf.stderr.strip()[-150:]}")
            failures += 1

    # Records (v5.103): a named record lowers like a tuple (multi-wire, decl order, twidth-padded, no
    # tag). Construct (ENamedRec) + destructure (PRecord match) over PRIVATE values — structured data
    # flowing through a proof. `order` returns Stats { lo, hi } (sorted bounds), `span` matches it to
    # prove hi-lo. x=3 y=8 -> 5 ACCEPT, witness3 AGREES; order normalizes (x=8 y=3 -> 5 too). Goldilocks native.
    _rs_path = os.path.join(EX, "prove", "record_stats.glass")
    _rs = _prove_run([sys.executable, GLASS, "prove", _rs_path, "x=3", "y=8", "--cross-check"],
                         capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_rs, "records: Stats{lo,hi} construct + match span = 5 ACCEPT (structured data in ZK)"):
        rs_ok = (_rs.returncode == 0) and ("result:  5" in _rs.stdout) and ("ACCEPT" in _rs.stdout) and ("THIRD LINEAGE AGREES" in _rs.stdout)
        print(f"  {'OK ' if rs_ok else 'FAIL'}  records: Stats{{lo,hi}} construct + match span = 5 ACCEPT (structured data in ZK)")
        if not rs_ok:
            print(f"        rc={_rs.returncode}  out: {_rs.stdout.strip()[-220:]}  err: {_rs.stderr.strip()[-150:]}")
            failures += 1
    # Soundness: a false claim about the record-derived result REJECTs (span=5; claim 4 is false).
    _rsf = _prove_run([sys.executable, GLASS, "prove", "--claim", "4", _rs_path, "x=3", "y=8"],
                          capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_rsf, "records: false claim REJECTs (span(order(3,8))=5; claim 4 is false)"):
        rsf_ok = ("proof:   REJECT" in _rsf.stdout) and ("proof:   ACCEPT" not in _rsf.stdout)
        print(f"  {'OK ' if rsf_ok else 'FAIL'}  records: false claim REJECTs (span(order(3,8))=5; claim 4 is false)")
        if not rsf_ok:
            print(f"        rc={_rsf.returncode}  out: {_rsf.stdout.strip()[-220:]}  err: {_rsf.stderr.strip()[-150:]}")
            failures += 1

    # Record field access r.field (v5.104): the idiomatic dot-access lowers via a type-env (reusing
    # the fenv slot, name -> "@rec:Type") + the v5.103 PRecord desugar. `solvent(a) = a.balance >= 100`
    # over a PRIVATE Account proves solvency by reading the field directly — revealing only the verdict.
    # bal=250 -> 1 ACCEPT, witness3 AGREES (balance + owner hidden). Goldilocks native.
    _rf_path = os.path.join(EX, "prove", "record_field.glass")
    _rf = _prove_run([sys.executable, GLASS, "prove", _rf_path, "bal=250", "own=7", "--cross-check"],
                         capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_rf, "record field access: solvent(a)=a.balance>=100 -> 1 ACCEPT (a.field read directly, hidden)"):
        rf_ok = (_rf.returncode == 0) and ("result:  1" in _rf.stdout) and ("ACCEPT" in _rf.stdout) and ("THIRD LINEAGE AGREES" in _rf.stdout)
        print(f"  {'OK ' if rf_ok else 'FAIL'}  record field access: solvent(a)=a.balance>=100 -> 1 ACCEPT (a.field read directly, hidden)")
        if not rf_ok:
            print(f"        rc={_rf.returncode}  out: {_rf.stdout.strip()[-220:]}  err: {_rf.stderr.strip()[-150:]}")
            failures += 1
    # Soundness: a false claim about the field-access result REJECTs (solvent(250)=1; claim 0 is false).
    _rff = _prove_run([sys.executable, GLASS, "prove", "--claim", "0", _rf_path, "bal=250", "own=7"],
                          capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_rff, "record field access: false claim REJECTs (solvent=1; claim 0 is false)"):
        rff_ok = ("proof:   REJECT" in _rff.stdout) and ("proof:   ACCEPT" not in _rff.stdout)
        print(f"  {'OK ' if rff_ok else 'FAIL'}  record field access: false claim REJECTs (solvent=1; claim 0 is false)")
        if not rff_ok:
            print(f"        rc={_rff.returncode}  out: {_rff.stdout.strip()[-220:]}  err: {_rff.stderr.strip()[-150:]}")
            failures += 1

    # Capstone (v5.108): the whole arc COMPOSES — a private access-policy decision combining records
    # (Applicant), field access (a.age, a.region), ordering comparison (>=, <=), and string dispatch
    # (tier in an allowlist), all in one proven circuit. age/region/tier are PRIVATE; only the verdict
    # is revealed. End-to-end composition test: eligible -> 1 ACCEPT + witness3 AGREES; false claim REJECTs.
    _el_path = os.path.join(EX, "prove", "private_eligibility.glass")
    _el = _prove_run([sys.executable, GLASS, "prove", _el_path, "age0=29", "region0=3", "tier0=gold", "--cross-check"],
                         capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_el, "capstone: records + field access + comparison + string dispatch compose -> eligible=1 ACCEPT"):
        el_ok = (_el.returncode == 0) and ("result:  1" in _el.stdout) and ("ACCEPT" in _el.stdout) and ("THIRD LINEAGE AGREES" in _el.stdout)
        print(f"  {'OK ' if el_ok else 'FAIL'}  capstone: records + field access + comparison + string dispatch compose -> eligible=1 ACCEPT")
        if not el_ok:
            print(f"        rc={_el.returncode}  out: {_el.stdout.strip()[-260:]}  err: {_el.stderr.strip()[-150:]}")
            failures += 1
    _elf = _prove_run([sys.executable, GLASS, "prove", "--claim", "0", _el_path, "age0=29", "region0=3", "tier0=gold"],
                          capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_elf, "capstone: false eligibility claim REJECTs (eligible=1; claim 0 is false)"):
        elf_ok = ("proof:   REJECT" in _elf.stdout) and ("proof:   ACCEPT" not in _elf.stdout)
        print(f"  {'OK ' if elf_ok else 'FAIL'}  capstone: false eligibility claim REJECTs (eligible=1; claim 0 is false)")
        if not elf_ok:
            print(f"        rc={_elf.returncode}  out: {_elf.stdout.strip()[-260:]}  err: {_elf.stderr.strip()[-150:]}")
            failures += 1

    # String-VALUED result (v5.110): a proven function can RETURN a string, not just a number / Bool.
    # A string is multi-wire (one codepoint wire per char), so the proof binds EVERY output wire as
    # the public claim (build_claim_mw) and DECODES it back to text — no `verify_b3`/Pentecost change
    # (a multi-wire claim is just more is-zero asserts). Selective disclosure: reveal_prefix reveals
    # the first 8 chars of a PRIVATE key, the rest hidden. -> "sk-live-" ACCEPT, witness3 AGREES.
    _rp_path = os.path.join(EX, "prove", "reveal_prefix.glass")
    _rpv = _prove_run([sys.executable, GLASS, "prove", _rp_path, "key=sk-live-9f3a2c7e1b", "--cross-check"],
                          capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_rpv, 'string-valued result: reveal_prefix -> "sk-live-" ACCEPT (string result bound + decoded, key hidden)'):
        rpv_ok = (_rpv.returncode == 0) and ('result:  "sk-live-"' in _rpv.stdout) and ("ACCEPT" in _rpv.stdout) and ("THIRD LINEAGE AGREES" in _rpv.stdout)
        print(f"  {'OK ' if rpv_ok else 'FAIL'}  string-valued result: reveal_prefix -> \"sk-live-\" ACCEPT (string result bound + decoded, key hidden)")
        if not rpv_ok:
            print(f"        rc={_rpv.returncode}  out: {_rpv.stdout.strip()[-260:]}  err: {_rpv.stderr.strip()[-150:]}")
            failures += 1
    # A string chosen by a PRIVATE comparison: verdict(score). Equal-width branches mux wire-by-wire;
    # the verdict WORD is revealed, the score hidden. score=820 -> "PASS", score=500 -> "FAIL" (the
    # branch genuinely selects — not a constant), both ACCEPT + witness3 AGREES on the string.
    _vd_path = os.path.join(EX, "prove", "private_verdict.glass")
    _vdp = _prove_run([sys.executable, GLASS, "prove", _vd_path, "score=820", "--cross-check"],
                          capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_vdp, 'string-valued result: private score 820 -> "PASS" ACCEPT (verdict word revealed, score hidden)'):
        vdp_ok = (_vdp.returncode == 0) and ('result:  "PASS"' in _vdp.stdout) and ("ACCEPT" in _vdp.stdout) and ("THIRD LINEAGE AGREES" in _vdp.stdout)
        print(f"  {'OK ' if vdp_ok else 'FAIL'}  string-valued result: private score 820 -> \"PASS\" ACCEPT (verdict word revealed, score hidden)")
        if not vdp_ok:
            print(f"        rc={_vdp.returncode}  out: {_vdp.stdout.strip()[-260:]}  err: {_vdp.stderr.strip()[-150:]}")
            failures += 1
    _vdf = _prove_run([sys.executable, GLASS, "prove", _vd_path, "score=500", "--cross-check"],
                          capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_vdf, 'string-valued result: private score 500 -> "FAIL" (the if-over-strings branch selects)'):
        vdf_ok = (_vdf.returncode == 0) and ('result:  "FAIL"' in _vdf.stdout) and ("THIRD LINEAGE AGREES" in _vdf.stdout)
        print(f"  {'OK ' if vdf_ok else 'FAIL'}  string-valued result: private score 500 -> \"FAIL\" (the if-over-strings branch selects)")
        if not vdf_ok:
            print(f"        rc={_vdf.returncode}  out: {_vdf.stdout.strip()[-260:]}  err: {_vdf.stderr.strip()[-150:]}")
            failures += 1
    # Unequal-width string results (v5.121): an `if`/`match` returning strings of DIFFERENT widths now
    # LOWERS soundly — the bridge NUL-pads the shorter branch (codepoint 0, a value real chars 32..126
    # never take) and decode_str stops at the sentinel, so the selected branch reveals its true text.
    # private_risk has four nested ifs of lengths 8/4/6/3; score=95 -> "CRITICAL" (the longest), score
    # hidden. (Until v5.121 this ABSTAINed and branches had to be hand-padded, as private_verdict does.)
    import tempfile as _tf_sr
    _rk_path = os.path.join(EX, "prove", "private_risk.glass")
    _rk = _prove_run([sys.executable, GLASS, "prove", _rk_path, "score=95", "--cross-check"],
                         capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_rk, 'unequal-width strings: private_risk score=95 -> "CRITICAL" ACCEPT (NUL-padded if-mux, score hidden)'):
        rk_ok = (_rk.returncode == 0) and ('result:  "CRITICAL"' in _rk.stdout) and ("ACCEPT" in _rk.stdout) and ("THIRD LINEAGE AGREES" in _rk.stdout)
        print(f"  {'OK ' if rk_ok else 'FAIL'}  unequal-width strings: private_risk score=95 -> \"CRITICAL\" ACCEPT (NUL-padded if-mux, score hidden)")
        if not rk_ok:
            print(f"        rc={_rk.returncode}  out: {_rk.stdout.strip()[-260:]}  err: {_rk.stderr.strip()[-150:]}")
            failures += 1
    # The shortest band, to show the nested if genuinely selects (not a constant) across widths.
    _rk2 = _prove_run([sys.executable, GLASS, "prove", _rk_path, "score=10", "--cross-check"],
                          capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_rk2, 'unequal-width strings: private_risk score=10 -> "LOW" (the shortest band selects)'):
        rk2_ok = (_rk2.returncode == 0) and ('result:  "LOW"' in _rk2.stdout) and ("THIRD LINEAGE AGREES" in _rk2.stdout)
        print(f"  {'OK ' if rk2_ok else 'FAIL'}  unequal-width strings: private_risk score=10 -> \"LOW\" (the shortest band selects)")
        if not rk2_ok:
            print(f"        rc={_rk2.returncode}  out: {_rk2.stdout.strip()[-260:]}  err: {_rk2.stderr.strip()[-150:]}")
            failures += 1
    # The latent-bug regression (v5.121): a `match` with unequal-width string arms used to SILENTLY
    # TRUNCATE to the last arm's width — `match s { 0 => "approved"; _ => "no" }` at s=0 attested the
    # corrupted "ap" yet ACCEPTed (a source<->circuit divergence only --witness3 caught). accw now keeps
    # the longer accumulator + decode stops at NUL, so it attests the true "approved" and witness3 AGREES.
    with _tf_sr.NamedTemporaryFile("w", suffix=".glass", delete=False) as _ufm:
        _ufm.write('fn lab(s: Int) : String = match s { 0 => "approved"; _ => "no" }\nlab(score)\n')
        _mtrunc_path = _ufm.name
    _mt = _prove_run([sys.executable, GLASS, "prove", _mtrunc_path, "score=0", "--cross-check"],
                         capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_mt, 'unequal-width match: s=0 -> "approved" ACCEPT (was silently truncated to "ap"; v5.121 fix)'):
        mt_ok = (_mt.returncode == 0) and ('result:  "approved"' in _mt.stdout) and ("ACCEPT" in _mt.stdout) and ("THIRD LINEAGE AGREES" in _mt.stdout)
        print(f"  {'OK ' if mt_ok else 'FAIL'}  unequal-width match: s=0 -> \"approved\" ACCEPT (was silently truncated to \"ap\"; v5.121 fix)")
        if not mt_ok:
            print(f"        rc={_mt.returncode}  out: {_mt.stdout.strip()[-260:]}  err: {_mt.stderr.strip()[-150:]}")
            failures += 1
    # Soundness guard: an unequal-width mux that is NOT both flat strings — here a tuple carrying a
    # variable-length string field — still ABSTAINs (is_str_expr is false for ETuple/ECtor), so a
    # structured value is never NUL-corrupted. Only provably-flat strings take the padding path.
    with _tf_sr.NamedTemporaryFile("w", suffix=".glass", delete=False) as _ufs:
        _ufs.write('fn pick(c: Int) : (String, Int) = if c >= 1 then ("ab", 1) else ("xyz", 2)\npick(flag)\n')
        _struct_path = _ufs.name
    _st = _prove_run([sys.executable, GLASS, "prove", _struct_path, "flag=1"],
                         capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_st, "unequal-width mux: a structured (tuple-with-string) value ABSTAINs (not NUL-corrupted)"):
        st_ok = ("verdict: ABSTAIN" in _st.stdout) and ("proof:   ACCEPT" not in _st.stdout)
        print(f"  {'OK ' if st_ok else 'FAIL'}  unequal-width mux: a structured (tuple-with-string) value ABSTAINs (not NUL-corrupted)")
        if not st_ok:
            print(f"        rc={_st.returncode}  out: {_st.stdout.strip()[-260:]}  err: {_st.stderr.strip()[-150:]}")
            failures += 1
    # Soundness guard 2: a multi-wire result that is NOT a string and NOT a tuple/record-of-scalars —
    # an ADT (a tagged constructor value) — is not bindable as a public claim, so it ABSTAINs rather
    # than silently publish only its first wire (the old `vh` truncation). (Tuples/records of scalars
    # ARE bindable since v5.117; ADTs are the residual multi-wire shape that still abstains.)
    with _tf_sr.NamedTemporaryFile("w", suffix=".glass", delete=False) as _uf2:
        _uf2.write("type Box = | B(Int) | C(Int)\nfn mk(a: Int) : Box = B(a)\nmk(x)\n")
        _tup_path = _uf2.name
    _tup = _prove_run([sys.executable, GLASS, "prove", _tup_path, "x=3"],
                          capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_tup, "structured result: a multi-wire ADT result ABSTAINs (not truncated to wire 0)"):
        tup_ok = ("verdict: ABSTAIN" in _tup.stdout) and ("proof:   ACCEPT" not in _tup.stdout)
        print(f"  {'OK ' if tup_ok else 'FAIL'}  structured result: a multi-wire ADT result ABSTAINs (not truncated to wire 0)")
        if not tup_ok:
            print(f"        rc={_tup.returncode}  out: {_tup.stdout.strip()[-260:]}  err: {_tup.stderr.strip()[-150:]}")
            failures += 1
    # Soundness guard 3 (v5.128): a built-in List<Int> threaded through a function and indexed used to
    # lower to a SILENT WRONG circuit. prism desugars [a,b,c]/[h,...t] to Cons/Nil ECtor/PCtor, but the
    # built-in List type is in no source TypeDecl, so ctag/ctor_argtypes returned tag 0 / no fields for
    # BOTH Cons and Nil -> every list pattern collapsed to the [] arm and the proof attested 0 (ACCEPT),
    # caught only by --witness3 (DIVERGENCE). Now ctag/ctor_argtypes ABSTAIN on ANY undeclared ctor: a
    # built-in list in proven position is refused loudly, never silently proven 0. (Declared ADTs like
    # map_prove's IntList still resolve and ACCEPT -- verified by the higher-order gate above.) The
    # refusal fires DURING lowering (pre-STARK), so this gate is fast.
    with _tf_sr.NamedTemporaryFile("w", suffix=".glass", delete=False) as _uf3:
        _uf3.write("fn dbl(xs: List<Int>) : List<Int> = match xs { [] => []; [h, ...t] => [h + h, ...dbl(t)] }\n"
                   "fn idx0(xs: List<Int>) : Int = match xs { [] => 0; [h, ...t] => h }\n"
                   "idx0(dbl(dbl([3, 5, 7])))\n")
        _lst_path = _uf3.name
    _lst = _prove_run([sys.executable, GLASS, "prove", _lst_path],
                          capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_lst, "built-in List threaded into a proof ABSTAINs (undeclared Cons/Nil, not silently proven 0)"):
        lst_ok = (("verdict: ABSTAIN" in _lst.stdout)
                  and ("undeclared constructor" in (_lst.stdout + _lst.stderr))
                  and ("proof:   ACCEPT" not in _lst.stdout))
        print(f"  {'OK ' if lst_ok else 'FAIL'}  built-in List threaded into a proof ABSTAINs (undeclared Cons/Nil, not silently proven 0)")
        if not lst_ok:
            print(f"        rc={_lst.returncode}  out: {_lst.stdout.strip()[-260:]}  err: {_lst.stderr.strip()[-150:]}")
            failures += 1
    # Soundness guard 4 (v5.129): an OUT-OF-BOUNDS substring used to OVER-READ — substring("ab",0,5)
    # lowered to a 5-wire slice whose OOB tail read nthI's default = wire 0 = the FIRST input codepoint,
    # attesting "abaaa" while the source (glass.py b_substring) CLAMPS to "ab"; the SOUND verify_b3
    # ACCEPTed the wrong string, caught only by --witness3. substr_bounds now reproduces b_substring
    # EXACTLY (clamp both bounds to the width), so the circuit value EQUALS the reference -> the Third
    # Witness AGREES (and a false predicate like substring(key,0,8)=="sk-live-" can no longer be made
    # to pass for a short key). The clamp is a no-op for in-bounds slices (private_prefix/email above).
    with _tf_sr.NamedTemporaryFile("w", suffix=".glass", delete=False) as _ufoob:
        _ufoob.write("fn f(s: String) : String = substring(s, 0, 5)\nf(inp)\n")
        _oob_path = _ufoob.name
    _oob = _prove_run([sys.executable, GLASS, "prove", _oob_path, "inp=ab", "--cross-check"],
                          capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_oob, 'substring OOB now CLAMPS to the reference ("ab", not over-read "abaaa") -> Third Witness AGREES'):
        oob_ok = ((_oob.returncode == 0) and ('result:  "ab"' in _oob.stdout)
                  and ("ACCEPT" in _oob.stdout) and ("THIRD LINEAGE AGREES" in _oob.stdout)
                  and ("abaaa" not in _oob.stdout))
        print(f"  {'OK ' if oob_ok else 'FAIL'}  substring OOB now CLAMPS to the reference (\"ab\", not over-read \"abaaa\") -> Third Witness AGREES")
        if not oob_ok:
            print(f"        rc={_oob.returncode}  out: {_oob.stdout.strip()[-260:]}  err: {_oob.stderr.strip()[-150:]}")
            failures += 1
    # Soundness guard 5 (v5.129): an INVERTED substring (start > end) used to produce an empty slice
    # silently, which then reached the SCALAR claim binder (build_claim_m) and bound wire 0 VACUOUSLY
    # (mks(vhi([])=0, 0)=0), ACCEPTing an arbitrary claim. substr_bounds now ABSTAINs on start>end
    # (matching b_substring's raise), and build_claim_m/build_claim_pub now guard ilenI(outws)==1. The
    # program ABSTAINs (pre-STARK), never a vacuous ACCEPT.
    with _tf_sr.NamedTemporaryFile("w", suffix=".glass", delete=False) as _ufinv:
        _ufinv.write("fn f(s: String) : String = substring(s, 5, 2)\nf(inp)\n")
        _inv_path = _ufinv.name
    _inv = _prove_run([sys.executable, GLASS, "prove", _inv_path, "inp=ab"],
                          capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_inv, "substring start>end ABSTAINs (no silent empty slice -> no vacuous wire-0 claim bind)"):
        inv_ok = (("verdict: ABSTAIN" in _inv.stdout)
                  and ("start > end" in (_inv.stdout + _inv.stderr))
                  and ("proof:   ACCEPT" not in _inv.stdout))
        print(f"  {'OK ' if inv_ok else 'FAIL'}  substring start>end ABSTAINs (no silent empty slice -> no vacuous wire-0 claim bind)")
        if not inv_ok:
            print(f"        rc={_inv.returncode}  out: {_inv.stdout.strip()[-260:]}  err: {_inv.stderr.strip()[-150:]}")
            failures += 1
    # Soundness guard 6 (v5.130, audit hole B1) — a recursive-ADT value can be WIDER than its fixed
    # `twidth` slot (Cons(7,Nil)=27 wires vs twidth(IntList)=25, since twidth decrements fuel per level
    # while construction pads flat). When such an over-wide field is FOLLOWED by another field, the
    # following field was read at a shifted offset (onto the overflow wires) -> silent wrong value:
    # second(MkPair(Cons(7,Nil), inp)) proved 0, not inp. The *_fields lowering now ABSTAINs on a NON-LAST
    # over-width field. (BENIGN when the recursive field is LAST -> map_prove still ACCEPTs 13, gated above.)
    with _tf_sr.NamedTemporaryFile("w", suffix=".glass", delete=False) as _ufb1:
        _ufb1.write("type IntList = | Nil | Cons(Int, IntList)\ntype Pair2 = | MkPair(IntList, Int)\n"
                    "fn second(p: Pair2) : Int = match p { MkPair(l, x) => x }\nsecond(MkPair(Cons(7, Nil), inp))\n")
        _b1_path = _ufb1.name
    _b1 = _prove_run([sys.executable, GLASS, "prove", _b1_path, "inp=99"], capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_b1, "ADT layout: a non-last field WIDER than its twidth slot ABSTAINs (recursive-ADT overflow, not silent 0)"):
        b1_ok = (("verdict: ABSTAIN" in _b1.stdout) and ("WIDER than" in (_b1.stdout + _b1.stderr))
                 and ("proof:   ACCEPT" not in _b1.stdout))
        print(f"  {'OK ' if b1_ok else 'FAIL'}  ADT layout: a non-last field WIDER than its twidth slot ABSTAINs (recursive-ADT overflow, not silent 0)")
        if not b1_ok:
            print(f"        rc={_b1.returncode}  out: {_b1.stdout.strip()[-260:]}  err: {_b1.stderr.strip()[-150:]}")
            failures += 1
    # Soundness guard 7 (v5.130, audit hole B2) — a String FIELD embedded in a record/ADT/tuple has no
    # fixed type-determined wire width (it is codepoint-count dependent), so a width-1 twidth slot
    # mis-offset the following fields (or truncated the string): getn(Box{s:"hello", n:inp}) read a
    # codepoint of "hello" instead of inp. twidth now ABSTAINs on a String field. (Standalone String
    # inputs/results are unaffected -- private_prefix/email/reveal_prefix gated above.)
    with _tf_sr.NamedTemporaryFile("w", suffix=".glass", delete=False) as _ufb2:
        _ufb2.write("type Box = { s: String, n: Int }\nfn getn(b: Box) : Int = match b { Box { s, n } => n }\n"
                    "getn(Box { s: \"hello\", n: inp })\n")
        _b2_path = _ufb2.name
    _b2 = _prove_run([sys.executable, GLASS, "prove", _b2_path, "inp=42"], capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_b2, "ADT layout: a String FIELD in a record/ADT ABSTAINs (no fixed wire width, not a mis-offset read)"):
        b2_ok = (("verdict: ABSTAIN" in _b2.stdout) and ("fixed type-determined wire width" in (_b2.stdout + _b2.stderr))
                 and ("proof:   ACCEPT" not in _b2.stdout))
        print(f"  {'OK ' if b2_ok else 'FAIL'}  ADT layout: a String FIELD in a record/ADT ABSTAINs (no fixed wire width, not a mis-offset read)")
        if not b2_ok:
            print(f"        rc={_b2.returncode}  out: {_b2.stdout.strip()[-260:]}  err: {_b2.stderr.strip()[-150:]}")
            failures += 1

    # String --claim (v5.111): assert a SPECIFIC string result. The claimed string's codepoints are
    # bound (not the computed result), so a FALSE claim makes the circuit unsatisfiable and the
    # independent verify_b3 REJECTs — the soundness property for string results, made testable
    # end-to-end (v5.110 string results had only the structural REJECT argument). verdict(820)="PASS".
    _vc = _prove_run([sys.executable, GLASS, "prove", "--claim", "PASS", _vd_path, "score=820"],
                         capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_vc, 'string --claim: a TRUE string claim ("PASS") ACCEPTs'):
        vc_ok = (_vc.returncode == 0) and ('claim:   "PASS"' in _vc.stdout) and ("proof:   ACCEPT" in _vc.stdout)
        print(f"  {'OK ' if vc_ok else 'FAIL'}  string --claim: a TRUE string claim (\"PASS\") ACCEPTs")
        if not vc_ok:
            print(f"        rc={_vc.returncode}  out: {_vc.stdout.strip()[-260:]}  err: {_vc.stderr.strip()[-150:]}")
            failures += 1
    # The soundness headline: a FALSE equal-length string claim REJECTs (verdict(820)="PASS"; "FAIL" is false).
    _vcf = _prove_run([sys.executable, GLASS, "prove", "--claim", "FAIL", _vd_path, "score=820"],
                          capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_vcf, 'string --claim: a FALSE string claim ("FAIL") REJECTs (the string-result soundness gate)'):
        vcf_ok = ("proof:   REJECT" in _vcf.stdout) and ("proof:   ACCEPT" not in _vcf.stdout)
        print(f"  {'OK ' if vcf_ok else 'FAIL'}  string --claim: a FALSE string claim (\"FAIL\") REJECTs (the string-result soundness gate)")
        if not vcf_ok:
            print(f"        rc={_vcf.returncode}  out: {_vcf.stdout.strip()[-260:]}  err: {_vcf.stderr.strip()[-150:]}")
            failures += 1
    # A wrong-LENGTH string claim ABSTAINs (build_claim_mw's length guard) — never bound as a matching
    # prefix (which would wrongly ACCEPT a too-short claim). "PASSING" (7) vs the 4-char result.
    _vcl = _prove_run([sys.executable, GLASS, "prove", "--claim", "PASSING", _vd_path, "score=820"],
                          capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_vcl, "string --claim: a wrong-LENGTH claim ABSTAINs (no matching-prefix under-binding)"):
        vcl_ok = ("verdict: ABSTAIN" in _vcl.stdout) and ("proof:   ACCEPT" not in _vcl.stdout)
        print(f"  {'OK ' if vcl_ok else 'FAIL'}  string --claim: a wrong-LENGTH claim ABSTAINs (no matching-prefix under-binding)")
        if not vcl_ok:
            print(f"        rc={_vcl.returncode}  out: {_vcl.stdout.strip()[-260:]}  err: {_vcl.stderr.strip()[-150:]}")
            failures += 1
    # A non-numeric --claim on a SCALAR result is a category error -> ABSTAIN (a pure pre-lowering guard).
    with _tf_sr.NamedTemporaryFile("w", suffix=".glass", delete=False) as _uf3:
        _uf3.write("fn add(a: Int, b: Int) : Int = a + b\nadd(x, y)\n")
        _sclaim_path = _uf3.name
    _scc = _prove_run([sys.executable, GLASS, "prove", "--claim", "foo", _sclaim_path, "x=5", "y=7"],
                          capture_output=True, text=True, cwd=ROOT)
    scc_ok = ("verdict: ABSTAIN" in _scc.stdout) and ("proof:   ACCEPT" not in _scc.stdout)
    print(f"  {'OK ' if scc_ok else 'FAIL'}  string --claim: a string claim on a SCALAR result ABSTAINs (type mismatch)")
    if not scc_ok:
        print(f"        rc={_scc.returncode}  out: {_scc.stdout.strip()[-260:]}  err: {_scc.stderr.strip()[-150:]}")
        failures += 1

    # Portable STRING-RESULT proof (v5.112): `glass prove --emit` a string-valued proof, then the
    # INDEPENDENT Pentecost verifier must ACCEPT it. v5.110 string results couldn't --emit (multi-wire
    # ABSTAIN); now the multi-wire claim (gprove_emit_mw) serializes to the same token stream Pentecost
    # parses, so the second verifier checks the string-VALUED proof shape end-to-end via the CLI. (The
    # committed corpus fixture honest_string_result.b3.txt.gz tamper-checks the same shape statically.)
    with _tf_sr.NamedTemporaryFile("w", suffix=".b3.txt", delete=False) as _ef:
        _emit_proof_path = _ef.name
    _emi = _prove_run([sys.executable, GLASS, "prove", "--emit", _emit_proof_path, _rp_path, "key=sk-live-9f3a2c7e1b"],
                          capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_emi, "portable string-result proof: --emit a string-valued proof, Pentecost verifies it"):
        _emv = subprocess.run([sys.executable, GLASS, "verify", _emit_proof_path], capture_output=True, text=True, cwd=ROOT)
        emi_ok = (_emi.returncode == 0) and ("wrote a portable proof" in _emi.stdout) and ("PENTECOST: ACCEPT" in _emv.stdout)
        print(f"  {'OK ' if emi_ok else 'FAIL'}  portable string-result proof: --emit a string-valued proof, Pentecost verifies it")
        if not emi_ok:
            print(f"        emit rc={_emi.returncode} out: {_emi.stdout.strip()[-180:]}  verify out: {_emv.stdout.strip()[-180:]}")
            failures += 1

    # Computed higher-order callee (v5.113): a callee CHOSEN AT RUNTIME — `(if mode >= 1 then double
    # else increment)(x)` — was the last refused call form (named-fn HOFs already proved, v5.87). The
    # cut: push the application inside the selector (applying a conditionally-chosen function == cond-
    # itionally applying each candidate), so it lowers as `if c then g(x) else h(x)` — named-fn calls
    # muxed by the same gadget an `if` uses; the rewrite is shared by seval (guard) + unroll (circuit).
    _cc_path = os.path.join(EX, "prove", "computed_callee.glass")
    _cc1 = _prove_run([sys.executable, GLASS, "prove", _cc_path, "mode=1", "x=21", "--cross-check"],
                          capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_cc1, "computed callee: (if mode>=1 then double else increment)(21), mode=1 -> 42 ACCEPT"):
        cc1_ok = (_cc1.returncode == 0) and ("result:  42" in _cc1.stdout) and ("ACCEPT" in _cc1.stdout) and ("THIRD LINEAGE AGREES" in _cc1.stdout)
        print(f"  {'OK ' if cc1_ok else 'FAIL'}  computed callee: (if mode>=1 then double else increment)(21), mode=1 -> 42 ACCEPT")
        if not cc1_ok:
            print(f"        rc={_cc1.returncode}  out: {_cc1.stdout.strip()[-260:]}  err: {_cc1.stderr.strip()[-150:]}")
            failures += 1
    # The runtime-chosen callee genuinely depends on the private flag (not a constant): mode=0 -> increment.
    _cc0 = _prove_run([sys.executable, GLASS, "prove", _cc_path, "mode=0", "x=21", "--cross-check"],
                          capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_cc0, "computed callee: mode=0 -> increment(21)=22 (the runtime-chosen callee depends on the flag)"):
        cc0_ok = (_cc0.returncode == 0) and ("result:  22" in _cc0.stdout) and ("THIRD LINEAGE AGREES" in _cc0.stdout)
        print(f"  {'OK ' if cc0_ok else 'FAIL'}  computed callee: mode=0 -> increment(21)=22 (the runtime-chosen callee depends on the flag)")
        if not cc0_ok:
            print(f"        rc={_cc0.returncode}  out: {_cc0.stdout.strip()[-260:]}  err: {_cc0.stderr.strip()[-150:]}")
            failures += 1
    # Soundness: a false claim about the computed-callee result REJECTs (run(1,21)=42; claim 22 is false).
    _ccf = _prove_run([sys.executable, GLASS, "prove", "--claim", "22", _cc_path, "mode=1", "x=21"],
                          capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_ccf, "computed callee: false claim REJECTs (run(1,21)=42; claim 22 is false)"):
        ccf_ok = ("proof:   REJECT" in _ccf.stdout) and ("proof:   ACCEPT" not in _ccf.stdout)
        print(f"  {'OK ' if ccf_ok else 'FAIL'}  computed callee: false claim REJECTs (run(1,21)=42; claim 22 is false)")
        if not ccf_ok:
            print(f"        rc={_ccf.returncode}  out: {_ccf.stdout.strip()[-260:]}  err: {_ccf.stderr.strip()[-150:]}")
            failures += 1

    # Let-aliased fn callee (v5.114): `let f = g in f(x)` binds a function NAME locally and calls it
    # — closing the "unresolved call to 'f'" refusal for a let-bound fn name (distinct from the v5.113
    # runtime-chosen callee; reuses the v5.87 fn-arg fenv mechanism, aliasing f -> g in fenv and
    # dropping the let). g0 = double, so `let f = g0 in f(6)` = 12.
    with _tf_sr.NamedTemporaryFile("w", suffix=".glass", delete=False) as _laf:
        _laf.write("fn g0(x: Int) : Int = x + x\nfn run(n: Int) : Int = let f = g0 in f(n)\nrun(k)\n")
        _la_path = _laf.name
    _la = _prove_run([sys.executable, GLASS, "prove", _la_path, "k=6", "--cross-check"],
                         capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_la, "let-aliased fn callee: let f = g0 in f(6) -> 12 ACCEPT (the 'unresolved f' refusal closed)"):
        la_ok = (_la.returncode == 0) and ("result:  12" in _la.stdout) and ("ACCEPT" in _la.stdout) and ("THIRD LINEAGE AGREES" in _la.stdout)
        print(f"  {'OK ' if la_ok else 'FAIL'}  let-aliased fn callee: let f = g0 in f(6) -> 12 ACCEPT (the 'unresolved f' refusal closed)")
        if not la_ok:
            print(f"        rc={_la.returncode}  out: {_la.stdout.strip()[-260:]}  err: {_la.stderr.strip()[-150:]}")
            failures += 1
    _laf2 = _prove_run([sys.executable, GLASS, "prove", "--claim", "11", _la_path, "k=6"],
                           capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_laf2, "let-aliased fn callee: false claim REJECTs (f(6)=12; claim 11 is false)"):
        laf2_ok = ("proof:   REJECT" in _laf2.stdout) and ("proof:   ACCEPT" not in _laf2.stdout)
        print(f"  {'OK ' if laf2_ok else 'FAIL'}  let-aliased fn callee: false claim REJECTs (f(6)=12; claim 11 is false)")
        if not laf2_ok:
            print(f"        rc={_laf2.returncode}  out: {_laf2.stdout.strip()[-260:]}  err: {_laf2.stderr.strip()[-150:]}")
            failures += 1

    # Selector-let callee (v5.115): `let f = (if c then g else h) in f(x)` — a let bound to a RUNTIME
    # SELECTOR over functions, the last residual call form. The cut is the DUAL of push_app: distribute
    # the let over the selector (== if c then (let f=g in body) else (let f=h in body)), each branch
    # then a v5.114 alias. c>=1 -> dbl(5)=10, c=0 -> inc(5)=6 (the callee depends on the private flag).
    with _tf_sr.NamedTemporaryFile("w", suffix=".glass", delete=False) as _slf:
        _slf.write("fn dbl(x: Int) : Int = x + x\nfn inc(x: Int) : Int = x + 1\n"
                   "fn run(c: Int, n: Int) : Int = let f = (if c >= 1 then dbl else inc) in f(n)\nrun(c, n)\n")
        _sl_path = _slf.name
    _sl = _prove_run([sys.executable, GLASS, "prove", _sl_path, "c=1", "n=5", "--cross-check"],
                         capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_sl, "selector-let callee: let f = (if c then dbl else inc) in f(5), c=1 -> 10 ACCEPT"):
        sl_ok = (_sl.returncode == 0) and ("result:  10" in _sl.stdout) and ("ACCEPT" in _sl.stdout) and ("THIRD LINEAGE AGREES" in _sl.stdout)
        print(f"  {'OK ' if sl_ok else 'FAIL'}  selector-let callee: let f = (if c then dbl else inc) in f(5), c=1 -> 10 ACCEPT")
        if not sl_ok:
            print(f"        rc={_sl.returncode}  out: {_sl.stdout.strip()[-260:]}  err: {_sl.stderr.strip()[-150:]}")
            failures += 1
    _slf2 = _prove_run([sys.executable, GLASS, "prove", "--claim", "6", _sl_path, "c=1", "n=5"],
                           capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_slf2, "selector-let callee: false claim REJECTs (run(1,5)=10; claim 6 is false)"):
        slf2_ok = ("proof:   REJECT" in _slf2.stdout) and ("proof:   ACCEPT" not in _slf2.stdout)
        print(f"  {'OK ' if slf2_ok else 'FAIL'}  selector-let callee: false claim REJECTs (run(1,5)=10; claim 6 is false)")
        if not slf2_ok:
            print(f"        rc={_slf2.returncode}  out: {_slf2.stdout.strip()[-260:]}  err: {_slf2.stderr.strip()[-150:]}")
            failures += 1

    # Bitwise logic (v5.116): bit_and / bit_or / bit_xor over [0,2^32) — the one integer-operation
    # family the bridge lacked. The gadget decomposes both operands into boolean-pinned bits (reusing
    # the range gadget's machinery), combines per position (AND=a*b, OR=a+b-ab, XOR=(a-b)^2), and
    # recomposes. Each op is value-checked + Third-Witness-confirmed (so the per-bit formula matches
    # the reference int64 builtin); out-of-range ABSTAINs; a false claim REJECTs.
    def _bit_prog(op):
        with _tf_sr.NamedTemporaryFile("w", suffix=".glass", delete=False) as _bf:
            _bf.write("%s(a, b)\n" % op)
            return _bf.name
    for _op, _exp in [("bit_and", 8), ("bit_or", 14), ("bit_xor", 6)]:   # 12 & 10 = 8, | = 14, ^ = 6
        _bp = _prove_run([sys.executable, GLASS, "prove", _bit_prog(_op), "a=12", "b=10", "--cross-check"],
                             capture_output=True, text=True, cwd=ROOT)
        if not _heavy_skipped(_bp, f"bitwise: {_op}(12,10) -> {_exp} ACCEPT (Third Witness confirms the per-bit formula)"):
            bp_ok = (_bp.returncode == 0) and (f"result:  {_exp}" in _bp.stdout) and ("ACCEPT" in _bp.stdout) and ("THIRD LINEAGE AGREES" in _bp.stdout)
            print(f"  {'OK ' if bp_ok else 'FAIL'}  bitwise: {_op}(12,10) -> {_exp} ACCEPT (Third Witness confirms the per-bit formula)")
            if not bp_ok:
                print(f"        rc={_bp.returncode}  out: {_bp.stdout.strip()[-260:]}  err: {_bp.stderr.strip()[-150:]}")
                failures += 1
    # Out-of-range operand (>= 2^32) ABSTAINs (the bit-decomposition would be unsatisfiable — refused, not REJECTed).
    _boob = _prove_run([sys.executable, GLASS, "prove", _bit_prog("bit_and"), "a=8589934592", "b=5"],
                           capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_boob, "bitwise: out-of-range operand (2^33) ABSTAINs"):
        boob_ok = ("verdict: ABSTAIN" in _boob.stdout) and ("proof:   ACCEPT" not in _boob.stdout)
        print(f"  {'OK ' if boob_ok else 'FAIL'}  bitwise: out-of-range operand (2^33) ABSTAINs")
        if not boob_ok:
            print(f"        rc={_boob.returncode}  out: {_boob.stdout.strip()[-260:]}  err: {_boob.stderr.strip()[-150:]}")
            failures += 1
    # Soundness: a false claim about a bitwise result REJECTs (bit_and(12,10)=8; claim 9 is false).
    _bf2 = _prove_run([sys.executable, GLASS, "prove", "--claim", "9", _bit_prog("bit_and"), "a=12", "b=10"],
                          capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_bf2, "bitwise: false claim REJECTs (bit_and(12,10)=8; claim 9 is false)"):
        bf2_ok = ("proof:   REJECT" in _bf2.stdout) and ("proof:   ACCEPT" not in _bf2.stdout)
        print(f"  {'OK ' if bf2_ok else 'FAIL'}  bitwise: false claim REJECTs (bit_and(12,10)=8; claim 9 is false)")
        if not bf2_ok:
            print(f"        rc={_bf2.returncode}  out: {_bf2.stdout.strip()[-260:]}  err: {_bf2.stderr.strip()[-150:]}")
            failures += 1
    # Showcase: a PRIVATE permission bitmask — bit_and(perms, required) == required is a subset check.
    _bm_path = os.path.join(EX, "prove", "private_bitmask.glass")
    _bm1 = _prove_run([sys.executable, GLASS, "prove", _bm_path, "perms=29", "required=13", "--cross-check"],
                          capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_bm1, "bitwise showcase: private bitmask 13's bits ⊆ 29 -> 1 ACCEPT (perms hidden)"):
        bm1_ok = (_bm1.returncode == 0) and ("result:  1" in _bm1.stdout) and ("ACCEPT" in _bm1.stdout) and ("THIRD LINEAGE AGREES" in _bm1.stdout)
        print(f"  {'OK ' if bm1_ok else 'FAIL'}  bitwise showcase: private bitmask 13's bits subset 29 -> 1 ACCEPT (perms hidden)")
        if not bm1_ok:
            print(f"        rc={_bm1.returncode}  out: {_bm1.stdout.strip()[-260:]}  err: {_bm1.stderr.strip()[-150:]}")
            failures += 1
    _bm0 = _prove_run([sys.executable, GLASS, "prove", _bm_path, "perms=8", "required=13", "--cross-check"],
                          capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_bm0, "bitwise showcase: missing bits (8 lacks 13's) -> 0 (the check discriminates)"):
        bm0_ok = (_bm0.returncode == 0) and ("result:  0" in _bm0.stdout) and ("THIRD LINEAGE AGREES" in _bm0.stdout)
        print(f"  {'OK ' if bm0_ok else 'FAIL'}  bitwise showcase: missing bits (8 lacks 13's) -> 0 (the check discriminates)")
        if not bm0_ok:
            print(f"        rc={_bm0.returncode}  out: {_bm0.stdout.strip()[-260:]}  err: {_bm0.stderr.strip()[-150:]}")
            failures += 1

    # Tuple / record RESULTS (v5.117): a proof can RETURN a multi-component value (scalar components),
    # bound by the same multi-wire binder a string result uses (build_claim_mw) and displayed component
    # by component. divmod(17,5) -> (3, 2) ACCEPT; the Third Witness confirms BOTH components.
    _tr_path = os.path.join(EX, "prove", "private_divmod.glass")
    _tr = _prove_run([sys.executable, GLASS, "prove", _tr_path, "a=17", "b=5", "--cross-check"],
                         capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_tr, "tuple result: divmod(17,5) -> (3, 2) ACCEPT (both components bound + Third-Witness-confirmed)"):
        tr_ok = (_tr.returncode == 0) and ("result:  (3, 2)" in _tr.stdout) and ("ACCEPT" in _tr.stdout) and ("THIRD LINEAGE AGREES" in _tr.stdout)
        print(f"  {'OK ' if tr_ok else 'FAIL'}  tuple result: divmod(17,5) -> (3, 2) ACCEPT (both components bound + Third-Witness-confirmed)")
        if not tr_ok:
            print(f"        rc={_tr.returncode}  out: {_tr.stdout.strip()[-260:]}  err: {_tr.stderr.strip()[-150:]}")
            failures += 1
    # A RECORD result displays with field names (Type { f: v, ... }) and binds each field wire.
    with _tf_sr.NamedTemporaryFile("w", suffix=".glass", delete=False) as _rrf:
        _rrf.write("type Bounds = { lo: Int, hi: Int }\n"
                   "fn order(a: Int, b: Int) : Bounds = if a <= b then Bounds { lo: a, hi: b } else Bounds { lo: b, hi: a }\n"
                   "order(x, y)\n")
        _rr_path = _rrf.name
    _rr = _prove_run([sys.executable, GLASS, "prove", _rr_path, "x=8", "y=3", "--cross-check"],
                         capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_rr, "record result: order(8,3) -> Bounds { lo: 3, hi: 8 } ACCEPT (field-named display)"):
        rr_ok = (_rr.returncode == 0) and ("result:  Bounds { lo: 3, hi: 8 }" in _rr.stdout) and ("THIRD LINEAGE AGREES" in _rr.stdout)
        print(f"  {'OK ' if rr_ok else 'FAIL'}  record result: order(8,3) -> Bounds {{ lo: 3, hi: 8 }} ACCEPT (field-named display)")
        if not rr_ok:
            print(f"        rc={_rr.returncode}  out: {_rr.stdout.strip()[-260:]}  err: {_rr.stderr.strip()[-150:]}")
            failures += 1
    # A tuple with a NON-scalar component (a string) is not bindable this way -> ABSTAIN (the scalar
    # multi-wire guard catches it; never a wrong proof). Restricts the feature to scalar components.
    with _tf_sr.NamedTemporaryFile("w", suffix=".glass", delete=False) as _nsf:
        _nsf.write('fn p(a: Int) : (Int, String) = (a + 1, "x")\np(x)\n')
        _ns_path = _nsf.name
    _ns = _prove_run([sys.executable, GLASS, "prove", _ns_path, "x=5"],
                         capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_ns, "tuple result: a non-scalar component (string) ABSTAINs (scalar components only)"):
        ns_ok = ("verdict: ABSTAIN" in _ns.stdout) and ("proof:   ACCEPT" not in _ns.stdout)
        print(f"  {'OK ' if ns_ok else 'FAIL'}  tuple result: a non-scalar component (string) ABSTAINs (scalar components only)")
        if not ns_ok:
            print(f"        rc={_ns.returncode}  out: {_ns.stdout.strip()[-260:]}  err: {_ns.stderr.strip()[-150:]}")
            failures += 1

    # --zk hiding on a LARGE circuit (v5.118 audit-HIGH fix): a comparison is ~700 gates, so the old
    # `targetN - glen(gs)` gave ZERO dummy rows yet still labelled the proof "zero-knowledge". zk_pad_k
    # now floors the dummy-row count at 256 (> the ~170 opening surface), so --zk genuinely hides any
    # circuit size. This gate is also the first to exercise the (previously untested) --zk path.
    with _tf_sr.NamedTemporaryFile("w", suffix=".glass", delete=False) as _zkf:
        _zkf.write("a < b\n")
        _zk_path = _zkf.name
    _zk = _prove_run([sys.executable, GLASS, "prove", "--zk", _zk_path, "a=3", "b=5"],
                         capture_output=True, text=True, cwd=ROOT)
    if not _heavy_skipped(_zk, "--zk hiding on a ~700-gate comparison ACCEPTs with genuine padding (audit-HIGH fix)"):
        zk_ok = (_zk.returncode == 0) and ("proof:   ACCEPT" in _zk.stdout) and ("zero-knowledge" in _zk.stdout)
        print(f"  {'OK ' if zk_ok else 'FAIL'}  --zk hiding on a ~700-gate comparison ACCEPTs with genuine padding (audit-HIGH fix)")
        if not zk_ok:
            print(f"        rc={_zk.returncode}  out: {_zk.stdout.strip()[-260:]}  err: {_zk.stderr.strip()[-150:]}")
            failures += 1

    # The unboxed single-Int Goldilocks field (goldw_*) must agree with the trusted
    # base-2^16 limb field (gold_*) and obey the field laws — the load-bearing
    # correctness of the "unbox the field" speed cut. (Interpreter check; the native
    # half of the difftest + the bootstrap fixpoint are run separately.)
    rc, out, err = run_file(os.path.join(EX, "prove", "goldw_difftest.glass"))
    gw_ok = (rc == 0) and ("CHECK" in out) and (" F" not in out)
    print(f"  {'OK ' if gw_ok else 'FAIL'}  goldw_* unboxed field == gold_* (field laws hold)")
    if not gw_ok:
        print(f"        rc={rc}; any 'CHECK ... F' is a field mismatch")
        print(f"        out: {out.strip()[-200:]}  err: {err.strip()[-150:]}")
        failures += 1

    # LogUp range argument (v5.105): the cheap-range frontier's foundation — a standalone
    # log-derivative range-lookup over Goldilocks / F_{p^2}, soundness-vetted by an adversarial
    # design panel (the DENSE literal table closes the sparse-support self-cancellation hole that
    # would otherwise ACCEPT an out-of-range value). Interpreter check; the native byte-identical
    # dogfood runs via run_native.sh separately. Honest in-range -> match; out-of-range value AND
    # forged multiplicity -> no-match (caught); duplicates handled; degenerate beta -> ABSTAIN.
    rc, out, err = run_file(os.path.join(EX, "frost", "frost_logup.glass"))
    lu_ok = (rc == 0) \
        and ("correct m -> sums match: yes" in out) \
        and ("[3,7,16] (16 >= 2^4)      -> sums match: no" in out) \
        and ("(m_7 claimed 1, is 2)    -> sums match: no" in out) \
        and ("(m_3 claimed 2, is 1)    -> sums match: no" in out) \
        and ("[5,5,5,5], m_5 = 4           -> sums match: yes" in out) \
        and ("-> abstain (do NOT divide): abstain" in out)
    print(f"  {'OK ' if lu_ok else 'FAIL'}  LogUp range argument: in-range ACCEPT, out-of-range + forged-m REJECT, degenerate-beta ABSTAIN")
    if not lu_ok:
        print(f"        rc={rc}  out: {out.strip()[-300:]}  err: {err.strip()[-150:]}")
        failures += 1

    # LogUp running-sum (AIR) form (v5.106): the integration-shaped step — the lookup as a committed
    # running-sum column S with boundary (S_0=S_N=0) + transition ((S_{k+1}-S_k)(beta-v_k)=num_k)
    # constraints, like the PLONK grand-product Z. Demonstrates THE integration's central soundness
    # obligation: a forged S=0 FOOLS a boundary-only check (would certify an out-of-range lookup) but
    # is CAUGHT by the transition constraint. Interpreter check; native byte-identical dogfood separate.
    rc, out, err = run_file(os.path.join(EX, "frost", "frost_logup_air.glass"))
    la_ok = (rc == 0) \
        and ("boundary yes, transition yes  -> SOUND verdict: yes" in out) \
        and ("boundary no (S_N != 0)" in out) \
        and ("boundary-ONLY check (the unsound shortcut): yes" in out) \
        and ("+ TRANSITION constraint (the fix):         no" in out) \
        and ("SOUND verdict (boundary AND transition):   no" in out)
    print(f"  {'OK ' if la_ok else 'FAIL'}  LogUp running-sum: honest ACCEPT, out-of-range REJECT, forged-S=0 fools boundary-only but transition catches it")
    if not la_ok:
        print(f"        rc={rc}  out: {out.strip()[-320:]}  err: {err.strip()[-150:]}")
        failures += 1

    # LogUp committed + Fiat-Shamir (v5.107): closes the standalone LogUp arc — beta is derived by
    # hashing a commitment to the whole trace (MiMC, fresh tags 141/142), so the prover commits BEFORE
    # knowing beta and cannot adapt the trace to a lucky beta (commit-then-challenge soundness, like the
    # Goldilocks STARK's beta_of_root_g). Interpreter check; native byte-identical dogfood separate.
    rc, out, err = run_file(os.path.join(EX, "frost", "frost_logup_committed.glass"))
    lc_ok = (rc == 0) \
        and ("denominators invertible): yes" in out) \
        and ("sums match: yes   (ACCEPT)" in out) \
        and ("sums match: no   (no => caught; 16 has no table partner" in out)
    print(f"  {'OK ' if lc_ok else 'FAIL'}  LogUp committed+Fiat-Shamir: beta bound to the trace, honest ACCEPT, out-of-range REJECT (prover can't pick beta)")
    if not lc_ok:
        print(f"        rc={rc}  out: {out.strip()[-320:]}  err: {err.strip()[-150:]}")
        failures += 1

    # The native Poseidon-permutation intrinsic (poseidon_perm / q_poseidon_perm — the
    # "cut the rope" hash speed-up) must hit the Plonky2 known-answer anchor AND match a
    # hand-written Glass goldw_* reference permutation. (Interpreter check; the native half
    # + the bootstrap fixpoint are run separately; full byte-identity is in the difftest doc.)
    rc, out, err = run_file(os.path.join(EX, "prove", "poseidon_difftest.glass"))
    pp_ok = (rc == 0) and ("CHECK anchor T" in out) and (" F" not in out)
    print(f"  {'OK ' if pp_ok else 'FAIL'}  poseidon_perm == Plonky2 anchor + Glass goldw reference perm")
    if not pp_ok:
        print(f"        rc={rc}; anchor or reference-perm mismatch")
        print(f"        out: {out.strip()[-200:]}  err: {err.strip()[-150:]}")
        failures += 1

    # The native Poseidon2 intrinsic (poseidon2_perm / q_poseidon2_perm — the Plonky3 hash,
    # staged for the bridge migration) must hit Plonky3's published t=12 permutation vector.
    rc, out, err = run_file(os.path.join(EX, "prove", "poseidon2_difftest.glass"))
    p2_ok = (rc == 0) and ("CHECK plonky3_anchor T" in out) and (" F" not in out)
    print(f"  {'OK ' if p2_ok else 'FAIL'}  poseidon2_perm == Plonky3 published t=12 vector")
    if not p2_ok:
        print(f"        rc={rc}; Plonky3 anchor mismatch")
        print(f"        out: {out.strip()[-200:]}  err: {err.strip()[-150:]}")
        failures += 1

    # The native coset-NTT / low-degree-extension intrinsic (ntt_lde / q_ntt_lde — the rope-2
    # cut that removes the O(n^2) polynomial LDE) must equal the naive goldw coset evaluation
    # (eval[k] = P(7*omega^k)) AND be byte-identical interp vs native.
    rc, out, err = run_file(os.path.join(EX, "prove", "ntt_difftest.glass"))
    nt_ok = (rc == 0) and ("CHECK ntt8  T" in out) and (" F" not in out)
    print(f"  {'OK ' if nt_ok else 'FAIL'}  ntt_lde coset-NTT == naive goldw eval_on_dom (LDE)")
    if not nt_ok:
        print(f"        rc={rc}; an 'ntt.. F' is an NTT/eval mismatch")
        print(f"        out: {out.strip()[-200:]}  err: {err.strip()[-150:]}")
        failures += 1

    # The O(1)-indexable vector (to_vec/vget — the rope-3 cut that removes the prover's
    # pervasive O(n^2) wnth indexing) must agree with positional list indexing for every index.
    rc, out, err = run_file(os.path.join(EX, "prove", "vget_difftest.glass"))
    vg_ok = (rc == 0) and ("CHECK vget_all T" in out) and (" F" not in out)
    print(f"  {'OK ' if vg_ok else 'FAIL'}  vget/to_vec O(1) index == positional list index")
    if not vg_ok:
        print(f"        rc={rc}; a 'vget.. F' is an index mismatch")
        print(f"        out: {out.strip()[-200:]}  err: {err.strip()[-150:]}")
        failures += 1

    # The Measuring Reed: the bit-security re-derivation must be exact integer arithmetic tied to
    # the live params (ilog2(grind_modulus)=12; q=82 -> 80 provable / 135 list-decoding). The
    # end-to-end 'security:' line on a real Goldilocks ACCEPT is validated by the native prove path.
    rc, out, err = run_file(os.path.join(EX, "prove", "measure_difftest.glass"))
    mr_ok = (rc == 0) and ("CHECK provable80 T" in out) and (" F" not in out)
    print(f"  {'OK ' if mr_ok else 'FAIL'}  measure: bit-security re-derivation (82q -> 80/135, grind=12)")
    if not mr_ok:
        print(f"        rc={rc}; a 'CHECK .. F' is a security re-derivation drift")
        print(f"        out: {out.strip()[-200:]}  err: {err.strip()[-150:]}")
        failures += 1

    # The Name — Glass's content-addressed identity must match name/NAME (the committed
    # fingerprint is kept current, lockfile-style: regenerate with `glass name --write`).
    _root = os.path.dirname(os.path.dirname(os.path.abspath(__file__)))
    _nm = subprocess.run([sys.executable, os.path.join(_root, "name", "glass_name.py"), "--check"],
                         capture_output=True, text=True)
    nm_ok = (_nm.returncode == 0)
    print(f"  {'OK ' if nm_ok else 'FAIL'}  the Name: content-addressed identity matches name/NAME")
    if not nm_ok:
        print(f"        {(_nm.stdout + _nm.stderr).strip()[-220:]}")
        print(f"        (a canonical artifact changed — regenerate with: python3 name/glass_name.py --write)")
        failures += 1

    # The Preserved Tablet — the append-only proof-verdict ledger: determinism, inclusion
    # proofs verify, a forged entry does not, and tampering a past entry changes the root.
    _tab = subprocess.run([sys.executable, os.path.join(_root, "ledger", "tablet.py"), "--selftest"],
                          capture_output=True, text=True)
    tb_ok = (_tab.returncode == 0) and ("CHECK tablet T" in _tab.stdout)
    print(f"  {'OK ' if tb_ok else 'FAIL'}  the Preserved Tablet: append-only ledger (inclusion + tamper-evidence)")
    if not tb_ok:
        print(f"        {(_tab.stdout + _tab.stderr).strip()[-220:]}")
        failures += 1

    # Opening the Seals — selective disclosure over a blinded Poseidon commitment: a revealed
    # field binds to the root, a tampered value/path does not, a hidden change moves the root.
    _sl = subprocess.run([sys.executable, os.path.join(_root, "seal", "reveal.py"), "--selftest"],
                         capture_output=True, text=True)
    sl_ok = (_sl.returncode == 0) and ("CHECK seal T" in _sl.stdout)
    print(f"  {'OK ' if sl_ok else 'FAIL'}  Opening the Seals: selective disclosure (bind + hide + tamper-evidence)")
    if not sl_ok:
        print(f"        {(_sl.stdout + _sl.stderr).strip()[-220:]}")
        failures += 1

    # The second verifier's hash must stay faithful to the third-party vector. Pentecost's
    # keystone (independent Poseidon2 == Plonky3 t=12 out12) was NOT gated by the suite before
    # (the v5.56.0 gate-coverage lesson) — a Pentecost-side constant/matrix error would be invisible.
    _pk = subprocess.run([sys.executable, "-m", "pentecost.test_poseidon"],
                         capture_output=True, text=True, cwd=_root)
    pk_ok = (_pk.returncode == 0) and ("KEYSTONE OK" in _pk.stdout)
    print(f"  {'OK ' if pk_ok else 'FAIL'}  Pentecost keystone: independent Poseidon2 == Plonky3 t=12 vector")
    if not pk_ok:
        print(f"        {(_pk.stdout + _pk.stderr).strip()[-220:]}")
        failures += 1

    # The Third Witness: the reference interpreter (glass.py) re-executes f independently and
    # binds the proof's public result — a lineage separate from the bridge's heval AND cgen.
    # Gate the evaluator logic directly (fast; the end-to-end --witness3 line is validated natively).
    _w3check = ("import glass; "
               "assert glass._witness3_eval('a + b', [('a',3),('b',5)]) == 8; "
               "assert glass._witness3_eval('a < b', [('a',3),('b',5)]) == 1; "
               "assert glass._witness3_eval('a < b', [('a',5),('b',3)]) == 0; "
               "assert glass._witness3_eval('a / b', [('a',17),('b',5)]) == 3; "
               "assert glass._witness3_eval('a % b', [('a',17),('b',5)]) == 2; "
               "assert glass._witness3_eval('slt(a, b)', [('a',-5),('b',3)]) == 1; "
               "assert glass._witness3_eval('slt(a, b)', [('a',3),('b',-5)]) == 0; "
               "assert glass._witness3_eval('sgt(a, b)', [('a',-5),('b',-9)]) == 1; "
               "assert glass._witness3_eval('sle(a, b)', [('a',-5),('b',-5)]) == 1; "
               "assert glass._witness3_eval('sge(a, b)', [('a',-9),('b',-5)]) == 0; "
               "assert glass._witness3_eval('sdiv(a, b)', [('a',-17),('b',5)]) == -3; "
               "assert glass._witness3_eval('smod(a, b)', [('a',-17),('b',5)]) == -2; "
               "assert glass._witness3_eval('sdiv(a, b)', [('a',17),('b',-5)]) == -3; "
               "assert glass._witness3_eval('smod(a, b)', [('a',-17),('b',-5)]) == -2; "
               "assert glass._witness3_eval('sabs(a)', [('a',-5)]) == 5; "
               "assert glass._witness3_eval('sabs(a - b)', [('a',3),('b',17)]) == 14; "
               "assert glass._witness3_eval('smin(a, b)', [('a',-5),('b',3)]) == -5; "
               "assert glass._witness3_eval('smax(a, b)', [('a',-5),('b',3)]) == 3; "
               "assert glass._witness3_eval('(h * 31 + c) % 1000003', [('h',12345),('c',67)]) == 382762; "
               "assert glass._witness3_eval(open('examples/prove/gcd_prove.glass').read(), [('x',48),('y',18)]) == 6; "
               "assert glass._witness3_eval(open('examples/prove/gcd_prove.glass').read(), [('x',48),('y',36)]) == 12; "
               "print('W3 OK')")
    _w3p = subprocess.run([sys.executable, "-c", _w3check], capture_output=True, text=True, cwd=_root)
    w3 = (_w3p.returncode == 0) and ("W3 OK" in _w3p.stdout)
    if not w3:
        print(f"        {(_w3p.stdout + _w3p.stderr).strip()[-200:]}")
    print(f"  {'OK ' if w3 else 'FAIL'}  the Third Witness: reference-interpreter re-execution (a+b=8, 3<5=1, 5<3=0, 17/5=3, 17%5=2, slt(-5,3)=1, sge(-9,-5)=0)")
    if not w3:
        failures += 1

    # H3 milestone — in-circuit Merkle membership: the path-hashing program must be deterministic
    # and BINDING (a different leaf or sibling yields a different root). The full in-circuit proof
    # is validated natively (~39s); here the membership LOGIC is gated fast via the interpreter.
    _mmcheck = ("import glass; src=open('examples/prove/merkle_member.glass').read(); "
                "b=[('leaf',42),('s0',7),('d0',0),('s1',99),('d1',1)]; r=glass._witness3_eval(src,b); "
                "assert r is not None and r==glass._witness3_eval(src,b); "
                "assert r!=glass._witness3_eval(src,[('leaf',43)]+b[1:]); "
                "assert r!=glass._witness3_eval(src,b[:1]+[('s0',8)]+b[2:]); print('MM OK')")
    _mmp = subprocess.run([sys.executable, "-c", _mmcheck], capture_output=True, text=True, cwd=_root)
    mm_ok = (_mmp.returncode == 0) and ("MM OK" in _mmp.stdout)
    print(f"  {'OK ' if mm_ok else 'FAIL'}  H3: in-circuit Merkle membership (deterministic + binding path-hash)")
    if not mm_ok:
        print(f"        {(_mmp.stdout + _mmp.stderr).strip()[-200:]}")
        failures += 1

    # H3 milestone B1 (v5.126) — AUTHENTICATED FRI FOLD: two openings are each Merkle-authenticated AND
    # consumed by the exact FRI fold in ONE proven circuit (the structural heart of recursion). The
    # public result is (root_fx, root_fmx, fold); the fold of fx=10,fmx=20,beta=7,x=1 is exactly
    # (10+20)/2 + 7*(10-20)/2 = 15-35 = -20, computed mod p via the supplied field inverses. A native
    # prove (the int64-overflowing x^7 + huge inverses make this circuit-faithful, NOT witness3-agreeing,
    # like merkle_member). ACCEPT + the exact result pins the composed circuit; a lowering regression
    # would change the fold or the roots.
    _mfp = _prove_run([sys.executable, GLASS, "prove", os.path.join(EX, "prove", "merkle_fold_member.glass"),
                       "fx=10", "fmx=20", "sa=3", "da=0", "sc=5", "dc=1", "beta=7", "x=1",
                       "inv2=9223372034707292161", "inv2x=9223372034707292161"])
    if not _heavy_skipped(_mfp, "H3: authenticated FRI fold (membership + exact fold composed in one circuit) -> ACCEPT, fold=-20"):
        mf_ok = ("proof:   ACCEPT" in _mfp.stdout) and ("3264941531247994665, 6297486681267911818, -20)" in _mfp.stdout)
        print(f"  {'OK ' if mf_ok else 'FAIL'}  H3: authenticated FRI fold (membership + exact fold composed in one circuit) -> ACCEPT, fold=-20")
        if not mf_ok:
            print(f"        rc={_mfp.returncode}  out: {_mfp.stdout.strip()[-220:]}  err: {_mfp.stderr.strip()[-120:]}")
            failures += 1

    # H3 milestone B2 (v5.127) — the REAL production Poseidon2 (t=12, 30 rounds, 130 constants, M_E/M_I)
    # as a provable ~1.9k-gate circuit (vs merkle_member's reduced toy hash). poseidon2_node_check.py
    # proves it for input lanes 0..11 and cross-checks all 12 output lanes against the independent
    # from-scratch Poseidon2 spec (pentecost/poseidon.py) -- the right oracle, since the x^7 chains +
    # ~2^64 constants make the circuit faithful but NOT witness3-agreeing. The honest per-node cost anchor
    # for the H3 recursive-verifier estimate. (Native prove ~1-2 min; SKIPs on an env signal-kill.)
    _pn = _prove_run([sys.executable, os.path.join("fuzz", "poseidon2_node_check.py")])
    if not _heavy_skipped(_pn, "H3: real Poseidon2 (t=12, 30 rounds) in-circuit == independent spec on all 12 lanes"):
        pn_ok = (_pn.returncode == 0) and ("POSEIDON2-NODE: PASS" in _pn.stdout or "POSEIDON2-NODE: SKIP" in _pn.stdout)
        print(f"  {'OK ' if pn_ok else 'FAIL'}  H3: real Poseidon2 (t=12, 30 rounds) in-circuit == independent spec on all 12 lanes")
        if not pn_ok:
            print(f"        rc={_pn.returncode}  out: {(_pn.stdout + _pn.stderr).strip()[-260:]}")
            failures += 1

    # Adversarial fuzz of the second witness: a TAMPERED proof must never verify. tamper_pentecost.py
    # perturbs random single tokens of a committed honest proof and asserts the independent Pentecost
    # verifier REJECTs every one (0 wrong-ACCEPTs). A 1600-tamper/16-seed campaign (workflow whrym5q4r,
    # v5.78.0) was clean; the suite gates a fast slice so a future verify_b3 regression that makes a
    # forged proof pass cannot land silently. (Asserts the honest baseline ACCEPTs first.)
    _tp = subprocess.run([sys.executable, os.path.join("fuzz", "tamper_pentecost.py"), "20251", "6"],
                         capture_output=True, text=True, cwd=_root)
    tp_ok = (_tp.returncode == 0) and ("0 wrong-ACCEPTs" in _tp.stdout)
    print(f"  {'OK ' if tp_ok else 'FAIL'}  tamper-fuzz: independent verifier REJECTs every tampered proof")
    if not tp_ok:
        print(f"        {(_tp.stdout + _tp.stderr).strip()[-220:]}")
        failures += 1

    # Statement-binding: tampering the PUBLIC CLAIM (the GATES region — gate list + claimed result)
    # must REJECT. A break here is catastrophic (a true proof passed off as proving a false claim),
    # so it's fuzzed too. A 640-tamper/8-seed campaign (v5.80.0) was clean; the suite gates a slice.
    _tc = subprocess.run([sys.executable, os.path.join("fuzz", "tamper_pentecost.py"), "20251", "10", "--claim"],
                         capture_output=True, text=True, cwd=_root)
    tc_ok = (_tc.returncode == 0) and ("0 wrong-ACCEPTs" in _tc.stdout)
    print(f"  {'OK ' if tc_ok else 'FAIL'}  statement-binding: tampered public claim REJECTs (gates region)")
    if not tc_ok:
        print(f"        {(_tc.stdout + _tc.stderr).strip()[-220:]}")
        failures += 1

    # Multi-shape corpus: the differential + tamper guarantees, broadened beyond the single a+b
    # shape they originally ran on. For every committed proof fixture (a+b, a*b, a*a+b, a<b, a/b,
    # string-eq, a record destructure, AND a string-VALUED result — a multi-wire public claim) the
    # independent Pentecost verifier must ACCEPT the honest proof and REJECT a tamper in either the
    # proof region or the public-claim region. Catches a verify_b3 bug that only manifests on some
    # circuit shapes (more gates, different gate kinds, multi-wire string/record output bindings) —
    # invisible to a single-fixture gate.
    _cc = subprocess.run([sys.executable, os.path.join("fuzz", "corpus_check.py")],
                         capture_output=True, text=True, cwd=_root)
    cc_ok = (_cc.returncode == 0) and ("0 failures" in _cc.stdout)
    print(f"  {'OK ' if cc_ok else 'FAIL'}  proof corpus: two verifiers agree + tamper-rejected across shapes")
    if not cc_ok:
        print(f"        {(_cc.stdout + _cc.stderr).strip()[-220:]}")
        failures += 1

    # Native round-trip (v5.123): the strongest proof-FORMAT gate. The NATIVE Glass prover EMITS a real
    # proof token stream and the INDEPENDENT Pentecost verifier parses + checks it (honest ACCEPT, every
    # tamper REJECT). It is the only gate that exercises emit <-> parse TOGETHER, so it catches a
    # serialization drift the parse-only corpus_check cannot — a denser-encoding change that emits AND
    # parses consistently-wrong sails through corpus_check but fails here (the "green-but-broken" hazard
    # the v5.122 proof-size change had to guard by hand). Does a native compile (~1-2 min); timeout-guarded
    # so an under-load native stall SKIPs rather than hangs the suite. (Was "run separately"; wired in now
    # that the v5.122 difftest segfault — a stale input type — is fixed.)
    try:
        _dt = subprocess.run(["bash", os.path.join("pentecost", "difftest.sh")],
                             capture_output=True, text=True, cwd=_root, timeout=PROVE_TIMEOUT)
        if _dt.returncode >= 128:
            print(f"  OK   native round-trip: difftest emit<->Pentecost  (SKIPPED: native stall rc={_dt.returncode} — env-limited)")
        else:
            dt_ok = (_dt.returncode == 0) and ("PENTECOST DIFFERENTIAL PASSED" in _dt.stdout)
            print(f"  {'OK ' if dt_ok else 'FAIL'}  native round-trip: difftest emit<->Pentecost (honest ACCEPT + tampers REJECT)")
            if not dt_ok:
                print(f"        {(_dt.stdout + _dt.stderr).strip()[-260:]}")
                failures += 1
    except subprocess.TimeoutExpired:
        print("  OK   native round-trip: difftest emit<->Pentecost  (SKIPPED: timeout — env-limited)")

    # Plain-name surface (docs/naming.md): the public CLI exposes neutral names; the thematic
    # names remain as aliases. `glass help` must list the plain names, and each plain alias must
    # be identical to its thematic counterpart (so neither audience drifts out of test coverage).
    def _glass(*a):
        return subprocess.run([sys.executable, "glass.py", *a], capture_output=True, text=True, cwd=_root)
    _help = _glass("help")
    _fp_plain, _fp_them = _glass("fingerprint"), _glass("name")
    alias_ok = (
        _help.returncode == 0
        and all(w in _help.stdout for w in ("fingerprint", "ledger", "disclose", "verify"))
        and _fp_plain.stdout == _fp_them.stdout          # `fingerprint` ≡ `name`
        and _fp_plain.returncode == _fp_them.returncode)
    print(f"  {'OK ' if alias_ok else 'FAIL'}  plain-name surface: `help` + fingerprint/ledger/disclose aliases")
    if not alias_ok:
        print(f"        {(_help.stdout + _help.stderr).strip()[-200:]}")
        failures += 1

    total = (len(POSITIVE) + len(NEGATIVE) +
             len(inline_positive) + len(prism_checks) + len(repl_cases) + 84)  # +84: ... + v5.126 H3-B1 + v5.127 H3-B2 real-Poseidon2 + v5.128 builtin-list-threading-ABSTAIN + v5.129 substring-OOB-clamp + start>end-ABSTAIN + v5.130 ADT-layout-overflow-ABSTAIN (recursive-ADT non-last + String-field, no silent mis-offset)
    passed = total - failures
    quartz_failures = run_quartz_tests()
    failures += quartz_failures
    total += 174  # quartz: + 2 v4.73 (tuple-ctor dispatch + final `let _` discard); + 3 v5.54 glued-minus split; + 1 v5.57 shift-count mask
    passed = total - failures
    print(f"\n{passed}/{total} passed")
    return 0 if failures == 0 else 1


def run_quartz_tests() -> int:
    """Quartz v3.0: compile each .glass source to a native binary, run it,
    check stdout matches expectation. Each case proves codegen handles a
    specific language construct end-to-end."""
    import tempfile
    QUARTZ = os.path.join(ROOT, "quartz.py")
    print("== quartz native-compile cases ==")
    cases = [
        ("int literal",              "42\n",                                   "42\n"),
        ("arithmetic precedence",    "1 + 2 * 3\n",                            "7\n"),
        # Glued binary minus: `10-3` is subtraction, not `10` then a negative
        # literal `-3` (the lexer used to drop the subtraction). After a value
        # token a `-N` re-splits into MINUS + N; a prefix `-N` stays a literal.
        ("glued minus after int (lexer fix)",        "10-3\n",                 "7\n"),
        ("glued minus after ident; prefix -N kept",  "let n = -5\nn-3\n",      "-8\n"),
        ("glued minus after paren",                  "(2 + 3)-1\n",            "4\n"),
        ("prefix -N after = preserved, glued after int", "let n = -2\n100-1 + n\n", "97\n"),
        # Shift count masked to 6 bits in the emitted C (& 63): a shift of an
        # int64 by >= 64 is UB in C; the mask makes it well-defined and equal
        # to the host interpreter (b_bit_shl). 1 << (64 & 63) == 1 << 0 == 1.
        ("shift count masked to 6 bits (compiled, UB-free)", "bit_shl(1, 64)\n", "1\n"),
        ("top-level lets",           "let x = 5\nlet y = 10\nx + y\n",         "15\n"),
        ("if-then-else as expr",     "if 3 < 5 then 100 else 200\n",           "100\n"),
        ("nested let-in",            "let r = (let x = 7 in x * 3)\nr + 1\n",  "22\n"),
        ("string literal",           '"hello"\n',                              "hello\n"),
        # v3.1 — functions
        ("fn add",
         "fn add(x: Int, y: Int) : Int = x + y\nadd(3, 4)\n",
         "7\n"),
        ("fn recursion (fact)",
         "fn fact(n: Int) : Int = if n < 2 then 1 else n * fact(n - 1)\nfact(5)\n",
         "120\n"),
        ("fn calls fn",
         "fn double(x: Int) : Int = x * 2\nfn quad(x: Int) : Int = double(double(x))\nquad(3)\n",
         "12\n"),
        ("fn mutual recursion",
         "fn is_even(n: Int) : Bool = if n == 0 then true else is_odd(n - 1)\n"
         "fn is_odd(n: Int) : Bool = if n == 0 then false else is_even(n - 1)\n"
         "is_even(10)\n",
         "true\n"),
        ("string concat ++",
         'fn greet(name: String) : String = "hello, " ++ name\ngreet("world")\n',
         "hello, world\n"),
        ("C keyword name collision",
         "fn double(x: Int) : Int = x * 2\ndouble(21)\n",
         "42\n"),
        # v3.2 — ADTs + pattern matching
        ("ADT enum-style match",
         "type Color = Red | Green | Blue\n"
         "match (Red) { Red => 1; Green => 2; Blue => 3 }\n",
         "1\n"),
        ("ADT with payload + match",
         "type Box = Empty | Holds(Int)\n"
         "match Holds(42) { Holds(n) => n; Empty => 0 }\n",
         "42\n"),
        ("ADT multi-field variant",
         "type Bag = Empty | Twin(Int, Int)\n"
         "match Twin(10, 20) { Empty => 0; Twin(a, b) => a + b }\n",
         "30\n"),
        ("fn returns ADT",
         "type Color = Red | Green | Blue\n"
         "fn classify(n: Int) : Color = if n > 0 then Red else Blue\n"
         "match classify(-5) { Red => 1; Green => 2; Blue => 3 }\n",
         "3\n"),
        ("ADT wild pattern ignores payload",
         "type Outcome = Done(Int) | Failed(String)\n"
         'fn safe_div(n: Int, d: Int) : Outcome = if d == 0 then Failed("oops") else Done(n / d)\n'
         "match safe_div(100, 0) { Done(v) => v; Failed(_) => -1 }\n",
         "-1\n"),
        # v3.3 — records
        ("record construct + field access",
         "type Point = { x: Int, y: Int }\n"
         "let p = Point { x: 3, y: 4 }\n"
         "p.x + p.y\n",
         "7\n"),
        ("record as fn parameter",
         "type Point = { x: Int, y: Int }\n"
         "fn dot(a: Point, b: Point) : Int = a.x * b.x + a.y * b.y\n"
         "let p = Point { x: 3, y: 4 }\n"
         "let q = Point { x: 5, y: 6 }\n"
         "dot(p, q)\n",
         "39\n"),
        ("record destructure in match",
         "type User = { id: Int, name: String }\n"
         'let u = User { id: 42, name: "alice" }\n'
         "match u { User { id, name } => id }\n",
         "42\n"),
        ("record inside ADT variant",
         "type User = { id: Int, name: String }\n"
         "type Outcome = Found(User) | NotFound\n"
         "fn lookup(id: Int) : Outcome = "
         'if id == 1 then Found(User { id: 1, name: "alice" }) else NotFound\n'
         'match lookup(1) { Found(u) => u.name; NotFound => "missing" }\n',
         "alice\n"),
        ("chained field access (nested records)",
         "type Point = { x: Int, y: Int }\n"
         "type Rect = { tl: Point, br: Point }\n"
         "let r = Rect { tl: Point { x: 0, y: 0 }, br: Point { x: 1920, y: 1080 } }\n"
         "r.br.x - r.tl.x\n",
         "1920\n"),
        # v3.4 — generics
        ("generic ADT (user-declared)",
         "type Maybe<T> = Nope | Yep(T)\n"
         "match Yep(42) { Yep(n) => n; Nope => 0 }\n",
         "42\n"),
        ("generic record",
         "type Box<T> = { contents: T }\n"
         "let b = Box { contents: 7 }\n"
         "b.contents\n",
         "7\n"),
        ("prelude Option<Int>",
         "let o : Option<Int> = Some(42)\n"
         "match o { Some(n) => n; None => 0 }\n",
         "42\n"),
        ("prelude Result<Int, String>",
         "fn safe_div(n: Int, d: Int) : Result<Int, String> =\n"
         '  if d == 0 then Err("div by zero") else Ok(n / d)\n'
         "match safe_div(100, 0) { Ok(v) => v; Err(_) => -1 }\n",
         "-1\n"),
        ("generic record as fn parameter",
         "type Box<T> = { contents: T }\n"
         "fn unbox(b: Box<Int>) : Int = b.contents\n"
         "unbox(Box { contents: 99 })\n",
         "99\n"),
        # v3.4.1 — generic functions
        ("generic fn (Int instantiation)",
         "fn id<T>(x: T) : T = x\n"
         "id(42)\n",
         "42\n"),
        ("generic fn (String instantiation)",
         "fn id<T>(x: T) : T = x\n"
         'id("hello")\n',
         "hello\n"),
        ("generic fn calling generic fn",
         "fn id<T>(x: T) : T = x\n"
         "fn through<A>(x: A) : A = id(x)\n"
         "through(99)\n",
         "99\n"),
        ("generic fn returning ADT",
         "fn wrap<T>(x: T) : Option<T> = Some(x)\n"
         "match wrap(42) { Some(n) => n; None => 0 }\n",
         "42\n"),
        ("generic fn over ADT scrutinee",
         "fn unwrap_or<T>(opt: Option<T>, default: T) : T =\n"
         "  match opt { Some(x) => x; None => default }\n"
         "unwrap_or(Some(42), 0)\n",
         "42\n"),
        ("generic fn — None instantiation",
         "fn unwrap_or<T>(opt: Option<T>, default: T) : T =\n"
         "  match opt { Some(x) => x; None => default }\n"
         'unwrap_or(None, "missing")\n',
         "missing\n"),
        # v4.30 — Quartz gains tuples. Compile a fn that returns a
        # tuple, destructure in match, recombine. Tests TupleLit codegen
        # + TyTuple in fn signatures + tuple pattern destructuring.
        ("tuple construct + destructure (v4.30)",
         "fn pair(a: Int, b: Int) : (Int, Int) = (a, b)\n"
         "match pair(10, 20) { (x, y) => x + y }\n",
         "30\n"),
        ("3-tuple",
         "fn triple(a: Int, b: Int, c: Int) : (Int, Int, Int) = (a, b, c)\n"
         "match triple(100, 20, 3) { (x, y, z) => x + y + z }\n",
         "123\n"),
        ("mixed-type tuple (String, Int)",
         'fn label(n: Int) : (String, Int) = ("answer", n)\n'
         "match label(42) { (k, v) => v }\n",
         "42\n"),
        ("let-bound tuple",
         "fn pair(a: Int, b: Int) : (Int, Int) = (a, b)\n"
         "let p : (Int, Int) = pair(7, 3)\n"
         "match p { (x, y) => x - y }\n",
         "4\n"),
        # v4.31 — Quartz gains lists. Cons-chain representation in
        # q_value_t (Nil has num_fields=0; Cons has num_fields=2 with
        # head at fields[0] and tail at fields[1]). Tests recursive
        # walking, empty-list base case, length count, string element.
        ("list literal + recursive sum (v4.31)",
         "fn sum(xs: List<Int>) : Int =\n"
         "  match xs {\n"
         "    []        => 0;\n"
         "    [h, ...t] => h + sum(t)\n"
         "  }\n"
         "sum([1, 2, 3, 4, 5])\n",
         "15\n"),
        ("empty list (nil base case)",
         "fn sum(xs: List<Int>) : Int =\n"
         "  match xs {\n"
         "    []        => 0;\n"
         "    [h, ...t] => h + sum(t)\n"
         "  }\n"
         "sum([])\n",
         "0\n"),
        ("list length via wildcard head",
         "fn length(xs: List<Int>) : Int =\n"
         "  match xs {\n"
         "    []        => 0;\n"
         "    [_, ...t] => 1 + length(t)\n"
         "  }\n"
         "length([10, 20, 30, 40, 50, 60, 70])\n",
         "7\n"),
        ("list of strings — first element",
         'fn first_or(xs: List<String>, default: String) : String =\n'
         "  match xs {\n"
         "    []        => default;\n"
         "    [h, ..._] => h\n"
         "  }\n"
         'first_or(["alpha", "beta", "gamma"], "none")\n',
         "alpha\n"),
        # v4.32 — Quartz ++ dispatches on operand type. Pre-v4.32 always
        # called quartz_str_concat, which silently miscompiled list ++
        # (returned 0 instead of 66). The new path emits quartz_list_concat
        # for list operands.
        ("list ++ via quartz_list_concat (v4.32)",
         "fn sum(xs: List<Int>) : Int =\n"
         "  match xs { [] => 0; [h, ...t] => h + sum(t) }\n"
         "sum([1, 2, 3] ++ [10, 20, 30])\n",
         "66\n"),
        ("list ++ with empty lhs",
         "fn sum(xs: List<Int>) : Int =\n"
         "  match xs { [] => 0; [h, ...t] => h + sum(t) }\n"
         "let empty : List<Int> = []\n"
         "sum(empty ++ [5, 10, 15])\n",
         "30\n"),
        ("list ++ with empty rhs",
         "fn sum(xs: List<Int>) : Int =\n"
         "  match xs { [] => 0; [h, ...t] => h + sum(t) }\n"
         "let empty : List<Int> = []\n"
         "sum([1, 2, 3] ++ empty)\n",
         "6\n"),
        ("string ++ still works (regression guard)",
         'fn greet(name: String) : String = "hello, " ++ name\n'
         'greet("world")\n',
         "hello, world\n"),
        # v4.33 — Quartz `==` becomes type-aware. String compares now
        # use strcmp (content), so concat-then-compare works. The case
        # that returned 0 pre-v4.33 returns 1.
        ("Quartz == on concatenated String (v4.33)",
         "fn ok(b: Bool) : Int = if b then 1 else 0\n"
         'ok(("hel" ++ "lo") == "hello")\n',
         "1\n"),
        ("Quartz != on String content",
         "fn ok(b: Bool) : Int = if b then 1 else 0\n"
         'ok(("hel" ++ "lo") != "world")\n',
         "1\n"),
        # Regression guard: Int and Bool equality must still use plain
        # C `==`. The type-aware dispatch only kicks in for boxed types.
        ("Quartz == on Int still plain compare",
         "fn ok(b: Bool) : Int = if b then 1 else 0\n"
         "ok(42 == 42)\n",
         "1\n"),
        ("Quartz == on Bool still plain compare",
         "fn ok(b: Bool) : Int = if b then 1 else 0\n"
         "ok(true == true)\n",
         "1\n"),
        # v4.34 — Quartz structural == extends to List<P> and
        # Tuple<P, ...> when every P is primitive (Int/Bool/String).
        # The codegen emits a loop (lists) or per-field compare chain
        # (tuples) as statements + a fresh result bool. Pre-v4.34 these
        # all errored loudly via v4.33's TyList/TyTuple arms.
        ("List<Int> == List<Int> same (v4.34)",
         "fn ok(b: Bool) : Int = if b then 1 else 0\n"
         "ok([1, 2, 3] == [1, 2, 3])\n",
         "1\n"),
        ("List<Int> == List<Int> different content",
         "fn ok(b: Bool) : Int = if b then 1 else 0\n"
         "ok([1, 2, 3] == [1, 2, 4])\n",
         "0\n"),
        ("List<Int> == List<Int> different length",
         "fn ok(b: Bool) : Int = if b then 1 else 0\n"
         "ok([1, 2, 3] == [1, 2])\n",
         "0\n"),
        ("List<String> == content compare via concat",
         "fn ok(b: Bool) : Int = if b then 1 else 0\n"
         'ok([("hel" ++ "lo"), ("wor" ++ "ld")] == ["hello", "world"])\n',
         "1\n"),
        ("Tuple<Int, Int> == structural",
         "fn ok(b: Bool) : Int = if b then 1 else 0\n"
         "ok((1, 2) == (1, 2))\n",
         "1\n"),
        ("Tuple<Int, Int> != different",
         "fn ok(b: Bool) : Int = if b then 1 else 0\n"
         "ok((1, 2) != (1, 3))\n",
         "1\n"),
        ("Tuple<String, Int> mixed — content compare",
         "fn ok(b: Bool) : Int = if b then 1 else 0\n"
         'ok(("a" ++ "b", 42) == ("ab", 42))\n',
         "1\n"),
        # v4.35 — recursive structural ==. The primitive-only guards
        # on TyList and TyTuple arms of _emit_eq_atom were dropped, so
        # the existing recursive call dispatches through the type
        # structure. The recursive append order already places inner
        # statements inside the outer loop body — no scope-management
        # changes were needed.
        ("List<List<Int>> == structural (v4.35)",
         "fn ok(b: Bool) : Int = if b then 1 else 0\n"
         "ok([[1, 2], [3, 4]] == [[1, 2], [3, 4]])\n",
         "1\n"),
        ("List<List<Int>> != different inner",
         "fn ok(b: Bool) : Int = if b then 1 else 0\n"
         "ok([[1, 2], [3, 4]] != [[1, 2], [3, 5]])\n",
         "1\n"),
        ("Tuple<List<Int>, Int> mixed",
         "fn ok(b: Bool) : Int = if b then 1 else 0\n"
         "ok(([1, 2, 3], 42) == ([1, 2, 3], 42))\n",
         "1\n"),
        ("List<Tuple<Int, String>> nested tuples in list",
         "fn ok(b: Bool) : Int = if b then 1 else 0\n"
         'ok([(1, "a"), (2, "b")] == [(1, "a"), (2, "b")])\n',
         "1\n"),
        # v4.36 — structural == for records and concrete sum types.
        # Records: field-by-field compare using record_env field types.
        # Sum types: tag check + per-variant field compare. Generic
        # sum types (Option<T>, etc.) still error loudly.
        ("Record == Record same content (v4.36)",
         "type Point = { x: Int, y: Int }\n"
         "fn ok(b: Bool) : Int = if b then 1 else 0\n"
         "ok(Point { x: 1, y: 2 } == Point { x: 1, y: 2 })\n",
         "1\n"),
        ("Record != Record different field",
         "type Point = { x: Int, y: Int }\n"
         "fn ok(b: Bool) : Int = if b then 1 else 0\n"
         "ok(Point { x: 1, y: 2 } != Point { x: 1, y: 3 })\n",
         "1\n"),
        ("Record with String field — content compare",
         "type User = { id: Int, name: String }\n"
         "fn ok(b: Bool) : Int = if b then 1 else 0\n"
         'ok(User { id: 1, name: "alice" } == '
         'User { id: 1, name: "ali" ++ "ce" })\n',
         "1\n"),
        ("Concrete sum type enum",
         "type Color = Red | Green | Blue\n"
         "fn ok(b: Bool) : Int = if b then 1 else 0\n"
         "ok(Red == Red)\n",
         "1\n"),
        ("Concrete sum type different variants",
         "type Color = Red | Green | Blue\n"
         "fn ok(b: Bool) : Int = if b then 1 else 0\n"
         "ok(Red != Blue)\n",
         "1\n"),
        ("Sum type with Int payload same",
         "type Box = Empty | Holds(Int)\n"
         "fn ok(b: Bool) : Int = if b then 1 else 0\n"
         "ok(Holds(42) == Holds(42))\n",
         "1\n"),
        ("Sum type with Int payload different",
         "type Box = Empty | Holds(Int)\n"
         "fn ok(b: Bool) : Int = if b then 1 else 0\n"
         "ok(Holds(42) != Holds(99))\n",
         "1\n"),
        ("Sum type Empty vs Holds — different tags",
         "type Box = Empty | Holds(Int)\n"
         "fn ok(b: Bool) : Int = if b then 1 else 0\n"
         "ok(Empty != Holds(0))\n",
         "1\n"),
        # v4.37 — closes the structural-eq story for generic sum types.
        # Quartz now substitutes the TyADT's type args into variant
        # field types via _substitute_ty + adt_params, and type_of
        # infers ctor calls' type args by unifying arg types against
        # the variant's declared (TyVar-containing) field types.
        ("Option<Int>: Some(42) == Some(42) (v4.37)",
         "fn ok(b: Bool) : Int = if b then 1 else 0\n"
         "ok(Some(42) == Some(42))\n",
         "1\n"),
        ("Option<Int>: Some(42) != Some(99)",
         "fn ok(b: Bool) : Int = if b then 1 else 0\n"
         "ok(Some(42) != Some(99))\n",
         "1\n"),
        ("Option<String> via concat — string content compare in variant",
         "fn ok(b: Bool) : Int = if b then 1 else 0\n"
         'let a : Option<String> = Some("hello")\n'
         'let b : Option<String> = Some("hel" ++ "lo")\n'
         "ok(a == b)\n",
         "1\n"),
        ("Result<Int, String>: Ok(42) == Ok(42)",
         "fn ok(b: Bool) : Int = if b then 1 else 0\n"
         "let r1 : Result<Int, String> = Ok(42)\n"
         "let r2 : Result<Int, String> = Ok(42)\n"
         "ok(r1 == r2)\n",
         "1\n"),
        ("Result<Int, String>: Ok vs Err — different tags",
         "fn ok(b: Bool) : Int = if b then 1 else 0\n"
         "let r1 : Result<Int, String> = Ok(42)\n"
         'let r2 : Result<Int, String> = Err("oops")\n'
         "ok(r1 != r2)\n",
         "1\n"),
        ("Option<Int>: None == None via let annotation",
         "fn ok(b: Bool) : Int = if b then 1 else 0\n"
         "let a : Option<Int> = None\n"
         "let b : Option<Int> = None\n"
         "ok(a == b)\n",
         "1\n"),
        ("User-declared generic ADT: Maybe<T>",
         "type Maybe<T> = Nope | Yep(T)\n"
         "fn ok(b: Bool) : Int = if b then 1 else 0\n"
         "ok(Yep(7) == Yep(7))\n",
         "1\n"),
        # v4.38 — Quartz gains three host-prelude builtins:
        # string_length, substring, int_to_string. Each is recognized
        # by type_of and emit_expr; substring and int_to_string get
        # malloc-based C runtime helpers, string_length inlines as
        # ((int64_t)strlen(s)).
        ("string_length (v4.38)",
         'string_length("hello, world")\n',
         "12\n"),
        ("string_length empty",
         'string_length("")\n',
         "0\n"),
        ("substring slice (v4.38)",
         'substring("hello, world", 7, 12)\n',
         "world\n"),
        ("substring clamps end to length",
         'substring("abc", 1, 100)\n',
         "bc\n"),
        ("int_to_string (v4.38)",
         "int_to_string(42)\n",
         "42\n"),
        ("int_to_string negative",
         "int_to_string(0 - 17)\n",
         "-17\n"),
        ("composed: int_to_string ++ string ++ string_length",
         'string_length(int_to_string(1000) ++ " items")\n',
         "10\n"),
        # v4.39 — Quartz gains five more host-prelude builtins:
        # len, head, tail, reverse, string_index_of. Builtin dispatch
        # was refactored to pass the Codegen instance to emit_fns so
        # Option-returning builtins can resolve Some/None tags. Args
        # are cast through intptr_t to the formal's C type, mirroring
        # v4.22's generic-fn-call bridge — this lets pattern-bound
        # values (erased to int64_t) flow through builtin formals
        # that expect q_value_t* (e.g., `head(rest)` after
        # `Some(rest)` from `tail`).
        ("len (v4.39)",
         "len([10, 20, 30, 40, 50])\n",
         "5\n"),
        ("len empty",
         "let empty : List<Int> = []\nlen(empty)\n",
         "0\n"),
        ("reverse + len composition",
         "len(reverse([1, 2, 3, 4]))\n",
         "4\n"),
        ("head — Some case (v4.39)",
         "match head([10, 20, 30]) { Some(x) => x; None => 0 - 1 }\n",
         "10\n"),
        ("head — None case",
         "let empty : List<Int> = []\n"
         "match head(empty) { Some(x) => x; None => 0 - 1 }\n",
         "-1\n"),
        ("tail + head chain — pattern bridge through int64_t",
         "match tail([10, 20, 30]) {\n"
         "  Some(rest) => match head(rest) { Some(x) => x; None => 0 - 1 };\n"
         "  None => 0 - 1\n"
         "}\n",
         "20\n"),
        ("string_index_of — found (v4.39)",
         'match string_index_of("hello, world", "world") { '
         'Some(i) => i; None => 0 - 1 }\n',
         "7\n"),
        ("string_index_of — not found",
         'match string_index_of("hello", "xyz") { '
         'Some(i) => i; None => 0 - 1 }\n',
         "-1\n"),
        ("compose: head(reverse(...)) — last element",
         "match head(reverse([1, 2, 3, 4, 5])) { Some(x) => x; None => 0 }\n",
         "5\n"),
        # v4.40 — string_to_upper / string_to_lower added to BOTH the
        # host and Quartz. ASCII-only semantics: bytes outside A-Z /
        # a-z pass through unchanged. The host uses explicit char
        # arithmetic (not Python's Unicode-aware .upper()) to match
        # Quartz exactly, so programs produce identical output through
        # either interpreter.
        ("string_to_upper basic (v4.40)",
         'string_to_upper("hello, world")\n',
         "HELLO, WORLD\n"),
        ("string_to_lower mixed",
         'string_to_lower("HELLO, World 123")\n',
         "hello, world 123\n"),
        ("string_to_upper empty",
         'string_to_upper("")\n',
         "\n"),
        ("string_to_upper already-caps",
         'string_to_upper("ALREADY")\n',
         "ALREADY\n"),
        ("string_to_upper preserves non-letters",
         'string_to_upper("a1!b2@c3")\n',
         "A1!B2@C3\n"),
        ("upper then lower round-trip",
         'string_to_lower(string_to_upper("Mixed Case"))\n',
         "mixed case\n"),
        # v4.41 — char_at added to BOTH host and Quartz with codepoint
        # (Int) semantics, matching what quartz_parser.glass and djb2
        # hash usage expect. Prism's internal `fn char_at` (returning
        # String) still shadows the builtin inside prism's own source,
        # preserving prism's lexer behavior unchanged.
        ("char_at first byte (v4.41)",
         'char_at("hello", 0)\n',
         "104\n"),
        ("char_at last byte",
         'char_at("hello", 4)\n',
         "111\n"),
        ("char_at composes with arithmetic",
         'char_at("Z", 0) - char_at("A", 0)\n',
         "25\n"),
        # The djb2 canary: this hash function is the textbook use
        # case for codepoint char_at. The expected output (193485963)
        # matches every standard djb2 reference implementation.
        ("djb2 hash via char_at composes correctly",
         "fn djb2_at(s: String, i: Int, len: Int, h: Int) : Int =\n"
         "  if i == len then h\n"
         "  else djb2_at(s, i + 1, len, h * 33 + char_at(s, i))\n"
         'djb2_at("abc", 0, string_length("abc"), 5381)\n',
         "193485963\n"),
        # v4.42 — bitwise ops added to BOTH host and Quartz. The host
        # masks results through int64 wrap so non-overflowing values
        # match Quartz exactly. The compiled toolchain had these since
        # v4.16 (quartz_parser.glass); v4.42 just brings the host and
        # Quartz-proper to parity with that.
        ("bit_and (v4.42)",
         "bit_and(12, 10)\n",
         "8\n"),
        ("bit_or",
         "bit_or(12, 10)\n",
         "14\n"),
        ("bit_xor",
         "bit_xor(12, 10)\n",
         "6\n"),
        ("bit_shl",
         "bit_shl(1, 4)\n",
         "16\n"),
        ("bit_shr",
         "bit_shr(16, 2)\n",
         "4\n"),
        ("bit_not all ones",
         "bit_not(0)\n",
         "-1\n"),
        # The djb2 canary now uses bit_shl AND char_at together — both
        # added in v4.41/v4.42. Same expected value through host or
        # Quartz, matching the standard djb2 reference.
        ("djb2 via bit_shl + char_at",
         "fn djb2_from(s: String, i: Int, len: Int, h: Int) : Int =\n"
         "  if i == len then h\n"
         "  else djb2_from(s, i + 1, len, "
         "bit_shl(h, 5) + h + char_at(s, i))\n"
         'djb2_from("abc", 0, string_length("abc"), 5381)\n',
         "193485963\n"),
        # v4.43 — bundle of three small carry-forward items:
        # - range(lo, hi) builtin in Quartz (host already had it)
        # - wrap_int64 in both host and Quartz, lets users opt into
        #   int64 wrap on host so overflow-sensitive algorithms agree
        #   byte-for-byte across interpreters
        # - cast-bridge factoring in Quartz codegen (internal; no
        #   user-visible behavior change, but all existing tests must
        #   continue to pass)
        ("range basic (v4.43)",
         "len(range(0, 5))\n",
         "5\n"),
        ("range sum 1..10",
         "fn sum(xs: List<Int>) : Int =\n"
         "  match xs { [] => 0; [h, ...t] => h + sum(t) }\n"
         "sum(range(1, 11))\n",
         "55\n"),
        ("range head — first element of range",
         "match head(range(10, 20)) { Some(x) => x; None => 0 - 1 }\n",
         "10\n"),
        ("range empty when lo == hi",
         "len(range(5, 5))\n",
         "0\n"),
        ("range empty when lo > hi",
         "len(range(10, 3))\n",
         "0\n"),
        ("wrap_int64 basic (v4.43)",
         "wrap_int64(42)\n",
         "42\n"),
        # The big payoff: with explicit wrap_int64, the overflowing
        # djb2 hash matches between host and Quartz. Before v4.43,
        # host produced 13826554139369386393 and Quartz produced
        # -4620189934340165223 — same bit pattern, different sign
        # interpretation due to host's unbounded ints.
        ("djb2 with wrap_int64 — host/Quartz agree on overflow",
         "fn djb2_from(s: String, i: Int, len: Int, h: Int) : Int =\n"
         "  if i == len then h\n"
         "  else djb2_from(s, i + 1, len,\n"
         "                 wrap_int64("
         "bit_shl(h, 5) + h + char_at(s, i)))\n"
         'djb2_from("Glass v4.20", 0, string_length("Glass v4.20"), 5381)\n',
         "-4620189934340165223\n"),
        # v4.44 — non-capturing lambdas (first cut). Quartz learns
        # TyFn -> q_value_t* (closure values), lambda-lifting (each
        # ELam becomes a generated __lambda_N static C fn), and
        # indirect-call codegen through fields[0]. v4.44 is unary
        # and non-capturing; multi-arg lambdas and free-variable
        # capture land in v4.45.
        ("lambda canary (v4.44)",
         "(fn(x: Int) -> x * 2)(5)\n",
         "10\n"),
        ("let-bound lambda, called later",
         "let f = fn(x: Int) -> x + 100\n"
         "f(7)\n",
         "107\n"),
        ("lambda returning String",
         "let greet = fn(s: String) -> \"hello, \" ++ s\n"
         'greet("world")\n',
         "hello, world\n"),
        ("lambda passed as fn arg (higher-order)",
         "fn apply(f: (Int) -> Int, x: Int) : Int = f(x)\n"
         "apply(fn(n: Int) -> n * n, 9)\n",
         "81\n"),
        # v4.45 — capturing closures. The lifted lambda now does
        # free-variable analysis on its body; outer-scope names
        # referenced inside become captures, packed into
        # __env->fields[1..] at construction and unpacked back into
        # locals at the top of the lifted fn body.
        ("simple capture from let (v4.45)",
         "let y = 100\n"
         "(fn(x: Int) -> x + y)(7)\n",
         "107\n"),
        ("multi-capture",
         "let a = 10\n"
         "let b = 20\n"
         "(fn(x: Int) -> x + a + b)(5)\n",
         "35\n"),
        ("fn returns lambda — captures fn's param",
         "fn adder(x: Int) : (Int) -> Int = fn(y: Int) -> x + y\n"
         "let add5 = adder(5)\n"
         "add5(7)\n",
         "12\n"),
        ("String capture",
         'let prefix = "hi, "\n'
         '(fn(name: String) -> prefix ++ name)("alice")\n',
         "hi, alice\n"),
        # The canary: nested closures, each capturing from its enclosing
        # scope. Inner lambda captures `a` from outer fn, plus `b` from
        # outer lambda — both layers flow through correctly.
        ("nested closure captures both layers",
         "fn make_double_adder(a: Int) : (Int) -> ((Int) -> Int) =\n"
         "  fn(b: Int) -> fn(c: Int) -> a + b + c\n"
         "let f = make_double_adder(100)\n"
         "let g = f(20)\n"
         "g(3)\n",
         "123\n"),
        # v4.46 — multi-arg lambdas + map/filter/fold. The v4.44
        # unary restriction is lifted; lifted fns now take N int64_t
        # args and indirect calls build the fn-pointer cast at the
        # matching arity. fold's binary combine closure exercises
        # this path directly.
        ("multi-arg lambda (v4.46)",
         "(fn(a: Int, b: Int) -> a + b)(3, 4)\n",
         "7\n"),
        ("let-bound multi-arg, called many times",
         "let combine = fn(acc: Int, x: Int) -> acc * 10 + x\n"
         "combine(combine(combine(0, 1), 2), 3)\n",
         "123\n"),
        ("map doubles a list (v4.46)",
         "fn sum(xs: List<Int>) : Int =\n"
         "  match xs { [] => 0; [h, ...t] => h + sum(t) }\n"
         "sum(map([1, 2, 3, 4, 5], fn(x: Int) -> x * 2))\n",
         "30\n"),
        ("filter by predicate",
         "fn sum(xs: List<Int>) : Int =\n"
         "  match xs { [] => 0; [h, ...t] => h + sum(t) }\n"
         "sum(filter([1, 2, 3, 4, 5, 6], fn(x: Int) -> x > 3))\n",
         "15\n"),
        ("fold sum — canonical accumulator",
         "fold([1, 2, 3, 4, 5], 0, fn(acc: Int, x: Int) -> acc + x)\n",
         "15\n"),
        # The composition canary — map -> filter -> fold all chained.
        # Verifies higher-order builtins compose cleanly through the
        # closure-call protocol.
        ("compose: map then filter then fold",
         "fold(\n"
         "  filter(\n"
         "    map([1, 2, 3, 4, 5], fn(x: Int) -> x * x),\n"
         "    fn(y: Int) -> y > 5),\n"
         "  0,\n"
         "  fn(acc: Int, n: Int) -> acc + n)\n",
         "50\n"),
        # Fold with a CAPTURED accumulator (closure capturing from
        # outer scope and ALSO doing real per-iteration math).
        ("fold with captured multiplier",
         "let k = 10\n"
         "fold([1, 2, 3], 1, fn(acc: Int, x: Int) -> acc * x * k)\n",
         "6000\n"),
        # v4.22 — nested generic ADT round-trip. id<A>(Some(99)) erases
        # through TyVar (int64_t) and the return-cast unboxes it back to
        # q_value_t*; unwrap_or<T> then takes a q_value_t* via the v4.22
        # call-site bridge fix. If the call-site cast is wrong in either
        # direction, this fails to compile.
        ("nested generic ADT round-trip (v4.22)",
         "fn id<A>(x: A) : A = x\n"
         "fn unwrap_or<T>(opt: Option<T>, default: T) : T =\n"
         "  match opt { Some(x) => x; None => default }\n"
         "unwrap_or(id(Some(99)), 0)\n",
         "99\n"),
        # v4.49: Quartz refinement runtime checks. Pre-v4.49 the C-type
        # mapping threw `NotImplementedError: Quartz does not yet
        # support type: TyRefine` the moment ANY refined param hit
        # codegen, so the entire refinement subset of Glass couldn't
        # be native-compiled. v4.49 strips TyRefine for the C-type
        # layer and emits an inline guard at the top of the fn body
        # for each refined param. Good value flows through unchanged.
        ("refined param compiles + good value (v4.49)",
         "fn positive_double(n: Int where (n > 0)) : Int = n * 2\n"
         "let x : Int = 21\n"
         "positive_double(x)\n",
         "42\n"),
        # Return-type refinement: parser accepts `: Int where (result > 0)`,
        # and the codegen materializes the body result into a `result`
        # local, runs the guard, then returns. Mirrors host's
        # apply_fn return-refinement path (line 2368).
        ("refined return compiles + holds (v4.49)",
         "fn pos_sq_plus_one(n: Int) : Int where (result > 0) = n * n + 1\n"
         "let x : Int = 5\n"
         "pos_sq_plus_one(x)\n",
         "26\n"),
        # Refined param composed with normal param: only the refined
        # position should grow a guard. Acts as a regression on
        # accidentally inserting guards for every param.
        ("refined param mixed with normal param (v4.49)",
         "fn add_pos(a: Int where (a > 0), b: Int) : Int = a + b\n"
         "add_pos(3, 4)\n",
         "7\n"),
        # v4.50: refined let-binding at top level. The guard runs
        # right after the value is computed, in main(), before any
        # subsequent expression uses the let-bound name.
        ("refined let-binding compiles + holds (v4.50)",
         "let n : Int where (n > 0) = 42\n"
         "n + 1\n",
         "43\n"),
        # v4.50: refined LetIn nested in a fn body. Distinct codegen
        # path from the top-level LetDecl loop — exercises the
        # Codegen.emit_expr LetIn branch.
        ("refined let-in inside fn body (v4.50)",
         "fn doit(k: Int) : Int =\n"
         "  let n : Int where (n > 0) = k * 2 in\n"
         "  n + 1\n"
         "doit(7)\n",
         "15\n"),
        # v4.50: refined lambda param. The guard lives inside the
        # lifted __lambda_N C function emitted by _lift_lambda, so it
        # fires regardless of whether the lambda is called directly
        # or indirectly through higher-order builtins.
        ("refined lambda param compiles + holds (v4.50)",
         "let dbl = fn(x: Int where (x > 0)) -> x * 2\n"
         "dbl(5)\n",
         "10\n"),
        # v4.50: composes with v4.46's higher-order list builtins.
        # The refined lambda's guard fires for every element fold
        # visits — and each element satisfies the predicate, so the
        # fold runs end to end. (We fold instead of map because
        # Quartz can't print a List directly.)
        ("refined lambda through fold (v4.50)",
         "fold([1, 2, 3], 0, fn(acc: Int, x: Int where (x > 0))"
         " -> acc + x)\n",
         "6\n"),
        # v4.51: && / || in regular Glass code compile through Quartz's
        # BIN_OP_C map. C's && and || are short-circuiting so semantics
        # match host eval directly.
        ("&& and || in normal code (v4.51)",
         "let r : Int = if (1 > 0) && (1 < 5) then 42 else 0\n"
         "r\n",
         "42\n"),
        # v4.51 canonical range refinement: param checked against an
        # interval. The guard becomes `((n > 0LL) && (n < 100LL))`.
        ("range refinement via && (v4.51)",
         "fn middling(n: Int where (n > 0 && n < 100)) : Int = n + 1\n"
         "middling(50)\n",
         "51\n"),
        # v4.51 || refinement: enum-style "this OR that" check.
        ("|| refinement (v4.51)",
         "fn flag(n: Int where (n == 0 || n == 1)) : Int = n + 10\n"
         "flag(1)\n",
         "11\n"),
        # v4.53: modulo in regular Quartz code via BIN_OP_C entry.
        ("modulo in normal code (v4.53)",
         "let r : Int = 17 % 5\n"
         "r\n",
         "2\n"),
        # v4.53: parity refinement compiles + the guard fires only
        # for an actually-even arg. 10 is even, so even_only returns
        # 11. Pinned by both this and the structural test below.
        ("parity refinement compiles (v4.53)",
         "fn even_only(n: Int where (n % 2 == 0)) : Int = n + 1\n"
         "even_only(10)\n",
         "11\n"),
        # v4.54: unary NOT in normal code via emit_expr UnaryNot arm.
        ("unary NOT in normal code (v4.54)",
         "let r : Int = if !(3 > 5) then 42 else 0\n"
         "r\n",
         "42\n"),
        # v4.54: NOT refinement compiles + holds. 5 is nonzero, so
        # 100 / 5 = 20.
        ("NOT refinement compiles (v4.54)",
         "fn nonzero(n: Int where (!(n == 0))) : Int = 100 / n\n"
         "nonzero(5)\n",
         "20\n"),
        # v4.55: arithmetic-in-predicate now compiles. `n + 1 > 0`
        # was rejected pre-v4.55 (only bare `binder OP lit` was
        # allowed); the recursive compiler handles the offset.
        ("offset arithmetic in predicate (v4.55)",
         "fn f(n: Int where (n + 1 > 0)) : Int = n\n"
         "f(5)\n",
         "5\n"),
        # v4.55: nonlinear predicate + boolean combinator. `n * n`
        # compiles as `(n * n)`; composed with a range bound via &&.
        ("nonlinear predicate with && (v4.55)",
         "fn g(n: Int where (n * n >= 1 && n < 100)) : Int = n\n"
         "g(7)\n",
         "7\n"),
        # v4.56: cross-parameter refinement. `hi > lo` references the
        # earlier param `lo`, which is a C function parameter in scope
        # at the guard site. clamp(3, 10) = 7.
        ("cross-parameter refinement (v4.56)",
         "fn clamp(lo: Int, hi: Int where (hi > lo)) : Int = hi - lo\n"
         "clamp(3, 10)\n",
         "7\n"),
        # v4.56: return refinement referencing a param. `result > a`
        # sees `a` (all params in scope when the body completes).
        ("return refinement references param (v4.56)",
         "fn addpos(a: Int, b: Int) : Int where (result > a) = a + b + 1\n"
         "addpos(5, 3)\n",
         "9\n"),
        # v4.71 (Phase A1/A2 — migration): effectful functions compile.
        # Effects are erased at codegen; `print` is a C runtime call.
        # The binary prints "hi" (from the IO effect) then the result 5.
        ("effectful fn compiles, print works (v4.71)",
         "fn g(x: Int) : Int !{IO} = let _ = print(\"hi\") in x\n"
         "g(5)\n",
         "hi\n5\n"),
        # v4.71: a prelude function the program uses (string_contains)
        # is now emitted, not just type-checked. Usage-based: simple
        # programs don't drag in higher-order prelude fns.
        ("prelude fn string_contains compiles (v4.71)",
         "if string_contains(\"hello\", \"ell\") then 1 else 0\n",
         "1\n"),
        # v4.72 (Phase A4): nested patterns — a cons whose head is a
        # ctor pattern. Recursive pattern binding handles the nesting.
        ("nested cons-of-ctor pattern (v4.72)",
         "type P = | P(Int, Int)\n"
         "fn sh(xs: List<P>) : Int =\n"
         "  match xs { [] => 0; [P(a, b), ...rest] => a + b + sh(rest) }\n"
         "sh([P(1, 2), P(3, 4), P(10, 0)])\n",
         "20\n"),
        # v4.72: literal patterns over scalar scrutinees (Int + String).
        ("literal int/string patterns (v4.72)",
         "fn classify(n: Int) : String ="
         " match n { 0 => \"z\"; 1 => \"o\"; _ => \"m\" }\n"
         "fn day(c: String) : Int ="
         " match c { \"mon\" => 1; \"tue\" => 2; _ => 0 }\n"
         "let _ = print(classify(0) ++ classify(1) ++ classify(9))\n"
         "day(\"tue\")\n",
         "zom\n2\n"),
        # v4.73 (Phase A4): a tuple pattern whose first element is a CTOR
        # must DISCRIMINATE on that ctor, not match every tuple. This is
        # exactly prism's tokenizer dispatch shape `(TEnd, _) => …`. The
        # bug: _pattern_test returned "true" for any tuple, so the first
        # arm swallowed every case. Here `(A, k)` must NOT match (B, 9);
        # the `(B, k)` arm must win → 9, not 0.
        ("tuple pattern discriminates on ctor sub-pattern (v4.73)",
         "type Tag = | A | B\n"
         "fn pick(p: (Tag, Int)) : Int ="
         " match p { (A, k) => 0; (B, k) => k }\n"
         "pick((B, 9))\n",
         "9\n"),
        # v4.73: an explicit `let _ : T = <effectful stmt>` final decl is
        # a discard run for effects, NOT a REPL result — so `print` fires
        # once, not twice. (prism's last line is this shape.)
        ("final `let _ : T` discard prints once (v4.73)",
         "let _ : String = print(\"once\")\n",
         "once\n"),
    ]
    failures = 0
    for label, src, expected in cases:
        with tempfile.NamedTemporaryFile(
            mode="w", suffix=".glass", delete=False
        ) as f:
            f.write(src)
            src_file = f.name
        with tempfile.NamedTemporaryFile(suffix="", delete=False) as f:
            out_bin = f.name
        try:
            p = subprocess.run(
                [sys.executable, QUARTZ, src_file, "-o", out_bin],
                capture_output=True, text=True,
            )
            if p.returncode != 0:
                print(f"  FAIL  {label} (compile)")
                print(f"        stderr: {p.stderr.strip()}")
                failures += 1
                continue
            r = subprocess.run([out_bin], capture_output=True, text=True)
            ok = (r.stdout == expected)
            print(f"  {'OK ' if ok else 'FAIL'}  {label}")
            if not ok:
                print(f"        expected {expected!r}, got {r.stdout!r}")
                failures += 1
        finally:
            os.unlink(src_file)
            try:
                os.unlink(out_bin)
            except OSError:
                pass

    # v4.49: structural codegen checks. The runtime cases above can't
    # distinguish "guard emitted but never fired" from "guard silently
    # dropped" — for both, the program returns the right value. These
    # cases run `quartz.py --verbose`, capture the generated C, and
    # grep for the actual `if (!...) { fprintf ... exit(1); }` shape
    # so a future change that quietly stops emitting the guard FAILS
    # this test instead of looking healthy.
    print("== quartz refinement codegen structure (v4.49) ==")
    ref_cases = [
        ("param guard in C source",
         "fn p(n: Int where (n > 0)) : Int = n\np(1)\n",
         "if (!(n > 0LL))"),
        ("return guard in C source",
         "fn p(n: Int) : Int where (result > 0) = n + 1\np(1)\n",
         "if (!(result > 0LL))"),
        # Literal-on-the-left form: ensures the parser of the
        # predicate handles both `binder OP literal` AND
        # `literal OP binder` (the latter must flip the C operator).
        ("literal-on-left predicate shape",
         "fn p(n: Int where (0 < n)) : Int = n\np(3)\n",
         "if (!(0LL < n))"),
        # v4.50: refined let-decl in main()'s C source. Pin down that
        # the guard lives in main(), not duplicated in the surrounding
        # fn machinery.
        ("refined let-decl guard in main (v4.50)",
         "let n : Int where (n > 0) = 42\nn\n",
         "if (!(n > 0LL))"),
        # v4.50: refined LetIn inside fn body — guard must be emitted
        # inside the fn, not the surrounding main().
        ("refined let-in guard inside fn (v4.50)",
         "fn f(k: Int) : Int = let n : Int where (n > 0) = k in n\nf(3)\n",
         "if (!(n > 0LL))"),
        # v4.50: refined lambda param — guard lives inside the
        # lifted __lambda_N C fn, not at the call site.
        ("refined lambda param guard in lifted fn (v4.50)",
         "let dbl = fn(x: Int where (x > 0)) -> x * 2\ndbl(5)\n",
         "if (!(x > 0LL))"),
        # v4.51: && compiled in a refinement predicate. Verifies
        # _compile_refinement_pred recurses correctly: both sides
        # become parenthesized comparisons and combine via C's `&&`.
        ("&& refinement guard shape (v4.51)",
         "fn p(n: Int where (n > 0 && n < 100)) : Int = n\np(50)\n",
         "((n > 0LL) && (n < 100LL))"),
        # v4.51 || refinement guard — same shape with `||`.
        ("|| refinement guard shape (v4.51)",
         "fn p(n: Int where (n == 0 || n == 1)) : Int = n\np(0)\n",
         "((n == 0LL) || (n == 1LL))"),
        # v4.53: parity refinement guard. `_compile_refinement_pred`
        # recognizes the `binder %% int_lit OP int_lit` shape and emits
        # `((mangled % KLL) OP MLL)` — the natural C transcription.
        ("parity refinement guard shape (v4.53)",
         "fn p(n: Int where (n % 2 == 0)) : Int = n\np(2)\n",
         "((n % 2LL) == 0LL)"),
        # v4.54: NOT refinement guard. `_compile_refinement_pred`
        # recurses through UnaryNot, emitting `(!inner)` — so the full
        # guard double-negates: `if (!(!(n == 0LL)))`.
        ("NOT refinement guard shape (v4.54)",
         "fn p(n: Int where (!(n == 0))) : Int = n\np(5)\n",
         "(!(n == 0LL))"),
        # v4.55: recursive compiler transcribes nested arithmetic. The
        # offset `n + 1` becomes `(n + 1LL)`, then the comparison wraps
        # it: `((n + 1LL) > 0LL)`. Pins down that arithmetic recurses
        # rather than being special-cased.
        ("offset arithmetic guard shape (v4.55)",
         "fn p(n: Int where (n + 1 > 0)) : Int = n\np(5)\n",
         "((n + 1LL) > 0LL)"),
        # v4.56: cross-param guard references the earlier param by its
        # mangled name — `(hi > lo)`, not `(hi > <literal>)`.
        ("cross-parameter guard shape (v4.56)",
         "fn clamp(lo: Int, hi: Int where (hi > lo)) : Int = hi - lo\n"
         "clamp(3, 10)\n",
         "(hi > lo)"),
    ]
    for label, src, needle in ref_cases:
        with tempfile.NamedTemporaryFile(
            mode="w", suffix=".glass", delete=False
        ) as f:
            f.write(src)
            src_file = f.name
        with tempfile.NamedTemporaryFile(suffix="", delete=False) as f:
            out_bin = f.name
        try:
            p = subprocess.run(
                [sys.executable, QUARTZ, src_file, "-o", out_bin, "--verbose"],
                capture_output=True, text=True,
            )
            ok = (p.returncode == 0) and (needle in p.stdout)
            print(f"  {'OK ' if ok else 'FAIL'}  {label}")
            if not ok:
                print(f"        rc={p.returncode}, expected substring "
                      f"{needle!r}")
                print(f"        stdout tail: {p.stdout.strip()[-300:]}")
                print(f"        stderr tail: {p.stderr.strip()[-300:]}")
                failures += 1
        finally:
            os.unlink(src_file)
            try:
                os.unlink(out_bin)
            except OSError:
                pass

    # v4.56: cross-parameter refinements now compile — a later param's
    # predicate may reference an EARLIER param (`b < a`), so the v4.55
    # "non-binder identifier" negative was retired (it compiles now).
    # What's STILL refused: a non-arithmetic expression form (function
    # calls, field access). The cross-param boundary itself (forward
    # references, truly-unbound names) is caught by the host's pre-eval
    # during glass-build, so it can't be isolated to Quartz's envelope
    # via the CLI — the envelope branch stays as defense-in-depth for
    # standalone codegen.
    print("== quartz refinement: unsupported predicate (v4.56) ==")
    bad_cases = [
        # A function call inside the predicate — not an arithmetic /
        # comparison / boolean form, so it hits the envelope error.
        ("function call in predicate",
         "fn id(x: Int) : Int = x\n"
         "fn p(n: Int where (id(n) > 0)) : Int = n\np(3)\n",
         "Quartz refinement predicates support arithmetic"),
    ]
    for label, src, needle in bad_cases:
        with tempfile.NamedTemporaryFile(
            mode="w", suffix=".glass", delete=False
        ) as f:
            f.write(src)
            src_file = f.name
        try:
            p = subprocess.run(
                [sys.executable, QUARTZ, src_file],
                capture_output=True, text=True,
            )
            ok = (p.returncode != 0) and (needle in p.stderr)
            print(f"  {'OK ' if ok else 'FAIL'}  {label}")
            if not ok:
                print(f"        rc={p.returncode}, expected substring "
                      f"{needle!r}")
                print(f"        stderr: {p.stderr.strip()[-300:]}")
                failures += 1
        finally:
            os.unlink(src_file)

    return failures


if __name__ == "__main__":
    sys.exit(main())