GP1: A typed compiler with a bytecode verifier

Purpose, prerequisites, and nonrequirements#

Build an end-to-end language tool that you can explain without relying on a large compiler framework. Prerequisites are G01–G03, the foundation’s C15–C16, and independent comfort with recursive tree traversal. The work connects mathematical semantics to actual state transitions and tests. It could inform game-engine scripting or configuration tooling, but it does not modify a production engine or propose replacing a production scripting system with a classroom interpreter.

The reference accepts a bounded pure expression language, type-checks it, simplifies selected expressions, compiles to a small stack machine, verifies the bytecode, and executes it. It is not a Python implementation, a secure untrusted-code sandbox, a native-code compiler, or a language with loops, functions, objects, external calls, or mutable user variables.

Functional contract and input/output#

The source spelling uses integer and Boolean literals, variable names, addition, multiplication, less-than comparison, conditional expressions, and let("name", value, body). Examples include 2+3*4 and let("x",3,x*x if x<4 else 0). Source input is one string of 1–4,096 characters. The parser rejects syntax outside the explicit whitelist. It converts accepted host parse nodes into the independent tuple AST from G02, then checks the complete expression’s type. The Python AST documentation defines the host parser’s interfaces; the toy language remains our own restricted semantics. [G-AST]

Accepted types are integer and Boolean, distinct even though Python permits some Boolean/integer interoperation. Addition and multiplication require integers; less-than compares integers and returns Boolean; the conditional requires a Boolean guard and equally typed branches. A let initializer uses the outer environment; its body uses a fresh extended binding. No free variables are allowed in the project source.

The reference limits syntax depth to 48, integer literals to 256 bits, bytecode length to 1,024 instructions, and local slots to 128. Arithmetic results beyond 4,096 bits cause a documented resource exception in the VM. The parser’s host implementation and overall process still consume resources; these limits do not certify resistance to hostile inputs. Some otherwise well-typed expressions can exceed a resource bound and be rejected.

A successful command reports the AST, inferred type, emitted bytecode, interpreter value, and VM value. Error categories distinguish invalid syntax, wrong types, unbound names, invalid bytecode, and resource limits. The program must not invoke eval or exec on the source.

Milestones and acceptance evidence#

First, implement literals and arithmetic through the entire path: parse, type, interpret, compile, verify, run. Second, add lexical let and conditionals with tests that would fail under dynamic scope or leaked bindings. Third, implement verifier joins and reject malformed code before VM execution. Fourth, add semantics-preserving simplification and explain each rewrite’s assumptions. Preserve an early working vertical slice at each stage.

Acceptance requires both branches type-checking even when a guard is constant; correct shadowing; matching interpreter and VM results; rejection of unsupported host syntax; a verifier rejecting stack underflow, wrong operand types, backward or invalid jumps, loads before definite assignment, incompatible join stacks, and malformed termination. Include generated small expressions and hand-designed failures. A low test count is not inherently wrong, but random arithmetic alone is inadequate coverage for control flow and scope.

Hints before the reference solution#

Give every lexical binding a fresh local slot. The source name and the storage slot are different objects. At a branch join, ask which stack shape every path supplies and which locals are definitely available on every path. For rewriting $0e$ to zero, state why evaluating $e$ has no effects and terminates in the ideal language model; do not transfer that rewrite blindly to a language with exceptions or external calls.

Complete solutions: GP1#

Compare the first step where your work differs. A corrected answer is not yet an independent success.

Open every solution

GP1Show solution

Reference architecture and why its stages agree

The pipeline has three representations: host parser nodes, the restricted tuple AST, and instruction tuples. Each transition validates the assumptions the next stage relies on. The host parser handles precedence and surface syntax; the whitelist prevents unrelated syntax from being mistaken for a supported language feature. The type checker defines accepted ASTs; the interpreter supplies an independently structured execution oracle for the compiler. The verifier checks the generated or externally supplied bytecode rather than trusting that it came from the compiler.

This diagram is a software dependency schematic. The comparison is between two implementations of the same accepted AST semantics, not a claim that they share no possible bugs. They share the type checker and input AST, so independent tests of parsing and typing remain necessary.

Back to GP1

Stack-machine meaning and a complete trace#

PUSH appends a literal; LOAD appends a local value; STORE removes the top value and writes a slot. Arithmetic pops the right operand, then the left, and pushes the result. LT has the same operand order but pushes a Boolean. JIF pops a Boolean and jumps when false; JMP always jumps. HALT requires exactly one result.

For let("x",3,x*x if x<4 else 0), one emitted program is:

0 PUSH 3       1 STORE 0
2 LOAD 0       3 PUSH 4       4 LT
5 JIF 10
6 LOAD 0       7 LOAD 0       8 MUL
9 JMP 11
10 PUSH 0
11 HALT

