Evaluating Logic-Based Policies via Fixpoints

In an earlier post, we argued that an agent-security policy is best expressed as a logic program. In particular, we expressed such a policy in Datalog. This declarative representation separated the policy’s intent from the machinery used to enforce it: the rules said what the policy meant without prescribing how an engine should evaluate them. A subsequent close read of two sasy-guard rules showed this representation in practice, including a rule that uses CurrentDepends to follow data through a session graph.

Those posts described the rules and what they enforce, but not how the engine applies them and reaches a verdict. We compressed this step into one phrase: the engine computes the rules. This post asks what that phrase entails. As an example, consider the recursive definition of CurrentDepends(src), which means that the current tool call depends on the session node src:

CurrentDepends(src) :- Current(id), Edge(src, id).
CurrentDepends(src) :- CurrentDepends(mid), Edge(src, mid).

The second rule uses CurrentDepends to derive more CurrentDepends facts. There is no loop, worklist, or visited set in the policy. Yet the engine must walk a dependency graph, terminate even when the graph has cycles, and return the same verdict regardless of rule order.

What, exactly, is the engine doing?

The session we already know

We will return to the four-node session from the compiled-logic post. A coding agent reads .env, writes the value into a script, and is now about to run an outbound curl. An edge points from each node to the node that used its data.

The pending call depends on the edit, which depends on the secret-bearing read. The policy engine receives this graph as facts.

The relevant facts are:

Edge("m1", "r1").
Edge("r1", "e1").
Edge("e1", "c1").
Current("c1").
ToolResult("r1", "Read", "{\"file_path\": \".env\"}").

Two classification facts are also part of the initial input:

SensitivePathIn("{\"file_path\": \".env\"}").
IsExfil("c1").

The first marks the Read arguments as referring to a sensitive path. The second marks the pending call c1 as an egress channel, meaning that it can send data out of the agent’s environment. Together, the five recorded facts and these two classification facts form the initial fact set $I_0$.

Current("c1") marks the call awaiting a verdict. The first CurrentDepends rule says that the current call depends on each of its direct parents. The second says that it also depends on the parents of anything it already depends on.

Question 1. Start with the initial fact set above. Which CurrentDepends fact can the engine derive immediately? Which one must wait for a later step?

Only CurrentDepends("e1") can appear immediately. The engine knows that c1 is current and has the fact Edge("e1", "c1"), so the first rule matches with src = "e1" and id = "c1".

CurrentDepends("r1") cannot appear yet. Its derivation needs CurrentDepends("e1") in the body of the recursive rule, and that fact was not present when the step began. This delay gives us the basic unit of evaluation: one step derives consequences from the facts known at the start of that step.

One update step

Let $I$ denote the set of facts currently known. The letter $I$ stands for an interpretation, the logician’s name for one candidate account of which facts are true.

For the positive Datalog program $P$ studied here, let $C_P(I)$ be the set of immediate consequences: all rule heads whose bodies match facts in $I$. Positive means that the rule bodies test only for facts that are present; they contain no negated conditions. For our first step, CurrentDepends("e1") belongs to $C_P(I)$.

The engine then performs an update:

$$U_P(I) = I \cup C_P(I).$$

This equation says: keep every fact already in $I$, and add every consequence the rules can derive from $I$. The union symbol $\cup$ means “everything from both sets.” Nothing is overwritten.

Question 2. Why include the old set $I$ in the update? Why not replace it with $C_P(I)$ and keep only the newly derived facts?

Replacement would make evaluation forget its own premises. After the first step, the engine would retain CurrentDepends("e1") but lose Current("c1") and the Edge facts that justified it. The next step could no longer continue the walk.

Union makes the state grow-only. Starting from the initial input $I_0$, the successive states are

$$I_1 = U_P(I_0), \qquad I_2 = U_P(I_1), \qquad I_3 = U_P(I_2), \ldots$$

Every state contains the one before it:

$$I_0 \subseteq I_1 \subseteq I_2 \subseteq \cdots$$

The symbol $\subseteq$ means “is a subset of.” This growing chain is the execution of the program.

Why more facts cannot undo a result

The update has another property. Suppose $I \subseteq J$, so $J$ contains every fact in $I$ and possibly some additional ones. Any positive rule body that matches in $I$ still matches in $J$. Therefore

$$U_P(I) \subseteq U_P(J).$$

A function with this property is called monotone. Giving a monotone rule engine more facts may enable more derivations, but it cannot invalidate an earlier one.

Question 3. Imagine that the graph contains a cycle: Edge("e1", "r1") as well as Edge("r1", "e1"). The recursive rule can now follow those two edges forever. Why does the evaluation still stop?

The rule may rediscover the same fact, but facts live in a set. Adding CurrentDepends("r1") to a set that already contains it changes nothing. Cycles can produce repeated justifications; they cannot produce endlessly many distinct facts.

Datalog also restricts rules so they cannot manufacture an unbounded stream of new values. A ground fact is a concrete fact with no variables. Because ordinary Datalog has no value-creating function symbols, its rules can only combine values already present in the finite input and policy. Only finitely many ground facts can therefore be formed, so a sequence that only grows inside that finite universe must eventually stop growing.

The point where nothing changes

Suppose evaluation reaches a set $I^*$ for which another update adds nothing:

$$U_P(I^*) = I^*.$$

The star is just a label for the settled state. A value unchanged by a function is called a fixpoint of that function. The engine has finished when the current fact set is a fixpoint of the update operator.

