PROP-017 — Resolvo as the production resolver

1. Why resolvo now — reversing the libsolv-first call

• 03PROP-003 §2.2 picked libsolv "for v1" and explicitly kept the door open for resolvo (§4.1: "resolvo remains a viable second impl"). It gave three reasons to defer resolvo.
• By 2026-06 all three have decayed, while libsolv's costs — which §2.2 underweighted — are structural and do not decay:

04The three deferral reasons, re-evaluated:

• 05"Younger codebase (~3 years vs ~17)." resolvo is now ~4–5 years old, at 0.11.0, multi-threaded, and the production resolver for pixi, rattler (the Rust conda stack), and rip (PyPI-in-Rust).
• "Less battle-tested under adversarial inputs." conda dependency graphs are among the most conflict-rich in existence; resolvo runs against them in production at scale. This is the reason that has decayed most.
• "No rule-level introspection for explanation-driven errors." resolvo now ships structured conflict explanation (Conflict::display_user_friendly / Conflict::graph).

06libsolv's structural costs (do not decay):

• 07C toolchain + FFI + unsafe. libsolv is C; a thin FFI shim is still ~20–30 unsafe extern calls — the first C dependency in the workspace and the first unsafe surface in a crate that today carries #![forbid(unsafe_code)]. It forces a C compiler into CI on every platform. resolvo is pure Rust: the forbid(unsafe_code) posture on vibe-resolver survives intact.
• Eager pool population. libsolv wants the whole pool materialised before solving (PROP-003 §3.2 phase 1: walk list_versions for every transitively-reachable package up front). PROP-003 §3.4 itself names the network-bound fetch layer as the real bottleneck — and eager population maximises exactly those fetches. resolvo's provider is pulled lazily / on demand, so metadata is fetched only for packages the search actually visits.
• Windows operational risk. §2.2 named "libsolv proves operationally heavy on Windows" as the trigger to switch to resolvo. The maintainer's primary platform is Windows; a C library via FFI (MSVC/MinGW, submodule or build-script fragility) is precisely that risk, on precisely that platform.

• 08Net: resolvo is pure-Rust (no unsafe, no C toolchain), BSD-3-Clause (clean under PROP-000 §3 with no owner ruling needed), lazy-fetch (aligned with the real bottleneck), gives human-readable conflict explanations, and gets "prefer newest" almost free via candidate ordering.
• pubgrub was also considered and remains the weaker fit for vibevm: its range-over-named-packages model encodes the capability / virtual-package vocabulary as synthetic packages and degrades exactly the explanations we want (PROP-003 §4.2 records this).

09This decision was taken by the owner directly; the libsolv reasoning is retained in PROP-003 §2.2 as decision history.

2. Architecture — adapter behind the stable DepSolver seam

10The consumer seam does not move. crates/vibe-resolver/src/lib.rs keeps:

pub trait DepSolver {
    fn solve(&self, roots: &[PackageRef]) -> Result<ResolvedGraph, SolveError>;
}

12The install / update / vendor / check pipelines call DepSolver::solve and are untouched. resolvo arrives as one new impl DepSolver:

• 13ResolvoDepSolver<P: DepProvider> — a #[cell(seam = "DepSolver", variant = "resolvo")]. Its solve builds a VibevmResolvoProvider from the roots + the vibevm DepProvider, runs resolvo::Solver, and maps the chosen solvables back into a ResolvedGraph.
• VibevmResolvoProvider — implements resolvo's two traits, Interner + (async) DependencyProvider, adapting vibevm's world (package identities, version sets, manifests) to resolvo's NameId / SolvableId / VersionSetId model. This struct is the swap unit (§5): a different engine, or a future resolvo major, means rewriting this adapter and nothing the consumers can see.
• SemverVersionSet — a resolvo::utils::VersionSet with type V = semver::Version; an enum { Any, Req(semver::VersionReq), None } so that VersionSpec::Latest → Any, a [conflicts] / obsoletes range → a complement or None (match-nothing) set.

