The Prover

Domain independence

The central design insight is easy to miss because portage-ng is about Gentoo packages: the prover does not know what a “package” is. It works only with abstract literals and rules (Logic). That is deliberate. It means the reasoning core can be exercised and tested without importing the whole Portage domain, and the same engine could — in principle — prove goals in any domain that encodes its constraints as Horn-style expansions behind a single hook.

The prover’s only contract with the outside world is this: given a literal, resolving:rule/2 (or the configured rule/2 delegate) returns a body — a list of sub-literals that must hold for the head to hold. Everything that makes Gentoo “Gentoo” — USE flags, slots, version domains, PDEPEND side effects — lives in the rule layer and in proof-term annotations (?{Context}), not in the prover’s control flow. The prover walks literals; the domain explains what each literal means.

That separation is what keeps the implementation in Source/Pipeline/prover.pl readable: backward chaining, cycle handling, context merging, and bookkeeping — not emerge policy.

The prover is the core reasoning engine of portage-ng. Given a list of target literals, it constructs a formal proof that all dependencies can be satisfied — or completes with explicit assumptions documenting exactly where the dependency specification is unsatisfiable.

Why AVL trees?

The prover maintains its main state in four AVL trees from library(assoc) (Proof, Model, Constraints, and Triggers — see the module header in prover.pl). Plain hash tables would win on raw point lookups, but assoc trees buy a property that matters more here: they are persistent (functional). Each put_assoc/4 produces a new tree and leaves the previous one intact.

In Prolog, that lines up with backtracking. When the prover must undo a choice, variable bindings revert and the “old” assoc values bound in earlier choice points are still the right snapshots. A mutable hash map would need an explicit save/restore discipline on every failure — the sort of manual undo-stack work traditional Portage does in places, with corresponding risk of subtle inconsistency. Here, the data structures and Prolog’s search rule stay aligned.

Complexity is O(log n) per update and lookup. For on the order of tens of thousands of literals, that is a small constant number of comparisons (roughly fifteen for 32,000 entries) — more than fast enough compared with the cost of calling into domain rules and unification.

Inductive proof search

The prover performs inductive proof search via backward chaining. For each literal in the proof queue:

Check the model. If the literal is already proven (present in the Model AVL), merge contexts via feature term unification and continue.
Check the cycle stack. If the literal is currently being proved (on the stack), handle the cycle:
- If heuristic:cycle_benign/2 (literal + cycle path) succeeds, treat it as already proven (benign cycle — no assumption recorded).
- Otherwise, record a cycle-break assumption (assumed(rule(Lit)) in Proof, assumed(Lit) in Model).
Expand via rule/2. Call resolving:rule(Lit, Body) to get the rule body — the list of sub-literals that must be proven to justify Lit.
Record in Proof. Store rule(Lit) → dep(N, Body)?Ctx in the Proof AVL, where N is the dependency count.
Record in Model. Store Lit → Ctx in the Model AVL.
Update Triggers. For each body literal, add Lit to its trigger list in the Triggers AVL.
Recurse. Add the body literals to the proof queue and continue.

Steps 1 and 6 are where prescient proving and the reverse-dependency index connect; the sections below unpack those ideas.

Proof term structure

The Proof AVL maps rule keys to structured values:

rule(Lit) → dep(DepCount, Body)?Ctx

Field	Meaning
`rule(Lit)`	The literal that was proven
`DepCount`	Number of dependencies (body length)
`Body`	List of body literals
`Ctx`	Context under which the literal was proven

The dependency count is stored alongside the body because it is used by downstream consumers without having to recompute it: the explainer reads it when reconstructing justifications, and the special value -1 marks cycle-break assumptions. Storing the count once, at proof time, avoids repeated length/2 calls over the same body list.

Special keys:

assumed(rule(Lit)) with dep(-1, Body)?Ctx — prover cycle-break
rule(assumed(Lit)) with dep(0, [])?Ctx — domain assumption

Concrete Proof AVL entry

The literal itself is still just a term the prover passes through; the portage:// prefix and atom naming are domain choices. A representative Proof entry after expanding an install goal might look like this (body shortened):

