#!/usr/bin/env python3
"""L18: pure integer flowcharts, binding times and emitted residual programs.

Python 3 standard library. No eval, network or file writes. Print JSON only.
A step executes one finite basic block. Expression operations are total.
All local variables start at zero; inputs replace their initial values.
"""
from collections import deque
from copy import deepcopy
import json
import random

OPS = {"add", "sub", "mul", "lt", "eq"}


def require(condition, message):
    if not condition:
        raise ValueError(message)


def var_reads(expr):
    if type(expr) is str:
        yield expr
    elif type(expr) is tuple:
        yield from var_reads(expr[1])
        yield from var_reads(expr[2])


def check_expr(expr, names):
    if type(expr) is int:
        return
    if type(expr) is str:
        require(expr in names, "unknown expression variable")
        return
    require(type(expr) is tuple and len(expr) == 3, "bad expression")
    require(expr[0] in OPS, "unsupported primitive")
    check_expr(expr[1], names)
    check_expr(expr[2], names)


def validate(program):
    require(type(program) is dict and set(program) == {"vars", "inputs", "entry", "blocks"}, "bad program fields")
    for field in ("vars", "inputs"):
        items = program[field]
        require(type(items) is tuple and all(type(x) is str and x.isidentifier() for x in items), "bad variable names")
        require(len(items) == len(set(items)), "duplicate variable")
    names = set(program["vars"])
    require(set(program["inputs"]) <= names, "unknown input")
    blocks = program["blocks"]
    require(type(blocks) is dict and blocks, "missing blocks")
    require(all(type(x) is str and x.isidentifier() for x in blocks), "bad label")
    require(type(program["entry"]) is str and program["entry"] in blocks, "missing entry")
    for assigns, term in blocks.values():
        require(type(assigns) is tuple, "assignment list must be a tuple")
        for assignment in assigns:
            require(type(assignment) is tuple and len(assignment) == 2, "bad assignment")
            dest, expr = assignment
            require(type(dest) is str and dest in names, "unknown destination")
            check_expr(expr, names)
        require(type(term) is tuple and len(term) >= 2, "bad terminator")
        if term[0] == "goto":
            require(len(term) == 2 and term[1] in blocks, "bad goto")
        elif term[0] == "if":
            require(len(term) == 4 and term[2] in blocks and term[3] in blocks, "bad branch")
            check_expr(term[1], names)
        else:
            require(term[0] == "return" and len(term) == 2, "bad return")
            check_expr(term[1], names)
    return program


def primitive(op, a, b):
    require(type(a) is int and type(b) is int, "non-integer value")
    if op == "add":
        return a + b
    if op == "sub":
        return a - b
    if op == "mul":
        return a * b
    if op == "lt":
        return int(a < b)
    require(op == "eq", "unsupported primitive")
    return int(a == b)


def evaluate(expr, store, counts):
    if type(expr) is int:
        return expr
    if type(expr) is str:
        return store[expr]
    a = evaluate(expr[1], store, counts)
    b = evaluate(expr[2], store, counts)
    counts["primitives"] += 1
    return primitive(expr[0], a, b)


def reduce_expr(expr, static_store):
    if type(expr) is int:
        return expr
    if type(expr) is str:
        return static_store.get(expr, expr)
    a, b = reduce_expr(expr[1], static_store), reduce_expr(expr[2], static_store)
    if type(a) is int and type(b) is int:
        return primitive(expr[0], a, b)
    return (expr[0], a, b)


def initial_store(program, inputs):
    require(type(inputs) is dict and set(inputs) == set(program["inputs"]), "input names do not match")
    require(all(type(x) is int for x in inputs.values()), "inputs must be mathematical integers")
    store = dict.fromkeys(program["vars"], 0)
    store.update(inputs)
    return store


def block_step(program, label, store, counts):
    """Mutate one store; return (next label, None) or (None, returned integer)."""
    assigns, term = program["blocks"][label]
    counts["blocks"] += 1
    for dest, expr in assigns:
        store[dest] = evaluate(expr, store, counts)
        counts["assignments"] += 1
    if term[0] == "return":
        return None, evaluate(term[1], store, counts)
    if term[0] == "goto":
        return term[1], None
    return term[2] if evaluate(term[1], store, counts) != 0 else term[3], None


