Resolver.jl: harness measuring independent-conflict composition (second-order conflicts)

harness.jl

# How often does fixing every independent conflict actually finish the job?
#
# For each multi-conflict failing query:
#   * per-conflict repair menus (MCSes over that cluster + the emptied packages)
#   * ONE-EACH: pick one repair per conflict, apply them together, resolve.
#     SAT => that combination is a complete fix; UNSAT => second-order conflicts.
#     Sampled over several choices, since the answer may depend on which.
#   * ALL: apply every repair from every menu at once -- the most relaxed thing
#     the menus can reach. UNSAT => no choice can work (monotonicity).
#   * AGREE: do the per-conflict witnesses assign the same version to every
#     package they share? The cheap, choice-independent certificate candidate.
#
# The point is the rates, so nothing here is optimized.

using Random, Statistics
using Pkg.Versions: VersionSpec, VersionRange, VersionBound
using Resolver: Problem, SAT, pkg_info, prepare_pkg_info, is_satisfiable,
    installed_lit, sat_disjoint_muses, sat_mcses, with_classes_relaxed,
    relax, resolve
using Resolver.Diagnostics: Diagnostics

include(joinpath(@__DIR__, "test", "registry.jl"))

const data = registry.provider()
const NAMES = sort!(collect(data.packages))
const MENU_CAP = 6   # repairs kept per conflict, so the sampling stays bounded

tight(v) = (b = VersionBound(v.major, v.minor, v.patch); VersionSpec(VersionRange(b, b)))

# the squeeze that makes registry queries fail: requirements pinned to their
# newest, some of the closure pinned to its oldest
function make_problem(rng, nreq, nbound)
    reqs = unique(rand(rng, NAMES, nreq))
    base = pkg_info(data, Problem(reqs))
    pool = sort!(collect(keys(base)))
    isempty(pool) && return nothing
    compat = Dict{String,VersionSpec}()
    for p in reqs
        v = get(base, p, nothing)
        v === nothing || isempty(v.versions) || (compat[p] = tight(first(v.versions)))
    end
    for p in unique(rand(rng, pool, min(nbound, length(pool))))
        p in reqs && continue
        vs = base[p].versions
        isempty(vs) || (compat[p] = tight(last(vs)))
    end
    isempty(compat) ? nothing : Problem(reqs; compat)
end

# do two solutions agree wherever they overlap?
function agree(a, b)
    for (p, v) in a
        haskey(b, p) && b[p] != v && return false
    end
    return true
end

