#!/usr/bin/env python3
"""OS-16 teaching-model checks. Python 3 standard library only; no host OS claims.
Run: python foundations-os16-check.py
Output: deterministic JSON; assertions fail loudly. All addresses are integers.
"""
from dataclasses import dataclass, replace
from collections import Counter
from copy import deepcopy
from itertools import product
import json
checks=0
def ck(condition, message):
    global checks
    checks+=1
    assert condition, message
@dataclass
class PTE:
    frame:int
    read:bool=True
    write:bool=True
    execute:bool=False
    cow:bool=False
class OS:
    def __init__(self):
        self.maps={'P':{0x10:PTE(0x40,write=False,execute=True),0x12:PTE(0x30)},'Q':{0x12:PTE(0x50)}}
        self.regions={'P':{0x10:'RX',0x12:'RW',0x13:'RW'},'Q':{0x12:'RW'}}
        self.frames={f:bytearray(256) for f in [0x30,0x40,0x50]}
        self.frames[0x30][0xab]=7;self.frames[0x30][0xf0:0xf2]=b'XY';self.frames[0x50][0xab]=9
        self.free=[0x60,0x61,0x62];self.refs=Counter(p.frame for m in self.maps.values() for p in m.values())
        self.tlb={};self.copies=0;self.cow_faults=0;self.faults=[];self.trace=[]
    def inv(self):
        observed=Counter(p.frame for m in self.maps.values() for p in m.values())
        ck(+self.refs==observed,'map references differ from PTEs')
        ck(len(set(self.free))==len(self.free),'duplicate free frame')
        ck(not(set(self.free)&set(observed)),'free mapped frame')
        for m in self.maps.values():
            ck(len([p.frame for p in m.values()])==len(set(p.frame for p in m.values())),'private intra-process aliases excluded')
            for p in m.values():
                ck(not(p.write and self.refs[p.frame]>1),'writable shared private frame')
        for (pid,vpn),cached in self.tlb.items():
            ck(pid in self.maps and self.maps[pid].get(vpn)==cached,'stale TLB')
    def invalidate(self,pid,vpn=None):
        self.tlb={k:v for k,v in self.tlb.items() if not(k[0]==pid and(vpn is None or k[1]==vpn))}
    def alloc(self):
        if not self.free:raise MemoryError('no free data frame')
        f=self.free.pop(0);self.frames[f]=bytearray(256);self.refs[f]=0;return f
    def drop(self,f):
        self.refs[f]-=1
        if self.refs[f]==0:self.frames.pop(f);self.free.insert(0,f)
    def access(self,pid,va,op,value=None):
        ck(0<=va<65536,'address width')
        vpn,offset=divmod(va,256);mode=self.regions.get(pid,{}).get(vpn)
        if mode is None or op not in mode:
            self.faults.append('permission' if mode else 'unmapped');raise PermissionError('region denies access')
        if vpn not in self.maps[pid]:
            self.faults.append('legal-demand');f=self.alloc();self.maps[pid][vpn]=PTE(f);self.refs[f]=1;self.invalidate(pid,vpn)
        p=self.maps[pid][vpn]
        if op=='W' and not p.write:
            ck(p.cow,'non-COW protection failure')
            self.cow_faults+=1
            if self.refs[p.frame]>1:
                new=self.alloc() # failure before any mapping/ref mutation
                self.frames[new][:]=self.frames[p.frame]
                old=p.frame
                self.maps[pid][vpn]=PTE(new);self.refs[new]=1
                self.invalidate(pid,vpn);self.drop(old);self.copies+=1
            else:
                self.maps[pid][vpn]=replace(p,write=True,cow=False);self.invalidate(pid,vpn)
            p=self.maps[pid][vpn]
        hit=(pid,vpn) in self.tlb
        if not hit:
            if len(self.tlb)>=4:self.tlb.pop(next(iter(self.tlb)))
            self.tlb[(pid,vpn)]=replace(p)
        p=self.tlb[(pid,vpn)]
        if op=='W':self.frames[p.frame][offset]=value
        result=self.frames[p.frame][offset]
        self.inv();self.trace.append({'process':pid,'va':hex(va),'op':op,'pa':hex(p.frame*256+offset),'value':result,'tlb_hit':hit})
        return result
    def fork(self,src,dst):
        self.maps[dst]={};self.regions[dst]=dict(self.regions[src])
        for vpn,p in list(self.maps[src].items()):
            q=replace(p,write=False,cow=True) if p.write or p.cow else replace(p)
            self.maps[src][vpn]=q;self.maps[dst][vpn]=replace(q);self.refs[p.frame]+=1
        self.invalidate(src);self.invalidate(dst);self.inv()
    def unmap(self,pid,vpn):
        p=self.maps[pid].pop(vpn);self.invalidate(pid,vpn);self.drop(p.frame);self.regions[pid].pop(vpn,None);self.inv()
    def exit(self,pid):
        for vpn in list(self.maps[pid]):self.unmap(pid,vpn)
        del self.maps[pid];del self.regions[pid];self.invalidate(pid);self.inv()