def run(program, inputs, block_limit=10000):
    validate(program)
    require(type(block_limit) is int and block_limit >= 0, "bad block limit")
    store = initial_store(program, inputs)
    label, trace, seen = program["entry"], [], {}
    counts = {"blocks": 0, "assignments": 0, "primitives": 0}
    while counts["blocks"] < block_limit:
        state = (label, tuple(store[x] for x in program["vars"]))
        if state in seen:
            return {"status": "cycle", "cycle_start": seen[state], "cycle_length": len(trace) - seen[state], "counts": counts, "trace": trace}
        seen[state] = len(trace)
        trace.append({"label": label, "store": dict(store)})
        label, value = block_step(program, label, store, counts)
        if label is None:
            return {"status": "return", "value": value, "counts": counts, "trace": trace}
    return {"status": "prefix_only", "counts": counts, "trace": trace}


def binding_times(program, dynamic_inputs, force_dynamic=()):
    validate(program)
    names = set(program["vars"])
    inputs = set(dynamic_inputs)
    forced = set(force_dynamic)
    require(inputs <= set(program["inputs"]) and forced <= names, "unknown binding-time seed")
    edges = {x: [] for x in program["vars"]}
    for label, (assigns, _) in program["blocks"].items():
        for index, (dest, expr) in enumerate(assigns):
            for src in var_reads(expr):
                edges[src].append((dest, label, index))
    dynamic = inputs | forced
    queue = deque(sorted(dynamic))
    reasons = [{"variable": x, "reason": "seed"} for x in sorted(dynamic)]
    scanned = 0
    while queue:
        src = queue.popleft()
        for dest, label, index in edges[src]:
            scanned += 1
            if dest not in dynamic:
                dynamic.add(dest)
                queue.append(dest)
                reasons.append({"variable": dest, "reason": "assignment", "from": src, "label": label, "index": index})
    return {"dynamic": sorted(dynamic), "static": sorted(names - dynamic), "reasons": reasons,
            "dependency_occurrences": sum(map(len, edges.values())), "scanned_occurrences": scanned}


class SpecializationLimit(RuntimeError):
    def __init__(self, created, next_state):
        super().__init__("state budget exhausted; no residual program returned")
        self.created, self.next_state = created, next_state


def specialize(program, dynamic_inputs, known_inputs, force_dynamic=(), state_budget=10000):
    """Emit one residual block per discovered (label, full static store).

    A budget exception is failure, not a truncated or executable result.
    Known input values promoted to dynamic receive residual initialization.
    """
    dynamic_inputs = tuple(dynamic_inputs)
    force_dynamic = tuple(force_dynamic)
    analysis = binding_times(program, dynamic_inputs, force_dynamic)
    dynamic_inputs = set(dynamic_inputs)
    require(type(known_inputs) is dict and set(known_inputs) == set(program["inputs"]) - dynamic_inputs, "known input names do not match")
    require(all(type(x) is int for x in known_inputs.values()), "known inputs must be integers")
    require(type(state_budget) is int and state_budget > 0, "bad state budget")
    dynamic = set(analysis["dynamic"])
    static_names = tuple(x for x in program["vars"] if x not in dynamic)
    initial = dict.fromkeys(program["vars"], 0)
    initial.update(known_inputs)
    labels, pending, residual, certificate = {}, deque(), {}, {}

    def intern(label, static_store):
        key = (label, tuple(static_store[x] for x in static_names))
        if key not in labels:
            if len(labels) >= state_budget:
                raise SpecializationLimit(len(labels), {"source_label": label, "static": dict(static_store)})
            fresh = "r" + str(len(labels))
            labels[key] = fresh  # Reserve BEFORE scanning successors; cycles fold here.
            certificate[fresh] = {"source_label": label, "static": dict(static_store)}
            pending.append(key)
        return labels[key]

    first = intern(program["entry"], {x: initial[x] for x in static_names})
    while pending:
        key = pending.popleft()
        label, static_values = key
        static_store = dict(zip(static_names, static_values))
        out = []
        assigns, term = program["blocks"][label]
        for dest, expr in assigns:
            reduced = reduce_expr(expr, static_store)
            if dest in dynamic:
                out.append((dest, reduced))
            else:
                require(type(reduced) is int, "unsafe static assignment")
                static_store[dest] = reduced
        if term[0] == "goto":
            last = ("goto", intern(term[1], static_store))
        elif term[0] == "return":
            last = ("return", reduce_expr(term[1], static_store))
        else:
            expr = reduce_expr(term[1], static_store)
            if type(expr) is int:
                last = ("goto", intern(term[2] if expr != 0 else term[3], static_store))
            else:
                last = ("if", expr, intern(term[2], static_store), intern(term[3], static_store))
        residual[labels[key]] = (tuple(out), last)
    # Preserve the original unknown-input API, even if a known input is promoted.
    init = tuple((x, known_inputs[x]) for x in program["inputs"] if x in dynamic and x in known_inputs)
    entry = first
    if init:
        residual["init"] = (init, ("goto", first))
        entry = "init"
    target = {"vars": tuple(x for x in program["vars"] if x in dynamic),
              "inputs": tuple(x for x in program["inputs"] if x in dynamic_inputs),
              "entry": entry, "blocks": residual}
    validate(target)
    return {"program": target, "analysis": analysis, "states": certificate, "initialization_block": bool(init)}


