From 1a273357c226e900fa3a8c956d41aa2ad4864e36 Mon Sep 17 00:00:00 2001 From: Dzmitry Prychyna Date: Mon, 17 Aug 2026 18:48:03 -0300 Subject: [PATCH] assurance: bind closed formal scope and isolate release airgap --- ...est_alpha4_runtime_release_architecture.py | 36 ++ ...test_alpha4_runtime_three_way_assurance.py | 123 +++++- tools/alpha4_runtime_expression_airgap.py | 353 ++++++++++++++++-- tools/alpha4_runtime_manifest.py | 97 +++++ tools/alpha4_runtime_public_release_audit.py | 6 +- tools/alpha4_runtime_relational_expression.py | 28 +- tools/alpha4_runtime_release_admission.py | 25 +- tools/alpha4_runtime_release_profiles.py | 2 +- .../alpha4_runtime_triangulated_expression.py | 66 +++- 9 files changed, 670 insertions(+), 66 deletions(-) diff --git a/tests/test_alpha4_runtime_release_architecture.py b/tests/test_alpha4_runtime_release_architecture.py index 6ea5594..68e11e6 100644 --- a/tests/test_alpha4_runtime_release_architecture.py +++ b/tests/test_alpha4_runtime_release_architecture.py @@ -123,3 +123,39 @@ def test_generated_python_preserves_formal_evidence_set_identity(tmp_path: Path) assert next_runtime == current assert next_seed == seed assert result["code"] == "IDEMPOTENT_REPLAY" + + +def test_runtime_airgap_executes_generated_companion_under_restricted_runtime( + tmp_path: Path, monkeypatch +) -> None: + from tools import alpha4_runtime_expression_airgap as airgap + + profiles = tmp_path / "profiles" + base = profiles / "base/seed/python/aset_seed_alpha4.py" + runtime = profiles / "python/aset_runtime_alpha4.py" + base.parent.mkdir(parents=True) + runtime.parent.mkdir(parents=True) + base.write_text( + "def state(subject, authority, recognition='UNKNOWN', evidence=()):\n" + " return {'subject': subject, 'authority': authority, " + "'recognition': recognition, 'evidence': tuple(evidence)}\n\n" + "def apply_component(current, component_id, **kwargs):\n" + " return dict(current)\n", + encoding="utf-8", + ) + digest = "sha256:" + hashlib.sha256(base.read_bytes()).hexdigest() + write_python(runtime, digest, manifest_records()) + + class Binding: + companions = {"PYTHON": ("base/seed/python/aset_seed_alpha4.py", digest)} + + monkeypatch.setattr(airgap, "parse_seed_binding", Binding) + evidence = airgap.check_expression_airgap(profiles) + assert evidence["cases"]["start"] == 1452 + assert evidence["cases"]["end"] == 5808 + assert evidence["cases"]["total"] == 7260 + assert evidence["cases"]["identity_sensitivity"] == 5 + assert evidence["cases"]["grand_total"] == 7265 + assert evidence["companion_import_surface"] == "RESTRICTED" + assert evidence["companion_file_access"] == "MATERIALIZED_PROFILE_TREE_READ_ONLY" + assert evidence["status"] == "PASS" diff --git a/tests/test_alpha4_runtime_three_way_assurance.py b/tests/test_alpha4_runtime_three_way_assurance.py index 8e524a9..f4ca52f 100644 --- a/tests/test_alpha4_runtime_three_way_assurance.py +++ b/tests/test_alpha4_runtime_three_way_assurance.py @@ -39,7 +39,7 @@ def test_three_way_assurance_covers_complete_bounded_domain() -> None: assert evidence["causal_closed_world_contracts"] == 8 assert evidence["operational_causal_result_code_bindings"] == 8 assert evidence["relational_source_derivations"] == 8 - assert evidence["interface_validator_cases"] == 4 + assert evidence["interface_validator_cases"] == 28 assert evidence["identity_field_sensitivity"] == 5 assert evidence["evidence_set_order_invariance"] == 1 assert evidence["pairwise_relations"] == { @@ -92,7 +92,7 @@ def test_runtime_causal_output_surface_rejects_wrong_result_code(tmp_path: Path) def test_relational_source_derivation_and_identity_sensitivity_are_first_class() -> None: evidence = check_triangulated_assurance() assert evidence["relational_source_derivations"] == 8 - assert evidence["interface_validator_cases"] == 4 + assert evidence["interface_validator_cases"] == 28 assert evidence["identity_field_sensitivity"] == 5 assert evidence["evidence_set_order_invariance"] == 1 @@ -148,7 +148,7 @@ def test_bound_runtime_tla_replay_mutation_breaks_gate(tmp_path: Path) -> None: ) status, output = _run_gate(repo) assert status != 0 - assert "mismatch" in output.lower() or "sensitivity" in output.lower() + assert "relational canonical scope drift" in output.lower() def test_runtime_manifest_duplicate_precedence_breaks_gate(tmp_path: Path) -> None: @@ -220,3 +220,120 @@ def test_runtime_tlaps_runner_rejects_reduced_proof_scope(tmp_path: Path) -> Non ) assert result.returncode != 0 assert "SCOPE_DRIFT" in result.stdout + + +def test_runtime_relational_and_proof_scopes_are_closed_world(tmp_path: Path) -> None: + from tools.alpha4_runtime_manifest import ManifestError, parse_runtime_manifest + + repo = _copy_repo(tmp_path / "relational") + relational = repo / "runtime/alpha4/formal/RuntimeRelations.tla" + text = relational.read_text(encoding="utf-8") + marker = "ExactStartReplay(s, start) == start \\in s.starts" + assert marker in text + relational.write_text(text.replace(marker, marker + " /\\ FALSE", 1), encoding="utf-8") + with pytest.raises(ManifestError, match="relational canonical scope drift"): + parse_runtime_manifest(repo) + + repo = _copy_repo(tmp_path / "proof") + proof = repo / "runtime/alpha4/formal/OperationalRelationalPairingProofs.tla" + text = proof.read_text(encoding="utf-8") + marker = "THEOREM StartFreshPairing ==" + assert marker in text + proof.write_text(text.replace(marker, marker + "\n /\\ TRUE", 1), encoding="utf-8") + with pytest.raises(ManifestError, match="proof canonical scope drift"): + parse_runtime_manifest(repo) + + +def test_runtime_airgap_rejects_repository_semantic_import() -> None: + from tools.alpha4_runtime_expression_airgap import AirgapError, _validate_companion_ast + + source = "from tools.alpha4_runtime_relational_expression import derive_runtime_contract\n" + with pytest.raises(AirgapError, match="import forbidden"): + _validate_companion_ast( + source, + allowed_imports=frozenset({"hashlib", "copy", "pathlib"}), + allow_seed_loader=True, + ) + + +def test_runtime_airgap_rejects_import_smuggling_and_object_traversal() -> None: + from tools.alpha4_runtime_expression_airgap import AirgapError, _validate_companion_ast + + with pytest.raises(AirgapError, match="import forbidden"): + _validate_companion_ast( + "from pathlib import os\n", + allowed_imports=frozenset({"hashlib", "copy", "pathlib"}), + allow_seed_loader=True, + ) + + with pytest.raises(AirgapError, match="private attribute forbidden"): + _validate_companion_ast( + "value = ().__class__\n", + allowed_imports=frozenset({"hashlib", "copy", "pathlib"}), + allow_seed_loader=True, + ) + + +def test_runtime_release_sensitivity_rejects_ignored_start_binding() -> None: + from copy import deepcopy + + from tools.alpha4_runtime_expression_airgap import AirgapError, _check_identity_sensitivity + + def buggy_start(current, start, seed_state): + next_state = deepcopy(current) + same = [ + item + for item in next_state["starts"] + if item["attempt_id"] == start["attempt_id"] + and item["attempt_digest"] == start["attempt_digest"] + ] + if same: + result = { + "accepted": True, + "code": "IDEMPOTENT_REPLAY", + "state_changed": False, + "seed_projection": {"action": "STUTTER", "effect_permitted": False}, + } + else: + next_state["starts"].append(deepcopy(start)) + result = { + "accepted": True, + "code": "ATTEMPT_STARTED", + "state_changed": True, + "seed_projection": {"action": "STUTTER", "effect_permitted": False}, + } + return next_state, deepcopy(seed_state), result + + namespace = {"start_attempt": buggy_start, "end_attempt": lambda *args: args} + seed_state = {"subject": "s", "authority": "a", "recognition": "UNKNOWN", "evidence": ()} + with pytest.raises(AirgapError, match="start identity sensitivity"): + _check_identity_sensitivity(namespace, seed_state) + + +def test_runtime_formal_reflection_scope_is_closed_world(tmp_path: Path) -> None: + from tools.alpha4_runtime_manifest import ManifestError, parse_runtime_manifest + + repo = _copy_repo(tmp_path) + reflection = repo / "runtime/alpha4/formal/RestrictedOperationalSemantics.tla" + text = reflection.read_text(encoding="utf-8") + marker = "OperationalStartFresh(s, t, start, result) ==" + assert marker in text + reflection.write_text(text.replace(marker, marker + "\n /\\ TRUE", 1), encoding="utf-8") + with pytest.raises(ManifestError, match="formal reflection canonical scope drift"): + parse_runtime_manifest(repo) + + +def test_runtime_tla_scope_preserves_comment_tokens_inside_strings(tmp_path: Path) -> None: + from tools.alpha4_runtime_manifest import ManifestError, parse_runtime_manifest + + repo = _copy_repo(tmp_path) + relational = repo / "runtime/alpha4/formal/RuntimeRelations.tla" + text = relational.read_text(encoding="utf-8") + marker = 'result = "ATTEMPT_STARTED"' + assert marker in text + relational.write_text( + text.replace(marker, 'result = "ATTEMPT_STARTED(*scope-drift*)"', 1), + encoding="utf-8", + ) + with pytest.raises(ManifestError, match="relational canonical scope drift"): + parse_runtime_manifest(repo) diff --git a/tools/alpha4_runtime_expression_airgap.py b/tools/alpha4_runtime_expression_airgap.py index 9eb173e..2b5fdc6 100644 --- a/tools/alpha4_runtime_expression_airgap.py +++ b/tools/alpha4_runtime_expression_airgap.py @@ -1,6 +1,9 @@ from __future__ import annotations import argparse +import ast +import builtins +import io import itertools import json from copy import deepcopy @@ -12,6 +15,41 @@ ROOT = Path(__file__).resolve().parents[1] +_ALLOWED_DIRECT_IMPORTS = frozenset({"hashlib"}) +_ALLOWED_FROM_IMPORTS = { + "copy": frozenset({"deepcopy"}), + "pathlib": frozenset({"Path"}), +} +_FILESYSTEM_INSPECTION_METHODS = frozenset( + { + "absolute", + "cwd", + "exists", + "expanduser", + "glob", + "group", + "home", + "is_block_device", + "is_char_device", + "is_dir", + "is_fifo", + "is_file", + "is_mount", + "is_socket", + "is_symlink", + "iterdir", + "lstat", + "owner", + "readlink", + "resolve", + "rglob", + "samefile", + "stat", + "walk", + } +) + + class AirgapError(RuntimeError): pass @@ -21,13 +59,189 @@ def require(condition: bool, message: str) -> None: raise AirgapError(message) -def _load_expression(path: Path) -> dict[str, Any]: +def _validate_companion_ast( + source: str, *, allowed_imports: frozenset[str], allow_seed_loader: bool +) -> None: + tree = ast.parse(source) + parents: dict[ast.AST, ast.AST] = {} + for parent in ast.walk(tree): + for child in ast.iter_child_nodes(parent): + parents[child] = parent + + def enclosing_function(node: ast.AST) -> str | None: + current = node + while current in parents: + current = parents[current] + if isinstance(current, (ast.FunctionDef, ast.AsyncFunctionDef)): + return current.name + return None + + for node in ast.walk(tree): + if isinstance(node, ast.Import): + for alias in node.names: + require( + alias.asname is None + and alias.name in allowed_imports + and alias.name in _ALLOWED_DIRECT_IMPORTS, + f"air-gap companion import forbidden: {alias.name}", + ) + elif isinstance(node, ast.ImportFrom): + module = node.module or "" + imported = {alias.name for alias in node.names} + require(node.level == 0, "air-gap companion relative import forbidden") + if module == "__future__": + require( + imported == {"annotations"} + and all(alias.asname is None for alias in node.names), + "air-gap companion future import drift", + ) + else: + require( + module in allowed_imports + and module in _ALLOWED_FROM_IMPORTS + and imported <= _ALLOWED_FROM_IMPORTS[module] + and all(alias.asname is None for alias in node.names), + f"air-gap companion import forbidden: {module}", + ) + elif isinstance(node, ast.Name) and node.id == "__builtins__": + raise AirgapError("air-gap companion accesses __builtins__") + elif isinstance(node, ast.Attribute) and node.attr.startswith("_"): + raise AirgapError(f"air-gap companion private attribute forbidden: {node.attr}") + elif isinstance(node, ast.Call) and isinstance(node.func, ast.Name): + if node.func.id in { + "__import__", + "breakpoint", + "delattr", + "dir", + "eval", + "getattr", + "globals", + "help", + "input", + "locals", + "setattr", + "type", + "vars", + }: + raise AirgapError(f"air-gap companion dynamic capability forbidden: {node.func.id}") + if node.func.id in {"exec", "compile"}: + require( + allow_seed_loader and enclosing_function(node) == "_load_seed_base", + f"air-gap companion {node.func.id} permitted only for exact Seed base loader", + ) + elif isinstance(node, ast.Call) and isinstance(node.func, ast.Attribute): + require( + node.func.attr not in _FILESYSTEM_INSPECTION_METHODS, + f"air-gap companion filesystem inspection forbidden: {node.func.attr}", + ) + require( + node.func.attr + not in { + "write_text", + "write_bytes", + "unlink", + "rename", + "replace", + "mkdir", + "touch", + "chmod", + "symlink_to", + "hardlink_to", + }, + f"air-gap companion filesystem mutation forbidden: {node.func.attr}", + ) + elif isinstance(node, ast.Constant) and isinstance(node.value, str): + lowered = node.value.lower() + require( + not any( + marker in lowered for marker in ("tools.", "tools/", ".tla", ".forth", ".petri") + ), + "air-gap companion embeds repository semantic-source locator", + ) + + +def _load_expression( + path: Path, + allowed_root: Path, + *, + allowed_imports: frozenset[str], + allow_seed_loader: bool, +) -> dict[str, Any]: + source = path.read_text(encoding="utf-8") + _validate_companion_ast( + source, allowed_imports=allowed_imports, allow_seed_loader=allow_seed_loader + ) + allowed_root = allowed_root.resolve() + original_io_open = io.open + + def guarded_open(file: object, *args: object, **kwargs: object): + if isinstance(file, int): + return original_io_open(file, *args, **kwargs) + mode = kwargs.get("mode", args[0] if args else "r") + require( + isinstance(mode, str) and not any(flag in mode for flag in "wax+"), + "air-gap companion file access must be read-only", + ) + candidate = Path(file).resolve() # type: ignore[arg-type] + require( + candidate == allowed_root or allowed_root in candidate.parents, + f"air-gap companion file access escaped materialized profile tree: {candidate}", + ) + return original_io_open(file, *args, **kwargs) + + original_import = builtins.__import__ + + def guarded_import( + name: str, + globals: dict[str, Any] | None = None, + locals: dict[str, Any] | None = None, + fromlist: tuple[str, ...] = (), + level: int = 0, + ) -> Any: + requested = set(fromlist or ()) + if level != 0: + raise ImportError("air-gap companion relative import forbidden") + if name == "__future__": + if requested != {"annotations"}: + raise ImportError("air-gap companion future import drift") + elif name in _ALLOWED_DIRECT_IMPORTS: + if name not in allowed_imports or requested: + raise ImportError(f"air-gap companion import forbidden: {name}") + elif name in _ALLOWED_FROM_IMPORTS: + if ( + name not in allowed_imports + or not requested + or not requested <= _ALLOWED_FROM_IMPORTS[name] + ): + raise ImportError(f"air-gap companion import forbidden: {name}") + else: + raise ImportError(f"air-gap companion import forbidden: {name}") + return original_import(name, globals, locals, fromlist, level) + + safe_builtins = dict(vars(builtins)) + safe_builtins["__import__"] = guarded_import + safe_builtins["open"] = guarded_open + + def guarded_exec( + code: object, + globals_dict: dict[str, Any] | None = None, + locals_dict: dict[str, Any] | None = None, + ) -> None: + target_globals = {} if globals_dict is None else globals_dict + target_globals.setdefault("__builtins__", safe_builtins) + exec(code, target_globals, locals_dict) + + safe_builtins["exec"] = guarded_exec namespace: dict[str, Any] = { "__file__": str(path), "__name__": "aset_runtime_alpha4_airgap_subject", + "__builtins__": safe_builtins, } - source = path.read_text(encoding="utf-8") - exec(compile(source, str(path), "exec"), namespace) + io.open = guarded_open # type: ignore[assignment] + try: + exec(compile(source, str(path), "exec"), namespace) + finally: + io.open = original_io_open # type: ignore[assignment] return namespace @@ -156,6 +370,90 @@ def _expected_end( return next_state, _result(True, code, True) +def _check_identity_sensitivity(namespace: dict[str, Any], seed_state: dict[str, Any]) -> int: + identity_checks = 0 + identity_start = { + "attempt_id": "identity-a", + "attempt_digest": "identity-d", + "runtime_binding": "runtime:0", + "descriptor_binding": "descriptor:0", + } + identity_state = {"starts": [deepcopy(identity_start)], "terminals": []} + for field, replacement_value in ( + ("runtime_binding", "runtime:1"), + ("descriptor_binding", "descriptor:1"), + ): + candidate = {**identity_start, field: replacement_value} + expected_state, expected_result = _expected_start(identity_state, candidate) + actual_state, actual_seed, actual_result = namespace["start_attempt"]( + deepcopy(identity_state), deepcopy(candidate), deepcopy(seed_state) + ) + require( + actual_state == expected_state, + f"Runtime start identity sensitivity state mismatch: {field}", + ) + require( + actual_result == expected_result, + f"Runtime start identity sensitivity result mismatch: {field}", + ) + require(actual_seed == seed_state, "Runtime start identity sensitivity changed Seed state") + identity_checks += 1 + + set_start = { + "attempt_id": "set-a", + "attempt_digest": "set-d", + "runtime_binding": "runtime:set", + "descriptor_binding": "descriptor:set", + } + set_terminal = { + "attempt_id": "set-a", + "attempt_digest": "set-d", + "terminal_kind": "RESULT", + "terminal_digest": "set-t", + "terminal_binding": "terminal-binding:set", + "evidence_bindings": ["e0", "e1"], + } + terminal_state = {"starts": [deepcopy(set_start)], "terminals": [deepcopy(set_terminal)]} + for field, replacement_value in ( + ("terminal_binding", "terminal-binding:other"), + ("evidence_bindings", ["e0", "e2"]), + ): + candidate = {**set_terminal, field: replacement_value} + expected_state, expected_result = _expected_end(terminal_state, candidate) + actual_state, actual_seed, actual_result = namespace["end_attempt"]( + deepcopy(terminal_state), deepcopy(candidate), deepcopy(seed_state) + ) + require( + actual_state == expected_state, + f"Runtime terminal identity sensitivity state mismatch: {field}", + ) + require( + actual_result == expected_result, + f"Runtime terminal identity sensitivity result mismatch: {field}", + ) + require( + actual_seed == seed_state, + "Runtime terminal identity sensitivity changed Seed state", + ) + identity_checks += 1 + + reordered = {**set_terminal, "evidence_bindings": ["e1", "e0"]} + expected_state, expected_result = _expected_end(terminal_state, reordered) + actual_state, actual_seed, actual_result = namespace["end_attempt"]( + deepcopy(terminal_state), deepcopy(reordered), deepcopy(seed_state) + ) + require(actual_state == expected_state, "Runtime evidence-set replay state mismatch") + require(actual_result == expected_result, "Runtime evidence-set replay result mismatch") + require(actual_seed == seed_state, "Runtime evidence-set replay changed exact Seed state") + require( + actual_result["code"] == "IDEMPOTENT_REPLAY", + "Runtime evidence-set order changed identity", + ) + identity_checks += 1 + require(identity_checks == 5, "Runtime identity sensitivity coverage drift") + return identity_checks + + def check_expression_airgap(profiles_root: Path) -> dict[str, Any]: profiles_root = profiles_root.resolve() binding = parse_seed_binding() @@ -168,7 +466,13 @@ def check_expression_airgap(profiles_root: Path) -> dict[str, Any]: "Seed Python base byte identity mismatch", ) tree_before = tree_digest(profiles_root) - namespace = _load_expression(expression) + _load_expression(seed_base, profiles_root, allowed_imports=frozenset(), allow_seed_loader=False) + namespace = _load_expression( + expression, + profiles_root, + allowed_imports=frozenset({"hashlib", "copy", "pathlib"}), + allow_seed_loader=True, + ) require(callable(namespace.get("start_attempt")), "generated Runtime start entry point missing") require(callable(namespace.get("end_attempt")), "generated Runtime end entry point missing") require( @@ -204,34 +508,7 @@ def check_expression_airgap(profiles_root: Path) -> dict[str, Any]: require(actual_result == expected_result, "generated Runtime end result mismatch") require(actual_seed == seed_state, "Runtime end changed exact Seed state") end_checks += 1 - set_order_checks = 0 - set_start = { - "attempt_id": "set-a", - "attempt_digest": "set-d", - "runtime_binding": "runtime:set", - "descriptor_binding": "descriptor:set", - } - set_terminal = { - "attempt_id": "set-a", - "attempt_digest": "set-d", - "terminal_kind": "RESULT", - "terminal_digest": "set-t", - "terminal_binding": "terminal-binding:set", - "evidence_bindings": ["e0", "e1"], - } - set_state = {"starts": [deepcopy(set_start)], "terminals": [deepcopy(set_terminal)]} - reordered = {**set_terminal, "evidence_bindings": ["e1", "e0"]} - expected_state, expected_result = _expected_end(set_state, reordered) - actual_state, actual_seed, actual_result = namespace["end_attempt"]( - deepcopy(set_state), deepcopy(reordered), deepcopy(seed_states[0]) - ) - require(actual_state == expected_state, "Runtime evidence-set replay state mismatch") - require(actual_result == expected_result, "Runtime evidence-set replay result mismatch") - require(actual_seed == seed_states[0], "Runtime evidence-set replay changed exact Seed state") - require( - actual_result["code"] == "IDEMPOTENT_REPLAY", "Runtime evidence-set order changed identity" - ) - set_order_checks += 1 + identity_checks = _check_identity_sensitivity(namespace, seed_states[0]) require( tree_digest(profiles_root) == tree_before, "Runtime profile tree changed during air-gap verification", @@ -242,15 +519,19 @@ def check_expression_airgap(profiles_root: Path) -> dict[str, Any]: "semantic_precedence": "NONE", "semantic_source_runtime_dependency": "NONE", "generator_runtime_dependency": "NONE", + "companion_import_surface": "RESTRICTED", + "companion_file_access": "MATERIALIZED_PROFILE_TREE_READ_ONLY", "seed_base": {"sha256": sha256(seed_base), "status": "EXACT"}, "profile_tree_digest": tree_before, "cases": { "start": start_checks, "end": end_checks, "total": start_checks + end_checks, + "identity_sensitivity": identity_checks, + "grand_total": start_checks + end_checks + identity_checks, }, "seed_states_checked": ["UNKNOWN", "ALLOW", "BLOCK"], - "evidence_set_order_checks": set_order_checks, + "evidence_set_order_checks": 1, "seed_projection": "STUTTER", "status": "PASS", } @@ -274,6 +555,12 @@ def main() -> int: print(f"ALPHA4_RUNTIME_PYTHON_AIRGAP_START={cases['start']}/{cases['start']} PASS") print(f"ALPHA4_RUNTIME_PYTHON_AIRGAP_END={cases['end']}/{cases['end']} PASS") print(f"ALPHA4_RUNTIME_PYTHON_AIRGAP_TOTAL={cases['total']}/{cases['total']} PASS") + print( + "ALPHA4_RUNTIME_PYTHON_AIRGAP_IDENTITY_SENSITIVITY=" + f"{cases['identity_sensitivity']}/5 PASS" + ) + print(f"ALPHA4_RUNTIME_PYTHON_AIRGAP_GRAND_TOTAL={cases['grand_total']}/7265 PASS") + print("ALPHA4_RUNTIME_PYTHON_COMPANION_RUNTIME_ISOLATION=PASS") print( "ALPHA4_RUNTIME_PYTHON_EVIDENCE_SET_ORDER=" f"{evidence['evidence_set_order_checks']}/{evidence['evidence_set_order_checks']} PASS" diff --git a/tools/alpha4_runtime_manifest.py b/tools/alpha4_runtime_manifest.py index ae06107..b8e914b 100644 --- a/tools/alpha4_runtime_manifest.py +++ b/tools/alpha4_runtime_manifest.py @@ -1,5 +1,6 @@ from __future__ import annotations +import hashlib from collections import Counter from dataclasses import dataclass from pathlib import Path @@ -201,6 +202,80 @@ def require(condition: bool, message: str) -> None: ) +def _strip_tla_comments(source: str) -> str: + out: list[str] = [] + index = 0 + block_depth = 0 + in_string = False + while index < len(source): + if block_depth: + if source.startswith("(*", index): + block_depth += 1 + index += 2 + elif source.startswith("*)", index): + block_depth -= 1 + index += 2 + elif source[index] == "\n": + out.append("\n") + index += 1 + else: + index += 1 + continue + + if in_string: + char = source[index] + out.append(char) + if char == "\\" and index + 1 < len(source): + out.append(source[index + 1]) + index += 2 + else: + if char == '"': + in_string = False + index += 1 + continue + + if source.startswith("(*", index): + block_depth = 1 + index += 2 + continue + if source.startswith("\\*", index): + while index < len(source) and source[index] != "\n": + index += 1 + continue + char = source[index] + out.append(char) + if char == '"': + in_string = True + index += 1 + + if block_depth: + raise ManifestError("unterminated TLA block comment in canonical scope") + if in_string: + raise ManifestError("unterminated TLA string in canonical scope") + return "".join(out) + + +def _canonical_tla_scope_sha256(path: Path) -> str: + source = path.read_text(encoding="utf-8").replace("\r\n", "\n").replace("\r", "\n") + uncommented = _strip_tla_comments(source) + canonical = "\n".join(line.strip() for line in uncommented.splitlines() if line.strip()) + return "sha256:" + hashlib.sha256(canonical.encode("utf-8")).hexdigest() + + +EXPECTED_RELATIONAL_SCOPE_SHA256 = ( + "sha256:9908a323393ce02d08e8c4fc5d398611d23df07aba5497e53ff153aad3c7216d" +) +EXPECTED_FORMAL_REFLECTION_SCOPE_SHA256 = ( + "sha256:635c0aaf93cd792d5caad314b434dd3ba76673f6f19b2133a8ca67e4300e6125" +) +EXPECTED_PROOF_SCOPE_SHA256 = { + "OPERATIONAL_RELATIONAL_PAIRING": ( + "sha256:b7ff1f0337c949f242c110cd6b0191860d4fabdb81174e4a89653609e83f1f36" + ), + "SEED_BOUNDARY": ("sha256:ded37c5612ee835f8e8661519453ec5ef4d90a24b8926de6e3a9242cf451c928"), +} + + def _theorem_present(path: Path, theorem: str) -> bool: text = path.read_text(encoding="utf-8") return f"THEOREM {theorem}" in text or f"{theorem} ==" in text @@ -255,6 +330,22 @@ def parse_runtime_manifest(root: Path = ROOT) -> RuntimeBindingPlan: require(len({x.pairing_theorem for x in pairs}) == 8, "duplicate Runtime pairing theorem") for relative in (*sources.values(), *(p.module for p in proofs), *(p for _, p in derivers)): require((root / relative).is_file(), f"Runtime bound file missing: {relative}") + require( + _canonical_tla_scope_sha256(root / sources["RELATIONAL"]) + == EXPECTED_RELATIONAL_SCOPE_SHA256, + "Runtime relational canonical scope drift", + ) + require( + _canonical_tla_scope_sha256(root / sources["FORMAL-REFLECTION"]) + == EXPECTED_FORMAL_REFLECTION_SCOPE_SHA256, + "Runtime formal reflection canonical scope drift", + ) + for proof in proofs: + require( + _canonical_tla_scope_sha256(root / proof.module) + == EXPECTED_PROOF_SCOPE_SHA256[proof.proof_id], + f"Runtime proof canonical scope drift: {proof.proof_id}", + ) relational_text = (root / sources["RELATIONAL"]).read_text(encoding="utf-8") reflection_text = (root / sources["FORMAL-REFLECTION"]).read_text(encoding="utf-8") proof_text = "\n".join((root / proof.module).read_text(encoding="utf-8") for proof in proofs) @@ -294,6 +385,12 @@ def main() -> int: total = sum(item.expected_obligations for item in plan.proofs) print(f"ALPHA4_RUNTIME_MANIFEST_PAIRS={len(plan.pairs)}/{len(plan.pairs)} PASS") print(f"ALPHA4_RUNTIME_MANIFEST_PROOFS={len(plan.proofs)}/{len(plan.proofs)} PASS") + print("ALPHA4_RUNTIME_RELATIONAL_CANONICAL_SCOPE=1/1 PASS") + print("ALPHA4_RUNTIME_FORMAL_REFLECTION_CANONICAL_SCOPE=1/1 PASS") + print( + "ALPHA4_RUNTIME_PROOF_CANONICAL_SCOPES=" + f"{len(EXPECTED_PROOF_SCOPE_SHA256)}/{len(EXPECTED_PROOF_SCOPE_SHA256)} PASS" + ) print(f"ALPHA4_RUNTIME_MANIFEST_EXPECTED_TLAPS_OBLIGATIONS={total}") print("ALPHA4_RUNTIME_BINDING_PLAN=PASS") return 0 diff --git a/tools/alpha4_runtime_public_release_audit.py b/tools/alpha4_runtime_public_release_audit.py index 05528dd..6c22711 100644 --- a/tools/alpha4_runtime_public_release_audit.py +++ b/tools/alpha4_runtime_public_release_audit.py @@ -168,8 +168,10 @@ def check_public_release( require( isinstance(python_airgap, dict) and python_airgap.get("status") == "PASS" - and isinstance(python_airgap.get("cases"), int) - and python_airgap["cases"] > 0, + and python_airgap.get("structural_cases") == 7260 + and python_airgap.get("identity_sensitivity_cases") == 5 + and python_airgap.get("grand_total_cases") == 7265 + and python_airgap.get("runtime_isolation") == "PASS", "Python air-gap public evidence invalid", ) require(certificate.get("archive_binding") == "EXACT", "archive binding is not exact") diff --git a/tools/alpha4_runtime_relational_expression.py b/tools/alpha4_runtime_relational_expression.py index 34553d3..c57c357 100644 --- a/tools/alpha4_runtime_relational_expression.py +++ b/tools/alpha4_runtime_relational_expression.py @@ -257,17 +257,33 @@ def _result(contract: RuntimeContract, rule: RuntimeRule) -> dict[str, Any]: def _exact_start(contract: RuntimeContract, value: dict[str, Any]) -> bool: - return set(value) == set(contract.start_fields) + fields = set(contract.start_fields) + return set(value) == fields and all( + isinstance(value[field], str) and value[field] for field in fields + ) def _exact_terminal(contract: RuntimeContract, value: dict[str, Any]) -> bool: - if ( - set(value) != set(contract.terminal_fields) - or value.get("terminal_kind") not in contract.terminal_kinds - ): + fields = set(contract.terminal_fields) + if set(value) != fields or value.get("terminal_kind") not in contract.terminal_kinds: return False + for field in fields - {"terminal_kind", "evidence_bindings"}: + if not isinstance(value[field], str) or not value[field]: + return False evidence = value.get("evidence_bindings") - return isinstance(evidence, list) and len(evidence) == len(set(evidence)) + return ( + isinstance(evidence, list) + and all(isinstance(item, str) and item for item in evidence) + and len(evidence) == len(set(evidence)) + ) + + +def relational_exact_start_from_source(value: dict[str, Any], root: Path = ROOT) -> bool: + return _exact_start(derive_runtime_contract(root), value) + + +def relational_exact_terminal_from_source(value: dict[str, Any], root: Path = ROOT) -> bool: + return _exact_terminal(derive_runtime_contract(root), value) def _terminal_equal(contract: RuntimeContract, left: dict[str, Any], right: dict[str, Any]) -> bool: diff --git a/tools/alpha4_runtime_release_admission.py b/tools/alpha4_runtime_release_admission.py index 1a96ed4..ae83869 100644 --- a/tools/alpha4_runtime_release_admission.py +++ b/tools/alpha4_runtime_release_admission.py @@ -102,6 +102,21 @@ def check_release_admission( ) require(airgap["seed_base"]["status"] == "EXACT", "Python air-gap Seed base not exact") require(airgap["seed_projection"] == "STUTTER", "Python air-gap Seed projection drift") + cases = airgap.get("cases") + require( + isinstance(cases, dict) + and cases.get("total") == 7260 + and cases.get("identity_sensitivity") == 5 + and cases.get("grand_total") == 7265, + "Runtime Python air-gap sensitivity coverage drift", + ) + require( + airgap.get("semantic_source_runtime_dependency") == "NONE" + and airgap.get("generator_runtime_dependency") == "NONE" + and airgap.get("companion_import_surface") == "RESTRICTED" + and airgap.get("companion_file_access") == "MATERIALIZED_PROFILE_TREE_READ_ONLY", + "Runtime Python air-gap independence boundary drift", + ) seed_english = profiles_root / "base/seed/en/Seed.md" seed_python = profiles_root / "base/seed/python/aset_seed_alpha4.py" @@ -146,7 +161,10 @@ def check_release_admission( "python_seed_base": "EXACT", "python_airgap": { "status": "PASS", - "cases": airgap["cases"]["total"], + "structural_cases": airgap["cases"]["total"], + "identity_sensitivity_cases": airgap["cases"]["identity_sensitivity"], + "grand_total_cases": airgap["cases"]["grand_total"], + "runtime_isolation": "PASS", }, "release": { "tree_digest": release_tree, @@ -209,8 +227,11 @@ def main() -> int: print("ALPHA4_RUNTIME_RELEASE_ADMISSION_POST_BUILD_TLAPS=PASS") print("ALPHA4_RUNTIME_RELEASE_ADMISSION_ENGLISH_SEED_BASE=EXACT") print("ALPHA4_RUNTIME_RELEASE_ADMISSION_PYTHON_SEED_BASE=EXACT") - cases = certificate["python_airgap"]["cases"] + cases = certificate["python_airgap"]["structural_cases"] print(f"ALPHA4_RUNTIME_RELEASE_ADMISSION_PYTHON_AIRGAP={cases}/{cases} PASS") + print("ALPHA4_RUNTIME_RELEASE_ADMISSION_PYTHON_AIRGAP_IDENTITY_SENSITIVITY=5/5 PASS") + print("ALPHA4_RUNTIME_RELEASE_ADMISSION_PYTHON_AIRGAP_GRAND_TOTAL=7265/7265 PASS") + print("ALPHA4_RUNTIME_RELEASE_ADMISSION_PYTHON_RUNTIME_ISOLATION=PASS") print("ALPHA4_RUNTIME_RELEASE_ADMISSION_ARCHIVE_BINDING=EXACT") print("ALPHA4_RUNTIME_PUBLIC_ASSURANCE_REPRESENTATIONS=OPERATIONAL,RELATIONAL,CAUSAL") print("ALPHA4_RUNTIME_PUBLIC_POST_BUILD_FORMAL_ASSURANCE=PASS") diff --git a/tools/alpha4_runtime_release_profiles.py b/tools/alpha4_runtime_release_profiles.py index aaea1a7..d44f6e8 100644 --- a/tools/alpha4_runtime_release_profiles.py +++ b/tools/alpha4_runtime_release_profiles.py @@ -122,7 +122,7 @@ def write_python(target: Path, seed_python_sha256: str, records: list[dict[str, from pathlib import Path BASE_SEED_EXPRESSION_SHA256 = {seed_python_sha256!r} BASE_SEED_EXPRESSION_PATH = ( - Path(__file__).resolve().parents[1] + Path(__file__).parent.parent / "base" / "seed" / "python" diff --git a/tools/alpha4_runtime_triangulated_expression.py b/tools/alpha4_runtime_triangulated_expression.py index e0f5680..08780cf 100644 --- a/tools/alpha4_runtime_triangulated_expression.py +++ b/tools/alpha4_runtime_triangulated_expression.py @@ -24,7 +24,11 @@ relational_end, relational_start, ) -from tools.alpha4_runtime_relational_expression import validate_runtime_relational_source +from tools.alpha4_runtime_relational_expression import ( + relational_exact_start_from_source, + relational_exact_terminal_from_source, + validate_runtime_relational_source, +) ROOT = Path(__file__).resolve().parents[1] MANIFEST = ROOT / "runtime/alpha4/RUNTIME.aset" @@ -62,24 +66,48 @@ def check_interface_validator_independence() -> int: "terminal_binding": "b", "evidence_bindings": ["e0", "e1"], } - cases = [ - (exact_start(valid_start), causal_exact_start(valid_start), True), - ( - exact_start({**valid_start, "extra": "x"}), - causal_exact_start({**valid_start, "extra": "x"}), - False, - ), - (exact_terminal(valid_terminal), causal_exact_terminal(valid_terminal), True), - ( - exact_terminal({**valid_terminal, "evidence_bindings": ["e0", "e0"]}), - causal_exact_terminal({**valid_terminal, "evidence_bindings": ["e0", "e0"]}), - False, - ), - ] - for operational, causal, expected in cases: - if operational != expected or causal != expected: - raise RuntimeError("Runtime independent interface validators disagree with contract") - return len(cases) + start_cases: list[tuple[dict[str, object], bool]] = [(valid_start, True)] + for field in tuple(valid_start): + start_cases.append( + ({key: value for key, value in valid_start.items() if key != field}, False) + ) + start_cases.append(({**valid_start, "extra": "x"}, False)) + for field in tuple(valid_start): + start_cases.append(({**valid_start, field: ""}, False)) + start_cases.append(({**valid_start, "runtime_binding": 1}, False)) + + terminal_cases: list[tuple[dict[str, object], bool]] = [(valid_terminal, True)] + for field in tuple(valid_terminal): + terminal_cases.append( + ({key: value for key, value in valid_terminal.items() if key != field}, False) + ) + terminal_cases.extend( + [ + ({**valid_terminal, "extra": "x"}, False), + ({**valid_terminal, "terminal_kind": "WRONG"}, False), + ({**valid_terminal, "attempt_id": ""}, False), + ({**valid_terminal, "attempt_digest": ""}, False), + ({**valid_terminal, "terminal_digest": ""}, False), + ({**valid_terminal, "terminal_binding": ""}, False), + ({**valid_terminal, "terminal_binding": 1}, False), + ({**valid_terminal, "evidence_bindings": ["e0", "e0"]}, False), + ({**valid_terminal, "evidence_bindings": "e0"}, False), + ({**valid_terminal, "evidence_bindings": ["e0", ""]}, False), + ] + ) + for value, expected in start_cases: + operational = exact_start(value) + relational = relational_exact_start_from_source(value) + causal = causal_exact_start(value) + if operational != relational or relational != causal or causal != expected: + raise RuntimeError("Runtime start interface validators disagree with contract") + for value, expected in terminal_cases: + operational = exact_terminal(value) + relational = relational_exact_terminal_from_source(value) + causal = causal_exact_terminal(value) + if operational != relational or relational != causal or causal != expected: + raise RuntimeError("Runtime terminal interface validators disagree with contract") + return len(start_cases) + len(terminal_cases) def check_operational_causal_interface(net: CausalNet) -> tuple[int, int, int]: