#!/usr/bin/env python3
"""CS03b educational oracles, Python 3.10+, standard library only.
No real ELF, ISA, LLVM or garbage-collected host implementation is claimed.
All check() calls survive python -O. Public drivers are small reference models.
Trace events, full validation, AST/environment copying and output are separate costs.
"""
from collections import deque
from dataclasses import dataclass
import argparse
import copy
import json
from pathlib import Path

class ModelError(ValueError):
    pass

def check(ok, message):
    if not ok:
        raise ModelError(message)

@dataclass(frozen=True)
class Rule:
    name: str
    pattern: str
    mode: str = 'literal'
    skip: bool = False
    def step(self, state, char):
        if self.mode == 'literal':
            return state+1 if state < len(self.pattern) and self.pattern[state] == char else None
        if self.mode == 'id':
            return 1 if char in 'abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ_' + ('0123456789' if state else '') else None
        if self.mode == 'int':
            return 1 if char in '0123456789' else None
        if self.mode == 'space':
            return 1 if char in ' \n\t\r' else None
        if self.mode == 'astar_b':
            return (0 if char == 'a' else 1 if char == 'b' else None) if state == 0 else None
        raise ModelError('unknown rule mode')
    def accepts(self, state):
        return state == len(self.pattern) if self.mode == 'literal' else state == 1

KEYWORDS = ['let','in','fun','ref','fst','snd']
RULES = [Rule(x.upper(),x) for x in KEYWORDS] + [Rule('ID','','id'),Rule('INT','','int')]
RULES += [Rule(x,x) for x in ['->',':=','+','!','(',')',',',';','=']]
RULES += [Rule('WS','','space',True)]

def lex(text, rules=None):
    rules = RULES if rules is None else rules
    check(all(not (r.mode == 'literal' and not r.pattern) for r in rules),'empty-token rule')
    out=[]; p=0; stats={'character_attempts':0,'rule_attempts':0,'accepted_characters':0}
    while p<len(text):
        state=tuple((i,0) for i in range(len(rules))); j=p; last=None
        while j<len(text):
            stats['character_attempts']+=1
            nxt=[]
            for i,q in state:
                stats['rule_attempts']+=1
                v=rules[i].step(q,text[j])
                if v is not None: nxt.append((i,v))
            if not nxt: break
            state=tuple(nxt); j+=1; stats['accepted_characters']+=1
            labels=[i for i,q in state if rules[i].accepts(q)]
            if labels: last=(j,min(labels))
        check(last is not None,f'lexical error at {p}')
        end,i=last
        if not rules[i].skip: out.append((rules[i].name,text[p:end],p,end))
        p=end
    return out+[('EOF','',len(text),len(text))],stats

class Parser:
    """A recursive-descent adapter, not a replacement LL/LR theory implementation."""
    def __init__(self,tokens): self.tokens=tokens; self.i=0
    def at(self,k): return self.tokens[self.i][0]==k
    def take(self,k):
        t=self.tokens[self.i]; check(t[0]==k,f'expected {k} at {t[2]}, got {t[0]}'); self.i+=1; return t
    def expr(self):
        if self.at('LET'):
            self.take('LET'); b=self.take('ID'); self.take('='); rhs=self.expr(); self.take('IN')
            return ('let',b[1],rhs,self.expr())
        if self.at('FUN'):
            self.take('FUN'); b=self.take('ID'); self.take('->'); return ('fun',b[1],self.expr())
        e=self.assign()
        if self.at(';'): self.take(';'); return ('seq',e,self.expr())
        return e
    def assign(self):
        e=self.add()
        if self.at(':='): self.take(':='); return ('store',e,self.assign())
        return e
    def add(self):
        e=self.prefix()
        while self.at('+'): self.take('+'); e=('add',e,self.prefix())
        return e
    def prefix(self):
        for tok,op in [('!','load'),('REF','ref'),('FST','fst'),('SND','snd')]:
            if self.at(tok): self.take(tok); return (op,self.prefix())
        e=self.primary()
        while self.at('('):
            self.take('('); arg=self.expr(); self.take(')'); e=('call',e,arg)
        return e
    def primary(self):
        if self.at('INT'): return ('num',int(self.take('INT')[1]))
        if self.at('ID'):
            t=self.take('ID'); return ('var',t[1],(t[2],t[3]))
        self.take('(')
        if self.at(')'): self.take(')'); return ('unit',)
        e=self.expr()
        if self.at(','): self.take(','); e=('pair',e,self.expr())
        self.take(')'); return e
    def parse(self):
        e=self.expr(); self.take('EOF'); return e

