Volume I — Chapter 4: Search and Backtracking

Textbook: Modern SWI-Prolog (2026 Edition): Sovereign Infrastructure & Industrial Logic Volume: I — Foundations of Sovereign Logic Chapter: 4 of 24 Audience: Senior Engineers, Systems Architects, Infrastructure Security Practitioners Prerequisites: Chapters 1–3 complete. WAM Heap, Trail, and Choice Point frame vocabulary established. proxmox_inventory.pl loaded at /opt/logic-node/kb/inventory/. Logic Node running.

Core Concepts

Prolog's execution model is not a function call graph. It is a search. Every query the engine receives is a problem statement — "find all substitutions for these variables that make this formula true" — and the engine's job is to explore the space of possible answers systematically. Understanding how it explores that space, what it remembers along the way, and what happens when it hits a dead end is not an academic exercise. It is the prerequisite for writing infrastructure logic that terminates correctly, uses bounded memory, and cannot be forced into pathological behaviour by adversarial input.

Five properties define SLD resolution and the choice point stack as engineering primitives.

1. SLD Resolution is a formal algorithm, not an interpreter loop. Selected Linear Definite clause resolution is the mathematical procedure underlying every Prolog query. Given a goal G and a KB of Horn clauses, SLD resolution selects a literal from G, finds all clauses whose head unifies with that literal, and for each such clause produces a new goal by replacing the selected literal with the clause's body. The process repeats until either the goal is empty (success) or no clause unifies (failure). The "selected" in SLD refers to the fact that the algorithm always picks the leftmost literal in the current goal — a deterministic selection rule that makes the search tree predictable and traceable.

2. The search tree is a concrete data structure, not a metaphor. Every branch point in an SLD resolution tree corresponds to a moment when more than one clause in the KB unifies with the current goal literal. At that moment, the WAM must commit to one branch and remember that the others exist. The data structure it uses to remember this is the Choice Point Frame — a record on the Local Stack capturing the complete execution state at the moment of the branch. The search tree is not drawn on paper; it lives in the WAM's Local Stack as a linked list of these frames.

3. A choice point is a memory obligation. Every choice point frame that the WAM creates costs memory on the Local Stack and adds entries to the Trail. A predicate that has exactly one matching clause for a given call creates no choice point — it is deterministic and leaves no memory obligation. A predicate that has three matching clauses creates a choice point frame that persists until all three alternatives are exhausted. For a Logic Node processing continuous infrastructure queries, non-determinism that is never resolved — predicates that leave open choice points on the stack — is a memory leak in the proof engine.

4. Backtracking is controlled, not accidental. When the engine exhausts one branch and backtracks, it does not "undo" work in the imperative sense. It restores the WAM's state to the last choice point frame by: resetting the argument registers, restoring the environment pointer, restoring the continuation pointer, rewinding the Trail (unbinding all variables bound since the choice point), and truncating the Heap to its state at the choice point. This is a precise, bounded operation. It is not an exception, not a setjmp/longjmp, not a restart. It is the WAM executing its built-in state restoration protocol.

5. Exhaustive search is a security surface. Depth-first search over a graph with cycles does not terminate without an explicit cycle-detection mechanism. A network topology encoded as a Prolog relation, queried with a recursive reachability predicate, will loop indefinitely on any topology containing a cycle — which is every real production network. This is not a hypothetical risk. It is a stack-overflow DoS vector that requires explicit engineering to close. The depth limit, visited-list, and tabling mechanisms (Chapter 16) are not optional features. They are correctness requirements for any recursive graph query in a production Logic Node.

Chapter Roadmap

Section	Title	Focus
4.1	The SLD Resolution Tree	SLD algorithm, search tree structure, branch/fail visualisation
4.2	Choice Points: The Memory of Alternatives	Frame layout, Trail interaction, determinism cost model
4.3	The Mechanics of Backtracking	Redo port, state restoration, Local Stack footprint
4.4	The Build: VLAN Reachability Tracer	`can_reach/2`, placement oracle, trace observation
4.5	Security Context: Stack Exhaustion	Left recursion, cycle detection, rbtrees, depth limits, `limit/2` Sovereign Ceiling
Outcome	From Boolean Logic to Solution Space	Verification checklist, conceptual transition

4.1 The SLD Resolution Tree

4.1.1 SLD Resolution: The Formal Foundation

The name encodes the algorithm precisely: Selected Literal Definite clause resolution.

Definite clause: a Horn clause with exactly one positive literal in its head — the form every Prolog fact and rule takes.
Selected literal: the algorithm always picks the leftmost goal in the current goal list — the selection function is fixed and deterministic.
Linear: each resolution step produces exactly one new goal list (the resolvent) by replacing the selected literal with a clause body.

The algorithm for a goal G and KB Π:

1. If G is empty: SUCCESS — the empty goal is trivially satisfied.
2. Select the leftmost literal L from G.
3. Find all clauses C in Π whose head H unifies with L under substitution σ.
4. If no such clause exists: FAIL — this branch is closed.
5. For each matching clause C_i with body B_i:
   a. Apply σ to (G with L replaced by B_i) to get new goal G_i.
   b. Recursively attempt to prove G_i.

Step 5 is where the tree branches. If three clauses match in step 3, the algorithm creates three independent resolution paths. The WAM implements this as depth-first search with backtracking: it commits to the first matching clause (leftmost in the KB), proceeds, and if that branch fails, backtracks to try the next matching clause.

The leftmost-literal selection rule has a security implication: if the first goal in a conjunction is expensive to prove, the engine does that expensive work even if a later, cheaper goal would immediately eliminate most candidates. Goal ordering is a performance and security control, not a stylistic preference.

4.1.2 Constructing the Search Tree

Consider the query: find all running VMs on pve-node-01.

% KB (from Chapter 3):
vm(100, 'nginx-prod-01',    'pve-node-01', running).
vm(101, 'postgres-prod-01', 'pve-node-01', running).
vm(102, 'nginx-prod-02',    'pve-node-02', running).
vm(103, 'worker-01',        'pve-node-02', stopped).
vm(104, 'monitoring-01',    'pve-node-03', running).
vm(105, 'orphan-vm-01',     'pve-node-99', running).

% Query:
?- vm(ID, Name, 'pve-node-01', running).

The selected literal is vm(ID, Name, 'pve-node-01', running). The engine checks each vm/4 clause in database order:

Clause 1 vm(100, 'nginx-prod-01', 'pve-node-01', running) — third argument pve-node-01 matches; fourth argument running matches. Unification succeeds. ID=100, Name='nginx-prod-01'. Goal list is now empty. SUCCESS (first solution).
Engine creates a choice point before committing to clause 1, recording clauses 2–6 as alternatives.
After the user presses ;, the engine backtracks to the choice point and tries Clause 2: vm(101, 'postgres-prod-01', 'pve-node-01', running) — matches. SUCCESS (second solution).
Clause 3: third argument pve-node-02 ≠ pve-node-01. Unification fails. FAIL — branch closed.
Clause 4: fourth argument stopped ≠ running. Unification fails. FAIL.
Clause 5: third argument pve-node-03 ≠ pve-node-01. FAIL.
Clause 6: third argument pve-node-99 ≠ pve-node-01. FAIL.
No more clauses. Overall query produces exactly two solutions.

4.1.3 Diagram: SLD Search Tree for VM Subnet Query