def lockstep(source, specialized, source_inputs, block_limit=10000):
    """Check the actual block-boundary relation, with exact cycle witnesses.

    A finite nonrepeating prefix is explicitly inconclusive on termination.
    """
    target = specialized["program"]
    validate(source)
    validate(target)
    s = initial_store(source, source_inputs)
    t = initial_store(target, {x: source_inputs[x] for x in target["inputs"]})
    sl, tl = source["entry"], target["entry"]
    sc = {"blocks": 0, "assignments": 0, "primitives": 0}
    tc = dict(sc)
    if specialized["initialization_block"]:
        tl, value = block_step(target, tl, t, tc)
        require(value is None, "initializer unexpectedly returns")
    trace, seen = [], {}
    for _ in range(block_limit):
        cert = specialized["states"][tl]
        require(sl == cert["source_label"], "source-label relation failed")
        require(all(s[x] == value for x, value in cert["static"].items()), "static-store relation failed")
        require(all(s[x] == t[x] for x in target["vars"]), "dynamic-store relation failed")
        key = (sl, tuple(s[x] for x in source["vars"]), tl, tuple(t[x] for x in target["vars"]))
        if key in seen:
            return {"status": "cycle", "cycle_start": seen[key], "cycle_length": len(trace) - seen[key],
                    "source_counts": sc, "residual_counts": tc, "trace": trace}
        seen[key] = len(trace)
        trace.append({"source_label": sl, "residual_label": tl, "static": cert["static"], "dynamic": dict(t)})
        sl, sv = block_step(source, sl, s, sc)
        tl, tv = block_step(target, tl, t, tc)
        require((sl is None) == (tl is None), "return/continue mismatch")
        if sl is None:
            require(sv == tv, "return-value mismatch")
            return {"status": "return", "value": sv, "source_counts": sc, "residual_counts": tc, "trace": trace}
    return {"status": "prefix_only", "source_counts": sc, "residual_counts": tc, "trace": trace}


def affine_program():
    return {"vars": ("n", "x", "i", "a", "b", "y"), "inputs": ("n", "x"), "entry": "E", "blocks": {
        "E": ((("i", 0), ("a", 2), ("b", 1), ("y", "x")), ("goto", "H")),
        "H": ((), ("if", ("lt", "i", "n"), "B", "R")),
        "B": ((("y", ("add", ("mul", "a", "y"), "b")), ("a", ("add", "a", 1)),
               ("b", ("add", "b", 2)), ("i", ("add", "i", 1))), ("goto", "H")),
        "R": ((), ("return", "y"))}}


def branch_program():
    return {"vars": ("p", "x", "k", "y"), "inputs": ("p", "x"), "entry": "E", "blocks": {
        "E": ((), ("if", "p", "T", "F")), "T": ((("k", 2),), ("goto", "J")),
        "F": ((("k", 5),), ("goto", "J")), "J": ((("y", ("mul", "k", "x")),), ("return", "y"))}}


def growing_program():
    return {"vars": ("x", "i"), "inputs": ("x",), "entry": "E", "blocks": {
        "E": ((("i", 0),), ("goto", "H")), "H": ((), ("if", ("lt", "i", "x"), "B", "R")),
        "B": ((("i", ("add", "i", 1)),), ("goto", "H")), "R": ((), ("return", "i"))}}