class Resolver:
    def __init__(self): self.stack={}; self.next_id=0; self.decisions=[]; self.declarations=[]
    def fresh(self,name):
        self.next_id+=1; self.declarations.append((self.next_id,name)); return self.next_id
    def body(self,name,b,e):
        self.stack.setdefault(name,[]).append(b)
        try: return self.resolve(e)
        finally:
            self.stack[name].pop()
            if not self.stack[name]: del self.stack[name]
    def resolve(self,e):
        op=e[0]
        if op in ('num','unit'): return e
        if op=='var':
            span=e[2] if len(e)>2 else None
            check(e[1] in self.stack,f'unbound name {e[1]} at {span}')
            b=self.stack[e[1]][-1]; self.decisions.append((e[1],b,span)); return ('var',b,span)
        if op=='fun':
            b=self.fresh(e[1]); return ('fun',b,self.body(e[1],b,e[2]))
        if op=='let':
            b=self.fresh(e[1]); rhs=self.resolve(e[2]); return ('let',b,rhs,self.body(e[1],b,e[3]))
        return (op,*(self.resolve(x) for x in e[1:]))

class Normalizer:
    def __init__(self): self.next_id=0
    def fresh(self): self.next_id+=1; return f't{self.next_id}'
    def norm(self,e): return self.atom(e,lambda a:('ret',a))
    def atom(self,e,k):
        op=e[0]
        if op in ('num','unit','var'): return k(e)
        if op=='fun': return k(('fun',e[1],self.norm(e[2])))
        if op=='let': return self.atom(e[2],lambda a:('let',e[1],a,self.atom(e[3],k)))
        if op=='seq': return self.atom(e[1],lambda ignored:self.atom(e[2],k))
        def args(i,values):
            if i==len(e):
                b=self.fresh(); return ('let',b,(op,*values),k(('var',b)))
            return self.atom(e[i],lambda a:args(i+1,values+(a,)))
        return args(1,())

def anf_wellformed(e):
    arity={'ref':1,'load':1,'store':2,'add':2,'call':2,'pair':2,'fst':1,'snd':1}
    def node(x): return isinstance(x,(tuple,list)) and len(x)>0
    def atomic(a):
        if not node(a): return False
        if a[0]=='fun': return len(a)==3 and anf_wellformed(a[2])
        if a[0]=='num': return len(a)==2 and type(a[1]) is int
        if a[0]=='unit': return len(a)==1
        if a[0]=='var': return len(a) in (2,3) and isinstance(a[1],(str,int))
        return False
    def simple(c):
        if not node(c): return False
        if c[0] in ('num','unit','var','fun'): return atomic(c)
        return c[0] in arity and len(c)==arity[c[0]]+1 and all(atomic(a) for a in c[1:])
    if not node(e): return False
    return (e[0]=='ret' and len(e)==2 and atomic(e[1])) or (e[0]=='let' and len(e)==4 and simple(e[2]) and anf_wellformed(e[3]))

def free(e):
    if e[0]=='var': return {e[1]}
    if e[0] in ('num','unit'): return set()
    if e[0]=='fun': return free(e[2])-{e[1]}
    if e[0]=='let': return free(e[2]) | (free(e[3])-{e[1]})
    return set().union(*(free(x) for x in e[1:]))

class ClosureCompiler:
    """Adapter to the existing closure-conversion contract: code + explicit env slots."""
    def __init__(self): self.code={}; self.next_label=0
    def compile(self,e):
        op=e[0]
        if op=='fun':
            self.next_label+=1; label=f'L{self.next_label}'; captures=sorted(free(e[2])-{e[1]},key=str)
            body=self.compile(e[2]); self.code[label]=(e[1],captures,body)
            return ('cc',label,tuple(('var',b) for b in captures))
        if op in ('num','unit','var'): return e
        if op=='let': return ('let',e[1],self.compile(e[2]),self.compile(e[3]))
        return (op,*(self.compile(x) for x in e[1:]))

@dataclass(frozen=True)
class Loc: addr:int
@dataclass
class Closure: param:object; body:tuple; env:dict
@dataclass
class Converted: label:str; fields:tuple