After instruction 1, local slot 0 holds 3 and the stack is empty. Instructions 2–4 produce Boolean true. Instruction 5 consumes it and falls through. Instructions 6–8 produce integer 9; instruction 9 jumps to the halt, which returns 9. With bound value 6, the false branch pushes 0 instead. Each branch reaches instruction 11 with one integer and no leftover guard.

A nested shadowed name gets a different slot. In let("x",2,let("x",x+1,x)+x), the outer binding occupies slot 0 and the inner initializer loads it before storing the new value into slot 1. The inner body loads slot 1; the final outer occurrence still loads slot 0. The result is $3+2=5$. Slot lifetime here is a bounded VM representation choice; source lexical scope determines which slot a name selects.

A verifier is an abstract execution, not a sample run#

At each instruction the verifier tracks a stack of types and a map from definitely assigned local slots to types. It executes transfer rules on these abstract states. A LOAD requires the slot in the map; an arithmetic operation requires two integer types; JIF requires a Boolean. It analyzes both successors regardless of the guard’s eventual value.

At a join, incoming stack type sequences must match exactly. Local maps are intersected, retaining a slot only if every incoming path assigns it the same type. A slot assigned on just one branch is not definitely assigned afterward. All jumps go to strictly later instruction indices, so every incoming state is known before an instruction is processed in ascending order. That acyclic restriction makes one ordered pass sufficient. A language with backward jumps would need a fixed-point/worklist analysis and a termination argument for the analyzer, not this one-pass assumption.

The verifier also rejects unreachable instructions by policy. That is stricter than necessary for all bytecode safety systems, but simplifies this bounded contract. It rejects a final stack with zero or multiple values rather than guessing which value is the result. Type safety means accepted instructions cannot fail from the modeled stack/type/local errors; it does not establish the intended business result or exclude a documented integer-resource exception.

The semantics-preservation argument#

Use structural induction on a well-typed AST under corresponding source bindings and VM local slots. A compiled expression must leave exactly its value atop the incoming stack and preserve unrelated stack entries. A literal pushes its own value. A variable loads the corresponding binding slot. For arithmetic, the induction hypotheses give each operand value in the intended left-to-right order; the machine operation applies the same integer operation. For comparison, the analogous rule yields the same Boolean.

For a let binding, the initializer is compiled in the old environment. Its resulting value is stored in a fresh slot, and the body is compiled under the extended name-to-slot map. This matches lexical semantics. For a conditional, the guard hypothesis supplies the same Boolean as the interpreter; the branch jump executes exactly the selected branch and leaves the same result type. The final halt returns that value. Fresh slot allocation prevents shadowed names from overwriting a still-needed outer binding.

The statement is for accepted programs whose executions stay inside the stated resource limits. The ideal mathematical language terminates because its finite AST has no recursive calls or loops. A VM instruction bound and forward-only branches give a bounded number of instruction executions, but large-integer arithmetic still has nonconstant cost. Do not label every arithmetic operation constant time without specifying an integer-size model.

What simplification preserves#

The simplifier first type-checks the entire expression. It recursively folds literal arithmetic and comparisons when the folded literal remains within 256 bits, eliminates a constant conditional guard, and applies integer identities such as $e+0=e$, $e\cdot1=e$, and $e\cdot0=0$. It does not make ill-typed dead branches valid by deleting them before type checking.

These rules preserve values in this pure, terminating ideal language. They do not preserve every resource-limit outcome: simplifying a large computation multiplied by zero may avoid an exception that the bounded VM would otherwise raise. The project explicitly separates ideal semantic equality from identical resource consumption or exception behavior. Extending the source language with effects, division-by-zero, or nontermination requires revisiting the rewrite proofs.

Complete buildable reference#

The full compiler file follows. Its import of language.py refers to G02’s complete reference, also in the companion. Run from the code directory with python -m solutions.compiler. The CLI displays the ordinary compilation path; the tests additionally call the simplifier.

"""GP1: pure expressions -> typed AST -> verified, forward-only bytecode.
This is an educational compiler, not a sandbox for hostile programs.
"""
import ast
import sys
from .language import infer, evaluate


