The judge. Pure: it never executes the term it is given. It walks a goal or a clause, consults the loaded profiles (allow/2, meta_spec/2) and the pinned class table (pinned/2), and returns a verdict:

• admit
• admit_with(Guarded) - under dynamic_dispatch(judged): admissible as Guarded, the term with every unbound goal or closure rewritten to a call the judge sees again at the moment it runs. Run Guarded, never the original.
• admit_needs(Needs) - admissible once the host satisfies each need: profile(Name) for a known profile not in force, predicate(Indicator) for a sandboxed predicate not yet stored (only under defer_unknown(true))
• refused(Reason, Class, Rule) Reason: an ISO error term the host may show the author, subject to its oracle policy Class: benign_miss | capability_probe | escape_attempt | reconnaissance | shadowing | semantics | evasion shadowing is the head family: a clause that would stand in for a definition the judge reasons about. Its body is walked like any other; the harm is to what the host's predicate answers, not to what a call can do, and in practice it is the class a policy gap shows up as (see tools/triage.pl). Rule: pinned(Class) | unbound_goal | qualified | meta_spec(Indicator) | unknown | not_callable | head(Why) | directive | unsupported(What) | evaluable(Name/Arity) | unstratified(Members, Head-Callee) | floundering(NegatedGoal) | cyclic_term | term_depth A pinned rule nested inside a meta-argument carries + depth(N). head(Why) is one of control, pinned(Class), profile(Name), trusted, qualified.

The semantics class is not a threat signal. It marks a program the judge can admit capability-wise but refuses to store because it has no single intended meaning: recursion through negation or aggregation (hornguard_stratification/2), and negation used as if it bound a variable (hornguard_floundering/2). The latter is refused only under strict_negation(true), the default; a host that passes strict_negation(false) may still call hornguard_floundering/2 itself and warn.

Structural rules, in the order the walk applies them:

1. An unbound goal in call position is refused. Always. This closes construct-then-call at the sink.
2. Module-qualified goals are refused; the sandbox has one module.
3. The control constructs (,)/2 (;)/2 (->)/2 (*->)/2 and (^)/2 are walked through without counting depth.
4. A predicate in a pinned class is refused before any profile is consulted.
5. A predicate the host declared trust(Indicator, Spec) is admitted with its declared meta spec applied and its body not walked.
6. A predicate allowed by a profile in force has each goal argument judged one level deeper; closures are completed to full arity with fresh variables first. On backends with introspection, an allowed predicate that the engine declares meta but no profile gives a spec for is refused (fail closed).
7. A predicate allowed only by a profile not in force is recorded as a need; under defer_unknown(true) so is a predicate the engine does not define.
8. Anything else is refused as unknown, with an existence or permission reason depending on what the backend can tell.

Two more rules apply where the walk would otherwise not look. An arithmetic predicate's expressions are checked for pinned evaluables (the clock-reading functions), since arithmetic is a second language inside the first. And a clause head may not name a predicate the host trusts: the trusted definition is the one whose body is never walked, and a clause in sandboxed space would stand in for it.

