"""Prospective equal-child nonleaf fullscreen handler; applied evidence is sampled.""" import re,time import cases,validators from engine import COLORS from geometry import * from ipc_predicates import ancestry from model import Provenance from PIL import Image,ImageChops,ImageDraw from predicates import geometry def group_candidate(state,peer_id,group_id=None,fullscreen=True): path=ancestry(state['snapshot']['tree'],state['owner']['id']) if fullscreen: group=validators.fullscreen_ancestor(path) need(group['type']=='con' and group.get('fullscreen_mode')==1 and len(group['nodes'])==2,'exact nonleaf fullscreen group') else: rows=[n for n in path[:-1] if n.get('type')=='con' and n.get('id')==group_id] need(len(rows)==1,'current two-child group absent after fullscreen exit');group=rows[0] need(group.get('fullscreen_mode',0)==0 and len(group.get('nodes',[]))==2,'group still fullscreen or child count changed') need(group_id is None or group['id']==group_id,'fullscreen group identity changed') need({n['id'] for n in group['nodes']}=={state['owner']['id'],peer_id},'fullscreen exact owner/peer children') need(group.get('layout')=='splith','fullscreen group split orientation') rect=group['rect'];out=next(o for o in state['snapshot']['outputs'] if o['name']==state['workspace']['output'])['rect'] if fullscreen:need(rect==out,'fullscreen group does not cover output') else:need(rect==out,'current split group does not cover output after fullscreen exit') widths=[n['rect']['width'] for n in group['nodes']] need(widths[0]==widths[1] and sum(widths)==rect['width'],'fullscreen equal child widths') return group def comparable(pristine,core): # WHY/CONTRACT/INVARIANT: compare actual roles, configures and geometry # measured for these binaries; matching requested placement is insufficient. for r in (pristine,core): need(r['fresh'] and r['crossing_A'] and r['crossing_B'] and crossing(r['popup_A'],0,0) and crossing(r['popup_B'],0,0),'stale/noncrossing fullscreen evidence') keys=('client_sha256','roles','top_configure','child_rects','group_rect','popup_A','popup_B','configured_A','configured_B','origin','outputs') need(all(pristine[k]==core[k] for k in keys),'noncomparable pristine/core fullscreen evidence') return dict(status='PARTIALLY_FEASIBLE',atomic_current_state='NOT_PROVEN') def fresh_geometry(s,state,p): return geometry(s.log('owner'),state['origin'],Provenance(state['owner']['id'],state['workspace']['id'],'NOT OBSERVABLE','fresh native paint + pointer-local corroboration')) def fullscreen_h2_field(images,baseline,g,output,frame,colors,active_roles=('POPUP_A','POPUP_B'),require_crossing=False): # WHY/CONTRACT/INVARIANT: fullscreen standard overflow must reproduce the # complete measured H2 field. P1/C8 are scale-1, normal, logical captures; # configured global rectangles are clipped with half-open output bounds. need(frame=='logical' and output['scale']==1 and output['transform']=='normal','fullscreen H2 frame/scale/transform unsupported') ox,oy,ow,oh=output['logical'];need(baseline.size==(ow,oh) and images[1].size==baseline.size,'fullscreen H2 image dimensions') expected=baseline.copy();draw=ImageDraw.Draw(expected) parent=g['origin'] for key,name in (('A','POPUP_A'),('B','POPUP_B')): configured=g['configured_'+key];rect=g[key] need(len(configured)==len(rect)==4 and configured[2]>0 and configured[3]>0,'fullscreen popup configured extent') need(rect==[parent[0]+configured[0],parent[1]+configured[1],configured[2],configured[3]],'fullscreen popup geometry/configure mismatch') if require_crossing:need(g.get('crossing',{}).get(key) is True,'fullscreen popup crossing not traversed') left=max(rect[0],ox);top=max(rect[1],oy);right=min(rect[0]+rect[2],ox+ow);bottom=min(rect[1]+rect[3],oy+oh) if name in active_roles and left