def parse(source):
    if type(source) is not str or not 1 <= len(source) <= 4096:
        raise ValueError("source must contain 1..4096 characters")
    try:
        host = ast.parse(source, mode="eval")
    except (SyntaxError, RecursionError) as error:
        raise ValueError("invalid source syntax") from error

    def convert(node, depth=0):
        if depth > 48:
            raise ValueError("syntax depth exceeds 48")
        if isinstance(node, ast.Constant) and type(node.value) in (int, bool):
            if type(node.value) is int and node.value.bit_length() > 256:
                raise ValueError("integer literal exceeds 256 bits")
            return node.value
        if isinstance(node, ast.UnaryOp) and isinstance(node.op, ast.USub):
            if isinstance(node.operand, ast.Constant) and type(node.operand.value) is int:
                return -convert(node.operand, depth+1)
        if isinstance(node, ast.Name):
            return node.id
        if isinstance(node, ast.BinOp) and type(node.op) in (ast.Add, ast.Mult):
            tag = "+" if isinstance(node.op, ast.Add) else "*"
            return tag, convert(node.left,depth+1), convert(node.right,depth+1)
        if isinstance(node, ast.Compare) and len(node.ops) == 1 and isinstance(node.ops[0],ast.Lt):
            return "<",convert(node.left,depth+1),convert(node.comparators[0],depth+1)
        if isinstance(node, ast.IfExp):
            return ("if",convert(node.test,depth+1),convert(node.body,depth+1),
                    convert(node.orelse,depth+1))
        if (isinstance(node, ast.Call) and isinstance(node.func,ast.Name)
                and node.func.id == "let" and len(node.args) == 3 and not node.keywords):
            name = node.args[0]
            if not isinstance(name,ast.Constant) or type(name.value) is not str or not name.value.isidentifier():
                raise ValueError("let requires a quoted identifier")
            return "let",name.value,convert(node.args[1],depth+1),convert(node.args[2],depth+1)
        raise ValueError("unsupported source construct")

    expression = convert(host.body)
    infer(expression)  # both branches checked, including dead branches
    return expression


def simplify(expression):
    infer(expression)

    def visit(e):
        if type(e) is not tuple:
            return e
        tag = e[0]
        if tag == "let":
            return tag,e[1],visit(e[2]),visit(e[3])
        if tag == "if":
            c,a,b = visit(e[1]),visit(e[2]),visit(e[3])
            return (a if c else b) if type(c) is bool else (tag,c,a,b)
        a,b = visit(e[1]),visit(e[2])
        if type(a) is int and type(b) is int:
            value = a+b if tag == "+" else a*b if tag == "*" else a < b
            if type(value) is bool or value.bit_length() <= 256:
                return value
        if tag == "+":
            if type(a) is int and a == 0: return b
            if type(b) is int and b == 0: return a
        if tag == "*":
            if (type(a) is int and a == 0) or (type(b) is int and b == 0): return 0
            if type(a) is int and a == 1: return b
            if type(b) is int and b == 1: return a
        return tag,a,b

    return visit(expression)


def compile_expr(expression):
    infer(expression)
    instructions, next_slot = [],0

    def emit(instruction):
        if len(instructions) >= 1023:  # reserve HALT
            raise ValueError("bytecode exceeds 1024 instructions")
        instructions.append(instruction)
        return len(instructions)-1

    def visit(e, scope):
        nonlocal next_slot
        if type(e) in (int,bool):
            if type(e) is int and e.bit_length() > 256:
                raise ValueError("literal exceeds 256 bits")
            emit(("PUSH",e))
        elif type(e) is str:
            emit(("LOAD",scope[e]))
        elif e[0] == "let":
            visit(e[2],scope)
            if next_slot >= 128:
                raise ValueError("local slots exceed 128")
            slot = next_slot
            next_slot += 1
            emit(("STORE",slot))
            visit(e[3],{**scope,e[1]:slot})
        elif e[0] == "if":
            visit(e[1],scope)
            branch = emit(("JIF",None))
            visit(e[2],scope)
            jump = emit(("JMP",None))
            instructions[branch] = ("JIF",len(instructions))
            visit(e[3],scope)
            instructions[jump] = ("JMP",len(instructions))
        else:
            visit(e[1],scope)
            visit(e[2],scope)
            emit(({"+":"ADD","*":"MUL","<":"LT"}[e[0]],))

    visit(expression,{})
    instructions.append(("HALT",))
    verify(instructions)
    return instructions


