assurance: derive Runtime bindings from declared sources

runtime/alpha4/RUNTIME.aset

@@ -40,20 +40,25 @@ 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
 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

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"

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"

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

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")