These tables map each definition and theorem in the paper to its mechanised counterpart in this development.
All file paths are relative to the PackageCalculus/ source directory.
Where the paper writes structured names like ⟨n, vs⟩ ∈ N or ⟨n, f⟩, the Lean uses dedicated inductive name/version types and Has*Names / Has*Versions typeclasses to inject them.
The paper states one standing condition on every dependency relation: Functional in Name (Def 3.1.2).
In Lean it appears as an explicit hypothesis (DepRel.FunctionalInName) on the theorems that consume it.
The paper's normalisation remark -- merging same-name entries per depender by intersecting their version sets -- is mechanised as DepRel.merge (merge_functionalInName, merge_resolution_iff), alongside DepRel.restrictReal (restrictReal_resolution_iff) for restricting version sets to real packages; both preserve the set of resolutions.
3. The Package Calculus #
| Paper |
Lean |
File |
| Def 3.1.1 Package |
Real, Package |
Core/Definition.lean |
| Def 3.1.2 Dependency |
DepRel |
Core/Definition.lean |
| Def 3.1.3 Resolution |
IsResolution |
Core/Definition.lean |
Thm 3.1.4 DependencyResolution NP-complete |
see Appendix B below (satRed_*) |
Complexity/ |
| Def 3.2.1 Version Ordering |
the [LT V] / [DecidableRel (· < ·)] order on V |
used throughout Versions/Formula.lean |
| Def 3.2.2 Version Formula |
VersionFormula, VersionFormula.eval (CmpOp.eval) |
Versions/Formula.lean |
| Def 3.2.3 Version Formula Dependency |
VFDepRel |
Versions/Formula.lean |
| Def 3.2.4 Version Formula Resolution |
IsVFResolution |
Versions/Formula.lean |
| Def 3.2.5 Version Formula Reduction |
vfReduce |
Versions/Reduction/Definition.lean |
| Thm 3.2.6 Correctness |
version_formula_correct |
Versions/Reduction/Correctness.lean |
4. Package Managers, Mise en Place #
4.1 Conflicts #
| Paper |
Lean |
File |
| Def 4.1.1 Conflict |
ConflictRel |
Extensions/Conflict/Definition.lean |
| Def 4.1.2 Conflict Resolution |
IsConflictResolution |
Extensions/Conflict/Definition.lean |
| Def 4.1.3 Conflict Reduction |
conflictReal / conflictDeps |
Extensions/Conflict/Reduction/Definition.lean |
| Thm 4.1.4 Soundness |
conflict_soundness |
Extensions/Conflict/Reduction/Soundness.lean |
| Thm 4.1.5 Completeness |
conflict_completeness |
Extensions/Conflict/Reduction/Completeness.lean |
4.2 Concurrent Versions #
| Paper |
Lean |
File |
| Def 4.2.1 Granularity Function |
g : V → G (parameter) |
Extensions/Concurrent/Definition.lean |
| Def 4.2.2 Concurrent Resolution |
IsConcurrentResolution |
Extensions/Concurrent/Definition.lean |
| Def 4.2.3 Concurrent Reduction |
concurrentReal / concurrentDeps |
Extensions/Concurrent/Reduction/Definition.lean |
| Thm 4.2.4 Soundness |
concurrent_soundness |
Extensions/Concurrent/Reduction/Soundness.lean |
| Thm 4.2.5 Completeness |
concurrent_completeness |
Extensions/Concurrent/Reduction/Completeness.lean |
4.3 Peer Dependencies #
| Paper |
Lean |
File |
| Def 4.3.1 Peer Dependency |
PeerRel |
Extensions/PeerDependency/Definition.lean |
| Def 4.3.2 Peer Dependency Resolution |
IsPeerResolution |
Extensions/PeerDependency/Definition.lean |
| Def 4.3.3 Peer Dependency Reduction |
peerReal / peerDeps |
Extensions/PeerDependency/Reduction/Definition.lean |
| Thm 4.3.4 Soundness |
peer_soundness |
Extensions/PeerDependency/Reduction/Soundness.lean |
| Thm 4.3.5 Completeness |
peer_completeness |
Extensions/PeerDependency/Reduction/Completeness.lean |
4.4 Dependency Visibility #
| Paper |
Lean |
File |
| Def 4.4.1 Public Dependency |
PubRel, Priv |
Extensions/Visibility/Definition.lean |
| Def 4.4.2 Visible Subgraph |
InSub |
Extensions/Visibility/Definition.lean |
| Def 4.4.3 Visibility Resolution |
IsVisibilityResolution |
Extensions/Visibility/Definition.lean |
| Def 4.4.4 Visibility Reduction |
visReal / visDeps (potentialOrigins, carried) |
Extensions/Visibility/Reduction/Definition.lean |
| Thm 4.4.5 Soundness |
visibility_soundness |
Extensions/Visibility/Reduction/Soundness.lean |
| Thm 4.4.6 Completeness |
visibility_completeness |
Extensions/Visibility/Reduction/Completeness.lean |
4.5 Features #
| Paper |
Lean |
File |
| Def 4.5.1 Feature |
Support |
Extensions/Feature/Definition.lean |
| Def 4.5.2 Feature Dependency |
FeatDepRel, AddlDepRel |
Extensions/Feature/Definition.lean |
| Def 4.5.3 Feature Resolution |
IsFeatureResolution |
Extensions/Feature/Definition.lean |
| Def 4.5.4 Feature Reduction |
featureReal / featureDeps |
Extensions/Feature/Reduction/Definition.lean |
| Thm 4.5.5 Soundness |
feature_soundness |
Extensions/Feature/Reduction/Soundness.lean |
| Thm 4.5.6 Completeness |
feature_completeness |
Extensions/Feature/Reduction/Completeness.lean |
| Paper |
Lean |
File |
| Def 4.6.1 Package Formula |
Formula (in namespace PkgFormula) |
Extensions/PackageFormula/Definition.lean |
| Def 4.6.2 Package Formula Dependency |
PFDepRel |
Extensions/PackageFormula/Definition.lean |
| Def 4.6.3 Package Formula Resolution |
IsPFResolution |
Extensions/PackageFormula/Definition.lean |
| Def 4.6.4 Package Formula Reduction |
pfReal / pfDeps (via encode / encodeNNF) |
Extensions/PackageFormula/Reduction/Definition.lean |
| Thm 4.6.5 Soundness |
package_formula_soundness |
Extensions/PackageFormula/Reduction/Soundness.lean |
| Thm 4.6.6 Completeness |
package_formula_completeness |
Extensions/PackageFormula/Reduction/Completeness.lean |
| Paper |
Lean |
File |
| Def 4.7.1 Variable Formula |
Formula N V X Y (in namespace VarFormula), dep. relation VFDepRel |
Extensions/VariableFormula/Definition.lean |
| Def 4.7.2 Variable Formula Resolution |
IsVFResolution |
Extensions/VariableFormula/Definition.lean |
| Def 4.7.3 Variable Formula Reduction |
vfReal / vfDeps |
Extensions/VariableFormula/Reduction/Definition.lean |
| Thm 4.7.4 Soundness |
variable_formula_soundness |
Extensions/VariableFormula/Reduction/Soundness.lean |
| Thm 4.7.5 Completeness |
variable_formula_completeness |
Extensions/VariableFormula/Reduction/Completeness.lean |
4.8 Virtual Packages #
| Paper |
Lean |
File |
| Def 4.8.1 Virtual Package Provides |
ProvidesRel |
Extensions/Virtual/Definition.lean |
| Def 4.8.2 Virtual Package Resolution |
IsVirtualResolution |
Extensions/Virtual/Definition.lean |
| Def 4.8.3 Virtual Package Reduction |
virtualReal / virtualDeps |
Extensions/Virtual/Reduction/Definition.lean |
| Thm 4.8.4 Soundness |
virtual_soundness |
Extensions/Virtual/Reduction/Soundness.lean |
| Thm 4.8.5 Completeness |
virtual_completeness |
Extensions/Virtual/Reduction/Completeness.lean |
5. Package Managers, à la Carte #
5.1 Composition of Extensions #
| Paper |
Lean |
File |
| Def 5.1.1 Concurrent Feature Resolution |
IsConcurrentFeatureResolution |
Composition/FeatureConcurrent/Definition.lean |
| Def 5.1.2 Concurrent Feature Reduction |
concurrentFeatureReal / concurrentFeatureDeps |
Composition/FeatureConcurrent/Reduction/Definition.lean |
| Thm 5.1.3 Soundness |
concurrent_feature_soundness |
Composition/FeatureConcurrent/Reduction/Soundness.lean |
| Thm 5.1.4 Completeness |
concurrent_feature_completeness |
Composition/FeatureConcurrent/Reduction/Completeness.lean |
5.2 Solving Reduced Instances #
The paper states restriction invariance: out is unchanged when the instance is restricted to the named sub-instance. The Lean carries the equivalent fibred form: <ext>Lookup<Source> consumes exactly the sub-instance's blocks and <ext>Deps_lookup<Source> proves it agrees with the monolithic encoding; the restriction form follows by filter algebra.
| Paper |
Lean |
File |
| Thm 5.2.1 Version Formula Lookup |
edge-wise by definition (vfReduce) |
Versions/Reduction/Definition.lean |
| Thm 5.2.2 Conflict Lookup |
conflictDeps_lookupOrig, conflictDeps_synthetic_src |
Extensions/Lookup.lean |
| Thm 5.2.3 Concurrent Lookup |
concurrentDeps_lookupGranular, concurrentDeps_lookupIntermediate |
Extensions/Lookup.lean |
| Thm 5.2.4 Peer Lookup |
peerDeps_lookupGranular, peerDeps_lookupIntermediate |
Extensions/Lookup.lean |
| Thm 5.2.5 Visibility Lookup |
visDeps_lookupOccurrence, visDeps_lookupIntermediate, visDeps_agreement_src |
Extensions/Lookup.lean |
| Thm 5.2.6 Feature Lookup |
featureDeps_lookupOrig, featureDeps_lookupFeatured |
Extensions/Lookup.lean |
| Thm 5.2.7 Package Formula Lookup |
paper only (needs an occurrence relation over the atom closure) |
-- |
| Thm 5.2.8 Variable Formula Lookup |
paper only, as 5.2.7 |
-- |
| Thm 5.2.9 Virtual Lookup |
virtualDeps_lookupOrig, virtualDeps_lookupSelector |
Extensions/Lookup.lean |
5.3 Transpiling Packaging Languages #
Lifting is mechanised per extension under Extensions/<Extension>/Lifting/ (and Versions/Lifting/): Definition.lean defines lift, Retraction.lean proves the round trip, and Soundness.lean/Completeness.lean carry core resolutions back to extension resolutions.
| Extension |
Round trip |
Mechanised statement |
Side conditions |
| Conflict |
conflictLift_conflictReduce |
lift ∘ reduce = id (packages, dependencies, conflicts) |
-- |
| Concurrent |
concurrentLift_concurrentReduce |
lift ∘ reduce = id (packages, dependencies) |
DepRel.FunctionalInName |
| Peer |
peerLift_peerReduce |
lift ∘ reduce = id (packages, dependencies, peers) |
PeerRel.GroundedIn |
| Feature |
featureLift_featureReduce |
lift ∘ reduce = id (packages, support, feature deps, additional deps) |
Support.GroundedIn, FeatDepRel.FunctionalInName, AddlDepRel.FunctionalInName, AddlDepRel.BaseIrredundant |
| Virtual |
virtualLift_virtualReduce, liftProv_virtualDeps |
recovers (R, Δ.restrictReal R); provides recovered as its instantiation |
DepRel.FunctionalInName, ProvidesRel.NoSelfProvides |
| Package formulae |
liftAtoms_pfDeps, satisfies_iff_atoms |
NNF atom-set normal form (no formula retraction exists) |
-- |
| Variable formulae |
liftAtoms_vfDeps, satisfies_iff_atoms |
atom-set normal form, comparisons up to extension |
-- |
| Version formulae |
vfReduce ∘ liftVFDeps = restrictReal |
section direction only |
-- |
Where the statement is weaker than lift ∘ reduce = id, the loss is syntactic rather than semantic: the lift recovers a normal form that is proven faithful.
Formulae are recovered as their NNF atom sets, and satisfies_iff_atoms shows a resolution satisfies a formula iff it satisfies its atoms; a variable comparison is recovered as its extension, which is all evaluation consults; virtual and version-formula dependencies are recovered up to restrictReal, which removes only versions no resolution can select.
The Virtual provides relation is likewise recovered as a normal form, its instantiation on Δ -- the admissible (provider, name, depender) triples -- and instantiate_resolution_congr shows resolutions consult it only through this instantiation; only the guards' behaviour on dependencies outside Δ is lost.
Each side condition's docstring in the Lean states why it is needed.
Appendix B -- DependencyResolution complexity #
The paper's NP-completeness result (Thm 3.1.4) combines NP-hardness -- a polynomial-time reduction from 3SAT -- with NP-membership, which the paper establishes by direct polynomial-time verification of a candidate resolution (root inclusion, dependency closure, version uniqueness).
In Lean we mechanise the reduction's soundness and completeness (below); the polynomial-time bound and the membership verification are argued by inspection in the paper, not formalised.
The SAT encoding in Appendix C is a separate SAT-based solving method (formalised in SATEncoding.lean).
| Paper |
Lean |
File |
| 3SAT instance / clause |
ThreeClause, Literal |
Complexity/ThreeSAT.lean |
| 3SAT → resolution reduction |
satRedReal / satRedDeps |
Complexity/NPHardness.lean |
| Reduction soundness |
satRed_soundness |
Complexity/NPHardness.lean |
| Reduction completeness |
satRed_completeness |
Complexity/NPHardness.lean |
Appendix C -- SAT-based resolution #
| Paper |
Lean |
File |
| Def C.1 Package Calculus SAT Encoding |
satisfiesEncoding |
Complexity/SATEncoding.lean |
| Thm C.2 Soundness |
satEncoding_soundness |
Complexity/SATEncoding.lean |
| Thm C.3 Completeness |
satEncoding_completeness |
Complexity/SATEncoding.lean |
Appendix D -- Singular Dependencies #
| Paper |
Lean |
File |
| Def D.1 Singular Dependency |
SingularRel |
Extensions/Singular.lean |
| Def D.2 Singular Dependency Resolution |
IsSingularResolution (reduction singularToCore, singular_is_core) |
Extensions/Singular.lean |
Defs C.5 and C.6 (resolution ordering, ordered SAT encoding) and Appendix E (build graph, optional dependencies) are definitional discussion with no accompanying theorems, and are not mechanised.
