#!/usr/bin/env python3 # SPDX-License-Identifier: GPL-3.0-or-later """Closed host-only model of one bounded BigApp launcher lifecycle. The model accepts only exact built-in fake operations. It imports no target headers, socket, process, syscall, clock, CLI or filesystem interface. """ from __future__ import annotations from dataclasses import dataclass FIXED_TITLE = "PPSA01659" MAX_MAIN_TICKS = 64 MAX_FAKE_EVENTS = 64 MAX_CLEANUP_EVENTS = 3 CHECK_NO_BIGAPP = "CHECK_NO_BIGAPP" ATTACH_PARENT = "ATTACH_PARENT" ARM_FORK = "ARM_FORK" CONTINUE_PARENT = "CONTINUE_PARENT" LAUNCH_FIXED_TITLE = "LAUNCH_FIXED_TITLE" AWAIT_UNIQUE_CHILD = "AWAIT_UNIQUE_CHILD" DETACH_PARENT = "DETACH_PARENT" ARM_EXEC = "ARM_EXEC" CONTINUE_CHILD = "CONTINUE_CHILD" AWAIT_EXEC = "AWAIT_EXEC" REPLACE_EXACT_PAYLOAD = "REPLACE_EXACT_PAYLOAD" RESTORE_MUTATIONS = "RESTORE_MUTATIONS" DETACH_CHILD = "DETACH_CHILD" TERMINATE_CHILD = "TERMINATE_CHILD" EMIT_RESULT = "EMIT_RESULT" OK = "OK" NONE = "NONE" EXISTS = "EXISTS" CHILD = "CHILD" TIMEOUT = "TIMEOUT" ERROR = "ERROR" ALLOWED = { CHECK_NO_BIGAPP: {NONE, EXISTS, ERROR}, ATTACH_PARENT: {OK, ERROR}, ARM_FORK: {OK, ERROR}, CONTINUE_PARENT: {OK, ERROR}, LAUNCH_FIXED_TITLE: {OK, ERROR}, AWAIT_UNIQUE_CHILD: {CHILD, TIMEOUT, ERROR}, DETACH_PARENT: {OK, ERROR}, ARM_EXEC: {OK, ERROR}, CONTINUE_CHILD: {OK, ERROR}, AWAIT_EXEC: {OK, TIMEOUT, ERROR}, REPLACE_EXACT_PAYLOAD: {OK, ERROR}, RESTORE_MUTATIONS: {OK, ERROR}, DETACH_CHILD: {OK, ERROR}, TERMINATE_CHILD: {OK, ERROR}, EMIT_RESULT: {OK, ERROR}, } class LifecycleModelError(RuntimeError): """The synthetic lifecycle or its cleanup is invalid.""" @dataclass(frozen=True) class FakeEvent: operation: str result: str ticks: int = 1 child_id: int = 0 def __post_init__(self) -> None: if self.operation not in ALLOWED or self.result not in ALLOWED[self.operation]: raise LifecycleModelError("fake operation/result is invalid") if not isinstance(self.ticks, int) or isinstance(self.ticks, bool) \ or not 1 <= self.ticks <= MAX_MAIN_TICKS: raise LifecycleModelError("fake ticks are invalid") if self.operation == AWAIT_UNIQUE_CHILD and self.result == CHILD: if not isinstance(self.child_id, int) or isinstance(self.child_id, bool) \ or self.child_id <= 1: raise LifecycleModelError("fake child identity is invalid") elif self.child_id != 0: raise LifecycleModelError("unexpected fake child identity") class FakeLifecycleFacade: """Exact closed script; it cannot execute an operation itself.""" def __init__(self, events: tuple[FakeEvent, ...]) -> None: if not isinstance(events, tuple) or not 1 <= len(events) <= MAX_FAKE_EVENTS \ or any(type(event) is not FakeEvent for event in events): raise LifecycleModelError("fake lifecycle script is invalid") self._events = list(events) self.trace: list[str] = [] self.ticks = 0 def invoke(self, operation: str, cleanup: bool = False) -> FakeEvent: if not self._events: raise LifecycleModelError("fake lifecycle script is exhausted") event = self._events.pop(0) if event.operation != operation: raise LifecycleModelError("fake lifecycle ordering is invalid") self.ticks += event.ticks self.trace.append(f"{operation}:{event.result}") if not cleanup and self.ticks > MAX_MAIN_TICKS: raise LifecycleModelError("bounded main lifecycle expired") return event @property def remaining(self) -> int: return len(self._events) @dataclass(frozen=True) class LifecycleOutcome: classification: str success: bool child_id: int parent_detached: bool child_detached: bool child_terminated: bool mutations_restored: bool existing_bigapp_killed: bool fixed_title: str trace: tuple[str, ...] target_code_present: bool = False device_behavior_proven: bool = False def _require_ok(facade: FakeLifecycleFacade, operation: str) -> None: if facade.invoke(operation).result != OK: raise LifecycleModelError(f"{operation} failed") def run_lifecycle(facade: FakeLifecycleFacade) -> LifecycleOutcome: """Model one attempt and exhaustively unwind every acquired state.""" if type(facade) is not FakeLifecycleFacade: raise LifecycleModelError("only the exact fake facade is accepted") parent_attached = False parent_detached = False child_id = 0 child_detached = False child_terminated = False mutations_started = False mutations_restored = False success = False primary_error: Exception | None = None cleanup_events = 0 try: if facade.invoke(CHECK_NO_BIGAPP).result != NONE: raise LifecycleModelError("pre-existing BigApp blocks launch") _require_ok(facade, ATTACH_PARENT) parent_attached = True _require_ok(facade, ARM_FORK) _require_ok(facade, CONTINUE_PARENT) _require_ok(facade, LAUNCH_FIXED_TITLE) child = facade.invoke(AWAIT_UNIQUE_CHILD) if child.result != CHILD: raise LifecycleModelError("unique child was not observed") child_id = child.child_id _require_ok(facade, DETACH_PARENT) parent_attached = False parent_detached = True _require_ok(facade, ARM_EXEC) _require_ok(facade, CONTINUE_CHILD) _require_ok(facade, AWAIT_EXEC) replace = facade.invoke(REPLACE_EXACT_PAYLOAD) mutations_started = True if replace.result != OK: raise LifecycleModelError("exact payload replacement failed") _require_ok(facade, RESTORE_MUTATIONS) mutations_started = False mutations_restored = True _require_ok(facade, DETACH_CHILD) child_detached = True _require_ok(facade, EMIT_RESULT) success = True except Exception as error: # exact fake boundary normalization primary_error = error finally: try: if parent_attached: cleanup_events += 1 if facade.invoke(DETACH_PARENT, cleanup=True).result != OK: raise LifecycleModelError("parent cleanup failed") parent_attached = False parent_detached = True if mutations_started: cleanup_events += 1 if facade.invoke(RESTORE_MUTATIONS, cleanup=True).result != OK: raise LifecycleModelError("mutation restoration failed") mutations_started = False mutations_restored = True if child_id and not child_detached: cleanup_events += 1 if facade.invoke(TERMINATE_CHILD, cleanup=True).result != OK: raise LifecycleModelError("new child cleanup failed") child_terminated = True if cleanup_events > MAX_CLEANUP_EVENTS: raise LifecycleModelError("cleanup operation bound exceeded") except Exception as cleanup_error: raise LifecycleModelError("lifecycle cleanup is incomplete") from cleanup_error if facade.remaining: raise LifecycleModelError("fake lifecycle has unused operations") if primary_error is not None: return LifecycleOutcome( "OFFLINE_BIGAPP_LIFECYCLE_FAILED_CLEANLY", False, child_id, parent_detached, child_detached, child_terminated, mutations_restored, False, FIXED_TITLE, tuple(facade.trace)) if not success or not parent_detached or not child_detached \ or not mutations_restored or child_terminated: raise LifecycleModelError("successful lifecycle invariants failed") return LifecycleOutcome( "OFFLINE_BIGAPP_LIFECYCLE_MODEL_COMPLETE", True, child_id, parent_detached, child_detached, child_terminated, mutations_restored, False, FIXED_TITLE, tuple(facade.trace))