flowchart TD
    ROOT["<br/>Query:<br/>vm(ID, Name, 'pve-node-01', running)<br/>"]

    ROOT ---> C1["Unify with: vm(100,<br/> 'nginx-prod-01',<br/>'pve-node-01', running)"]
    ROOT ---> C2["Unify with: vm(101,<br/>vm(101, 'postgres-prod-01',<br/>'pve-node-01', running)"]
    ROOT ---> C3["Unify with: vm(102,<br/>vm(102, 'nginx-prod-02',<br/>'pve-node-02', running)"]
    ROOT ---> C4["Unify with: vm(103,<br/>vm(103, 'worker-01',<br/>'pve-node-02', stopped)"]
    ROOT ---> C5["Unify with: vm(104,<br/>vm(104, 'monitoring-01',<br/>'pve-node-03', running)"]
    ROOT ---> C6["Unify with: vm(105,<br/>vm(105, 'orphan-vm-01',<br/>'pve-node-99', running)"]

    C1 ---> S1["SUCCESS<br/>ID=100<br/>Name=nginx-prod-01"]
    C2 ---> S2["SUCCESS<br/>ID=101<br/>Name=postgres-prod-01"]
    C3 ---> F3["FAIL<br/>Node Mismatch"]
    C4 ---> F4["FAIL<br/>Node Mismatch"]
    C5 ---> F5["FAIL<br/>Node Mismatch"]
    C6 ---> F6["FAIL<br/>Node Mismatch"]

    S1 -->|"Choice point\nretains clauses 2–6"| CP["Choice Point Frame\nstored on Local Stack\nTrail mark: T₂"]
    S2 -->|"Choice point\nretains clauses 3–6"| CP2["Choice Point Frame\nstored on Local Stack\nTrail mark: T₄"]

    style S1 fill:#1A6B3A,color:#FFFFFF
    style S2 fill:#1A6B3A,color:#FFFFFF
    style F3 fill:#8B0000,color:#FFFFFF
    style F4 fill:#8B0000,color:#FFFFFF
    style F5 fill:#8B0000,color:#FFFFFF
    style F6 fill:#8B0000,color:#FFFFFF
    style CP fill:#4A235A,color:#FFFFFF
    style CP2 fill:#4A235A,color:#FFFFFF
    style ROOT fill:#1A2B4A,color:#FFFFFF

Reading the diagram: The root node is the initial query. Each branch corresponds to one clause in the KB being tried against the query literal. Clauses 1 and 2 produce successes; clauses 3–6 fail immediately on argument mismatch. The two purple choice point frames persist on the Local Stack while their respective solutions are presented to the user — they are not released until all alternatives in the branch are exhausted.

The WAM's JIT first-argument indexing (Chapter 2, Section 2.4.4) eliminates the failing branches before they are even tried: it indexes vm/4 by first argument and does not attempt clauses whose VM ID cannot match. But third-argument filtering (on HostName) requires either second-level indexing (if JIT has built it) or sequential traversal of all matching first-argument clauses. This asymmetry in indexing depth is why goal ordering matters for performance, which Section 4.5.3 addresses.

4.2 Choice Points: The Memory of Alternatives

4.2.1 The Choice Point Frame Layout

When the WAM encounters a predicate call that has more than one matching clause, it creates a choice point frame on the Local Stack before proceeding with the first matching clause. The frame is a snapshot of the execution state that is sufficient to restore the engine to exactly this moment if the chosen branch fails.

A WAM choice point frame contains the following fields:

Field	Contents	Restoration purpose
`n`	Number of argument registers at time of choice point	Restore argument registers A1–An
`A1…An`	Copies of argument registers	Restore the call arguments for retrying
`E`	Current environment frame pointer	Restore the current clause environment
`CP`	Continuation pointer	Restore the return address after this call
`B0`	Previous choice point pointer	Restore the choice point stack linkage
`BP`	Next clause pointer	The next clause to try on backtracking
`TR`	Trail pointer at choice point creation	Trail unwind boundary on backtracking
`H`	Heap (Global Stack) pointer at choice point	Heap truncation boundary on backtracking
`B`	Previous choice point (for stack linkage)	Re-link the choice point chain

The frame is allocated on the Local Stack, which grows downward (toward the Heap). Each frame is fixed in size for a given predicate arity — n argument registers means n+8 words per frame on a 64-bit system.

Local Stack layout with two active choice points:

High address (bottom of Local Stack)
│
│  [Choice Point Frame B₀]   ← oldest, from outermost non-det call
│    n=2, A1='pve-node-01', A2=running
│    E=env_ptr_0, CP=ret_addr_0
│    B0=null, BP=clause_ptr_3
│    TR=T₀, H=H₀
│
│  [Environment Frame]        ← clause execution frame
│
│  [Choice Point Frame B₁]   ← newest, from inner non-det call
│    n=4, A1=100, A2='nginx-prod-01', ...
│    E=env_ptr_1, CP=ret_addr_1
│    B0=B₀, BP=clause_ptr_2
│    TR=T₂, H=H₂
│
Low address (top of Local Stack, growing downward)

The BP (next clause pointer) field is updated each time the engine backtracks to this choice point and tries the next alternative. When BP has exhausted all alternatives for the predicate, the choice point frame is popped — this is the only time Local Stack space is recovered from a choice point.

4.2.2 The Trail Interaction

The Trail's mark field in the choice point frame (TR) is the most security-relevant component. Every variable binding made after the choice point was created is recorded on the Trail at addresses above TR. When the WAM backtracks to this choice point, it unwinds all Trail entries above TR, resetting those heap cells to unbound. This is what makes backtracking semantically clean: the heap state after backtracking is indistinguishable from the heap state before the failed branch was attempted.

The Heap truncation field H allows the WAM to recover heap memory allocated during the failed branch. All heap cells allocated above H at the time of choice point creation are reclaimed by resetting the heap pointer to H. Terms constructed during the failed branch — intermediate compounds, strings, new variable cells — evaporate.

Memory reclamation on backtrack to choice point B₁:

BEFORE backtrack:
  Trail top: T₅   (T₂ = choice point mark; T₂–T₅ are bindings to undo)
  Heap top:  H₆   (H₂ = choice point mark; H₂–H₆ are cells to reclaim)
  Local top: below B₁

DURING backtrack:
  1. Unwind Trail: reset cells at T₅, T₄, T₃, T₂+1 → all unbound
     Trail top restored to T₂
  2. Reset Heap pointer to H₂
     Terms allocated since B₁ are implicitly freed
  3. Restore argument registers A1…An from B₁ frame
  4. Restore E, CP from B₁ frame
  5. Set BP to next clause in B₁ (clause_ptr_2 → clause_ptr_3, etc.)
  6. Continue execution from CP with the restored registers

AFTER backtrack:
  Trail top: T₂   (exactly as it was when B₁ was created)
  Heap top:  H₂   (exactly as it was when B₁ was created)
  Execution: resuming from the continuation of the backtracked call,
             now trying the next alternative

4.2.3 Determinism: The Performance and Security Case

A deterministic predicate is one that, for any given call pattern, has at most one matching clause. The WAM can detect this statically (if the predicate has only one clause, or if first-argument indexing reduces the candidate set to one) or dynamically (if only one clause unifies during execution).

