Chapter 6: Control Flow and The Cut (!)

Textbook: Modern SWI-Prolog (2026 Edition): Sovereign Infrastructure & Industrial Logic Volume: I — Foundations of Sovereign Logic Chapter: 6 of 24 Audience: Senior Engineers, Systems Architects, Infrastructure Security Practitioners Prerequisites: Chapters 1–5 complete. SLD resolution, choice point frames, Trail mechanics, and the LFCG oracle pattern operational. proxmox_inventory.pl, zfs_oracle.pl, and proxmox_oracle.pl loaded at /opt/logic-node/. logicadmin user active.

Core Concepts

Backtracking is Prolog's correctness mechanism: it exhausts all proof paths, guaranteeing that every solution is found. For general logic programming this is a virtue. For infrastructure control predicates — where a predicate must produce exactly one answer, where "trying alternatives" is not exploration but ambiguity, and where the first-matching security rule must be the only rule that fires — unrestricted backtracking is a defect. The cut operator (!) is the mechanism by which a Prolog predicate commits to the branch it has chosen and severs the alternatives it will never need.

The cut is the most operationally significant control primitive in Prolog after unification itself. It is also the most misused. The difference between a cut that improves performance without changing semantics and a cut that fundamentally changes what a predicate means is the difference between an optimisation and a design decision — and confusing the two produces predicates whose behaviour under backtracking is impossible to reason about.

Five properties define the cut as a commitment and resource reclamation mechanism.

1. The cut is a WAM instruction that destroys choice points. When the WAM executes !, it removes all choice point frames created since the most recent parent choice point — the choice point that was active when the predicate containing the cut was called. Those frames are gone: the alternatives they encoded are permanently discarded. The WAM's Local Stack reclaims the memory. The Trail entries associated with those frames are released. The cut does not merely skip alternatives — it makes them unreachable.

2. Commitment is irreversible within the predicate. Once execution passes a cut in a clause, that clause is committed. If the remainder of the clause fails, the engine does not backtrack into the alternatives that the cut destroyed. It backtracks to the parent choice point — the level above the predicate that contained the cut. The cut's scope is precisely: "among the clauses of this predicate, I have chosen this one. There will be no others." Everything outside this predicate is unaffected.

3. Green cuts reclaim resources without changing semantics. A green cut is placed in a clause whose remaining alternatives would all fail anyway if tried — the cut merely tells the WAM to stop looking. The predicate with the green cut and the predicate without it produce identical solution sets. The difference is stack depth, Trail size, and execution time. Green cuts are optimisations. They can be added or removed without changing the logical meaning of any query that uses the predicate.

4. Red cuts change what the predicate means. A red cut encodes logic that cannot be expressed without the cut. The classic form: a predicate whose second clause is a "fallback" that should only fire when the first clause's condition was not satisfied. Without the cut, both clauses can fire. With the cut in the first clause, the second fires only when the first was never reached. The cut is load-bearing: removing it changes the predicate's semantics. Red cuts must be identified, documented, and treated with the same rigour as any other security-critical branch.

5. Negation as failure is a cut in disguise. \+ Goal succeeds if Goal cannot be proven. Its implementation is: attempt Goal; if it succeeds, cut and fail; if it fails, succeed. The cut inside \+ destroys the choice points created during the attempted proof of Goal. This means \+ is always a red cut operation — it changes semantics, not merely performance. And it carries a specific unsafety: if Goal contains unbound variables, the negation may succeed vacuously ("I cannot prove anything about this unbound variable, therefore \+ succeeds") when the intended meaning was "this entity does not satisfy this condition."

Chapter Roadmap

Section	Title	Focus
6.1	The Cut: Architectural Pruning	WAM mechanics, Local Stack reclamation, commitment scope
6.2	Green vs. Red Cuts: The Security Line	Semantics-preserving vs. semantics-changing, `must_be/2` post-cut assertion
6.3	Negation as Failure as a Guard Dog	`\+` safety, groundness requirement, CWA relationship
6.4	The Build: HA Migration Pre-flight	`can_migrate/2`, fail-fast cuts, Node Health Oracle, `setup_call_cleanup/3`
6.5	Reclaiming the Local Stack	Trail debt, choice point destruction, determinism patterns
Outcome	The Pruned Logic Model	Verification checklist, conceptual transition

6.1 The Cut: Architectural Pruning

6.1.1 The Cut as a WAM Instruction

The cut is written as ! and appears as a goal within a clause body. As a goal, it always succeeds — but its side effect is the destruction of all choice points created since the parent choice point of the predicate currently being executed.

To be precise about scope: when the WAM calls predicate p, it records the current choice point as B_parent. If p has multiple clauses, the WAM creates a choice point B_p before trying the first clause. When ! executes inside a clause of p, it sets the current choice point back to B_parent — effectively making B_p and any choice points created after it unreachable for garbage collection. All alternatives for p and for any goals between the call to p and the ! are destroyed.

% Anatomy of cut scope:
parent_predicate :-
    first_goal,          % May create choice points — CPs survive the cut
    p(X),               % <-- B_parent is the active choice point at this call
    second_goal.        % Continues after p/1 succeeds

p(X) :-
    condition_a(X),     % Creates choice point B_p_1 for condition_a alternatives
    !,                  % Destroys B_p_1 and all choice points for p's clauses
    action_a(X).        % If this fails: backtracks to B_parent (NOT to condition_a)

p(X) :-
    action_b(X).        % This clause is NEVER reached after ! in first clause

The cut's scope is confined to the predicate it appears in. It does not affect choice points in first_goal, second_goal, or condition_a that were created before p/1 was called. Those choice points remain intact and are reachable by any backtracking that goes above p/1.

6.1.2 Memory Reclamation: What the WAM Does

When the cut executes, the WAM performs the following sequence:

B_cut = B_parent  (set current choice point to the parent level)

For each choice point frame F between B_p and B_current:
  1. The frame is no longer reachable from the active choice point chain
  2. The heap pointer reset value stored in F (H field) is no longer needed
  3. Trail entries between F.TR and the current Trail top are examined:
     — Variable bindings made AFTER B_parent that are still needed remain on Trail
     — The Trail mark in B_parent governs what gets unwound on eventual backtrack
  4. Local Stack space occupied by F is eligible for reclamation
     once no environment frames above F hold references to F

The reclamation is not always immediate — the Local Stack grows downward, and a frame cannot be freed until all frames above it are also freed. But the choice points are logically gone: no backtracking path leads to them. The memory they occupy becomes a "dead zone" in the Local Stack that is reclaimed when the current clause frame exits. For deep chains of non-deterministic calls, a strategically placed cut can release megabytes of Local Stack in a single instruction.

6.1.3 Diagram: Pruned SLD Search Tree

The following diagram shows an SLD tree for a classify_host/2 predicate that uses a cut to commit to the first matching classification. Without the cut, all three clauses would be candidates. With the cut in the first clause, once high_memory/1 succeeds and the cut fires, clauses 2 and 3 are permanently pruned.