# Physical page walk with distinct root and leaf addresses.
roots={'P':0x100,'Q':0x300}; root_links={0x110:0x02,0x310:0x04}; leaves={0x220:0x30,0x420:0x50}
walk=[]
for pid in ['P','Q']:
    va=0x12ab;i1=(va>>12)&15;i0=(va>>8)&15;off=va&255
    ra=roots[pid]+16*i1;la=256*root_links[ra]+16*i0;pa=256*leaves[la]+off
    walk.append({'process':pid,'root_pte':hex(ra),'leaf_pte':hex(la),'pa':hex(pa)})
ck([x['pa'] for x in walk]==['0x30ab','0x50ab'],'walk addresses')
ck(17*256>256*16,'dense multilevel has extra root cost')
o=OS();ck(o.access('P',0x12ab,'R')==7,'P read');ck(o.access('Q',0x12ab,'R')==9,'Q read')
o.access('P',0x1305,'W',1);ck(sum(o.frames[0x60])==1,'zero before first publication')
before=deepcopy((o.maps,o.refs,o.free,o.frames))
try:o.access('P',0x1000,'W',2);raise AssertionError('write protected code accepted')
except PermissionError:pass
ck((o.maps,o.refs,o.free,o.frames)==before,'permission fault mutated data')
o.fork('P','C');reftrace=[dict(o.refs)]
o.access('C',0x12ab,'W',8);reftrace.append(dict(o.refs));ck(o.access('P',0x12ab,'R')==7,'C changed parent')
o.access('P',0x12ab,'W',11);reftrace.append(dict(o.refs));ck(o.access('C',0x12ab,'R')==8,'P changed child')
o.unmap('C',0x13);reftrace.append(dict(o.refs))
ck(o.copies==1 and o.cow_faults==2,'COW copy/fault totals')
fail=OS();fail.fork('P','C');fail.free=[];snap=deepcopy((fail.maps,fail.refs,fail.frames))
try:fail.access('C',0x12ab,'W',8);raise AssertionError('allocation unexpectedly succeeded')
except MemoryError:pass
ck((fail.maps,fail.refs,fail.frames)==snap,'failed COW changed old state')
copyout=OS();copyout.fork('P','C');copyout.access('C',0x12ab,'W',8) # kernel helper deliberately shares checked path
ck(copyout.access('P',0x12ab,'R')==7,'copyout isolation')
# Broken path: retained writable translation bypasses the fault.
bug=OS();bug.access('P',0x12ab,'R');old=deepcopy(bug.tlb[('P',0x12)]);bug.fork('P','C');bug.tlb[('P',0x12)]=old
bug.frames[old.frame][0xab]=11
ck(bug.frames[bug.maps['C'][0x12].frame][0xab]==11,'expected stale writable TLB counterexample')
# OFD graph; names and fds are separate dictionaries.
file=bytearray(b'abcdefgh');fds={'P':{3:'O7'}};ofd={'O7':{'offset':0,'refs':1}};fdtrace=[]
def fd_inv():
    counts=Counter(v for table in fds.values() for v in table.values())
    ck(counts==Counter({k:v['refs'] for k,v in ofd.items()}),'OFD references')
def rd(pid,fd,n):
    ob=ofd[fds[pid][fd]];b=bytes(file[ob['offset']:ob['offset']+n]);ob['offset']+=len(b);fd_inv();return b.decode()
def wr(pid,fd,b):
    ob=ofd[fds[pid][fd]];start=ob['offset'];file[start:start+len(b)]=b;ob['offset']+=len(b);fd_inv();return len(b)
def close(pid,fd):
    k=fds[pid].pop(fd);ofd[k]['refs']-=1
    if ofd[k]['refs']==0:del ofd[k]
    fd_inv();fdtrace.append(deepcopy(ofd))
fds['P'][4]='O7';ofd['O7']['refs']+=1;fds['C']=dict(fds['P']);ofd['O7']['refs']+=2;fd_inv()
received=rd('C',3,2);ck(received=='ab','shared read prefix')
for i,ch in enumerate(received):o.access('C',0x1280+i,'W',ord(ch))
user_buffer=bytes([o.access('P',0x12f0+i,'R') for i in range(2)])
ck(wr('P',4,user_buffer)==2,'write count');ck(ofd['O7']['offset']==4,'shared offset')
fds['C'][5]='O8';ofd['O8']={'offset':0,'refs':1};received=rd('C',5,3);ck(received=='abX','independent open read')
for i,ch in enumerate(received):o.access('C',0x1282+i,'W',ord(ch))
ck(ofd['O7']['offset']==4 and ofd['O8']['offset']==3,'independent offsets')
fd_stage_content=file.decode();ofd_offsets={k:v['offset'] for k,v in ofd.items()}
# D is inserted before P closes fd4: pwrite-style explicit offset does not move O7.
file[0]=ord('Z');ck(ofd['O7']['offset']==4,'pwrite leaves shared offset unchanged')
for pid,fd in [('P',3),('C',4),('C',3),('P',4)]:close(pid,fd)
ck('O7' not in ofd and ofd['O8']['refs']==1,'OFD lifetime')
close('C',5);o.exit('P');reftrace.append(dict(o.refs));o.exit('C');reftrace.append(dict(o.refs));ck(+o.refs==Counter({0x50:1}),'only Q survives')
# Clock trace: h does not move on hit.
slots=['a','b','c'];bits=[1,1,1];h=0;scans=[]
def replace_clock(new):
    global h
    count=0
    while True:
        count+=1
        if bits[h]==0:
            victim=slots[h];slots[h]=new;bits[h]=1;h=(h+1)%3;scans.append(count);return victim
        bits[h]=0;h=(h+1)%3