When the engine calls a deterministic predicate, it creates no choice point. No Local Stack frame is allocated. No Trail mark is stored. No BP field needs updating. The execution path is a straight line through the WAM's instruction sequence, as fast as any compiled function call.

The security dimension: a choice point frame that is never resolved — because the code path that would exhaust it is never reached — is a permanent Local Stack allocation for the life of that proof. Consider:

% Non-deterministic: leaves an open choice point after the first solution
host_has_issue(Host) :-
    vm(_, _, Host, error).    % Stops at first error VM; choice point persists
                               % for remaining vm/4 clauses

% Deterministic equivalent using aggregate:
host_has_any_error_vm(Host) :-
    aggregate_all(count, vm(_, _, Host, error), Count),
    Count > 0.                 % Single answer, no choice point

The first version leaves a choice point open for every unexhausted vm/4 alternative. If host_has_issue/1 is called within a larger query that itself has multiple choice points, the Local Stack accumulates frames proportionally. The second version is deterministic by design: aggregate_all/3 exhausts all solutions internally and produces a single count, no trailing choice points.

For the Logic Node, determinism is not just a performance goal. It is a memory-bounding property. A Logic Node processing 10,000 infrastructure queries per minute under the first pattern accumulates choice points at a rate proportional to the number of VMs per host times the depth of the proof tree. Under the second pattern, memory is constant per query regardless of topology size.

4.2.4 Measuring Choice Point Presence

SWI-Prolog provides direct introspection of the choice point stack:

% Check if the current execution has any open choice points
?- ( vm(_, Name, 'pve-node-01', running) ->
     format("First result: ~w~n", [Name]),
     format("Choice points may remain~n")
   ; true ).
First result: nginx-prod-01
Choice points may remain
true.
% The -> (if-then) cuts the choice point for the condition.
% But vm/4 itself left choice points before the -> was reached.

% Direct choice point depth introspection
?- nb_getval(choice_point_depth, N) ; N = unknown.
% (Non-standard — use statistics/2 for portable measurement)

?- statistics(choice_points_created, N).
N = 47.   % Total choice points created since session start

The deterministic/1 meta-predicate tests whether a goal leaves open choice points:

% From library(deterministic) — or implement directly
is_deterministic(Goal) :-
    \+ ( call(Goal), \+ deterministic ).

% More practically: use findall/3 and check list length
?- findall(N, vm(_, N, 'pve-node-01', running), Ns), length(Ns, Count).
Ns = ['nginx-prod-01', 'postgres-prod-01'],
Count = 2.
% findall/3 is always deterministic — it collects ALL solutions,
% leaves no choice points, and returns a list.

4.3 The Mechanics of Backtracking

4.3.1 The Redo Port

Chapter 2 introduced the four-port model (Call/Exit/Redo/Fail). The Redo port fires when the user presses ; in the REPL, or when an enclosing goal's failure forces the engine back to a previously exited predicate.

When a predicate exits with a solution, its choice point frame (if one was created) is not destroyed — it is suspended. The engine continues forward with the solution. If backtracking is later triggered, the engine returns to the choice point frame, updates BP to point to the next alternative clause, restores the saved state, and re-enters the predicate at the Redo port.

% Observing the Redo port with trace/0
?- trace.
true.

[trace]  ?- vm(_, Name, 'pve-node-01', running).
   Call: (11) vm(_A, _B, pve-node-01, running)
   Exit: (11) vm(100, nginx-prod-01, pve-node-01, running)
Name = 'nginx-prod-01' ;         % User presses ;

   Redo: (11) vm(_A, _B, pve-node-01, running)
   Exit: (11) vm(101, postgres-prod-01, pve-node-01, running)
Name = 'postgres-prod-01' ;      % User presses ;

   Redo: (11) vm(_A, _B, pve-node-01, running)
   Fail: (11) vm(_A, _B, pve-node-01, running)
false.

?- notrace.

The Redo port on line 3 is the WAM restoring the choice point frame for vm/4 and advancing BP to the next candidate clause. The trail is unwound for Name (which was bound to nginx-prod-01) and the argument registers are restored. The Fail on the third Redo confirms that clauses 3–6 all failed argument matching, leaving no further solutions.

4.3.2 Shallow Search vs. Deep Recursion

The Local Stack footprint of a proof is determined by the depth of the recursion and the number of open choice points at each level. These are independent dimensions with different resource profiles.

Shallow, wide search — a single predicate with many matching clauses (like vm/4 with six clauses):

Local Stack profile:
  One choice point frame (B₀) — created at the call
  One environment frame per clause tried
  Maximum depth: 2 frames
  Memory: O(clauses_tried × frame_size) — bounded, flat

Deep, recursive search — a recursive predicate like can_reach/2 traversing a network graph:

Local Stack profile at depth d:
  d environment frames (one per recursive call)
  Up to d choice point frames (one per branch in the graph)
  Maximum depth: O(graph_diameter) environment frames
  Memory: O(depth × (env_frame_size + choice_point_size))
  Risk: stack overflow at depth = stack_limit / frame_size

On a 64-bit system, an environment frame is approximately 5–8 words and a choice point frame is approximately 9–12 words. With SWI-Prolog's default 256MB stack limit, a pure left-recursive traversal of a graph with 100,000 nodes exhausts the Local Stack at approximately depth 4–5 million — well beyond any real network topology. The practical risk is not depth per se; it is cycles, which cause infinite recursion at any stack size.

4.3.3 Determinism After a Single Solution

A critical and frequently misunderstood property: a choice point created by a non-deterministic predicate is not automatically destroyed when the predicate produces its first solution. It persists until one of:

The proof explicitly exhausts all alternatives (all clauses tried, all failed)
A cut (!) is executed in the clause that succeeded — this destroys all choice points back to the nearest parent choice point
The predicate is wrapped in once/1, which commits to the first solution and destroys the choice point

% Choice point persists after first solution — memory held
first_vm_on_host(Host, VMName) :-
    vm(_, VMName, Host, running).   % Non-deterministic; choice point lives
                                     % until caller backtracks or proof ends

% Equivalent, deterministic — choice point destroyed after first solution
first_vm_on_host_det(Host, VMName) :-
    once(vm(_, VMName, Host, running)).  % once/1 commits; no trailing choice point

For a Logic Node, once/1 is the correct wrapper whenever only the first solution is needed and multiple solutions are known to exist. It is both a semantic declaration ("I only need one answer") and a memory management directive ("release the choice point after the first match").

4.4 The Build: VLAN Reachability Tracer

4.4.1 Network Topology KB Extension

Extend the Chapter 3 KB with a directed connectivity graph for VLAN routing. Create a new file:

logicadmin@logic-node-01:~$ nano /opt/logic-node/kb/networking/topology.pl

%% =============================================================================
%% FILE:    /opt/logic-node/kb/networking/topology.pl
%% PURPOSE: VLAN-level network connectivity facts for the Proxmox cluster.
%% Connectivity is directed: connected(A, B) means A can route to B.
%% For bidirectional links, assert both directions.
%% =============================================================================

:- module(topology, [connected/2, vlan_gateway/2, link_cost/3, vlan_isolation/2]).

%% connected(+From, +To)
%% Directed VLAN-level connectivity. "From can reach To in one hop."
%% Nodes are atoms: vlan_10, vlan_20, vlan_30, vlan_100, internet_gw, dmz_fw

