Changelog
0.1.1 â 2026-09-24
- Fix: pack_install/1 failed on the 0.1.0 archive. SWI's pack manager runs
make, `make check and make install` when the pack root carries a Makefile, and the Makefile's default target was the whole suite, which needs the engines and the Rust toolchain. make and `make install` are no-ops now; `make check` loads the pack; the suite is `make test` as before. No change to the judge, the profiles or the worker.
0.1.0 â 2026-09-22
First release. The judge, the profiles, the policy file, the judge worker,
the Rust client, and four backends. Enforcement, rewrites and events are
designed and not built; see "Not yet built" in the architecture notes.
- Fix: a stored clause could define a predicate the host had declared
trusted. The head check refused pinned and profile indicators but not the trust list, so an author could stand their own body-judged clause in for the host's unwalked one. Heads naming a trusted predicate are refused as head(trusted); a mutant that disables the rule is in the harness.
- Fix: a policy file that reopened a class with
unpin and then failed validation left the class open with the previous policy still recorded, against what the documentation said. The whole file is now validated, unpins and allows included, before anything changes; an unpin of a class that does not exist is a load error like any other. hornguard_load_profiles/1 does the same: every file is read and checked before the tables are replaced, so a directory that fails to load leaves the profiles in force untouched.
- Fix: the canonical form was not a fixed point for an author's own
'$VAR'/1 terms. The writer ran in numbervars mode, so p('$VAR'('Shell')) came back as p(Shell), which an engine reads as a fresh variable where the judge saw ground data; a stored fact could thereby match every argument. Variables are now named through the writer's variable_names option and an author's '$VAR' terms print as the compounds they are. Reader fixture rd_dollar_var.
- Arithmetic is checked. The expressions of is/2 and the comparisons are walked for pinned evaluables, a new pinned_evaluable/2 term in the profiles directory;
cputime and realtime are pinned as timing, consistent with sleep/1 and get_time/1. Refused as evaluable(Name/Arity) with the class and depth a pinned goal would carry. Randomness is deliberately not pinned: swi_random admits it.
- The generated profile header no longer carries a "Reviewed by" line for a person to edit in a generated file.
profiles/REVIEWS.md is the review record: which generation of which profile, against which engine, reviewed by whom, when.
- hornguard_rewrite/3 no longer throws
not_implemented; see the judged-dispatch entry.
- CI: the "generated profiles are current" check compares the engine version recorded in the profile header with the runner's before diffing, and reports instead of failing when they differ, as the test already did; the Scryer and Trealla installs no longer fail the suite when a third-party build breaks, since the engine-agreement fixtures skip an engine that is not there.
- Attestation by experiment (
tools/attest.pl, `make attest`, `make test-attest`, in CI). Every allowed predicate the engine defines is called under seven argument shapes with tripwires around output, printed messages, global variables, flags, operators, streams, modules, threads, the recorded database, every dynamic predicate's clause count, the random state, the working directory and a scratch directory's files; the harness's own noise is calibrated out against true, and an undeclared change fails. First run on SWI-Prolog 9.2.9: 313 pure, 10 declared (swi_random moves the generator, on purpose), and four findings. write_ln/1 from library(backcomp) writes to current output, which SWI's sandbox tolerates because its hosts capture output; it is pinned under streams. eval_license/0, hash/1 and index/1 print; they leave the generated profile. And a list in goal position is consult/1 on SWI, so '[|]'/2 and '.'/2 are pinned under loading, turning what was an unknown-functor refusal into a loading probe.
- The attestation's first run on the SWI development branch (10.1.14) crashed the engine: a caught type error from bounded_number/3 frees an invalid pointer when a global variable holding a compound is set, a five-line reproducer that does not fire on 10.0.2 or 9.2.9. Reported upstream. The attestation's purpose is to find what a builtin does under arguments an author can hand it, and an engine that goes down on a caught error is such a finding, so nothing in the harness is changed for it; the development-branch CI job is advisory from now on, since that branch is early warning and not a gate.
- The differential's first run on SWI 10.x found drift in both directions, and the two are now handled differently. reduced/1, reduced/3 and, on the development branch, term_factorized/3 are safe to 9.2's sandbox and refused by 10's, whose implementations build a trie; Hornguard admitted them, which on the engine a host runs is a hole, so they are excluded from the generated profile on every version. foldall/4, ord_range/4 and string/4 are sandbox-safe on 10.x and unknown to the profile, which was generated before they existed or were safe; Hornguard refuses them, so the test that asks for every such refusal to be explained now fails only on the attested engine, where an unexplained one is the generator and the profile disagreeing, and reports them as new since attestation elsewhere. The hole test fails on every engine, always.
- Release tooling. `tools/tag.sh VERSION` checks that the tree is clean and on main, that
pack.pl, the crate and the changelog agree on the version, runs the suite, and makes the tag, signed when a signing key is configured; pushing the tag runs release.yml, which builds the pack archive, takes the release notes from this file's section for that version, and publishes the GitHub release. pack.pl points at GitHub's per-tag archive, so a tag alone is enough for pack_install/1. RELEASING.md is the runbook.
- Generated files carry no date. The profile and manifest headers stamped the generation day, so every regeneration was a diff and the currency check could only pass on that day; the review record is where dates belong. The manifest header now records the engine version the probe ran in, where the engine reports one (Trealla does, Scryer does not), and no longer names a probe file that does not exist: the probe is written by
tools/gen_engine_manifest.pl. Manifest facts are written engine(Backend, Name/Arity) with the same spacing as the profiles.
- CI runs the suite on SWI 9.2.9 as well as the PPA's stable and devel channels. 9.2.9 is the version the profiles were attested on and the version a distribution's stable package and many hosts run, so it is a supported baseline rather than a stepping stone. The first run showed the matrix had been testing 10.x only: the profile-currency check, guarded to the version in the profile header, had never run, and the review's numbers had no job that could reproduce them. A job in the official
swipl:9.2.9 container now holds that baseline and runs the currency check; on the PPA jobs the same regeneration is reported as drift. Rehearsed in the container before it was committed.
- The canonical form no longer depends on which SWI wrote it. The first CI run, on SWI 10.x, showed the engine's writer printing
{a,b} as {}(','(a,b)) and 1.5e10 as 1.5e+10 where 9.2.9 wrote {','(a,b)} and 15000000000.0; a receipt hashes this text and another engine reads it, so it cannot move with the writer. Curly terms are now always functional, {}(X), and floats are formatted by the worker: the shortest of 15 and 17 significant digits that reads back to the same double, through C's printf, with a fraction always present so an ISO engine reads a float. Reader fixtures for both.
- A seventh class,
shadowing, for the head family: a clause whose head names a trusted, allowed, pinned or control predicate, a module-qualified head, an unbound head. These were escape_attempt, which names a capability escape, and a head refusal is not one: the body is walked regardless, and the harm is to what the host's predicate answers. It is also the class a policy gap shows up as, which the first census made plain. escape_attempt now means only what it says. The Rust client gains `Class::Shadowing`; older clients see `Other("shadowing")`.
tools/triage.pl: reads a list of refusals with the scope each came from, groups them by class, rule and indicator, and separates what recurs across scopes from what stands alone. The judge cannot know intent; a host can read recurrence, and this is that reading. `make triage` on a file of Scope-Verdict terms; the census tool in a host is expected to call it.
author_defines(Name/Arity) in a policy file: a host predicate that authors legitimately add clauses to, such as the fact tables of a fact store. Its head is permitted where a trusted or allowed predicate's head is refused as shadowing; the clause body is walked as any other; calls to it follow its own allow or trust line; a pinned or control indicator is a load error. Without it, a host whose fact store is a set of platform predicates sees every author fact under those heads refused as a shadow of the trusted definition, which is what a first census against such a host showed. One mutant guards the rule.
- The attestation sweeps argument kinds. Beyond the generic shapes, each data argument of every allowed predicate takes in turn each value of the kinds known to make a quiet predicate act (stream aliases, file names, flag names, operator specs, module-qualified goals, text in three forms, extreme numbers, odd atoms) while the others stay neutral, and the
user_output and user_error aliases are captured for the call. First run: normalize_space/2 accepts a stream where an output spec is expected and writes to it, so normalize_space(user_error, X) printed from an allowed predicate; SWI's library(sandbox) declares it safe, which is why the differential never saw it. Pinned under streams, out of the generated profile, with fixtures. The same sweep runs inside Scryer and Trealla.
- The fuzzer generates evasions with canaries. Pinned goals are placed where a judge can lose them (a list handed to call/1, behind
=, =.. or functor/3, under negation, in catch/3, in an untaken branch, module-qualified, as a closure completed at the call), every generated term carries whether a pin stands where it runs, and an admitted one is reported as a judge miss whether or not a wire tripped. The pins used are harmless canaries a tripwire can see, so a miss is observable and safe. A test that re-judged admitted terms and could not fail is gone.
- Engine attestation (
tools/attest_engine.pl, `make attest-engines`, `make test-attest-engines`, in CI). The attestation experiment run inside Scryer and Trealla: for every allowed predicate an engine's manifest names, a strict-ISO probe is generated and run in that engine, one process per predicate under a wall-clock bound, with the tripwires the engine can express (output, flags, operators, streams, the predicate table, dynamic clause counts, the scratch directory). A manifest entry the engine does not define is reported as not_defined, never passed as pure. First run: Scryer 0.10.0, 69 allowed predicates pure and one finding; Trealla 3.10.41, 109 pure. The finding: Scryer's predicate_property/2 reports variant/2 as built-in while a call raises an existence error, so the manifest claimed a predicate the engine as started does not have. The manifest generator now carries a phantom list and the Scryer manifest no longer names it; regeneration also writes the enforcement declaration instead of dropping the hand-added one, which `make manifests` had been doing.
- Admit-then-run fuzzing (
tools/fuzz.pl, `make fuzz`, `make test-fuzz`, in CI). Seeded terms from the allowed, meta, control and pinned vocabulary are judged and every admitted one is run in the attestation sandbox; a tripwire on an admitted term is a composition failure. The attestation is per predicate, this is per composition. Four hundred terms at the fixed seed, and two hundred at another: no composition failure and no judge miss.
- Composition tests (
test/test_compose.pl, `make test-compose`): admitted fixtures run inert; judged dispatch through the worker, the canonical form and the runtime half, refusing at the sink inside the sandbox; a stored program rewritten, loaded and called with goals built from data; a host operator through the reader and back.
- Dynamic dispatch, judged at the sink.
dynamic_dispatch(judged) rewrites an unbound goal or closure to hornguard_call/N, which judges the goal under the loaded policy (plus hornguard_set_runtime_context/1) at the moment it runs and only then calls it; catch/3 becomes hornguard_catch/3, which cannot swallow a runtime refusal, a time limit or a resource error. The verdict is admit_with(Guarded); the worker returns the guarded canonical form; the Rust client has `Verdict::AdmitWith and Builder::dynamic_dispatch`. Bound goals are still judged statically, the default mode is unchanged, and a host may hook the runtime judgment out of the engine with runtime_judge_hook/2. Profile hornguard_runtime carries the introduced calls so no stored clause may define them. Four mutants guard the rewrite, the runtime judgment, the uncatchable set and defining. A refusal found at run time is error(Reason, hornguard(Class, runtime(Rule))); only a ball with that context is uncatchable, so an author's own throw(error(X, _)), whose context is unbound, is caught as ever.
defining(Profiles) option: a program that is a profile's definition (a battery, installed as platform code) is judged with its heads treated as definitions rather than shadows. Never unpins.
op(Priority, Type, Name) terms in a profiles directory declare operators the judge worker's reader honours; hornguard_ops/1 lists them. The canonical form stays operator-free and op/3 stays pinned for authors.
- hornguard_rewrite/3 is exported again, now as the judged-mode rewrite on its own.
- Fix: the stratification check enumerated paths with a visited list, exponential on a dense dependency graph: eleven mutually referencing predicates took six seconds and fourteen did not finish, so a small stored program could stall the judge and with it the host's rule storage. Reachability is one transitive closure now; sixty such predicates take milliseconds, and a test holds the line.
- Two pinned classes for what the walk cannot see through:
deferred_execution (freeze/2, when/2, call_residue_vars/2: the goal is judged, but it runs later at a unification the host performs) and shared_state (set_random/1, the table-abolishing predicates: what one author sets and another's query reads). None was in a shipped profile; the pins mean no host profile can admit them by accident.
- The worker's handshake reports
profiles_engine, the engine version the generated profile records, and engine_matches_profiles. An attestation of purity is per engine version.
- The worker loads every autoloadable library once at start and switches autoloading off. On SWI, asking whether a predicate is defined autoloads the library that defines it, so until now an author's text decided which libraries the judge's own process loaded.
- NOTICE file; a
CONTRIBUTING.md review clause that one maintainer can honour. The README and SECURITY.md call Hornguard what it is, the admission boundary of a sandbox, and say what a host should hash into a certificate to prove a judgment later.
- Fix:
defer_unknown(true) asked what the engine defines only on swi. On a manifest-driven backend every unrecognised predicate was deferred, including ones the manifest declared, so deferral widened the engine surface by exactly what the manifest was written to describe. Deferral and the unknown-predicate reason now come from one predicate and cannot disagree. No shipped configuration was affected, because every entry in the Scryer and Trealla manifests is either pinned or allowed by a profile; a host installing a manifest for its own engine build would have been.
- Scryer and Trealla backends: engine manifests generated by running a probe inside each engine (`make manifests`), and declared enforcement. hornguard_run/4 now refuses on any backend that is not
native, naming what the host has to do instead.
- Backend knowledge is manifest-driven where the engine cannot be asked:
engine(Backend, Indicator) and enforcement(Backend, Kind) are accepted in the profiles directory, and drive the unknown-predicate reason and defer_unknown.
- Cross-engine reader agreement: reader fixtures for Scryer and Trealla run against the real engine when it is installed, checking that it reads our canonical form into the term we meant.
- Rust client (
crates/hornguard): spawns a judge worker, checks the protocol version at the handshake, and returns a typed Verdict with Class, rule, depth and the canonical form. Locates the pack by builder path, HORNGUARD_HOME, or asking swipl. Judges only: no way to execute Prolog, by design.
- Judge worker:
prolog/hornguard_worker.pl with entry hornguard_worker_main.pl, JSON-lines over stdio (judge_goal, judge_clause, judge_program, load_policy, load_profiles, profiles, ping). Reads author text under the backend's reader flags with the standard operator table, refuses syntax errors, quasi-quotations, oversized input and extra terms as evasion/reader(_), and returns canonical operator-free text with the author's variable names preserved. Reader-agreement fixtures in `fixtures/reader/`.
- Floundering: a later occurrence inside another negation or inside an aggregation goal is a fresh local scope, not a use; found by judging a production puzzle solver that reused a local name across two negations and a forall.
- Profiles
swi_random and swi_backcomp (library(random), library(backcomp) as module backward_compatibility).
- The Rust core is deferred: a judge worker running the pack in its own process with canonical re-emission covers trusted-position judging and parser differentials for any host;
crates/README.md records the reasoning and the signals that would revive it.
- README: "Beyond the judge" describes the layers a real deployment needs above admission and where the library came from; SECURITY.md names who receives reports.
- hornguard_load_profiles/1 accepts a list of directories so a host installs its own profiles beside the shipped ones; the pin check runs over the union.
- README rewritten around use: the firewall framing, worked verdicts, installing profiles, policy files, what is and is not built, how it is tested. Diagrams in Mermaid.
- Generated-term properties:
test/test_generated.pl builds 400 seeded goals from pure, pinned, meta and control vocabulary and checks that a pinned goal in call position is always refused, a clean term never is, a pinned functor in data position is admitted, refusal is monotonic under profile subsets, the judge never binds its input, verdicts are deterministic, the swi backend agrees with iso on refusals, and a goal and the same goal as a clause body refuse under the same class.
- Mutation harness:
tools/mutate.py disables one walker rule at a time (25 mutants at release) and requires every mutant to fail the suite. Its first run found one blind spot, the fail-closed meta-gap rule, now covered; head-shadowing and trust-spec coverage widened.
- Policy files: hornguard_load_policy/1 reads backend, profiles, options, host allows, trust declarations and unpins from a file of facts; hornguard_admit/2, hornguard_admit_clause/2 and hornguard_admit_program/2 judge under the loaded policy. Unpinning is logged at every load and undone by the next policy; load errors leave the previous policy in force.
- CI over SWI stable and devel with Scryer and Trealla installed, and a weekly run so a changed builtin surfaces early.
- Private fixture overlay: HORNGUARD_FIXTURES_EXTRA names directories of additional fixtures to run alongside the public suite, for cases a host derives from its own incidents. The mutation harness decides what belongs in the public contract.
defer_unknown(Bool) option: an indicator the engine does not define is reported as predicate(Indicator) in admit_needs instead of refused, so a rule may be stored before the rules it calls. Needs are now self-describing: profile(Name) or predicate(Indicator).
- Engine profiles:
swi, swi_lists, swi_apply, swi_aggregate, swi_solution_sequences, swi_strings, swi_pairs, swi_ordsets, swi_assoc, swi_terms, swi_error, generated from the engine by tools/gen_swi_profiles.pl with meta specs derived from meta_predicate declarations. New pins: timing class (sleep), at_halt, cancel_halt, thread_self, statistics, module reflection, attribute deletion, nb_current, writeln and the remaining output family.
- Sandbox differential:
tools/differential.pl judges every engine predicate with Hornguard and with SWI's library(sandbox); test/test_differential.pl fails on any unexplained disagreement or a stale generated profile. First run: 702 predicates, zero.
- Fix: a partially bound Verdict argument now fails instead of leaking the internal refusal exception.
- Judge hardening: cyclic terms are refused before the walk (the walk did not terminate on them), stack exhaustion on pathologically deep terms becomes a refusal instead of an engine error, and the judged copy is stripped of attributes so a coroutine on the caller's term cannot fire inside the judge. New class
evasion, rules cyclic_term and term_depth.
- Floundering check: hornguard_floundering/2 reports negated goals that introduce a variable used after them; refused under
semantics when strict_negation(true) (the default), skipped under strict_negation(false).
- Program admission and stratification: hornguard_admit_program/4,5 judges a clause set with its own heads admitted in bodies and refuses unstratified programs under the new
semantics class; hornguard_stratification/2 returns strata or the offending cycle. Aggregation is stratified like negation.
- prologue profile admits not/1 with the same meta shape as \\+/1.
- Judge extracted into the pack: hornguard_admit/4,5 and hornguard_admit_clause/4,5 over loaded profiles and pinned classes; fixture runner and clause fixtures.
- Repository scaffold: architecture notes, pack skeleton, seed profiles (
iso,
prologue, pinned classes), fixture format and first verdict fixtures.