assets/dry-run-formalism.svg
<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 1200 1180" font-family="'DejaVu Sans', 'Segoe UI', sans-serif">
<defs>
<linearGradient id="board" x1="0" y1="0" x2="0" y2="1"><stop offset="0" stop-color="#0b1c2e"/><stop offset="1" stop-color="#06111d"/></linearGradient>
<linearGradient id="rail" x1="0" y1="0" x2="0" y2="1"><stop offset="0" stop-color="#173d57"/><stop offset="1" stop-color="#0c2438"/></linearGradient>
<linearGradient id="slot" x1="0" y1="0" x2="0" y2="1"><stop offset="0" stop-color="#123448"/><stop offset="1" stop-color="#0a2032"/></linearGradient>
<linearGradient id="chip" x1="0" y1="0" x2="0" y2="1"><stop offset="0" stop-color="#14384f"/><stop offset="1" stop-color="#0e2a3e"/></linearGradient>
</defs>
<style>
.mono{font-family:'DejaVu Sans Mono','SF Mono',monospace;}
.h{fill:#eaf6ff;font-weight:700;} .sub{fill:#9fc9e0;} .dim{fill:#86b3cc;} .code{fill:#bfe6ff;} .amb{fill:#f0cf94;} .ambd{fill:#c8b183;} .ok{fill:#8fe0a8;} .warn{fill:#f0a9a9;}
.sec{fill:#7fbfe0;font-weight:700;}
</style>
<rect x="0" y="0" width="1200" height="1180" fill="url(#board)"/>
<g stroke="#143a52" stroke-width="1"><line x1="0" y1="78" x2="1200" y2="78"/><line x1="0" y1="1132" x2="1200" y2="1132"/></g>
<g fill="#16415c"><circle cx="40" cy="40" r="2"/><circle cx="1160" cy="40" r="2"/><circle cx="40" cy="1152" r="2"/><circle cx="1160" cy="1152" r="2"/></g>
<text class="h" x="40" y="44" font-size="22">Dwarves release</text>
<text class="sub" x="272" y="44" font-size="14.5">the formal model — a <tspan class="code" font-weight="700">feature-conditional dependency multi-graph</tspan>, proven by two gates</text>
<text class="dim mono" x="40" y="66" font-size="11">Package Calculus (Gibb 2026) + a 4th condition, Feature-Availability · version solving = SAT/CDCL (EDOS→Mancoosi, PubGrub) · Tarjan SCC · Sugiyama drawing</text>
<!-- §1 THE GRAPH -->
<rect x="36" y="94" width="1128" height="196" rx="12" fill="url(#rail)" stroke="#7fc8ea" stroke-width="2"/>
<text class="sec" x="56" y="122" font-size="15">§1 · the graph</text>
<text class="code mono" x="56" y="150" font-size="15">G = (V, E)</text>
<text class="dim" x="180" y="150" font-size="12">directed, feature-conditional, multi-edge (a pair of crates may share several kinds of edge)</text>
<rect x="56" y="164" width="536" height="106" rx="8" fill="url(#slot)" stroke="#6fd3f5" stroke-width="1.4"/>
<text class="h" x="72" y="186" font-size="12.5">node — a crate <tspan class="mono code">v ∈ V</tspan></text>
<text class="code mono" x="72" y="210" font-size="12">v = ( name, version, F(v), publishable )</text>
<text class="dim" x="72" y="232" font-size="11"><tspan class="mono code">F(v)</tspan> = the set of features v DECLARES · <tspan class="mono code">A(v) ⊆ F(v)</tspan> = features ACTIVE in a build</text>
<text class="dim" x="72" y="252" font-size="11"><tspan class="mono code">publishable</tspan> = false when <tspan class="mono">publish = false</tspan> / <tspan class="mono">release = false</tspan></text>
<rect x="612" y="164" width="552" height="106" rx="8" fill="url(#slot)" stroke="#6fd3f5" stroke-width="1.4"/>
<text class="h" x="628" y="186" font-size="12.5">edge — a dependency <tspan class="mono code">e ∈ E</tspan></text>
<text class="code mono" x="628" y="210" font-size="12">e = ( u, v, req, Φ, kind, cond )</text>
<text class="dim" x="628" y="232" font-size="11"><tspan class="mono code">req</tspan> semver interval · <tspan class="mono code">Φ ⊆ F(v)</tspan> features required on v · <tspan class="mono">kind ∈ {normal,build,dev}</tspan></text>
<text class="dim" x="628" y="252" font-size="11"><tspan class="mono code">cond ⊆ F(u)</tspan> = features of u that ACTIVATE this (optional) edge; ∅ if non-optional</text>
<!-- §2 FEATURE ACTIVATION -->
<rect x="36" y="304" width="1128" height="182" rx="12" fill="url(#rail)" stroke="#7fc8ea" stroke-width="2"/>
<text class="sec" x="56" y="332" font-size="15">§2 · feature activation — a least fixed-point</text>
<text class="dim" x="470" y="332" font-size="11">(features turn on optional edges, which require more features … so solve globally)</text>
<rect x="56" y="346" width="640" height="124" rx="8" fill="url(#slot)" stroke="#6fd3f5" stroke-width="1.4"/>
<text class="code mono" x="72" y="370" font-size="12.5">an edge is ACTIVE: Active(e) ⇔ cond = ∅ ∨ cond ⊆ A(u)</text>
<text class="dim" x="72" y="392" font-size="11">propagation step T over the active-feature map A:</text>
<text class="code mono" x="72" y="414" font-size="12">T(A)[v] = A[v] ∪ ⋃ₓ { Φₑ ∪ (default(v) unless no-default) }</text>
<text class="dim mono" x="72" y="432" font-size="10.5"> over every Active(e), e = (u→v) , seeded with the entry crates' default features</text>
<text class="dim" x="72" y="456" font-size="11">T is monotone on the powerset lattice ⇒ Knaster–Tarski gives a unique <tspan class="ok">least fixed point A* = lfp(T)</tspan></text>
<rect x="712" y="346" width="452" height="124" rx="8" fill="url(#chip)" stroke="#5aa6cf" stroke-width="1.6"/>
<text class="h" x="728" y="368" font-size="12">why it matters</text>
<text class="dim" x="728" y="390" font-size="11">a version requirement is NOT enough — an edge also</text>
<text class="dim" x="728" y="406" font-size="11">carries <tspan class="code mono">Φ</tspan>, and a feature can pull in a whole</text>
<text class="dim" x="728" y="422" font-size="11">optional subtree. Resolve with the UNIFIED A*</text>
<text class="dim" x="728" y="438" font-size="11">(cargo resolver v2), the same set the build uses.</text>
<text class="warn" x="728" y="458" font-size="11">the <tspan class="mono">holger-server-lib/online</tspan> miss lives here.</text>
<!-- §3 THE FOUR CONDITIONS -->
<rect x="36" y="500" width="1128" height="190" rx="12" fill="url(#rail)" stroke="#e0b366" stroke-width="2.2"/>
<text class="amb" x="56" y="528" font-size="15" font-weight="700">§3 · a resolution is VALID iff all four hold</text>
<text class="dim" x="470" y="528" font-size="11">(Package Calculus' three + Dwarves' fourth)</text>
<rect x="56" y="542" width="266" height="134" rx="8" fill="url(#slot)" stroke="#e0b366" stroke-width="1.3"/>
<text class="amb" x="70" y="564" font-size="12.5" font-weight="700">1 · Root Inclusion</text>
<text class="ambd" x="70" y="588" font-size="11">every target crate to release</text>
<text class="ambd" x="70" y="604" font-size="11">is in the resolution set R.</text>
<rect x="336" y="542" width="266" height="134" rx="8" fill="url(#slot)" stroke="#e0b366" stroke-width="1.3"/>
<text class="amb" x="350" y="564" font-size="12.5" font-weight="700">2 · Dependency Closure</text>
<text class="ambd mono" x="350" y="588" font-size="10.5">∀ active e=(u,v,req):</text>
<text class="ambd mono" x="350" y="606" font-size="10.5">∃ chosen ver(v) ∈ req</text>
<text class="ambd" x="350" y="626" font-size="10.5">every dep is satisfied.</text>
<rect x="616" y="542" width="266" height="134" rx="8" fill="url(#slot)" stroke="#e0b366" stroke-width="1.3"/>
<text class="amb" x="630" y="564" font-size="12.5" font-weight="700">3 · Version Uniqueness</text>
<text class="ambd" x="630" y="588" font-size="11">exactly ONE version per</text>
<text class="ambd" x="630" y="604" font-size="11">crate name is selected</text>
<text class="ambd" x="630" y="620" font-size="11">(no duplicate runtimes).</text>
<rect x="896" y="542" width="268" height="134" rx="8" fill="url(#slot)" stroke="#8fe0a8" stroke-width="1.8"/>
<text class="ok" x="910" y="564" font-size="12.5" font-weight="700">4 · Feature Availability</text>
<text class="dim" x="910" y="582" font-size="9.5">Dwarves' contribution</text>
<text class="code mono" x="910" y="606" font-size="11">Active(e) ⇒ Φ ⊆ F(v)</text>
<text class="ambd" x="910" y="628" font-size="10.5">v must EXPOSE every</text>
<text class="ambd" x="910" y="644" font-size="10.5">feature the edge needs.</text>
<!-- §4 VERIFICATION THEOREM -->
<rect x="36" y="704" width="1128" height="118" rx="12" fill="url(#chip)" stroke="#7fc8ea" stroke-width="2"/>
<text class="sec" x="56" y="732" font-size="15">§4 · the Verification Theorem (Gate A, static)</text>
<text class="code mono" x="56" y="766" font-size="14">valid(R) ⇔ ∀ active e = (u, v, req, Φ, kind∈{normal,build}) : Vplan(v) ∈ req ∧ Φ ⊆ F( v @ Vplan(v) )</text>
<text class="dim" x="56" y="792" font-size="11.5">checked over the merged graph in-memory, in milliseconds — NO compiler. dev edges are stripped on publish and never constrain the order.</text>
<text class="dim" x="56" y="810" font-size="11.5">a failed clause prints its PubGrub derivation (which requirement, which feature, which consumer) — the needle, not the haystack.</text>
<!-- §5 TWO-GRAPH MERGE + THREE PROOFS -->
<rect x="36" y="836" width="1128" height="160" rx="12" fill="url(#rail)" stroke="#7fc8ea" stroke-width="2"/>
<text class="sec" x="56" y="864" font-size="15">§5 · the two-graph merge — three proofs</text>
<text class="code mono" x="440" y="864" font-size="14">G = G_io ⊕ G_src</text>
<text class="dim" x="600" y="864" font-size="11">crates.io reality ⊕ local source</text>
<rect x="56" y="878" width="356" height="100" rx="8" fill="url(#slot)" stroke="#e0b366" stroke-width="1.4"/>
<text class="amb" x="72" y="900" font-size="12.5" font-weight="700">(a) resolvable</text>
<text class="ambd" x="72" y="922" font-size="11">§4 holds over G — versions &</text>
<text class="ambd" x="72" y="938" font-size="11">features. <tspan class="h">Gate A</tspan>, static proof.</text>
<text class="dim mono" x="72" y="962" font-size="10">PubGrub interval CSP + Feature-Availability</text>
<rect x="422" y="878" width="356" height="100" rx="8" fill="url(#slot)" stroke="#6fd3f5" stroke-width="1.4"/>
<text class="code" x="438" y="900" font-size="12.5" font-weight="700">(b) acyclic after condensation</text>
<text class="dim" x="438" y="922" font-size="11">Tarjan SCC → condense → a topo</text>
<text class="dim" x="438" y="938" font-size="11">order EXISTS (Kahn). A DAG.</text>
<text class="dim mono" x="438" y="962" font-size="10">crate-level interleave inside a repo-SCC</text>
<rect x="788" y="878" width="376" height="100" rx="8" fill="url(#slot)" stroke="#8fe0a8" stroke-width="1.6"/>
<text class="ok" x="804" y="900" font-size="12.5" font-weight="700">(c) constructively valid</text>
<text class="dim" x="804" y="922" font-size="11">it actually BUILDS + publishes the whole</text>
<text class="dim" x="804" y="938" font-size="11">cascade into a throwaway registry. <tspan class="h">Gate B</tspan>.</text>
<text class="dim mono" x="804" y="962" font-size="10">served holger /sparring · deps-first · wait-for-index</text>
<!-- §6 ALGORITHM STACK -->
<rect x="36" y="1010" width="1128" height="104" rx="12" fill="url(#chip)" stroke="#5aa6cf" stroke-width="1.8"/>
<text class="sec" x="56" y="1036" font-size="14">§6 · the algorithm stack</text>
<g font-size="10.5">
<text class="code mono" x="56" y="1060">Tarjan SCC</text><text class="dim" x="56" y="1076">O(V+E) linear</text>
<text class="code mono" x="216" y="1060">condensation</text><text class="dim" x="216" y="1076">quotient → DAG</text>
<text class="code mono" x="376" y="1060">Kahn topo</text><text class="dim" x="376" y="1076">O(V+E) order</text>
<text class="code mono" x="536" y="1060">MFAS (Eades)</text><text class="dim" x="536" y="1076">NP-hard; m/2−n/6 greedy advisory</text>
<text class="code mono" x="820" y="1060">PubGrub / CDCL</text><text class="dim" x="820" y="1076">version SAT + explanation</text>
<text class="code mono" x="1010" y="1060">Sugiyama</text><text class="dim" x="1010" y="1076">layered drawing</text>
</g>
<text class="dim" x="40" y="1152" font-size="10">G_io = crates.io reality · G_src = local source · Φ = features an edge requires · A* = least-fixed-point active features · R = the resolution set · Vplan = planned publish version</text>
</svg>