connected(vlan_10,   vlan_20).      % Management → Production (controlled)
connected(vlan_20,   vlan_10).      % Production → Management (monitoring traffic)
connected(vlan_10,   vlan_30).      % Management → Storage backend
connected(vlan_30,   vlan_10).      % Storage → Management
connected(vlan_20,   vlan_100).     % Production → DMZ (outbound web)
connected(vlan_100,  dmz_fw).       % DMZ → Firewall
connected(dmz_fw,    internet_gw).  % Firewall → Internet gateway
connected(internet_gw, dmz_fw).     % Internet → Firewall (inbound)
connected(dmz_fw,    vlan_100).     % Firewall → DMZ (inbound reply traffic)
% Note: vlan_30 (storage) has NO path to vlan_100 (DMZ) — deliberate air gap

%% vlan_isolation/2 — Zero-Trust Policy Layer
%% vlan_isolation(+From, +To) is true when a path is PROHIBITED by policy,
%% regardless of whether connected(From, To) exists in the topology.
%%
%% Design principle: connected/2 describes physical/logical capability.
%% vlan_isolation/2 describes policy prohibition.
%% The reachability rules enforce: a path is valid only if it is connected
%% AND not isolated. connected/2 alone is insufficient for security decisions.
%%
%% If connected(A, B) exists AND vlan_isolation(A, B) exists,
%% the proof must fail-closed — policy beats topology.

vlan_isolation(vlan_30,  vlan_20).   % Storage must not reach production directly
vlan_isolation(vlan_30,  vlan_100).  % Storage must not reach DMZ under any path
vlan_isolation(vlan_100, vlan_10).   % DMZ must not reach management network
vlan_isolation(internet_gw, vlan_10). % Internet must not reach management

%% vlan_gateway(+VLAN, +GatewayNode)
%% The default gateway node for each VLAN segment

vlan_gateway(vlan_10,  'pve-mgmt-gw').
vlan_gateway(vlan_20,  'prod-router-01').
vlan_gateway(vlan_100, dmz_fw).

%% link_cost(+From, +To, +Cost)
%% Relative hop cost — used by path-cost queries in Chapter 10

link_cost(vlan_10,  vlan_20,  1).
link_cost(vlan_20,  vlan_10,  1).
link_cost(vlan_10,  vlan_30,  1).
link_cost(vlan_30,  vlan_10,  1).
link_cost(vlan_20,  vlan_100, 2).   % Production→DMZ has higher policy cost
link_cost(vlan_100, dmz_fw,   1).
link_cost(dmz_fw,   internet_gw, 3).
link_cost(internet_gw, dmz_fw, 3).
link_cost(dmz_fw,   vlan_100, 1).

4.4.2 The `can_reach/2` Predicate: Naive Implementation

logicadmin@logic-node-01:~$ nano /opt/logic-node/kb/networking/reachability.pl

%% =============================================================================
%% FILE:    /opt/logic-node/kb/networking/reachability.pl
%% PURPOSE: Network reachability rules — Version 1 (naive, cycle-unsafe).
%% WARNING: The naive implementation below (can_reach_unsafe/2) will loop
%%          on topologies containing cycles. Do NOT load into production
%%          without the safe variant (Section 4.5).
%% =============================================================================

:- module(reachability, [
    can_reach_unsafe/2,
    can_reach/3,
    can_reach/2,
    can_reach_policy_enforced/2,
    shortest_path/4,
    reachable_from/2
]).

:- use_module('/opt/logic-node/kb/networking/topology').

%% ---- UNSAFE VERSION (for pedagogic comparison only) ----

%% can_reach_unsafe(+From, +To)
%% Base case: directly connected in one hop.
can_reach_unsafe(From, To) :-
    connected(From, To).

%% Recursive case: reach To via an intermediate node C.
%% DANGEROUS: will loop if the topology contains any cycle (all real networks do).
can_reach_unsafe(From, To) :-
    connected(From, C),
    can_reach_unsafe(C, To).

%% ---- SAFE VERSION (production use) — see Section 4.5 for full explanation ----

%% can_reach(+From, +To, +Visited)
%% Visited is an accumulator list of already-visited nodes.
%% A node is not revisited if it is already in Visited.
%% This is the "visited list" pattern — O(depth) membership check.

can_reach(From, To, _Visited) :-
    connected(From, To).

can_reach(From, To, Visited) :-
    connected(From, C),
    \+ member(C, Visited),          % Cycle guard: C not already visited
    can_reach(C, To, [C|Visited]).  % Extend visited list at each hop

%% Convenience wrapper with empty initial visited list
can_reach(From, To) :-
    can_reach(From, To, [From]).

%% can_reach_policy_enforced(+From, +To)
%% Zero-trust reachability: a path from From to To is valid ONLY IF
%% connected(From, To) exists AND no vlan_isolation/2 fact prohibits any hop.
%%
%% Policy beats topology: if vlan_isolation(A, B) exists, the hop A→B is
%% refused even when connected(A, B) is asserted. This models zero-trust
%% correctly — capability and permission are separate facts; permission
%% is the authoritative filter.
%%
%% This predicate is the production default for all routing queries
%% on the Sovereign Node. can_reach/2 (topology-only) is reserved for
%% network diagnostic tools that need to see physical capability
%% independently of policy.

can_reach_policy_enforced(From, To) :-
    can_reach_policy_(From, To, [From]).

can_reach_policy_(From, To, _Visited) :-
    connected(From, To),
    \+ vlan_isolation(From, To).          % Policy check on direct hop

can_reach_policy_(From, To, Visited) :-
    connected(From, C),
    \+ vlan_isolation(From, C),           % Policy check on each intermediate hop
    \+ member(C, Visited),
    can_reach_policy_(C, To, [C|Visited]).

%% reachable_from(+From, -To)
%% Enumerate ALL nodes reachable from From (multi-solution, backtrackable).

reachable_from(From, To) :-
    can_reach(From, To, [From]).

4.4.3 REPL Exercise: Observing Choice Points During Network Search

Load the topology and reachability modules:

?- consult('/opt/logic-node/kb/networking/topology.pl').
true.
?- consult('/opt/logic-node/kb/networking/reachability.pl').
true.

Exercise 4.4.1: Basic reachability — single query

?- can_reach(vlan_10, internet_gw).
true.

?- can_reach(vlan_30, internet_gw).
false.
% Storage VLAN cannot reach the internet gateway — confirmed by topology.
% The CWA enforces the air gap: no connected/2 path exists.

?- can_reach(vlan_30, vlan_100).
false.
% Deliberate: storage_backend has no route to DMZ.

%% Zero-trust policy enforcement verification
%% Topology says vlan_20 → vlan_10 (production can reach management).
%% Policy says vlan_isolation(vlan_100, vlan_10) — DMZ cannot reach management.
%% These are independent facts; policy_enforced checks both.

?- connected(vlan_10, vlan_20).
true.   % Physical connectivity exists

?- vlan_isolation(vlan_100, vlan_10).
true.   % Policy prohibits this path

?- can_reach_policy_enforced(vlan_100, vlan_10).
false.  % Correctly refused — policy overrides topology

?- can_reach_policy_enforced(vlan_10, vlan_20).
true.   % Permitted — connected and no isolation fact