class Evaluator:
    def __init__(self,trace=False,code=None,fuel=100000):
        self.heap={}; self.events=[] if trace else None; self.event_count=0; self.nodes=0; self.env_entries_copied=0
        self.code=code or {}; self.fuel=fuel
    def emit(self,*e):
        self.event_count+=1
        if self.events is not None: self.events.append(e)
    def extend(self,env,b,v):
        self.env_entries_copied+=len(env); out=dict(env); out[b]=v; return out
    def eval(self,e,env=None):
        env={} if env is None else env
        self.nodes+=1; self.fuel-=1; check(self.fuel>=0,'evaluation fuel exhausted (not proof of divergence)')
        op=e[0]
        if op=='num': return e[1]
        if op=='unit': return None
        if op=='var': check(e[1] in env,'unknown variable ID'); return env[e[1]]
        if op=='fun':
            self.env_entries_copied+=len(env); return Closure(e[1],e[2],dict(env))
        if op=='cc': return Converted(e[1],tuple(self.eval(a,env) for a in e[2]))
        if op=='let': return self.eval(e[3],self.extend(env,e[1],self.eval(e[2],env)))
        if op=='ret': return self.eval(e[1],env)
        if op=='seq': self.eval(e[1],env); return self.eval(e[2],env)
        vals=[self.eval(a,env) for a in e[1:]]
        if op=='ref':
            p=Loc(len(self.heap)+1); self.heap[p.addr]=vals[0]; self.emit('alloc',p.addr,vals[0]); return p
        if op in ('load','store'):
            p=vals[0]; check(isinstance(p,Loc) and p.addr in self.heap,'invalid cell')
            if op=='load': self.emit('load',p.addr,self.heap[p.addr]); return self.heap[p.addr]
            self.heap[p.addr]=vals[1]; self.emit('store',p.addr,vals[1]); return None
        if op=='add': check(all(type(v) is int for v in vals),'integer operands required'); return sum(vals)
        if op=='pair': return tuple(vals)
        if op in ('fst','snd'): check(type(vals[0]) is tuple and len(vals[0])==2,'pair required'); return vals[0][op=='snd']
        if op=='call':
            f,arg=vals
            if isinstance(f,Closure): return self.eval(f.body,self.extend(f.env,f.param,arg))
            check(isinstance(f,Converted) and f.label in self.code,'function required')
            p,captures,body=self.code[f.label]; check(len(captures)==len(f.fields),'environment arity')
            local=dict(zip(captures,f.fields)); self.env_entries_copied+=len(captures)
            return self.eval(body,self.extend(local,p,arg))
        raise ModelError('unknown operation '+op)

SOURCE='''let x = ref 4 in
let make = fun u -> (fun d -> (x := !x + d; !x), fun v -> !x) in
let p = make(0) in
let f = fst p in
let g = snd p in
let x = 100 in
(f((f(1); 2)), (g(0), x))'''

def frontend(source=SOURCE, trace=False):
    tokens,lexstats=lex(source); ast=Parser(tokens).parse(); resolver=Resolver(); resolved=resolver.resolve(ast)
    normal=Normalizer().norm(resolved); check(anf_wellformed(normal),'ANF grammar violation')
    cc=ClosureCompiler(); converted=cc.compile(normal)
    observations=[]; costs=[]
    for name,e,code in [('source',ast,None),('resolved',resolved,None),('anf',normal,None),('explicit_environment',converted,cc.code)]:
        vm=Evaluator(trace=trace,code=code); value=vm.eval(e)
        observations.append((value,vm.heap,vm.events))
        costs.append({'stage':name,'ast_evaluations':vm.nodes,'environment_entries_copied':vm.env_entries_copied,'event_count':vm.event_count})
    check(all(o==observations[0] for o in observations),'stage observation mismatch')
    return {'result':observations[0][0],'heap':observations[0][1],'events':observations[0][2],'tokens':tokens,'lex_cost':lexstats,'declarations':resolver.declarations,'binding_decisions':resolver.decisions,'resolved':resolved,'anf':normal,'code':cc.code,'costs':costs}

def needs(direct,calls):
    check(set(direct)==set(calls),'function domain mismatch')
    check(all(g in direct for gs in calls.values() for g in gs),'unknown callee')
    current={f:set(v) for f,v in direct.items()}; rounds=0; edge_scans=0; copies=0; union_inputs=0; equality_inputs=0
    while True:
        nxt={f:set(v) for f,v in current.items()}; copies+=sum(map(len,current.values()))
        for f,gs in calls.items():
            for g in gs: nxt[f].update(current[g]); edge_scans+=1; union_inputs+=len(current[g])
        rounds+=1
        equality_inputs+=sum(len(nxt[f])+len(current[f]) for f in current)
        if nxt==current: return current,{'rounds_including_stable':rounds,'edge_scans':edge_scans,'copied_set_entries':copies,'union_input_entries':union_inputs,'set_equality_input_entries_upper_bound':equality_inputs}
        current=nxt

