From ac8421cb4bfe3693e58a801c851ca8aa4a4b05a2 Mon Sep 17 00:00:00 2001 From: Dzmitry Prychyna Date: Mon, 17 Aug 2026 15:30:32 -0300 Subject: [PATCH] assurance: enforce closed-world operational causal contracts --- runtime/alpha4/RUNTIME.aset | 3 + ...test_alpha4_runtime_three_way_assurance.py | 52 ++++++- tools/alpha4_runtime_causal_expression.py | 131 ++++++++++++++++++ tools/alpha4_runtime_paired_expression.py | 33 ++++- .../alpha4_runtime_triangulated_expression.py | 40 ++++++ 5 files changed, 253 insertions(+), 6 deletions(-) diff --git a/runtime/alpha4/RUNTIME.aset b/runtime/alpha4/RUNTIME.aset index 2c4cb02..8f4a55f 100644 --- a/runtime/alpha4/RUNTIME.aset +++ b/runtime/alpha4/RUNTIME.aset @@ -50,6 +50,9 @@ CHECK TRIANGULATED_EXPRESSION tools/alpha4_runtime_triangulated_expression.py RELATION OPERATIONAL_RELATIONAL BOUNDED_OPERATIONAL_RELATIONAL_CONGRUENCE RELATION OPERATIONAL_CAUSAL BOUNDED_OPERATIONAL_CAUSAL_CONGRUENCE +RELATION OPERATIONAL_INTERFACE EXACT_STACK_EFFECT_CONTRACT +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 diff --git a/tests/test_alpha4_runtime_three_way_assurance.py b/tests/test_alpha4_runtime_three_way_assurance.py index 94e80aa..c4e457c 100644 --- a/tests/test_alpha4_runtime_three_way_assurance.py +++ b/tests/test_alpha4_runtime_three_way_assurance.py @@ -1,6 +1,16 @@ from __future__ import annotations -from tools.alpha4_runtime_causal_expression import check_causal_bindings +from pathlib import Path + +import pytest + +from tools.alpha4_runtime_causal_expression import ( + CausalExpressionError, + check_causal_bindings, + parse_causal_net, + validate_causal_contract, +) +from tools.alpha4_runtime_paired_expression import parse_operational_words from tools.alpha4_runtime_triangulated_expression import ( check_representation_source_independence, check_triangulated_assurance, @@ -25,6 +35,9 @@ def test_three_way_assurance_covers_complete_bounded_domain() -> None: assert evidence["start_checks"] == 484 assert evidence["end_checks"] == 1936 assert evidence["total_checks"] == 2420 + assert evidence["operational_stack_contracts"] == 8 + assert evidence["causal_closed_world_contracts"] == 8 + assert evidence["operational_causal_result_code_bindings"] == 8 assert evidence["pairwise_relations"] == { "operational_relational": "PASS", "operational_causal": "PASS", @@ -33,3 +46,40 @@ def test_three_way_assurance_covers_complete_bounded_domain() -> None: assert evidence["representation_source_independence"] == "PASS" assert evidence["seed_action"] == "STUTTER" assert evidence["status"] == "PASS" + + +def _mutated_source(tmp_path: Path, source: Path, old: str, new: str) -> Path: + target = tmp_path / source.name + text = source.read_text(encoding="utf-8") + assert old in text + target.write_text(text.replace(old, new, 1), encoding="utf-8") + return target + + +def test_runtime_operational_stack_contract_rejects_missing_start(tmp_path: Path) -> None: + source = Path("runtime/alpha4/operational/components.forth") + mutated = _mutated_source( + tmp_path, source, "( state start -- state result )", "( state -- state result )" + ) + with pytest.raises(RuntimeError, match="stack contract mismatch"): + parse_operational_words(mutated) + + +def test_runtime_causal_effect_surface_rejects_unbound_extra_effect(tmp_path: Path) -> None: + source = Path("runtime/alpha4/causal/components.petri") + mutated = _mutated_source( + tmp_path, source, "EFFECT ADD_START", "EFFECT ADD_START\nEFFECT DESTROY_STATE" + ) + net = parse_causal_net(mutated) + with pytest.raises(CausalExpressionError, match="causal effect contract drift"): + validate_causal_contract(net) + + +def test_runtime_causal_output_surface_rejects_wrong_result_code(tmp_path: Path) -> None: + source = Path("runtime/alpha4/causal/components.petri") + mutated = _mutated_source( + tmp_path, source, "OUTPUT CODE ATTEMPT_STARTED", "OUTPUT CODE WRONG_CODE" + ) + net = parse_causal_net(mutated) + with pytest.raises(CausalExpressionError, match="causal output contract drift"): + validate_causal_contract(net) diff --git a/tools/alpha4_runtime_causal_expression.py b/tools/alpha4_runtime_causal_expression.py index e682466..af7bbc7 100644 --- a/tools/alpha4_runtime_causal_expression.py +++ b/tools/alpha4_runtime_causal_expression.py @@ -42,6 +42,133 @@ class CausalNet: transitions: tuple[CausalTransition, ...] +EXPECTED_CAUSAL_CONTRACTS: dict[str, tuple[str, frozenset[str], frozenset[str], dict[str, str]]] = { + "START-FRESH": ( + "ASET-RUNTIME-COMPONENT-START-FRESH", + frozenset({"EXACT_START", "FRESH_ID"}), + frozenset({"ADD_START"}), + { + "ACCEPTED": "TRUE", + "CODE": "ATTEMPT_STARTED", + "STATE_CHANGED": "TRUE", + "SEED_ACTION": "STUTTER", + "SEED_EFFECT": "FALSE", + }, + ), + "START-REPLAY": ( + "ASET-RUNTIME-COMPONENT-START-REPLAY", + frozenset({"EXACT_START", "EXACT_START_REPLAY"}), + frozenset({"PRESERVE_STATE"}), + { + "ACCEPTED": "TRUE", + "CODE": "IDEMPOTENT_REPLAY", + "STATE_CHANGED": "FALSE", + "SEED_ACTION": "STUTTER", + "SEED_EFFECT": "FALSE", + }, + ), + "REJECT-START-CONFLICT": ( + "ASET-RUNTIME-COMPONENT-REJECT-START-CONFLICT", + frozenset({"EXACT_START", "START_CONFLICT"}), + frozenset({"PRESERVE_STATE"}), + { + "ACCEPTED": "FALSE", + "CODE": "ATTEMPT_IDENTITY_CONFLICT", + "STATE_CHANGED": "FALSE", + "SEED_ACTION": "STUTTER", + "SEED_EFFECT": "FALSE", + }, + ), + "END-RESULT": ( + "ASET-RUNTIME-COMPONENT-END-RESULT", + frozenset({"EXACT_TERMINAL", "EXACT_RUNNING", "FRESH_TERMINAL", "KIND_RESULT"}), + frozenset({"ADD_TERMINAL"}), + { + "ACCEPTED": "TRUE", + "CODE": "ATTEMPT_ENDED_WITH_RESULT", + "STATE_CHANGED": "TRUE", + "SEED_ACTION": "STUTTER", + "SEED_EFFECT": "FALSE", + }, + ), + "END-NO-RESULT": ( + "ASET-RUNTIME-COMPONENT-END-NO-RESULT", + frozenset({"EXACT_TERMINAL", "EXACT_RUNNING", "FRESH_TERMINAL", "KIND_NO_RESULT"}), + frozenset({"ADD_TERMINAL"}), + { + "ACCEPTED": "TRUE", + "CODE": "ATTEMPT_ENDED_WITH_NO_RESULT", + "STATE_CHANGED": "TRUE", + "SEED_ACTION": "STUTTER", + "SEED_EFFECT": "FALSE", + }, + ), + "END-REPLAY": ( + "ASET-RUNTIME-COMPONENT-END-REPLAY", + frozenset({"EXACT_TERMINAL", "EXACT_TERMINAL_REPLAY"}), + frozenset({"PRESERVE_STATE"}), + { + "ACCEPTED": "TRUE", + "CODE": "IDEMPOTENT_REPLAY", + "STATE_CHANGED": "FALSE", + "SEED_ACTION": "STUTTER", + "SEED_EFFECT": "FALSE", + }, + ), + "REJECT-END-CONFLICT": ( + "ASET-RUNTIME-COMPONENT-REJECT-END-CONFLICT", + frozenset({"EXACT_TERMINAL", "TERMINAL_CONFLICT"}), + frozenset({"PRESERVE_STATE"}), + { + "ACCEPTED": "FALSE", + "CODE": "TERMINAL_ATTEMPT_IMMUTABLE", + "STATE_CHANGED": "FALSE", + "SEED_ACTION": "STUTTER", + "SEED_EFFECT": "FALSE", + }, + ), + "REJECT-END-NOT-RUNNING": ( + "ASET-RUNTIME-COMPONENT-REJECT-END-NOT-RUNNING", + frozenset({"EXACT_TERMINAL", "NO_TERMINAL_FOR_ID", "NOT_EXACT_RUNNING"}), + frozenset({"PRESERVE_STATE"}), + { + "ACCEPTED": "FALSE", + "CODE": "ATTEMPT_NOT_RUNNING", + "STATE_CHANGED": "FALSE", + "SEED_ACTION": "STUTTER", + "SEED_EFFECT": "FALSE", + }, + ), +} + + +def validate_causal_contract(net: CausalNet) -> int: + actual = {item.symbol: item for item in net.transitions} + require( + set(actual) == set(EXPECTED_CAUSAL_CONTRACTS), + "Runtime causal transition surface drift", + ) + for symbol, (component_id, requirements, effects, outputs) in EXPECTED_CAUSAL_CONTRACTS.items(): + transition = actual[symbol] + require( + transition.component_id == component_id, + f"{symbol}: causal component identity drift", + ) + require( + frozenset(transition.requirements) == requirements, + f"{symbol}: causal requirement contract drift", + ) + require( + frozenset(transition.effects) == effects, + f"{symbol}: causal effect contract drift", + ) + require( + transition.output_map() == outputs, + f"{symbol}: causal output contract drift", + ) + return len(EXPECTED_CAUSAL_CONTRACTS) + + def _lines(path: Path) -> list[str]: return [line.strip() for line in path.read_text(encoding="utf-8").splitlines() if line.strip()] @@ -94,6 +221,9 @@ def parse_causal_net(path: Path = CAUSAL) -> CausalNet: raise CausalExpressionError(f"{symbol}: unsupported statement {body[0]}") index += 1 require(index < len(lines) and lines[index] == "END", f"{symbol}: END missing") + require(len(set(requirements)) == len(requirements), f"{symbol}: duplicate requirement") + require(len(set(effects)) == len(effects), f"{symbol}: duplicate effect") + require(len({key for key, _ in outputs}) == len(outputs), f"{symbol}: duplicate output") transitions.append( CausalTransition( symbol=symbol, @@ -127,6 +257,7 @@ def check_causal_bindings() -> CausalNet: net = parse_causal_net() actual = {item.component_id: item.symbol for item in net.transitions} require(actual == manifest_bindings(), "causal component binding mismatch") + validate_causal_contract(net) for transition in net.transitions: outputs = transition.output_map() require(outputs.get("SEED_ACTION") == "STUTTER", f"{transition.symbol}: Seed action drift") diff --git a/tools/alpha4_runtime_paired_expression.py b/tools/alpha4_runtime_paired_expression.py index 74ea445..cefc2b6 100644 --- a/tools/alpha4_runtime_paired_expression.py +++ b/tools/alpha4_runtime_paired_expression.py @@ -60,6 +60,17 @@ ), } +EXPECTED_STACK_EFFECTS = { + "START-FRESH": (("state", "start"), ("state", "result")), + "START-REPLAY": (("state", "start"), ("state", "result")), + "REJECT-START-CONFLICT": (("state", "start"), ("state", "result")), + "END-RESULT": (("state", "terminal"), ("state", "result")), + "END-NO-RESULT": (("state", "terminal"), ("state", "result")), + "END-REPLAY": (("state", "terminal"), ("state", "result")), + "REJECT-END-CONFLICT": (("state", "terminal"), ("state", "result")), + "REJECT-END-NOT-RUNNING": (("state", "terminal"), ("state", "result")), +} + START_FIELDS = {"attempt_id", "attempt_digest", "runtime_binding", "descriptor_binding"} TERMINAL_FIELDS = { "attempt_id", @@ -72,14 +83,26 @@ TERMINAL_KINDS = {"RESULT", "NO_RESULT"} -def parse_operational_words() -> dict[str, tuple[str, ...]]: - text = FORTH.read_text(encoding="utf-8") - pattern = re.compile(r":\s+(?P[A-Z0-9-]+)\s+\([^)]*--[^)]*\)\s+(?P.*?)\s*;") - words = { - match.group("word"): tuple(match.group("body").split()) for match in pattern.finditer(text) +def parse_operational_words(path: Path = FORTH) -> dict[str, tuple[str, ...]]: + text = path.read_text(encoding="utf-8") + pattern = re.compile( + r":\s+(?P[A-Z0-9-]+)\s+" + r"\(\s*(?P.*?)\s*--\s*(?P.*?)\s*\)\s+" + r"(?P.*?)\s*;" + ) + matches = list(pattern.finditer(text)) + words = {match.group("word"): tuple(match.group("body").split()) for match in matches} + stacks = { + match.group("word"): ( + tuple(match.group("inputs").split()), + tuple(match.group("outputs").split()), + ) + for match in matches } if words != EXPECTED_WORDS: raise RuntimeError(f"restricted operational vocabulary mismatch: {words!r}") + if stacks != EXPECTED_STACK_EFFECTS: + raise RuntimeError(f"restricted operational stack contract mismatch: {stacks!r}") return words diff --git a/tools/alpha4_runtime_triangulated_expression.py b/tools/alpha4_runtime_triangulated_expression.py index 0caa125..45e34fa 100644 --- a/tools/alpha4_runtime_triangulated_expression.py +++ b/tools/alpha4_runtime_triangulated_expression.py @@ -3,14 +3,18 @@ from pathlib import Path from tools.alpha4_runtime_causal_expression import ( + EXPECTED_CAUSAL_CONTRACTS, + CausalNet, causal_end, causal_start, check_causal_bindings, ) from tools.alpha4_runtime_paired_expression import ( + EXPECTED_STACK_EFFECTS, bounded_domain, operational_end, operational_start, + parse_operational_words, relational_end, relational_start, ) @@ -29,6 +33,13 @@ 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() @@ -45,9 +56,25 @@ def check_representation_source_independence() -> dict[str, str]: return sources +def check_operational_causal_interface(net: CausalNet) -> tuple[int, int, int]: + words = parse_operational_words() + transitions = {item.symbol: item for item in net.transitions} + if set(words) != set(transitions): + raise RuntimeError("Runtime operational/causal transition surface mismatch") + result_bindings = 0 + for symbol, body in words.items(): + operational_code = body[-1].replace("-", "_") + causal_code = transitions[symbol].output_map()["CODE"] + if operational_code != causal_code: + raise RuntimeError(f"{symbol}: operational/causal result-code mismatch") + result_bindings += 1 + return len(EXPECTED_STACK_EFFECTS), len(EXPECTED_CAUSAL_CONTRACTS), result_bindings + + def check_triangulated_assurance() -> dict[str, object]: sources = check_representation_source_independence() net = check_causal_bindings() + stack_contracts, causal_contracts, result_bindings = check_operational_causal_interface(net) starts, terminals, states = bounded_domain() start_checks = 0 end_checks = 0 @@ -98,6 +125,9 @@ def check_triangulated_assurance() -> dict[str, object]: "operational_causal": "PASS", "relational_causal": "PASS", }, + "operational_stack_contracts": stack_contracts, + "causal_closed_world_contracts": causal_contracts, + "operational_causal_result_code_bindings": result_bindings, "start_checks": start_checks, "end_checks": end_checks, "total_checks": total_checks, @@ -112,6 +142,9 @@ def print_evidence(evidence: dict[str, object]) -> None: start = int(evidence["start_checks"]) end = int(evidence["end_checks"]) total = int(evidence["total_checks"]) + stacks = int(evidence["operational_stack_contracts"]) + causal_contracts = int(evidence["causal_closed_world_contracts"]) + result_bindings = int(evidence["operational_causal_result_code_bindings"]) 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") @@ -120,6 +153,13 @@ def print_evidence(evidence: dict[str, object]) -> None: print(f"ALPHA4_RUNTIME_TRIANGULATED_START={start}/{start} PASS") print(f"ALPHA4_RUNTIME_TRIANGULATED_END={end}/{end} PASS") print(f"ALPHA4_RUNTIME_TRIANGULATED_TOTAL={total}/{total} PASS") + print(f"ALPHA4_RUNTIME_OPERATIONAL_STACK_CONTRACTS={stacks}/{stacks} PASS") + print( + f"ALPHA4_RUNTIME_CAUSAL_CLOSED_WORLD_CONTRACTS={causal_contracts}/{causal_contracts} PASS" + ) + print( + f"ALPHA4_RUNTIME_OPERATIONAL_CAUSAL_RESULT_CODES={result_bindings}/{result_bindings} PASS" + ) print("ALPHA4_RUNTIME_REPRESENTATION_SOURCE_INDEPENDENCE=PASS") print("ALPHA4_RUNTIME_TRIANGULATED_SEED_ACTION=STUTTER") print("ALPHA4_RUNTIME_TRIANGULATED_EXPRESSION=PASS")