PROP-003 — Dependency-model evolution: SAT solver, features, subskills, context activation, i18n

2.1 Solver upgrade path: SAT-class engine behind the existing DepSolver trait

15Decision. Add a second DepSolver impl, SatDepSolver, alongside NaiveDepSolver. Both implement the same crates/vibe-resolver/src/lib.rs::DepSolver trait (fn solve(&self, roots: &[PackageRef]) -> Result<ResolvedGraph, SolveError>). NaiveDepSolver stays in tree as the "small graphs / no features / no disjunctions" fast path. The default clause is superseded (PROP-017): both impls shipped (naive.rs, sat.rs), but the production default became resolvo, not sat.

16The selector is a single line in vibe-cli/install.rs (and the parallel paths in update, vendor, check). Three clauses aged and are corrected here: the lockfile selection key [meta].solver was never wired (PROP-017 §8 records the gap — the live vibe.lock carries no solver key); the shipped CLI override is --solver <naive|sat|resolvo>, not <naive|sat>; and the default is resolvo, as the flag's own help states.

17Why two impls, not "rip out Naive." Naive is ~250 lines of straightforward Rust covering ~95 % of today's fixture graphs at constant-fold-of-DFS speed. The SAT-class engine, even when wrapping libsolv, is heavier to cold-start (rule encoding, watched-literals init); for trivial graphs that's pure overhead. Keeping both lets us regression-test the SAT impl against Naive's outputs on simple graphs, which is the cheapest oracle we'll ever have.

18DepSolver trait — minimal additions. The trait gains one method:

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

    /// Hint the solver to prefer keeping packages already pinned in the
    /// caller's lockfile. The default impl ignores the hint (correct
    /// for `NaiveDepSolver`, which has no preference machinery).
    /// `SatDepSolver` honours it via libsolv's "favor" rules.
    fn pin_preferences(&mut self, _pins: &[(PackageRef, semver::Version)]) {}
}

20pin_preferences is what enables the vibe update "minimum churn" property: re-resolve, but prefer the existing version of every untouched package. PROP-002 §2.7's [meta].root_dependencies carries the user-typed roots; the lockfile's [[package]] entries carry the satisfying pins. pin_preferences consumes the latter.

2.2 SAT solver backend: libsolv (BSD-3-Clause), via thin Rust FFI

21SUPERSEDED (2026-06-14) by PROP-017. The production solver is resolvo (pure-Rust, BSD-3-Clause), not libsolv. The decision below is retained as history; PROP-017 §1 records why the libsolv-first call was reversed — its three deferral reasons for resolvo decayed by 2026, while libsolv's C-FFI / unsafe / eager-pool / Windows costs are structural. PROP-003's dependency vocabulary (§2.4–2.10) is unaffected; only the engine changed.

