420 lines
14 KiB
Nim
420 lines
14 KiB
Nim
## Property-Based Tests for Resolution Completeness
|
|
##
|
|
## **Feature: 02-nip-dependency-resolution, Property 5: Resolution Completeness**
|
|
## **Validates: Requirements 5.1, 5.4**
|
|
##
|
|
## Property: For any satisfiable dependency graph, the resolver SHALL find a solution
|
|
##
|
|
## This property verifies that:
|
|
## 1. If a solution exists, the resolver finds it
|
|
## 2. The solution satisfies all dependencies
|
|
## 3. The installation order respects dependency relationships
|
|
## 4. The resolver is deterministic (same input → same output)
|
|
|
|
import std/[unittest, tables, sets, options, random, sequtils]
|
|
import ../src/nip/resolver/[
|
|
resolver_integration,
|
|
dependency_graph,
|
|
variant_types,
|
|
cnf_translator,
|
|
cdcl_solver
|
|
]
|
|
import ../src/nip/manifest_parser
|
|
|
|
# --- Test Data Generators ---
|
|
|
|
proc generateVariant(rng: var Rand, numFlags: int = 0): VariantProfile =
|
|
## Generate a random variant profile
|
|
var domains = initTable[string, VariantDomain]()
|
|
|
|
if numFlags > 0:
|
|
var flagSet = initHashSet[string]()
|
|
for i in 0..<numFlags:
|
|
flagSet.incl("flag" & $i)
|
|
|
|
domains["features"] = VariantDomain(
|
|
name: "features",
|
|
exclusivity: NonExclusive,
|
|
flags: flagSet
|
|
)
|
|
|
|
result = VariantProfile(
|
|
domains: domains,
|
|
hash: "hash-" & $rng.rand(1000000)
|
|
)
|
|
|
|
proc generateAcyclicGraph(rng: var Rand, numPackages: int): DependencyGraph =
|
|
## Generate a random acyclic dependency graph
|
|
## Uses a layered approach to ensure no cycles
|
|
result = newDependencyGraph()
|
|
|
|
if numPackages == 0:
|
|
return
|
|
|
|
# Create packages in layers (layer 0 has no dependencies)
|
|
let layerSize = max(1, numPackages div 3)
|
|
var packages: seq[seq[PackageTermId]] = @[]
|
|
var currentLayer: seq[PackageTermId] = @[]
|
|
|
|
for i in 0..<numPackages:
|
|
let variant = generateVariant(rng, numFlags = 0)
|
|
let packageName = "pkg" & $i
|
|
let termId = createTermId(packageName, variant.hash)
|
|
|
|
result.addTerm(PackageTerm(
|
|
id: termId,
|
|
packageName: packageName,
|
|
variantProfile: variant,
|
|
optional: false,
|
|
source: "test"
|
|
))
|
|
|
|
currentLayer.add(termId)
|
|
|
|
# Start new layer
|
|
if currentLayer.len >= layerSize:
|
|
packages.add(currentLayer)
|
|
currentLayer = @[]
|
|
|
|
# Add remaining packages to last layer
|
|
if currentLayer.len > 0:
|
|
packages.add(currentLayer)
|
|
|
|
# Add edges between layers (only from higher layer to lower layer)
|
|
for layerIdx in 1..<packages.len:
|
|
for termId in packages[layerIdx]:
|
|
# Each package depends on 0-2 packages from previous layer
|
|
let numDeps = rng.rand(min(2, packages[layerIdx - 1].len))
|
|
|
|
for _ in 0..<numDeps:
|
|
let depIdx = rng.rand(packages[layerIdx - 1].len - 1)
|
|
let depTermId = packages[layerIdx - 1][depIdx]
|
|
|
|
result.addEdge(DependencyEdge(
|
|
fromTerm: termId,
|
|
toTerm: depTermId,
|
|
dependencyType: Required
|
|
))
|
|
|
|
proc generateChainGraph(numPackages: int): DependencyGraph =
|
|
## Generate a simple chain: P0 -> P1 -> P2 -> ... -> Pn
|
|
result = newDependencyGraph()
|
|
|
|
var prevTermId: Option[PackageTermId] = none(PackageTermId)
|
|
|
|
for i in 0..<numPackages:
|
|
let variant = VariantProfile(
|
|
domains: initTable[string, VariantDomain](),
|
|
hash: "hash-" & $i
|
|
)
|
|
let packageName = "pkg" & $i
|
|
let termId = createTermId(packageName, variant.hash)
|
|
|
|
result.addTerm(PackageTerm(
|
|
id: termId,
|
|
packageName: packageName,
|
|
variantProfile: variant,
|
|
optional: false,
|
|
source: "test"
|
|
))
|
|
|
|
if prevTermId.isSome:
|
|
result.addEdge(DependencyEdge(
|
|
fromTerm: prevTermId.get(),
|
|
toTerm: termId,
|
|
dependencyType: Required
|
|
))
|
|
|
|
prevTermId = some(termId)
|
|
|
|
proc generateDiamondGraph(): DependencyGraph =
|
|
## Generate a diamond: A -> B, A -> C, B -> D, C -> D
|
|
result = newDependencyGraph()
|
|
|
|
let variantA = VariantProfile(domains: initTable[string, VariantDomain](), hash: "hash-A")
|
|
let variantB = VariantProfile(domains: initTable[string, VariantDomain](), hash: "hash-B")
|
|
let variantC = VariantProfile(domains: initTable[string, VariantDomain](), hash: "hash-C")
|
|
let variantD = VariantProfile(domains: initTable[string, VariantDomain](), hash: "hash-D")
|
|
|
|
let termIdA = createTermId("A", variantA.hash)
|
|
let termIdB = createTermId("B", variantB.hash)
|
|
let termIdC = createTermId("C", variantC.hash)
|
|
let termIdD = createTermId("D", variantD.hash)
|
|
|
|
for (id, name, variant) in [(termIdA, "A", variantA), (termIdB, "B", variantB),
|
|
(termIdC, "C", variantC), (termIdD, "D", variantD)]:
|
|
result.addTerm(PackageTerm(
|
|
id: id,
|
|
packageName: name,
|
|
variantProfile: variant,
|
|
optional: false,
|
|
source: "test"
|
|
))
|
|
|
|
result.addEdge(DependencyEdge(fromTerm: termIdA, toTerm: termIdB, dependencyType: Required))
|
|
result.addEdge(DependencyEdge(fromTerm: termIdA, toTerm: termIdC, dependencyType: Required))
|
|
result.addEdge(DependencyEdge(fromTerm: termIdB, toTerm: termIdD, dependencyType: Required))
|
|
result.addEdge(DependencyEdge(fromTerm: termIdC, toTerm: termIdD, dependencyType: Required))
|
|
|
|
# --- Property Tests ---
|
|
|
|
suite "Resolution Completeness Properties":
|
|
|
|
test "Property 5: Resolution Completeness - Chain graphs":
|
|
## **Feature: 02-nip-dependency-resolution, Property 5: Resolution Completeness**
|
|
## **Validates: Requirements 5.1, 5.4**
|
|
##
|
|
## Property: For any chain graph (no cycles), resolution SHALL succeed
|
|
## and produce a valid installation order
|
|
|
|
var rng = initRand(12345)
|
|
var successCount = 0
|
|
var totalTests = 0
|
|
|
|
# Test with various chain lengths
|
|
for chainLength in [1, 2, 5, 10, 20]:
|
|
for iteration in 0..<4: # 4 iterations per length
|
|
totalTests += 1
|
|
|
|
let graph = generateChainGraph(chainLength)
|
|
|
|
# Create resolution request for first package
|
|
let request = ResolutionRequest(
|
|
rootPackages: @[PackageSpec(
|
|
packageName: "pkg0",
|
|
versionConstraint: VersionConstraint(
|
|
operator: OpAny,
|
|
version: SemanticVersion(major: 1, minor: 0, patch: 0)
|
|
),
|
|
variantProfile: VariantProfile(
|
|
domains: initTable[string, VariantDomain](),
|
|
hash: "hash-0"
|
|
)
|
|
)],
|
|
constraints: @[]
|
|
)
|
|
|
|
let result = resolve(request, graph)
|
|
|
|
# Property: Resolution should succeed
|
|
if not result.success:
|
|
echo "FAILED: Chain length ", chainLength, " iteration ", iteration
|
|
echo " Conflict: ", result.conflict.details
|
|
check false
|
|
continue
|
|
|
|
# Property: All packages should be in solution
|
|
check result.packages.len == chainLength
|
|
|
|
# Property: Installation order should respect dependencies
|
|
# In a chain, pkg(i) depends on pkg(i+1), so pkg(i+1) must come first
|
|
var orderMap = initTable[string, int]()
|
|
for i, name in result.installOrder:
|
|
orderMap[name] = i
|
|
|
|
for i in 0..<(chainLength - 1):
|
|
let dependent = "pkg" & $i
|
|
let dependency = "pkg" & $(i + 1)
|
|
|
|
if orderMap.hasKey(dependent) and orderMap.hasKey(dependency):
|
|
if orderMap[dependency] >= orderMap[dependent]:
|
|
echo "FAILED: Dependency order violated"
|
|
echo " ", dependent, " (index ", orderMap[dependent], ") depends on ",
|
|
dependency, " (index ", orderMap[dependency], ")"
|
|
check false
|
|
continue
|
|
|
|
successCount += 1
|
|
|
|
echo "Property 5 (Chain): ", successCount, "/", totalTests, " tests passed"
|
|
check successCount == totalTests
|
|
|
|
test "Property 5: Resolution Completeness - Diamond graphs":
|
|
## **Feature: 02-nip-dependency-resolution, Property 5: Resolution Completeness**
|
|
## **Validates: Requirements 5.1, 5.4**
|
|
##
|
|
## Property: For diamond graphs, resolution SHALL succeed and D SHALL come before B and C
|
|
|
|
var successCount = 0
|
|
var totalTests = 20
|
|
|
|
for iteration in 0..<totalTests:
|
|
let graph = generateDiamondGraph()
|
|
|
|
let request = ResolutionRequest(
|
|
rootPackages: @[PackageSpec(
|
|
packageName: "A",
|
|
versionConstraint: VersionConstraint(
|
|
operator: OpAny,
|
|
version: SemanticVersion(major: 1, minor: 0, patch: 0)
|
|
),
|
|
variantProfile: VariantProfile(
|
|
domains: initTable[string, VariantDomain](),
|
|
hash: "hash-A"
|
|
)
|
|
)],
|
|
constraints: @[]
|
|
)
|
|
|
|
let result = resolve(request, graph)
|
|
|
|
# Property: Resolution should succeed
|
|
if not result.success:
|
|
echo "FAILED: Diamond iteration ", iteration
|
|
echo " Conflict: ", result.conflict.details
|
|
check false
|
|
continue
|
|
|
|
# Property: All 4 packages should be in solution
|
|
check result.packages.len == 4
|
|
|
|
# Property: D must come before B and C (shared dependency)
|
|
var orderMap = initTable[string, int]()
|
|
for i, name in result.installOrder:
|
|
orderMap[name] = i
|
|
|
|
if orderMap["D"] >= orderMap["B"] or orderMap["D"] >= orderMap["C"]:
|
|
echo "FAILED: D should come before B and C"
|
|
echo " Order: ", result.installOrder
|
|
check false
|
|
continue
|
|
|
|
# Property: B and C must come before A
|
|
if orderMap["B"] >= orderMap["A"] or orderMap["C"] >= orderMap["A"]:
|
|
echo "FAILED: B and C should come before A"
|
|
echo " Order: ", result.installOrder
|
|
check false
|
|
continue
|
|
|
|
successCount += 1
|
|
|
|
echo "Property 5 (Diamond): ", successCount, "/", totalTests, " tests passed"
|
|
check successCount == totalTests
|
|
|
|
test "Property 5: Resolution Completeness - Random acyclic graphs":
|
|
## **Feature: 02-nip-dependency-resolution, Property 5: Resolution Completeness**
|
|
## **Validates: Requirements 5.1, 5.4**
|
|
##
|
|
## Property: For any acyclic graph, resolution SHALL succeed
|
|
|
|
var rng = initRand(54321)
|
|
var successCount = 0
|
|
var totalTests = 20
|
|
|
|
for iteration in 0..<totalTests:
|
|
# Generate random acyclic graph with 5-15 packages
|
|
let numPackages = rng.rand(5..15)
|
|
let graph = generateAcyclicGraph(rng, numPackages)
|
|
|
|
if graph.nodeCount() == 0:
|
|
continue
|
|
|
|
# Pick first package as root
|
|
let rootTerm = toSeq(graph.terms.values)[0]
|
|
|
|
let request = ResolutionRequest(
|
|
rootPackages: @[PackageSpec(
|
|
packageName: rootTerm.packageName,
|
|
versionConstraint: VersionConstraint(
|
|
operator: OpAny,
|
|
version: SemanticVersion(major: 1, minor: 0, patch: 0)
|
|
),
|
|
variantProfile: rootTerm.variantProfile
|
|
)],
|
|
constraints: @[]
|
|
)
|
|
|
|
let result = resolve(request, graph)
|
|
|
|
# Property: Resolution should succeed for acyclic graphs
|
|
if not result.success:
|
|
echo "FAILED: Random graph iteration ", iteration, " (", numPackages, " packages)"
|
|
echo " Conflict: ", result.conflict.details
|
|
check false
|
|
continue
|
|
|
|
# Property: Solution should contain at least the root package
|
|
check result.packages.len >= 1
|
|
|
|
# Property: Installation order should be valid (no package before its dependencies)
|
|
var orderMap = initTable[string, int]()
|
|
for i, name in result.installOrder:
|
|
orderMap[name] = i
|
|
|
|
var orderValid = true
|
|
for edge in graph.edges:
|
|
let fromTerm = graph.getTerm(edge.fromTerm)
|
|
let toTerm = graph.getTerm(edge.toTerm)
|
|
|
|
if fromTerm.isSome and toTerm.isSome:
|
|
let fromName = fromTerm.get().packageName
|
|
let toName = toTerm.get().packageName
|
|
|
|
if orderMap.hasKey(fromName) and orderMap.hasKey(toName):
|
|
if orderMap[toName] >= orderMap[fromName]:
|
|
echo "FAILED: Dependency order violated in random graph"
|
|
echo " ", fromName, " depends on ", toName
|
|
echo " But ", toName, " comes after ", fromName, " in install order"
|
|
orderValid = false
|
|
break
|
|
|
|
if not orderValid:
|
|
check false
|
|
continue
|
|
|
|
successCount += 1
|
|
|
|
echo "Property 5 (Random): ", successCount, "/", totalTests, " tests passed"
|
|
check successCount == totalTests
|
|
|
|
test "Property 5: Determinism - Same input produces same output":
|
|
## **Feature: 02-nip-dependency-resolution, Property 5: Resolution Completeness**
|
|
## **Validates: Requirements 5.1, 5.4**
|
|
##
|
|
## Property: Resolving the same graph multiple times SHALL produce identical results
|
|
|
|
let graph = generateDiamondGraph()
|
|
|
|
let request = ResolutionRequest(
|
|
rootPackages: @[PackageSpec(
|
|
packageName: "A",
|
|
versionConstraint: VersionConstraint(
|
|
operator: OpAny,
|
|
version: SemanticVersion(major: 1, minor: 0, patch: 0)
|
|
),
|
|
variantProfile: VariantProfile(
|
|
domains: initTable[string, VariantDomain](),
|
|
hash: "hash-A"
|
|
)
|
|
)],
|
|
constraints: @[]
|
|
)
|
|
|
|
# Resolve multiple times
|
|
var results: seq[ResolutionResult] = @[]
|
|
for _ in 0..<10:
|
|
results.add(resolve(request, graph))
|
|
|
|
# Property: All results should be identical
|
|
let firstResult = results[0]
|
|
|
|
for i in 1..<results.len:
|
|
let result = results[i]
|
|
|
|
# Check success status matches
|
|
check result.success == firstResult.success
|
|
|
|
if result.success:
|
|
# Check same number of packages
|
|
check result.packages.len == firstResult.packages.len
|
|
|
|
# Check same installation order
|
|
check result.installOrder == firstResult.installOrder
|
|
|
|
# Check same package names
|
|
let firstNames = firstResult.packages.mapIt(it.packageName).toHashSet
|
|
let resultNames = result.packages.mapIt(it.packageName).toHashSet
|
|
check firstNames == resultNames
|
|
|
|
echo "Property 5 (Determinism): All 10 resolutions produced identical results"
|