theories · pac · Tangled

This repository has no description

pac theories

26 files

Ryan Gibb · PeerDependency.v's versions_lookupIntermediate binds its dependee name as o, as its sibling dependees theorems do · 4w ago

theories: GFacts is GF; ownedBy takes the owner first in npm as in opam; split4 where PackageFormula said repeat split would overrun; alpine's bare provides are PBare and bareProvSet

Cargo.v's lookup theorems bind the crate name as n, the slot class as w, the chosen class as w' and the delivered feature as f'

theories: one skeleton across the ecosystem files, membership lemmas everywhere, comments a Rocq reader needs, dead fields gone

Prelude.v holds if_scrutinee, SetSpecs.mem_eq_of_iff and one granFibre functor, which Npm.v, Concurrent.v and FeatureConcurrent.v share rather than each keeping its own

theories: one skeleton across the ecosystem files, membership lemmas everywhere, comments a Rocq reader needs, dead fields gone

ConflictClass.v

ConflictClass and DebianMA: classPkgs and clsPreimage take their set of packages as ps

theories: shared membership lemmas, and an inversion spec with named cases beside each reduction

Debian.v and DebianMA.v state their instance as a record, as Alpine.v, Opam.v and Npm.v do

ConflictClass and DebianMA: classPkgs and clsPreimage take their set of packages as ps

the core calculus over list-backed ordered sets: dependency relation, resolutions, dependees

theories: one skeleton across the ecosystem files, membership lemmas everywhere, comments a Rocq reader needs, dead fields gone

FeatureConcurrent.v

Prelude.v holds if_scrutinee, SetSpecs.mem_eq_of_iff and one granFibre functor, which Npm.v, Concurrent.v and FeatureConcurrent.v share rather than each keeping its own

Npm.v's lookup theorems bind the directory key as k', the peer name as n and a descriptor's registry name as m

NpmPlacement.v and Placement.v keep only Rocq comments, the npm reasoning moving to the driver, and NpmCommon holds what NpmPlacement.v restated of Npm.v

Placement's reduction drops the Tree atom and its soundness decodes the layout's reachable restriction, so the placement driver hands PubGrub only exact ranges and solves once, and npm-place.t's grow cases pass in pubgrub order

Cargo.v's versions_link_mono and Opam.v's versions_class_mono show a links value's and a class's versions only grow with the loaded instance, and the drivers' comments cite the resolver contract

PackageFormula.v

PackageFormula.v's lookup theorems bind the looked-up name as n and a negated name as m

PeerDependency.v

PeerDependency.v's versions_lookupIntermediate binds its dependee name as o, as its sibling dependees theorems do

Placement's reduction drops the Tree atom and its soundness decodes the layout's reachable restriction, so the placement driver hands PubGrub only exact ranges and solves once, and npm-place.t's grow cases pass in pubgrub order

Prelude.v holds if_scrutinee, SetSpecs.mem_eq_of_iff and one granFibre functor, which Npm.v, Concurrent.v and FeatureConcurrent.v share rather than each keeping its own

theories: restore the class-table bridge the Debian driver relies on; drop the true orphans

The placement reading keeps the project apart from the registry package of its name, and the npm reading refuses a query that reaches its own name

VariableFormula.v

VariableFormula.v's lookup theorems bind the looked-up name as n and a negated name as m

theories: one skeleton across the ecosystem files, membership lemmas everywhere, comments a Rocq reader needs, dead fields gone

theories: one skeleton across the ecosystem files, membership lemmas everywhere, comments a Rocq reader needs, dead fields gone

theories: one skeleton across the ecosystem files, membership lemmas everywhere, comments a Rocq reader needs, dead fields gone