def lift_run(start,n,x,need_map):
    check(start in ('f','g','h') and type(n) is int and n>=0,'invalid lifting fixture')
    f=start; args={'x':x}; steps=0
    while True:
        check(need_map[f] <= args.keys(),'missing lifted parameter'); steps+=1
        if n==0: return ({'f':0,'g':args.get('x'),'h':1}[f],steps)
        g={'f':'g','g':'h','h':'f'}[f]
        args={v:args[v] for v in need_map[g] if v in args}; f=g; n-=1

def parallel_assign(registers, assignments):
    """Read all right-hand sides in the old register state before any writes."""
    values=[(name,expression(registers)) for name,expression in assignments]
    result=dict(registers)
    for name,value in values:result[name]=value
    return result

def sequential_assign_wrong(registers, assignments):
    """Deliberate counterexample: later RHS sees earlier writes."""
    result=dict(registers)
    for name,expression in assignments:result[name]=expression(result)
    return result

def tail_sum(n,trace=False):
    check(type(n) is int and n>=0,'nonnegative integer n required')
    initial=n; a=0; events=[] if trace else None; steps=0
    fp,sp,parent,ret,saved=8144,8112,8192,'main.after_sum',55
    while True:
        check(a+n*(n+1)//2==initial*(initial+1)//2,'sum invariant')
        if events is not None: events.append((n,a,fp,sp,parent,ret,saved))
        if n==0: break
        new=parallel_assign({'n':n,'a':a}, [('n',lambda old:old['n']-1),('a',lambda old:old['a']+old['n'])]); n,a=new['n'],new['a']; steps+=1
    return {'value':a,'tail_transfers':steps,'max_sum_frames':1,'frame_bytes':48,'ordinary_frames':initial+1,'ordinary_bytes':48*(initial+1),'returned_fp':parent,'returned_sp':8160,'returned_S':saved,'trace':events}

def align(n,a):
    check(type(a) is int and a>0 and a&(a-1)==0,'alignment must be a positive power of two')
    return (n+a-1)//a*a

def link(objects,bases):
    """Input dictionaries are never changed. Failure before result has no external writes."""
    check(len({o['name'] for o in objects})==len(objects),'duplicate object identity')
    check(all(type(v) is int and 0<=v<2**32 for v in bases.values()),'bad region base')
    cursors=dict(bases); layout={}; ranges=[]; sizes={}
    for o in objects:
        for section,spec in o['sections'].items():
            check(section in cursors,'missing region'); data=bytes(spec['data']); p=align(cursors[section],spec['align'])
            check(p+len(data)<=2**32,'section address overflow')
            ranges.append((p,p+len(data))); key=(o['name'],section); layout[key]=p; sizes[key]=len(data); cursors[section]=p+len(data)
    ordered_ranges=sorted(ranges)
    check(all(a[1]<=b[0] for a,b in zip(ordered_ranges,ordered_ranges[1:])),'section overlap')
    globals_={}; locals_={}
    for o in objects:
        for sym in o['symbols']:
            check(sym['binding'] in ('local','global'),'unsupported symbol binding')
            key=(o['name'],sym['section']); off=sym['offset']; check(key in layout and type(off) is int and 0<=off<sizes[key],'symbol offset outside section')
            table,key2=(globals_,sym['name']) if sym['binding']=='global' else (locals_,(o['name'],sym['name']))
            check(key2 not in table,'duplicate symbol'); table[key2]=layout[key]+off
    patches=[]; occupied=set()
    for o in objects:
        for r in o['relocations']:
            check(r['type'] in ('ABS32','PCREL16'),'unknown relocation type')
            key=(o['name'],r['section']); off=r['offset']; width=4 if r['type']=='ABS32' else 2
            check(key in layout and type(off) is int and 0<=off and off+width<=sizes[key],'patch outside section')
            P=layout[key]+off; slots=set(range(P,P+width)); check(not occupied&slots,'overlapping relocation fields'); occupied |= slots
            check(r['binding'] in ('local','global'),'unsupported reference binding')
            table,symkey=(globals_,r['symbol']) if r['binding']=='global' else (locals_,(o['name'],r['symbol']))
            check(symkey in table,'unresolved symbol'); S=table[symkey]; A=r['addend']; check(type(A) is int,'invalid addend')
            value=S+A-(P if r['type']=='PCREL16' else 0)
            check((-2**15<=value<2**15) if width==2 else (0<=value<2**32),'relocation overflow')
            encoded=value.to_bytes(width,'little',signed=width==2); patches.append({'object':o['name'],'section':r['section'],'offset':off,'P':P,'S':S,'A':A,'value':value,'bytes':encoded.hex()})
    image={}
    # Sections, not padding, are stored sparsely. Layout accounting includes padding separately.
    for o in objects:
        for sec,spec in o['sections'].items():
            for i,b in enumerate(spec['data']): image[layout[o['name'],sec]+i]=b
    for p in patches:
        for i,b in enumerate(bytes.fromhex(p['bytes'])): image[p['P']+i]=b
    return {'layout':{a+'.'+b:p for (a,b),p in layout.items()},'globals':globals_,'locals':{a+'.'+b:p for (a,b),p in locals_.items()},'patches':patches,'image':image,'stored_section_bytes':len(image),'region_spans':{k:cursors[k]-bases[k] for k in bases}}

def object_fixture():
    def sec(size,alignment): return {'data':[0]*size,'align':alignment}
    def sym(name,binding,section,offset): return dict(name=name,binding=binding,section=section,offset=offset)
    def rel(section,offset,type_,symbol,A): return dict(section=section,offset=offset,type=type_,symbol=symbol,addend=A,binding='global')
    return [dict(name='A',sections={'text':sec(12,4),'data':sec(8,8)},symbols=[sym('main','global','text',0),sym('scratch','local','data',4)],relocations=[rel('text',2,'PCREL16','inc',-2),rel('data',0,'ABS32','counter',4)]),dict(name='B',sections={'text':sec(8,8),'data':sec(8,8)},symbols=[sym('inc','global','text',0),sym('counter','global','data',0),sym('scratch','local','data',4)],relocations=[rel('text',2,'PCREL16','main',-2)])]

def call_target(image,pc):
    check(all(pc+2+i in image for i in range(2)),'missing displacement')
    disp=int.from_bytes(bytes(image[pc+2+i] for i in range(2)),'little',signed=True)
    return pc+4+disp

class ReferenceCounter:
    """Trusted heap-test interface. Raw IDs are not unforgeable mutator capabilities.
    Caller must supply new references already protected by a legal live handle.
    Allocation/count checks reject dangling or zero objects, not unreachable positive cycles.
    """
    def __init__(self,roots=(),trace=False,max_count=None):
        check(max_count is None or type(max_count) is int and max_count>=1,'invalid max_count')
        self.roots={r:None for r in roots}; self.heap={}; self.rc={}; self.queue=deque(); self.events=[] if trace else None
        self.max_count=max_count; self.core_operations=0; self.validation_slots=0
    def emit(self,*event):
        self.core_operations+=1
        if self.events is not None: self.events.append(event)
    def slot(self,s):
        if isinstance(s,str): check(s in self.roots,'unknown root slot'); return self.roots,s
        check(isinstance(s,tuple) and len(s)==2,'bad slot handle'); o,i=s
        check(o in self.heap and type(i) is int and 0<=i<len(self.heap[o]),'invalid field slot')
        check(self.rc[o]>0,'field owner pending release'); return self.heap[o],i
    def alloc(self,root,oid,field_count=0):
        check(root in self.roots and self.roots[root] is None,'allocation needs empty root')
        check(oid not in self.heap and oid is not None,'duplicate/null object identity')
        check(type(field_count) is int and field_count>=0,'invalid field count')
        self.heap[oid]=[None]*field_count; self.rc[oid]=1; self.roots[root]=oid; self.emit('alloc',oid,field_count)
    def replace(self,s,new):
        store,key=self.slot(s); old=store[key]
        check(new is None or new in self.heap and self.rc[new]>0,'invalid new reference or resurrection')
        check(old is None or old in self.heap and self.rc[old]>0,'invalid old reference')
        if old==new: self.emit('same',str(s)); return
        check(new is None or self.max_count is None or self.rc[new]<self.max_count,'reference count overflow')
        if new is not None: self.rc[new]+=1
        store[key]=new
        if old is not None:
            self.rc[old]-=1
            if self.rc[old]==0:self.queue.append(old)
        self.emit('replace',str(s),old,new)
    def drain(self,budget=None):
        check(budget is None or type(budget) is int and budget>=0,'invalid object budget')
        freed=[]
        while self.queue and (budget is None or len(freed)<budget):
            o=self.queue[0]; check(o in self.heap and self.rc[o]==0,'corrupt release queue')
            # Corruption preflight only for this object. Valid model preserves these facts inductively.
            counts={}
            for child in self.heap[o]:
                if child is not None: counts[child]=counts.get(child,0)+1
            check(all(c in self.rc and self.rc[c]>=v for c,v in counts.items()),'invalid outgoing counts')
            self.queue.popleft()
            for child in self.heap[o]:
                if child is not None:
                    self.rc[child]-=1
                    if self.rc[child]==0:self.queue.append(child)
                self.emit('delete_edge',o,child)
            del self.heap[o]; del self.rc[o]; freed.append(o); self.emit('free',o)
        return freed
    def validate(self):
        counts=dict.fromkeys(self.heap,0); slots=list(self.roots.values())+[v for fs in self.heap.values() for v in fs]; self.validation_slots+=len(slots)
        for v in slots:
            check(v is None or v in counts,'dangling RC pointer')
            if v is not None: counts[v]+=1
        check(counts==self.rc,'reference count invariant')
        check(len(set(self.queue))==len(self.queue) and set(self.queue)=={o for o,c in self.rc.items() if c==0},'zero-queue invariant')
        return True

def reachable(roots,heap):
    seen=set(); q=list(roots)
    while q:
        p=q.pop()
        if p is None or p in seen: continue
        check(p in heap,'dangling trace pointer'); seen.add(p); q.extend(heap[p])
    return seen

class GenerationalHeap:
    """All fields are managed pointers; object size is 8*(1+field count)."""
    def __init__(self,old,young,roots,remembered=(),trace=False):
        self.old=copy.deepcopy(old); self.young=copy.deepcopy(young); self.roots=dict(roots); self.remembered=set(remembered)
        self.events=[] if trace else None; self.core_operations=0; self.preflight_words=0
        self.validate()
    def validate(self):
        check(not self.old.keys() & self.young.keys(),'duplicate generation identity')
        heap={**self.old,**self.young}; ranges=[]
        for p,fs in heap.items():
            check(type(p) is int and p>=0,'invalid object address')
            # Object bases follow the existing 8-byte-aligned heap model.
            check(p%8==0,'unaligned object address'); ranges.append((p,p+8*(1+len(fs))))
            for v in fs: self.preflight_words+=1; check(v is None or v in heap,'invalid pointer')
        ordered=sorted(ranges); check(all(a[1]<=b[0] for a,b in zip(ordered,ordered[1:])),'overlapping heap objects')
        for v in self.roots.values(): self.preflight_words+=1; check(v is None or v in heap,'invalid root pointer')
        for o,i in self.remembered: check(o in self.old and type(i) is int and 0<=i<len(self.old[o]),'invalid remembered slot')
        return True
    def write(self,o,i,new,barrier=True):
        heap=self.old if o in self.old else self.young
        check(o in heap and type(i) is int and 0<=i<len(heap[o]),'invalid write slot')
        check(new is None or new in self.old or new in self.young,'invalid new pointer')
        # Set insertion precedes publication so a Python allocation failure cannot silently omit the barrier.
        if barrier and o in self.old and new in self.young:self.remembered.add((o,i))
        heap[o][i]=new; self.core_operations+=1
        if self.events is not None:self.events.append(('write',o,i,new,barrier))
    def promote(self,p):
        check(p in self.young,'only young objects promote')
        extra={(p,i) for i,v in enumerate(self.young[p]) if v in self.young and v!=p}
        # Compute and reserve complete new metadata before changing generation membership.
        new_m=self.remembered|extra; fields=self.young[p]; self.old[p]=fields; del self.young[p]; self.remembered=new_m
        self.core_operations+=len(fields)+1
    def minor(self,to_base,capacity,preflight=True):
        check(type(to_base) is int and to_base>=0 and to_base%8==0,'invalid target base')
        check(type(capacity) is int and capacity>=0,'invalid capacity')
        if preflight:self.validate()
        # Arena overlap validation scans allocated object intervals; counted separately from the collector kernel.
        for p,fs in list(self.old.items())+list(self.young.items()):
            self.preflight_words+=1
            check(to_base+capacity<=p or p+8*(1+len(fs))<=to_base,'target arena overlaps current heap')
        for o,i in self.remembered:check(o in self.old and type(i) is int and 0<=i<len(self.old[o]),'invalid remembered slot')
        mapping={}; target={}; work=deque(); cursor=to_base; events=[] if self.events is not None else None; ops=0
        def forward(p):
            nonlocal cursor,ops
            ops+=1
            if p is None or p in self.old:return p
            check(p in self.young,'invalid young pointer')
            if p in mapping:return mapping[p]
            size=8*(1+len(self.young[p])); check(cursor+size<=to_base+capacity,'minor target capacity exhausted')
            q=cursor; cursor+=size; mapping[p]=q; target[q]=list(self.young[p]); work.append(q)
            if events is not None:events.append(('copy',p,q,size))
            ops+=size//8; return q
        roots={s:forward(v) for s,v in self.roots.items()}; patches={}
        for o,i in self.remembered:patches[o,i]=forward(self.old[o][i])
        while work:
            q=work.popleft()
            target[q]=[forward(v) for v in target[q]]
        new_m={s for s,v in patches.items() if v in target}
        # Commit only after successful traversal; original heap/roots/metadata survive ModelError above.
        for (o,i),v in patches.items():self.old[o][i]=v
        self.roots=roots; self.young=target; self.remembered=new_m; self.core_operations+=ops
        if self.events is not None:self.events.extend(events)
        return {'mapping':mapping,'live_bytes':cursor-to_base,'kernel_operations':ops,'preflight_words_total':self.preflight_words}


def expect_error(fn):
    try: fn()
    except ModelError:return True
    raise ModelError('expected rejection did not occur')

def run_checks(trace=False):
    front=frontend(trace=trace); check(front['result']==(7,(7,100)),'frontend endpoint')
    for text in ['let x=x in x','(let x=1 in x,x)']:
        expect_error(lambda text=text:Resolver().resolve(Parser(lex(text)[0]).parse()))
    tiny=lex('let letx=10==2;',[Rule('LET','let'),Rule('ID','','id'),Rule('INT','','int'),Rule('EQEQ','=='),Rule('EQ','='),Rule('SEMI',';'),Rule('WS','','space',True)])[0]
    check([t[0] for t in tiny]==['LET','ID','EQ','INT','EQEQ','INT','SEMI','EOF'],'maximal munch fixture')
    backtrack=[]
    for n in range(1,9):
        ts,c=lex('a'*n,[Rule('A','a'),Rule('LONG','','astar_b')]); check(c['accepted_characters']==n*(n+1)//2,'backtrack cost'); backtrack.append((n,c['accepted_characters']))
    for src,want in [('let x=4 in let f=fun y -> x+y in let x=x+1 in f(x)',9),('let x=ref 4 in let f=fun d -> (x:=!x+d;!x) in (f(1),f(2))',(5,7)),('()',None)]:
        check(frontend(src,trace)['result']==want,'frontend transfer')
    need,cost=needs({'f':set(),'g':{'x'},'h':set()},{'f':['g'],'g':['h'],'h':['f']})
    check(all(v=={'x'} for v in need.values()),'lifting closure'); check(lift_run('h',3,7,need)[0]==1 and lift_run('h',2,7,need)[0]==7,'lifting execution')
    tail=tail_sum(3,trace); check(tail['value']==6,'tail endpoint'); check(tail_sum(10000)['value']==50005000,'long tail chain'); swap=[('a',lambda old:old['b']),('b',lambda old:old['a'])]; correct_swap=parallel_assign({'a':2,'b':9},swap); wrong_swap=sequential_assign_wrong({'a':2,'b':9},swap); check(correct_swap=={'a':9,'b':2} and wrong_swap=={'a':9,'b':9},'parallel move execution')
    objects=object_fixture(); original=copy.deepcopy(objects); linked=link(objects,{'text':0x1000,'data':0x2000}); check(objects==original,'link mutates input')
    check([p['value'] for p in linked['patches']]==[12,0x200c,-20],'relocation values')
    targets=[call_target(linked['image'],0x1000),call_target(linked['image'],0x1010)]; check(targets==[0x1010,0x1000],'ISA call target')
    shifted=link(objects,{'text':0x4000,'data':0x5000}); check([p['value'] for p in shifted['patches']]==[12,0x500c,-20],'uniform rebase')
    bad=copy.deepcopy(objects); bad[0]['relocations'][0]['addend']=0; wrong=link(bad,{'text':0x1000,'data':0x2000}); check(call_target(wrong['image'],0x1000)==0x1012,'wrong addend witness')
    bad=copy.deepcopy(objects); bad[1]['sections']['text']['align']=0x10000; snap=copy.deepcopy(bad); expect_error(lambda:link(bad,{'text':0x1000,'data':0x2000})); check(bad==snap,'failed link mutates input')
    rc=ReferenceCounter(['r','t'],trace); rc.alloc('r','P',2); rc.alloc('t','C'); rc.replace(('P',0),'C'); rc.replace(('P',1),'C'); rc.validate(); check(rc.rc=={'P':1,'C':3},'parallel RC slots')
    rc.replace('r',None); check(rc.rc['C']==3,'queued parent still owns outgoing slots'); rc.drain(); rc.validate(); check(rc.rc=={'C':1},'RC shared release')
    rc.replace('t','C'); rc.validate(); rc.replace('t',None); rc.drain(); rc.validate(); check(not rc.heap,'RC acyclic completion')
    cycle=ReferenceCounter(['r','tmp'],trace); cycle.alloc('r','X',1); cycle.alloc('tmp','Y',1); cycle.replace(('X',0),'Y'); cycle.replace(('Y',0),'X'); cycle.replace('tmp',None); cycle.replace('r',None); cycle.drain(); cycle.validate(); check(cycle.rc=={'X':1,'Y':1},'RC cycle retention'); check(not reachable(cycle.roots.values(),cycle.heap),'cycle unreachable')
    limited=ReferenceCounter(['r','s'],max_count=1); limited.alloc('r','C'); expect_error(lambda:limited.replace('s','C')); limited.validate(); check(limited.roots['s'] is None,'RC overflow atomicity')
    gc=GenerationalHeap({800:[None]},{104:[120],120:[None],136:[None]},{'r':800},trace=trace); gc.write(800,0,104); gc_result=gc.minor(200,48); check(gc_result['mapping']=={104:200,120:216},'minor reachability'); check(gc.old[800]==[200] and gc.remembered=={(800,0)},'remembered slot update')
    gc.validate(); gc.write(800,0,None); gc_second=gc.minor(304,48); check(not gc.young and not gc.remembered,'stale remembered cleanup')
    missing=GenerationalHeap({800:[None]},{104:[120],120:[None],136:[None]},{'r':800}); missing.write(800,0,104,barrier=False); missing.minor(200,48); expect_error(missing.validate)
    small=GenerationalHeap({800:[104]},{104:[120],120:[None]},{'r':800},{(800,0)}); before=copy.deepcopy((small.old,small.young,small.roots,small.remembered)); expect_error(lambda:small.minor(200,16)); check(before==(small.old,small.young,small.roots,small.remembered),'minor failure atomicity')
    promoted=GenerationalHeap({800:[104]},{104:[120],120:[None]},{'r':800},{(800,0)}); promoted.promote(104); check((104,0) in promoted.remembered,'promotion barrier'); promoted.minor(200,16); check(promoted.old[104][0]==200,'promoted field relocation')
    return {'status':'passed','frontend':front,'backtracking':backtrack,'lifting':{'need':{k:sorted(v) for k,v in need.items()},'cost':cost},'tail':tail,'link':{k:v for k,v in linked.items() if k!='image'},'call_targets':targets,'rc':{'final_heap':rc.heap,'cycle_counts':cycle.rc,'operations':rc.core_operations,'validation_slots':rc.validation_slots,'events':rc.events},'minor':gc_result,'minor_second':gc_second,'negative_tests':['scope leak','nonrecursive self-reference','wrong PC addend','relocation overflow atomicity','RC count overflow atomicity','missing write barrier','minor capacity failure atomicity']}

def main():
    p=argparse.ArgumentParser(description=__doc__); p.add_argument('--trace',action='store_true'); p.add_argument('--out',type=Path); args=p.parse_args()
    report=run_checks(args.trace); encoded=json.dumps(report,ensure_ascii=False,indent=2)
    if args.out:args.out.write_text(encoded+'\n')
    print(json.dumps({'status':report['status'],'result':report['frontend']['result'],'pages':8,'trace':args.trace,'json_characters':len(encoded),'note':'Python AST/environment copies and preflight validations are reported separately; these bounded tests are not general proofs.'},ensure_ascii=False))
if __name__=='__main__':main()