def verify(code):
    """Abstractly execute all acyclic paths; intersect definitely assigned locals."""
    if not isinstance(code,(list,tuple)) or not 1 <= len(code) <= 1024:
        raise ValueError("bounded nonempty instruction sequence required")
    states = {0:((),{})}
    result_type = None

    def merge(target, stack, slots):
        incoming = tuple(stack)
        if not 0 <= target < len(code):
            raise ValueError("fallthrough or jump beyond bytecode")
        if target not in states:
            states[target] = incoming,dict(slots)
        else:
            old_stack,old_slots = states[target]
            if incoming != old_stack:
                raise ValueError("incompatible join stacks")
            states[target] = incoming,{k:v for k,v in old_slots.items() if slots.get(k) == v}

    for pc,instruction in enumerate(code):
        if pc not in states:
            raise ValueError("unreachable instruction rejected by policy")
        if type(instruction) is not tuple or not instruction or type(instruction[0]) is not str:
            raise ValueError("malformed instruction")
        op = instruction[0]
        arity = {"PUSH":2,"LOAD":2,"STORE":2,"JIF":2,"JMP":2,
                 "ADD":1,"MUL":1,"LT":1,"HALT":1}.get(op)
        if arity is None or len(instruction) != arity:
            raise ValueError("unknown instruction or arity")
        stack,slots = states[pc]
        stack,slots = list(stack),dict(slots)

        def pop(expected=None):
            if not stack:
                raise ValueError("stack underflow")
            typ = stack.pop()
            if expected is not None and typ != expected:
                raise ValueError("wrong operand type")
            return typ

        if op == "PUSH":
            value = instruction[1]
            if type(value) not in (int,bool) or (type(value) is int and value.bit_length() > 256):
                raise ValueError("invalid literal")
            stack.append("bool" if type(value) is bool else "int")
        elif op in ("LOAD","STORE"):
            slot = instruction[1]
            if type(slot) is not int or not 0 <= slot < 128:
                raise ValueError("invalid slot")
            if op == "LOAD":
                if slot not in slots:
                    raise ValueError("load before definite assignment")
                stack.append(slots[slot])
            else:
                slots[slot] = pop()
        elif op in ("ADD","MUL","LT"):
            pop("int"); pop("int")
            stack.append("bool" if op == "LT" else "int")
        elif op in ("JIF","JMP"):
            target = instruction[1]
            if type(target) is not int or not pc < target < len(code):
                raise ValueError("jumps must target strictly later instructions")
            if op == "JIF": pop("bool")
            merge(target,stack,slots)
            if op == "JMP": continue
        elif op == "HALT":
            if len(stack) != 1:
                raise ValueError("HALT requires exactly one result")
            if result_type is not None and result_type != stack[0]:
                raise ValueError("incompatible result types")
            result_type = stack[0]
            continue
        merge(pc+1,stack,slots)
    if result_type is None:
        raise ValueError("no valid halt")
    return result_type


def run(code):
    verify(code)
    stack,slots,pc = [],{},0
    while True:
        instruction = code[pc]
        op = instruction[0]
        if op == "PUSH": stack.append(instruction[1])
        elif op == "LOAD": stack.append(slots[instruction[1]])
        elif op == "STORE": slots[instruction[1]] = stack.pop()
        elif op in ("ADD","MUL","LT"):
            b,a = stack.pop(),stack.pop()
            value = a+b if op == "ADD" else a*b if op == "MUL" else a < b
            if type(value) is int and value.bit_length() > 4096:
                raise ValueError("arithmetic result exceeds 4096 bits")
            stack.append(value)
        elif op == "JIF":
            if not stack.pop():
                pc = instruction[1]
                continue
        elif op == "JMP":
            pc = instruction[1]
            continue
        elif op == "HALT": return stack.pop()
        pc += 1


if __name__ == "__main__":
    source = sys.argv[1] if len(sys.argv)>1 else 'let("x",3,x*x if x<4 else 0)'
    expression = parse(source)
    code = compile_expr(expression)
    print("AST:",expression,"type:",infer(expression))
    for pc,instruction in enumerate(code): print(pc,instruction)
    print("interpreter:",evaluate(expression),"VM:",run(code))

Testing, failure analysis, and evaluation rubric#

The current test suite compares 200 generated small trees with the recursive interpreter, tests both branch outcomes and shadowing, and exercises verifier rejection cases. Added tests compare simplification semantics, ensure dead ill-typed branches are rejected, and avoid folding a result into an oversized source literal. Generated trees are limited in depth and form; they supplement, not replace, the written argument and hand-crafted counterexamples.

When a differential test fails, preserve the original tree and reduce it to a smaller failure by simplifying subtrees while keeping the mismatch. Print both values, the bytecode, and a stack/local trace. A mismatch at a branch often indicates incorrect jump patching or a leftover guard. A mismatch only with shadowing suggests a scope map reused incorrectly. A verifier disagreement may expose an overly restrictive policy rather than a wrong runtime result; compare against the written accepted language.

Evaluate five dimensions separately: specification and rejection behavior; semantic reasoning; implementation clarity; independent tests and debugging; and communication of limits. Each can be missing, guided, independently adequate, or independently transferred. A correct result on one expression is not a passing project when malformed bytecode can underflow the stack. A clean verifier is not sufficient when source scope is wrong.

Unassigned extensions. Add subtraction, tuples, closures, or loops one at a time, updating the syntax, typing, semantics, compiler, verifier, and tests together. A register allocator or SSA representation is a substantial further project, not a small feature implied by this reference. Native compiler performance and hostile-code isolation need additional specialized work.