Cornerstone Engineering Monograph · UK Patent Pending

Rice's Theorem, Static ASTs, and Lengauer-Tarjan: Proving Compliance Dominance in CI/CD in Under 50ms

How Blockstate enforces a decidable Declarative Control Grammar via ast.parse ([Blockstate E014]) and runs the Lengauer-Tarjan dominator tree algorithm in under 50ms to prove compliance safety invariants.

1. The Verification Gap in Regulated Conversational AI

When an enterprise engineering team builds a conversational agent for retail banking wire transfers, mortgage origination, or insurance claims settlement, the deployment inevitably reaches a Model Risk Management (MRM) or Application Security review board.

The MRM auditor asks a deceptively simple question:

"Can you prove that there is no execution path through this agent from the initial greeting to faster_payments_uk, sepa_euro_transfer, or swift_international that bypasses step_up_mfa_kyc?"

In conventional LLM orchestration frameworks, engineering teams attempt to answer this question with empirical evaluation datasets: "We ran 1,000 red-team test prompts and the agent called step_up_mfa_kyc first in 98.4% of runs."

Under UK FCA SYSC 13.7 (Operational Risk Systems and Controls), Bank of England PRA SS1/23 (Model Risk Management Principles), and EU AI Act Articles 12 and 14, statistical evaluation pass rates do not constitute a deterministic technical control. A single refactor in a Pull Request can introduce an unauthenticated shortcut branch that standard prompt evaluations fail to exercise.

To prove path safety mathematically in Continuous Integration (CI/CD), we need a formal graph property: precursor dominance.

2. Why Rice's Theorem Forbids Unconstrained Dynamic Routing

In graph theory, given a directed Control Flow Graph (CFG) $G = (V, E, r)$ with entry root vertex $r \in V$, a vertex $u \in V$ dominates a vertex $v \in V$ (written $u \text{ dom } v$) if every path from $r$ to $v$ must contain $u$.

Before we can run a dominator algorithm on a Python agent class, we must first extract $G = (V, E, r)$ from the Python source code. Here we encounter Rice's Theorem (1953): any non-trivial semantic property of an arbitrary, unconstrained Turing-complete program is undecidable by static analysis.

If a Python developer writes state transitions using dynamic reflection or computed string targets:

# UNDECIDABLE BY STATIC ANALYSIS:
class UnsafeDynamicAgent:
    async def route_turn(self, user_tier: str) -> str:
        # Target depends on arbitrary runtime state and reflection
        handler = getattr(self, f"stage_{user_tier.lower()}")
        return await handler()

no static analyser can construct the exact edge set $E$ without executing the program across all possible inputs. Furthermore, importing and executing arbitrary module code inside a CI linter risks triggering database connections, external HTTP requests, or side effects.

3. The Declarative Control Grammar (DCG) & ast.parse ([Blockstate E014])

To make the Control Flow Graph 100% decidable and extractable without executing bytecode, Blockstate (src/blockstate/compiler/ast_extractor.py) defines a static Declarative Control Grammar (DCG) using @Stage, @Transition, and @Guard decorators paired with PEP 695 union return annotations.

When you run blockstate check agent.py, the compiler parses the source file into an Abstract Syntax Tree via Python's standard ast.parse and enforces three compile-time structural invariants (BLK-AST-014 / [Blockstate E014]):

1. No getattr Reflection in @Stage Methods: Any call to getattr(...) inside a @Stage method raises DynamicTransitionError (BLK-AST-014).
2. Compile-Time Non-Empty String Literal Targets: Every Transition.to(target) directive must pass a compile-time non-empty string literal constant (ast.Constant(value=str)). Variables, f-strings, and function call expressions inside Transition.to(...) are rejected immediately.
3. Zero Transitions Inside Data Validators: Any @field_validator method on a Pydantic model is inspected to verify that it contains zero Transition.* directives, keeping data validation strictly orthogonal to control flow.

$ blockstate check mortgage_flow.py
[Blockstate E014] Dynamic transition destination detected at mortgage_flow.py:42.
Transitions must reference static State definitions to enable Lengauer-Tarjan dominator verification.

Once static transition extraction completes, the compiler constructs $G = (V, E, r)$ by combining:

• Nominal @Transition(targets=...) edges; and
• Deterministic stage fallback edges (on_breach, on_refusal, on_max_turns_exceeded, on_security_violation).

It then executes a breadth-first search (BFS) from initial_stage ($r$) to verify that every declared @Stage in $V$ is reachable, raising BLK-AST-002 if any dead or orphaned stage exists.

flowchart TD
    subgraph CompileTime["Compile-Time Pipeline (blockstate check & verify)"]
        SRC["Python 3.12+ Agent Source Code"] --> AST["ast.parse Zero-Execution AST Extractor"]
        AST -->|"Rejects getattr & dynamic targets"| E014["Halt: [Blockstate E014] (BLK-AST-014)"]
        AST -->|"Valid DCG"| CFG["Construct Complete Directed CFG G = (V, E, r)<br/>Includes on_breach, on_refusal, on_max_turns_exceeded"]
        CFG --> BFS["BFS Reachability Verification from initial_stage"]
        BFS --> LT["LengauerTarjanSolver (dfnum, sdom, idom)<br/>Path-Compression Forest (_link, _eval, _compress)"]
        LT -->|"Violation Detected"| BYPASS["BFS Counterexample Synthesis in G \ {u}<br/>Exit Code 1 (BLK-AST-002)"]
        LT -->|"All Invariants Proven (<50ms)"| CERT["Emit Signed JSON / Mermaid Dominance Certificate"]
    end