%%{init: {"themeVariables": {"fontSize": "18px"}}}%%
flowchart TD
    ROOT["Query: classify_host('pve-node-01', Class)"]

    ROOT --->|"Try clause 1"| C1["Clause 1:\nhigh_memory(Host), !, Class = tier_1"]
    ROOT --->|"Try clause 2 ?"| C2["Clause 2:\nmedium_memory(Host), !, Class = tier_2"]
    ROOT --->|"Try clause 3 ?"| C3["Clause 3:\nClass = tier_3"]

    C1 --->|"high_memory('pve-node-01')\nRAM=256 >= 200 ✓"| CUT["! executes\nChoice points for\nclauses 2 & 3\nDESTROYED"]
    C1 --->|"Without cut:\nclauses 2 & 3\nremain available"| NCUT["Choice Point B_p\nretains clauses 2,3\n(no cut variant)"]

    CUT --->|"Class = tier_1\nUnifies"| S1["SUCCESS\nClass = tier_1\n\nLocal Stack reclaimed:\nB_p frame + alternatives\nreleased"]

    C2 --->|"PRUNED by !\nnever reached"| P2["PRUNED\n(dashed — unreachable\nafter cut fires)"]
    C3 --->|"PRUNED by !\nnever reached"| P3["PRUNED\n(dashed — unreachable\nafter cut fires)"]

    NCUT --->|"clause 2 still\nreachable on ;"| ALT["Alternative solutions\nstill on stack\n(no-cut: memory held)"]

    style ROOT fill:#1A2B4A,color:#FFFFFF
    style CUT fill:#8B6914,color:#FFFFFF
    style S1 fill:#1A6B3A,color:#FFFFFF
    style P2 fill:#4A4A4A,color:#AAAAAA
    style P3 fill:#4A4A4A,color:#AAAAAA
    style NCUT fill:#5A1A1A,color:#FFFFFF
    style ALT fill:#5A1A1A,color:#FFFFFF
    style C1 fill:#1A3A6A,color:#FFFFFF
    style C2 fill:#3A3A3A,color:#AAAAAA
    style C3 fill:#3A3A3A,color:#AAAAAA

Reading the diagram: The gold node is the cut instruction. Left branch (blue): with the cut, clause 1 fires, cut destroys the alternatives for clauses 2 and 3, and Class = tier_1 is the sole result. Right branch (dark red): without the cut, the choice point B_p retains references to clauses 2 and 3, which remain available via backtracking — classify_host/2 would produce all three tier classifications if backtracked exhaustively.

6.2 Green vs. Red Cuts: The Security Line

6.2.1 Green Cuts: Performance Without Semantic Change

A green cut is placed in a clause where the engine would never succeed at any remaining alternative even if it tried. The cut tells the WAM to stop looking — but the answer set is unchanged. The predicate is still logically equivalent to its cut-free version; it just executes faster and with less memory.

The canonical green cut pattern: membership testing when only the first match matters.

% Non-deterministic member — backtracks through all occurrences
member_nd(X, [X|_]).
member_nd(X, [_|T]) :- member_nd(X, T).

% Green-cut member — stops at first occurrence
% (semantics identical for "does X appear in the list?" queries)
memberchk(X, [X|_]) :- !.
memberchk(X, [_|T]) :- memberchk(X, T).

memberchk/2 and member_nd/2 produce the same answer for the query memberchk(running, [running, stopped, running]) — true. But memberchk/2 creates no choice points: the cut in the first clause fires immediately on the first match and destroys the alternative that would have found the second running. For the Logic Node's security policy checks — "is this status in the permitted set?" — only the boolean answer matters. The cut is green: it changes performance but not meaning.

Green cuts are safe to add, safe to remove, and safe to refactor. They require no special documentation beyond a comment noting that the cut is a performance optimisation.

% Infrastructure examples of green cuts:

% Checking if a VM is in a live state — first match is sufficient
vm_is_live(VMID) :-
    vm(VMID, _, _, Status),
    memberchk(Status, [running, suspended]),
    !.   % Green cut: any additional matching vm/4 clauses are irrelevant

% host_tier/2 — first-argument indexed, but cut removes residual choice points
host_tier(Host, Tier) :-
    physical_host(Host, _, RAM),
    ram_to_tier(RAM, Tier),
    !.   % Green cut: physical_host/3 produces exactly one result per host

ram_to_tier(RAM, tier_1) :- RAM >= 200, !.
ram_to_tier(RAM, tier_2) :- RAM >= 64,  !.
ram_to_tier(_,   tier_3).

6.2.1.1 Post-Cut Groundness Enforcement with `must_be/2`

A green cut commits the WAM to a branch. What it does not do is verify that the variables produced by that branch are in the state the downstream logic requires. In a clause where a cut fires after a pattern match, the variables bound by that match are ground by construction — but compound terms, derived bindings, and outputs computed by called predicates may not be. A downstream goal that receives an unbound variable fails silently, and in a deterministic (cut) predicate that failure propagates upward with no diagnostic information about which variable was uninstantiated and why.

error:must_be/2 from library(error) converts that silent failure into a typed, catchable exception at the exact point of the violation:

:- use_module(library(error)).

%% must_be(+Type, +Term)
%% Throws type_error(Type, Term) if Term is not of Type.
%% Throws instantiation_error if Term is unbound.
%% Types relevant to oracle predicates:
%%   ground    — Term contains no unbound variables
%%   atom      — Term is an atom
%%   integer   — Term is an integer
%%   positive_integer — Term is an integer > 0
%%   string    — Term is a Prolog string

The pattern: after a cut commits to a branch and binds outputs, assert the type requirements of every output variable before passing them to downstream logic.

%% host_tier/2 — green cut with post-cut groundness assertion
host_tier(Host, Tier) :-
    must_be(atom, Host),              % Precondition: Host must be ground atom
    physical_host(Host, _, RAM),
    must_be(positive_integer, RAM),   % Postcondition: KB fact is well-formed
    ram_to_tier(RAM, Tier),
    !,                                % Green cut: commit to first tier match
    must_be(atom, Tier).              % Postcondition: Tier was bound by ram_to_tier/2

%% access_decision/3 — red cut with must_be on committed output
access_decision(VMID, _Op, deny) :-
    must_be(positive_integer, VMID),  % Precondition: VMID must be instantiated
    vm(VMID, _, _, error),
    !,                                % RED CUT: error → deny, unconditional
    true.   % Output 'deny' is a literal atom — ground by definition

access_decision(VMID, Op, permit) :-
    must_be(positive_integer, VMID),
    must_be(atom, Op),
    vm(VMID, _, _, Status),
    memberchk(Status, [running, stopped]),
    permitted_operation(Op),
    must_be(atom, Op).    % Re-assert before permit output — belt-and-suspenders

The security argument for must_be/2 after a cut: once the cut fires, backtracking cannot rescue an unbound variable by trying an alternative branch. The proof is committed. If a downstream goal fails on an unbound variable, the predicate fails silently with no indication of which variable caused the failure or which committed branch produced it. must_be/2 transforms this into a structured exception:

% Without must_be — silent failure on unbound Tier:
?- host_tier(UnknownHost, Tier).
false.
% Was UnknownHost the problem? Was RAM? Was Tier? Impossible to tell.

% With must_be — explicit instantiation error:
?- host_tier(UnknownHost, Tier).
ERROR: type_error(atom, _G123)
% Immediately identifies: the Host argument was not an atom.
% The cut had not fired yet — the error is at the precondition.

For oracle predicates in the Logic Node, must_be/2 preconditions on all input arguments and postconditions on all output arguments are the standard. The additional overhead is one type-check per argument per call — negligible compared to KB scan cost, and invaluable during development and KB-update debugging.

6.2.2 Red Cuts: Load-Bearing Logic

A red cut is one whose removal changes the predicate's meaning. The most common form: a two-clause predicate where the second clause is a fallback that should only be reached when the first clause's specific condition was not met.

% Red cut — security rule with fallback
% access_decision/3: determines whether a VM operation is permitted.
% Rule 1: if the VM is in error state, deny ALL operations unconditionally.
% Rule 2: if the VM is not in error state, check the operation whitelist.