rule(portage://'sys-apps/portage-3.0.77-r3':install)
  → dep(5,
        [ portage://'dev-lang/python-3.12.3':install,
          portage://'sys-libs/glibc-2.40-r5':install,
          … ])?{[ self(portage://'sys-apps/portage-3.0.77-r3'),
                … ]}

So the Proof AVL answers: which rule instance was used, how many dependencies it had, what the body literals are, and under which ?{Context} list that expansion was valid. The exact features inside ?{…} are documented in Chapter 5: Proof Literals; the prover treats them as data merged by feature term unification, not as special cases.

Model construction

Model construction flow

The Model AVL records every proven literal with its context. It serves two purposes:

Memoization. When a literal is encountered again, the prover checks the model first. If found, it merges the new context with the existing one via feature term unification rather than re-proving the literal (when the incoming context is not already equivalent to the stored one — see below).
Plan generation. The ordering pass and the printer read the model to determine which literals are in the proof and what contexts they carry.

A lightweight variant, prove_model, skips Proof and Triggers bookkeeping for internal query-side model construction where only the model is needed.

Concrete Model AVL entry

Model entries are simpler: literal → context under which it was last committed to the proof.

portage://'dev-libs/openssl-3.3.2':install
  → [ build_with_use:use_state([ssl], []),
      … ]

Multiple features can accumulate in that list as different dependency paths impose different requirements; the merge semantics are defined by the domain’s feature term unification (sampler:ctx_union/3).

Re-encountering a literal: feature term unification

When the queue delivers the same Lit again with a new ?{Context}:

The prover finds Lit in the Model AVL (with stored context OldCtx).
If the new context is semantically the same as the stored one (prover:proven/3), nothing more is done — no second expansion.
Otherwise it merges contexts via feature term unification (sampler:ctx_union/3). If the merge fails (e.g. conflicting USE enable/disable sets), the goal fails and ordinary Prolog backtracking retracts the choice that led to the clash.
If the merge succeeds, the prover may re-call rule/2 on a canonical literal carrying MergedCtx, subtract the previously proven body from the new body, and prove only the difference — updating Proof, Model, and Triggers incrementally and storing Lit → MergedCtx in the Model.

So “seen before” does not mean “frozen forever”; it means accumulate constraints and re-expand only what new information demands.

Prescient proving

When a literal is re-encountered with a changed context (e.g. new USE requirements from a different dependency path), the prover merges contexts via feature-unification and re-expands only the difference. This is called prescient proving because knowledge about constraints imposed later in the proof is incorporated into earlier decisions without unwinding the whole branch and starting the literal from scratch.

Walkthrough: two paths into `dev-libs/openssl`

Imagine two dependency paths that both need dev-libs/openssl:install:

Path A pulls it in with USE ssl required in the build set.
Path B pulls it in with USE threads required.

Without prescient-style merging, a naive story would be: prove openssl once under path A’s context; later, when path B arrives with incompatible or extra requirements, discover that the earlier proof was too weak and backtrack far enough to re-prove openssl under a wider or corrected context — repeating work and thrashing the search.

With prescient proving, the second encounter does not throw away the first. The prover merges the proof-term contexts:

First encounter:   openssl:install ?{use_state([ssl],       [])}
Second encounter:  openssl:install ?{use_state([threads],   [])}
After unification: openssl:install ?{use_state([ssl,threads],[])}

The merged context commits openssl to satisfying both paths at once. The prover then checks whether this wider context is still consistent with every constraint the rules attach to that literal — profile masks, REQUIRED_USE, version domains, and so on.

If the check succeeds, no full re-proof is needed. The prover re-expands the rule under the merged context and proves only the new body literals that the wider context introduces beyond what was already established.
If the check fails (for example, contradictory flags — a USE flag required both enabled and disabled), the merge is rejected and the prover backtracks to try another candidate.

That is the sense in which the prover is “prescient”: later requirements are folded into the context of an earlier proof step through merging and targeted re-expansion, rather than discovering the conflict only after committing to a too-narrow past choice.

Triggers and the reverse-dependency index

Triggers reverse-dependency index

The Triggers AVL is the piece that makes prescient updates addressable: it records, for each body literal, which rule heads depend on it.

Construction

When the prover proves head literal A with body [B, C, D], it extends the Triggers AVL with three reverse edges:

Proof (forward):     rule(A) → dep(3, [B, C, D])

Triggers (reverse):  B → [A, …]
                     C → [A, …]
                     D → [A, …]

In general, for a rule rule(H, Body) where Body = [L₁, L₂, …, Lₙ], the operation add_triggers/4 inserts:

For each Lᵢ ∈ Body: Triggers[Lᵢ] := [H | Triggers[Lᵢ]]

Each time a rule is recorded or re-recorded (including after a prescient merge), these reverse edges are extended so the index stays consistent with the current bodies.

Concrete example

Suppose the prover establishes:

rule(sys-apps/portage:install) → dep(3, [dev-lang/python:install,
                                          dev-libs/openssl:install,
                                          sys-libs/glibc:install])

The Triggers AVL then contains:

dev-lang/python:install  → [sys-apps/portage:install, …]
dev-libs/openssl:install → [sys-apps/portage:install, …]
sys-libs/glibc:install   → [sys-apps/portage:install, …]

If openssl’s context later changes (prescient merge adds a new USE flag), the prover can look up Triggers[dev-libs/openssl:install] in O(log n) time and immediately find that sys-apps/portage:install needs to be revisited.

Forward vs reverse lookup

The Proof and Triggers AVLs are duals of each other:

Direction	AVL	Lookup	Answers
Forward	Proof	`rule(H) → dep(N, Body)`	What does H depend on?
Reverse	Triggers	`L → [H₁, H₂, …]`	Who depends on L?

Together they form a bidirectional dependency graph: Proof walks forward from heads to bodies; Triggers walks backward from bodies to heads.

Downstream use

Later phases — the orderer (merge-order bias), diagnostics — use Triggers to answer “if this literal moves, what else moves?” in logarithmic time per lookup. Without these reverse edges, nothing in the pipeline could enumerate which install heads depended on a given dependency literal, and the graph carried out of proving would be incomplete for anything that walks dependencies backwards.

Entry rules and the pipeline

prove_plan pipeline

The pipeline module provides two canonical entry points, both with the same 5-tier committed-choice progressive relaxation (strict, keyword_acceptance, blockers, unmask, keyword_unmask):

pipeline:prove_plan_with_fallback/5 — full pipeline (prove + order). Used by production paths (--pretend, --graph, --build) and pipeline:test_stats.
pipeline:prove_with_fallback/4 — resolve pass only. Used by layered tests (resolver:test, orderer:test) and --bugs. Each test layer adds its own stages on top.

Underneath, prove_plan_basic/6 chains two stages (the trailing SCCs argument is always [] — the rule-based orderer leaves no remainder):

pipeline:prove_plan_basic(Goals, ProofAVL, ModelAVL, Plan, TriggersAVL, SCCs)

resolver:resolve/9 — hands the resolving rule set to prover:prove/10; constructs Proof, Model, Constraints, and Triggers
orderer:order/5 — hands the ordering rule set to the same prover for a second proving pass; projects the wave-list plan (Chapter 13)

The prover is wrapped in with_reprove_state which saves and restores the learned constraint store across reprove retries. Inside that, prove_with_retries catches prover_reprove exceptions and restarts up to reprove_max_retries times (default 3).

See Chapter 9: Assumptions and Constraint Learning for the reprove mechanism in detail.

Multiple stable models

The prover can produce different solutions (stable models) of the USE flag configuration space. Variants are explored by re-proving the target under thread-local branch-preference overrides (variant:use_override, variant:branch_prefer) that steer the committed choices — the choice-group cut is never removed within a single proof.

For example, a REQUIRED_USE="|| ( linux macos )" constraint yields two stable models:

Model A:  USE="linux -macos"     Model B:  USE="-linux macos"

The --variants CLI option enables this mode, running the prover with different USE flag configurations via variant:use_override and variant:branch_prefer.

Proof obligations

After a literal is proven, the prover queries the domain for additional proof obligations via heuristic:proof_obligation/4. This lets the domain inject derived obligations — extra literals to be appended to the proof queue — without the prover understanding domain-specific semantics.

PDEPEND dependencies are handled this way: they are discovered only after a literal is resolved and are injected as proof obligations via heuristic:proof_obligation/4.

Choice-event log

For debugging which || arm or version candidate the resolver tried, use --choice-log via the portage-ng-dev wrapper. The wrapper passes -Dchoice_log=true so emit/wrap sites are compiled in; without that define, goal_expansion compiles them to true / the wrapped Goal (zero overhead, same pattern as --profile / instrumentation).

Runtime arming still requires --choice-log (or choicelog:arm/0). choicelog (Source/Application/Performance/choicelog.pl) records:

any_of — trying / succeeded / failed for choice-group arms
version — alternative multi-candidate binds (index > 1 only)
reject / learn / reprove / assumption — sparse conflict path

After prove, a human-readable dump is written to stderr. From --shell (with -Dchoice_log=true), choicelog:events/1 returns the term list and choicelog:dump/0 reprints it. See also Policy: Choice.

The Prover

#Domain independence

#Why AVL trees?

#Inductive proof search

#Proof term structure

#Concrete Proof AVL entry

#Model construction

#Concrete Model AVL entry

#Re-encountering a literal: feature term unification

#Prescient proving

#Walkthrough: two paths into dev-libs/openssl

#Triggers and the reverse-dependency index

#Construction

#Concrete example

#Forward vs reverse lookup

#Downstream use

#Entry rules and the pipeline

#Multiple stable models

#Proof obligations

#Choice-event log

#Further reading