4. Lengauer-Tarjan Dominator Tree Verification in <50ms

With a verified finite directed graph $G = (V, E, r)$, blockstate verify invokes LengauerTarjanSolver (src/blockstate/compiler/dominators.py).

While a naive dominator check removes each candidate vertex $u$ and runs a graph traversal in $\mathcal{O}(|V| \cdot |E|)$, the Lengauer-Tarjan algorithm computes the complete dominator tree for all vertices in $\mathcal{O}(|E| \alpha(|E|, |V|))$ time:

1. Depth-First Search Numbering (dfnum): A DFS from $r$ assigns discovery ranks dfnum[v], parent pointers, and vertex ordering.
2. Semidominator Computation (sdom): Processing vertices in reverse DFS order, the solver computes the semidominator sdom[w] for each vertex $w \neq r$ using a disjoint-set forest with path compression (_link, _eval, _compress).
3. Immediate Dominator Resolution (idom): A final pass resolves the immediate dominator idom[w] for every vertex, yielding the full reflexive dominator set $\text{Dom}(v)$ for every stage in the workflow.

Consider our multi-rail retail banking wire transfer agent:

from pydantic import BaseModel, Field
from blockstate import Agent, Stage, Transition, Guard, ChoicePayload, ChoiceOption

class TransferDetails(BaseModel):
    rail: str = Field(description="uk_faster | sepa_eur | swift_intl")
    amount_gbp: float = Field(gt=0, le=250_000)
    beneficiary_iban: str = Field(min_length=15, max_length=34)

class RetailWireTransferAgent(Agent):
    @Stage(name="select_payment_rail", initial=True, collect=TransferDetails)
    @Transition(targets=("step_up_mfa_kyc",))
    async def select_payment_rail(
        self, slots: TransferDetails
    ) -> Transition["step_up_mfa_kyc"]:
        return Transition.to("step_up_mfa_kyc")

    @Stage(
        name="step_up_mfa_kyc",
        tools=["verify_fido2_passkey"],
        max_turns=3,
        on_max_turns_exceeded="fraud_lock",
    )
    @Guard(requires=("user_id",))
    @Transition(targets=("faster_payments_uk", "sepa_euro_transfer", "swift_international", "fraud_lock"))
    async def step_up_mfa_kyc(
        self, slots: TransferDetails
    ) -> Transition["faster_payments_uk" | "sepa_euro_transfer" | "swift_international" | "fraud_lock"]:
        verified = await self.tools.verify_fido2_passkey(user_id=self.session["user_id"])
        if not verified:
            return Transition.to("fraud_lock")
        match slots.rail:
            case "uk_faster":
                return Transition.to("faster_payments_uk")
            case "sepa_eur":
                return Transition.to("sepa_euro_transfer")
            case _:
                return Transition.to("swift_international")

5. Counterexample Bypass Path Synthesis in $G \setminus \{u\}$

Suppose a developer modifies select_payment_rail in a Pull Request to route transfers under £10 directly to faster_payments_uk to reduce friction on small payments.

When blockstate verify runs in CI:

1. It checks whether step_up_mfa_kyc ($u$) belongs to $\text{Dom}(\text{faster\_payments\_uk})$.
2. Because select_payment_rail now has a direct edge to faster_payments_uk, idom["faster_payments_uk"] becomes "select_payment_rail". The dominance check fails.
3. The solver constructs the residual graph $G \setminus \{\text{step\_up\_mfa\_kyc}\}$ and executes a breadth-first search from select_payment_rail ($r$) to faster_payments_uk ($v$), outputting the exact shortest bypass path:

$ blockstate verify wire_agent.py \
    --dominates "step_up_mfa_kyc -> [faster_payments_uk, sepa_euro_transfer, swift_international]"

✖ [BLK-AST-002] DOMINATOR VIOLATION DETECTED
  Assertion:  step_up_mfa_kyc dom faster_payments_uk
  Status:     FAILED (Immediate dominator of 'faster_payments_uk' is 'select_payment_rail', not 'step_up_mfa_kyc')
  Counter-Example Bypass Path:
    [0] select_payment_rail (wire_agent.py:24)
    └──► [1] faster_payments_uk (wire_agent.py:49)  <-- BYPASSED 'step_up_mfa_kyc'
  Exit Code:  1

6. Try It Live & CI/CD Integration

You can test this exact Lengauer-Tarjan bypass synthesis in your browser using the Blockstate Interactive Dominator Simulator or install the CLI locally via pip install blockstate.

Statutory Notice: Blockstate is UK Patent Pending ("Process execution control system", UKIPO priority filing 28 October 2026, UK Patents Act 1977 s.62(1)) and distributed under a Source-Available Dual Licence (LICENSE & PATENTS.md): £0 Free for local development, academic research, CI/CD verification (blockstate verify), and 90-day enterprise staging evaluation; paid commercial licence required for live commercial production deployments.