access_decision(VMID, _Op, deny) :-
    vm(VMID, _, _, error),
    !.   % RED CUT: "error state → deny" must be final.
         % Without this cut, an error-state VM could still match Rule 2
         % if the operation happened to be in the whitelist.
         % The cut enforces: error state overrides all other checks.

access_decision(VMID, Op, permit) :-
    vm(VMID, _, _, Status),
    memberchk(Status, [running, stopped]),
    permitted_operation(Op).

Remove the cut from Rule 1, and an error-state VM that matches Rule 2's conditions gets a permit decision. The cut is not a performance optimisation — it is the logic that enforces Rule 1's unconditional authority. Its absence is a security defect.

The test for red vs. green: can the cut be removed without changing the predicate's solution set for any possible call? If yes: green. If no: red. For infrastructure control predicates, red cuts must be:

Documented with an explicit comment stating what the cut enforces
Tested with a case that would produce the wrong answer if the cut were absent
Never refactored away in favour of "cleaner" multi-clause logic without re-running that test

6.2.3 The Reversibility Trade-off

Cuts destroy reversibility. A predicate with a cut cannot be used in a mode that requires backtracking through its alternatives — because the alternatives have been destroyed. For a command oracle (Chapter 5), this is the correct trade-off: replace_disk/4 must produce exactly one command; its cut-enforced determinism is the security contract. For a multi-solution enumeration predicate like find_placement/3, adding a cut would be a defect.

The rule: cut belongs in predicates that are architectural commitments — predicates where the first-matching solution is the correct solution and exploring further alternatives would be wrong. It does not belong in predicates that are designed to enumerate a solution space.

% CORRECT: cut in a commitment predicate
classify_migration_priority(VMID, critical) :-
    vm(VMID, _, _, error),
    !.   % Error VMs: always critical, never demoted by further clauses

classify_migration_priority(VMID, high) :-
    vm(VMID, Name, _, running),
    production_vm(Name),   % Fact: vm is production-critical
    !.

classify_migration_priority(_, normal).

% INCORRECT: cut in an enumeration predicate
find_eligible_hosts_bad(VMName, Host) :-
    vm_spec(VMName, Required),
    physical_host(Host, _, RAM),
    RAM >= Required,
    !.   % BUG: stops after first qualifying host — findall/3 gets only one result

6.2.4 The If-Then-Else as a Structured Cut

The ( Condition -> Then ; Else ) construct is the preferred, readable form for the pattern "if condition holds, commit to Then; otherwise do Else." It is syntactic sugar over a cut, but its scope is strictly contained: the cut inside -> applies only within the ( -> ; ) construct and does not affect choice points outside it.

% Explicit cut version — cut affects the whole clause
pool_layout_command(Host, Command) :-
    physical_host(Host, _, RAM),
    ( RAM >= 128 ->
        % Large host: generate RAID-Z2 command
        with_output_to(string(Command),
            format("zpool create 'data-~w' raidz2 /dev/sda /dev/sdb /dev/sdc /dev/sdd",
                   [Host]))
    ;
        % Small host: generate mirror command
        with_output_to(string(Command),
            format("zpool create 'data-~w' mirror /dev/sda /dev/sdb", [Host]))
    ).
% The -> cuts the choice point for the condition check only.
% No residual choice points from the condition evaluation remain.

The -> form is preferred over explicit cuts in two-branch logic because:

Its scope is visually explicit — the cut affects exactly the condition
It cannot accidentally prune choice points from surrounding goals
It reads as imperative branching, which is what it is

The explicit ! remains necessary for multi-clause predicates where the cut enforces priority ordering across clause boundaries — as in access_decision/3 above.

6.3 Negation as Failure as a Guard Dog

6.3.1 `\+` Mechanics: A Cut in Proof Clothing

\+ Goal is syntactic sugar for ( Goal -> fail ; true ). The semantics: attempt to prove Goal; if the proof succeeds, fail (the negation is false); if the proof fails, succeed (the negation is true). The cut inside -> ensures that if Goal succeeds, its choice points are discarded before the outer fail is reached — the WAM does not backtrack into Goal looking for a way to make it fail.

This means \+ is always non-invertible. \+(Goal) produces at most one answer (true or false) regardless of how many solutions Goal might have. And it binds no variables — \+ never produces bindings, because the only thing it returns is success or failure for the outer context.

% \+ is correct for these uses:
\+ vm(_, _, 'pve-node-99', _).   % pve-node-99 has no VMs — CWA enforcement
\+ storage(_, "WD-NEW001", _).   % This serial is not yet in use

% \+ is INCORRECT for these uses (covered in Section 6.3.3):
\+ vm(_, Name, 'pve-node-01', _). % UNSAFE: Name is unbound

6.3.2 `\+` and the Closed-World Assumption

Chapter 3 defined the CWA: what is not in the KB is false. \+ is the logical operator that queries this absence. \+ physical_host('pve-node-99', _, _) succeeds because no such fact exists — under CWA, the host does not exist.

The relationship is precise: \+ is correct whenever the intended semantics is "this ground fact is not in the KB." It becomes dangerous when the semantics is meant to be "this entity does not have this property" but the entity itself is not yet identified (unbound variable). The CWA is a closed-world claim about specific ground entities — not about unbound placeholders.

% Correct use: CWA over ground terms
safe_to_decommission(Host) :-
    physical_host(Host, _, _),      % Host is GROUND after this
    \+ vm(_, _, Host, running).     % No running VMs on this (ground) host

% What the CWA claim means:
% "The KB contains no fact of the form vm(_, _, Host, running)
%  for this specific, identified Host."
% This is sound because Host is bound before \+ is evaluated.

6.3.3 The Safety of `\+`: Groundness is Mandatory

The negation-on-unbound-variables hazard is the most dangerous misuse of \+ in infrastructure logic. When \+ is called with an unbound variable in the goal, it may succeed vacuously — "proving" a universal negative that was never the intended claim.

% UNSAFE: unbound variable inside \+

% Intended meaning: "find a host that has no running VMs"
find_idle_host_unsafe(Host) :-
    \+ vm(_, _, Host, running),     % DANGER: Host is unbound here
    physical_host(Host, _, _).

% What actually happens:
% \+ vm(_, _, Host, running) with Host unbound
% attempts to prove: vm(_, _, _SomeHost, running) — any host, any VM
% The KB DOES contain vm(100, 'nginx-prod-01', 'pve-node-01', running)
% So vm(_, _, _, running) SUCCEEDS
% Therefore \+(...) FAILS
% find_idle_host_unsafe/1 fails for ALL hosts — produces no results
%
% This is not a crash. It is a silent wrong answer.
% An operator querying "which hosts have no running VMs?" gets: false.
% The correct answer might be: pve-node-04 (if it existed with no VMs).
% The operator cannot distinguish "no idle hosts" from "query is broken."

The correct pattern: bind all variables before negating.

% SAFE: ground Host before \+
find_idle_host(Host) :-
    physical_host(Host, _, _),      % Host is GROUND after this line
    \+ vm(_, _, Host, running).     % Now asks: does THIS host have running VMs?

The rule is absolute: every variable that appears inside \+ must be ground (fully bound) at the point \+ is evaluated. The WAM does not enforce this. There is no type error, no instantiation error (in most cases), no warning. The predicate silently produces an incorrect result. The defence is goal ordering: goals that bind variables always precede the \+ goals that use those variables.

6.3.4 Groundness Checking in Security-Critical Predicates

For predicates where an unground \+ would be a security violation — not merely a logical error — add an explicit groundness check:

%% safe_negation(+Goal)
%% Verifies all variables in Goal are ground before attempting \+.
%% Throws an error if any variable in Goal is unbound.
%% Use as a wrapper around \+ in security-critical predicates.

