931 lines
64 KiB
Python
931 lines
64 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)}
|
|
|
|
R09_COMMIT = '31aa7706d28a92e313c432d5a62e35d19503dcc3'
|
|
R09_DOCS = 'docs/plans/original-completion-2026-10-02/execution/p08-03'
|
|
|
|
VALIDATORS = {'tools/check_p08_normal_placement_evidence.py',
|
|
'tools/test_p08_normal_placement_evidence.py'}
|
|
|
|
def r09_allowed(name):
|
|
return name in VALIDATORS or name.startswith(R09_DOCS+'/')
|
|
|
|
def pinned_document(pin):
|
|
path = Path(pin['path'])
|
|
require(path.stat().st_size == pin['bytes'] and sha(path) == pin['sha256'], 'collection pin SHA')
|
|
return load(path)
|
|
|
|
def r09_runner_binding(evidence, index, pins):
|
|
run = load(evidence/'runner-input.json')
|
|
original = pinned_document(pins['runner_input'])
|
|
require(run['engine'] == original['engine'] and run['engine_sha256'] == original['engine_sha256'],
|
|
'R09 engine hash/version drift')
|
|
require(run == original, 'R09 settings/config/environment drift')
|
|
original_index = pinned_document(pins['index'])
|
|
for role in ('writer', 'reader'):
|
|
receipt = load(evidence/('os-runs/'+role+'/ended.json'))
|
|
pinned = pinned_document(pins['OS'][role]['receipt'])
|
|
require(receipt == pinned, 'R09 settings/config/environment drift')
|
|
name = 'os-pair/'+role+'-profile.json'
|
|
require(index['artifacts'][name] == original_index['artifacts'][name]
|
|
and sha(evidence/name) == original_index['artifacts'][name]['sha256'],
|
|
'R09 engine hash/version drift')
|
|
require(run['commit'] == index['commit'] == R09_COMMIT, 'R09 reuse candidate')
|
|
|
|
def r09_applicability(root, index):
|
|
head = subprocess.check_output(['git', '-C', str(root), 'rev-parse', 'HEAD'], text=True).strip()
|
|
require(index['commit'] == R09_COMMIT, 'R09 reuse candidate')
|
|
result = subprocess.run(['git', '-C', str(root), 'merge-base', '--is-ancestor', R09_COMMIT, head],
|
|
capture_output=True)
|
|
require(result.returncode == 0, 'R09_COMMIT not an ancestor')
|
|
diff = subprocess.check_output(['git', '-C', str(root), 'diff', '--name-status',
|
|
'--no-renames', '-z', R09_COMMIT, head]).decode().split('\0')
|
|
require(all(r09_allowed(name) for name in diff[1::2] if name), 'non-whitelisted committed change')
|
|
status = subprocess.check_output(['git', '-C', str(root), 'status', '--porcelain', '-z']).decode().split('\0')
|
|
require(all(len(row) >= 4 and r09_allowed(row[3:]) and 'R' not in row[:2]
|
|
and 'C' not in row[:2] for row in status if row), 'dirty working tree outside whitelist')
|
|
require(input_map(root) == index['inputs'], 'stale reuse input')
|
|
actual = {n:v['sha256'] for n,v in runner.source_refs(root).items()}
|
|
require({n:v for n,v in actual.items() if not r09_allowed(n)} ==
|
|
{n:v for n,v in index['source_map'].items() if not r09_allowed(n)}, 'stale reuse source')
|
|
for name in VALIDATORS:
|
|
baseline = subprocess.check_output(['git', '-C', str(root), 'show', R09_COMMIT+':'+name])
|
|
require(index['source_map'][name] == hashlib.sha256(baseline).hexdigest(), 'reuse source pin')
|
|
pins = load(root/R09_DOCS/'ROOT_NATIVE_R09_COLLECTION_PINS.json')
|
|
original = Path(pins['original_root'])
|
|
pinned = pinned_document(pins['runner_input'])
|
|
current = load(original/'runner-input.json')
|
|
require(current == pinned, 'R09 runner input drift')
|
|
require(pinned['commit'] == index['commit'] and pinned['inputs'] == index['inputs'],
|
|
'R09 runner binding drift')
|
|
require(sha(pinned['engine']) == pinned['engine_sha256'], 'R09 engine hash drift')
|
|
for role in ('writer', 'reader'):
|
|
receipt = pinned_document(pins['OS'][role]['receipt'])
|
|
require(receipt['engine_sha256'] == pinned['engine_sha256'], 'R09 engine hash/version drift')
|
|
require(receipt['environment_sha256'] == hashlib.sha256(
|
|
json.dumps(receipt['environment'], sort_keys=True).encode()).hexdigest(),
|
|
'R09 settings/environment drift')
|
|
return {name:sha(root/name) for name in sorted(VALIDATORS)}
|
|
|
|
def jpeg_dimensions(data):
|
|
"""Structural validation only; positive validity requires original capture hashes."""
|
|
require(data[:2] == b'\xff\xd8' and data[-2:] == b'\xff\xd9', 'invalid JPEG SOI/EOI')
|
|
pos, dimensions, scans = 2, None, 0
|
|
components, quant, huffman = {}, set(), set()
|
|
while pos < len(data):
|
|
require(data[pos] == 255, 'invalid JPEG marker')
|
|
while pos < len(data) and data[pos] == 255: pos += 1
|
|
require(pos < len(data), 'truncated JPEG marker')
|
|
marker = data[pos]; pos += 1
|
|
if marker == 0xd9:
|
|
require(pos == len(data) and dimensions is not None and scans > 0, 'invalid JPEG end')
|
|
return dimensions
|
|
require(marker not in (0, 0xd8, 1) and not 0xd0 <= marker <= 0xd7,
|
|
'invalid JPEG standalone marker')
|
|
require(pos+2 <= len(data), 'truncated JPEG length')
|
|
length = int.from_bytes(data[pos:pos+2], 'big')
|
|
require(length >= 2 and pos+length <= len(data)-2, 'truncated JPEG segment')
|
|
body = data[pos+2:pos+length]; pos += length
|
|
if marker == 0xdb:
|
|
offset = 0
|
|
while offset < len(body):
|
|
info = body[offset]; offset += 1
|
|
require(info >> 4 in (0, 1) and info & 15 <= 3, 'invalid JPEG DQT')
|
|
size = 64 * (1 + (info >> 4))
|
|
require(offset+size <= len(body), 'invalid JPEG DQT')
|
|
quant.add(info & 15); offset += size
|
|
elif marker == 0xc4:
|
|
offset = 0
|
|
while offset < len(body):
|
|
require(offset+17 <= len(body), 'invalid JPEG DHT')
|
|
info = body[offset]; count = sum(body[offset+1:offset+17])
|
|
require(info >> 4 in (0, 1) and info & 15 <= 3 and count > 0
|
|
and offset+17+count <= len(body), 'invalid JPEG DHT')
|
|
huffman.add((info >> 4, info & 15)); offset += 17+count
|
|
elif marker in (0xc0, 0xc2):
|
|
require(dimensions is None and len(body) >= 6 and body[0] == 8
|
|
and body[5] > 0 and len(body) == 6+3*body[5], 'invalid JPEG SOF')
|
|
height, width = struct.unpack('>HH', body[1:5])
|
|
require(width > 0 and height > 0, 'invalid JPEG dimensions')
|
|
components = {body[i]:body[i+2] for i in range(6, len(body), 3)}
|
|
require(len(components) == body[5], 'invalid JPEG SOF components')
|
|
dimensions = (width, height)
|
|
elif 0xc0 <= marker <= 0xcf and marker not in (0xc4, 0xc8, 0xcc):
|
|
raise ValueError('unsupported JPEG SOF')
|
|
elif marker == 0xda:
|
|
require(dimensions is not None and body and body[0] > 0
|
|
and len(body) == 4+2*body[0], 'invalid JPEG SOS')
|
|
ids = [body[i] for i in range(1, 1+2*body[0], 2)]
|
|
require(len(ids) == len(components) and set(ids) == set(components),
|
|
'JPEG SOF/SOS component mismatch')
|
|
require(set(components.values()) <= quant, 'missing JPEG DQT')
|
|
require(bool(huffman), 'missing JPEG DHT')
|
|
for i in range(2, 1+2*body[0], 2):
|
|
table = body[i]
|
|
require((0, table >> 4) in huffman and (1, table & 15) in huffman,
|
|
'JPEG SOS undefined table')
|
|
start, nonempty = pos, False
|
|
while pos < len(data):
|
|
if data[pos] != 255:
|
|
nonempty = True; pos += 1; continue
|
|
require(pos+1 < len(data), 'truncated JPEG scan')
|
|
if data[pos+1] == 0:
|
|
nonempty = True; pos += 2; continue
|
|
if 0xd0 <= data[pos+1] <= 0xd7:
|
|
pos += 2; continue
|
|
break
|
|
require(nonempty and pos > start, 'empty JPEG entropy stream')
|
|
scans += 1
|
|
raise ValueError('missing JPEG EOI')
|
|
|
|
def r09_images(evidence, index, measurement, pins=None):
|
|
require(measurement['original_index_sha256'] == sha(evidence/'index.json'), 'stale image index pin')
|
|
expected = {f'os-pair/{role}-request-{i:04d}/screen-{side}.png'
|
|
for role, count in (('reader', 5), ('writer', 64))
|
|
for i in range(1, count+1) for side in ('before', 'after')}
|
|
rows = keyed(measurement['images'], 'file')
|
|
indexed = {n for n in index['artifacts'] if n.startswith('os-pair/') and n.endswith('.png')
|
|
and n not in ('os-pair/formal/thumbnail.png', 'os-pair/formal.bak/thumbnail.png')}
|
|
require(set(rows) == indexed == expected, 'missing/extra image entry')
|
|
original_index = None
|
|
if pins is not None:
|
|
original_index = pinned_document(pins['index'])
|
|
for role in ('writer', 'reader'):
|
|
pinned_document(pins['OS'][role]['receipt'])
|
|
sizes = {}
|
|
for name in sorted(expected):
|
|
data = (evidence/name).read_bytes()
|
|
sizes[name] = jpeg_dimensions(data)
|
|
row, pin = rows[name], index['artifacts'][name]
|
|
if original_index is not None:
|
|
capture = original_index['artifacts'][name]
|
|
original_bytes = (Path(pins['original_root'])/name).read_bytes()
|
|
require(hashlib.sha256(original_bytes).hexdigest() == capture['sha256']
|
|
and len(original_bytes) == capture['bytes']
|
|
and pin == capture and hashlib.sha256(data).hexdigest() == capture['sha256']
|
|
and len(data) == capture['bytes'], 'original capture hash mismatch')
|
|
require(row['source_sha256'] == capture['sha256'], 'measurement capture hash altered')
|
|
role = name.split('/')[1].split('-')[0]
|
|
ack_name = name.rsplit('/', 1)[0]+'/ack.json'
|
|
ack_path = Path(pins['original_root'])/ack_name
|
|
require(sha(ack_path) == original_index['artifacts'][ack_name]['sha256'],
|
|
'original capture receipt hash mismatch')
|
|
ack = load(ack_path)
|
|
receipt = pinned_document(pins['OS'][role]['receipt'])
|
|
side = 'screen_before' if name.endswith('screen-before.png') else 'screen_after'
|
|
require(ack[side] == name and ack['target_pid'] == receipt['actual_pid'],
|
|
'original capture receipt mismatch')
|
|
require(hashlib.sha256(data).hexdigest() == row['source_sha256'] == pin['sha256']
|
|
and len(data) == pin['bytes'], 'image source_sha256 mismatch')
|
|
require(row['format_by_magic'] == 'JPEG' and type(row['width']) is int
|
|
and type(row['height']) is int and sizes[name] == (row['width'], row['height']),
|
|
'image SOF dimension mismatch')
|
|
for name in expected:
|
|
if name.endswith('screen-before.png'):
|
|
require(sizes[name] == sizes[name.replace('screen-before.png', 'screen-after.png')],
|
|
'before/after dimension drift')
|
|
|
|
def r09_collection(evidence, index, pins):
|
|
original = Path(pins['original_root'])
|
|
require(original.is_absolute() and pins['native_candidate'] == index['commit'] == R09_COMMIT,
|
|
'R09 reuse candidate')
|
|
pinned = [pins['index'], pins['runner_input'], pins['runner_ended']]
|
|
pinned += [pins['OS'][role]['receipt'] for role in ('writer', 'reader')]
|
|
for pin in pinned:
|
|
path = Path(pin['path'])
|
|
require(path.is_relative_to(original) and not path.is_symlink(), 'collection pin path')
|
|
require(path.stat().st_size == pin['bytes'] and sha(path) == pin['sha256'], 'collection pin SHA')
|
|
for name in ['index.json', *index['artifacts']]:
|
|
require(not Path(name).is_absolute() and '..' not in Path(name).parts, 'collection unsafe path')
|
|
a, b = original/name, evidence/name
|
|
require(not a.is_symlink() and a.resolve().is_relative_to(original.resolve())
|
|
and a.read_bytes() == b.read_bytes(), 'original/canonical byte divergence '+name)
|
|
return original
|
|
|
|
def keyed(rows, key):
|
|
result = {r[key]: r for r in rows}
|
|
require(len(result) == len(rows), 'duplicate '+key)
|
|
return result
|
|
|
|
def infrastructure(r, facilities, root):
|
|
"""Runtime separates schema proxies from FacilityService; audit live topology.
|
|
|
|
FacilityInfrastructureProjector._projection_from_project_input,
|
|
_projection_live_matches and _expected_stair_connector are the authority.
|
|
"""
|
|
kinds = {'guest_corridor', 'service_corridor', 'staff_door', 'guest_elevator',
|
|
'service_elevator', 'guest_stairs', 'service_stairs'}
|
|
proxies = {k:v for k,v in facilities.items() if v['definition_id'] in kinds}
|
|
projections = keyed(r['facility_infrastructure'].get('projections', []), 'instance_id')
|
|
require(set(projections) == set(proxies), 'missing/extra infrastructure projection')
|
|
entities = keyed(r['spatial_subslots'].get('entities', []), 'entity_id')
|
|
connectors = keyed(r['path'].get('connectors', []), 'id')
|
|
routes, links, shafts = set(), set(), set()
|
|
for fid, f in proxies.items():
|
|
p = projections[fid]; kind = f['definition_id']
|
|
for field in ('definition_id', 'origin', 'rotation', 'layer', 'source_job_id', 'completed_at'):
|
|
require(p[field] == f[field], 'infrastructure construction drift '+field)
|
|
route = 'infra.route:'+fid
|
|
link = 'infra.connector:'+fid if kind in {'staff_door','guest_stairs','service_stairs'} else ''
|
|
require(p['kind'] == kind and p['cells'] == f['occupied_cells'] and
|
|
p['route_entity_id'] == route and p['connector_id'] == link,
|
|
'wrong infrastructure projection')
|
|
# Definition inputs are independently read from the unchanged registry resources.
|
|
definition = (root/'data/facilities/infrastructure'/(kind+'.tres')).read_text()
|
|
tags = re.findall(r'&"([^"]+)"', re.search(r'^tags = (.+)$', definition, re.M)[1])
|
|
footprint = [int(v) for v in re.search(r'footprint = Vector2i\((\d+), (\d+)\)', definition).groups()]
|
|
require(p['definition_tags'] == sorted(tags) and p['footprint'] == footprint and
|
|
p['pass_through'] == ('pass_through = true' in definition) and
|
|
p['staff_only'] == (kind in {'service_corridor','staff_door','service_elevator','service_stairs'}),
|
|
'infrastructure definition drift')
|
|
canonical = 'projection|'
|
|
for field in ('instance_id','definition_id','kind','route_entity_id','connector_id','source_job_id'):
|
|
text = p[field]; canonical += '%d:%s|' % (len(text),text)
|
|
canonical += 'layer=%d|staff=%d|pass=%d|footprint=%d,%d|rotation=%d|completed=%d|' % (
|
|
p['layer'],p['staff_only'],p['pass_through'],*p['footprint'],p['rotation'],p['completed_at'])
|
|
canonical += 'origin=%d,%d,%d|tags=' % tuple(p['origin'])
|
|
canonical += ''.join('%d:%s;' % (len(t),t) for t in p['definition_tags'])+'|cells='
|
|
canonical += ''.join('%d,%d,%d;' % tuple(c) for c in p['cells'])
|
|
require(p['record_fingerprint'] == hashlib.sha256(canonical.encode()).hexdigest(), 'infrastructure fingerprint drift')
|
|
require(entities.get(route) == {'entity_id':route,'category':'ROUTE','cells':p['cells']}, 'wrong infrastructure ROUTE topology')
|
|
routes.add(route)
|
|
if link:
|
|
upper = p['origin']; lower = [upper[0],upper[1]-1,upper[2]]
|
|
stair = kind.endswith('stairs')
|
|
expected = {'id':link,'from':upper if stair else [upper[0],upper[1],0],
|
|
'to':lower if stair else upper,'cost':150 if stair else 120,
|
|
'bidirectional':True,'access_id':'staff' if p['staff_only'] else '',
|
|
'enabled':True,'movement_type':'CONNECTOR','dynamic_cost':0,
|
|
'operational_state':'OPERATIONAL','cabin_capacity':8,'queue_capacity':256,
|
|
'cabin_state':'IDLE','current_floor':upper[1],'travel_minutes_per_floor':1,'request_queue':[]}
|
|
require(connectors.get(link) == expected, 'wrong infrastructure connector topology')
|
|
if stair:
|
|
require(lower in r['route_projection']['projected_walkable_cells'], 'missing stair landing')
|
|
links.add(link)
|
|
if kind.endswith('elevator'):
|
|
shafts.add('infra.shaft:'+fid)
|
|
require({k for k in entities if k.startswith('infra.route:')} == routes, 'extra infrastructure ROUTE topology')
|
|
require({k for k in connectors if k.startswith('infra.connector:')} == links, 'extra infrastructure connector topology')
|
|
blockers = keyed(r['path'].get('vertical_walk_blockers', []), 'owner_id')
|
|
require({k for k in blockers if k.startswith('infra.shaft:')} == shafts, 'wrong infrastructure shaft topology')
|
|
for fid, p in projections.items():
|
|
if 'infra.shaft:'+fid in shafts:
|
|
require(blockers['infra.shaft:'+fid]['cells'] == p['cells'], 'wrong infrastructure shaft cells')
|
|
if entities or proxies:
|
|
route_cells = {tuple(c) for e in entities.values() if e['category'] == 'ROUTE' for c in e['cells']}
|
|
projection = r['route_projection']
|
|
require(route_cells == {tuple(c) for c in projection['projected_route_cells']}, 'wrong projected ROUTE cells')
|
|
walkable = route_cells | {tuple(c) for c in projection['base_walkable_cells']}
|
|
require(walkable == {tuple(c) for c in projection['projected_walkable_cells']} ==
|
|
{tuple(c['cell']) for c in r['path']['cell_traffic']}, 'wrong projected walkable topology')
|
|
return proxies
|
|
|
|
def state(node, root=HERE.parent):
|
|
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')
|
|
proxies = infrastructure(r, facilities, root)
|
|
require(set(operational) == set(facilities)-set(proxies), '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 dispatch_gate(p, events):
|
|
d = p['dispatch']
|
|
presses = [e for e in events if e.get('button') == 1 and e.get('pressed') is True]
|
|
require(len(presses) == 1 and presses[0].get('dispatch') == d
|
|
and presses[0]['position'] == d['viewport'], 'OS dispatch event mismatch')
|
|
for key in ('bounds', 'map_position', 'cell_dimensions', 'zoom', 'pan',
|
|
'viewport_transform', 'screen_transform'):
|
|
require(d[key] == p[key], 'OS dispatch transform drift')
|
|
x, y = d['local']
|
|
require(math.isfinite(x) and math.isfinite(y), 'OS nonfinite dispatch')
|
|
origin, size, bounds = d['map_position'], d['cell_dimensions'], d['bounds']
|
|
derived = [bounds['min_x'] + math.floor((x-origin[0])/size[0]),
|
|
bounds['max_y'] - math.floor((y-origin[1])/size[1]), p['world_cell'][2]]
|
|
require(d['world_cell'] == derived == p['world_cell'], 'OS actual input cell drift')
|
|
for target in ('viewport', 'screen'):
|
|
matrix = d[target+'_transform']
|
|
expected = [matrix[0]*x+matrix[2]*y+matrix[4], matrix[1]*x+matrix[3]*y+matrix[5]]
|
|
require(len(d[target]) == 2 and all(math.isfinite(v) for v in d[target])
|
|
and all(abs(a-b) < 0.001 for a,b in zip(expected,d[target])), 'OS dispatch coordinate drift')
|
|
selection = p['selection']
|
|
require(isinstance(selection['required'], bool), 'OS selection requirement')
|
|
if selection['required']:
|
|
require(selection['occupant_id'] and selection['entity_id'] == selection['occupant_id'],
|
|
'OS selected entity 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, root=HERE.parent):
|
|
coordinates(row['position'])
|
|
before, after = typed(row['before']), typed(row['after'])
|
|
a, b = state(before, root), state(after, root)
|
|
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']), root)
|
|
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()}
|
|
original = evidence
|
|
pins_path = root/R09_DOCS/'ROOT_NATIVE_R09_COLLECTION_PINS.json'
|
|
if pins_path.exists():
|
|
r09_applicability(root, index)
|
|
r09_runner_binding(evidence, index, load(pins_path))
|
|
original = r09_collection(evidence, index, load(pins_path))
|
|
r09_images(evidence, index, load(root/R09_DOCS/'ROOT_R09_READONLY_IMAGE_DIMENSIONS.json'), load(pins_path))
|
|
actual = index['source_map']
|
|
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')
|
|
if not pins_path.exists():
|
|
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(original/prefix/'teardown', pid, original/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, root)
|
|
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']), root)['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, root)
|
|
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'):
|
|
data = artifact(ack[key]).read_bytes()
|
|
if pins_path.exists():
|
|
require(ack[key] == folder+key.replace('_', '-')+'.png', 'R09 screenshot request binding')
|
|
jpeg_dimensions(data)
|
|
else:
|
|
png(data)
|
|
if request['action'] == 'cell' and 'position' in row:
|
|
dispatch_gate(row['position'], observed['events'])
|
|
if row['id'] == 'pan_zoom':
|
|
selection = row['position']['selection']
|
|
require(selection['required'], 'OS missing entity selection')
|
|
occupants = decode(document('os-pair/'+row['after']+'.json'))['systems']['runtime']['world']['occupancies']
|
|
matches = [o['entity_id'] for o in occupants if row['position']['world_cell'] in o['cells']]
|
|
require(matches == [selection['occupant_id']], 'OS selected occupancy mismatch')
|
|
require(request['world_cell'] == row['position']['world_cell']
|
|
and request['viewport'] == row['position']['viewport']
|
|
and request['screen'] == row['position']['screen'], 'OS transformed cell drift')
|
|
matrix = request['viewport_to_screen']; x,y = request['viewport']
|
|
require(len(matrix) == 6 and all(math.isfinite(v) for v in matrix), 'invalid OS canvas mapping')
|
|
require(all(abs(a-b) < 0.001 for a,b in zip(request['screen'],
|
|
[matrix[0]*x+matrix[2]*y+matrix[4],matrix[1]*x+matrix[3]*y+matrix[5]])), 'OS canvas mapping drift')
|
|
if row['id'] == 'unsupported' and request['guide_visible']:
|
|
gx,gy,gw,gh = request['guide_rect']
|
|
require(not (gx <= x < gx+gw and gy <= y < gy+gh), 'OS guide interception')
|
|
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())
|