?- can_reach_policy_enforced(internet_gw, vlan_10).
false.  % Prohibited — vlan_isolation(internet_gw, vlan_10) exists

Exercise 4.4.2: All reachable nodes from vlan_10

?- findall(To, reachable_from(vlan_10, To), Targets).
Targets = [vlan_20, vlan_30, vlan_100, dmz_fw, internet_gw].
% Management VLAN reaches: production, storage, DMZ, firewall, internet.
% Note: internet_gw is reachable via multi-hop path through vlan_20 and dmz_fw.

Exercise 4.4.3: Trace a reachability proof to observe choice points

?- trace.
true.

[trace]  ?- can_reach(vlan_20, internet_gw, [vlan_20]).
   Call: (11) can_reach(vlan_20, internet_gw, [vlan_20])
   Call: (12) connected(vlan_20, internet_gw)
   Fail: (12) connected(vlan_20, internet_gw)
   Redo: (11) can_reach(vlan_20, internet_gw, [vlan_20])
   Call: (12) connected(vlan_20, _C)         % Branch point: multiple connected/2 clauses
   Exit: (12) connected(vlan_20, vlan_10)    % First match: hop to vlan_10
   Call: (12) \+ member(vlan_10, [vlan_20])  % Cycle guard: vlan_10 not yet visited
   Exit: (12) \+ member(vlan_10, [vlan_20])  % Passes — continue
   Call: (12) can_reach(vlan_10, internet_gw, [vlan_10, vlan_20])  % Recurse
   ...
   [engine backtracks through vlan_10 branch, eventually fails]
   Redo: (12) connected(vlan_20, _C)         % Try next: vlan_20 → vlan_100
   Exit: (12) connected(vlan_20, vlan_100)
   Call: (12) \+ member(vlan_100, [vlan_20])
   Exit: (12) \+ member(vlan_100, [vlan_20])
   Call: (12) can_reach(vlan_100, internet_gw, [vlan_100, vlan_20])
   Call: (13) connected(vlan_100, internet_gw)
   Fail: (13) connected(vlan_100, internet_gw)
   Redo: (13) can_reach(vlan_100, internet_gw, [vlan_100, vlan_20])
   Call: (13) connected(vlan_100, _C)
   Exit: (13) connected(vlan_100, dmz_fw)
   Call: (13) can_reach(dmz_fw, internet_gw, [dmz_fw, vlan_100, vlan_20])
   Call: (14) connected(dmz_fw, internet_gw)
   Exit: (14) connected(dmz_fw, internet_gw)
   Exit: (13) can_reach(dmz_fw, internet_gw, [dmz_fw, vlan_100, vlan_20])
   Exit: (12) can_reach(vlan_100, internet_gw, [vlan_100, vlan_20])
   Exit: (11) can_reach(vlan_20, internet_gw, [vlan_20])
true.

?- notrace.

The trace reveals the DFS path: vlan_20 → vlan_100 → dmz_fw → internet_gw. The initial attempt via vlan_10 is explored first (DFS commits to the leftmost connected/2 clause), eventually fails to reach internet_gw, and the engine backtracks to try the vlan_100 branch. This is SLD resolution in action: the trace is the search tree traversal.

4.4.4 Path Extraction

A reachability predicate that proves whether a path exists is useful for policy checks. One that returns what the path is is required for audit and explanation:

%% Add to reachability.pl

%% path(+From, +To, -Path, +Visited)
%% Path is the list of nodes from From to To, inclusive.

path(From, To, [From, To], _Visited) :-
    connected(From, To).

path(From, To, [From|Rest], Visited) :-
    connected(From, C),
    \+ member(C, Visited),
    path(C, To, Rest, [C|Visited]).

%% path/3 — convenience wrapper
path(From, To, Path) :-
    path(From, To, Path, [From]).

%% shortest_path(+From, +To, -Path, -Hops)
%% Finds the shortest path by enumerating all paths and selecting minimum length.
%% Uses findall/3 to collect all paths, then picks the shortest.
%% This is exhaustive — use only on bounded topologies.

shortest_path(From, To, ShortestPath, Hops) :-
    findall(P, path(From, To, P), AllPaths),
    AllPaths \= [],
    shortest_in_list(AllPaths, ShortestPath),
    length(ShortestPath, HopsPlusOne),
    Hops is HopsPlusOne - 1.

shortest_in_list([H], H).
shortest_in_list([H|T], Shortest) :-
    shortest_in_list(T, ShortestT),
    length(H, LH),
    length(ShortestT, LST),
    ( LH =< LST -> Shortest = H ; Shortest = ShortestT ).

?- path(vlan_10, internet_gw, Path).
Path = [vlan_10, vlan_20, vlan_100, dmz_fw, internet_gw] ;
% (other paths via backtracking, if the cycle guard allows them)
false.

?- shortest_path(vlan_10, internet_gw, Path, Hops).
Path = [vlan_10, vlan_20, vlan_100, dmz_fw, internet_gw],
Hops = 4.

4.4.5 The Placement Oracle: Multi-Solution VM Migration Query

The placement oracle answers the question: given a VM with a specific RAM requirement, which physical hosts are capable of running it? This is a multi-solution query — there may be zero, one, or many qualifying hosts.

%% Add to /opt/logic-node/kb/inventory/proxmox_rules.pl

%% find_placement(+VMName, -TargetHost, -AvailableRAM)
%% Returns all physical hosts with sufficient RAM to host the named VM.
%% VM's RAM requirement is stored in a vm_spec/2 fact (add to inventory):

%% vm_spec(+VMName, +RAM_Required_GB)
vm_spec('nginx-prod-01',    2).
vm_spec('postgres-prod-01', 16).
vm_spec('worker-01',        4).
vm_spec('monitoring-01',    8).

find_placement(VMName, TargetHost, HostRAM) :-
    vm_spec(VMName, Required),
    physical_host(TargetHost, _, HostRAM),
    HostRAM >= Required.

%% find_placement_excluding_current(+VMName, -TargetHost, -HostRAM)
%% Migration query: finds hosts that can take the VM but are not its current host.

find_placement_excluding_current(VMName, TargetHost, HostRAM) :-
    vm(_, VMName, CurrentHost, _),
    find_placement(VMName, TargetHost, HostRAM),
    TargetHost \= CurrentHost.

%% best_placement(+VMName, -BestHost)
%% The host with the most available RAM that can run the VM.
%% "Available" here means total RAM — a production version would subtract
%% the sum of RAM allocations for running VMs. That query is in Chapter 9.

best_placement(VMName, BestHost) :-
    findall(RAM-Host, find_placement(VMName, Host, RAM), Pairs),
    Pairs \= [],
    msort(Pairs, Sorted),
    last(Sorted, _-BestHost).

?- consult('/opt/logic-node/kb/inventory/proxmox_rules.pl').
true.

% All hosts that can run postgres-prod-01 (needs 16GB):
?- find_placement('postgres-prod-01', Host, RAM).
Host = 'pve-node-01', RAM = 256 ;
Host = 'pve-node-02', RAM = 128 ;
Host = 'pve-node-03', RAM = 256.
% All three hosts qualify — 16GB fits easily in 128GB or 256GB.

% Migration candidates for postgres-prod-01 (currently on pve-node-01):
?- find_placement_excluding_current('postgres-prod-01', Host, RAM).
Host = 'pve-node-02', RAM = 128 ;
Host = 'pve-node-03', RAM = 256.