def slow_binding_times(program, seeds):
    dynamic = set(seeds)
    while True:
        after = set(dynamic)
        for assigns, _ in program["blocks"].values():
            for dest, expr in assigns:
                if set(var_reads(expr)) & dynamic:
                    after.add(dest)
        if after == dynamic:
            return dynamic
        dynamic = after


def self_test():
    source = affine_program()
    result = specialize(source, ("x",), {"n": 3})
    main = lockstep(source, result, {"n": 3, "x": 4})
    require(main["value"] == 125 and len(result["states"]) == 9, "affine main")
    require(main["source_counts"] == {"blocks": 9, "assignments": 16, "primitives": 19}, "source cost")
    require(main["residual_counts"] == {"blocks": 9, "assignments": 4, "primitives": 6}, "residual cost")
    affine_cases = 0
    for n in range(-3, 13):
        spec = specialize(source, ("x",), {"n": n})
        for x in range(-15, 16):
            check = lockstep(source, spec, {"n": n, "x": x})
            expected, a, b = x, 2, 1
            for _ in range(max(n, 0)):
                expected, a, b = a * expected + b, a + 1, b + 2
            require(check["status"] == "return" and check["value"] == expected, "affine regression")
            affine_cases += 1
    branch = branch_program()
    bs = specialize(branch, ("p", "x"), {})
    require(len(bs["states"]) == 5 and bs["analysis"]["static"] == ["k"], "branch division")
    j2 = next(l for l, c in bs["states"].items() if c == {"source_label": "J", "static": {"k": 2}})
    j5 = next(l for l, c in bs["states"].items() if c == {"source_label": "J", "static": {"k": 5}})
    damaged = deepcopy(bs["program"])
    for l, (assigns, term) in list(damaged["blocks"].items()):
        if term == ("goto", j5):
            damaged["blocks"][l] = (assigns, ("goto", j2))
    bad_value = run(damaged, {"p": 0, "x": 4})["value"]
    require(bad_value == 8, "missing-static-key counterexample")
    wrong_certificate = dict(bs)
    wrong_certificate["program"] = damaged
    try:
        lockstep(branch, wrong_certificate, {"p": 0, "x": 4})
        raise RuntimeError("wrong static-key merge escaped relation check")
    except ValueError as err:
        require(str(err) == "static-store relation failed", "unexpected failure witness")
        relation_failure = str(err)
    branch_dynamic = specialize(branch, ("p", "x"), {}, force_dynamic=("k",))
    require(len(branch_dynamic["states"]) == 4, "dynamic k should merge J safely")
    for flag, answer in ((1, 8), (0, 20)):
        require(lockstep(branch, branch_dynamic, {"p": flag, "x": 4})["value"] == answer, "dynamic k result")
    branch_traces = [lockstep(branch, bs, {"p": p, "x": 4}) for p in (1, 0)]
    require([x["value"] for x in branch_traces] == [8, 20], "branch values")
    spin = {"vars": ("k",), "inputs": (), "entry": "L", "blocks": {"L": ((), ("goto", "L"))}}
    ss = specialize(spin, (), {})
    spin_trace = lockstep(spin, ss, {})
    require(len(ss["states"]) == 1 and spin_trace["status"] == "cycle" and spin_trace["cycle_length"] == 1, "preserve static loop")
    growing_forever = {"vars": ("i",), "inputs": (), "entry": "L", "blocks": {
        "L": ((("i", ("add", "i", 1)),), ("goto", "L"))}}
    forever_spec = specialize(growing_forever, (), {}, force_dynamic=("i",))
    prefix = lockstep(growing_forever, forever_spec, {}, block_limit=7)
    require(prefix["status"] == "prefix_only", "nonrepeating prefix is not a cycle certificate")
    growing = growing_program()
    try:
        specialize(growing, ("x",), {}, state_budget=12)
        raise RuntimeError("unbounded specialization incorrectly returned")
    except SpecializationLimit as err:
        limit = {"status": "budget_exhausted", "created": err.created, "next_state": err.next_state,
                 "residual_program_returned": False}
    gs = specialize(growing, ("x",), {}, force_dynamic=("i",))
    require(len(gs["states"]) == 4, "promotion should give four variants")
    for x in range(-20, 81):
        check = lockstep(growing, gs, {"x": x})
        require(check["status"] == "return" and check["value"] == max(0, x), "promoted counter")
    # A known input remains fixed even when deliberately residualized.
    promoted = specialize(source, ("x",), {"n": 3}, force_dynamic=("n", "i", "a", "b"))
    require(promoted["initialization_block"] and promoted["program"]["inputs"] == ("x",), "preserve unknown-input API")
    init_check = lockstep(source, promoted, {"n": 3, "x": 4})
    require(init_check["value"] == 125 and len(promoted["states"]) == 4, "known-input initialization")
    rng = random.Random(18018)
    bta_cases = residual_cases = 0
    for _ in range(600):
        names = ("a", "b", "c", "d", "e")
        blocks = {}
        for j in range(4):
            assignments = tuple((rng.choice(names), (rng.choice(tuple(sorted(OPS))), rng.choice(names), rng.choice(names))) for _ in range(4))
            blocks["B" + str(j)] = (assignments, ("if", rng.choice(names), "B" + str(rng.randrange(4)), "B" + str(rng.randrange(4))))
        p = {"vars": names, "inputs": names, "entry": "B0", "blocks": blocks}
        seeds = {x for x in names if rng.randrange(2)}
        require(set(binding_times(p, seeds)["dynamic"]) == slow_binding_times(p, seeds), "BTA differential")
        bta_cases += 1
    # Acyclic random programs give finite specialization, including dynamic control.
    for _ in range(500):
        names = ("p", "x", "k", "z")
        blocks = {}
        for j in range(5):
            assignments = []
            for _ in range(2):
                dest = rng.choice(names)
                left = rng.choice(names) if rng.randrange(2) else rng.randrange(-3, 4)
                right = rng.choice(names) if rng.randrange(2) else rng.randrange(-3, 4)
                assignments.append((dest, (rng.choice(tuple(sorted(OPS))), left, right)))
            term = ("return", rng.choice(names)) if j == 4 else ("if", rng.choice(names), "B" + str(rng.randrange(j + 1, 5)), "B" + str(rng.randrange(j + 1, 5)))
            blocks["B" + str(j)] = (tuple(assignments), term)
        p = {"vars": names, "inputs": ("p", "x"), "entry": "B0", "blocks": blocks}
        spec = specialize(p, ("x",), {"p": rng.randrange(-2, 3)})
        fixed_p = next(iter(spec["states"].values()))["static"].get("p")
        # p may be promoted by dependency closure; recover its given literal then.
        if fixed_p is None:
            fixed_p = dict(spec["program"]["blocks"]["init"][0])["p"]
        for x in range(-3, 4):
            check = lockstep(p, spec, {"p": fixed_p, "x": x})
            require(check["status"] == "return", "acyclic pair must return")
            residual_cases += 1
    rejected = []
    bad_inputs = [({"n": True, "x": 4}, "boolean"), ({"n": 3}, "missing input")]
    for inputs, reason in bad_inputs:
        try:
            run(source, inputs)
            raise RuntimeError("bad input accepted")
        except ValueError:
            rejected.append(reason)
    invalid = deepcopy(source)
    invalid["blocks"]["E"] = ((("y", ("div", 1, "x")),), ("goto", "H"))
    try:
        specialize(invalid, ("x",), {"n": 3})
        raise RuntimeError("partial primitive accepted")
    except ValueError:
        rejected.append("division primitive")
    return {"status": "PASS", "main": {"division": result["analysis"], "states": result["states"],
             "residual_program": result["program"], "lockstep": main},
            "dynamic_branch": {"division": bs["analysis"], "states": bs["states"], "residual_program": bs["program"],
             "traces": branch_traces, "wrong_merged_result": bad_value, "relation_failure": relation_failure, "dynamic_k_program": branch_dynamic["program"]},
            "static_cycle": {"program": ss["program"], "lockstep": spin_trace},
            "nonrepeating_prefix": prefix,
            "growing_static_counter": {"division": binding_times(growing, ("x",)), "budget": limit,
             "promoted_program": gs["program"], "example": lockstep(growing, gs, {"x": 5})},
            "promoted_known_input": {"residual_program": promoted["program"], "lockstep": init_check},
            "regressions": {"affine_input_pairs": affine_cases, "BTA_differential_programs": bta_cases,
             "acyclic_input_pairs": residual_cases, "promoted_counter_inputs": 101, "rejected": rejected}}


if __name__ == "__main__":
    print(json.dumps(self_test(), ensure_ascii=False, indent=2, sort_keys=True))