603 lines
43 KiB
Python
603 lines
43 KiB
Python
#!/usr/bin/env python3
|
|
"""Read-only P08-03 evidence gate. Integrity success is never unit acceptance."""
|
|
import argparse
|
|
import hashlib
|
|
import importlib.util
|
|
import json
|
|
import math
|
|
import os
|
|
from pathlib import Path
|
|
import re
|
|
import sys
|
|
import struct
|
|
import zlib
|
|
import subprocess
|
|
import copy
|
|
|
|
sys.dont_write_bytecode = True
|
|
HERE = Path(__file__).resolve().parent
|
|
SPEC = 'docs/spec/acceptance/P08-03.json'
|
|
SPEC_SHA = '7941da4edbd3c43a636a4a3d834d57c095b56da988fa3a056e55b22d3a5d50e9'
|
|
CONTRACT = 'docs/plans/original-completion-2026-10-02/execution/completion_marker_contracts.json'
|
|
TEST = 'tests/ui/test_p08_normal_placement_ops.gd'
|
|
RECORDER = 'docs/plans/original-completion-2026-10-02/execution/p08-03/passive_os_placement_recorder.gd'
|
|
CONDITIONS = ['support_connection', 'invalid_position_reason', 'demolish_rebuild',
|
|
'pan_zoom_world_identity', 'separate_pid_resume']
|
|
MEMBERS = ['world.bin', 'manifest.json', 'thumbnail.png', 'journal.log']
|
|
WRITER = ['unsupported', 'out_of_bounds', 'supported_connected', 'overlap',
|
|
'missing_connection', 'lower_stair', 'upper_stair', 'refused_demolition',
|
|
'cancel_demolition', 'demolition', 'rebuild', 'pan_zoom']
|
|
RUNTIME_KEYS = set(('runtime_schema_version weather world_seed next_command_id '
|
|
'staffing_projection_enabled save_lifecycle command_queue id_generator domain_events rng_streams '
|
|
'world path movement_credits mana economy facility_upkeep upkeep_settlement inventory kitchen_production '
|
|
'auto_purchase_plans elevators legacy_stairs logistics_dispatcher logistics_requests facilities '
|
|
'facility_cleanliness guests staff catalog_manifest progression hired_staff_candidate_ids operations '
|
|
'relationships event_definitions events authority defense construction excavation spatial_subslots '
|
|
'route_projection facility_infrastructure').split())
|
|
REASONS = {'unsupported': ('UNSUPPORTED', '配置不可: 構造を支えられません'),
|
|
'out_of_bounds': ('OUT_OF_BOUNDS', '配置不可: 世界の範囲外です'),
|
|
'overlap': ('OVERLAP', '配置不可: ほかの施設または工事と重なります'),
|
|
'resume_overlap': ('OVERLAP', '配置不可: ほかの施設または工事と重なります')}
|
|
|
|
def module(name, path):
|
|
spec = importlib.util.spec_from_file_location(name, path)
|
|
obj = importlib.util.module_from_spec(spec)
|
|
spec.loader.exec_module(obj)
|
|
return obj
|
|
|
|
prior = module('p08_placement_typed_codec', HERE/'check_p08_migration_evidence.py')
|
|
runner = module('p08_placement_source_inventory', HERE/'run_all_tests.py')
|
|
decode = prior.decode
|
|
typed_differences = prior.typed_differences
|
|
def sha(path): return hashlib.sha256(Path(path).read_bytes()).hexdigest()
|
|
def load(path): return json.loads(Path(path).read_bytes())
|
|
def require(ok, message):
|
|
if not ok: raise ValueError(message)
|
|
|
|
def scalar(value, kind=None):
|
|
kind = kind or ('bool' if isinstance(value, bool) else 'int' if isinstance(value, int) else 'String')
|
|
return {'type':kind, 'text':('&' if kind == 'StringName' else '')+json.dumps(value, ensure_ascii=False)}
|
|
|
|
def dictionary(entries, key_type='String'):
|
|
return {'type':'Dictionary', 'entries':[[scalar(k, key_type), v] for k,v in entries.items()]}
|
|
|
|
def typed_member(node, *path):
|
|
for key in path:
|
|
matches = [v for k,v in node['entries'] if decode(k) == key]
|
|
require(len(matches) == 1, 'missing/duplicate typed model member '+repr(path))
|
|
node = matches[0]
|
|
return node
|
|
|
|
def expected_operation(formal, result, event_type):
|
|
"""Rebuild the full typed state from source rules, never from the actual delta.
|
|
|
|
Runtime 4680-4720, StableIdGenerator.next_id, SimulationDomainEvent.to_dictionary
|
|
and DomainEventStream.publish/create_snapshot define this single notification.
|
|
"""
|
|
saved = decode(formal)
|
|
minute = saved['clock']['absolute_minute']
|
|
values = {'ok':bool(result.get('ok',False)), 'code':str(result.get('code','UNKNOWN')),
|
|
'message':str(result.get('message','')), 'operation':str(result.get('operation','unknown')),
|
|
'save_path':str(result.get('save_path',result.get('path',''))), 'reason':str(result.get('reason','')),
|
|
'request_id':int(result.get('request_id',0)),
|
|
'checkpoint_absolute_minute':int(result.get('checkpoint_absolute_minute',minute)),
|
|
'duration_us':int(result.get('duration_us',0)), 'runtime_duration_us':int(result.get('runtime_duration_us',0))}
|
|
names = {'code','operation','reason','selected_candidate_id','selected_candidate_kind'}
|
|
if isinstance(result.get('selected'),dict):
|
|
selected = result['selected']
|
|
values.update(selected_candidate_id=str(selected.get('id','')),
|
|
selected_candidate_kind=str(selected.get('kind','')), selected_generation=int(selected.get('generation',-1)))
|
|
if isinstance(result.get('manifest'),dict):
|
|
manifest = result['manifest']
|
|
values.update(save_id=str(manifest.get('save_id','')), saved_absolute_minute=int(manifest.get('absolute_minute',-1)))
|
|
expected = copy.deepcopy(formal)
|
|
runtime = typed_member(expected,'systems','runtime')
|
|
counters = typed_member(runtime,'id_generator','counters')
|
|
count = decode(counters).get('domain_event',0)+1
|
|
require(0 < count <= 999999999999, 'invalid domain event counter')
|
|
for key,value in counters['entries']:
|
|
if decode(key) == 'domain_event':
|
|
value.update(scalar(count)); break
|
|
else:
|
|
counters['entries'].append([scalar('domain_event'),scalar(count)])
|
|
event_id = 'domain_event.%012d' % count
|
|
stream = typed_member(runtime,'domain_events')
|
|
published = typed_member(stream,'published_ids')
|
|
require(event_id not in decode(published), 'duplicate operation notification')
|
|
published['items'].append(scalar(event_id))
|
|
published['items'].sort(key=decode)
|
|
payload = dictionary({k:scalar(v,'StringName' if k in names else None) for k,v in values.items()},'StringName')
|
|
event = dictionary({'event_id':scalar(event_id), 'event_type':scalar(event_type),
|
|
'absolute_minute':scalar(minute), 'source_service':scalar('save_service'),
|
|
'entity_ids':{'type':'Array','element_type':4,'element_class':'','items':[]},
|
|
'payload':payload, 'causation_command_id':scalar(0)})
|
|
recent = typed_member(stream,'recent_events')
|
|
recent['items'].append(event)
|
|
recent['items'] = recent['items'][-256:]
|
|
return expected
|
|
|
|
def png(data):
|
|
require(data.startswith(b'\x89PNG\r\n\x1a\n'), 'missing OS screenshot')
|
|
offset = 8; chunks = []; payload = b''
|
|
while offset < len(data):
|
|
require(offset+12 <= len(data), 'invalid OS screenshot')
|
|
size = int.from_bytes(data[offset:offset+4], 'big')
|
|
kind = data[offset+4:offset+8]; body = data[offset+8:offset+8+size]
|
|
require(offset+12+size <= len(data), 'invalid OS screenshot')
|
|
crc = int.from_bytes(data[offset+8+size:offset+12+size], 'big')
|
|
require(zlib.crc32(kind+body) == crc, 'invalid OS screenshot CRC')
|
|
if kind == b'IHDR':
|
|
require(len(body) == 13 and all(v > 0 for v in struct.unpack('>II',body[:8])), 'invalid OS screenshot dimensions')
|
|
if kind == b'IDAT': payload += body
|
|
chunks.append(kind); offset += size+12
|
|
require(chunks and chunks[0] == b'IHDR' and chunks[-1] == b'IEND' and payload, 'invalid OS screenshot chunks')
|
|
try:
|
|
require(bool(zlib.decompress(payload)), 'empty OS screenshot')
|
|
except zlib.error as exc:
|
|
raise ValueError('invalid OS screenshot pixels') from exc
|
|
|
|
def input_map(root):
|
|
names = [SPEC, CONTRACT, 'AGENTS.md', RECORDER, RECORDER+'.uid',
|
|
'docs/plans/original-completion-2026-10-02/IMPLEMENTATION_PLAN.md',
|
|
'docs/traceability/original/BASELINE.txt']
|
|
names += [p.relative_to(root).as_posix() for p in (root/'tests/fixtures/p08-03').rglob('*')
|
|
if p.is_file() and '__pycache__' not in p.parts and '.scratch' not in p.parts]
|
|
return {name: sha(root/name) for name in sorted(names)}
|
|
|
|
def keyed(rows, key):
|
|
result = {r[key]: r for r in rows}
|
|
require(len(result) == len(rows), 'duplicate '+key)
|
|
return result
|
|
|
|
def state(node):
|
|
snap = decode(node)
|
|
require(set(snap) == {'schema_version', 'clock', 'game_state', 'systems'}, 'missing whole snapshot envelope')
|
|
r = snap['systems']['runtime']
|
|
require(set(r) == RUNTIME_KEYS, 'missing whole Runtime members')
|
|
facilities = keyed(r['construction']['facilities'], 'instance_id')
|
|
jobs = keyed(r['construction']['jobs'], 'job_id')
|
|
for job in jobs.values():
|
|
if job['state'] == 'COMPLETED':
|
|
require(job['facility_instance_id'] in facilities, 'orphan completed job')
|
|
owners = {k: v['occupied_cells'] for k, v in facilities.items()}
|
|
owners.update({k: v['reserved_cells'] for k, v in jobs.items() if v['state'] not in ('COMPLETED', 'CANCELLED')})
|
|
occupancy = keyed(r['world']['occupancies'], 'entity_id')
|
|
require(set(owners) == set(occupancy), 'orphan/lost occupancy')
|
|
seen = set()
|
|
for key, cells in owners.items():
|
|
actual = {tuple(c) for c in occupancy[key]['cells']}
|
|
require(actual == {tuple(c) for c in cells} and len(actual) == len(cells), 'partial occupancy')
|
|
require(not seen.intersection(actual), 'overlapping occupancy')
|
|
seen.update(actual)
|
|
operational = keyed(r['facilities']['instances'], 'instance_id')
|
|
require(set(operational) == set(facilities), 'partial demolition/completion')
|
|
for key, row in operational.items():
|
|
require(row['occupied_cells'] == facilities[key]['occupied_cells'], 'operational cells drift')
|
|
return snap
|
|
|
|
def coordinates(p):
|
|
cell = p['world_cell']
|
|
require(cell == p['selected_cell'] and len(cell) == 3, 'world-cell drift')
|
|
bounds, origin, dimensions = p['bounds'], p['map_position'], p['cell_dimensions']
|
|
require(len(dimensions) == 2 and all(math.isfinite(v) and v > 0 for v in dimensions), 'invalid cell dimensions')
|
|
wanted = [origin[0] + (cell[0]-bounds['min_x']+0.5)*dimensions[0],
|
|
origin[1] + (bounds['max_y']-cell[1]+0.5)*dimensions[1]]
|
|
require(all(math.isfinite(v) for v in p['viewport']+p['local']), 'nonfinite viewport')
|
|
require(all(abs(a-b) < 0.001 for a, b in zip(p['local'], wanted)), 'converted cell pixel mismatch')
|
|
require(0.5 <= p['zoom'] <= 4.0, 'zoom bounds')
|
|
for target in ('viewport','screen'):
|
|
if target == 'screen' and target not in p: continue
|
|
matrix = p[target+'_transform']
|
|
require(len(matrix) == 6 and all(math.isfinite(v) for v in matrix), 'invalid viewport transform')
|
|
x, y = p['local']
|
|
expected = [matrix[0]*x+matrix[2]*y+matrix[4], matrix[1]*x+matrix[3]*y+matrix[5]]
|
|
require(len(p[target]) == 2 and all(abs(a-b) < 0.001 for a,b in zip(expected,p[target])), 'transformed '+target+' mismatch')
|
|
|
|
def preserve(a, b, results):
|
|
differences = typed_differences(a, b)
|
|
if not results:
|
|
require(not differences, 'cancel/preview partially applied')
|
|
return
|
|
# Keep every typed field. Only the command envelope may grow on a refusal.
|
|
allowed = [('systems', 'runtime', key) for key in
|
|
('command_queue', 'next_command_id', 'domain_events', 'id_generator')]
|
|
require(all(any(p[:3] == prefix for prefix in allowed) for p in differences), 'refusal partially applied')
|
|
old, new = [decode(n)['systems']['runtime'] for n in (a, b)]
|
|
require(new['next_command_id'] == old['next_command_id'] + len(results), 'refusal command sequence')
|
|
oq, nq = old['command_queue'], new['command_queue']
|
|
require(nq['processed'] == oq['processed'] + results, 'refusal result/journal mismatch')
|
|
for key in ('pending', 'in_flight'):
|
|
require(nq[key] == oq[key], 'refusal queue loss')
|
|
|
|
def action_gate(row, typed):
|
|
coordinates(row['position'])
|
|
before, after = typed(row['before']), typed(row['after'])
|
|
a, b = state(before), state(after)
|
|
require(row['position']['bounds'] == a['systems']['runtime']['world']['bounds'], 'invented world bounds')
|
|
kind, label = row['kind'], row['id']
|
|
expected_kind = 'camera' if label == 'pan_zoom' else 'cancel' if label == 'cancel_demolition' else 'demolish' if label in ('demolition','refused_demolition') else 'build'
|
|
require(kind == expected_kind, 'operation kind mismatch')
|
|
expected_reason = REASONS[label][0] if label in REASONS else {'missing_connection':'STAIR_LANDING_MISSING', 'refused_demolition':'STAIR_LANDING_IN_USE'}.get(label, '')
|
|
require(row.get('expected', expected_reason) == expected_reason, 'required refusal reason changed')
|
|
results = row.get('results', [])
|
|
if label in REASONS:
|
|
code, message = REASONS[label]
|
|
require(row['report']['error_codes'][0] == code and row['status'] == message, 'reason mismatch')
|
|
require(not row['report']['can_build'] and not results, 'preview rejection bypassed')
|
|
preserve(before, after, results)
|
|
elif kind == 'cancel':
|
|
require(not results and row['status'] == '撤去を取り消しました。', 'cancel submitted command')
|
|
preserve(before, after, results)
|
|
elif kind == 'camera':
|
|
preserve(before, after, [])
|
|
require(row['pan_before'] != row['pan_after'], 'move-mode wheel did not pan')
|
|
require(row['ctrl_pressed'] is False and row['steps'] == [max(0.5, row['steps'][0]-0.5*i) for i in range(9)] + [min(4.0, 1.0+0.5*i) for i in range(9)], 'wheel clamp sequence')
|
|
require(row['steps'][8] == 0.5 and row['steps'][-1] == 4.0, 'missing clamp boundaries')
|
|
require(row['original_local'] != row['position']['local'], 'fixed pixels substituted for world identity')
|
|
else:
|
|
require(len(results) == 1, 'one real Runtime result required')
|
|
result = results[0]
|
|
processed = b['systems']['runtime']['command_queue']['processed']
|
|
require(result in processed, 'result absent from actual model')
|
|
if row['expected']:
|
|
require(result['code'] == 'VALIDATION_FAILED' and result['details']['reason'] == row['expected'], 'reason mismatch')
|
|
preserve(before, after, results)
|
|
else:
|
|
require(result['code'] == 'OK', 'positive rejected')
|
|
if kind == 'demolish':
|
|
require(row['status'] == '%s | %s | %s' % (result['code'], result['details'].get('reason', ''), result['message']), 'displayed domain reason mismatch')
|
|
if not row['expected']:
|
|
fid = row['instance_id']
|
|
old = keyed(a['systems']['runtime']['construction']['facilities'], 'instance_id')
|
|
new = keyed(b['systems']['runtime']['construction']['facilities'], 'instance_id')
|
|
require(fid in old and fid not in new and set(new) == set(old)-{fid}, 'partial demolition')
|
|
require(row['position']['world_cell'] in old[fid]['occupied_cells'], 'demolition wrong cell')
|
|
refund = result['details']['refund']
|
|
resources_a, resources_b = a['game_state']['resources'], b['game_state']['resources']
|
|
require(set(resources_a) == set(resources_b) and all(resources_b[k] == v + refund.get(k, 0) for k, v in resources_a.items()), 'demolition refund mismatch')
|
|
if kind == 'build' and not row['expected']:
|
|
completed = state(typed(row['completed']))
|
|
facilities = completed['systems']['runtime']['construction']['facilities']
|
|
require(any(f['definition_id'] == row['definition'] and f['origin'] == row['position']['world_cell'] for f in facilities), 'construction completion missing')
|
|
require(row['report']['can_build'], 'positive support invalid')
|
|
cost = row['report']['total_cost']
|
|
resources_a, resources_b = a['game_state']['resources'], b['game_state']['resources']
|
|
require(set(resources_a) == set(resources_b) and all(resources_b[k] == v - cost.get(k, 0) for k, v in resources_a.items()), 'build cost mismatch')
|
|
if label == 'supported_connected':
|
|
require(row['report']['connection']['status'] == 'CONNECTED', 'positive connection absent')
|
|
if label == 'missing_connection':
|
|
require(row['status'] == '操作に失敗しました: '+result['message'], 'connection reason mismatch')
|
|
require(row['report']['can_build'], 'connection refusal did not reach Runtime')
|
|
|
|
def check(project_root, evidence_dir):
|
|
root, evidence = Path(project_root).resolve(), Path(evidence_dir).resolve()
|
|
try:
|
|
index = load(evidence/'index.json')
|
|
require(index['schema'] == 'p08-normal-placement-v1' and index['acceptance'] == 'pending', 'schema/acceptance')
|
|
require(index['collection_error'] is None, 'collection failed')
|
|
require(index['conditions'] == CONDITIONS, 'missing condition')
|
|
actual = {n: v['sha256'] for n, v in runner.source_refs(root).items()}
|
|
require(index['source_map'] == actual, 'stale source')
|
|
require(index['inputs'] == input_map(root), 'stale input')
|
|
require(index['spec_sha256'] == SPEC_SHA == hashlib.sha256((root/SPEC).read_text().strip().encode()).hexdigest(), 'immutable spec')
|
|
require(index['marker_contract_sha256'] == sha(root/CONTRACT), 'stale marker')
|
|
require(re.fullmatch('[0-9a-f]{40}', index['commit']) is not None, 'commit')
|
|
require(index['commit'] == subprocess.check_output(['git','-C',str(root),'rev-parse','HEAD'],text=True).strip(), 'stale commit')
|
|
def artifact(name):
|
|
require(isinstance(name, str) and name and not Path(name).is_absolute() and '..' not in Path(name).parts, 'unsafe/missing artifact')
|
|
p = evidence/name
|
|
require(not p.is_symlink() and p.resolve().is_relative_to(evidence), 'artifact escape')
|
|
pin = index['artifacts'][name]
|
|
require(p.stat().st_size == pin['bytes'] and sha(p) == pin['sha256'], 'artifact hash '+name)
|
|
return p
|
|
def document(name): return load(artifact(name))
|
|
for name in index['artifacts']: artifact(name)
|
|
run = document('runner-input.json')
|
|
require(run['selected_source_map'] == actual and run['commit'] == index['commit'], 'runner source')
|
|
require(sha(run['engine']) == run['engine_sha256'], 'engine hash')
|
|
ended = document('runner-ended.json')
|
|
require(ended['error'] is None and not ended['cleanup_errors'], 'outer failure')
|
|
markers = module('p08_placement_markers', HERE/'strict_test_markers.py')
|
|
contracts = markers.load_contracts(root/CONTRACT)
|
|
pids = set()
|
|
def phase(name):
|
|
receipt = document(name)
|
|
pid = receipt['actual_pid']
|
|
require(type(pid) is int and pid > 0 and pid not in pids, 'missing/duplicate actual PID')
|
|
pids.add(pid)
|
|
require('--headless' in receipt['command'] and '--script' in receipt['command']
|
|
and '--path' in receipt['command'], 'handler command contract')
|
|
prefix = str(Path(name).parent)+'/'
|
|
folder = prefix+receipt['phase']+'/'
|
|
start, end, outer = [document(folder+n) for n in ('started.json', 'ended.json', 'outer-owned-finally.json')]
|
|
require(all(v['actual_pid'] == pid and v['command'] == receipt['command'] for v in (start, end)), 'raw lifecycle identity')
|
|
require(start.get('live_identity_exact') is True or start.get('tracked_child_ended_before_initial_probe') is True, 'unobserved native PID')
|
|
require(end['engine_ended'] is True and end['exit_code'] == 0, 'unended PID')
|
|
require(outer['actual_captured_pids'] == [pid] and outer['all_captured_ended'] is True and not outer['outer_cleanup_errors'] and outer['foreign_process_or_group_signals'] == 0, 'owned cleanup')
|
|
native = receipt['native_process']
|
|
require(native['exit_code'] == native['helper_exit_code'] == 0 and native['timed_out'] is False and native['lifecycle_error'] is None, 'native failure')
|
|
require(receipt['exit_code'] == 0 and receipt['engine_ended'] is True and not receipt['failed'], 'phase failure')
|
|
profile = receipt['actual_private_profile']['report']
|
|
require(profile['fresh_before_parent_initialize'] is True and profile['profile_writes_before_guard'] == 0 and profile['actual_user_data_dir'] == profile['expected_user_data_dir'], 'profile guard')
|
|
require(receipt['test'] == TEST and receipt['source_sha256'] == actual[TEST], 'executed suite source')
|
|
require(not markers.parse_raw(TEST, artifact(prefix+receipt['log']).read_text(), contracts, actual[TEST])['errors'], 'strict completion')
|
|
return pid
|
|
def os_phase(name):
|
|
end = document(name)
|
|
prefix = str(Path(name).parent)+'/'
|
|
start = document(prefix+'started.json')
|
|
spawned = document(prefix+'process-started.json')
|
|
pid = end['actual_pid']
|
|
require(type(pid) is int and pid > 0 and pid not in pids, 'missing/duplicate actual PID')
|
|
pids.add(pid)
|
|
command = end['command']
|
|
require(command == [run['engine'], '--path', end['stage'], '--script', command[-1]], 'OS native argv')
|
|
require('--headless' not in command and len(command) == 5, 'OS headless masquerade')
|
|
require(spawned['actual_pid'] == pid and spawned['command'] == command and spawned['monotonic_ns'] > 0,
|
|
'OS raw process identity')
|
|
for doc in (start, spawned, end):
|
|
require(doc['protocol'] == 'p08-placement-native-os-v1' and doc['source_map'] == actual
|
|
and doc['commit'] == index['commit'], 'OS exact source/commit')
|
|
require(doc['controller_sha256'] == actual['tools/run_p08_normal_placement.py']
|
|
and doc['recorder_sha256'] == sha(root/RECORDER), 'OS controller/recorder SHA')
|
|
require(doc['command'] == command and doc['engine_sha256'] == run['engine_sha256'], 'OS command/engine drift')
|
|
require(sha(artifact(prefix+'passive_os.gd')) == sha(root/RECORDER), 'executed OS recorder SHA')
|
|
require(end['error'] is None and not end['guard_errors'] and not end['cleanup_errors']
|
|
and end['exit_code'] == 0 and end['engine_ended'] is True and end['passed'] is True, 'OS native failure')
|
|
cleanup = end['owned_cleanup']
|
|
require(len(cleanup) == 1 and cleanup[0]['pid'] == pid and cleanup[0]['engine_ended'] is True
|
|
and not cleanup[0]['outer_cleanup_errors'] and cleanup[0]['foreign_process_or_group_signals'] == 0,
|
|
'OS owned cleanup')
|
|
require(end['stage_before'] == end['stage_after'] and end['default_before'] == end['default_after'], 'OS protected state changed')
|
|
require({n:v['sha256'] for n,v in end['source_after'].items()} == actual, 'OS source changed')
|
|
require(end['profile_before'] == {'existed':False,'files':{}}, 'OS profile not fresh')
|
|
owners = module('p08_verify_os_owners', HERE/'regression/ordinary_proof_gate.py')
|
|
actual_owner_proof = owners.ordinary_gate(evidence/prefix/'teardown', pid, evidence/prefix, ['single'])
|
|
require(end['ordinary_owner_proof'] == actual_owner_proof, 'OS ordinary owner proof mismatch')
|
|
profile = document('os-pair/'+end['role']+'-profile.json')
|
|
require(profile['pid'] == pid and Path(profile['user_data_dir']).resolve() == Path(end['profile']).resolve()
|
|
and profile['display'] != 'headless', 'OS actual profile/display')
|
|
raw = artifact(prefix+'engine-native.log').read_text()
|
|
require('ERROR:' not in raw and re.findall(r'(?m)^P08 passive OS placement: ([0-9]+) checks, 0 failures$', raw)
|
|
and 'P08 normal placement:' not in raw, 'OS raw diagnostics/completion')
|
|
members = end['formal_input']
|
|
require(set(members) == set(MEMBERS), 'OS missing formal input')
|
|
source_dir = 'pair/initial-formal' if end['role'] == 'writer' else 'os-pair/formal'
|
|
for member, pin in members.items():
|
|
source = artifact(source_dir+'/'+member)
|
|
require(pin == {'bytes':source.stat().st_size,'sha256':sha(source)}, 'OS formal input SHA')
|
|
return pid
|
|
case = index['cases'][0]
|
|
require(len(index['cases']) == 1 and len(case['phases']) == 2, 'writer/reader pair')
|
|
pair_pids = [phase(n) for n in case['phases']]
|
|
def pair_gate(directory, expected_pids, native_os=False):
|
|
def typed(name):
|
|
artifact(directory+'/'+name+'.var')
|
|
return document(directory+'/'+name+'.json')
|
|
rows = []
|
|
normal_results = {}
|
|
inspections = {}
|
|
bootstrap_inspection = None
|
|
bootstrap_result = None
|
|
for role, pid in zip(('writer', 'reader'), expected_pids):
|
|
process = document(directory+'/'+role+'-process.json')
|
|
require(process['pid'] == pid and process['failures'] == 0 and process['checks'] > 0, 'process attribution')
|
|
require(bool(process['engine']['hash']) and bool(process['engine']['string']), 'engine version')
|
|
save_log = document(directory+'/'+role+'-save-results.json')
|
|
require(save_log['pid'] == pid and save_log['records'], 'missing actual save results')
|
|
operations = []
|
|
for stem in save_log['records']:
|
|
record = document(directory+'/'+stem+'.json')
|
|
raw = artifact(directory+'/'+stem+'.var')
|
|
require(record['pid'] == pid and record['raw_sha256'] == sha(raw), 'save result attribution/SHA')
|
|
path = record['requested_path']
|
|
require(path.startswith('user://') and record['absolute_path'] == str(Path(record['user_data_dir'])/path[7:]), 'save outside private user profile')
|
|
result = decode(record['result'])
|
|
require(isinstance(result, dict) and result.get('ok') is True, 'actual save/load failed')
|
|
if native_os and role == "writer" and record["operation"] == "initial_inspect":
|
|
require(result.get("read_only") is True and "snapshot" in result, "missing bootstrap inspection")
|
|
bootstrap_inspection = typed_member(record["result"],"snapshot")
|
|
if record['operation'] == 'runtime_operation':
|
|
if native_os and role == "writer" and bootstrap_result is None:
|
|
bootstrap_result = record["result"]
|
|
operations.append(result.get('operation'))
|
|
normal_results[role] = result
|
|
if record['operation'] == 'formal_inspect':
|
|
require(result.get('read_only') is True and 'snapshot' in result, 'missing read-only formal model')
|
|
inspections[role] = typed_member(record['result'],'snapshot')
|
|
require(('save' in operations) if role == 'writer' else any(op in ('load','recovery','recovery_candidate') for op in operations), 'missing actual normal save/load result')
|
|
doc = document(directory+'/'+role+'-actions.json')
|
|
require(doc['setup'] == 'diagnostic', 'unlabelled diagnostic')
|
|
expected = WRITER if role == 'writer' else ['resume_overlap']
|
|
require([r['id'] for r in doc['actions']] == expected, 'missing operations')
|
|
if role == 'writer':
|
|
budget = doc['budget']
|
|
require(budget['setup'] == 'diagnostic', 'budget setup')
|
|
costs = {'reception': root/'data/facilities/reception.tres', 'guest_stairs': root/'data/facilities/infrastructure/guest_stairs.tres'}
|
|
total = {'gold': 0, 'materials': 0}
|
|
require([r['definition'] for r in budget['costs']] == ['reception', 'reception', 'guest_stairs', 'guest_stairs'], 'diagnostic build roster')
|
|
for entry in budget['costs']:
|
|
text = costs[entry['definition']].read_text()
|
|
line = re.search(r'^construction_cost = (.+)$', text, re.M).group(1)
|
|
original = {k: int(v) for k, v in re.findall(r'&"([^"]+)":\s*(\d+)', line)}
|
|
require(entry['cost'] == original, 'invented diagnostic cost')
|
|
for k in total: total[k] += original.get(k, 0)
|
|
delta = {k: v-budget['initial'][k] for k, v in total.items() if v > budget['initial'][k]}
|
|
require(total == budget['needed'] and delta == budget['deltas'], 'diagnostic budget mismatch')
|
|
for row in doc['actions']:
|
|
require(row['input_method'] == ('native_os' if native_os else 'handler'), 'fake OS provenance')
|
|
action_gate(row, typed)
|
|
if row['kind'] == 'build':
|
|
wanted_definition = 'standard_room' if row['id'] == 'unsupported' else 'guest_stairs' if row['id'] in ('missing_connection','lower_stair','upper_stair') else 'reception'
|
|
require(row['definition'] == wanted_definition, 'diagnostic definition substituted')
|
|
if not row.get('expected', REASONS.get(row['id'], ('',))[0]):
|
|
path = root/('data/facilities/infrastructure/' if wanted_definition == 'guest_stairs' else 'data/facilities/')/(wanted_definition+'.tres')
|
|
text = path.read_text()
|
|
line = re.search(r'^construction_cost = (.+)$',text,re.M).group(1)
|
|
cost = {k:int(v) for k,v in re.findall(r'&"([^"]+)":\s*(\d+)',line)}
|
|
require(row['report']['total_cost'] == cost, 'invented production cost')
|
|
width,height = map(int,re.search(r'^footprint = Vector2i\((\d+), (\d+)\)$',text,re.M).groups())
|
|
x,y,z = row['position']['world_cell']
|
|
cells = {(x+dx,y+dy,z) for dx in range(width) for dy in range(height)}
|
|
completed = state(typed(row['completed']))['systems']['runtime']['construction']['facilities']
|
|
matches = [f for f in completed if f['origin'] == [x,y,z] and f['definition_id'] == wanted_definition]
|
|
require(len(matches) == 1 and {tuple(c) for c in matches[0]['occupied_cells']} == cells, 'production footprint mismatch')
|
|
rows += doc['actions']
|
|
checkpoint = typed('writer-checkpoint')
|
|
state(checkpoint)
|
|
formal = typed('writer-formal-model')
|
|
require(not typed_differences(typed('writer-presave'),formal), 'wrong presave formal model')
|
|
require(sha(artifact(directory+'/writer-presave.var')) == sha(artifact(directory+'/writer-formal-model.var')), 'wrong raw presave formal model')
|
|
require(not typed_differences(formal,typed('reader-formal-model')), 'wrong formal resume model')
|
|
require(sha(artifact(directory+'/writer-formal-model.var')) == sha(artifact(directory+'/reader-formal-model.var')), 'wrong raw formal resume model')
|
|
for role in ('writer','reader'):
|
|
require(role in inspections and not typed_differences(formal,inspections[role]), 'wrong read-only formal model')
|
|
result = normal_results[role]
|
|
require(result['operation'] == ('save' if role == 'writer' else 'recovery'), 'wrong operation notification kind')
|
|
event_type = 'SAVE_CHECKPOINT_SUCCEEDED' if role == 'writer' else 'SAVE_RECOVERY_LOADED'
|
|
expected = expected_operation(formal,result,event_type)
|
|
differences = typed_differences(expected,typed(role+'-checkpoint'))
|
|
require(not differences, 'wrong resume model: source-defined operation drift '+role+' '+repr(differences))
|
|
require(not typed_differences(expected,typed(role+'-expected-operation')), 'wrong reconstructed operation model')
|
|
require(sha(artifact(directory+'/'+role+'-expected-operation.var')) == sha(artifact(directory+'/'+role+'-checkpoint.var')), 'wrong raw operation model')
|
|
require(not typed_differences(typed(role+'-checkpoint'),typed(role+'-operation-actual')), 'inspection changed live model')
|
|
require(sha(artifact(directory+'/'+role+'-operation-actual.var')) == sha(artifact(directory+'/'+role+'-checkpoint.var')), 'wrong raw inspection preservation')
|
|
comparison = document(directory+'/'+role+'-operation-comparison.json')
|
|
require(comparison == {'pid':expected_pids[0 if role == 'writer' else 1],
|
|
'delta_kind':'source_defined_notification','formal_model':role+'-formal-model',
|
|
'actual_model':role+'-checkpoint','expected_model':role+'-expected-operation',
|
|
'returned_result':comparison['returned_result'],
|
|
'saved_recent_count':len(decode(formal)['systems']['runtime']['domain_events']['recent_events']),
|
|
'expected_recent_count':len(decode(expected)['systems']['runtime']['domain_events']['recent_events']),
|
|
'actual_recent_count':len(decode(typed(role+'-checkpoint'))['systems']['runtime']['domain_events']['recent_events']),
|
|
'whole_raw_equal':True} and decode(comparison['returned_result']) == result, 'wrong operation comparison attribution')
|
|
if native_os:
|
|
prefix = "writer-bootstrap-"
|
|
bootstrap_formal = typed(prefix+"formal-model")
|
|
returned = typed(prefix+"returned-result")
|
|
require(bootstrap_inspection is not None and not typed_differences(bootstrap_formal,bootstrap_inspection), "wrong bootstrap formal inspection")
|
|
require(bootstrap_result is not None and not typed_differences(returned,bootstrap_result), "wrong bootstrap returned Dictionary")
|
|
result = decode(returned)
|
|
require(result.get("ok") is True and result.get("operation") == "recovery", "wrong bootstrap load result")
|
|
expected = expected_operation(bootstrap_formal,result,"SAVE_RECOVERY_LOADED")
|
|
actual = typed(prefix+"checkpoint")
|
|
require(not typed_differences(expected,actual), "bootstrap source-defined operation drift")
|
|
require(not typed_differences(expected,typed(prefix+"expected-operation")), "wrong bootstrap expected model")
|
|
require(not typed_differences(actual,typed(prefix+"operation-actual")), "bootstrap inspection drift")
|
|
for label in ("expected-operation","operation-actual"):
|
|
require(sha(artifact(directory+"/"+prefix+label+".var")) == sha(artifact(directory+"/"+prefix+"checkpoint.var")), "wrong bootstrap raw model")
|
|
comparison = document(directory+"/"+prefix+"operation-comparison.json")
|
|
require(comparison == {
|
|
"pid":expected_pids[0], "delta_kind":"source_defined_notification",
|
|
"formal_model":prefix+"formal-model", "actual_model":prefix+"checkpoint",
|
|
"expected_model":prefix+"expected-operation", "returned_result":returned,
|
|
"saved_recent_count":len(decode(bootstrap_formal)["systems"]["runtime"]["domain_events"]["recent_events"]),
|
|
"expected_recent_count":len(decode(expected)["systems"]["runtime"]["domain_events"]["recent_events"]),
|
|
"actual_recent_count":len(decode(actual)["systems"]["runtime"]["domain_events"]["recent_events"]),
|
|
"whole_raw_equal":True}, "wrong bootstrap comparison attribution")
|
|
saved = document(directory+'/save.json')
|
|
require(set(saved['members']) == set(MEMBERS) and saved['pid'] == expected_pids[0], 'missing formal members/writer')
|
|
for member in MEMBERS:
|
|
require(saved['members'][member] == sha(artifact(directory+'/formal/'+member)), 'formal member changed')
|
|
exported = document(directory+'/formal-export.json')
|
|
require(exported['pid'] == expected_pids[0] and exported['requested_path'] == 'user://saves/manual_ui', 'formal export attribution')
|
|
absolute = str(Path(exported['user_data_dir'])/'saves/manual_ui')
|
|
require(exported['absolute_path'] == absolute, 'save outside private user profile')
|
|
for name in ('formal','formal.bak'):
|
|
package = exported['packages'][name]
|
|
require(package['present'] and package['source_path'] == absolute+('.bak' if name.endswith('.bak') else '') and set(package['members']) == set(MEMBERS), 'missing formal backup export')
|
|
for member, pin in package['members'].items():
|
|
file = artifact(directory+'/'+name+'/'+member)
|
|
require(pin == {'sha256':sha(file),'bytes':file.stat().st_size}, 'formal export SHA')
|
|
metadata = exported['slot_metadata']
|
|
require(metadata['file'] == 'formal-slot-metadata.json' and metadata['sha256'] == sha(artifact(directory+'/'+metadata['file'])) == saved['members']['manifest.json'], 'slot metadata SHA')
|
|
if not native_os:
|
|
initial = document(directory+'/initial-formal-export.json')
|
|
initial_absolute = str(Path(initial['user_data_dir'])/'saves/p08_initial')
|
|
require(initial['pid'] == expected_pids[0] and initial['requested_path'] == 'user://saves/p08_initial' and initial['absolute_path'] == initial_absolute, 'initial formal private path')
|
|
package = initial['packages']['initial-formal']
|
|
require(package['present'] and package['source_path'] == initial_absolute and set(package['members']) == set(MEMBERS), 'initial formal members')
|
|
for member, pin in package['members'].items():
|
|
file = artifact(directory+'/initial-formal/'+member)
|
|
require(pin == {'sha256':sha(file),'bytes':file.stat().st_size}, 'initial formal SHA')
|
|
require(initial['packages']['initial-formal.bak'] == {'present':False,'source_path':initial_absolute+'.bak','members':{}}, 'unexpected initial backup')
|
|
metadata = initial['slot_metadata']
|
|
require(metadata['file'] == 'initial-formal-slot-metadata.json' and metadata['sha256'] == sha(artifact(directory+'/'+metadata['file'])) == package['members']['manifest.json']['sha256'], 'initial slot metadata SHA')
|
|
facilities = keyed(decode(checkpoint)['systems']['runtime']['construction']['facilities'], 'instance_id')
|
|
require(saved['instance_id'] in facilities and facilities[saved['instance_id']]['origin'] == saved['cell'], 'wrong resume instance')
|
|
by_id = {r['id']: r for r in rows}
|
|
require(all(by_id[n]['position']['world_cell'] == saved['cell'] for n in ('supported_connected', 'demolition', 'rebuild', 'pan_zoom', 'resume_overlap')), 'target world-cell drift')
|
|
require(by_id['demolition']['instance_id'] != saved['instance_id'], 'rebuild did not create new instance')
|
|
return rows
|
|
pair_gate(case['directory'], pair_pids)
|
|
os_proof = document(index['os_proof'])
|
|
require(os_proof['source_map'] == actual and os_proof['inputs'] == index['inputs'], 'stale OS source/input')
|
|
require(os_proof['input_method'] == 'native_os' and os_proof['observer_mutations'] == [], 'fake OS provenance')
|
|
os_pids = [os_phase(n) for n in os_proof['phases']]
|
|
require(len(os_pids) == 2, 'OS separate PID pair')
|
|
os_rows = pair_gate(os_proof['directory'], os_pids, True)
|
|
lifecycle = []
|
|
for role, pid in zip(('writer','reader'),os_pids):
|
|
requests = document('os-pair/'+role+'-requests.json')
|
|
require(requests['pid'] == pid, 'OS lifecycle PID')
|
|
actions = [document(str(Path(name).parent)+'/request.json') for name in requests['requests']]
|
|
require(any(a['action'] == 'load_menu' for a in actions), 'missing OS normal load')
|
|
if role == 'writer':
|
|
require(any(a['action'] == 'button' and a.get('node','').endswith('/ManualSaveButton') for a in actions), 'missing OS normal save')
|
|
lifecycle.append({'id':role+'-lifecycle', 'requests':requests['requests']})
|
|
all_ack = {name for name in index['artifacts'] if name.startswith('os-pair/') and name.endswith('/ack.json')}
|
|
require(all_ack == {name for row in lifecycle for name in row['requests']}, 'omitted OS lifecycle requests')
|
|
require(all(set(row['requests']) <= all_ack for row in os_rows), 'OS action request missing')
|
|
os_rows += lifecycle
|
|
for row in os_rows:
|
|
requests = row['requests']
|
|
require(requests and len(requests) == len(set(requests)), 'missing/duplicate OS requests')
|
|
expected_pid = os_pids[1 if row['id'] in ('resume_overlap','reader-lifecycle') else 0]
|
|
wheel_requests = []
|
|
for name in requests:
|
|
ack = document(name)
|
|
folder = str(Path(name).parent)+'/'
|
|
request = document(folder+'request.json')
|
|
observed = document(folder+'observed.json')
|
|
require(ack['target_pid'] == request['target_pid'] == observed['pid'] == expected_pid
|
|
and ack['sequence'] == request['sequence'] == observed['sequence'], 'fake OS provenance')
|
|
require(ack['request_sha256'] == sha(artifact(folder+'request.json')), 'OS ack request mismatch')
|
|
raw = document(ack['input_receipt'])
|
|
require(raw['method'] == 'native_os' and raw['target_pid'] == expected_pid and raw['timestamp_ns'] > 0
|
|
and raw['tool_name'] and raw['tool_call_id'], 'fake OS provenance')
|
|
require(raw['events'] and observed['events'], 'missing OS events')
|
|
require(raw['collector_pid'] > 0 and raw['collector_pid'] not in os_pids, 'fake OS collector')
|
|
for key in ('screen_before', 'screen_after'):
|
|
png(artifact(ack[key]).read_bytes())
|
|
if request['action'] == 'cell' and 'position' in row:
|
|
require(request['world_cell'] == row['position']['world_cell']
|
|
and request['viewport'] == row['position']['viewport']
|
|
and request['screen'] == row['position']['screen'], 'OS transformed cell drift')
|
|
if request['action'] == 'wheel':
|
|
wheel_requests.append(request)
|
|
if row['id'] == 'pan_zoom':
|
|
require(any(e['move_mode'] and not e['ctrl'] for e in wheel_requests), 'missing OS pan')
|
|
require(sum(not e['move_mode'] and not e['ctrl'] for e in wheel_requests) == 18, 'missing OS zoom')
|
|
# Full regression remains a separately verified Root requirement; this
|
|
# finite gate cannot replace the standard runner or independent review.
|
|
return []
|
|
except (KeyError, ValueError, TypeError, OSError, IndexError, AttributeError, AssertionError, subprocess.SubprocessError) as exc:
|
|
return [str(exc)]
|
|
|
|
def main(argv=None):
|
|
parser = argparse.ArgumentParser(description=__doc__)
|
|
parser.add_argument('--verify-only', action='store_true', required=True)
|
|
parser.add_argument('--project-root', type=Path, default=HERE.parent)
|
|
args = parser.parse_args(argv)
|
|
build = os.environ.get('BUILD_OUTPUT_DIR')
|
|
if not build:
|
|
print('BUILD_OUTPUT_DIR is required', file=sys.stderr)
|
|
return 2
|
|
deficits = check(args.project_root, Path(build)/'p08-normal-placement-evidence')
|
|
print(json.dumps({'task_id': 'P08-03', 'integrity': 'fail' if deficits else 'pass',
|
|
'deficits': deficits, 'acceptance': 'pending'}, ensure_ascii=False))
|
|
return 1 if deficits else 0
|
|
|
|
if __name__ == '__main__':
|
|
raise SystemExit(main())
|