22Decision. The SAT engine of SatDepSolver is libsolv (https://github.com/openSUSE/libsolv). Wrap it through a thin in-tree FFI layer (a new vibe-resolver-libsolv crate or feature-gated module under vibe-resolver); do not pull in libdnf5 or any LGPL-licensed shim.

23License audit (load-bearing). libsolv is dual-licensed BSD-3-Clause / FreeBSD (LICENSE.BSD). Permissive, satisfies PROP-000 §3 (third-party deps: permissive only — MIT / Apache-2.0 / BSD / Unlicense; MPL-2.0 case-by-case; GPL/AGPL/LGPL forbidden). Linking against libsolv as a C library or a static archive is fine. We MUST NOT link against libdnf5 (LGPL-2.1-or-later) — its API is the most ergonomic layer over libsolv but its license places a copyleft obligation on every consumer.

24Why libsolv, not the alternatives.

• 25resolvo (https://github.com/prefix-dev/resolvo): pure-Rust, BSD-3-Clause, used by Pixi / Rattler at conda scale. Strong candidate, was the leading PROP-002-era choice. Reasons not to pick first: (a) younger codebase (~3 years vs libsolv's ~17), (b) less battle-tested under adversarial inputs, (c) does not expose the rule-level introspection libsolv does, which we need for explanation-driven error messages. We keep the door open: vibe-resolver-resolvo could be a future second SAT impl behind the same trait if libsolv proves operationally heavy on Windows or surfaces unfixable upstream bugs.
• pubgrub (Cargo's solver): BSD-3-Clause (well, MIT/Apache-2.0 dual), pure-Rust, designed for SemVer-shaped constraints. Strong on disjunction explanation. Reasons not to pick first: pubgrub's cost model and rule encoding don't map cleanly onto our capability model (provides/requires/obsoletes/conflicts plus weak-deps); we'd have to encode capabilities as virtual packages and lose pubgrub's native explanation hooks.
• Custom solver from scratch. Out of scope. PROP-000 §15 ("dep weight not a decision factor") + §17 ("production architecture in prototype phase") both push us toward "use the best library, full stop."

26Rust FFI surface — minimal. We expose only the libsolv calls we use:

// crates/vibe-resolver-libsolv/src/ffi.rs (sketch)
extern "C" {
    fn pool_create() -> *mut Pool;
    fn pool_free(pool: *mut Pool);
    fn solver_create(pool: *mut Pool) -> *mut Solver;
    fn solver_solve(solver: *mut Solver, jobs: *mut Queue) -> c_int;
    fn solver_problem_count(solver: *mut Solver) -> c_int;
    fn solver_findproblemrule(solver: *mut Solver, problem: c_int) -> Id;
    fn solver_describe_decision(solver: *mut Solver, p: Id, info: *mut c_int) -> Id;
    // … 20-30 more, all from libsolv's stable public header `solv/*`
}

28Build-side: vendor libsolv as a git submodule (or fetch via build-script — preferred to avoid submodule fragility on Windows); compile with cc crate; link statically. Windows builds use the bundled C compiler from MSVC or MinGW (the same toolchains we already require for cargo build).

29Cargo features. A vibe-resolver-libsolv crate is gated behind a workspace-level feature so a contributor on a fresh checkout without a C toolchain can still build the rest of the workspace and run NaiveDepSolver for tests. CI builds with the feature on.

2.3 SAT solver capabilities we rely on

30These are the libsolv-provided algorithmic guarantees that make the rest of PROP-003 tractable. None of them are present in NaiveDepSolver today.

1. 31Conflict-driven clause learning (CDCL). When a [[requires_any]] choice contradicts later constraints, the solver backtracks, learns a clause excluding the bad combination, and tries an alternative. This is the table-stakes property NaiveDepSolver lacks.
2. Watched-literals propagation. O(literals × decisions) propagation cost rather than O(rules × decisions), keeping per-decision work near-constant on graphs with hundreds of capabilities.
3. Weak-deps semantics — the four levels libsolv inherited from RPM:
4. Recommends: prefer to install, but don't fail solve if impossible.
5. Suggests: hint to the user; never auto-installed.
6. Supplements: install me if some other package in the graph wants it.
7. Enhances: hint that I enhance another package; UI surface only.
8. These map onto vibevm [recommends] / [suggests] / [supplements] / [enhances] manifest sections (§2.9).
9. The crucial property: a missing [recommends] package is a warning, not an error — NaiveDepSolver cannot represent this distinction at all today.
10. Problem reporting (decision-tree explanation). When the graph is unsatisfiable, libsolv returns a structured Problem per conflict — naming the offending rules, the chain that led there, and a list of Solutions the user can apply (relax constraint X, drop package Y, accept downgrade Z). We map these to vibevm's existing SolveError variants and surface them in vibe install / vibe update.
11. Favor / disfavor / pin rules. libsolv accepts soft-preference rules: "if multiple solutions exist, prefer the one keeping <pkgref>@<version> installed." This is what pin_preferences rides on; it gives vibe update predictable minimum-churn behaviour even on graphs where an unrelated update opens new flexibility.
12. Multi-version / multi-arch handling we don't need today (RPM-specific) is left disabled — libsolv supports it but vibevm has no parallel concept (every install is single-version per (kind, name)).

32What we don't rely on from libsolv:

• 33RPM rich-dep boolean expressions ((A or B) in the Requires: field). Our [[requires_any]] covers the most common use case; richer logic can be added later if pulled by adoption.
• Module / stream / context machinery from dnf modules (it's RPM-specific and orthogonal to our subskill model — see §2.5).
• libsolv's repo-format readers (solv files, repomd.xml). Our MultiRegistryResolver already produces ResolvedNodes; we feed those into libsolv's pool, not the other way around.

2.4 Optional components (features) — cargo-tradition with vibevm twists

34Decision. A package's vibe-package.toml gains a [features] table describing optional, conditionally-activated components:

[features]
default = ["wal-protocol", "atomic-commits-section"]
wal-protocol = []                    # zero-cost feature toggle
atomic-commits-section = ["dep:flow-atomic-commits"]
llm-prompt-templates = ["subskill:llm-coordinator/anthropic"]
rust-stack = ["subskill:stack/rust"]
python-stack = ["subskill:stack/python"]

# Mutually exclusive — solver enforces. Named groups, not the
# underscore-prefixed sigil from revision r1; TOML-idiomatic.
[features.exclusive]
stacks = ["rust-stack", "python-stack"]

36Semantics — copied from cargo's feature resolver v2 with one reduction and one extension.

37The cargo subset we keep, verbatim:

• 38Additive only. Enabling a feature can introduce additional content; never remove or contradict existing content. (Cargo enforces this informally; vibevm enforces it via vibe check since spec content collisions are easier to detect than code-level ones.)
• Default features. default = [...] lists features active when no override is given. --no-default-features on the install / update CLI omits them.
• Feature-feature dependency. feat-A = ["feat-B"] — enabling A enables B transitively.
• Optional dep activation. A [dependencies.foo] optional = true entry creates an implicit feature named foo that activates the dep; alternatively the explicit dep:foo syntax in a feature list activates the dep without exposing the implicit feature name.
• Weak feature (cargo's dep?/feat syntax): feat-A = ["other-pkg?/some-feat"] — if other-pkg is already in the graph, request some-feat on it; otherwise no-op. The ? prevents activation-by-default of other-pkg.
• Per-target feature activation (cargo's [target."cfg(...)".dependencies] shape): for vibevm this maps onto [target."context(stack:rust)".dependencies] — see §2.6.
• Feature unification across the dep graph. If pkg-A and pkg-B both depend on pkg-C and request different features, the solver unifies — pkg-C is built/materialised once with the union of requested features.

39The cargo subset we drop:

• 40dev-dependencies / build-dependencies distinction. vibevm has no compile-time graph; a single category of deps suffices.
• Feature unification opt-out (resolver = "1" in cargo). vibevm always unifies (resolver v2 only).
• cfg(...) based feature gating on rustc target triple. vibevm replaces this with our own context predicates (§2.6).

41The vibevm-specific extension we add:

• 42Mutual exclusion via [features.exclusive] named groups — each value list is an at-most-one set, enforced by the SAT solver via direct conflict rules. cargo has no equivalent (because rustc cfg-conditioning makes mutual exclusion software-rebuilt, not solver-enforced); vibevm uses it for cross-cutting choices like rust-stack vs python-stack where both make sense individually but not together. Named groups (stacks = [...], languages = [...]) read better than r1's underscore-prefixed __exclusive = [[…], […]].
• Feature → subskill mapping. A feature can list subskill:<path> in its activation list, which directs the resolver to materialise the corresponding subskill (§2.5). This is the bridge between cargo-style features and vibevm-native subskill content.
• Feature visibility. Features prefixed with _ (underscore) are implementation details — invisible to consumer manifests; cannot be activated by name from outside the package. Cargo has an informal convention here; we make it solver-enforced.

2.5 Subskills — vibevm-native optional content units with three delivery modes

43Decision. A package may carry a subskills/ subtree alongside its top-level content:

flow-wal/
├── vibe-package.toml
├── README.md                        # canonical, always materialised
├── boot/10-flow-wal.md              # canonical, always materialised
├── spec/flows/wal/
│   ├── WAL-PROTOCOL.xml              # canonical, always materialised
│   └── morning-routine.xml           # canonical, always materialised
└── subskills/
    ├── stack/rust/
    │   ├── vibe-subskill.toml       # the subskill manifest
    │   ├── README.md
    │   └── rust-specific-protocol.md
    ├── stack/python/
    │   ├── vibe-subskill.toml
    │   └── python-specific-protocol.md
    ├── feature/atomic-only/
    │   ├── vibe-subskill.toml
    │   └── atomic-commits-addendum.md
    └── llm-coordinator/anthropic/
        ├── vibe-subskill.toml
        └── claude-prompt-templates.md

45A subskill is the smallest activatable content unit inside a package. Structurally it looks like a tiny package: own manifest, own files, own optional further subskill children (§2.5.5). What changes per subskill is the delivery mode (§2.5.0 below) and the activation rules (§2.5.2): together they decide when the subskill's content reaches the agent and how.

[subskill]
path = "stack/rust"                   # canonical addressable name within parent package
summary = "Rust-specific guidance for the WAL flow"

# Natural-language activation trigger — load-bearing for `lazy-push` mode
# and `vibe-mcp` exposure. Required for delivery = "lazy-push" /
# "lazy-pull"; recommended for delivery = "eager" so `vibe-mcp` /
# `vibe show subskills` can describe what the subskill is for. Style:
# "When you ...". Specificity beats verbosity — the agent matches this
# against task / files / conversation, so vague triggers ("about Rust")
# trip on every Rust-adjacent task; concrete triggers ("when adding a
# new WAL checkpoint to a Rust project that uses sqlx for storage")
# only fire when the situation actually applies. `vibe review` scores
# this string under the "activation" axis.
description = """
When you are adding or modifying WAL checkpoints in a Rust project,
especially when using sqlx, diesel, or similar SQL libraries, and need
the Rust-specific naming, error-handling, and trace-id conventions
that complement the canonical WAL protocol.
"""

# How this subskill reaches the agent. See §2.5.0.
delivery = "lazy-push"   # one of: "eager", "lazy-push", "lazy-pull"

# Optional: pin this subskill to an upstream OSS package version. PURL
# syntax (https://github.com/package-url/purl-spec). Set when the
# content is genuinely version-specific to the upstream library —
# e.g. a Rust-stack subskill that documents a sqlx 0.8 API. See
# §2.5.6.
describes = "pkg:cargo/sqlx@0.8.0"

# Activation rules — any one matches → subskill is active.
# Channels described in §2.5.2.
[activation]
# Manual: parent package's [features] map a feature name to this path.
# (No declaration needed here — the parent's [features] table holds
# the linkage. Stated for documentation only.)

# Context-based: capabilities/interfaces/files/commands/env/PURL match.
context.if_present = ["stack:rust"]
context.if_provides = ["interface/build-system"]
context.if_files = ["**/Cargo.toml"]
context.if_command = ["cargo"]
context.if_env = ["RUST_LOG"]
context.if_os = ["linux", "macos"]           # OS scope — the same probe
                                              # the [boot_snippet] `when`
                                              # gate ships (PROP-009 §2.4).
context.if_describes_match = true            # match if any package in
                                              # the graph `describes` an
                                              # upstream PURL whose `type`
                                              # equals this subskill's
                                              # `describes` type
                                              # (e.g. pkg:cargo/*).
context.if_language = ["en", "ru"]

# LLM-inferred activation: the post-M1.5 LLM build pipeline can emit
# *virtual* capabilities into the dep graph (§2.5.3), which then
# activate this subskill through the normal `if_present` /
# `if_provides` channels. Set `context.allow_llm_emission = false` to
# refuse virtual capabilities for this subskill specifically (default
# true — opt-out, not opt-in).
context.allow_llm_emission = true

# Soft-preference: if activated alongside any of these, prefer to also
# activate them (libsolv-Recommends-style).
[recommends]
subskills = ["feature/atomic-only"]

# Hard exclusion: never activate alongside any of these.
[conflicts]
subskills = ["stack/python"]

# Files this subskill ships, relative to its own root.
[content]
files_written = [
    "spec/flows/wal/rust-specific-protocol.md",
    "spec/boot/15-flow-wal-rust.md",        # boot-snippet prefix MUST not collide
                                            # with anything else in scope; vibe-check
                                            # gates this at install time.
]

2.6 Capability-based interface tags — the abstract layer

71Decision. Extend PROP-002 §2.9's [provides] / [requires] capability surface with a new concept: interface tags.

[provides]
# concrete package identity (existing)
flow:wal = "0.1.0"
# capability provided (existing)
"capability:wal-protocol" = "*"
# NEW: interface tag — abstract role this package fills
"interface:build-system" = "*"
"interface:auth-provider" = "*"

[requires]
# require a concrete package or capability (existing)
flow:wal = "^0.1"
# NEW: require some package that fills an interface, regardless of name
"interface:build-system" = "*"

74Interface tags differ from capabilities in two ways:

1. 75Abstraction over name. A package requiring interface:build-system doesn't care whether the consumer has stack:rust-cargo, stack:python-poetry, or stack:nix-flake; any of them with [provides] matching the interface satisfies. Capabilities (capability:wal-protocol) tend to be more specific and authored together.
2. Discovery surface. Subskills can context.if_provides against an interface to auto-activate when the consumer happens to have any package fulfilling the role. Capabilities are matched against [requires] only.

76Naming convention. Interface tags use the interface:<name> namespace. The <name> segment uses - for word boundaries (kebab-case), / for category nesting (interface:storage/sql, interface:storage/key-value). Solver treats them as opaque strings; no semantic meaning beyond match/no-match.

77Provenance. Both [provides] and [requires] interface tags are user-authored (no LLM inference). The author is making an intentional declaration about an architectural role; that's not a thing the LLM should be guessing at. Note: §2.5.3 introduces virtual capabilities the LLM may emit at runtime (post-M1.5) — those flow through a different channel and never persist into the package manifest.

2.6.1 Conditional dependencies — [target."context(...)".dependencies]

78Decision. Beyond subskill activation (which controls content within an active package), vibevm gains conditional dependencies (which control whether a package is in the graph at all), modelled on Cargo's [target."cfg(...)".dependencies] shape but predicated on vibevm's context probes rather than rustc target triples:

[target."context(stack:rust)".dependencies]
flow:rust-best-practices = "^0.1"
flow:cargo-discipline = "^0.1"

[target."context(if_files = '**/Dockerfile')".dependencies]
flow:container-best-practices = "^0.1"

[target."context(if_provides = 'interface:database-migrations')".dependencies]
flow:migration-discipline = "^0.1"

2.7 Internationalization (i18n) — multi-language package content

90Decision. Adopt a sidecar file naming pattern with BCP-47 language tags as suffixes, plus first-class language-preference declarations at three levels (CLI flag, project manifest, package manifest).

flow-wal/
├── README.md                        # canonical (default language: en)
├── README.ru.md                     # Russian translation
├── README.ja.md                     # Japanese translation
├── boot/
│   ├── 10-flow-wal.xml               # canonical
│   └── 10-flow-wal.ru.md            # Russian
└── spec/flows/wal/
    ├── WAL-PROTOCOL.xml
    ├── WAL-PROTOCOL.ru.md
    └── morning-routine.xml           # only canonical — no translation yet, fallback used

  [i18n]
  preferred = "ru"
  fallback = ["en"]    # if a package has no `ru`, try `en` before erroring;
                       # default behaviour is the same — explicit form for clarity

  [i18n]
  canonical = "en"           # default; the form filenames-without-suffix carry
  available = ["en", "ru"]   # `ja` is in our fixture above but not declared here:
                             # vibe check would warn that `README.ja.md` is unindexed

[package]
name = "wal"
kind = "flow"
version = "0.1.0"
description = "Append-only checkpoint protocol"
description.ru = "Протокол append-only-чекпоинтов"
description.ja = "追記専用チェックポイント・プロトコル"

[features.rust-stack]
description = "Rust-specific guidance for WAL"
description.ru = "Руководство по WAL для проектов на Rust"

description = { en = "Append-only checkpoint protocol", ru = "Протокол ..." }

[package.description]
en = "Append-only checkpoint protocol"
ru = "Протокол append-only-чекпоинтов"
ja = "追記専用チェックポイント・プロトコル"

[meta]
schema_version = 2
language = "ru"
language_fallback = ["en"]
# shipped shape: schema_version = 5, language_chain = ["ru", "en"]

2.8 Manifest schema additions — the consolidated picture

116Pulling together every section above, the v0.2 package schema looks like the fence below. Two r1 leftovers survive in it and are not the shipped grammar: the __exclusive = [[…]] sigil was replaced by named [features.exclusive] groups in r2's own §2.4, and the manifest file itself is vibe.toml's [package] section, not the retired vibe-package.toml:

[package]
name = "wal"
kind = "flow"
version = "0.1.0"
description = { en = "Append-only checkpoint protocol", ru = "Протокол ..." }

[i18n]
canonical = "en"
available = ["en", "ru"]

[provides]
flow:wal = "0.1.0"
"capability:wal-protocol" = "*"
"interface:checkpointing" = "*"

[requires]
"interface:build-system" = "*"

[[requires_any]]
one_of = [
    { "stack:rust-cargo" = "^0.1" },
    { "stack:python-poetry" = "^0.1" },
]

[recommends]
flow:git-atomic-commits = "^0.1"

[suggests]
flow:sync-from-code = "^0.1"

[supplements]
"capability:claude-coordinator" = "*"

[enhances]
"capability:llm-build-pipeline" = "*"

[obsoletes]
flow:wal-legacy = "<0.1"

[conflicts]
flow:wal-experimental = "*"

[features]
default = ["wal-protocol"]
wal-protocol = []
atomic-commits-section = ["dep:flow-atomic-commits"]
rust-stack = ["subskill:stack/rust"]
python-stack = ["subskill:stack/python"]
__internal-helper = []          # underscore-prefixed: implementation detail

__exclusive = [["rust-stack", "python-stack"]]

[content]
files_written = [
    "spec/flows/wal/WAL-PROTOCOL.md",
    "spec/flows/wal/morning-routine.md",
    "spec/boot/10-flow-wal.md",
]

118Each subskill carries its own vibe-subskill.toml per §2.5.1.

119deny_unknown_fields everywhere — vibevm never silently drops unfamiliar manifest keys; we'd rather fail loud and add the section to the schema than corrupt provenance.

2.9 Lockfile schema impact (v3)

120The lockfile gains:

• 121[meta].language_chain (§2.7.5) — shipped as one ordered field merging the preference and its fallback, not the language + language_fallback pair this section drafted.
• [meta].active_features = [...] — full list of features active in the resolution. Per-package activation goes under each [[package]] entry.
• [meta].virtual_capabilities = [...] — capabilities emitted by the LLM during resolution (§2.5.3). Each entry carries name, emitter (the LLM provider/model identifier), trace_id (link into the audit log), and emitted_at.
• [[package]] entries gain features = ["..."], subskills_active = [...] (with each entry being { path = "stack/rust", delivery = "lazy-push" } so the materialisation behaviour is reproducible) and the latter's delivery mode persisted because eager / lazy-push / lazy-pull are operationally distinct on the consumer side.
• [[package]] entries gain optional language field if the package was materialised in a non-canonical language (otherwise inherits [meta].language).
• [[package]] and per-subskill entries gain optional describes PURL when set in the source manifest.

[meta]
schema_version = 3
solver = "sat"
language = "ru"
language_fallback = ["en"]
active_features = ["flow:wal/wal-protocol", "flow:wal/rust-stack", "flow:git-atomic-commits/atomic-commits-section"]
root_dependencies = ["flow:wal", "flow:git-atomic-commits"]

[[package]]
kind = "flow"
name = "wal"
version = "0.1.0"
registry = "vibespecs"
source_url = "https://github.com/vibespecs/flow-wal.git"
source_ref = "v0.1.0"
content_hash = "sha256:8136..."
features = ["wal-protocol", "rust-stack"]
subskills_active = ["stack/rust"]
language = "ru"
boot_snippet = "10-flow-wal.xml"
files_written = [
    "spec/flows/wal/WAL-PROTOCOL.md",      # written from WAL-PROTOCOL.ru.md (or canonical fallback)
    "spec/flows/wal/morning-routine.md",
    "spec/flows/wal/rust-specific-protocol.md",   # from subskills/stack/rust/
    "spec/boot/10-flow-wal.md",
    "spec/boot/15-flow-wal-rust.md",              # from subskill
]

123schema_version = 3 triggers the v2 → v3 read-side migration on next vibe install. Schema-write side is unconditional v3 once this PROP lands — pre-release, no migration burden.

2.10 CLI surface — additions and adjustments

124New flags / commands:

• 125vibe install <pkgref> [--features <a,b,c>] [--no-default-features] [--all-features] — control feature activation (cargo-shape).
• vibe install <pkgref> [--language <bcp47>] — override resolved language for this install.
• vibe show features <pkgref> — list the package's features, default state, current activation in the project.
• vibe show subskills <pkgref> — list the package's subskills, activation state with reason ("active because feature rust-stack", "active because stack:rust is in the project", "available but not active", "would-activate-if-LLM-build" — post-M1.5).
• vibe check's existing checks gain four new entries (numbered per VIBEVM-SPEC §12 expansion):
• i18n coverage: every file declared in [content].files_written exists for the package's canonical language; missing translations warn (not error) per language declared in [i18n].available.
• subskill structure: subskill manifests parse, activation rules are valid (if_present references exist, if_provides interface tags are well-formed, if_files glob patterns parse, delivery is one of the three allowed values, description is present when delivery ∈ {lazy-push, lazy-pull}).
• feature graph: feature activations don't form cycles, exclusion sets are not violated by default, every subskill:<path> reference resolves to a real subskill in the package.
• activation conflict: subskill description triggers don't materially overlap. Detection runs an LLM-judge (when available) or a heuristic substring-overlap pass (in vibe check's static mode) over every pair of subskills with delivery ∈ {lazy-push, lazy-pull} in the same package, flagging pairs whose triggers contain ≥75% of each other's content keywords. Mirrors Tessl's review-rubric "activation distinctiveness" axis (research at PROP-004 §2.11). Authors are expected to either tighten one description or merge the two subskills.

126Existing flags pick up new behaviours:

• 127vibe update --features <list> — re-resolve with a different feature set. Specified, not shipped: the install-side --features is live, but the update-side re-resolve was never wired (vibe update --help carries only all / json / path / quiet plus the global flags).
• vibe show config exposes the resolved language preference and its provenance per the existing precedence chain.
• vibe show effective materialises the effective spec at the project's resolved language, falling back per §2.7.2; --all-languages shows every available language side-by-side (debugging aid).

2.11 Migration path from NaiveDepSolver

128The codebase has no shipped users; migration is internal. Order:

1. 129Land libsolv FFI (crates/vibe-resolver-libsolv) and SatDepSolver impl behind a trait. Naive stays the default.
2. Land manifest schema additions (§2.8) without runtime activation logic — parser-only. Existing manifests parse unchanged.
3. Land features semantics in SatDepSolver (rule encoding, solving, activation map); vibe install --features and --no-default-features start working. Naive remains feature-blind.
4. Land subskill materialisation in vibe-install: walk activation rules post-solve, write subskill files, integrity-check (boot collision, file collision).
5. Land i18n resolution in vibe-install: at file-write time, walk the language fallback chain. CLI flag wired.
6. Switch default solver — executed, but to resolvo, not sat: PROP-017 reversed the engine call before this step ran, and runtime resolution defaults to resolvo in the R-001 selection seam. Naive remains for fixtures/tests exactly as written.
7. Lockfile v3 migration on read; unconditional v3 write.

130Each step is its own PR, lockfile-shape-stable mid-step (we control the format pre-release; if a step needs to break, we break and don't carry compatibility).

3.1 Rule encoding — vibevm concepts → libsolv rules

131libsolv's solver is rule-based: every constraint becomes a clause in the SAT problem. We map our concepts:

133This is the same encoding dnf5 uses for RPM weak-deps; we just reuse the RULE_* constants from libsolv's public solv/solver.h.

3.2 Solver phases

134For one vibe install invocation:

1. 135Pool population. Walk MultiRegistryResolver::list_versions for every root and transitively-discovered package. Each (kind, name, version) becomes a libsolv solvable; capabilities/interfaces become provides relations; deps become requires relations. Known-version cache from PROP-002 §2.4 cuts repeat lookups.
2. Job formulation. Each root pkgref becomes a SOLVER_INSTALL | SOLVER_SOLVABLE_NAME job with version constraint. Active features become enabling literals on root solvables.
3. Rule materialisation. Encode every constraint above as libsolv rules.
4. Solve. solver_solve() runs CDCL. On unsat, walk problems with solver_problem_count() → solver_findproblemrule() → reconstruct vibevm-shape SolveError::Unsatisfiable { problems: Vec<Problem> } for the CLI to render.
5. Decoding. Walk solver_get_decisionqueue() to extract the chosen solvables, decode back into ResolvedNodes with the version + features picked.
6. Subskill projection. For each resolved package, evaluate its subskills' context.if_present and if_provides rules against the full graph. Set activation flags. (No SAT round-trip; this is a deterministic post-pass.)
7. Materialisation handoff. vibe-install reads the final node list (with feature + subskill flags) and walks the i18n fallback at file-write time.

3.3 Determinism

136libsolv's solver is deterministic for a fixed pool, fixed jobs, fixed rules — it does not use randomness or wall-clock-driven heuristics. Two solves with the same inputs produce the same result. This is a property we explicitly rely on for cargo xtask check-codegen-style drift checks: vibe check --simulate-install <pkgref> should produce a stable hash per (manifest, lockfile) pair. We test this via a fixture-driven integration test that runs the same install N times and asserts identical lockfile bytes.

3.4 Performance envelope

137libsolv is the engine YUM and DNF have used for ~15 years against repos with 50K+ packages and conflict-rich constraint sets. vibevm's expected scale (hundreds of packages, tens of features per package, depth-3 graphs typical) is comfortably within the linear regime. We don't anticipate performance pressure from libsolv; we anticipate it from the registry-fetch layer (network bound), which is unchanged.

138The Rust FFI cost is negligible — one solver_solve() call per vibe install invocation; everything else is in-process.

4.1 resolvo as primary SAT engine

140Already covered in §2.2. Re-stated for completeness: pure-Rust appeal is real, but libsolv's battle-testing, weak-deps semantics, and rule-introspection wins for v1. resolvo remains a viable second impl.

4.2 Pubgrub as primary SAT engine

141Pubgrub's contribution (incremental version solving with native disjunction explanation) is genuinely best-in-class for SemVer-shaped constraints — Cargo's adoption is the existence proof. But pubgrub's data model assumes constraints are version ranges over named packages; capability/interface/virtual-package shapes need to be encoded as synthetic packages, and pubgrub's explanation hooks degrade when synthetic packages dominate the unsat core. Once the encoding is shoehorned in, the explanation quality slips below libsolv's. Door left open via DepSolver trait.

4.3 Composite content via packages-only (no subskills)

142i.e. split flow:wal into N packages instead of one with subskills. Already covered in §2.5.4 (the rationale moved there when r2 inserted the LLM virtual-capabilities section at §2.5.3). Discoverability + cohesion losses outweigh the schema simplicity.

4.4 _<lang> filename suffix instead of .<lang>

143Already covered in §2.7.1. Case-folding bugs and BCP-47 incompatibility are dealbreakers.

4.5 Whole-language directory pattern (i18n/<lang>/<canonical-tree>)

144Already covered in §2.7.1. Path-depth doubling and filesystem-watch fragility are real costs; the operational wins of sidecar-per-file outweigh the grouping benefit of per-language trees. A package can still have a per-language directory under subskills/ (e.g. subskills/i18n/ru-extras/) if it wants to ship language-specific content (not translation) — but that's subskills, not the i18n mechanism.

4.6 LLM-driven inference of [provides] / [requires] / interfaces

145Tempting: the LLM reads the package and infers what it provides. We don't do it. [provides] is an architectural commitment and authorship matters — having the author intentionally declare interfaces is the only way the system stays auditable. The LLM channel is reserved for activation (which subskills to materialise) where the author has already declared the option space.

4.7 Inline-key i18n for entire markdown files

146description = { en = "...", ru = "..." } works for short strings but doesn't scale to multi-paragraph documents (TOML strings without escapes are awkward; multiline literal strings disrupt the toml-edit roundtrip). Sidecar files are the right unit at the document level.

4.8 Multiple solvers concurrently selectable per-package

147A package declaring [meta] solver = "naive" for itself while the rest of the graph uses sat — rejected. Single-solver-per-resolution keeps semantics consistent.

Phase A — solver swap with no semantic change

• 150libsolv FFI crate.
• SatDepSolver impl matching NaiveDepSolver's output on all fixture graphs.
• Naive stays default; --solver sat opt-in.
• Acceptance: every existing test passes with --solver sat and --solver naive.

Phase B — features (cargo subset)

• 151Manifest schema for [features].
• Feature activation in solver, lockfile v3 records.
• --features / --no-default-features / --all-features CLI flags.
• Acceptance: a feat that depends on flow:wal with --features rust-stack materialises the rust-specific files; without the flag, those files are absent.

Phase C — subskills (manual + context-based + three delivery modes)

• 152Subskill manifest format, package layout convention.
• Manifest fields: delivery, description, describes, full [activation] probe set (if_present / if_provides / if_files / if_command / if_env / if_describes_match / if_language).
• Manual feature → subskill mapping (Phase B's hooks).
• Context-based activation post-pass: probes evaluated against the resolved graph + project tree + machine state.
• Eager-mode materialisation in vibe-install. Lazy-push / lazy-pull modes plumb through but require vibe-mcp (M1.7) to be useful — when M1.7 hasn't landed, the modes degrade to eager with a tracing::warn! so the consumer is never silently broken.
• vibe show subskills CLI.
• Acceptance: a package with subskills/stack/rust/ (delivery=eager) activates under a stack:rust project without explicit user opt-in. A package with subskills/sqlx-0.8/ (delivery=lazy-push, describes=pkg:cargo/sqlx@0.8.0) does NOT materialise files but registers itself for vibe-mcp exposure once M1.7 is in. Activation-conflict check fires when two lazy-push subskills' descriptions overlap.

Phase D — i18n

• 153BCP-47 sidecar file resolution.
• Manifest field translations (dotted-key form).
• --language flag, [i18n] blocks at project/package level.
• Lockfile v3 records resolved language.
• Acceptance: vibe install flow:wal --language ru against a package shipping Russian translations writes the Russian files; --language en writes the canonical; --language ja (no translation in this package) writes the canonical with a tracing::info! "language ja not available, using en fallback".

Phase E — switch default solver to SAT

• 154Default flips — to resolvo, in the R-001 selection seam (PROP-017 DONE-DEFAULT-FLIP; --solver's help reads "Defaults to resolvo"). The sat this line named was superseded before the flip shipped.
• Naive demoted to "tests + small graphs" path.
• Acceptance: clean runs of every smoke (M1.5-gate-v2, M1.6-mirror-vendor, plus new feature/subskill smokes) green on fresh install.

Phase F — LLM-emitted virtual capabilities (post-M1.5)

• 155Wire into the vibe build LLM tool-use loop.
• LLM is invoked with the effective spec + project context + a request to emit virtual capabilities (§2.5.3).
• Subskills with matching if_present / if_provides rules activate through the normal channel.
• Audit surface: every emission logs (name, emitter, trace_id, reasoning) to the lockfile's [meta].virtual_capabilities. vibe show effective annotates virtually-emitted capabilities with [virtual via LLM].
• Project-level policy: [llm].emission.allowed_namespaces = ["capability:*", "interface:*"] (default — generous; restrict by namespace if security-sensitive). Per-subskill context.allow_llm_emission = false is the per-subskill opt-out, but most subskills won't need it because they simply don't declare if_present against the LLM-emission namespace.
• Acceptance: a feat:welcome-page × stack:rust build emits interface:llm-coordinator based on detecting an LLM-mediated workflow, which activates the flow:wal/llm-coordinator/anthropic subskill via its if_provides = ["interface:llm-coordinator"] rule, and the lockfile records the emission with full audit trail.