:- module(hornguard_gen_engine_manifest, [ gen_probe/3, assemble/3 ]). %% Engine manifests: what a backend's engine defines. %% %% The judge needs this for backends it cannot introspect. On SWI it asks the %% engine directly; on Scryer and Trealla there is no way to ask from here, so %% a manifest is generated by running a probe inside that engine and recording %% what it answered. %% %% The probe is generated self-contained — candidates, backend name and output %% path all embedded — because the engines disagree about command-line %% arguments: Scryer has no `argv` flag, and Trealla consumes the first %% argument as a file to consult. Nothing is passed in. %% %% swipl -g "gen_probe(scryer, '/tmp/hg_scryer.pl', '/tmp/hg_probe.pl')" -t halt tools/gen_engine_manifest.pl %% scryer-prolog /tmp/hg_probe.pl %% swipl -g "assemble(scryer, '/tmp/hg_scryer.pl', 'profiles/engine_scryer.pl')" -t halt tools/gen_engine_manifest.pl %% %% `make manifests` does all of it. A manifest records existence, never %% permission: an indicator here that no profile allows is still refused, and %% the manifest only changes the *reason* (permission rather than existence) %% and stops defer_unknown from deferring something the engine really has. :- use_module(library(lists)). :- use_module(library(apply)). :- use_module('../prolog/hornguard'). max_probe_arity(8). %! gen_probe(+Backend, +OutFile, +ProbeFile) is det. % % Write a self-contained probe for Backend. It asks about every indicator % worth asking an engine about: everything the profiles allow, everything % pinned (name-only pins expanded over plausible arities), and the control % constructs. Candidates are emitted as `cand(Name, Arity)` rather than as % indicators because Scryer's reader rejects a quoted operator atom before % `/`: `'=..'/2` is a syntax error there while `'=..'` as a plain argument % is fine. gen_probe(Backend, OutFile, ProbeFile) :- hornguard_profiles(_), findall(N-A, candidate(N, A), Cs0), sort(Cs0, Cs), setup_call_cleanup(open(ProbeFile, write, S), emit_probe(S, Backend, OutFile, Cs), close(S)), length(Cs, Len), format("~w: probe for ~w over ~d candidates~n", [ProbeFile, Backend, Len]). emit_probe(S, Backend, OutFile, Cs) :- format(S, "%% GENERATED probe: runs inside ~w and writes its manifest.~n", [Backend]), format(S, "%% Strict ISO plus predicate_property/2; nothing is passed in.~n~n", []), forall(member(N-A, Cs), format(S, "cand(~q, ~w).~n", [N, A])), % A sentinel keeps phantom/2 defined on an engine with no phantoms. format(S, "phantom(hg_no_phantom, -1).~n", []), forall(reports_but_does_not_define(Backend, N/A), format(S, "phantom(~q, ~w).~n", [N, A])), format(S, "~ndefined(N, A) :- \\+ phantom(N, A), functor(G, N, A), catch(predicate_property(G, built_in), _, fail).~n~n", []), % A failure-driven loop, not forall/2: Scryer has no forall/2 without a % library, and a probe that needs libraries is a probe of the libraries. format(S, "emit(S) :- cand(N, A), defined(N, A),~n", []), format(S, " write_canonical(S, engine(~q, N/A)), write(S, '.'), nl(S), fail.~n", [Backend]), format(S, "emit(S) :- catch(current_prolog_flag(version_data, V), _, fail),~n", []), format(S, " write_canonical(S, engine_version(~q, V)), write(S, '.'), nl(S), fail.~n", [Backend]), format(S, "emit(_).~n~n", []), format(S, "probe :- open(~q, write, S), emit(S), close(S), halt.~n~n", [OutFile]), format(S, ":- initialization(probe).~n", []). % What an engine's predicate_property/2 calls built_in but raises an % existence error for when called, as started. Found by the engine % attestation (`make attest-engines`), which reports such an entry as % `not_defined`; it is listed here so regeneration does not put it back. % Scryer 0.10.0: variant/2 belongs to library(terms) and is not loaded. reports_but_does_not_define(scryer, variant/2). candidate(N, A) :- hornguard:hg_allow(_, N/A). candidate(N, A) :- hornguard:hg_pinned(_, N/A0), ( integer(A0) -> A = A0 ; max_probe_arity(Max), between(0, Max, A) ). candidate(N, A) :- member(N/A, [(',')/2, (;)/2, (->)/2, (*->)/2, (^)/2, (:)/2, (!)/0, true/0, fail/0, false/0, (\+)/1, call/1, call/2, call/3]). %! assemble(+Backend, +ProbeOutput, +ManifestFile) is det. % % Copy the probe's answer into the profiles directory, with a header, and % report what the engine defines that Hornguard pins — the interesting % part of a manifest, since those are the capabilities that engine really % exposes to an author. assemble(Backend, ProbeOut, Manifest) :- read_terms(ProbeOut, Terms), include([engine(_, _)]>>true, Terms, Engine0), sort(Engine0, Engine), ( memberchk(engine_version(_, VData), Terms), engine_version_text(VData, Version0) -> format(atom(Version), "against ~w", [Version0]) ; Version = 'against an engine that reports no version; the review record names it' ), length(Engine, N), hornguard_profiles(_), findall(Class-Ind, ( member(engine(_, Ind), Engine), hornguard:hg_pinned(Class, Ind) ), Pinned0), sort(Pinned0, Pinned), setup_call_cleanup(open(Manifest, write, S), emit(S, Backend, Version, Engine, Pinned), close(S)), length(Pinned, NP), format("~w: ~d predicates, ~d of them in pinned classes~n", [Manifest, N, NP]). % trealla(3,10,41,[]) -> "trealla 3.10.41"; anything else as written. engine_version_text(VData, Text) :- compound(VData), VData =.. [Name|Parts], include(integer, Parts, Nums), Nums \== [], atomic_list_concat(Nums, '.', Dotted), format(atom(Text), "~w ~w", [Name, Dotted]), !. engine_version_text(VData, Text) :- format(atom(Text), "~q", [VData]). % No date in the header: the review record carries dates, and a stamp % here would make every regeneration a diff. emit(S, Backend, Version, Engine, Pinned) :- format(S, "%% Engine manifest: what ~w defines.~n", [Backend]), format(S, "%%~n%% GENERATED by a probe tools/gen_engine_manifest.pl writes and runs inside~n", []), format(S, "%% the engine, over the candidate list the loaded profiles and pins give,~n", []), format(S, "%% ~w.~n", [Version]), format(S, "%% Regenerate with `make manifests`.~n%%~n", []), format(S, "%% This records what EXISTS, never what is allowed. An indicator here~n", []), format(S, "%% that no profile allows is still refused; the manifest only changes the~n", []), format(S, "%% reason to a permission error and stops defer_unknown from deferring it.~n%%~n", []), format(S, "%% It describes the engine AS STARTED, with no libraries loaded. Libraries~n", []), format(S, "%% widen what exists: Scryer reaches shell/1 and the sockets through~n", []), format(S, "%% library(os) and library(sockets), which is why `loading` is pinned. A~n", []), format(S, "%% host that loads libraries into author space has widened the engine, and~n", []), format(S, "%% should regenerate this manifest with those libraries loaded.~n%%~n", []), format(S, "%% Capabilities this engine really exposes, all of them pinned:~n", []), forall(member(Class-Ind, Pinned), format(S, "%% ~q~t~34|~w~n", [Ind, Class])), nl(S), format(S, ":- multifile engine/2.~n~n", []), forall(member(engine(B, Ind), Engine), format(S, "engine(~q, ~q).~n", [B, Ind])), enforcement_note(Backend, Kind, Lines), nl(S), forall(member(L, Lines), format(S, "%% ~w~n", [L])), format(S, "enforcement(~q, ~q).~n", [Backend, Kind]). % The declared enforcement travels with the manifest. It is knowledge % about the engine, not a probe result, so it lives here and is written % on every regeneration rather than hand-added to a generated file. enforcement_note(scryer, external, [ "Enforcement: Scryer has no in-engine time, inference or stack caps, no", "protected static code, and no module isolation an author cannot see", "through. A host runs it under an external bound — a process wrapper that", "caps address space and kills on RSS or on the parent's exit — and attests", "that before running anything." ]). enforcement_note(trealla, external, [ "Enforcement: like Scryer, Trealla has no in-engine caps the judge's host", "can rely on. Compiled to WebAssembly it inherits the runtime's fuel and", "memory limits, which is the strongest hermetic option here, but that is a", "property of the deployment rather than of the engine, so the host attests", "it." ]). read_terms(File, Terms) :- setup_call_cleanup(open(File, read, S), read_all(S, Terms), close(S)). read_all(S, Terms) :- read_term(S, T, []), ( T == end_of_file -> Terms = [] ; Terms = [T|Rest], read_all(S, Rest) ).