fn list_versions(&self, group: &Group, name: &str)
    -> Result<Vec<semver::Version>, DepProviderError>;

SolveError::Unsatisfiable { explanation: String }

3. Vocabulary → resolvo encoding

• 22vibevm's dependency vocabulary is RPM-lineage (provides / requires / conflicts / obsoletes plus the four weak-dep levels) — the same lineage resolvo inherits from libsolv, so the mapping is natural.
• resolvo's constraint channels: KnownDependencies.requirements: Vec<ConditionalRequirement> ("must be satisfied", pulls the package in) and KnownDependencies.constrains: Vec<VersionSetId> ("if present, the version must match" — does not pull the package in).
• Requirements are Requirement::Single(VersionSetId) or Requirement::Union(VersionSetUnionId).
• Single-version-per-name is enforced by resolvo automatically.

24Conditional dependencies (PROP-003 §2.6.1) keep their fixpoint shape: solve unconditional → evaluate context predicates → add requirements → re-solve. resolvo is cheap to re-run, and its laziness means the re-solve only re-touches the changed subtree.

4. Correctness — the differential dominance contract

25crates/vibe-resolver/tests/solver_properties.rs already drives two DepSolver cells over the same generated world and demands they agree; it was built (its own docs say so) as "DBT-0011's landing pad" for exactly this. ResolvoDepSolver plugs into the same socket as Sat, under a dominance contract:

• 26naive solves ⟹ resolvo solves identically. Provable for the concrete-dep worlds the generator emits: when naive's greedy first-pick succeeds, that pick is the highest version satisfying the first constraint, and (since it also satisfies all others) it equals the highest version satisfying all constraints — which is resolvo's optimum. So the graphs are byte-identical. Any drift here is a bug.
• naive fails ⟹ resolvo may solve. The first-pick-wins trap arises naturally in generated worlds (a root takes a dep's highest version, another path carets a lower major); resolvo's complete CDCL search finds the feasible lower version. This is resolvo's reason to exist.
• resolvo fails where naive solves ⟹ always a bug.
• both fail ⟹ pass without comparing error discriminants. Unlike the Sat cell — which re-emits naive's own SolveError verbatim and so shares its discriminant — resolvo produces its own richer errors (Unsatisfiable with a derivation). Demanding discriminant equality would force resolvo to throw away its better diagnostics. The relaxation is deliberate and recorded here (card scaffold-d: "a divergence is recorded with its debt id before the assertion is relaxed").

27The capability / disjunction / conflict / obsolete / weak-dep vocabulary is not exercised by the generator (it emits [requires.packages] only); those land with their own unit tests mirroring naive/tests.rs, plus resolvo-only cases (disjunction backtracking) naive cannot pass.

5. Abstraction & the swap requirement

• 28Requirement (owner, 2026-06-14). Changing the resolver engine — a different solver, or a future incompatible resolvo major — must cost one new provider/adapter and nothing else.
• The consumer-facing DepSolver and the world-facing DepProvider are the stable boundaries; everything resolvo-specific is confined to ResolvoDepSolver + VibevmResolvoProvider + SemverVersionSet.

29Concretely, a future swap is: write a new impl DepSolver whose adapter bridges the same vibevm DepProvider world to the new engine, register it as a #[cell] variant, and add it to the differential oracle so it is held to the same dominance contract. No consumer, no manifest, no lockfile change. This is the same GitBackend-style indirection PROP-001 uses to keep the git backend swappable, applied to the solver.

6. Phases / staging

30Status (2026-06-14): the port is COMPLETE — resolvo is the default production solver. Each slice landed as a topic commit with green gates.

• 31DONE — this document + the PROP-003 §2.2 supersede note.
• DONE — the shared output builder + the VersionEnumerator seam + SolveError::Unsatisfiable.
• DONE — resolvo dep; ResolvoDepSolver + VibevmResolvoProvider + SemverVersionSet; [requires.packages] + newest + narrowing.
• DONE — differential_naive_vs_resolvo_dominance (the oracle).
• DONE — [[requires_any]]→Union, [conflicts], [obsoletes], and capabilities via the closure pre-scan.
• DONE — production version enumeration (MultiRegistryResolver::list_versions + the VersionEnumerator provider impls).
• DONE — --solver <naive|sat|resolvo> override + the default flipped to resolvo in the R-001 selection seam (vibe-cli).
• DONE (forward weak-deps) — [recommends] (a post-solve greedy best-effort expansion) and [suggests] (parsed, never auto-installed) gained a Manifest schema and solver behaviour; [features.exclusive] was already validated in features.rs.
• FAR BACKLOG (reverse weak-deps + lockfile, §8) — [supplements] and [enhances] (reverse-direction, need a reverse index) and the [meta].solver lockfile recording (needs a lockfile schema-version bump) wait until the rest is ready.

32naive and sat stay in tree: naive as the small-graph fast path and the oracle's reference cell; sat as a recorded pure-Rust backtracker — both still selectable via --solver.

7. Determinism & performance

• 33Determinism. list_versions returns a stable order; sort_candidates is a total order over semver::Version; the output builder re-sorts into roots-first + (group, name) order. Given deterministic provider responses, solve is deterministic — the property the oracle's solve_is_deterministic pins.
• Performance. resolvo's laziness preserves vibevm's network profile: a package's versions are fetched only when the search first asks for that name, a manifest only when a solvable is explored. "Prefer newest" costs a sort, not a separate optimisation pass. At vibevm's scale (hundreds of packages, depth-3 graphs — PROP-003 §3.4) the solve is far from the bottleneck; the fetch layer is, and laziness is the right lever there.

8. Future work

• 34Capability resolution via a registry reverse-index. The near-term capability handling (§3) resolves [requires.capabilities] against a pre-scan of the transitive package closure — correct, and strictly stronger than naive's already-seen-graph matching, but it forgoes laziness for capabilities and only finds providers reachable through the package-dependency graph. A fuller design adds a real capability → providers reverse-index to the registry (the git-backed registry has none today): the resolver would then enumerate capability providers lazily, exactly as it enumerates package versions, and so find providers that no package edge references. This is new registry infrastructure — an index format, a publish-time emitter, and a query path — recorded here as the capability layer's natural evolution. Not scheduled; the trigger is capability routing across packages-not-yet-seen becoming load-bearing.
• Reverse weak-deps + the [meta].solver lockfile field. The forward weak-deps ([recommends], [suggests]) are implemented (PROP-003 §2.3.3) — schema in vibe-core, behaviour in ResolvoDepSolver (recommends a greedy best-effort expansion, suggests never installed). The reverse levels wait on a reverse index: [supplements] ("install me if Y is present") and [enhances] ("what enhances Y") are reverse-direction lookups, the same shape as the capability reverse-index above. Folding the per-recommend loop into one soft_requirements-batched solve is a perf optimisation that can land any time. Separately, the lockfile [meta] block has no solver field (despite PROP-003 §2.1's note); recording the selected cell for a reproducible re-resolve needs a lockfile schema-version bump.

9. References

• 35resolvo: https://github.com/prefix-dev/resolvo (BSD-3-Clause), crate resolvo 0.11 (MSRV 1.85.1); Interner + async DependencyProvider, Solver / Problem / Requirement / KnownDependencies / conflict::Conflict, utils::{Pool, VersionSet}, runtime::NowOrNeverRuntime.
• PROP-003 — dependency-model evolution (vocabulary retained; §2.2 backend superseded here).
• PROP-002 §2.8 — the DepSolver / DepProvider seam.
• PROP-000 §3 — permissive-license policy (resolvo BSD-3-Clause is clean).