% Best single placement target:
?- best_placement('postgres-prod-01', BestHost).
BestHost = 'pve-node-03'.
% pve-node-03 has 256GB — tied with pve-node-01, msort picks last of equal entries.

% All hosts that CANNOT run postgres-prod-01:
?- physical_host(Host, _, RAM), \+ find_placement('postgres-prod-01', Host, _).
false.
% None — all hosts exceed the 16GB requirement.

% Enumerate ALL placement solutions with findall (deterministic, no choice points):
?- findall(Host-RAM, find_placement('postgres-prod-01', Host, RAM), Placements).
Placements = ['pve-node-01'-256, 'pve-node-02'-128, 'pve-node-03'-256].

The placement oracle is a concrete example of the transition from "Boolean logic" (can this host run this VM? yes/no) to "exhaustive solution space" (which hosts can run this VM, and what are their properties?). find_placement/3 is non-deterministic by design — it is supposed to produce multiple answers. The choice points it leaves are semantically required and resolved either by the user's ; presses or by findall/3's internal exhaustion.

4.5 Security Context: Stack Exhaustion and Infinite Loops

4.5.1 Left Recursion and the Cycle Risk

The naive can_reach_unsafe/2 predicate from Section 4.4.2 fails catastrophically on any topology with cycles — and real networks have cycles by design. VLAN routing loops, redundant paths, and ring topologies are operational features that become existential threats to a recursive Prolog query without cycle detection.

The failure mode is stack overflow via infinite left recursion:

% Topology excerpt with a cycle:
connected(vlan_10, vlan_20).
connected(vlan_20, vlan_10).  % Cycle: 10 → 20 → 10 → 20 → ...

% Query that loops:
?- can_reach_unsafe(vlan_10, vlan_30).

% Execution trace (abbreviated):
% can_reach_unsafe(vlan_10, vlan_30)
%   connected(vlan_10, vlan_30)? FAIL
%   connected(vlan_10, C) → C = vlan_20
%     can_reach_unsafe(vlan_20, vlan_30)
%       connected(vlan_20, vlan_30)? FAIL
%       connected(vlan_20, C) → C = vlan_10
%         can_reach_unsafe(vlan_10, vlan_30)   ← SAME AS ROOT
%           ... recursion is now infinite ...

% ERROR: Stack limit (0.25Gb) exceeded
%        Stack sizes: local: 0.25Gb, global: 2.6Mb, trail: 0.6Mb

This is not merely a logical error — it is a resource exhaustion event. On SWI-Prolog with its default stack limit, this terminates with an ERROR: Stack limit exceeded exception. If the Logic Node handles this query in a service context where the exception is caught and logged but execution continues, the Local Stack has been exhausted and the WAM may be in an undefined state requiring a process restart.

If the Logic Node is accessible to external queries (via a REST interface built in Chapter 13, for example), a single malformed topology query containing a cycle reference can crash the inference service. This is a concrete, exploitable DoS vector.

4.5.2 The Visited List Pattern

The visited list pattern, shown in can_reach/3 in Section 4.4.2, prevents cycles at the cost of O(depth) membership checks per hop:

can_reach(From, To, _Visited) :-
    connected(From, To).

can_reach(From, To, Visited) :-
    connected(From, C),
    \+ member(C, Visited),        % O(|Visited|) check — linear scan
    can_reach(C, To, [C|Visited]).

The \+ member(C, Visited) check is O(n) in the current path length. For a topology with maximum diameter D, this means O(D²) membership operations in the worst case — quadratic in path length. For real network topologies where D is bounded by the number of VLANs (typically 4–20 for a datacenter cluster), this is negligible.

For larger topologies, replace the list with a lookup structure:

%% Efficient visited set using SWI-Prolog's nb_getval/nb_setval for
%% session-scoped mutable state — or use library(assoc) for a pure approach

:- use_module(library(assoc)).

can_reach_assoc(From, To) :-
    empty_assoc(Empty),
    put_assoc(From, Empty, visited, Visited0),
    can_reach_assoc_(From, To, Visited0).

can_reach_assoc_(From, To, _Visited) :-
    connected(From, To).

can_reach_assoc_(From, To, Visited) :-
    connected(From, C),
    \+ get_assoc(C, Visited, _),      % O(log n) AVL tree lookup
    put_assoc(C, Visited, visited, Visited1),
    can_reach_assoc_(C, To, Visited1).

The library(assoc) implementation uses AVL trees, giving O(log n) lookup instead of O(n) list scan. For a 500-node network graph, this reduces the per-hop overhead from 250 comparisons (average) to 9.

Scaling beyond 1,000 nodes — library(rbtrees): For network graphs exceeding 1,000 nodes, library(rbtrees) provides marginally better real-world performance than library(assoc) for the specific insert-and-check pattern of DFS visited tracking. Red-Black trees maintain tighter balance invariants than AVL trees, reducing worst-case rebalancing cost during the rapid sequential insertions that characterise a DFS path accumulator.

:- use_module(library(rbtrees)).

%% can_reach_rbtree(+From, +To)
%% Visited set implemented as an RB-tree for O(log n) insert and membership.

can_reach_rbtree(From, To) :-
    rb_empty(Empty),
    rb_insert(Empty, From, t, Visited0),
    can_reach_rbt_(From, To, Visited0).

can_reach_rbt_(From, To, _Visited) :-
    connected(From, To).

can_reach_rbt_(From, To, Visited) :-
    connected(From, C),
    \+ rb_lookup(C, _, Visited),          % O(log n) RB-tree lookup
    rb_insert(Visited, C, t, Visited1),   % O(log n) RB-tree insert
    can_reach_rbt_(C, To, Visited1).

Performance comparison for the insert-and-check pattern at varying graph sizes:

Graph nodes	List `member/2`	`library(assoc)` AVL	`library(rbtrees)` RB
20 (datacenter VLAN)	~10 ops	~4 ops	~4 ops
500	~250 ops	~9 ops	~9 ops
1,000	~500 ops	~10 ops	~10 ops
10,000	~5,000 ops	~13 ops	~13 ops

For the current Proxmox cluster topology (8–12 VLAN nodes), the list implementation is correct and the overhead is immeasurable. The assoc/rbtrees choice becomes material when the Logic Node's KB is extended to model host-level or service-mesh connectivity, where graph size routinely exceeds 1,000 nodes.

4.5.3 Depth Limiting as a Security Primitive

Even with cycle detection, a sufficiently large topology can produce a proof that exhausts the Local Stack through sheer depth. A depth limit is the explicit bound:

%% can_reach_bounded(+From, +To, +MaxDepth)
%% Fails if the path requires more than MaxDepth hops.
%% This is the correct production default for any recursive graph query.

can_reach_bounded(From, To, _Depth, _Visited) :-
    connected(From, To).

can_reach_bounded(_From, _To, 0, _Visited) :-
    !,
    fail.   % Depth exceeded — close this branch

can_reach_bounded(From, To, MaxDepth, Visited) :-
    MaxDepth > 0,
    connected(From, C),
    \+ member(C, Visited),
    Depth1 is MaxDepth - 1,
    can_reach_bounded(C, To, Depth1, [C|Visited]).

