"""Observed applied transition; EXPERIMENTAL, no atomic generation claim. WHY: an accepted layout request can precede the transaction applying it. CONTRACT: keep the old state, then require two coherent standard observations. INVARIANT: no first-row discard, last-row shortcut or pending-as-applied proof. PI_POPUP has no owner field: uniqueness + exact live XDG hierarchy + IPC ancestry provide bounded correlation only. The actual private output.c reads current. """ import json import re from model import require from predicates import protocol from ipc_predicates import ancestry,nodes SOURCE_FILES = { 'output.c': '/home/fy59/swayfx-mosaic-static-runtime-hm5kbdkt/mosaic-source/sway/desktop/output.c', 'transaction.c': '/home/fy59/swayfx-mosaic-static-runtime-hm5kbdkt/mosaic-source/sway/desktop/transaction.c', 'xdg_shell.c': '/home/fy59/swayfx-mosaic-static-runtime-hm5kbdkt/mosaic-source/sway/desktop/xdg_shell.c', } def fields(line): return dict(re.findall(r'(\w+)=([^\s]+)', line)) def observed_epochs(text, output, start_ns, end_ns): """Group the exact commit callback's ordered SCENE/OWNER/POPUP records. Other output callbacks may contain the same global popup tree. We examine all callbacks for the selected output and never filter by desired owner. """ epochs=[]; active=None; last=0 for line in text.splitlines(): if not re.search(r'\bPI_(?:OUTPUT_COMMIT|SCENE|OWNER|POPUP)\b',line):continue f=fields(line) if f.get('output')!=output:continue ns=int(f['ns']) if not start_ns<=ns<=end_ns:continue require(ns>last,'trace-monotonic-order');last=ns if 'PI_OUTPUT_COMMIT ' in line: active={'commit':f,'scene':None,'owners':[],'roots':[],'raw':[line]};epochs.append(active) else: require(active is not None,'trace-without-commit') active['raw'].append(line) if 'PI_SCENE ' in line: require(active['scene'] is None,'duplicate-scene');active['scene']=f elif 'PI_OWNER ' in line:active['owners'].append(f) else:active['roots'].append(f) require(bool(epochs),'applied-observations-missing') return epochs def transition_window_start(trace,output,root_id,owner_id,workspace_id,mapped_after_ns,request_ns): """Select an explicitly coherent mapped A/B Mosaic callback before request. Earlier no-popup callbacks belong to opening evidence, not the transition. We require a complete commit header + current scene + owner + unique root; no unconditional trace-row deletion is allowed. """ epochs=observed_epochs(trace,output,0,request_ns) candidates=[] for epoch in epochs: c,s,roots=epoch['commit'],epoch['scene'],epoch['roots'] if int(c['ns'])bounds[1],'standard-before-request-application') require(s['clip_valid']==r['clip_valid']=='0' and s['clip']==r['clip']=='0,0,0,0' and s['tile_scene']=='0,0','standard-clips-absent') state='applied-standard';standard.append(epoch) else:require(False,'unexpected-applied-layout') states.append({'ns':t,'state':state,'owner':o,'scene':s,'root':r,'commit':c}) require(states[0]['state']=='old-applied-Mosaic' and states[0]['ns']<=ipc_response['ns'], 'old-applied-mosaic-required') require(len(standard)>=2,'two-standard-observations-required') # Coherent stabilization retains actual owner geometry and root identity. stable=[{k:e['owners'][next(i for i,o in enumerate(e['owners']) if o['id']==str(owner_id))][k] for k in ('scene','applied_size','current')} for e in standard] require(all(v==stable[0] for v in stable),'standard-geometry-not-stabilized') first_ns=int(standard[0]['roots'][0]['ns']) require(isinstance(captures,list) and len(captures)==2 and {c.get('output') for c in captures}=={'HEADLESS-1','HEADLESS-2'},'two-standard-captures') for capture in captures: require(capture.get('exit')==0 and type(capture.get('start_ns')) is int and first_nsfirst_ns and snapshot['ns']<=end,'snapshot-applied-epoch') return dict(status='PASS',states=states,request_bounds=bounds,ipc_reply_ns=ipc_response['ns'], first_standard_ns=first_ns,stabilized_ns=int(standard[-1]['roots'][0]['ns']), owner=owner_id,root=root_id,workspace=workspace_id,output=output,ids=prot['ids'], captures=captures,source_contract=source_contract, limitation='bounded unique-root correlation; independent observations, not atomic transaction generation') EXPECTED_SOURCE = {'output.c':'b517c07655c6796a74fba731ab42d0f96ef53e104f6a9a4c0af256f26a25ded1', 'transaction.c':'b04483d05100f57867560289d2a7db346e3e8925cec9fa4be35b23b1f6928165', 'xdg_shell.c':'2a57ba553cacd82220bf16459debb167a3db5889c172af28d9067951f2df3610'} def source_bindings(): from support import sha observed={name:sha(path) for name,path in SOURCE_FILES.items()} require(observed==EXPECTED_SOURCE,'private-source-bytes-changed') return observed def validate_applied_standard_transition(*args,**kwargs): """Malformed/omitted evidence is Invalid/INCONCLUSIVE, never accepted.""" from model import Invalid try:return _validate_applied_standard_transition(*args,**kwargs) except Invalid:raise except (KeyError,IndexError,TypeError,ValueError,AttributeError,AssertionError) as exc: raise Invalid('malformed-transition-evidence:'+str(exc)) from exc