function trial(rng, nreq, nbound)
    prob = make_problem(rng, nreq, nbound)
    prob === nothing && return nothing
    reqs = unique(prob.reqs)
    info = pkg_info(data, prob)
    univ = prepare_pkg_info(info, prob)
    sat = SAT(univ)
    is_satisfiable(sat, reqs) && return nothing
    req_lits = Int[installed_lit(sat, p) for p in reqs if haskey(sat.vars, p)]
    isempty(req_lits) && return nothing
    clusters = sat_disjoint_muses(sat, req_lits)
    k = length(clusters)
    k < 2 && return (; k, multi = false)

    vm = Diagnostics.VarMap(sat)
    # the packages each cluster's requirements name: verifying one conflict's
    # repair means dropping the OTHER clusters' requirements, or their still
    # unfixed conflicts make every sub-problem unsatisfiable
    cluster_pkgs = [Set(String[Diagnostics.decode(vm, l)[1] for l in c])
                    for c in clusters]
    menus = Vector{Vector{Diagnostics.Action{String}}}[]
    menu_cluster = Int[]
    with_classes_relaxed(sat) do
        Diagnostics.with_emptied_packages(sat, vm) do pkg_lits, pkgs
            emptied = Dict{Int,String}(zip(pkg_lits, pkgs))
            for c in clusters
                sets = Vector{Diagnostics.Action{String}}[]
                for mcs in sat_mcses(sat, [c; pkg_lits]; limit = MENU_CAP)
                    push!(sets, Diagnostics.correction_actions(
                        sat, prob, vm, emptied, mcs, String[]))
                end
                if !isempty(sets)
                    push!(menus, sets)
                    push!(menu_cluster, findfirst(==(c), clusters))
                end
            end
        end
    end
    length(menus) < 2 && return (; k, multi = false)

    # resolve the relaxation a set of actions asks for, on the failed instance
    function try_actions(actions; also_drop = String[])
        dr, dc = Diagnostics.withdrawal(actions)
        return resolve(sat, relax(univ, prob, unique(vcat(dr, also_drop)), dc))
    end

    # conflict i's sub-problem: every other cluster's requirements dropped
    others(i) = collect(String, reduce(union,
        (cluster_pkgs[menu_cluster[j]] for j in eachindex(menus) if j != i);
        init = Set{String}()))

    # ALL: the most relaxed combination the menus can reach
    all_actions = reduce(vcat, reduce(vcat, menus); init = Diagnostics.Action{String}[])
    all_sat = try_actions(unique(all_actions)) !== nothing

    # Witnesses for EVERY repair in every menu -- what the real diagnosis
    # computes anyway, since each listed fix is verified by resolving it.
    wits = Vector{Vector{Any}}()
    for (i, m) in enumerate(menus)
        ws = Any[]
        for actions in m
            w = try_actions(actions; also_drop = others(i))
            w === nothing || push!(ws, w)
        end
        push!(wits, ws)
    end
    any(isempty, wits) && return (; k, multi = false)

    # The choice-INDEPENDENT certificate: every witness of every repair of one
    # conflict agrees with every witness of every repair of another. If that
    # holds, no choice the user can make puts two of them in disagreement.
    allpairs = true
    for i in eachindex(wits), j in i+1:length(wits)
        for a in wits[i], b in wits[j]
            agree(a, b) || (allpairs = false; break)
        end
        allpairs || break
    end

    # ground truth: sample combinations and see whether they actually compose
    combos = 0; combos_sat = 0
    for t in 1:6
        pick = [t == 1 ? m[1] : rand(rng, m) for m in menus]
        combos += 1
        try_actions(unique(reduce(vcat, pick))) === nothing || (combos_sat += 1)
    end
    return (; k, multi = true, all_sat, allpairs, combos, combos_sat)

end

const NREQ   = parse(Int, get(ENV, "NREQ", "14"))
const TARGET = parse(Int, get(ENV, "N", "60"))
rng = MersenneTwister(0xD00D + NREQ)
res = NamedTuple[]
tries = 0; t0 = time()
while count(r -> r.multi, res) < TARGET && tries < 40TARGET && time() - t0 < 5400
    global tries += 1
    r = try trial(rng, rand(rng, max(2, NREQ ÷ 2):NREQ), rand(rng, 1:8))
        catch e; e isa InterruptException && rethrow(); nothing end
    r === nothing && continue
    push!(res, r)
    n = count(x -> x.multi, res)
    n % 10 == 0 && n > 0 && (println("… $n multi-conflict, $tries tries, $(round(Int,time()-t0))s"); flush(stdout))
end

multi = [r for r in res if r.multi]
println("\n=== nreq ≤ $NREQ: $(length(res)) failing queries, $(length(multi)) multi-conflict ===")
isempty(multi) && exit(0)
tot = sum(r.combos for r in multi)
sat = sum(r.combos_sat for r in multi)
println("combinations tested: $tot | complete: $sat ($(round(100sat/tot,digits=1))%) | second-order: $(tot-sat)")
fired = [r for r in multi if r.allpairs]
println("\nCHOICE-INDEPENDENT certificate (all witnesses of all repairs agree pairwise):")
println("  fired on $(length(fired))/$(length(multi)) queries ($(round(100length(fired)/length(multi),digits=1))%)")
if !isempty(fired)
    ft = sum(r.combos for r in fired); fs = sum(r.combos_sat for r in fired)
    println("  their combinations: $fs/$ft complete ",
            fs == ft ? "(certificate held everywhere)" : "(!! CERTIFICATE VIOLATED)")
end
notf = [r for r in multi if !r.allpairs]
if !isempty(notf)
    nt = sum(r.combos for r in notf); ns = sum(r.combos_sat for r in notf)
    println("  where it did NOT fire: $ns/$nt combinations complete anyway ",
            "($(round(100ns/nt,digits=1))% — the sentence would print unnecessarily this often)")
end