%% Production wrapper with configurable depth ceiling
%% Default 10 hops — sufficient for any real datacenter VLAN topology
can_reach_safe(From, To) :-
    can_reach_bounded(From, To, 10, [From]).

%% Configurable variant for policy-controlled depth
can_reach_policy(From, To, MaxHops) :-
    integer(MaxHops),
    MaxHops > 0,
    MaxHops =< 20,              % Hard ceiling — prevents unbounded calls
    can_reach_bounded(From, To, MaxHops, [From]).

% Verify depth limiting works:
?- can_reach_safe(vlan_10, internet_gw).
true.   % Reachable within 10 hops ✓

?- can_reach_bounded(vlan_10, internet_gw, 3, [vlan_10]).
false.  % Path is 4 hops — correctly fails at depth limit 3

?- can_reach_bounded(vlan_10, internet_gw, 4, [vlan_10]).
true.   % Path is exactly 4 hops — succeeds at limit 4

4.5.4 Goal Ordering as a Security Control

SLD resolution evaluates goals left to right. A conjunction A, B, C evaluates A first, and only if A succeeds does it attempt B. This creates a goal-ordering optimisation that is also a security control: expensive goals that depend on cheap goals for their input should always appear after the cheap goals that bind their arguments.

% INSECURE: bad goal ordering — filter runs too late
find_placement_bad(VMName, Host, RAM) :-
    physical_host(Host, _, RAM),          % Scans all hosts — binds Host and RAM
    vm_spec(VMName, Required),            % Single lookup
    RAM >= Required.                      % Filter after full expansion

% GENUINELY EXPENSIVE (bad ordering):
find_hosts_for_large_vms_bad(Host, VMName) :-
    physical_host(Host, _, RAM),          % Binds Host and RAM
    vm(_, VMName, _, running),            % Scans all VMs regardless of size
    vm_spec(VMName, Required),            % Lookup requirement
    Required > 100,                       % Filter: only large VMs
    RAM >= Required.

% SECURE (good ordering — filter before expanding):
find_hosts_for_large_vms(Host, VMName) :-
    vm_spec(VMName, Required),            % Get requirement first
    Required > 100,                       % Filter immediately — prunes early
    vm(_, VMName, _, running),            % Only then fetch VM record
    physical_host(Host, _, RAM),          % Then check hosts
    RAM >= Required.

The security implication: in the bad version, if there are 1,000 VMs and 3 hosts, the engine generates 3,000 (Host, VM) combinations before filtering on Required > 100. In the good version, the vm_spec/2 + Required > 100 filter runs first and reduces the VM set to, say, 20 large VMs, generating only 60 combinations. The difference is not just performance — it is the difference between a query that completes in milliseconds and one that takes 50x longer, which under adversarial load becomes a throughput DoS.

4.5.5 Stack Limit Configuration for the Logic Node

The WAM stack limits set in Chapter 1's /etc/swipl.rc apply to all queries. For a Logic Node running recursive graph queries, these defaults need explicit review:

% In /etc/swipl.rc — review and adjust for topology query workloads
% Default: stack_limit = 2GB (set in Chapter 1)
% For pure topology queries (bounded depth, no large data): 256MB is sufficient
% For large-topology KB with deep recursion: keep at 2GB

:- set_prolog_flag(stack_limit, 2_000_000_000).  % 2GB — Chapter 1 default

% Per-query timeout for service contexts (Chapter 13 covers the full service layer):
% :- set_prolog_flag(max_query_time, 30).  % 30 second hard limit per query

Monitoring Local Stack usage during development:

?- statistics(local_stack, [Used, Available]).
Used = 4096,
Available = 2147479552.
% After a complex recursive query:

?- findall(To, reachable_from(vlan_10, To), _Targets),
   statistics(local_stack, [Used, _]).
Used = 8192.
% Local stack usage for this topology: 8KB — well within bounds.
% For a 10,000-node topology, multiply by O(depth) — still manageable.

The local_stack statistic reports the current high-water mark of Local Stack usage. For production Logic Nodes, run the most complex expected queries during pre-deployment testing and record the peak local_stack value. Set stack_limit to 4–10× that value to provide safety margin without reserving unnecessary address space.

4.5.6 The Sovereign Ceiling: `limit/2` from `library(solution_sequences)`

Stack limits and depth counters protect the WAM from runaway recursion, but they operate at different levels — stack limits kill the process, depth counters require modifying the underlying predicates. library(solution_sequences) provides limit/2, which enforces a solution count ceiling on any goal without touching the goal's implementation.

:- use_module(library(solution_sequences)).

% limit(+N, +Goal)
% Succeeds for at most N solutions of Goal, then cuts.
% If Goal produces fewer than N solutions, limit/2 behaves as Goal.
% If Goal produces more, limit/2 cuts after the Nth solution.
% The underlying Goal's implementation is unchanged — limit/2 is a wrapper.

Applied to the placement oracle and reachability queries:

% Without limit: enumerates ALL placement candidates
% On a 10,000-host KB this could return thousands of results
?- find_placement('postgres-prod-01', Host, RAM).
Host = 'pve-node-01', RAM = 256 ;
Host = 'pve-node-02', RAM = 128 ;
Host = 'pve-node-03', RAM = 256.

% With Sovereign Ceiling: at most 5 placement candidates returned
% regardless of KB size — O(1) response time guarantee
?- limit(5, find_placement('postgres-prod-01', Host, RAM)).
Host = 'pve-node-01', RAM = 256 ;
Host = 'pve-node-02', RAM = 128 ;
Host = 'pve-node-03', RAM = 256.
% (Only 3 solutions exist — limit/2 is transparent when goal is under the ceiling)

% Enforcing a ceiling on reachable node enumeration
% Prevents a large topology from flooding an API response
?- limit(10, reachable_from(vlan_10, To)).
To = vlan_20 ;
To = vlan_30 ;
...  % At most 10 results; stops cleanly even on 1,000-node graphs

% Combining with findall for deterministic bounded collection
?- findall(H-R, limit(20, find_placement('postgres-prod-01', H, R)), Results).
Results = ['pve-node-01'-256, 'pve-node-02'-128, 'pve-node-03'-256].
% findall/3 exhausts the limited stream — always terminates, always bounded

limit/2 is the correct architectural primitive for the Logic Node's future HTTP service layer (Chapter 13), where every inbound query must have a guaranteed upper bound on result count and execution time. The pattern is:

%% Sovereign query wrapper — used in Chapter 13's HTTP handler
%% All externally-triggered queries are wrapped with both a time guard
%% and a solution count ceiling.

sovereign_query(Goal, MaxSolutions, Results) :-
    findall(
        solution,
        limit(MaxSolutions, call(Goal)),
        Results
    ).

The key property distinguishing limit/2 from a depth counter: it counts solutions delivered, not steps taken. A query that produces one solution after exploring 10,000 branches (a needle-in-a-haystack search) passes through limit(1, Goal) correctly — it takes one step of computation and returns. A depth counter would reject it prematurely if the path to the solution happened to be deep. limit/2 is semantically precise: it bounds the output, not the work.

Outcome: From Boolean Logic to Exhaustive Solution Space

4.6.1 The Conceptual Transition

Every chapter to this point has used predicates that answer "yes" or "no" — can_reach(A, B) either succeeds or fails. Chapter 4 establishes that this is a special case of a more general operation: Prolog queries over non-deterministic predicates produce not a boolean but a solution stream — a potentially infinite, lazily-evaluated sequence of substitutions. The engine commits to one solution, holds the rest in abeyance via choice points, and produces them on demand via backtracking.