Rule 1 has one sanctioned relaxation. Under dynamic_dispatch(judged) an unbound goal or closure is not refused but rewritten to hornguard_call/N, which judges the goal under the same policy at the moment it runs and only then calls it, and catch/3 becomes hornguard_catch/3, which cannot swallow a runtime refusal. The verdict is then admit_with(Guarded), and the host runs Guarded. Judgment happens twice, statically where the goal is known and at the sink where it is not; nothing runs unjudged either way. The runtime judge is the loaded policy plus whatever hornguard_set_runtime_context/1 has set (a namespace's stored predicates, typically), or a host's own runtime_judge_hook/2 when it wants the judging done in a process the author cannot reach.

Enforcement (hornguard_run/4) is not yet implemented; it belongs to the backend layer, not the judge.

 hornguard_load_profiles(+DirOrDirs) is det

Replace the loaded profiles with every `.pl` profile file under the given directory, or under each of a list of directories in order. A host installs its own profiles by naming its directory after the library's: the shipped profiles and the host's load into one table, and the policy check runs over the union.

The directory holds profiles and backend manifests. Accepted terms: allow(Profile, Name/Arity), meta_spec(Profile, Spec), pinned(Class, Name/Arity), pinned_evaluable(Class, Name/Arity), engine(Backend, Name/Arity), enforcement(Backend, Kind) and directives (ignored). Anything else is a domain_error. An allow that names a pinned indicator is a load error: pinned classes are not reopened by profile.

Every file is read and checked before any table changes, so a directory that fails to load leaves the profiles that were in force exactly as they were.

 hornguard_ops(-Ops) is det

The operators the loaded profiles declare, as op(Priority, Type, Name) terms. A host whose stored rules use an operator (a battery's ::, say) declares it in its profiles directory; the judge worker's reader honours it, and the canonical form it emits is operator-free, so the engine never needs to know. op/3 itself stays pinned for authors.

 hornguard_profiles(-Names) is det

The profile names the loaded policy knows about.

 hornguard_load_policy(+File) is det

Load a host policy: what the host adds on top of the profiles. The file holds Prolog facts, read with read_term/2 and never consulted:

• backend(Name) default iso
• profiles(List) profiles in force; default [iso]
• option(Opt) strict_negation(B) | defer_unknown(B)
• allow(Name/Arity) a sandboxed predicate whose clauses were body-judged at storage
• trust(Name/Arity, Spec) a host predicate admitted without walking its body; Spec is none or a meta_predicate-style term of the same name and arity
• author_defines(Name/Arity) a host predicate authors may add clauses to, such as a fact table: a permitted head, with the clause body walked as any other. Calls to it follow its allow or trust declaration. Never a pinned or control indicator.
• unpin(Class) reopen a pinned class. Logged as a warning at load, every time.

Load errors are thrown: an allow that names a pinned indicator (unless that class is unpinned in the same file), a trust spec whose name or arity does not match, an unknown profile, an unknown option, or any other term. Loading replaces the previous policy.

 hornguard_policy(-Policy) is det

The loaded policy as policy(Backend, Profiles, Options, Allow, Trust), or the default policy(iso, [iso], [], [], []) when none is loaded.

 hornguard_admit(+Goal, -Verdict) is det

 hornguard_admit_clause(+Clause, -Verdict) is det

 hornguard_admit_program(+Clauses, -Verdict) is det

Judge under the loaded policy.

 hornguard_admit(+Backend, +Profiles, +Goal, -Verdict) is det

 hornguard_admit(+Backend, +Profiles, +Goal, +Options, -Verdict) is det

Judge Goal under the named Profiles. Goal is never executed and never bound. Options:

• allow(ListOfIndicators) Host predicates whose clauses live in sandboxed space and were body-judged at storage. Admitted like a profile entry, no spec.
• trust(ListOf(Indicator-Spec)) Host predicates admitted without walking their bodies. Spec is a meta_predicate-style term or the atom none.
• strict_negation(Bool) Default true: a negated goal that introduces a variable used later is refused under semantics. False skips the refusal.
• defer_unknown(Bool) Default false. True reports an indicator the engine does not define as predicate(Indicator) in admit_needs instead of refusing it, so a stored rule may call a rule stored later. Engine-defined predicates no profile allows are still refused.

 hornguard_admit_clause(+Backend, +Profiles, +Clause, -Verdict) is det

 hornguard_admit_clause(+Backend, +Profiles, +Clause, +Options, -Verdict) is det

Judge a clause for storage. The body is judged exactly as a goal. The head may not be unbound, module-qualified, a control construct, or an indicator that a pinned class or a loaded profile already claims: a stored clause must not shadow anything the judge reasons about. Directives are refused. DCG rules are refused until the translation is judged post-expansion.

 hornguard_admit_program(+Backend, +Profiles, +Clauses, -Verdict) is det

 hornguard_admit_program(+Backend, +Profiles, +Clauses, +Options, -Verdict) is det

Judge a clause set for storage as one program. Every clause is judged as by hornguard_admit_clause/5 with the program's own heads admitted in bodies, so rules may call each other. Then the program must be stratified: no recursion through negation or aggregation. A capability refusal wins over a semantics refusal; the first refusal in clause order is reported.

 hornguard_stratification(+Clauses, -Result) is det

Result is stratified(Strata), Strata a list of lists of indicators from the lowest stratum up, or unstratified(Members, Head-Callee): the strongly connected predicates that recurse through a negative dependency, and the negative edge that closes the cycle.

Dependencies are collected from rule bodies. Control constructs are transparent. \+, not/1, forall/2, and the all-solutions and aggregation predicates (findall, bagof, setof, aggregate_all) make their goal arguments negative dependencies, as Datalog treats aggregation, because their result depends on the callee being complete. Other meta-predicates pass the current polarity to their goal and closure arguments. Only predicates defined in Clauses take part; everything else is a base relation. Directives and DCG rules are ignored here (hornguard_admit_program/5 refuses them first).

 hornguard_floundering(+ClauseOrGoal, -NegatedGoals) is det

NegatedGoals are the \+ G and not(G) goals in the clause body (or in the goal, read as a body with no head) that introduce a variable and then rely on it: the variable does not occur in the head or in any earlier positive goal, and does occur somewhere after the negation. Negation never binds, so such a variable is unbound where it is used.

A variable that occurs only inside the negated goal is existential and fine (\+ parent(_, X)). Aggregation goals (findall/3 and friends) bind only their result argument; their template and goal variables are local and do not count as bound afterwards. Disjunction is read permissively: an occurrence in any earlier branch counts as bound.

 hornguard_rewrite(+Backend, +Term, -Guarded) is det

Term with every unbound goal or closure in a sink position rewritten to hornguard_call/N, and every catch/3 to hornguard_catch/3. Bound goals are left alone: the judge sees them statically. Uses the loaded profiles' meta specs and the loaded policy's trust specs to know which argument positions are sinks. hornguard_admit/5 under dynamic_dispatch(judged) does this itself and returns the result in admit_with/1; this is the same rewrite for a host that wants it separately.

 hornguard_call(:Goal) is nondet

Judge Goal under the loaded policy, plus what the host set with hornguard_set_runtime_context/1, at the moment it is called; then call it. In judged mode, so a goal that itself carries an unbound sink is rewritten and judged again when that sink runs. A refusal is thrown as

error(Reason, hornguard(Class, runtime(Rule)))

which hornguard_catch/3 will not swallow. A host that wants the judging done outside the engine defines runtime_judge_hook/2.

 hornguard_set_runtime_context(+Options) is det

What hornguard_call/N judges under, beyond the loaded policy: profiles(Names), allow(Indicators), trust(Pairs). A host sets this for the namespace whose rules are about to run, from a position the author cannot reach; the setter is not in any profile.

 hornguard_catch(:Goal, ?Catcher, :Recovery) is nondet

catch/3 as a stored rule gets it: a runtime refusal, a time limit, a resource error and an execute permission error pass straight through, so a catch-all recovery cannot hide that a goal was refused or keep a query running past its budget.

 hornguard_run(+Backend, +Profiles, +Caps, +Goal)

Not yet implemented, and it refuses before it gets that far on any backend that cannot bound a running goal. A judge-only backend has no caps, no isolation and no uncatchable abort: admitting a goal there and running it anyway is the mistake this predicate exists to prevent.

Undocumented predicates

The following predicates are exported, but not or incorrectly documented.

 hornguard_admit(Arg1, Arg2, Arg3, Arg4, Arg5)

 hornguard_admit_clause(Arg1, Arg2, Arg3, Arg4, Arg5)

 hornguard_admit_program(Arg1, Arg2, Arg3, Arg4, Arg5)

 hornguard_call(Arg1, Arg2)

 hornguard_call(Arg1, Arg2, Arg3)

 hornguard_call(Arg1, Arg2, Arg3, Arg4)

 hornguard_call(Arg1, Arg2, Arg3, Arg4, Arg5)

 hornguard_call(Arg1, Arg2, Arg3, Arg4, Arg5, Arg6)

 hornguard_call(Arg1, Arg2, Arg3, Arg4, Arg5, Arg6, Arg7)

 hornguard_call(Arg1, Arg2, Arg3, Arg4, Arg5, Arg6, Arg7, Arg8)

 hornguard_admit_clause(Arg1, Arg2)

 hornguard_admit_program(Arg1, Arg2)