ck(replace_clock('d')=='a','first Clock victim');bits[slots.index('b')]=1
ck(replace_clock('e')=='c','second Clock victim');ck(scans==[4,2] and h==0,'Clock scans')
# Block mapping and holes.
def block_lookup(q,size,d,ind):
    if not 0<=q<size:return 'EOF'
    j,off=divmod(q,256)
    if j>=130:raise OverflowError
    block=d[j] if j<2 else (ind[j-2] if ind else 0)
    return (block,off) if block else 'ZERO'
ck(block_lookup(600,800,[20,21],[30,31])==(30,88),'indirect offset')
ck(block_lookup(799,800,[20,21],[30,31])==(31,31),'last byte')
ck(block_lookup(800,800,[20,21],[30,31])=='EOF','file length guard')
ck(block_lookup(600,800,[20,21],None)=='ZERO','absent indirect is a hole')
# Redirty and completion/durability are independent.
g,c,w,s=1,0,1,0;g=2;c=w;w=None;ck(g>c,'redirty must remain dirty');w=g;c=w;w=None;ck(c==g and s==0,'clean can still be volatile');s=g;ck(s==2,'flush latest')
ck(0<=1<=1 and 0<=0<=1,'stable may precede completion: g=1,s=1,c=0')
# Exhaust all completed subsets at protocol stages. Stable writes are atomic blocks.
old=(0,0,0,0);new=(1,1,1,1)
subsets=list(product([False,True],repeat=4))
def overlay(a,b,mask):return tuple(y if flag else x for x,y,flag in zip(a,b,mask))
def recovery(home,payload,commit):return payload if commit else home
cases=[]
for mask in subsets:cases.append(('payload',old,overlay(old,new,mask),False))
for commit in [False,True]:cases.append(('commit',old,new,commit))
for mask in subsets:cases.append(('home',overlay(old,new,mask),new,True))
for commit in [False,True]:cases.append(('clear',new,new,commit))
recovery_crashes=0
for phase,home,payload,commit in cases:
    result=recovery(home,payload,commit)
    ck(result in [old,new], 'journal mixed recovery')
    if commit:ck(result==new,'committed transaction lost')
    if commit:
        for mask in subsets:
            partial=overlay(home,payload,mask)
            ck(recovery(partial,payload,True)==new,'repeat recovery after crash')
            recovery_crashes+=1
mutants={'no_payload_barrier':recovery(old,(1,0,0,0),True),'no_home_barrier':recovery((1,0,0,0),new,False),'reuse_before_durable_clear':recovery(new,(2,1,1,1),True)}
for name,result in mutants.items():ck(len(set(result))>1,'mutant lacks counterexample '+name)
# Application write-all handles short writes and detects no progress.
def write_all(data,returns):
    offset=0;pieces=[]
    for n in returns:
        if n<=0 or n>len(data)-offset:raise RuntimeError('error or no progress')
        pieces.append(data[offset:offset+n]);offset+=n
        if offset==len(data):return pieces
    raise RuntimeError('incomplete output')
ck(write_all('abcdef',[2,1,3])==['ab','c','def'],'partial writes advance pointer')
try:write_all('abcdef',[2,0]);raise AssertionError('zero write should stop')
except RuntimeError:pass
result={'model':'OS-16, 256-byte pages/blocks, single core, explicit flush and atomic stable blocks','checks':checks,'page_walk':walk,'faults':o.faults,'cow':{'copies':o.copies,'bytes_copied':o.copies*256,'write_faults':o.cow_faults,'ref_trace':[{hex(k):v for k,v in r.items()} for r in reftrace],'only_survivor':{hex(k):v for k,v in (+o.refs).items()}},'fd':{'file_after_C':fd_stage_content,'file_after_D':file.decode(),'O8_offset_before_close':ofd_offsets['O8'],'close_trace':fdtrace},'clock':{'scans':scans,'final_slots':slots,'accessed':bits,'hand':h},'journal':{'crash_cases':len(cases),'recovery_crash_cases':recovery_crashes,'negative_witnesses':mutants},'scope':'Deterministic teaching-model arithmetic, lifecycle assertions and finite crash subsets. Not a real kernel, device, browser or power-cut test.'}
print(json.dumps(result,ensure_ascii=False,indent=2))