safe_negation(Goal) :-
    ( ground(Goal) ->
        \+ Goal
    ;
        throw(error(
            unsafe_negation(Goal, 'Unbound variable in negation-as-failure'),
            context(safe_negation/1, Goal)
        ))
    ).

% Usage in a security predicate:
no_vm_conflict(TargetHost, VMName) :-
    physical_host(TargetHost, _, _),  % Bind TargetHost
    atom(VMName),                     % Verify VMName is ground
    safe_negation(vm(_, VMName, _, _)).   % Now safe: both args are ground

% REPL verification:
?- find_idle_host(Host).
false.   % All three hosts have running VMs — correct answer

?- safe_negation(vm(_, _, 'pve-node-01', running)).
false.   % pve-node-01 HAS running VMs — \+ correctly returns false

?- safe_negation(vm(_, _, Name, running)).
ERROR: unsafe_negation(vm(_,_,_G123,running), ...)
% Correctly rejected — Name is unground

6.3.5 `\+` vs. `dif/2`: Constraint-Based Negation

For the specific case of "these two terms must be different," \+(X = Y) has a groundness trap: if either X or Y is unbound, X = Y succeeds (unification produces a binding), so \+(X = Y) fails — the wrong result. The correct tool is dif/2, a constraint that suspends until both arguments are sufficiently instantiated:

% UNSAFE: \+ with unbound variables for inequality
vm_on_different_hosts_unsafe(VM1, VM2) :-
    vm(_, VM1, Host1, _),
    vm(_, VM2, Host2, _),
    \+(Host1 = Host2).   % If Host1 or Host2 is unbound: wrong result

% SAFE: dif/2 suspends until both are ground
:- use_module(library(dif)).

vm_on_different_hosts(VM1, VM2) :-
    vm(_, VM1, Host1, _),
    vm(_, VM2, Host2, _),
    dif(Host1, Host2).   % Constraint: Host1 ≠ Host2, enforced when both bound

For the oracle predicates in Chapter 5, TargetHost \= CurrentHost (structural non-unifiability) is correct when both arguments are ground atoms. dif/2 is the safer choice when either might remain unbound deeper in the proof.

6.4 The Build: HA Migration Pre-flight Checks

6.4.1 Pre-flight KB Extensions

Add the following facts to the inventory KB to support the pre-flight oracle:

%% Add to /opt/logic-node/kb/inventory/proxmox_inventory.pl
%% (Follow the chattr -i / edit / chattr +i procedure from Chapter 3)

%% host_maintenance_mode(+HostName)
%% True if the named host is in Proxmox maintenance mode.
%% No VMs should be migrated TO a host in maintenance.
%% (This fact is added manually when maintenance begins; removed when it ends.)

% host_maintenance_mode('pve-node-03').   % Example — commented out by default

%% host_cluster_member(+HostName)
%% True if the host is currently an active Proxmox cluster node.
%% Hosts removed from the cluster must not be migration targets.

host_cluster_member('pve-node-01').
host_cluster_member('pve-node-02').
host_cluster_member('pve-node-03').

%% vm_ha_group(+VMName, +GroupName)
%% HA group membership for VMs that have HA policies.

vm_ha_group('nginx-prod-01',    production_ha).
vm_ha_group('postgres-prod-01', production_ha).
vm_ha_group('monitoring-01',    infra_ha).

%% ha_group_allowed_hosts(+GroupName, +HostName)
%% HA policy: members of this group may only run on these hosts.

ha_group_allowed_hosts(production_ha, 'pve-node-01').
ha_group_allowed_hosts(production_ha, 'pve-node-02').
ha_group_allowed_hosts(infra_ha,      'pve-node-01').
ha_group_allowed_hosts(infra_ha,      'pve-node-03').

%% host_storage_compatible(+HostName, +StorageLayout)
%% Storage layout supported by each host for VM disk migration.
%% Layouts: raidz2 | mirror | stripe

host_storage_compatible('pve-node-01', raidz2).
host_storage_compatible('pve-node-01', mirror).
host_storage_compatible('pve-node-02', mirror).
host_storage_compatible('pve-node-03', raidz2).
host_storage_compatible('pve-node-03', mirror).

6.4.1.1 The Node Health Oracle: IO-Wait as a Cut Condition

The KB facts added above encode policy state (maintenance mode, cluster membership, HA group). Production migrations also require performance state: a host may be a valid migration target by policy but disqualified by real-time IO-Wait load. A migration onto a host with high IO-Wait compounds the problem — the migration itself adds IO pressure, creating a performance cascade where each new VM worsens the IO saturation that caused the migration need in the first place.

The Sovereign architecture keeps the Logic Node stateless — it never reads live metrics directly. Instead, the operator or an authorised monitoring integration pushes condensed health facts into a dedicated KB file, which the Logic Node reads as ground truth during the proof session.

%% Add to /opt/logic-node/kb/health/node_health.pl
%% This file is updated by a monitoring agent (e.g., cron + pvestatd parser)
%% before any migration planning session begins.
%% Format: host_io_wait(+HostName, +IOWaitPercent)
%% IOWaitPercent: integer 0–100, sampled over the last 60-second window.

host_io_wait('pve-node-01', 3).    % 3% IO-Wait — healthy
host_io_wait('pve-node-02', 78).   % 78% IO-Wait — degraded
host_io_wait('pve-node-03', 5).    % 5% IO-Wait — healthy

%% io_wait_threshold/1
%% Maximum acceptable IO-Wait percentage for a migration target.
%% Exceeding this threshold disqualifies the host unconditionally.
%% Default: 40%. Tune per site based on storage class and workload.

io_wait_threshold(40).

With this KB file in place, add Check 8 — the IO-Wait gate — to migration_blocked_reason/3. The cut here is a red cut with a specific architectural role: it prunes not just the current migration query but any further precondition evaluation for the disqualified host. Once IO-Wait is above threshold, computing HA policy or RAM headroom for that host is waste.

%% Add to preflight_oracle.pl — insert BEFORE the RAM capacity check (Check 7)
%% so that IO-Wait disqualification fires before the more expensive capacity scan.

:- use_module('/opt/logic-node/kb/health/node_health').

%% Check 8: Node IO-Wait must be below threshold (performance cascade prevention)
migration_blocked_reason(_VMName, TargetHost,
        high_io_wait(TargetHost, IOWait, Threshold)) :-
    host_io_wait(TargetHost, IOWait),
    io_wait_threshold(Threshold),
    IOWait > Threshold,
    !.   % RED CUT: high IO-Wait is a hard disqualification.
         % Prevents performance cascades: migrating onto a saturated host
         % worsens the saturation that caused the migration need.
         % No further checks for this host are meaningful.

%% Node Health Oracle — direct query interface
%% Enumerate all hosts currently above IO-Wait threshold:

:- module(node_health_oracle, [
    healthy_migration_targets/1,
    host_health_report/2
]).

:- use_module('/opt/logic-node/kb/health/node_health').
:- use_module('/opt/logic-node/kb/inventory/proxmox_inventory').

%% healthy_migration_targets(-Hosts)
%% Returns all cluster-member hosts currently below IO-Wait threshold.
%% Deterministic: findall exhausts all options, returns sorted list.

healthy_migration_targets(Hosts) :-
    io_wait_threshold(Threshold),
    findall(Host, (
        host_cluster_member(Host),
        host_io_wait(Host, IOWait),
        IOWait =< Threshold,
        \+ host_maintenance_mode(Host)
    ), Hosts).

%% host_health_report(+HostName, -Report)
%% Structured health summary for a single host.