There may be many sets that satisfy all the rules. The engine chooses the least fixpoint: the smallest one containing the input facts and closed under the rules. “Least” matters because every derived fact must have a chain of rule applications back to the recorded session. The engine does not add facts merely because they would be consistent with the policy.

Question 4. Why should repeated updates from the input facts land on the least fixpoint rather than some larger fixpoint?

The process has no operation that can guess an unsupported fact. It begins with $I_0$ and adds only immediate consequences. After one step it contains the facts justified in one round; after two, those justified in at most two rounds. When the process stops, it contains every fact the rules can justify and nothing else. Any fixpoint containing the input must contain this entire chain, so none can be smaller than the result.

This is the mathematical meaning of a positive Datalog program: its least fixpoint on the input facts.

Watching the verdict form

The graph walk is only the first part of the policy. The following abridged rules connect the slice to a security decision:

InContext(id) :- Current(id).
InContext(id) :- CurrentDepends(id).

SensitiveInContext() :- InContext(id),
    ToolResult(id, "Read", args), SensitivePathIn(args).

Unauthorized(id) :- IsExfil(id), SensitiveInContext().

InContext names the current call and everything it depends on. SensitiveInContext() is a zero-argument fact, a yes-or-no flag saying that the slice contains a sensitive read. IsExfil("c1") says that the pending call is an egress channel. The final rule derives Unauthorized("c1") when both conditions hold.

For the seven input facts and the rules shown here, the updates look like this:

State	New facts added by the update
$I_1$	CurrentDepends("e1"), InContext("c1")
$I_2$	CurrentDepends("r1"), InContext("e1")
$I_3$	CurrentDepends("m1"), InContext("r1")
$I_4$	InContext("m1"), SensitiveInContext()
$I_5$	Unauthorized("c1")
$I_6$	nothing; $I_6 = I_5$

Question 5. The engine knows from the start that c1 is an egress channel. Why can it not derive Unauthorized("c1") in the first update?

The verdict rule needs both IsExfil("c1") and SensitiveInContext(). The second fact depends on the graph walk reaching r1, then on r1 entering InContext. Each update can use only facts present at its start, so the evidence travels through the rules one stage at a time.

Each wave is one update. The security verdict appears only after the dependency slice reaches the sensitive read.

The fixpoint is therefore more than a stopping condition. It is the point at which the policy has followed every relevant chain of consequences. Once Unauthorized("c1") appears, monotonicity makes an immediate denial safe. Only at the fixpoint, however, can its absence be treated as the policy’s final answer.

Why evaluation order does not choose the verdict

The table groups derivations into neat rounds. A compiled engine is free to schedule work differently: it may evaluate one rule before another, process several matches in parallel, or use an index to jump directly to relevant facts.

Question 6. Could two legal schedules settle on different verdicts? Could one derive Unauthorized("c1") while the other misses it?

For these positive rules, which test only for the presence of facts, no. Adding facts cannot invalidate an earlier match. In van Emden and Kowalski’s standard semantics, the least fixpoint defines the meaning of the logic program.¹¹ Maarten H. van Emden and Robert A. Kowalski, “The Semantics of Predicate Logic as a Programming Language,” Journal of the ACM 23, no. 4 (1976): 733-742. A fair schedule, meaning one that eventually considers every enabled rule application, cannot permanently miss a derivable fact. Every such schedule reaches that same fixpoint regardless of rule order. This schedule-independence is an instance of the standard convergence result for fair chaotic iteration²² Patrick Cousot and Radhia Cousot, “Abstract Interpretation and Application to Logic Programs,” Journal of Logic Programming 13, nos. 2-3 (1992): 103-179, Proposition 28.

This separation is useful. The least fixpoint defines what the policy means. Soufflé’s generated native code chooses how to reach it quickly. Changing indexes, parallelism, or rule order may change the route and runtime; it does not change the policy’s answer.

What the compiled engine can reuse

The round-by-round table specifies meaning, not an implementation algorithm. Soufflé uses semi-naive evaluation: after the first round, it focuses rule evaluation on facts added in the previous round instead of repeating every old match. This is the compiled counterpart of noticing that only new evidence can produce a new consequence.

Question 7. If semi-naive evaluation makes the engine faster, is it part of the policy’s meaning?

It is not. Another engine could recompute every match from scratch and still be correct if it reached the same least fixpoint. The semantics gives us a stable target against which any implementation can be checked. Compilation, indexes, parallel evaluation, and semi-naive evaluation are strategies for reaching that target before the waiting tool call notices the delay.

What the fixpoint buys the policy

We can now replace the phrase the engine computes the rules with a precise account. The engine starts from the recorded session and classification facts, adds consequences without retracting earlier facts, and stops at the least fixpoint. At that point every recursive dependency has been followed, every supported policy fact has been derived, and the presence or absence of Unauthorized("c1") has a defined meaning.

That is why the fixpoint matters to enforcement. A policy verdict is not the result of whichever rule happened to run first. For the positive rules studied here, it is a fact in the unique least fixpoint for the current session.

Further reading

• Agentic Security Policies as Compiled Logic: why the policy is written as Datalog and compiled in the first place.
• Guarding against hidden prompt injections and unvetted packages: two sasy-guard rule groups, including one that follows dependencies through the session graph.
• Formal Policy Enforcement for Real-World Agentic Systems: the FORGE framework, policy language, and enforcement contract.
• Soufflé: the Datalog engine SASY compiles policies with.
• Least-fixpoint semantics: van Emden and Kowalski’s account of the least fixpoint as the meaning of a positive logic program.
• Fair chaotic iteration: Cousot and Cousot’s treatment of chaotic iteration and least-fixpoint convergence.