Boolean / deterministic	Solution stream / non-deterministic
One answer: yes or no	Zero, one, or many answers
No choice points on completion	Choice points held open until stream exhausted
Memory: O(1) per query	Memory: O(open choice points × frame size)
`once/1` / first-argument indexing	`findall/3`, `bagof/3`, `;`
Correct for policy decisions ("is this allowed?")	Correct for enumeration ("what are all valid options?")
`physical_host('pve-node-01', _, _)`	`physical_host(Host, _, RAM)`

The Placement Oracle (Section 4.4.5) is the canonical demonstration: the question is not "can pve-node-01 run postgres?" but "enumerate every host that can run postgres, with their available RAM." The solution stream is the answer. findall/3 materialises it. The choice points are the mechanism.

4.6.2 Verification Checklist

SLD Resolution mechanics:

?- consult('/opt/logic-node/kb/networking/topology.pl').
true.
?- consult('/opt/logic-node/kb/networking/reachability.pl').
true.
?- consult('/opt/logic-node/kb/inventory/proxmox_rules.pl').
true.

% 1. Reachability: known-good path
?- can_reach(vlan_10, internet_gw).
true.

% 2. Reachability: confirmed air gap
?- can_reach(vlan_30, internet_gw).
false.

% 3. Path extraction
?- path(vlan_10, internet_gw, Path).
Path = [vlan_10, vlan_20, vlan_100, dmz_fw, internet_gw].

Choice point and backtracking mechanics:

% 4. Multi-solution enumeration
?- findall(H-R, find_placement('postgres-prod-01', H, R), Ps), length(Ps, N).
N = 3.   % Three valid hosts

% 5. Determinism: once/1 leaves no choice points
?- once(vm(_, Name, 'pve-node-01', running)), format("~w~n", [Name]).
nginx-prod-01
true.   % No ; prompt — choice points were cut by once/1

% 6. Solution stream exhaustion
?- aggregate_all(count, find_placement('worker-01', _, _), N).
N = 3.   % All three hosts qualify for 4GB requirement

Security — cycle and depth safety:

% 7. Cycle safety: topology contains cycles (vlan_10 ↔ vlan_20)
%    safe version terminates; unsafe version would loop
?- can_reach(vlan_20, vlan_30).   % Goes 20→10→30 — requires cycle traversal
true.

% 8. Depth limiting: 3-hop limit should reject the 4-hop path
?- can_reach_bounded(vlan_10, internet_gw, 3, [vlan_10]).
false.

% 9. Stack usage bounded after complex query
?- findall(To, reachable_from(vlan_10, To), _),
   statistics(local_stack, [Used, _]),
   format("Local stack peak: ~w bytes~n", [Used]).
Local stack peak: 8192 bytes.   % Bounded — no leak

All nine checks passing confirms the Logic Node's search engine is operating correctly with cycle-safe recursion, bounded depth, and deterministic solution collection.

4.6.3 What Comes Next

Chapter 5 introduces arithmetic and comparison predicates — the mechanism by which numeric constraints are evaluated during proof search. The placement oracle developed here (Section 4.4.5) relies on RAM >= Required; Chapter 5 examines precisely how this arithmetic comparison interacts with unification, why it is not a unification operation, and how to correctly mix arithmetic evaluation with relational queries without triggering instantiation errors.

Chapter Summary

Concept	Operational Definition	Security / Performance Consequence
SLD Resolution	Leftmost-literal selection, depth-first branch-and-fail	Predictable, traceable — but DFS commits to first branch regardless of cost
Search tree	WAM choice point frames on Local Stack	Each branching point costs one frame — frame count bounded by clause alternatives
Choice point frame	Snapshot of WAM state (A1…An, E, CP, B, TR, H)	TR and H fields define backtrack cost; large term construction amplifies H cost
Determinism	Single matching clause, no choice point created	Memory O(1) per call; performance of compiled function call
Non-determinism	Multiple matching clauses, choice point frame allocated	Memory O(n × frame) for n open alternatives; resolved by `;`, `findall`, or `once`
Backtrack / Redo port	Trail unwind to TR mark; Heap truncate to H mark; restore A-regs	Bounded, precise, deterministic cost — not an exception mechanism
`once/1`	Commits to first solution; destroys trailing choice points	Semantic declaration + memory directive — use whenever only one answer is needed
Visited list	Accumulates explored nodes; `\+ member/2` guards recursion	Prevents cycles at O(depth²) cost — acceptable for bounded topologies
Depth limit	Counter decremented at each recursive step; fails at 0	Hard bound on Local Stack depth; required for any recursive graph query in production
Goal ordering	Cheap/filtering goals placed leftmost in conjunctions	Early pruning reduces the search tree exponentially — security and performance control
`library(rbtrees)`	RB-tree visited set for DFS on large graphs	O(log n) insert-and-check vs O(n) list scan — material above 1,000 nodes
`vlan_isolation/2`	Policy prohibition predicate orthogonal to `connected/2`	Zero-trust model: capability and permission are separate facts; policy always wins
`limit/2`	Bounds solution count without modifying the goal	Sovereign Ceiling: O(1) response-count guarantee for any query regardless of KB size
`findall/3`	Exhausts all solutions; returns deterministic list	Always terminates for finite KBs; safe for solution enumeration

Exercises

Exercise 4.1 — SLD Tree Construction For the query find_placement('monitoring-01', Host, RAM), manually construct the SLD resolution tree showing all branches, which clauses are tried, and which succeed or fail. Verify your tree by running the query with trace/0 enabled and comparing the trace output to your diagram.

Exercise 4.2 — Choice Point Cost Measurement Write a predicate measure_choice_points(Goal, Before, After, Delta) that uses statistics/2 to capture the Local Stack usage before and after executing Goal. Run it against: vm(_, _, 'pve-node-01', running) (non-deterministic), once(vm(_, _, 'pve-node-01', running)) (deterministic), and findall(N, vm(_, N, 'pve-node-01', running), _) (deterministic collection). Compare and explain the Delta values.

Exercise 4.3 — Topology Extension and Cycle Detection Add two new connected/2 facts to topology.pl that create a second cycle (for example, vlan_30 → vlan_20 and vlan_20 → vlan_30). Verify that can_reach_unsafe/2 loops on a query that traverses this cycle. Verify that can_reach/3 with the visited list terminates correctly and finds the path if one exists.

Exercise 4.4 — Depth Limit Calibration For the current topology, determine the minimum depth limit required for can_reach_bounded/4 to find all reachable nodes from vlan_10. Write a predicate minimum_required_depth(From, To, Depth) that discovers this value by trying can_reach_bounded with increasing depth limits from 1 upward. Explain the security tradeoff between a tight depth limit and a generous one.

Exercise 4.5 — Production Placement Oracle Extend find_placement/3 to account for current RAM allocation: a host's effective available RAM is its total RAM minus the sum of vm_spec/2 requirements for all VMs currently running on it. Write find_placement_realistic(+VMName, -Host, -EffectiveRAM) using aggregate_all/3 to compute the used RAM per host. Test it with the current inventory and explain which hosts drop out of the placement pool when realistic allocation is considered.