host_health_report(HostName, Report) :-
    must_be(atom, HostName),
    physical_host(HostName, _, RAM),
    ( host_io_wait(HostName, IOWait) ->
        true
    ;
        IOWait = unknown   % No health data — treated as suspect, not healthy
    ),
    io_wait_threshold(Threshold),
    ( IOWait = unknown ->
        HealthStatus = no_data
    ; IOWait > Threshold ->
        HealthStatus = degraded
    ;
        HealthStatus = healthy
    ),
    Report = host_health(
        host:         HostName,
        ram_gb:       RAM,
        io_wait_pct:  IOWait,
        threshold:    Threshold,
        status:       HealthStatus
    ).

% REPL demonstration:
?- healthy_migration_targets(Hosts).
Hosts = ['pve-node-01', 'pve-node-03'].
% pve-node-02 excluded: 78% IO-Wait > 40% threshold.

?- can_migrate('nginx-prod-01', 'pve-node-02', Decision).
Decision = deny(high_io_wait('pve-node-02', 78, 40)).
% IO-Wait check fires before HA policy and capacity checks.
% Cut ensures only this reason is reported.

?- host_health_report('pve-node-02', Report).
Report = host_health(
    host:        'pve-node-02',
    ram_gb:      128,
    io_wait_pct: 78,
    threshold:   40,
    status:      degraded
).

