diff --git a/runtime/alpha4/RUNTIME.aset b/runtime/alpha4/RUNTIME.aset index 8f4a55f..9bb91bb 100644 --- a/runtime/alpha4/RUNTIME.aset +++ b/runtime/alpha4/RUNTIME.aset @@ -40,14 +40,18 @@ SEED-PROJECTION ALL-RUNTIME-TRANSITIONS PRESERVE-SEED-STATE SEED-RECOGNITION-OWNER SEED-ONLY EFFECT-PERMITTED-BY-RUNTIME NEVER -PROOF OPERATIONAL_RELATIONAL_PAIRING runtime/alpha4/formal/OperationalRelationalPairingProofs.tla OperationalRelationalPairing -PROOF SEED_BOUNDARY runtime/alpha4/formal/SeedBoundaryProofs.tla RuntimePreservesSeedBoundary +PROOF OPERATIONAL_RELATIONAL_PAIRING runtime/alpha4/formal/OperationalRelationalPairingProofs.tla OperationalRelationalPairing 17 +PROOF SEED_BOUNDARY runtime/alpha4/formal/SeedBoundaryProofs.tla RuntimePreservesSeedBoundary 5 CHECK BINDING tools/validate_alpha4_runtime.py CHECK OPERATIONAL_RELATIONAL tools/alpha4_runtime_paired_expression.py CHECK ASSURANCE tools/alpha4_runtime_assurance.py CHECK TRIANGULATED_EXPRESSION tools/alpha4_runtime_triangulated_expression.py +DERIVER OPERATIONAL tools/alpha4_runtime_paired_expression.py +DERIVER RELATIONAL tools/alpha4_runtime_relational_expression.py +DERIVER CAUSAL tools/alpha4_runtime_causal_expression.py + RELATION OPERATIONAL_RELATIONAL BOUNDED_OPERATIONAL_RELATIONAL_CONGRUENCE RELATION OPERATIONAL_CAUSAL BOUNDED_OPERATIONAL_CAUSAL_CONGRUENCE RELATION OPERATIONAL_INTERFACE EXACT_STACK_EFFECT_CONTRACT @@ -55,5 +59,6 @@ RELATION CAUSAL_CONTRACT CLOSED_WORLD_REQUIREMENT_EFFECT_OUTPUT_CONTRACT RELATION OPERATIONAL_CAUSAL_RESULT OBSERVABLE_RESULT_CODE_CONGRUENCE RELATION RELATIONAL_CAUSAL BOUNDED_RELATIONAL_CAUSAL_CONGRUENCE RELATION TRIANGULATED THREE_WAY_BOUNDED_OBSERVATIONAL_CONGRUENCE +RELATION RELATIONAL_SOURCE BOUND_TLA_OPERATOR_DERIVATION GATE tools/alpha4_runtime_gate.py diff --git a/tests/test_alpha4_runtime.py b/tests/test_alpha4_runtime.py index b8a4596..dbaf02c 100644 --- a/tests/test_alpha4_runtime.py +++ b/tests/test_alpha4_runtime.py @@ -99,3 +99,27 @@ def test_terminal_identity_conflict_covers_terminal_binding() -> None: assert next_state == ended assert result["code"] == "TERMINAL_ATTEMPT_IMMUTABLE" assert result["accepted"] is False + + +def test_terminal_evidence_bindings_have_formal_set_identity() -> None: + start = { + "attempt_id": "a-set", + "attempt_digest": "d-set", + "runtime_binding": "runtime:set", + "descriptor_binding": "descriptor:set", + } + running, _ = operational_start({"starts": [], "terminals": []}, start) + terminal = { + "attempt_id": "a-set", + "attempt_digest": "d-set", + "terminal_kind": "RESULT", + "terminal_digest": "t-set", + "terminal_binding": "terminal-binding:set", + "evidence_bindings": ["e0", "e1"], + } + ended, _ = operational_end(running, terminal) + reordered = {**terminal, "evidence_bindings": ["e1", "e0"]} + next_state, result = operational_end(ended, reordered) + assert next_state == ended + assert result["accepted"] is True + assert result["code"] == "IDEMPOTENT_REPLAY" diff --git a/tests/test_alpha4_runtime_release_architecture.py b/tests/test_alpha4_runtime_release_architecture.py index 6c8e2eb..6ea5594 100644 --- a/tests/test_alpha4_runtime_release_architecture.py +++ b/tests/test_alpha4_runtime_release_architecture.py @@ -82,3 +82,44 @@ def test_public_root_matches_runtime_identity() -> None: assert identity["representation_id"] == "0.1.0-alpha.4" assert identity["subject_id"] == "ASET-RUNTIME-ALPHA4" assert identity["repository"] == "https://github.com/attractor-set/aset-runtime" + + +def test_generated_python_preserves_formal_evidence_set_identity(tmp_path: Path) -> None: + 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()) + namespace = {"__file__": str(runtime), "__name__": "runtime_test_subject_set"} + exec(compile(runtime.read_text(encoding="utf-8"), str(runtime), "exec"), namespace) + start = { + "attempt_id": "a", + "attempt_digest": "d", + "runtime_binding": "r", + "descriptor_binding": "q", + } + terminal = { + "attempt_id": "a", + "attempt_digest": "d", + "terminal_kind": "RESULT", + "terminal_digest": "t", + "terminal_binding": "b", + "evidence_bindings": ["e0", "e1"], + } + current = namespace["state"]([start], [terminal]) + seed = {"subject": "s", "authority": "a", "recognition": "ALLOW", "evidence": ("e",)} + reordered = {**terminal, "evidence_bindings": ["e1", "e0"]} + next_runtime, next_seed, result = namespace["end_attempt"](current, reordered, seed) + assert next_runtime == current + assert next_seed == seed + assert result["code"] == "IDEMPOTENT_REPLAY" diff --git a/tests/test_alpha4_runtime_three_way_assurance.py b/tests/test_alpha4_runtime_three_way_assurance.py index c4e457c..8e524a9 100644 --- a/tests/test_alpha4_runtime_three_way_assurance.py +++ b/tests/test_alpha4_runtime_three_way_assurance.py @@ -38,6 +38,10 @@ def test_three_way_assurance_covers_complete_bounded_domain() -> None: assert evidence["operational_stack_contracts"] == 8 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["identity_field_sensitivity"] == 5 + assert evidence["evidence_set_order_invariance"] == 1 assert evidence["pairwise_relations"] == { "operational_relational": "PASS", "operational_causal": "PASS", @@ -83,3 +87,136 @@ def test_runtime_causal_output_surface_rejects_wrong_result_code(tmp_path: Path) net = parse_causal_net(mutated) with pytest.raises(CausalExpressionError, match="causal output contract drift"): validate_causal_contract(net) + + +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["identity_field_sensitivity"] == 5 + assert evidence["evidence_set_order_invariance"] == 1 + + +def test_causal_interface_validators_are_not_imported_from_operational_model() -> None: + source = Path("tools/alpha4_runtime_causal_expression.py").read_text(encoding="utf-8") + assert "from tools.alpha4_runtime_paired_expression import exact_start" not in source + assert "from tools.alpha4_runtime_paired_expression import exact_terminal" not in source + assert "def causal_exact_start" in source + assert "def causal_exact_terminal" in source + + +def _copy_repo(tmp_path: Path) -> Path: + import shutil + import subprocess + + source = Path.cwd() + target = tmp_path / "repo" + shutil.copytree( + source, + target, + ignore=shutil.ignore_patterns(".git", ".pytest_cache", "__pycache__", ".tlacache", "dist"), + ) + subprocess.run(["git", "init", "-q"], cwd=target, check=True) + subprocess.run(["git", "add", "."], cwd=target, check=True) + return target + + +def _run_gate(repo: Path) -> tuple[int, str]: + import subprocess + import sys + + result = subprocess.run( + [sys.executable, "-m", "tools.alpha4_runtime_gate"], + cwd=repo, + text=True, + stdout=subprocess.PIPE, + stderr=subprocess.STDOUT, + check=False, + ) + return result.returncode, result.stdout + + +def test_bound_runtime_tla_replay_mutation_breaks_gate(tmp_path: Path) -> None: + repo = _copy_repo(tmp_path) + path = repo / "runtime/alpha4/formal/RuntimeRelations.tla" + text = path.read_text(encoding="utf-8") + old = "ExactStartReplay(s, start) == start \\in s.starts" + assert old in text + path.write_text( + text.replace(old, "ExactStartReplay(s, start) == StartIdentifierExists(s, start)", 1), + encoding="utf-8", + ) + status, output = _run_gate(repo) + assert status != 0 + assert "mismatch" in output.lower() or "sensitivity" in output.lower() + + +def test_runtime_manifest_duplicate_precedence_breaks_gate(tmp_path: Path) -> None: + repo = _copy_repo(tmp_path) + path = repo / "runtime/alpha4/RUNTIME.aset" + text = path.read_text(encoding="utf-8") + path.write_text( + text.replace( + "SEMANTIC-PRECEDENCE NONE", + "SEMANTIC-PRECEDENCE OPERATIONAL\nSEMANTIC-PRECEDENCE NONE", + 1, + ), + encoding="utf-8", + ) + status, output = _run_gate(repo) + assert status != 0 + assert "closed-world declaration drift" in output + + +def test_runtime_manifest_pair_and_proof_scope_are_canonical(tmp_path: Path) -> None: + import shutil + + from tools.alpha4_runtime_manifest import ManifestError, parse_runtime_manifest + + repo = _copy_repo(tmp_path) + manifest = repo / "runtime/alpha4/RUNTIME.aset" + text = manifest.read_text(encoding="utf-8") + text = text.replace( + "StartFresh OperationalStartFresh StartFreshPairing", + "BogusRelation OperationalStartFresh BogusPairing", + 1, + ) + manifest.write_text(text, encoding="utf-8") + with pytest.raises(ManifestError, match="PAIR binding drift"): + parse_runtime_manifest(repo) + + repo2 = tmp_path / "repo-proof" + shutil.copytree(repo, repo2) + manifest2 = repo2 / "runtime/alpha4/RUNTIME.aset" + text2 = manifest2.read_text(encoding="utf-8").replace( + "BogusRelation OperationalStartFresh BogusPairing", + "StartFresh OperationalStartFresh StartFreshPairing", + 1, + ) + text2 = text2.replace( + "OperationalRelationalPairing 17", + "OperationalRelationalPairing 1", + 1, + ) + manifest2.write_text(text2, encoding="utf-8") + with pytest.raises(ManifestError, match="proof binding/scope drift"): + parse_runtime_manifest(repo2) + + +def test_runtime_tlaps_runner_rejects_reduced_proof_scope(tmp_path: Path) -> None: + import subprocess + import sys + + fake = tmp_path / "tlapm" + fake.write_text("#!/bin/sh\necho 'All 1 obligation proved.'\n", encoding="utf-8") + fake.chmod(0o755) + result = subprocess.run( + [sys.executable, "tools/run_alpha4_runtime_tlaps.py", "--tlapm", str(fake)], + cwd=Path.cwd(), + text=True, + stdout=subprocess.PIPE, + stderr=subprocess.STDOUT, + check=False, + ) + assert result.returncode != 0 + assert "SCOPE_DRIFT" in result.stdout diff --git a/tools/alpha4_runtime_causal_expression.py b/tools/alpha4_runtime_causal_expression.py index af7bbc7..fab2e7f 100644 --- a/tools/alpha4_runtime_causal_expression.py +++ b/tools/alpha4_runtime_causal_expression.py @@ -5,11 +5,10 @@ from pathlib import Path from typing import Any -from tools.alpha4_runtime_paired_expression import exact_start, exact_terminal +from tools.alpha4_runtime_manifest import parse_runtime_manifest ROOT = Path(__file__).resolve().parents[1] CAUSAL = ROOT / "runtime/alpha4/causal/components.petri" -MANIFEST = ROOT / "runtime/alpha4/RUNTIME.aset" class CausalExpressionError(RuntimeError): @@ -142,6 +141,50 @@ class CausalNet: } +CAUSAL_START_FIELDS = {"attempt_id", "attempt_digest", "runtime_binding", "descriptor_binding"} +CAUSAL_TERMINAL_FIELDS = { + "attempt_id", + "attempt_digest", + "terminal_kind", + "terminal_digest", + "terminal_binding", + "evidence_bindings", +} +CAUSAL_TERMINAL_KINDS = {"RESULT", "NO_RESULT"} + + +def causal_exact_start(value: dict[str, Any]) -> bool: + return set(value) == CAUSAL_START_FIELDS and all( + isinstance(value[field], str) and value[field] for field in CAUSAL_START_FIELDS + ) + + +def causal_exact_terminal(value: dict[str, Any]) -> bool: + if ( + set(value) != CAUSAL_TERMINAL_FIELDS + or value.get("terminal_kind") not in CAUSAL_TERMINAL_KINDS + ): + return False + for field in CAUSAL_TERMINAL_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 all(isinstance(item, str) and item for item in evidence) + and len(evidence) == len(set(evidence)) + ) + + +def causal_terminal_equal(left: dict[str, Any], right: dict[str, Any]) -> bool: + if not causal_exact_terminal(left) or not causal_exact_terminal(right): + return False + scalar_fields = CAUSAL_TERMINAL_FIELDS - {"evidence_bindings"} + return all(left[field] == right[field] for field in scalar_fields) and set( + left["evidence_bindings"] + ) == set(right["evidence_bindings"]) + + def validate_causal_contract(net: CausalNet) -> int: actual = {item.symbol: item for item in net.transitions} require( @@ -242,21 +285,16 @@ def parse_causal_net(path: Path = CAUSAL) -> CausalNet: return CausalNet(1, "ASET-RUNTIME-ALPHA4-CAUSAL", semantic_precedence, mode, tuple(transitions)) -def manifest_bindings() -> dict[str, str]: - result: dict[str, str] = {} - for line in _lines(MANIFEST): - parts = line.split() - if parts[0] == "CAUSAL-BIND": - require(len(parts) == 3, f"invalid CAUSAL-BIND: {line}") - result[parts[1]] = parts[2] - require(len(result) == 8, "Runtime causal manifest bindings must contain eight entries") - return result +def manifest_bindings(root: Path = ROOT) -> dict[str, str]: + plan = parse_runtime_manifest(root) + return {item.component_id: item.causal_transition for item in plan.causal_bindings} -def check_causal_bindings() -> CausalNet: - net = parse_causal_net() +def check_causal_bindings(root: Path = ROOT) -> CausalNet: + plan = parse_runtime_manifest(root) + net = parse_causal_net(root / plan.causal_model) actual = {item.component_id: item.symbol for item in net.transitions} - require(actual == manifest_bindings(), "causal component binding mismatch") + require(actual == manifest_bindings(root), "causal component binding mismatch") validate_causal_contract(net) for transition in net.transitions: outputs = transition.output_map() @@ -290,7 +328,7 @@ def _result(transition: CausalTransition) -> dict[str, Any]: def causal_start( state: dict[str, list[dict[str, Any]]], start: dict[str, Any], net: CausalNet ) -> tuple[dict[str, list[dict[str, Any]]], dict[str, Any]]: - if not exact_start(start): + if not causal_exact_start(start): raise ValueError("exact start record required") current = _copy_state(state) same_id = [item for item in current["starts"] if item["attempt_id"] == start["attempt_id"]] @@ -319,7 +357,7 @@ def causal_start( def causal_end( state: dict[str, list[dict[str, Any]]], terminal: dict[str, Any], net: CausalNet ) -> tuple[dict[str, list[dict[str, Any]]], dict[str, Any]]: - if not exact_terminal(terminal): + if not causal_exact_terminal(terminal): raise ValueError("exact terminal record required") current = _copy_state(state) same_terminal_id = [ @@ -331,7 +369,7 @@ def causal_end( for item in current["starts"] ) facts = {"EXACT_TERMINAL"} - if terminal in same_terminal_id: + if any(causal_terminal_equal(item, terminal) for item in same_terminal_id): facts.add("EXACT_TERMINAL_REPLAY") elif same_terminal_id: facts.add("TERMINAL_CONFLICT") diff --git a/tools/alpha4_runtime_expression_airgap.py b/tools/alpha4_runtime_expression_airgap.py index ba2085c..9eb173e 100644 --- a/tools/alpha4_runtime_expression_airgap.py +++ b/tools/alpha4_runtime_expression_airgap.py @@ -103,6 +103,19 @@ def _result(accepted: bool, code: str, changed: bool) -> dict[str, Any]: } +def _terminal_equal(left: dict[str, Any], right: dict[str, Any]) -> bool: + scalar_fields = { + "attempt_id", + "attempt_digest", + "terminal_kind", + "terminal_digest", + "terminal_binding", + } + return all(left[field] == right[field] for field in scalar_fields) and set( + left["evidence_bindings"] + ) == set(right["evidence_bindings"]) + + def _expected_start( state: dict[str, list[dict[str, Any]]], start: dict[str, Any] ) -> tuple[dict[str, list[dict[str, Any]]], dict[str, Any]]: @@ -123,7 +136,7 @@ def _expected_end( same_id = [ item for item in next_state["terminals"] if item["attempt_id"] == terminal["attempt_id"] ] - if terminal in same_id: + if any(_terminal_equal(item, terminal) for item in same_id): return next_state, _result(True, "IDEMPOTENT_REPLAY", False) if same_id: return next_state, _result(False, "TERMINAL_ATTEMPT_IMMUTABLE", False) @@ -191,6 +204,34 @@ 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 require( tree_digest(profiles_root) == tree_before, "Runtime profile tree changed during air-gap verification", @@ -209,6 +250,7 @@ def check_expression_airgap(profiles_root: Path) -> dict[str, Any]: "total": start_checks + end_checks, }, "seed_states_checked": ["UNKNOWN", "ALLOW", "BLOCK"], + "evidence_set_order_checks": set_order_checks, "seed_projection": "STUTTER", "status": "PASS", } @@ -232,6 +274,10 @@ 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_EVIDENCE_SET_ORDER=" + f"{evidence['evidence_set_order_checks']}/{evidence['evidence_set_order_checks']} PASS" + ) print("ALPHA4_RUNTIME_PYTHON_SEED_BASE=EXACT") print("ALPHA4_RUNTIME_PYTHON_SEED_PROJECTION=STUTTER") print("ALPHA4_RUNTIME_PYTHON_SEMANTIC_SOURCE_DEPENDENCY=NONE") diff --git a/tools/alpha4_runtime_gate.py b/tools/alpha4_runtime_gate.py index d094b37..b229d22 100644 --- a/tools/alpha4_runtime_gate.py +++ b/tools/alpha4_runtime_gate.py @@ -8,6 +8,8 @@ COMMANDS = [ [sys.executable, "-m", "tools.validate_repository_minimal"], [sys.executable, "-m", "tools.validate_alpha4_runtime"], + [sys.executable, "-m", "tools.alpha4_runtime_manifest"], + [sys.executable, "-m", "tools.alpha4_runtime_relational_expression"], [sys.executable, "-m", "tools.alpha4_runtime_paired_expression"], [sys.executable, "-m", "tools.alpha4_runtime_assurance"], ] @@ -19,6 +21,7 @@ def main() -> int: if result.returncode: print("ALPHA4_RUNTIME_GATE=FAIL") return result.returncode + print("ALPHA4_RUNTIME_GATE_SCOPE=LOCAL_SEMANTIC_NO_TLAPS_NO_PYTEST") print("ALPHA4_RUNTIME_GATE=PASS") return 0 diff --git a/tools/alpha4_runtime_manifest.py b/tools/alpha4_runtime_manifest.py new file mode 100644 index 0000000..ae06107 --- /dev/null +++ b/tools/alpha4_runtime_manifest.py @@ -0,0 +1,307 @@ +from __future__ import annotations + +from collections import Counter +from dataclasses import dataclass +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[1] +MANIFEST = Path("runtime/alpha4/RUNTIME.aset") + + +class ManifestError(RuntimeError): + pass + + +@dataclass(frozen=True) +class PairBinding: + component_id: str + transition: str + formal_operator: str + operational_operator: str + pairing_theorem: str + + +@dataclass(frozen=True) +class CausalBinding: + component_id: str + causal_transition: str + + +@dataclass(frozen=True) +class ProofBinding: + proof_id: str + module: str + final_theorem: str + expected_obligations: int + + +@dataclass(frozen=True) +class RuntimeBindingPlan: + operational: str + relational: str + formal_reflection: str + causal_model: str + pairs: tuple[PairBinding, ...] + causal_bindings: tuple[CausalBinding, ...] + proofs: tuple[ProofBinding, ...] + derivers: tuple[tuple[str, str], ...] + relations: tuple[tuple[str, str], ...] + + def relation_map(self) -> dict[str, str]: + return dict(self.relations) + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ManifestError(message) + + +EXPECTED_HEADER = ("ASET-RUNTIME", "1", "ASET-RUNTIME-ALPHA4", "0.1.0-alpha.4") +EXPECTED_FIXED = ( + "SEMANTIC-PRECEDENCE NONE", + "PREDECESSOR-COMPATIBILITY NONE", + "UPSTREAM-SUBJECT ASET-SEED-0.4-ALPHA", + "UPSTREAM-BINDING upstream/ASET_SEED_ALPHA4_BINDING.aset", + ( + "SEED-EXTENSION-BIND OPERATIONAL " + "PRESERVE-UNKNOWN,PRESERVE-ALLOW,PRESERVE-BLOCK " + "ALL-RUNTIME-TRANSITIONS" + ), + ( + "SEED-EXTENSION-BIND RELATIONAL " + "PreserveUnknown,PreserveAllow,PreserveBlock " + "ALL-RUNTIME-TRANSITIONS" + ), + ( + "SEED-EXTENSION-BIND CAUSAL " + "PRESERVE-UNKNOWN,PRESERVE-ALLOW,PRESERVE-BLOCK " + "ALL-RUNTIME-TRANSITIONS" + ), + "STATE STARTS,TERMINALS EXACT-APPEND-ONLY-ATTEMPT-RECORDS", + "TRANSITION START-ATTEMPT", + "TRANSITION END-ATTEMPT", + "SEED-PROJECTION ALL-RUNTIME-TRANSITIONS PRESERVE-SEED-STATE", + "SEED-RECOGNITION-OWNER SEED-ONLY", + "EFFECT-PERMITTED-BY-RUNTIME NEVER", + "CHECK BINDING tools/validate_alpha4_runtime.py", + "CHECK OPERATIONAL_RELATIONAL tools/alpha4_runtime_paired_expression.py", + "CHECK ASSURANCE tools/alpha4_runtime_assurance.py", + "CHECK TRIANGULATED_EXPRESSION tools/alpha4_runtime_triangulated_expression.py", + "GATE tools/alpha4_runtime_gate.py", +) +EXPECTED_SOURCES = { + "OPERATIONAL": "runtime/alpha4/operational/components.forth", + "RELATIONAL": "runtime/alpha4/formal/RuntimeRelations.tla", + "FORMAL-REFLECTION": "runtime/alpha4/formal/RestrictedOperationalSemantics.tla", + "CAUSAL-MODEL": "runtime/alpha4/causal/components.petri", +} +EXPECTED_PAIRS = ( + PairBinding( + "ASET-RUNTIME-COMPONENT-START-FRESH", + "START-ATTEMPT", + "StartFresh", + "OperationalStartFresh", + "StartFreshPairing", + ), + PairBinding( + "ASET-RUNTIME-COMPONENT-START-REPLAY", + "START-ATTEMPT", + "StartReplay", + "OperationalStartReplay", + "StartReplayPairing", + ), + PairBinding( + "ASET-RUNTIME-COMPONENT-REJECT-START-CONFLICT", + "START-ATTEMPT", + "RejectStartConflict", + "OperationalRejectStartConflict", + "RejectStartConflictPairing", + ), + PairBinding( + "ASET-RUNTIME-COMPONENT-END-RESULT", + "END-ATTEMPT", + "EndResult", + "OperationalEndResult", + "EndResultPairing", + ), + PairBinding( + "ASET-RUNTIME-COMPONENT-END-NO-RESULT", + "END-ATTEMPT", + "EndNoResult", + "OperationalEndNoResult", + "EndNoResultPairing", + ), + PairBinding( + "ASET-RUNTIME-COMPONENT-END-REPLAY", + "END-ATTEMPT", + "EndReplay", + "OperationalEndReplay", + "EndReplayPairing", + ), + PairBinding( + "ASET-RUNTIME-COMPONENT-REJECT-END-CONFLICT", + "END-ATTEMPT", + "RejectEndConflict", + "OperationalRejectEndConflict", + "RejectEndConflictPairing", + ), + PairBinding( + "ASET-RUNTIME-COMPONENT-REJECT-END-NOT-RUNNING", + "END-ATTEMPT", + "RejectEndNotRunning", + "OperationalRejectEndNotRunning", + "RejectEndNotRunningPairing", + ), +) +EXPECTED_CAUSAL = tuple( + CausalBinding(item.component_id, transition) + for item, transition in zip( + EXPECTED_PAIRS, + ( + "START-FRESH", + "START-REPLAY", + "REJECT-START-CONFLICT", + "END-RESULT", + "END-NO-RESULT", + "END-REPLAY", + "REJECT-END-CONFLICT", + "REJECT-END-NOT-RUNNING", + ), + strict=True, + ) +) +EXPECTED_PROOFS = ( + ProofBinding( + "OPERATIONAL_RELATIONAL_PAIRING", + "runtime/alpha4/formal/OperationalRelationalPairingProofs.tla", + "OperationalRelationalPairing", + 17, + ), + ProofBinding( + "SEED_BOUNDARY", + "runtime/alpha4/formal/SeedBoundaryProofs.tla", + "RuntimePreservesSeedBoundary", + 5, + ), +) +EXPECTED_DERIVERS = ( + ("OPERATIONAL", "tools/alpha4_runtime_paired_expression.py"), + ("RELATIONAL", "tools/alpha4_runtime_relational_expression.py"), + ("CAUSAL", "tools/alpha4_runtime_causal_expression.py"), +) +EXPECTED_RELATIONS = ( + ("OPERATIONAL_RELATIONAL", "BOUNDED_OPERATIONAL_RELATIONAL_CONGRUENCE"), + ("OPERATIONAL_CAUSAL", "BOUNDED_OPERATIONAL_CAUSAL_CONGRUENCE"), + ("OPERATIONAL_INTERFACE", "EXACT_STACK_EFFECT_CONTRACT"), + ("CAUSAL_CONTRACT", "CLOSED_WORLD_REQUIREMENT_EFFECT_OUTPUT_CONTRACT"), + ("OPERATIONAL_CAUSAL_RESULT", "OBSERVABLE_RESULT_CODE_CONGRUENCE"), + ("RELATIONAL_CAUSAL", "BOUNDED_RELATIONAL_CAUSAL_CONGRUENCE"), + ("TRIANGULATED", "THREE_WAY_BOUNDED_OBSERVATIONAL_CONGRUENCE"), + ("RELATIONAL_SOURCE", "BOUND_TLA_OPERATOR_DERIVATION"), +) + + +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 + + +def parse_runtime_manifest(root: Path = ROOT) -> RuntimeBindingPlan: + path = root / MANIFEST + lines = [ + line.strip().split() + for line in path.read_text(encoding="utf-8").splitlines() + if line.strip() + ] + require(lines and tuple(lines[0]) == EXPECTED_HEADER, "Runtime manifest header drift") + fixed: list[str] = [] + sources: dict[str, str] = {} + pairs: list[PairBinding] = [] + causal: list[CausalBinding] = [] + proofs: list[ProofBinding] = [] + derivers: list[tuple[str, str]] = [] + relations: list[tuple[str, str]] = [] + for tokens in lines[1:]: + kind = tokens[0] + if kind in EXPECTED_SOURCES: + require(len(tokens) == 2 and kind not in sources, f"duplicate/invalid {kind}") + sources[kind] = tokens[1] + elif kind == "PAIR": + require(len(tokens) == 6, "invalid PAIR binding") + pairs.append(PairBinding(*tokens[1:])) + elif kind == "CAUSAL-BIND": + require(len(tokens) == 3, "invalid CAUSAL-BIND") + causal.append(CausalBinding(tokens[1], tokens[2])) + elif kind == "PROOF": + require(len(tokens) == 5, "proof binding must pin obligation count") + proofs.append(ProofBinding(tokens[1], tokens[2], tokens[3], int(tokens[4]))) + elif kind == "DERIVER": + require(len(tokens) == 3, "invalid DERIVER") + derivers.append((tokens[1], tokens[2])) + elif kind == "RELATION": + require(len(tokens) == 3, "invalid RELATION") + relations.append((tokens[1], tokens[2])) + else: + fixed.append(" ".join(tokens)) + require(Counter(fixed) == Counter(EXPECTED_FIXED), "Runtime closed-world declaration drift") + require(sources == EXPECTED_SOURCES, "Runtime representation source binding drift") + require(tuple(pairs) == EXPECTED_PAIRS, "Runtime PAIR binding drift") + require(tuple(causal) == EXPECTED_CAUSAL, "Runtime CAUSAL-BIND drift") + require(tuple(proofs) == EXPECTED_PROOFS, "Runtime proof binding/scope drift") + require(tuple(derivers) == EXPECTED_DERIVERS, "Runtime deriver binding drift") + require(tuple(relations) == EXPECTED_RELATIONS, "Runtime assurance relation binding drift") + require(len({x.component_id for x in pairs}) == 8, "duplicate Runtime pair component") + require(len({x.formal_operator for x in pairs}) == 8, "duplicate Runtime formal operator") + 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}") + 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) + for pair in pairs: + require( + f"{pair.formal_operator}(" in relational_text, + f"formal operator missing: {pair.formal_operator}", + ) + require( + f"{pair.operational_operator}(" in reflection_text, + f"operational reflection missing: {pair.operational_operator}", + ) + require( + pair.pairing_theorem in proof_text, f"pairing theorem missing: {pair.pairing_theorem}" + ) + for proof in proofs: + require( + _theorem_present(root / proof.module, proof.final_theorem), + f"final theorem missing: {proof.final_theorem}", + ) + return RuntimeBindingPlan( + operational=sources["OPERATIONAL"], + relational=sources["RELATIONAL"], + formal_reflection=sources["FORMAL-REFLECTION"], + causal_model=sources["CAUSAL-MODEL"], + pairs=tuple(pairs), + causal_bindings=tuple(causal), + proofs=tuple(proofs), + derivers=tuple(derivers), + relations=tuple(relations), + ) + + +def main() -> int: + try: + plan = parse_runtime_manifest(ROOT) + 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(f"ALPHA4_RUNTIME_MANIFEST_EXPECTED_TLAPS_OBLIGATIONS={total}") + print("ALPHA4_RUNTIME_BINDING_PLAN=PASS") + return 0 + except (ManifestError, OSError, UnicodeError, ValueError) as error: + print(f"ALPHA4_RUNTIME_MANIFEST_ERROR={error}") + print("ALPHA4_RUNTIME_BINDING_PLAN=FAIL") + return 1 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/tools/alpha4_runtime_paired_expression.py b/tools/alpha4_runtime_paired_expression.py index cefc2b6..7a94214 100644 --- a/tools/alpha4_runtime_paired_expression.py +++ b/tools/alpha4_runtime_paired_expression.py @@ -6,6 +6,11 @@ from pathlib import Path from typing import Any +from tools.alpha4_runtime_relational_expression import ( + relational_end_from_source, + relational_start_from_source, +) + ROOT = Path(__file__).resolve().parents[1] FORTH = ROOT / "runtime/alpha4/operational/components.forth" @@ -121,7 +126,20 @@ def exact_terminal(value: dict[str, Any]) -> bool: if not isinstance(value[field], str) or not value[field]: return False evidence = value["evidence_bindings"] - return isinstance(evidence, list) and all(isinstance(item, str) and item for item in evidence) + return ( + isinstance(evidence, list) + and all(isinstance(item, str) and item for item in evidence) + and len(evidence) == len(set(evidence)) + ) + + +def terminal_record_equal(left: dict[str, Any], right: dict[str, Any]) -> bool: + if not exact_terminal(left) or not exact_terminal(right): + return False + scalar_fields = TERMINAL_FIELDS - {"evidence_bindings"} + return all(left[field] == right[field] for field in scalar_fields) and set( + left["evidence_bindings"] + ) == set(right["evidence_bindings"]) def _result(accepted: bool, code: str, changed: bool) -> dict[str, Any]: @@ -164,17 +182,7 @@ def operational_start( def relational_start( state: dict[str, list[dict[str, Any]]], start: dict[str, Any] ) -> tuple[dict[str, list[dict[str, Any]]], dict[str, Any]]: - if not exact_start(start): - raise ValueError("exact start record required") - current = _copy_state(state) - identical = start in current["starts"] - identifier_exists = any(item["attempt_id"] == start["attempt_id"] for item in current["starts"]) - if identical: - return current, _result(True, "IDEMPOTENT_REPLAY", False) - if identifier_exists: - return current, _result(False, "ATTEMPT_IDENTITY_CONFLICT", False) - current["starts"].append(deepcopy(start)) - return current, _result(True, "ATTEMPT_STARTED", True) + return relational_start_from_source(state, start) def operational_end( @@ -187,7 +195,7 @@ def operational_end( same_terminal_id = [ item for item in current["terminals"] if item["attempt_id"] == terminal["attempt_id"] ] - if terminal in same_terminal_id: + if any(terminal_record_equal(item, terminal) for item in same_terminal_id): return current, _result(True, "IDEMPOTENT_REPLAY", False) if same_terminal_id: return current, _result(False, "TERMINAL_ATTEMPT_IMMUTABLE", False) @@ -202,27 +210,62 @@ def operational_end( def relational_end( state: dict[str, list[dict[str, Any]]], terminal: dict[str, Any] ) -> tuple[dict[str, list[dict[str, Any]]], dict[str, Any]]: - if not exact_terminal(terminal): - raise ValueError("exact terminal record required") - current = _copy_state(state) - identical = terminal in current["terminals"] - identifier_exists = any( - item["attempt_id"] == terminal["attempt_id"] for item in current["terminals"] - ) - if identical: - return current, _result(True, "IDEMPOTENT_REPLAY", False) - if identifier_exists: - return current, _result(False, "TERMINAL_ATTEMPT_IMMUTABLE", False) - matching = _matching_start(current, terminal) - if not matching: - return current, _result(False, "ATTEMPT_NOT_RUNNING", False) - current["terminals"].append(deepcopy(terminal)) - code = ( - "ATTEMPT_ENDED_WITH_RESULT" - if terminal["terminal_kind"] == "RESULT" - else "ATTEMPT_ENDED_WITH_NO_RESULT" - ) - return current, _result(True, code, True) + return relational_end_from_source(state, terminal) + + +def field_sensitivity_check() -> dict[str, int]: + base_start = { + "attempt_id": "sensitive-attempt", + "attempt_digest": "digest:0", + "runtime_binding": "runtime:0", + "descriptor_binding": "descriptor:0", + } + running = {"starts": [deepcopy(base_start)], "terminals": []} + start_cases = 0 + for field, replacement in ( + ("runtime_binding", "runtime:1"), + ("descriptor_binding", "descriptor:1"), + ): + candidate = {**base_start, field: replacement} + operational = operational_start(running, candidate) + relational = relational_start(running, candidate) + if operational != relational or operational[1]["code"] != "ATTEMPT_IDENTITY_CONFLICT": + raise RuntimeError(f"Runtime start field sensitivity failed: {field}") + start_cases += 1 + + base_terminal = { + "attempt_id": base_start["attempt_id"], + "attempt_digest": base_start["attempt_digest"], + "terminal_kind": "RESULT", + "terminal_digest": "terminal:0", + "terminal_binding": "terminal-binding:0", + "evidence_bindings": ["e0", "e1"], + } + ended = {"starts": [deepcopy(base_start)], "terminals": [deepcopy(base_terminal)]} + terminal_cases = 0 + for field, replacement in ( + ("terminal_binding", "terminal-binding:1"), + ("evidence_bindings", ["e0", "e2"]), + ): + candidate = {**base_terminal, field: replacement} + operational = operational_end(ended, candidate) + relational = relational_end(ended, candidate) + if operational != relational or operational[1]["code"] != "TERMINAL_ATTEMPT_IMMUTABLE": + raise RuntimeError(f"Runtime terminal field sensitivity failed: {field}") + terminal_cases += 1 + + reordered = {**base_terminal, "evidence_bindings": ["e1", "e0"]} + operational = operational_end(ended, reordered) + relational = relational_end(ended, reordered) + if operational != relational or operational[1]["code"] != "IDEMPOTENT_REPLAY": + raise RuntimeError("Runtime evidence set-order invariance failed") + evidence_set_cases = 1 + return { + "start": start_cases, + "terminal": terminal_cases, + "evidence_set": evidence_set_cases, + "total": start_cases + terminal_cases + evidence_set_cases, + } def bounded_domain() -> tuple[ @@ -361,12 +404,17 @@ def main() -> int: parse_operational_words() counts = bounded_pairing_check() safety = bounded_safety_check() + sensitivity = field_sensitivity_check() print("ALPHA4_RUNTIME_OPERATIONAL_WORDS=8/8 PASS") print(f"ALPHA4_RUNTIME_START_PAIRED_CASES={counts['start']}/{counts['start']} PASS") print(f"ALPHA4_RUNTIME_END_PAIRED_CASES={counts['end']}/{counts['end']} PASS") print(f"ALPHA4_RUNTIME_PAIRED_CASES={counts['total']}/{counts['total']} PASS") print(f"ALPHA4_RUNTIME_BOUNDED_SAFETY={safety['total']}/{safety['total']} PASS") print("ALPHA4_RUNTIME_APPEND_ONLY_BOUNDARY=PASS") + print( + "ALPHA4_RUNTIME_IDENTITY_FIELD_SENSITIVITY=" + f"{sensitivity['total']}/{sensitivity['total']} PASS" + ) print("ALPHA4_RUNTIME_PAIRED_EXPRESSION=PASS") return 0 diff --git a/tools/alpha4_runtime_relational_expression.py b/tools/alpha4_runtime_relational_expression.py new file mode 100644 index 0000000..34553d3 --- /dev/null +++ b/tools/alpha4_runtime_relational_expression.py @@ -0,0 +1,373 @@ +from __future__ import annotations + +import re +from copy import deepcopy +from dataclasses import dataclass +from pathlib import Path +from typing import Any + +from tools.alpha4_runtime_manifest import parse_runtime_manifest + +ROOT = Path(__file__).resolve().parents[1] + + +class RelationalExpressionError(RuntimeError): + pass + + +def require(condition: bool, message: str) -> None: + if not condition: + raise RelationalExpressionError(message) + + +def strip_tla_comments(text: str) -> str: + without_blocks = re.sub(r"\(\*.*?\*\)", "", text, flags=re.DOTALL) + return re.sub(r"(?m)\\\*.*$", "", without_blocks) + + +def compact(text: str) -> str: + return re.sub(r"\s+", "", text) + + +def extract_operator(text: str, operator: str) -> tuple[tuple[str, ...], str]: + pattern = re.compile( + rf"(?ms)^{re.escape(operator)}\((?P[^)]*)\)\s*==\s*(?P.*?)" + rf"(?=^[A-Z][A-Za-z0-9_]*\([^)]*\)\s*==|^[A-Z][A-Za-z0-9_]*\s*==|^=+)" + ) + match = pattern.search(text) + if match is None: + raise RelationalExpressionError(f"formal operator missing: {operator}") + args = tuple(item.strip() for item in match.group("args").split(",") if item.strip()) + return args, compact(match.group("body")) + + +def extract_value(text: str, operator: str) -> str: + pattern = re.compile( + rf"(?ms)^{re.escape(operator)}\s*==\s*(?P.*?)" + rf"(?=^[A-Z][A-Za-z0-9_]*\([^)]*\)\s*==|^[A-Z][A-Za-z0-9_]*\s*==|^=+)" + ) + match = pattern.search(text) + if match is None: + raise RelationalExpressionError(f"formal value missing: {operator}") + return compact(match.group("body")) + + +def _record_fields(body: str) -> tuple[str, ...]: + fields = tuple(re.findall(r"([a-z_]+):(?:SUBSET)?[A-Za-z][A-Za-z0-9_]*", body)) + require(fields, f"record fields missing: {body}") + return fields + + +def _quoted_set(body: str) -> frozenset[str]: + return frozenset(re.findall(r'"([A-Z0-9_]+)"', body)) + + +@dataclass(frozen=True) +class RuntimeRule: + component_id: str + operator: str + classifier: str + effect: str + result_code: str + terminal_kind: str | None = None + + +@dataclass(frozen=True) +class RuntimeContract: + start_fields: tuple[str, ...] + terminal_fields: tuple[str, ...] + terminal_kinds: frozenset[str] + start_identifier_field: str + terminal_identifier_field: str + start_replay_mode: str + terminal_replay_mode: str + matching_fields: tuple[str, ...] + accepted_results: frozenset[str] + seed_action: str + rules: tuple[RuntimeRule, ...] + + +def derive_runtime_contract(root: Path = ROOT) -> RuntimeContract: + plan = parse_runtime_manifest(root) + text = strip_tla_comments((root / plan.relational).read_text(encoding="utf-8")) + start_fields = _record_fields(extract_value(text, "StartUniverse")) + terminal_fields = _record_fields(extract_value(text, "TerminalUniverse")) + terminal_kinds = _quoted_set(extract_value(text, "TerminalKinds")) + + _, same_start = extract_operator(text, "SameStartIdentifier") + start_id_match = re.fullmatch(r"a\.([a-z_]+)=b\.([a-z_]+)", same_start) + require( + start_id_match is not None and start_id_match.group(1) == start_id_match.group(2), + "SameStartIdentifier semantics drift", + ) + start_identifier_field = start_id_match.group(1) + + _, same_terminal = extract_operator(text, "SameTerminalIdentifier") + terminal_id_match = re.fullmatch(r"a\.([a-z_]+)=b\.([a-z_]+)", same_terminal) + require( + terminal_id_match is not None and terminal_id_match.group(1) == terminal_id_match.group(2), + "SameTerminalIdentifier semantics drift", + ) + terminal_identifier_field = terminal_id_match.group(1) + + _, start_replay = extract_operator(text, "ExactStartReplay") + if start_replay == "start\\ins.starts": + start_replay_mode = "EXACT_RECORD" + elif start_replay == "StartIdentifierExists(s,start)": + start_replay_mode = "IDENTIFIER_ONLY" + else: + raise RelationalExpressionError("ExactStartReplay semantics unsupported") + _, terminal_replay = extract_operator(text, "ExactTerminalReplay") + if terminal_replay == "terminal\\ins.terminals": + terminal_replay_mode = "EXACT_RECORD" + elif terminal_replay == "TerminalIdentifierExists(s,terminal)": + terminal_replay_mode = "IDENTIFIER_ONLY" + else: + raise RelationalExpressionError("ExactTerminalReplay semantics unsupported") + + _, start_conflict = extract_operator(text, "StartConflict") + require( + "StartIdentifierExists(s,start)" in start_conflict + and "~ExactStartReplay(s,start)" in start_conflict, + "StartConflict semantics drift", + ) + _, terminal_conflict = extract_operator(text, "TerminalConflict") + require( + "TerminalIdentifierExists(s,terminal)" in terminal_conflict + and "~ExactTerminalReplay(s,terminal)" in terminal_conflict, + "TerminalConflict semantics drift", + ) + + _, matching = extract_operator(text, "MatchingStart") + matching_pairs = re.findall(r"start\.([a-z_]+)=terminal\.([a-z_]+)", matching) + require( + matching_pairs and all(left == right for left, right in matching_pairs), + "MatchingStart field relation drift", + ) + matching_fields = tuple(left for left, _ in matching_pairs) + + accepted_body = extract_operator(text, "AcceptedResult")[1] + marker = "result\\in" + require(marker in accepted_body, "AcceptedResult membership relation missing") + accepted_results = _quoted_set(accepted_body.split(marker, 1)[1]) + _, seed_action_body = extract_operator(text, "SeedProjectionAction") + seed_action_match = re.fullmatch(r'"([A-Z0-9_]+)"', seed_action_body) + require(seed_action_match is not None, "SeedProjectionAction literal missing") + _, seed_effect = extract_operator(text, "SeedProjectionEffectPermitted") + require(seed_effect == "FALSE", "SeedProjectionEffectPermitted must remain FALSE") + + rules: list[RuntimeRule] = [] + for pair in plan.pairs: + _, body = extract_operator(text, pair.formal_operator) + require( + "RuntimeInvariant(s)" in body, + f"{pair.formal_operator}: RuntimeInvariant precondition missing", + ) + universe = ( + "start\\inStartUniverse" + if pair.transition == "START-ATTEMPT" + else "terminal\\inTerminalUniverse" + ) + require(universe in body, f"{pair.formal_operator}: record universe precondition missing") + classifier: str + terminal_kind: str | None = None + if pair.formal_operator == "StartFresh": + require("FreshStartIdentifier(s,start)" in body, "StartFresh guard drift") + classifier, effect = "START_FRESH", "ADD_START" + elif pair.formal_operator == "StartReplay": + require("ExactStartReplay(s,start)" in body, "StartReplay guard drift") + classifier, effect = "START_REPLAY", "PRESERVE" + elif pair.formal_operator == "RejectStartConflict": + require("StartConflict(s,start)" in body, "RejectStartConflict guard drift") + classifier, effect = "START_CONFLICT", "PRESERVE" + elif pair.formal_operator in {"EndResult", "EndNoResult"}: + require( + "ExactRunning(s,terminal)" in body, + f"{pair.formal_operator}: ExactRunning guard drift", + ) + kind_match = re.search(r'terminal\.terminal_kind="(RESULT|NO_RESULT)"', body) + require(kind_match is not None, f"{pair.formal_operator}: terminal kind guard missing") + terminal_kind = kind_match.group(1) + classifier, effect = "END_RUNNING", "ADD_TERMINAL" + elif pair.formal_operator == "EndReplay": + require("ExactTerminalReplay(s,terminal)" in body, "EndReplay guard drift") + classifier, effect = "END_REPLAY", "PRESERVE" + elif pair.formal_operator == "RejectEndConflict": + require("TerminalConflict(s,terminal)" in body, "RejectEndConflict guard drift") + classifier, effect = "END_CONFLICT", "PRESERVE" + elif pair.formal_operator == "RejectEndNotRunning": + require( + "FreshTerminalIdentifier(s,terminal)" in body + and "~MatchingStart(s,terminal)" in body, + "RejectEndNotRunning guard drift", + ) + classifier, effect = "END_NOT_RUNNING", "PRESERVE" + else: + raise RelationalExpressionError(f"unsupported Runtime operator: {pair.formal_operator}") + if effect == "ADD_START": + require( + "!.starts=@\\cup{start}" in body, f"{pair.formal_operator}: add-start effect drift" + ) + elif effect == "ADD_TERMINAL": + require( + "!.terminals=@\\cup{terminal}" in body, + f"{pair.formal_operator}: add-terminal effect drift", + ) + else: + require("t=s" in body, f"{pair.formal_operator}: preserve-state effect drift") + result_match = re.search(r'result="([A-Z0-9_]+)"', body) + require(result_match is not None, f"{pair.formal_operator}: result code missing") + rules.append( + RuntimeRule( + pair.component_id, + pair.formal_operator, + classifier, + effect, + result_match.group(1), + terminal_kind, + ) + ) + + return RuntimeContract( + start_fields=start_fields, + terminal_fields=terminal_fields, + terminal_kinds=terminal_kinds, + start_identifier_field=start_identifier_field, + terminal_identifier_field=terminal_identifier_field, + start_replay_mode=start_replay_mode, + terminal_replay_mode=terminal_replay_mode, + matching_fields=matching_fields, + accepted_results=accepted_results, + seed_action=seed_action_match.group(1), + rules=tuple(rules), + ) + + +def _copy_state(state: dict[str, list[dict[str, Any]]]) -> dict[str, list[dict[str, Any]]]: + return {"starts": deepcopy(state["starts"]), "terminals": deepcopy(state["terminals"])} + + +def _result(contract: RuntimeContract, rule: RuntimeRule) -> dict[str, Any]: + return { + "accepted": rule.result_code in contract.accepted_results, + "code": rule.result_code, + "state_changed": rule.effect in {"ADD_START", "ADD_TERMINAL"}, + "seed_projection": {"action": contract.seed_action, "effect_permitted": False}, + } + + +def _exact_start(contract: RuntimeContract, value: dict[str, Any]) -> bool: + return set(value) == set(contract.start_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 + ): + return False + evidence = value.get("evidence_bindings") + return isinstance(evidence, list) and len(evidence) == len(set(evidence)) + + +def _terminal_equal(contract: RuntimeContract, left: dict[str, Any], right: dict[str, Any]) -> bool: + if not _exact_terminal(contract, left) or not _exact_terminal(contract, right): + return False + scalar_fields = set(contract.terminal_fields) - {"evidence_bindings"} + return all(left[field] == right[field] for field in scalar_fields) and set( + left["evidence_bindings"] + ) == set(right["evidence_bindings"]) + + +def _identifier_exists(records: list[dict[str, Any]], value: dict[str, Any], field: str) -> bool: + return any(item[field] == value[field] for item in records) + + +def _matching_start( + contract: RuntimeContract, state: dict[str, Any], terminal: dict[str, Any] +) -> bool: + return any( + all(start[field] == terminal[field] for field in contract.matching_fields) + for start in state["starts"] + ) + + +def relational_start_from_source( + state: dict[str, list[dict[str, Any]]], start: dict[str, Any], root: Path = ROOT +) -> tuple[dict[str, list[dict[str, Any]]], dict[str, Any]]: + contract = derive_runtime_contract(root) + if not _exact_start(contract, start): + raise ValueError("exact start record required") + current = _copy_state(state) + identifier_exists = _identifier_exists( + current["starts"], start, contract.start_identifier_field + ) + exact_replay = ( + start in current["starts"] + if contract.start_replay_mode == "EXACT_RECORD" + else identifier_exists + ) + classifier = ( + "START_REPLAY" if exact_replay else "START_CONFLICT" if identifier_exists else "START_FRESH" + ) + rules = [rule for rule in contract.rules if rule.classifier == classifier] + require(len(rules) == 1, f"Runtime start classification not singular: {classifier}") + rule = rules[0] + if rule.effect == "ADD_START": + current["starts"].append(deepcopy(start)) + return current, _result(contract, rule) + + +def relational_end_from_source( + state: dict[str, list[dict[str, Any]]], terminal: dict[str, Any], root: Path = ROOT +) -> tuple[dict[str, list[dict[str, Any]]], dict[str, Any]]: + contract = derive_runtime_contract(root) + if not _exact_terminal(contract, terminal): + raise ValueError("exact terminal record required") + current = _copy_state(state) + identifier_exists = _identifier_exists( + current["terminals"], terminal, contract.terminal_identifier_field + ) + exact_replay = ( + any(_terminal_equal(contract, item, terminal) for item in current["terminals"]) + if contract.terminal_replay_mode == "EXACT_RECORD" + else identifier_exists + ) + matching = _matching_start(contract, current, terminal) + if exact_replay: + classifier = "END_REPLAY" + elif identifier_exists: + classifier = "END_CONFLICT" + elif matching: + classifier = "END_RUNNING" + else: + classifier = "END_NOT_RUNNING" + rules = [rule for rule in contract.rules if rule.classifier == classifier] + if classifier == "END_RUNNING": + rules = [rule for rule in rules if rule.terminal_kind == terminal["terminal_kind"]] + require(len(rules) == 1, f"Runtime end classification not singular: {classifier}") + rule = rules[0] + if rule.effect == "ADD_TERMINAL": + current["terminals"].append(deepcopy(terminal)) + return current, _result(contract, rule) + + +def validate_runtime_relational_source(root: Path = ROOT) -> int: + contract = derive_runtime_contract(root) + return len(contract.rules) + + +def main() -> int: + try: + count = validate_runtime_relational_source(ROOT) + print(f"ALPHA4_RUNTIME_RELATIONAL_SOURCE_DERIVATIONS={count}/{count} PASS") + print("ALPHA4_RUNTIME_RELATIONAL_EXPRESSION=PASS") + return 0 + except (RelationalExpressionError, OSError, UnicodeError, ValueError, KeyError) as error: + print(f"ALPHA4_RUNTIME_RELATIONAL_EXPRESSION_ERROR={error}") + print("ALPHA4_RUNTIME_RELATIONAL_EXPRESSION=FAIL") + return 1 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/tools/alpha4_runtime_release_profiles.py b/tools/alpha4_runtime_release_profiles.py index 8bf324b..aaea1a7 100644 --- a/tools/alpha4_runtime_release_profiles.py +++ b/tools/alpha4_runtime_release_profiles.py @@ -4,6 +4,7 @@ import shutil from pathlib import Path +from tools.alpha4_runtime_manifest import parse_runtime_manifest from tools.alpha4_runtime_seed_extension import ( check_seed_companion_bases, parse_seed_binding, @@ -28,12 +29,8 @@ def _lines(path: Path) -> list[str]: def manifest_records(root: Path = ROOT) -> list[dict[str, str]]: - lines = _lines(root / "runtime/alpha4/RUNTIME.aset") - causal: dict[str, str] = {} - for line in lines: - if line.startswith("CAUSAL-BIND "): - _, component_id, causal_transition = line.split() - causal[component_id] = causal_transition + plan = parse_runtime_manifest(root) + causal = {item.component_id: item.causal_transition for item in plan.causal_bindings} operational_map = { "ASET-RUNTIME-COMPONENT-START-FRESH": "START-FRESH", "ASET-RUNTIME-COMPONENT-START-REPLAY": "START-REPLAY", @@ -44,25 +41,18 @@ def manifest_records(root: Path = ROOT) -> list[dict[str, str]]: "ASET-RUNTIME-COMPONENT-REJECT-END-CONFLICT": "REJECT-END-CONFLICT", "ASET-RUNTIME-COMPONENT-REJECT-END-NOT-RUNNING": "REJECT-END-NOT-RUNNING", } - records: list[dict[str, str]] = [] - for line in lines: - if not line.startswith("PAIR "): - continue - parts = line.split() - require(len(parts) == 6, f"bad PAIR declaration: {line}") - _, component_id, transition_binding, relational, _reflection, pairing = parts - require(component_id in causal, f"causal binding missing for {component_id}") - records.append( - { - "component_id": component_id, - "transition_binding": transition_binding, - "operational": operational_map[component_id], - "relational": relational, - "causal": causal[component_id], - "pairing": pairing, - "seed_extension": "PRESERVE-SEED-STATE", - } - ) + records = [ + { + "component_id": pair.component_id, + "transition_binding": pair.transition, + "operational": operational_map[pair.component_id], + "relational": pair.formal_operator, + "causal": causal[pair.component_id], + "pairing": pair.pairing_theorem, + "seed_extension": "PRESERVE-SEED-STATE", + } + for pair in plan.pairs + ] require(len(records) == 8, "Runtime release companion requires eight component records") return records @@ -192,7 +182,20 @@ def _exact_terminal(value: dict[str, Any]) -> bool: if not isinstance(value[field], str) or not value[field]: return False evidence = value["evidence_bindings"] - return isinstance(evidence, list) and all(isinstance(item, str) and item for item in evidence) + return ( + isinstance(evidence, list) + and all(isinstance(item, str) and item for item in evidence) + and len(evidence) == len(set(evidence)) + ) + + +def _terminal_equal(left: dict[str, Any], right: dict[str, Any]) -> bool: + if not _exact_terminal(left) or not _exact_terminal(right): + return False + scalar_fields = TERMINAL_FIELDS - {{"evidence_bindings"}} + return all(left[field] == right[field] for field in scalar_fields) and set( + left["evidence_bindings"] + ) == set(right["evidence_bindings"]) def _runtime_result(accepted: bool, code: str, changed: bool) -> dict[str, Any]: @@ -234,7 +237,7 @@ def end_attempt( same_id = [ item for item in next_runtime["terminals"] if item["attempt_id"] == terminal["attempt_id"] ] - if terminal in same_id: + if any(_terminal_equal(item, terminal) for item in same_id): return next_runtime, next_seed, _runtime_result(True, "IDEMPOTENT_REPLAY", False) if same_id: return next_runtime, next_seed, _runtime_result(False, "TERMINAL_ATTEMPT_IMMUTABLE", False) diff --git a/tools/alpha4_runtime_triangulated_expression.py b/tools/alpha4_runtime_triangulated_expression.py index 45e34fa..e0f5680 100644 --- a/tools/alpha4_runtime_triangulated_expression.py +++ b/tools/alpha4_runtime_triangulated_expression.py @@ -6,56 +6,82 @@ EXPECTED_CAUSAL_CONTRACTS, CausalNet, causal_end, + causal_exact_start, + causal_exact_terminal, causal_start, check_causal_bindings, ) +from tools.alpha4_runtime_manifest import parse_runtime_manifest from tools.alpha4_runtime_paired_expression import ( EXPECTED_STACK_EFFECTS, bounded_domain, + exact_start, + exact_terminal, + field_sensitivity_check, operational_end, operational_start, parse_operational_words, relational_end, relational_start, ) +from tools.alpha4_runtime_relational_expression import validate_runtime_relational_source ROOT = Path(__file__).resolve().parents[1] MANIFEST = ROOT / "runtime/alpha4/RUNTIME.aset" -def _manifest_lines() -> list[str]: - return [ - line.strip() for line in MANIFEST.read_text(encoding="utf-8").splitlines() if line.strip() - ] - - def check_representation_source_independence() -> dict[str, str]: - lines = _manifest_lines() - if "SEMANTIC-PRECEDENCE NONE" not in lines: - raise RuntimeError("Runtime semantic precedence drift") - for relation in ( - "RELATION OPERATIONAL_INTERFACE EXACT_STACK_EFFECT_CONTRACT", - "RELATION CAUSAL_CONTRACT CLOSED_WORLD_REQUIREMENT_EFFECT_OUTPUT_CONTRACT", - "RELATION OPERATIONAL_CAUSAL_RESULT OBSERVABLE_RESULT_CODE_CONGRUENCE", - ): - if relation not in lines: - raise RuntimeError(f"Runtime assurance relation missing: {relation}") - sources: dict[str, str] = {} - for line in lines: - tokens = line.split() - if tokens[0] in {"OPERATIONAL", "RELATIONAL", "CAUSAL-MODEL"}: - sources[tokens[0]] = tokens[1] - expected = {"OPERATIONAL", "RELATIONAL", "CAUSAL-MODEL"} - if set(sources) != expected: - raise RuntimeError(f"three-way Runtime source binding incomplete: {sources!r}") + plan = parse_runtime_manifest(ROOT) + sources = { + "OPERATIONAL": plan.operational, + "RELATIONAL": plan.relational, + "CAUSAL-MODEL": plan.causal_model, + } if len(set(sources.values())) != 3: raise RuntimeError(f"Runtime assurance representations share a source path: {sources!r}") + if plan.relation_map().get("RELATIONAL_SOURCE") != "BOUND_TLA_OPERATOR_DERIVATION": + raise RuntimeError("Runtime relational source derivation binding missing") for source in sources.values(): if not (ROOT / source).is_file(): raise RuntimeError(f"bound Runtime assurance source missing: {source}") return sources +def check_interface_validator_independence() -> int: + valid_start = { + "attempt_id": "a", + "attempt_digest": "d", + "runtime_binding": "r", + "descriptor_binding": "q", + } + valid_terminal = { + "attempt_id": "a", + "attempt_digest": "d", + "terminal_kind": "RESULT", + "terminal_digest": "t", + "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) + + def check_operational_causal_interface(net: CausalNet) -> tuple[int, int, int]: words = parse_operational_words() transitions = {item.symbol: item for item in net.transitions} @@ -73,8 +99,11 @@ def check_operational_causal_interface(net: CausalNet) -> tuple[int, int, int]: def check_triangulated_assurance() -> dict[str, object]: sources = check_representation_source_independence() + relational_derivations = validate_runtime_relational_source(ROOT) + validator_cases = check_interface_validator_independence() net = check_causal_bindings() stack_contracts, causal_contracts, result_bindings = check_operational_causal_interface(net) + sensitivity = field_sensitivity_check() starts, terminals, states = bounded_domain() start_checks = 0 end_checks = 0 @@ -128,6 +157,10 @@ def check_triangulated_assurance() -> dict[str, object]: "operational_stack_contracts": stack_contracts, "causal_closed_world_contracts": causal_contracts, "operational_causal_result_code_bindings": result_bindings, + "relational_source_derivations": relational_derivations, + "interface_validator_cases": validator_cases, + "identity_field_sensitivity": sensitivity["total"], + "evidence_set_order_invariance": sensitivity["evidence_set"], "start_checks": start_checks, "end_checks": end_checks, "total_checks": total_checks, @@ -145,6 +178,10 @@ def print_evidence(evidence: dict[str, object]) -> None: stacks = int(evidence["operational_stack_contracts"]) causal_contracts = int(evidence["causal_closed_world_contracts"]) result_bindings = int(evidence["operational_causal_result_code_bindings"]) + relational_derivations = int(evidence["relational_source_derivations"]) + validator_cases = int(evidence["interface_validator_cases"]) + sensitivity = int(evidence["identity_field_sensitivity"]) + evidence_set = int(evidence["evidence_set_order_invariance"]) print("ALPHA4_RUNTIME_ASSURANCE_REPRESENTATIONS=OPERATIONAL,RELATIONAL,CAUSAL") print("ALPHA4_RUNTIME_ASSURANCE_SEMANTIC_PRECEDENCE=NONE") print(f"ALPHA4_RUNTIME_OPERATIONAL_RELATIONAL_CONGRUENCE={total}/{total} PASS") @@ -160,6 +197,15 @@ def print_evidence(evidence: dict[str, object]) -> None: print( f"ALPHA4_RUNTIME_OPERATIONAL_CAUSAL_RESULT_CODES={result_bindings}/{result_bindings} PASS" ) + print( + "ALPHA4_RUNTIME_RELATIONAL_SOURCE_DERIVATIONS=" + f"{relational_derivations}/{relational_derivations} PASS" + ) + print( + f"ALPHA4_RUNTIME_INTERFACE_VALIDATOR_INDEPENDENCE={validator_cases}/{validator_cases} PASS" + ) + print(f"ALPHA4_RUNTIME_IDENTITY_FIELD_SENSITIVITY={sensitivity}/{sensitivity} PASS") + print(f"ALPHA4_RUNTIME_EVIDENCE_SET_ORDER_INVARIANCE={evidence_set}/{evidence_set} PASS") print("ALPHA4_RUNTIME_REPRESENTATION_SOURCE_INDEPENDENCE=PASS") print("ALPHA4_RUNTIME_TRIANGULATED_SEED_ACTION=STUTTER") print("ALPHA4_RUNTIME_TRIANGULATED_EXPRESSION=PASS") diff --git a/tools/run_alpha4_runtime_tlaps.py b/tools/run_alpha4_runtime_tlaps.py index 7ae5771..a1ea9ec 100644 --- a/tools/run_alpha4_runtime_tlaps.py +++ b/tools/run_alpha4_runtime_tlaps.py @@ -5,40 +5,66 @@ import subprocess from pathlib import Path +try: + from tools.alpha4_runtime_manifest import ProofBinding, parse_runtime_manifest +except ModuleNotFoundError: # direct ``python tools/...py`` execution + from alpha4_runtime_manifest import ProofBinding, parse_runtime_manifest + ROOT = Path(__file__).resolve().parents[1] -FORMAL = ROOT / "runtime/alpha4/formal" -MODULES = [ - FORMAL / "OperationalRelationalPairingProofs.tla", - FORMAL / "SeedBoundaryProofs.tla", -] + + +def _run_proof(tlapm: str, proof: ProofBinding) -> int: + module = ROOT / proof.module + formal = module.parent + print(f"ALPHA4_RUNTIME_TLAPS_PROOF={proof.proof_id}") + print(f"ALPHA4_RUNTIME_TLAPS_MODULE={proof.module}") + print(f"ALPHA4_RUNTIME_TLAPS_FINAL_THEOREM={proof.final_theorem}") + print(f"ALPHA4_RUNTIME_TLAPS_EXPECTED_OBLIGATIONS={proof.expected_obligations}") + result = subprocess.run( + [tlapm, "-I", str(formal), str(module)], + cwd=ROOT, + text=True, + stdout=subprocess.PIPE, + stderr=subprocess.STDOUT, + check=False, + ) + print(result.stdout, end="") + if result.returncode: + print(f"ALPHA4_RUNTIME_TLAPS_MODULE={module.name} FAIL") + return -1 + matches = re.findall(r"All ([0-9]+) obligations? proved\.", result.stdout) + if not matches: + print(f"ALPHA4_RUNTIME_TLAPS_MODULE={module.name} SUMMARY_MISSING") + return -1 + count = int(matches[-1]) + if count != proof.expected_obligations: + print( + f"ALPHA4_RUNTIME_TLAPS_MODULE={module.name} " + f"EXPECTED={proof.expected_obligations} ACTUAL={count} SCOPE_DRIFT" + ) + return -1 + print(f"ALPHA4_RUNTIME_TLAPS_MODULE={module.name} OBLIGATIONS={count} PASS") + return count def main() -> int: parser = argparse.ArgumentParser() parser.add_argument("--tlapm", required=True) args = parser.parse_args() + plan = parse_runtime_manifest(ROOT) total = 0 - for module in MODULES: - result = subprocess.run( - [args.tlapm, "-I", str(FORMAL), str(module)], - cwd=ROOT, - text=True, - stdout=subprocess.PIPE, - stderr=subprocess.STDOUT, - check=False, - ) - print(result.stdout, end="") - if result.returncode: - print(f"ALPHA4_RUNTIME_TLAPS_MODULE={module.name} FAIL") - return result.returncode - matches = re.findall(r"All ([0-9]+) obligations? proved\.", result.stdout) - if not matches: - print(f"ALPHA4_RUNTIME_TLAPS_MODULE={module.name} SUMMARY_MISSING") + expected_total = sum(proof.expected_obligations for proof in plan.proofs) + for proof in plan.proofs: + count = _run_proof(args.tlapm, proof) + if count < 0: + print("ALPHA4_RUNTIME_TLAPS=FAIL") return 1 - count = int(matches[-1]) total += count - print(f"ALPHA4_RUNTIME_TLAPS_MODULE={module.name} OBLIGATIONS={count} PASS") - print(f"ALPHA4_RUNTIME_TLAPS_OBLIGATIONS={total} PASS") + if total != expected_total: + print(f"ALPHA4_RUNTIME_TLAPS_OBLIGATIONS={total}/{expected_total} SCOPE_DRIFT") + print("ALPHA4_RUNTIME_TLAPS=FAIL") + return 1 + print(f"ALPHA4_RUNTIME_TLAPS_OBLIGATIONS={total}/{expected_total} PASS") print("ALPHA4_RUNTIME_TLAPS=PASS") return 0 diff --git a/tools/validate_alpha4_runtime.py b/tools/validate_alpha4_runtime.py index d84d796..4db02f2 100644 --- a/tools/validate_alpha4_runtime.py +++ b/tools/validate_alpha4_runtime.py @@ -3,6 +3,7 @@ from pathlib import Path from tools.alpha4_runtime_causal_expression import check_causal_bindings +from tools.alpha4_runtime_manifest import parse_runtime_manifest from tools.alpha4_runtime_paired_expression import EXPECTED_WORDS, parse_operational_words ROOT = Path(__file__).resolve().parents[1] @@ -23,6 +24,7 @@ def lines(path: Path) -> list[str]: def main() -> int: + plan = parse_runtime_manifest(ROOT) values = lines(MANIFEST) require( values[0] == "ASET-RUNTIME 1 ASET-RUNTIME-ALPHA4 0.1.0-alpha.4", @@ -83,6 +85,8 @@ def main() -> int: "Recognition remains local to Seed" in readme, "Runtime Seed authority boundary documentation missing", ) + print("ALPHA4_RUNTIME_BINDING_PLAN=PASS") + print(f"ALPHA4_RUNTIME_BINDING_PLAN_PROOFS={len(plan.proofs)}/{len(plan.proofs)} PASS") print("ALPHA4_RUNTIME_SUBJECT=PASS") print("ALPHA4_RUNTIME_COMPONENT_PAIRS=8/8 PASS") print("ALPHA4_RUNTIME_CAUSAL_BINDINGS=8/8 PASS") diff --git a/tools/validate_repository_minimal.py b/tools/validate_repository_minimal.py index 1d7b800..952a5ff 100644 --- a/tools/validate_repository_minimal.py +++ b/tools/validate_repository_minimal.py @@ -45,7 +45,9 @@ "tools/alpha4_runtime_causal_expression.py", "tools/alpha4_runtime_expression_airgap.py", "tools/alpha4_runtime_gate.py", + "tools/alpha4_runtime_manifest.py", "tools/alpha4_runtime_paired_expression.py", + "tools/alpha4_runtime_relational_expression.py", "tools/alpha4_runtime_public_release_audit.py", "tools/alpha4_runtime_release_admission.py", "tools/alpha4_runtime_release_gate.py",