The update procedure for the health KB is intentionally lightweight — a monitoring agent running as a separate, limited-privilege service writes the node_health.pl file and signals the Logic Node to reload it. The file itself follows the same chattr +i / edit / chattr -i cycle as the inventory KB, but with a shorter update interval (every 60 seconds versus the inventory's on-change update). The monitoring agent does not have access to the Logic Node's reasoning layer — it writes facts, not rules.

6.4.2 The `can_migrate/2` Predicate: Fail-Fast with Cuts

logicadmin@logic-node-01:~$ nano /opt/logic-node/kb/oracle/preflight_oracle.pl

%% =============================================================================
%% FILE:    /opt/logic-node/kb/oracle/preflight_oracle.pl
%% PURPOSE: HA migration pre-flight checks with fail-fast Cut enforcement.
%%
%% DESIGN: Each check is a separate clause or guard. Cuts enforce priority:
%%   — Maintenance mode rejection is unconditional and fires first.
%%   — Cluster membership is checked before capacity.
%%   — HA policy is checked before final permission is granted.
%%
%% A migration is permitted only when ALL checks pass.
%% Each failure clause uses a Cut to ensure exactly one rejection reason
%% is reported — not a cascade of redundant failures.
%% =============================================================================

:- module(preflight_oracle, [
    can_migrate/3,
    migration_blocked_reason/3,
    preflight_report/3
]).

:- use_module('/opt/logic-node/kb/inventory/proxmox_inventory').
:- use_module('/opt/logic-node/kb/health/node_health').
:- use_module('/opt/logic-node/kb/oracle/shell_safety').

%%  -----------------------------------------------------------------------
%%  migration_blocked_reason(+VMName, +TargetHost, -Reason)
%%  Returns the FIRST reason why migration is blocked, then cuts.
%%  This is a RED CUT predicate: the cut after each check enforces that
%%  only the highest-priority blocking reason is reported.
%%  Without the cuts, all blocking reasons would be enumerated —
%%  which is correct for an audit log but wrong for a fail-fast gate.
%%
%%  Check priority order:
%%    1. Host not in KB            (CWA: unknown host)
%%    2. Not a cluster member      (topological integrity)
%%    3. Host in maintenance mode  (operator-declared exclusion)
%%    4. VM not found              (CWA: unknown VM)
%%    5. VM in error state         (unsafe to migrate)
%%    6. VM suspended              (requires manual intervention)
%%    7. Same host                 (trivial: already there)
%%    8. HA policy violation       (governance constraint)
%%    9. High IO-Wait              (performance cascade prevention)
%%   10. Insufficient RAM          (capacity constraint)
%%  -----------------------------------------------------------------------

%% Check 1: Target host must exist in the KB (CWA enforcement)
migration_blocked_reason(_VMName, TargetHost, host_not_in_kb(TargetHost)) :-
    \+ physical_host(TargetHost, _, _),
    !.   % RED CUT: unknown host is terminal — no further checks meaningful

%% Check 2: Target host must be an active cluster member
migration_blocked_reason(_VMName, TargetHost, not_cluster_member(TargetHost)) :-
    \+ host_cluster_member(TargetHost),
    !.   % RED CUT: non-cluster host cannot receive migrations

%% Check 3: Target host must NOT be in maintenance mode
migration_blocked_reason(_VMName, TargetHost, host_in_maintenance(TargetHost)) :-
    host_maintenance_mode(TargetHost),
    !.   % RED CUT: maintenance mode is unconditional — no exceptions

%% Check 4: Source VM must exist and be in a migratable state
migration_blocked_reason(VMName, _TargetHost, vm_not_found(VMName)) :-
    \+ vm(_, VMName, _, _),
    !.

migration_blocked_reason(VMName, _TargetHost, vm_in_error_state(VMName)) :-
    vm(_, VMName, _, error),
    !.   % RED CUT: error-state VMs must not be migrated — may have corrupted state

migration_blocked_reason(VMName, _TargetHost, vm_suspended(VMName)) :-
    vm(_, VMName, _, suspended),
    !.   % Suspended VMs require manual intervention before migration

%% Check 5: Source and target must differ
migration_blocked_reason(VMName, TargetHost, same_host(VMName, TargetHost)) :-
    vm(_, VMName, TargetHost, _),
    !.   % VM is already on the target host

%% Check 6: HA group policy — if VM is in an HA group, target must be allowed
migration_blocked_reason(VMName, TargetHost, ha_policy_violation(VMName, TargetHost)) :-
    vm_ha_group(VMName, Group),
    \+ ha_group_allowed_hosts(Group, TargetHost),
    !.   % RED CUT: HA policy violation is a hard block

%% Check 7: Target host must have sufficient RAM
migration_blocked_reason(VMName, TargetHost, insufficient_ram(TargetHost, Has, Needs)) :-
    vm_spec(VMName, Required),
    physical_host(TargetHost, _, RAM),
    RAM < Required,
    !,
    Has = RAM, Needs = Required.

%%  -----------------------------------------------------------------------
%%  can_migrate(+VMName, +TargetHost, -Decision)
%%  Decision: permit(VMName, TargetHost) | deny(Reason)
%%  Deterministic: produces exactly one answer.
%%  -----------------------------------------------------------------------

can_migrate(VMName, TargetHost, deny(Reason)) :-
    migration_blocked_reason(VMName, TargetHost, Reason),
    !.   % First blocking reason found — deny immediately

can_migrate(VMName, TargetHost, permit(VMName, TargetHost)) :-
    % Reaching this clause means all blocking checks failed (none fired).
    % Final positive checks:
    physical_host(TargetHost, _, _),
    vm(_, VMName, _, _).

% REPL demonstration:

?- can_migrate('nginx-prod-01', 'pve-node-02', Decision).
Decision = permit('nginx-prod-01', 'pve-node-02').
% All checks pass: target exists, in cluster, not maintenance, VM is running,
% HA group allows pve-node-02, RAM sufficient.

?- can_migrate('nginx-prod-01', 'pve-node-99', Decision).
Decision = deny(host_not_in_kb('pve-node-99')).
% Check 1 fires: pve-node-99 not in physical_host/3. Cut → only this reason.

?- can_migrate('nginx-prod-01', 'pve-node-03', Decision).
Decision = deny(ha_policy_violation('nginx-prod-01', 'pve-node-03')).
% pve-node-03 is a valid cluster member with sufficient RAM,
% but nginx-prod-01 is in production_ha group which only allows pve-node-01/02.

% Add maintenance mode for pve-node-02, re-consult, then:
% ?- can_migrate('nginx-prod-01', 'pve-node-02', Decision).
% Decision = deny(host_in_maintenance('pve-node-02')).
% Check 3 fires before capacity or HA checks.

6.4.3 The Full Pre-flight Report

%% preflight_report(+VMName, +TargetHost, -Report)
%% Generates a structured report for operator review.
%% Uses can_migrate/3 for the decision and augments with KB-derived context.

preflight_report(VMName, TargetHost, Report) :-
    can_migrate(VMName, TargetHost, Decision),
    ( Decision = permit(_, _) ->
        % Collect context for the permit decision
        vm(VMID, VMName, CurrentHost, Status),
        physical_host(TargetHost, _, TargetRAM),
        vm_spec(VMName, Required),
        Report = report(
            decision:   permit,
            vm:         VMName,
            vm_id:      VMID,
            from:       CurrentHost,
            to:         TargetHost,
            vm_status:  Status,
            ram_needed: Required,
            ram_avail:  TargetRAM,
            margin_gb:  (TargetRAM - Required)
        )
    ;
        Decision = deny(Reason),
        Report = report(
            decision: deny,
            reason:   Reason,
            vm:       VMName,
            target:   TargetHost
        )
    ).

?- preflight_report('worker-01', 'pve-node-03', Report).
Report = report(
    decision:   permit,
    vm:         worker-01,
    vm_id:      103,
    from:       'pve-node-02',
    to:         'pve-node-03',
    vm_status:  stopped,
    ram_needed: 4,
    ram_avail:  256,
    margin_gb:  252
).

6.4.4 Refactoring the ZFS Oracle with `->`;

Chapter 5's ZFS oracle predicates used separate clauses for branching logic. The pool_scrub/3 predicate had two clauses (one for start, one for stop) — a design that requires reading both clauses to understand the full behaviour. Refactoring with ( -> ; ) consolidates this into a single clause with explicit branch logic, eliminates the residual choice point from multi-clause dispatch, and makes the branch condition visually explicit.

%% Refactored from Chapter 5 Section 5.3.3
%% Original: two separate clauses for start and stop.
%% Refactored: single clause with if-then-else — no residual choice point.

pool_scrub(HostName, Action, Command) :-
    physical_host(HostName, _, _),
    memberchk(Action, [start, stop]),   % Validate action before branching
    atom_string(HostName, HostStr),
    string_concat("data-", HostStr, PoolName),
    shell_quote(PoolName, QuotedPool),
    ( Action = stop ->
        with_output_to(string(Command),
            format("zpool scrub -s ~w", [QuotedPool]))
    ;
        with_output_to(string(Command),
            format("zpool scrub ~w", [QuotedPool]))
    ).

%% Storage layout selection — new predicate using if-then-else
%% Selects RAID-Z2 or mirror layout based on host storage compatibility
%% and available disk count.

pool_create_command(HostName, Disks, Command) :-
    physical_host(HostName, _, _),
    length(Disks, DiskCount),
    atom_string(HostName, HostStr),
    string_concat("data-", HostStr, PoolName),
    shell_quote(PoolName, QuotedPool),
    maplist(shell_quote, Disks, QuotedDisks),
    atomic_list_concat(QuotedDisks, ' ', DiskArgs),
    ( host_storage_compatible(HostName, raidz2), DiskCount >= 4 ->
        with_output_to(string(Command),
            format("zpool create ~w raidz2 ~w", [QuotedPool, DiskArgs]))
    ; host_storage_compatible(HostName, mirror), DiskCount >= 2 ->
        with_output_to(string(Command),
            format("zpool create ~w mirror ~w", [QuotedPool, DiskArgs]))
    ;
        throw(error(
            no_compatible_layout(HostName, DiskCount),
            context(pool_create_command/3,
                    'No supported storage layout for this host/disk combination')
        ))
    ).

% Refactored scrub — single clause, no choice point residue:
?- pool_scrub('pve-node-01', start, Cmd).
Cmd = "zpool scrub 'data-pve-node-01'".

?- pool_scrub('pve-node-01', stop, Cmd).
Cmd = "zpool scrub -s 'data-pve-node-01'".

?- pool_scrub('pve-node-01', invalid_action, Cmd).
false.   % memberchk/2 rejects unknown actions before branching

% Pool creation with layout selection:
?- pool_create_command('pve-node-01',
       ['/dev/sda', '/dev/sdb', '/dev/sdc', '/dev/sdd'], Cmd).
Cmd = "zpool create 'data-pve-node-01' raidz2 '/dev/sda' '/dev/sdb' '/dev/sdc' '/dev/sdd'".

?- pool_create_command('pve-node-02',
       ['/dev/sda', '/dev/sdb'], Cmd).
Cmd = "zpool create 'data-pve-node-02' mirror '/dev/sda' '/dev/sdb'".


---

### 6.4.5 `setup_call_cleanup/3`: Eliminating Side-Effect Debt

The preflight checks built in Sections 6.4.2 and 6.4.1.1 are purely logical — they query KB facts and produce structured terms. A more advanced deployment extends the Node Health Oracle with a live health check: opening a TCP connection to the Proxmox `pvestatd` socket to verify a host is actively reporting metrics, not merely present in the health KB from a stale prior run.

This introduces **side-effect debt**: the predicate allocates a resource (a socket) that must be released regardless of how the predicate terminates. Normal termination, failure, a cut firing mid-body, and an exception thrown by a downstream goal must all result in the socket being closed. This is the problem `setup_call_cleanup/3` exists to solve.

```prolog
%% setup_call_cleanup(+Setup, +Goal, +Cleanup)
%%
%% Execution contract:
%%   1. Setup is called once. If Setup fails or throws, Cleanup is NOT called.
%%   2. Goal is called. Cleanup is deterministically deferred.
%%   3. Cleanup is called exactly once when:
%%      a. Goal succeeds deterministically (no choice points)
%%      b. Goal fails
%%      c. Goal throws an exception
%%      d. A Cut fires in a parent predicate, pruning Goal's choice points
%%   Cleanup is NOT called if Goal succeeds with open choice points
%%   (choice points indicate Goal may be retried — Cleanup would be premature).
%%   Use setup_call_catcher_cleanup/4 if Cleanup must also fire on cut-with-choicepoints.

Applied to a live socket health check in the preflight oracle:

%% host_pvestatd_live(+HostName)
%% Verifies HostName is actively reporting to pvestatd by opening a
%% short-lived TCP probe to the Proxmox API status endpoint.
%% The socket is unconditionally closed by setup_call_cleanup/3
%% regardless of whether the check succeeds, fails, or throws.
%%
%% NOTE: This predicate performs a network call — it violates the
%% "KB is the only authority" principle from Chapter 5. It belongs in
%% a separate "liveness probe" module that is called explicitly before
%% a migration session, and whose result is written back to node_health.pl
%% by the authorised update procedure. It is shown here to demonstrate
%% setup_call_cleanup/3 mechanics; it must NOT be called inside
%% migration_blocked_reason/3 at query time.

:- use_module(library(socket)).

host_pvestatd_live(HostName) :-
    must_be(atom, HostName),
    atom_string(HostName, HostStr),
    string_concat(HostStr, ".cluster.local", FQDN),
    Port = 8006,   % Proxmox API port — probe for TCP accept only
    setup_call_cleanup(
        % Setup: open TCP socket to host:port
        tcp_connect(FQDN, Port, Socket),

        % Goal: verify connection succeeded — tcp_connect throws on failure,
        % so reaching this point means the host is accepting connections.
        ( stream_property(Socket, peer_address(PeerAddr)),
          format(atom(Msg), "~w pvestatd live at ~w", [HostName, PeerAddr]),
          nb_setval(last_health_probe, Msg),
          true   % Goal succeeds deterministically — Cleanup fires immediately
        ),

        % Cleanup: always close the socket, regardless of Goal outcome
        close(Socket)
    ).

The critical safety property: if a cut fires in the parent predicate after host_pvestatd_live/1 has opened its socket but before setup_call_cleanup/3 would normally close it, setup_call_cleanup/3 still closes the socket. The cut cannot create a resource leak.

%% Demonstrating the cleanup guarantee with a simulated failure:

probe_with_cut(HostName, Result) :-
    setup_call_cleanup(
        open('/tmp/probe_log.txt', write, Stream),   % Setup: open file
        (
            format(Stream, "Probing ~w~n", [HostName]),
            !,                   % Cut fires here — would orphan Stream without SCC
            Result = probed
        ),
        close(Stream)            % Cleanup: ALWAYS runs, even after the cut
    ).

?- probe_with_cut('pve-node-01', R).
R = probed.
% File '/tmp/probe_log.txt' is closed — no file descriptor leak despite the cut.

% Verify file was closed:
?- open('/tmp/probe_log.txt', read, S), read_term(S, T, []), close(S).
T = end_of_file.   % File exists and is properly closed

setup_call_cleanup/3 vs. setup_call_catcher_cleanup/4: when a goal leaves open choice points, setup_call_cleanup/3 defers Cleanup until all choice points are resolved. setup_call_catcher_cleanup/4 adds an explicit Catcher argument that fires on cut (the ! catcher) even with open choice points. For deterministic oracle predicates, setup_call_cleanup/3 is correct and sufficient. For non-deterministic predicates that use resources, setup_call_catcher_cleanup/4 provides the stronger guarantee.

The Logic Node architecture rule: any predicate that opens a file, allocates a socket, acquires a lock, or creates any external resource must wrap its body in setup_call_cleanup/3. The setup/cleanup boundary is the correctness contract that cut cannot violate.

6.5 Reclaiming the Local Stack

6.5.1 Binding Debt and the Trail

Every variable binding that occurs after a choice point is created generates a Trail entry. The Trail entry records the address of the bound heap cell so the binding can be undone on backtrack. As long as the choice point exists, all Trail entries above its TR mark are "in debt" — they must be retained in case backtracking needs them.

When a cut executes and destroys a choice point, the Trail debt associated with that choice point is resolved. The Trail entries above the cut point's TR mark are no longer needed for that choice point's backtrack. They may still be needed by the parent choice point if further backtracking occurs, but the cut's specific choice point no longer holds them hostage.

The practical consequence: a predicate that creates many choice points without cutting them accumulates Trail debt proportional to the number of variable bindings made in all those branches. For a Logic Node processing thousands of queries per session, unresolved Trail debt across many open choice points increases garbage collector pressure and slows Trail unwinding on any eventual backtrack.

6.5.2 Local Stack Reclamation: The Physical Sequence

When a cut executes in a clause of predicate p:

Before cut:
  Local Stack (top → bottom):
    [ env frame: current clause of p ]
    [ choice point B_p: clauses 2,3 of p ]
    [ env frame: goals before p in parent ]
    [ choice point B_parent ]
    ...

After cut executes:
  The WAM sets B = B_parent (skipping B_p)
  B_p is no longer reachable from the active chain
  B_p's Local Stack space: logically free
  (physically reclaimed when env frame above it is popped on clause exit)

  Trail: entries between B_p.TR and current Trail top
    that are NOT also between B_parent.TR and B_p.TR
    may be compacted (implementation-dependent; SWI-Prolog performs this lazily)

The key measurement: statistics(local_stack, [Used, Available]) before and after a heavily backtracking predicate with cuts shows the immediate reclamation effect.

% Measuring cut's Local Stack impact:

:- use_module(library(aggregate)).

benchmark_cut_effect :-
    statistics(local_stack, [Before, _]),

    % Without cut: enumerate all vm/4 solutions, keep all choice points
    findall(V-H, vm(_, V, H, running), AllVMs),

    statistics(local_stack, [AfterFindall, _]),

    % With cut via once: only first solution, choice point immediately destroyed
    once(vm(_, FirstVM, FirstHost, running)),

    statistics(local_stack, [AfterOnce, _]),

    format("Local stack before:        ~w bytes~n", [Before]),
    format("After findall (all VMs):   ~w bytes~n", [AfterFindall]),
    format("After once (first VM):     ~w bytes~n", [AfterOnce]),
    format("First VM: ~w on ~w~n",                  [FirstVM, FirstHost]).

6.5.3 Determinism as the Default; Cut as the Explicit Signal

The architecture for the Logic Node's oracle predicates follows a determinism hierarchy:

Level 1 — Structurally deterministic:
  Predicate has one clause. No choice point ever created.
  Example: physical_host(Name, MAC, RAM) — ground query.

Level 2 — Index-deterministic:
  JIT first-argument indexing reduces candidate set to one clause.
  No choice point created after indexing.
  Example: vm(100, Name, Host, Status) — ID 100 is unique.

Level 3 — Cut-deterministic:
  Multiple candidate clauses, but cut fires immediately after first match.
  Choice point created then immediately destroyed.
  Example: classify_migration_priority/2, access_decision/3.

Level 4 — once/1-deterministic:
  Caller wraps non-deterministic predicate in once/1.
  Choice point created and destroyed after first solution.
  Example: once(find_placement/3) when only first result is needed.

Level 5 — Intentionally non-deterministic:
  Predicate designed to enumerate multiple solutions.
  Choice points are semantically required.
  Example: find_placement/3, reachable_from/2.

For oracle predicates, the target is Level 1–3. Level 4 is acceptable when wrapping a Level 5 predicate for a specific single-answer query. Level 5 is correct for enumeration predicates but must never be used in command generation paths.

6.5.4 The `deterministic/0` Verification Pattern

After writing a predicate that must be deterministic, verify it leaves no choice points:

%% verify_deterministic(+Goal)
%% Executes Goal and checks that it leaves no open choice points.
%% Uses the deterministic/0 built-in (SWI-Prolog specific).

verify_deterministic(Goal) :-
    call_cleanup(
        ( call(Goal),
          ( deterministic -> Status = deterministic
          ; Status = non_deterministic
          )
        ),
        true
    ),
    ( Status = deterministic ->
        format("PASS: ~w is deterministic~n", [Goal])
    ;
        format("WARN: ~w left open choice points~n", [Goal])
    ).

% Verify oracle predicates are deterministic:
?- verify_deterministic(can_migrate('nginx-prod-01', 'pve-node-02', _)).
PASS: can_migrate(nginx-prod-01,pve-node-02,_) is deterministic

?- verify_deterministic(replace_disk('pve-node-01', "WD-WX11A2K3P801", "WD-NEW001", _)).
PASS: replace_disk(pve-node-01,...) is deterministic

?- verify_deterministic(find_placement('postgres-prod-01', _, _)).
WARN: find_placement(postgres-prod-01,_,_) left open choice points
% Expected — find_placement/3 is intentionally non-deterministic.
% Do not wrap this in can_migrate's code path.

Outcome: The Pruned Logic Model

6.6.1 The Conceptual Transition

Chapters 1–5 established Prolog as an exhaustive search engine over a KB: find all solutions, backtrack through all alternatives, enumerate all paths. That model is correct for the query layer — for finding all placement candidates, for enumerating all reachable VLANs, for collecting all orphaned VMs. It is incorrect for the decision layer — for determining whether a specific migration is permitted, for selecting the authoritative storage layout for a host, for classifying a VM's priority.

The pruned logic model draws a precise line between these two domains:

Query layer	Decision layer
Enumerate all solutions	Commit to the first valid solution
Backtracking is correct	Backtracking is a defect
No cuts	Green cuts (performance) and red cuts (logic)
`findall/3`, `bagof/3`	`once/1`, `( -> ; )`, `!`
`can_reach/2`	`can_migrate/3`
`find_placement/3`	`access_decision/3`
Non-deterministic by design	Deterministic by requirement

The cut operator is the mechanism that enforces this line at the predicate level. The ( -> ; ) construct is the mechanism that enforces it at the branch level. Both communicate the same intent: this predicate has made its decision; alternatives are not appropriate.

6.6.2 Verification Checklist

?- consult('/opt/logic-node/kb/oracle/preflight_oracle.pl').
true.
?- consult('/opt/logic-node/kb/inventory/proxmox_inventory.pl').
true.

Cut mechanics:

% 1. Green cut: classify_host produces exactly one tier
?- host_tier('pve-node-01', Tier).
Tier = tier_1.   % No ; prompt — cut eliminated choice points

% 2. Red cut: maintenance mode blocks migration unconditionally
% (assertz a test fact, verify, then retract)
?- assertz(host_maintenance_mode('pve-node-02')).
true.
?- can_migrate('nginx-prod-01', 'pve-node-02', Decision).
Decision = deny(host_in_maintenance('pve-node-02')).
?- retract(host_maintenance_mode('pve-node-02')).
true.

% 3. Priority ordering: host_not_in_kb fires before maintenance check
?- can_migrate('nginx-prod-01', 'pve-node-99', Decision).
Decision = deny(host_not_in_kb('pve-node-99')).
% Not maintenance, not capacity — first applicable check wins

Negation safety:

% 4. Ground \+: correct result
?- physical_host('pve-node-01', _, _),
   \+ vm(_, _, 'pve-node-01', error).
true.   % pve-node-01 has no error-state VMs

% 5. safe_negation/1: rejects unground input
?- safe_negation(vm(_, _, _UnboundHost, running)).
ERROR: unsafe_negation(...)   % Correctly caught

% 6. Idle host detection — safe pattern
?- find_idle_host(Host).
false.   % All hosts have running VMs — correct, not a bug

Local Stack and determinism:

% 7. Oracle predicates are deterministic
?- verify_deterministic(can_migrate('worker-01', 'pve-node-03', _)).
PASS: can_migrate(worker-01,pve-node-03,_) is deterministic

% 8. Refactored scrub has no residual choice points
?- verify_deterministic(pool_scrub('pve-node-01', start, _)).
PASS: pool_scrub(pve-node-01,start,_) is deterministic

% 9. Local Stack is stable after complex preflight query
?- statistics(local_stack, [Before, _]),
   can_migrate('nginx-prod-01', 'pve-node-02', _),
   statistics(local_stack, [After, _]),
   Delta is After - Before,
   format("Stack delta: ~w bytes~n", [Delta]).
Stack delta: 0 bytes.   % Deterministic predicate — no stack growth

6.6.3 What Comes Next

Chapter 7 introduces lists and recursive list processing — the data structure that underlies findall/3's result collection, the visited lists from Chapter 4's reachability tracer, and the Plan list from Chapter 5's migration plan generator. With the cut and determinism model established, Chapter 7's list predicates will be written from the outset with explicit determinism annotations.

Chapter Summary

Concept	Operational Definition	Security / Performance Consequence
Cut (`!`)	WAM instruction: destroys all choice points back to parent	Immediate Local Stack reclamation; permanent commitment
Green cut	Cut in clause where alternatives would all fail anyway	Performance only — safe to add/remove; no semantic change
Red cut	Cut encoding logic that requires commitment to first match	Semantic change — removal creates security defect; must be documented and tested
Cut scope	Affects only choice points within the predicate containing it	Does not prune parent's alternatives — scope is precise
`( -> ; )`	Structured if-then-else: cut scoped to condition	Preferred over explicit `!` for two-branch logic; visually explicit scope
`\+`	`( Goal -> fail ; true )` — negation as failure	Always non-invertible; binds no variables; fails silently on unground input
Groundness requirement	All variables inside `\+` must be bound before evaluation	Unground `\+` produces silent wrong answers — not exceptions
`safe_negation/1`	Throws on unground input to `\+`	Converts silent semantic error to catchable runtime error
`must_be/2`	Typed precondition/postcondition check; throws on violation	Converts silent uninstantiation failures to catchable typed errors; mandatory at oracle boundaries
Node Health Oracle	`host_io_wait/2` KB facts + IO-Wait threshold cut	Performance cascade prevention: saturated hosts pruned before capacity/HA checks
`setup_call_cleanup/3`	Setup → Goal → Cleanup, Cleanup fires on success/fail/exception/cut	Eliminates side-effect debt; resource release is cut-proof
`setup_call_catcher_cleanup/4`	Extends SCC with explicit catcher for cut-with-choicepoints	Required when non-deterministic goals hold resources across backtrack boundaries
`dif/2`	Constraint for inequality that suspends until both args ground	Correct replacement for `\+(X=Y)` with unbound variables
Binding debt	Trail entries held open by active choice points	Unresolved debt increases GC pressure; cut resolves it
Determinism levels	1=structural, 2=index, 3=cut, 4=once, 5=intentional	Oracle predicates target Level 1–3; enumeration predicates are Level 5
`verify_deterministic/1`	Runtime check that a goal leaves no open choice points	Regression test for oracle predicate determinism contracts

Exercises

Exercise 6.1 — Green vs. Red Cut Classification For each of the following predicates, classify the cut as green or red, justify your classification, and write a test case that demonstrates the semantic difference the cut makes (for red) or confirms the identical solution set (for green): memberchk/2, access_decision/3, ram_to_tier/2, can_migrate/3.

Exercise 6.2 — \+ Safety Audit Audit the predicates in proxmox_rules.pl from Chapter 3 (specifically orphaned_vm/1, storage_on_nonexistent_host/2, host_without_network/1). For each use of \+, verify that all variables inside the negation are ground at the point of evaluation. Write a corrected version of any predicate where the ordering is unsafe.

Exercise 6.3 — Pre-flight Extension Add a Check 8 to migration_blocked_reason/3: a VM whose name begins with "prod-" must not be migrated to a host whose storage layout is stripe (unreplicated). Implement host_storage_compatible/2 and vm_name_prefix/2 as KB predicates. Ensure the check integrates correctly into the priority ordering (it should fire after capacity but before final permit).

Exercise 6.4 — Determinism Verification Suite Write a predicate oracle_determinism_suite/0 that runs verify_deterministic/1 against every oracle predicate in zfs_oracle.pl and proxmox_oracle.pl. Any predicate that fails the determinism check should be flagged. Run the suite, explain any legitimate non-deterministic predicates found, and document why they are intentionally Level 5.

Exercise 6.5 — Refactoring pool_status/3 Chapter 5's pool_status/3 has two clauses (normal and verbose). Refactor it using ( -> ; ) exactly as pool_scrub/3 was refactored in Section 6.4.4. Verify with verify_deterministic/1 that the refactored version is deterministic. Explain why the original two-clause version, despite being practically correct, leaves a residual choice point that the refactored version eliminates.