From e28cdbae0a48456413ff3d7ff41afd723d28c68e Mon Sep 17 00:00:00 2001
From: Ryan Gibb <ryan@freumh.org>
Date: Sun, 27 Sep 2026 14:16:39 +0100
Subject: [PATCH] NpmPlacement.v reduces npm's node_modules layouts, aliases
 and optional edges included, through Placement.v, which gains optional
 dependencies and peers; sound, complete to a depth bound, with lookups in the
 per-edge form the driver uses

---
 extraction/Extract.v                  |   4 +-
 scripts/check-axioms.sh               |  18 +
 test/example/extensions/extensions.ml |   2 +
 theories/NpmPlacement.v               | 571 ++++++++++++++++++++++++++
 theories/Placement.v                  | 242 +++++++----
 theories/Smoke.v                      |  26 +-
 6 files changed, 780 insertions(+), 83 deletions(-)
 create mode 100644 theories/NpmPlacement.v

diff --git a/extraction/Extract.v b/extraction/Extract.v
index aeaa046..352a5e6 100644
--- a/extraction/Extract.v
+++ b/extraction/Extract.v
@@ -1,5 +1,5 @@
 From PackageCalculus Require Import Prelude Core Versions Conflict Visibility
-  Debian DebianMA Opam Cargo Alpine Npm Placement Smoke.
+  Debian DebianMA Opam Cargo Alpine Npm Placement NpmPlacement Smoke.
 From Stdlib Require Import Extraction ExtrOcamlBasic.
 
 Extraction Language OCaml.
@@ -22,4 +22,4 @@ Extraction Inline lex.
 Extraction "pac_extraction.ml"
   Smoke.C Smoke.Ver Smoke.Cfl Smoke.Conc Smoke.Peer Smoke.Vis
   Smoke.Feat Smoke.Virt Smoke.PkgF Smoke.VarF Smoke.FC Smoke.Op Smoke.Cgo Smoke.Alp
-  Debian DebianMA Opam Cargo Alpine Npm Placement.
+  Debian DebianMA Opam Cargo Alpine Npm Placement NpmPlacement.
diff --git a/scripts/check-axioms.sh b/scripts/check-axioms.sh
index 249e61b..57b65ea 100755
--- a/scripts/check-axioms.sh
+++ b/scripts/check-axioms.sh
@@ -390,6 +390,24 @@ NpmS.Reduction.reduceDeps
 NpmS.Reduction.reduceReal
 NpmS.Reduction.versions
 NpmS.rootPkg
+
+NplS.Lookup.dependees_lookupAbsent
+NplS.Lookup.dependees_lookupOcc
+NplS.Lookup.dependees_lookupRoot
+NplS.Lookup.dependees_lookupWalk
+NplS.Lookup.edgeAtom
+NplS.Lookup.occAtoms_agree
+NplS.Lookup.treeAtom_agree
+NplS.Lookup.versions_lookupLoc
+NplS.Lookup.versions_lookupWalk
+NplS.edgesOf
+NplS.npm_completeness
+NplS.npm_roundtrip
+NplS.npm_soundness
+NplS.reduceDeps
+NplS.reduceReal
+NplS.tr
+NplS.tr_resolution
 LIST
 )
 
diff --git a/test/example/extensions/extensions.ml b/test/example/extensions/extensions.ml
index 8573772..09e4e47 100644
--- a/test/example/extensions/extensions.ml
+++ b/test/example/extensions/extensions.ml
@@ -981,6 +981,8 @@ module Placement = struct
             (("B", "1"), ("C", vs [ "2" ]));
           ];
       inst_peers = M.C.DepRel.ofList [ (("C", "2"), ("A", vs [ "1" ])) ];
+      inst_optDeps = M.C.DepRel.empty;
+      inst_optPeers = M.C.DepRel.empty;
       inst_root = ("R", "1");
     }
 
diff --git a/theories/NpmPlacement.v b/theories/NpmPlacement.v
new file mode 100644
index 0000000..27e6ea7
--- /dev/null
+++ b/theories/NpmPlacement.v
@@ -0,0 +1,571 @@
+From Stdlib Require Import MSets List Bool.
+From PackageCalculus Require Import Prelude Core Versions Semver Placement.
+
+Create HintDb cmp_npl.
+Create Rewrite HintDb cmp_npl.
+
+Module NpmPlacement (N V : UsualOrderedType) (PM : SemverMatch V).
+  Module RPkg := PairUOT N V.
+  Module RepoSet := FSetUOT RPkg.
+  Module VS := FSetUOT V.
+  Module NKey := PairUOT N N.
+  Module KeySet := FSetUOT NKey.
+  Module NEqb := UOTEqb N.
+  Module RPkgEqb := UOTEqb RPkg.
+  Module RPkgF := UOTCompareFacts RPkg.
+  #[local] Hint Rewrite RPkgF.compare_eq_iff : cmp_npl.
+  #[local] Hint Extern 1 => cmp_by RPkgF.compare_antisym : cmp_npl.
+  #[local] Hint Extern 1 => cmp_by RPkgF.compare_lt_trans : cmp_npl.
+
+  Module Sv := Semver V VS PM.
+  Include Sv.
+
+  (* What a directory holds: a registry package, or the project, which
+     only the root holds.  They differ even at one name and version, as
+     arborist loads devDependencies for the top node alone. *)
+  Module Occ.
+    Inductive occ : Type :=
+    | Top
+    | Reg (m : N.t) (v : V.t).
+    Definition t := occ.
+
+    Definition rank (x : t) : nat := match x with Top => 0 | Reg _ _ => 1 end.
+
+    Definition compare (x y : t) : comparison :=
+      match Nat.compare (rank x) (rank y) with
+      | Eq => match x, y with
+              | Reg m1 v1, Reg m2 v2 => RPkg.compare (m1, v1) (m2, v2)
+              | _, _ => Eq
+              end
+      | c => c
+      end.
+
+    Lemma compare_eq_iff : forall x y, compare x y = Eq <-> x = y.
+    Proof. cmp_eq_iff cmp_npl. Qed.
+
+    Lemma compare_antisym : forall x y, compare y x = CompOpp (compare x y).
+    Proof. cmp_antisym cmp_npl. Qed.
+
+    Lemma compare_lt_trans : forall x y z,
+        compare x y = Lt -> compare y z = Lt -> compare x z = Lt.
+    Proof. cmp_lt_trans cmp_npl. Qed.
+  End Occ.
+
+  Module OccOT := UOTFromCompare Occ.
+  Module Pl := Placement N OccOT.
+
+  (* A dependency's directory key and the registry package it names there
+     differ under an npm: alias. *)
+  Record Dependency : Type := MkDep
+    { d_dir : N.t
+    ; d_name : N.t
+    ; d_range : Range
+    ; d_dev : bool
+    ; d_optional : bool }.
+
+  Record PeerDependency : Type := MkPeer
+    { p_dir : N.t
+    ; p_name : N.t
+    ; p_range : Range
+    ; p_optional : bool }.
+
+  (* The relation fields are lists, as in Npm.v: sets would demand an order
+     on Range used nowhere. *)
+  Record Inst : Type := MkInst
+    { inst_repo : RepoSet.t
+    ; inst_deps : list (RPkg.t * Dependency)
+    ; inst_peers : list (RPkg.t * PeerDependency)
+    ; inst_ovr : list (N.t * Range)
+    ; inst_root : RPkg.t }.
+
+  Definition ownedBy {A : Type} (p : RPkg.t) (l : list (RPkg.t * A)) : list A :=
+    List.map snd (List.filter (fun q => RPkgEqb.eqb (fst q) p) l).
+
+  Lemma in_ownedBy : forall (A : Type) (l : list (RPkg.t * A)) p a,
+      In a (ownedBy p l) <-> In (p, a) l.
+  Proof.
+    intros A l p a; unfold ownedBy; rewrite in_map_iff; split.
+    - intros [[q b] [<- H]]; apply filter_In in H; destruct H as [H E].
+      apply RPkgEqb.eqb_true_iff in E; cbn [fst] in E; subst q; exact H.
+    - intro H; exists (p, a); split; [reflexivity |].
+      apply filter_In; split; [exact H | apply RPkgEqb.eqb_refl].
+  Qed.
+
+  Module SOrv := SetOps RPkg V RepoSet VS.
+  Definition realVersions (R : RepoSet.t) (m : N.t) : VS.t :=
+    SOrv.filterMap
+      (fun q => if NEqb.eqb (fst q) m then Some (snd q) else None) R.
+
+  Lemma mem_realVersions : forall R m v,
+      VS.In v (realVersions R m) <-> RepoSet.In (m, v) R.
+  Proof.
+    intros R m v; unfold realVersions; rewrite SOrv.mem_filterMap_if; split.
+    - intros [[m' u] [HR [Hm ->]]]; cbn [fst snd] in *.
+      apply NEqb.eqb_true_iff in Hm; subst m'; exact HR.
+    - intro H; exists (m, v); cbn [fst snd]; rewrite NEqb.eqb_refl; auto.
+  Qed.
+
+  Fixpoint lookupOvr (l : list (N.t * Range)) (n : N.t) : option Range :=
+    match l with
+    | nil => None
+    | (m, rg) :: l' => if NEqb.eqb m n then Some rg else lookupOvr l' n
+    end.
+
+  (* A flat override, keyed by the registry package the edge names, as the
+     npm reading keys it. *)
+  Definition override (I : Inst) (n : N.t) (rg : Range) : Range :=
+    match lookupOvr (inst_ovr I) n with
+    | Some rg' => rg'
+    | None => rg
+    end.
+
+  Definition cands (I : Inst) (m : N.t) (rg : Range) : VS.t :=
+    rangeEval (override I m rg) (realVersions (inst_repo I) m).
+
+  (* An edge as arborist's Edge holds one: the directory it walks for, the
+     package and range it accepts there, whether it is a peer, and whether
+     finding nothing meets it. *)
+  Record Edge : Type := MkEdge
+    { e_dir : N.t
+    ; e_name : N.t
+    ; e_range : Range
+    ; e_peer : bool
+    ; e_opt : bool }.
+
+  (* An optional dependency no published version satisfies is left
+     unplaced, as npm abandons it on ENOTARGET; any other is placed as a
+     dependency, since npm fetches it. *)
+  Definition depEdge (I : Inst) (d : Dependency) : Edge :=
+    MkEdge (d_dir d) (d_name d) (d_range d) false
+      (andb (d_optional d) (VS.is_empty (cands I (d_name d) (d_range d)))).
+
+  Definition peerEdge (r : PeerDependency) : Edge :=
+    MkEdge (p_dir r) (p_name r) (p_range r) true (p_optional r).
+
+  Definition activeDeps (I : Inst) (x : Occ.t) : list Dependency :=
+    match x with
+    | Occ.Top => ownedBy (inst_root I) (inst_deps I)
+    | Occ.Reg m v =>
+        List.filter (fun d => negb (d_dev d)) (ownedBy (m, v) (inst_deps I))
+    end.
+
+  Definition declPeers (I : Inst) (x : Occ.t) : list PeerDependency :=
+    match x with
+    | Occ.Top => ownedBy (inst_root I) (inst_peers I)
+    | Occ.Reg m v => ownedBy (m, v) (inst_peers I)
+    end.
+
+  (* A node keeps one edge per name, and a dependency replaces a peer. *)
+  Definition replaced (ds : list Dependency) (r : PeerDependency) : bool :=
+    List.existsb (fun d => NEqb.eqb (d_dir d) (p_dir r)) ds.
+
+  Definition edgesOf (I : Inst) (x : Occ.t) : list Edge :=
+    List.map (depEdge I) (activeDeps I x) ++
+    List.map peerEdge
+      (List.filter (fun r => negb (replaced (activeDeps I x) r))
+         (declPeers I x)).
+
+  (* The occupant must be the registry package the edge names, not only a
+     version in range as npm's satisfiedBy has it. *)
+  Definition Sat (I : Inst) (e : Edge) (x : Occ.t) : Prop :=
+    exists u, x = Occ.Reg (e_name e) u /\
+      VS.In u (cands I (e_name e) (e_range e)).
+
+  (* edge.js's errors: finding nothing is MISSING unless the edge is
+     optional; a copy found must satisfy the edge, and a peer's must not sit
+     in its declarer's own node_modules (PEER LOCAL). *)
+  Definition EdgeOk (I : Inst) (L : Pl.Layout.t) (l : Pl.Path.t) (e : Edge)
+      : Prop :=
+    match Pl.walk L l (e_dir e) with
+    | None => e_opt e = true
+    | Some (l', x) => Pl.Suffix l' (Pl.land (e_peer e) l) /\ Sat I e x
+    end.
+
+  Module SOkk := SetOps NKey NKey KeySet KeySet.
+  Definition keysOf (I : Inst) : KeySet.t :=
+    SOkk.ofList
+      (List.map (fun q => (d_dir (snd q), d_name (snd q))) (inst_deps I) ++
+       List.map (fun q => (p_dir (snd q), p_name (snd q))) (inst_peers I)).
+
+  Record IsResolution (I : Inst) (L : Pl.Layout.t) : Prop :=
+    { res_avail :
+        forall l a x, Pl.Layout.In (l, (a, x)) L ->
+        exists m v, x = Occ.Reg m v /\ KeySet.In (a, m) (keysOf I) /\
+          RepoSet.In (m, v) (inst_repo I)
+    ; res_occupancy :
+        forall l a x x', Pl.Layout.In (l, (a, x)) L ->
+        Pl.Layout.In (l, (a, x')) L -> x = x'
+    ; res_tree :
+        forall b l p, Pl.Layout.In (b :: l, p) L ->
+        exists x, Pl.Layout.In (l, (b, x)) L
+    ; res_root : forall e, In e (edgesOf I Occ.Top) -> EdgeOk I L nil e
+    ; res_edges :
+        forall l a x, Pl.Layout.In (l, (a, x)) L ->
+        forall e, In e (edgesOf I x) -> EdgeOk I L (a :: l) e }.
+
+  Module SOkp := SetOps NKey Pl.Pkg KeySet Pl.PkgSet.
+  Module SOvp := SetOps V Pl.Pkg VS Pl.PkgSet.
+  Definition placeRepo (I : Inst) : Pl.PkgSet.t :=
+    SOkp.unionMap (fun k =>
+        SOvp.map (fun v => (fst k, Occ.Reg (snd k) v))
+          (realVersions (inst_repo I) (snd k)))
+      (keysOf I).
+
+  Lemma mem_placeRepo : forall I a x,
+      Pl.PkgSet.In (a, x) (placeRepo I) <->
+      exists m v, x = Occ.Reg m v /\ KeySet.In (a, m) (keysOf I) /\
+        RepoSet.In (m, v) (inst_repo I).
+  Proof.
+    intros I a x; unfold placeRepo; rewrite SOkp.mem_unionMap; split.
+    - intros [[a' m] [Hk Hv]]; apply SOvp.mem_map in Hv.
+      destruct Hv as [v [Hv E]]; injection E as -> ->.
+      exists m, v; split; [reflexivity |].
+      split; [exact Hk | apply mem_realVersions; exact Hv].
+    - intros [m [v [-> [Hk Hv]]]]; exists (a, m); split; [exact Hk |].
+      apply SOvp.mem_map; exists v; split; [| reflexivity].
+      apply mem_realVersions; exact Hv.
+  Qed.
+
+  Definition rootOcc (I : Inst) : Pl.Pkg.t := (fst (inst_root I), Occ.Top).
+
+  Definition occs (I : Inst) : Pl.PkgSet.t :=
+    Pl.PkgSet.add (rootOcc I) (placeRepo I).
+
+  Module SOvo := SetOps V OccOT VS Pl.VSet.
+  Definition accepts (I : Inst) (e : Edge) : Pl.VSet.t :=
+    SOvo.map (Occ.Reg (e_name e)) (cands I (e_name e) (e_range e)).
+
+  Lemma mem_accepts : forall I e x,
+      Pl.VSet.In x (accepts I e) <-> Sat I e x.
+  Proof.
+    intros I e x; unfold accepts, Sat; rewrite SOvo.mem_map.
+    split; intros [u [H1 H2]]; exists u; split; assumption.
+  Qed.
+
+  Definition kindb (pe o : bool) (e : Edge) : bool :=
+    andb (Bool.eqb (e_peer e) pe) (Bool.eqb (e_opt e) o).
+
+  Module SOpd := SetOps Pl.Pkg Pl.C.DepElt Pl.PkgSet Pl.C.DepRel.
+  Definition edgeRel (I : Inst) (pe o : bool) : Pl.C.DepRel.t :=
+    SOpd.unionMap (fun p =>
+        SOpd.ofList
+          (List.map (fun e => (p, (e_dir e, accepts I e)))
+             (List.filter (kindb pe o) (edgesOf I (snd p)))))
+      (occs I).
+
+  Lemma mem_edgeRel : forall I pe o p n vs,
+      Pl.C.DepRel.In (p, (n, vs)) (edgeRel I pe o) <->
+      Pl.PkgSet.In p (occs I) /\
+      exists e, In e (edgesOf I (snd p)) /\ e_peer e = pe /\ e_opt e = o /\
+        n = e_dir e /\ vs = accepts I e.
+  Proof.
+    intros I pe o p n vs; unfold edgeRel; rewrite SOpd.mem_unionMap; split.
+    - intros [q [Hq H]]; apply SOpd.mem_ofList, in_map_iff in H.
+      destruct H as [e [E He]]; injection E as <- <- <-.
+      apply filter_In in He; destruct He as [He Hk].
+      unfold kindb in Hk; apply andb_true_iff in Hk.
+      rewrite !Bool.eqb_true_iff in Hk; destruct Hk as [Hp Ho].
+      split; [exact Hq |]; exists e; auto.
+    - intros [Hq [e [He [Hp [Ho [-> ->]]]]]]; exists p; split; [exact Hq |].
+      apply SOpd.mem_ofList, in_map_iff; exists e; split; [reflexivity |].
+      apply filter_In; split; [exact He |].
+      unfold kindb; rewrite Hp, Ho, !Bool.eqb_reflx; reflexivity.
+  Qed.
+
+  (* The npm instance as a placement instance: a key holds every package
+     some entry aliases to it, and an occupant's edges are its package's. *)
+  Definition tr (I : Inst) : Pl.Inst :=
+    {| Pl.inst_repo := placeRepo I
+     ; Pl.inst_deps := edgeRel I false false
+     ; Pl.inst_peers := edgeRel I true false
+     ; Pl.inst_optDeps := edgeRel I false true
+     ; Pl.inst_optPeers := edgeRel I true true
+     ; Pl.inst_root := rootOcc I |}.
+
+  Lemma rel_tr : forall I pe o, Pl.rel (tr I) pe o = edgeRel I pe o.
+  Proof. intros I [|] [|]; reflexivity. Qed.
+
+  Lemma edgeOk_meets : forall I L l e,
+      EdgeOk I L l e <->
+      Pl.Meets L l (Pl.land (e_peer e) l) (e_dir e) (accepts I e) (e_opt e).
+  Proof.
+    intros I L l e; unfold EdgeOk, Pl.Meets, Pl.Resolves.
+    destruct (Pl.walk L l (e_dir e)) as [[l' x] |]; split.
+    - intros [Hs Hx]; left; exists l', x; split; [reflexivity |].
+      split; [exact Hs | apply mem_accepts; exact Hx].
+    - intros [[l0 [u [E [Hs Hu]]]] | [_ E]]; [| discriminate E].
+      injection E as <- <-; split; [exact Hs | apply mem_accepts; exact Hu].
+    - intro Ho; right; split; [exact Ho | reflexivity].
+    - intros [[l0 [u [E _]]] | [Ho _]]; [discriminate E | exact Ho].
+  Qed.
+
+  Theorem tr_resolution : forall I L,
+      Pl.IsResolution (tr I) L <-> IsResolution I L.
+  Proof.
+    intros I L; split.
+    - intros [Hsub Hocc Htree Hroot Hdeps].
+      assert (Hholds : forall p l, Pl.Holds (tr I) L l p ->
+                 Pl.PkgSet.In p (occs I) ->
+                 forall e, In e (edgesOf I (snd p)) -> EdgeOk I L l e).
+      { intros p l Hh Hp e He; apply edgeOk_meets, Hh.
+        rewrite rel_tr, mem_edgeRel; split; [exact Hp |].
+        exists e; auto. }
+      constructor.
+      + intros l a x H; apply mem_placeRepo, (Hsub l (a, x) H).
+      + exact Hocc.
+      + exact Htree.
+      + exact (Hholds (rootOcc I) nil Hroot
+                 (proj2 (Pl.PkgSet.add_spec _ _ _) (or_introl eq_refl))).
+      + intros l a x H; apply (Hholds (a, x) (a :: l) (Hdeps l (a, x) H)).
+        apply Pl.PkgSet.add_spec; right; exact (Hsub l (a, x) H).
+    - intros [Havail Hocc Htree Hroot Hedges].
+      assert (Hholds : forall p l,
+                 (forall e, In e (edgesOf I (snd p)) -> EdgeOk I L l e) ->
+                 Pl.Holds (tr I) L l p).
+      { intros p l He pe o n vs HE; rewrite rel_tr, mem_edgeRel in HE.
+        destruct HE as [_ [e [Hin [<- [<- [-> ->]]]]]].
+        apply edgeOk_meets, He; exact Hin. }
+      constructor.
+      + intros l [a x] H; apply mem_placeRepo, (Havail l a x H).
+      + exact Hocc.
+      + exact Htree.
+      + apply Hholds; exact Hroot.
+      + intros l [a x] H; apply Hholds; exact (Hedges l a x H).
+  Qed.
+
+  (* The npm reduction: the placement reduction of the translation.
+     Placement's Reduction is named in full, as an alias of it inside this
+     functor trips a kernel anomaly when the functor is applied. *)
+  Definition reduceReal (I : Inst) (depth : nat) : Pl.Reduction.T.PkgSet.t :=
+    Pl.Reduction.reduceReal (tr I) depth.
+
+  Definition reduceDeps (I : Inst) (depth : nat) : Pl.Reduction.T.DepRel.t :=
+    Pl.Reduction.reduceDeps (tr I) depth.
+
+  Definition rootPkg (I : Inst) : Pl.Reduction.T.Pkg.t :=
+    Pl.Reduction.rootPkg (tr I).
+
+  Theorem npm_soundness : forall I depth S,
+      Pl.Reduction.T.IsResolution (reduceReal I depth) (reduceDeps I depth)
+        (rootPkg I) S ->
+      IsResolution I (Pl.Reduction.placementResolution S) /\
+      Pl.Depth depth (Pl.Reduction.placementResolution S).
+  Proof.
+    intros I depth S H.
+    destruct (Pl.Reduction.placement_soundness _ _ _ H) as [H1 H2].
+    split; [apply tr_resolution; exact H1 | exact H2].
+  Qed.
+
+  Theorem npm_completeness : forall I depth L,
+      IsResolution I L -> Pl.Depth depth L ->
+      Pl.Reduction.T.IsResolution (reduceReal I depth) (reduceDeps I depth)
+        (rootPkg I) (Pl.Reduction.coreResolution (tr I) depth L).
+  Proof.
+    intros I depth L H Hd; apply Pl.Reduction.placement_completeness;
+      [apply tr_resolution; exact H | exact Hd].
+  Qed.
+
+  Theorem npm_roundtrip : forall I depth L,
+      IsResolution I L -> Pl.Depth depth L ->
+      Pl.Reduction.placementResolution
+        (Pl.Reduction.coreResolution (tr I) depth L) = L.
+  Proof.
+    intros I depth L H Hd;
+      apply Pl.Reduction.placementResolution_coreResolution;
+      [apply tr_resolution; exact H | exact Hd].
+  Qed.
+
+  Module Lookup.
+    (* Where two instances agree on which packages a key may hold. *)
+    Definition AgreesAtKey (I' I : Inst) (a : N.t) : Prop :=
+      forall m v,
+        (KeySet.In (a, m) (keysOf I') /\ RepoSet.In (m, v) (inst_repo I')) <->
+        (KeySet.In (a, m) (keysOf I) /\ RepoSet.In (m, v) (inst_repo I)).
+
+    Lemma keyVersions_agree : forall I' I a, AgreesAtKey I' I a ->
+        Pl.repoVersions (placeRepo I') a = Pl.repoVersions (placeRepo I) a.
+    Proof.
+      intros I' I a H; apply Pl.repoVersions_ext; intro x.
+      rewrite !mem_placeRepo; split; intros [m [v [-> Hk]]];
+        exists m, v; split; try reflexivity; apply H; exact Hk.
+    Qed.
+
+    (* A location's and a walk's versions read the key's packages alone. *)
+    Definition nameInst (I : Inst) : Pl.Inst :=
+      {| Pl.inst_repo := placeRepo I
+       ; Pl.inst_deps := Pl.C.DepRel.empty
+       ; Pl.inst_peers := Pl.C.DepRel.empty
+       ; Pl.inst_optDeps := Pl.C.DepRel.empty
+       ; Pl.inst_optPeers := Pl.C.DepRel.empty
+       ; Pl.inst_root := rootOcc I |}.
+
+    Theorem versions_lookupLoc : forall I I' depth l a,
+        Pl.Reduction.Lookup.Reached (tr I) depth (Pl.Reduction.Name.Loc l a) ->
+        AgreesAtKey I' I a ->
+        Pl.Reduction.T.versions (reduceReal I depth)
+          (Pl.Reduction.Name.Loc l a) =
+        Pl.Reduction.versions (nameInst I') depth (Pl.Reduction.Name.Loc l a).
+    Proof.
+      intros I I' depth l a H Ha; unfold reduceReal.
+      rewrite (Pl.Reduction.Lookup.versions_lookupLoc _ _ _ _ H).
+      unfold Pl.Reduction.versions, Pl.Reduction.Lookup.nameSubInst, nameInst,
+        tr, rootOcc; cbn [Pl.inst_repo].
+      rewrite Pl.Reduction.Lookup.versions_fibre, (keyVersions_agree _ _ _ Ha).
+      reflexivity.
+    Qed.
+
+    Theorem versions_lookupWalk : forall I I' depth l a,
+        Pl.Reduction.Lookup.Reached (tr I) depth (Pl.Reduction.Name.Walk l a) ->
+        AgreesAtKey I' I a ->
+        Pl.Reduction.T.versions (reduceReal I depth)
+          (Pl.Reduction.Name.Walk l a) =
+        Pl.Reduction.versions (nameInst I') depth (Pl.Reduction.Name.Walk l a).
+    Proof.
+      intros I I' depth l a H Ha; unfold reduceReal.
+      rewrite (Pl.Reduction.Lookup.versions_lookupWalk _ _ _ _ H).
+      unfold Pl.Reduction.versions, Pl.Reduction.Lookup.nameSubInst, nameInst,
+        tr, rootOcc; cbn [Pl.inst_repo].
+      rewrite Pl.Reduction.Lookup.versions_fibre, (keyVersions_agree _ _ _ Ha).
+      reflexivity.
+    Qed.
+
+    (* An edge's atom reads the location, the edge, and the packages it
+       accepts, so the driver computes the accepted set once per package
+       and range and the atom once per location and edge. *)
+    Definition atomOf (lam : Pl.Path.t) (e : Edge) (xs : Pl.VSet.t)
+        : Pl.Reduction.T.Dependees.t :=
+      (Pl.Reduction.Name.Walk lam (e_dir e),
+       Pl.Reduction.admit (e_opt e) (Pl.land (e_peer e) lam) xs).
+
+    Definition edgeAtom (I : Inst) (lam : Pl.Path.t) (e : Edge)
+        : Pl.Reduction.T.Dependees.t :=
+      atomOf lam e (accepts I e).
+
+    Module SOhh := SetOps Pl.Reduction.T.Dependees Pl.Reduction.T.Dependees
+      Pl.Reduction.T.DependeesSet Pl.Reduction.T.DependeesSet.
+    Definition occAtoms (I : Inst) (lam : Pl.Path.t) (x : Occ.t)
+        : Pl.Reduction.T.DependeesSet.t :=
+      SOhh.ofList (List.map (edgeAtom I lam) (edgesOf I x)).
+
+    Lemma edgeAtoms_tr : forall I p lam, Pl.PkgSet.In p (occs I) ->
+        Pl.Reduction.edgeAtoms (tr I) p lam = occAtoms I lam (snd p).
+    Proof.
+      intros I p lam Hp; apply Pl.Reduction.T.DependeesSet.ext; intro h.
+      rewrite Pl.Reduction.mem_edgeAtoms; unfold occAtoms.
+      rewrite SOhh.mem_ofList, in_map_iff; split.
+      - intros [pe [o [n [vs [HE ->]]]]]; rewrite rel_tr, mem_edgeRel in HE.
+        destruct HE as [_ [e [He [<- [<- [-> ->]]]]]].
+        exists e; split; [reflexivity | exact He].
+      - intros [e [<- He]].
+        exists (e_peer e), (e_opt e), (e_dir e), (accepts I e).
+        split; [| reflexivity].
+        rewrite rel_tr, mem_edgeRel; split; [exact Hp |].
+        exists e; auto.
+    Qed.
+
+    Theorem dependees_lookupRoot : forall I depth,
+        Pl.Reduction.T.dependees (reduceDeps I depth) (rootPkg I) =
+        occAtoms I nil Occ.Top.
+    Proof.
+      intros I depth; unfold reduceDeps, rootPkg.
+      rewrite Pl.Reduction.dependees_reduceDeps.
+      - cbn [Pl.Reduction.rootPkg Pl.Reduction.dependees tr Pl.inst_root
+               rootOcc snd]; unfold Pl.Reduction.occDeps.
+        rewrite (edgeAtoms_tr I (rootOcc I) nil)
+          by (apply Pl.PkgSet.add_spec; left; reflexivity).
+        apply Pl.Reduction.T.DependeesSet.ext; intro h.
+        rewrite Pl.Reduction.T.DependeesSet.union_spec.
+        cbn [Pl.par Pl.Reduction.treeAtom rootOcc snd]; split.
+        + intros [H | H]; [| exact H].
+          destruct (Pl.Reduction.T.DependeesSet.empty_spec H).
+        + intro H; right; exact H.
+      - apply Pl.Reduction.mem_reduceReal; split; [exact Logic.I |].
+        apply Pl.Reduction.T.VSet.singleton_spec; reflexivity.
+    Qed.
+
+    (* The driver's form: the Tree atom, then one atom per edge. *)
+    Theorem dependees_lookupOcc : forall I depth l a x,
+        Pl.Reduction.T.PkgSet.In
+          (Pl.Reduction.Name.Loc l a, Pl.Reduction.Version.Occ x)
+          (reduceReal I depth) ->
+        Pl.Reduction.T.dependees (reduceDeps I depth)
+          (Pl.Reduction.Name.Loc l a, Pl.Reduction.Version.Occ x) =
+        Pl.Reduction.T.DependeesSet.union
+          (Pl.Reduction.treeAtom (placeRepo I) l) (occAtoms I (a :: l) x).
+    Proof.
+      intros I depth l a x H; unfold reduceDeps.
+      rewrite (Pl.Reduction.dependees_reduceDeps _ _ _ H).
+      apply Pl.Reduction.mem_reduceReal in H; destruct H as [_ H].
+      apply Pl.Reduction.mem_versions_loc in H.
+      destruct H as [E | [v [_ [Hv E]]]]; [discriminate E |].
+      injection E as ->; cbn [Pl.Reduction.dependees].
+      unfold Pl.Reduction.occDeps.
+      rewrite (edgeAtoms_tr I (a, v) (a :: l))
+        by (apply Pl.PkgSet.add_spec; right; exact Hv).
+      reflexivity.
+    Qed.
+
+    Theorem dependees_lookupWalk : forall I depth l a w,
+        Pl.Reduction.T.PkgSet.In (Pl.Reduction.Name.Walk l a, w)
+          (reduceReal I depth) ->
+        Pl.Reduction.T.dependees (reduceDeps I depth)
+          (Pl.Reduction.Name.Walk l a, w) =
+        Pl.Reduction.walkDeps l a w.
+    Proof.
+      intros I depth l a w H.
+      exact (Pl.Reduction.Lookup.dependees_lookupWalk _ _ _ _ _ H).
+    Qed.
+
+    Theorem dependees_lookupAbsent : forall I depth l a,
+        Pl.Reduction.T.dependees (reduceDeps I depth)
+          (Pl.Reduction.Name.Loc l a, Pl.Reduction.Version.Bot) =
+        Pl.Reduction.T.DependeesSet.empty.
+    Proof. intros; apply Pl.Reduction.Lookup.dependees_lookupAbsent. Qed.
+
+    (* Where two instances agree on an occupant's own edges: its package's
+       manifest, the overrides, and the packages its edges name. *)
+    Definition AgreesAtOcc (I' I : Inst) (x : Occ.t) : Prop :=
+      activeDeps I' x = activeDeps I x /\ declPeers I' x = declPeers I x /\
+      inst_ovr I' = inst_ovr I /\
+      forall e, In e (edgesOf I x) -> forall u,
+        RepoSet.In (e_name e, u) (inst_repo I') <->
+        RepoSet.In (e_name e, u) (inst_repo I).
+
+    Lemma cands_agree : forall I' I m rg,
+        inst_ovr I' = inst_ovr I ->
+        (forall u, RepoSet.In (m, u) (inst_repo I') <->
+                   RepoSet.In (m, u) (inst_repo I)) ->
+        cands I' m rg = cands I m rg.
+    Proof.
+      intros I' I m rg Ho Hr; unfold cands, override; rewrite Ho; f_equal.
+      apply VS.ext; intro u; rewrite !mem_realVersions; exact (Hr u).
+    Qed.
+
+    Lemma edgesOf_agree : forall I' I x, AgreesAtOcc I' I x ->
+        edgesOf I' x = edgesOf I x.
+    Proof.
+      intros I' I x [Hd [Hp [Ho Hr]]]; unfold edgesOf; rewrite Hd, Hp.
+      f_equal; apply map_ext_in; intros d Hin; unfold depEdge.
+      rewrite (cands_agree I' I); [reflexivity | exact Ho |].
+      intro u; apply (Hr (depEdge I d)); unfold edgesOf.
+      apply in_or_app; left; apply in_map; exact Hin.
+    Qed.
+
+    Theorem occAtoms_agree : forall I' I lam x, AgreesAtOcc I' I x ->
+        occAtoms I' lam x = occAtoms I lam x.
+    Proof.
+      intros I' I lam x H; unfold occAtoms; rewrite (edgesOf_agree _ _ _ H).
+      f_equal; apply map_ext_in; intros e He; unfold edgeAtom, accepts.
+      destruct H as [_ [_ [Ho Hr]]].
+      rewrite (cands_agree I' I _ _ Ho (Hr e He)); reflexivity.
+    Qed.
+
+    Theorem treeAtom_agree : forall I' I b l, AgreesAtKey I' I b ->
+        Pl.Reduction.treeAtom (placeRepo I') (b :: l) =
+        Pl.Reduction.treeAtom (placeRepo I) (b :: l).
+    Proof.
+      intros I' I b l H; cbn [Pl.Reduction.treeAtom].
+      rewrite (keyVersions_agree _ _ _ H); reflexivity.
+    Qed.
+  End Lookup.
+End NpmPlacement.
diff --git a/theories/Placement.v b/theories/Placement.v
index c79a61a..eaacb18 100644
--- a/theories/Placement.v
+++ b/theories/Placement.v
@@ -22,8 +22,24 @@ Module Placement (N V : UsualOrderedType).
     { inst_repo : PkgSet.t
     ; inst_deps : C.DepRel.t
     ; inst_peers : C.DepRel.t
+    ; inst_optDeps : C.DepRel.t
+    ; inst_optPeers : C.DepRel.t
     ; inst_root : Pkg.t }.
 
+  (* An edge's kind: a peer refuses its declarer's own directory, and an
+     optional edge is also met when its walk finds nothing, though a copy
+     it finds must still be in range. *)
+  Definition rel (I : Inst) (pe o : bool) : C.DepRel.t :=
+    match pe, o with
+    | false, false => inst_deps I
+    | true, false => inst_peers I
+    | false, true => inst_optDeps I
+    | true, true => inst_optPeers I
+    end.
+
+  Definition land (pe : bool) (l : Path.t) : Path.t :=
+    if pe then par l else l.
+
   (* Core's versions inserts one version at a time, quadratic in a name's
      versions; this sorts them in one go. *)
   Definition repoVersions (R : PkgSet.t) (a : N.t) : VSet.t :=
@@ -82,12 +98,14 @@ Module Placement (N V : UsualOrderedType).
       : Prop :=
     exists l' u, walk L l n = Some (l', u) /\ Suffix l' la /\ VSet.In u vs.
 
+  Definition Meets (L : Layout.t) (l la : Path.t) (n : N.t) (vs : VSet.t)
+      (o : bool) : Prop :=
+    Resolves L l la n vs \/ (o = true /\ walk L l n = None).
+
   (* The root's peers may land in its own directory, as par nil is nil. *)
   Definition Holds (I : Inst) (L : Layout.t) (l : Path.t) (p : Pkg.t) : Prop :=
-    (forall n vs, C.DepRel.In (p, (n, vs)) (inst_deps I) ->
-       Resolves L l l n vs) /\
-    (forall n vs, C.DepRel.In (p, (n, vs)) (inst_peers I) ->
-       Resolves L l (par l) n vs).
+    forall pe o n vs, C.DepRel.In (p, (n, vs)) (rel I pe o) ->
+      Meets L l (land pe l) n vs o.
 
   Record IsResolution (I : Inst) (L : Layout.t) : Prop :=
     { res_subset :
@@ -130,8 +148,7 @@ Module Placement (N V : UsualOrderedType).
   Qed.
 
   Definition Edge (I : Inst) (p : Pkg.t) (n : N.t) : Prop :=
-    exists vs, C.DepRel.In (p, (n, vs)) (inst_deps I) \/
-               C.DepRel.In (p, (n, vs)) (inst_peers I).
+    exists pe o vs, C.DepRel.In (p, (n, vs)) (rel I pe o).
 
   Inductive Reaches (I : Inst) (L : Layout.t) : OccElt.t -> Prop :=
   | ReachesRoot : forall n l' u,
@@ -180,6 +197,23 @@ Module Placement (N V : UsualOrderedType).
       + rewrite (Hnone _ Hc); exact (IH Hw Hin).
   Qed.
 
+  Lemma walk_none_restrict : forall L L' l a,
+      (forall o, Layout.In o L' -> Layout.In o L) ->
+      walk L l a = None -> walk L' l a = None.
+  Proof.
+    intros L L' l a Hsub.
+    assert (Hnone : forall l, VSet.choose (occupants L l a) = None ->
+               VSet.choose (occupants L' l a) = None).
+    { intros l0 Hc; apply VSet.choose_spec2 in Hc.
+      destruct (VSet.choose (occupants L' l0 a)) as [x |] eqn:Hc';
+        [| reflexivity].
+      apply VSet.choose_spec1, mem_occupants, Hsub in Hc'.
+      destruct (Hc x); apply mem_occupants; exact Hc'. }
+    induction l as [| b l IH]; intro Hw; cbn [walk] in Hw |- *;
+      destruct (VSet.choose (occupants L _ a)) eqn:Hc; try discriminate Hw;
+      rewrite (Hnone _ Hc); [reflexivity | exact (IH Hw)].
+  Qed.
+
   Definition Settled (I : Inst) (L : Layout.t) (w : Path.t) : Prop :=
     forall b l u, Suffix (b :: l) w -> Layout.In (l, (b, u)) L ->
     Reaches I L (l, (b, u)).
@@ -220,18 +254,14 @@ Module Placement (N V : UsualOrderedType).
                (forall n l' u, Edge I p n -> walk L w n = Some (l', u) ->
                   Reaches I L (l', (n, u))) ->
                Holds I L' w p).
-    { intros w p [Hd Hp] Hr.
-      assert (Hw : forall n vs la, Edge I p n -> Resolves L w la n vs ->
-                 Resolves L' w la n vs).
-      { intros n vs la He [l' [u [Hw [Hs Hu]]]]; exists l', u.
-        split; [| split; assumption].
+    { intros w p Hh Hr pe o n vs HE.
+      assert (He : Edge I p n) by (exists pe, o, vs; exact HE).
+      destruct (Hh _ _ _ _ HE) as [[l' [u [Hw [Hs Hu]]]] | [Ho Hw]].
+      - left; exists l', u; split; [| split; assumption].
         apply (walk_restrict L L' w n l' u HinL Hocc Hw), Hin'.
-        exact (Hr _ _ _ He Hw). }
-      split; intros n vs HE; apply Hw.
-      - exists vs; left; exact HE.
-      - exact (Hd _ _ HE).
-      - exists vs; right; exact HE.
-      - exact (Hp _ _ HE). }
+        exact (Hr _ _ _ He Hw).
+      - right; split; [exact Ho |].
+        exact (walk_none_restrict L L' w n HinL Hw). }
     constructor.
     - intros l p H; exact (Hsub _ _ (HinL _ H)).
     - intros l a v v' H H'; exact (Hocc _ _ _ _ (HinL _ H) (HinL _ H')).
@@ -365,10 +395,15 @@ Module Placement (N V : UsualOrderedType).
     Module SOpn := SetOps Pkg N PkgSet NSet.
     Module SOdn := SetOps C.DepElt N C.DepRel NSet.
     Module SOnn := SetOps N N NSet NSet.
+    Definition relNames (E : C.DepRel.t) : NSet.t :=
+      SOdn.map (fun e => fst (snd e)) E.
+
     Definition locNames (I : Inst) : NSet.t :=
       NSet.union (SOpn.map fst (inst_repo I))
-        (NSet.union (SOdn.map (fun e => fst (snd e)) (inst_deps I))
-           (SOdn.map (fun e => fst (snd e)) (inst_peers I))).
+        (NSet.union
+           (NSet.union (relNames (inst_deps I)) (relNames (inst_peers I)))
+           (NSet.union (relNames (inst_optDeps I))
+              (relNames (inst_optPeers I)))).
 
     Lemma locNames_repo : forall I a v,
         PkgSet.In (a, v) (inst_repo I) -> NSet.In a (locNames I).
@@ -377,14 +412,15 @@ Module Placement (N V : UsualOrderedType).
       apply SOpn.mem_map; exists (a, v); split; [exact H | reflexivity].
     Qed.
 
-    Lemma locNames_deps : forall I p n vs,
-        C.DepRel.In (p, (n, vs)) (inst_deps I) \/
-        C.DepRel.In (p, (n, vs)) (inst_peers I) -> NSet.In n (locNames I).
+    Lemma locNames_deps : forall I pe o p n vs,
+        C.DepRel.In (p, (n, vs)) (rel I pe o) -> NSet.In n (locNames I).
     Proof.
-      intros I p n vs H; apply NSet.union_spec; right.
-      apply NSet.union_spec; destruct H as [H | H]; [left | right];
-        apply SOdn.mem_map; exists (p, (n, vs)); split;
-        [exact H | reflexivity | exact H | reflexivity].
+      intros I pe o p n vs H; apply NSet.union_spec; right.
+      assert (Hn : NSet.In n (relNames (rel I pe o)))
+        by (apply SOdn.mem_map; exists (p, (n, vs)); split;
+            [exact H | reflexivity]).
+      rewrite !NSet.union_spec.
+      destruct pe, o; cbn [rel] in Hn; tauto.
     Qed.
 
     Definition LocPath (I : Inst) (l : Path.t) : Prop :=
@@ -555,19 +591,36 @@ Module Placement (N V : UsualOrderedType).
     Definition accept (l : Path.t) (vs : VSet.t) : T.VSet.t :=
       along (fun _ => true) l vs.
 
+    (* An optional edge's walk may also find nothing. *)
+    Definition admit (o : bool) (la : Path.t) (vs : VSet.t) : T.VSet.t :=
+      if o then T.VSet.add Version.Bot (accept la vs) else accept la vs.
+
+    Lemma mem_admit : forall o la vs w,
+        T.VSet.In w (admit o la vs) <->
+        (o = true /\ w = Version.Bot) \/ T.VSet.In w (accept la vs).
+    Proof.
+      intros [|] la vs w; cbn [admit].
+      - rewrite SOvt.add_in; split.
+        + intros [H | H]; [left; split; [reflexivity | exact H] |].
+          right; exact H.
+        + intros [[_ H] | H]; [left; exact H | right; exact H].
+      - split; [intro H; right; exact H |].
+        intros [[E _] | H]; [discriminate E | exact H].
+    Qed.
+
     Module SOdh := SetOps C.DepElt T.Dependees C.DepRel T.DependeesSet.
-    Definition atoms (E : C.DepRel.t) (p : Pkg.t) (l la : Path.t)
+    Definition atoms (o : bool) (E : C.DepRel.t) (p : Pkg.t) (l la : Path.t)
         : T.DependeesSet.t :=
       SOdh.filterMap (fun '(q, (n, vs)) =>
-          if Pkg.eq_dec q p then Some (Name.Walk l n, accept la vs) else None)
+          if Pkg.eq_dec q p then Some (Name.Walk l n, admit o la vs) else None)
         E.
 
-    Lemma mem_atoms : forall E p l la h,
-        T.DependeesSet.In h (atoms E p l la) <->
+    Lemma mem_atoms : forall o E p l la h,
+        T.DependeesSet.In h (atoms o E p l la) <->
         exists n vs, C.DepRel.In (p, (n, vs)) E /\
-          h = (Name.Walk l n, accept la vs).
+          h = (Name.Walk l n, admit o la vs).
     Proof.
-      intros E p l la h; unfold atoms; rewrite SOdh.mem_filterMap; split.
+      intros o E p l la h; unfold atoms; rewrite SOdh.mem_filterMap; split.
       - intros [[q [n vs]] [He H]]; cbn beta iota in H.
         destruct (Pkg.eq_dec q p) as [-> |]; [| discriminate H].
         injection H as <-; exists n, vs; split; [exact He | reflexivity].
@@ -575,6 +628,32 @@ Module Placement (N V : UsualOrderedType).
         cbn beta iota; apply dec_refl.
     Qed.
 
+    Definition kindAtoms (I : Inst) (pe o : bool) (p : Pkg.t) (l : Path.t)
+        : T.DependeesSet.t :=
+      atoms o (rel I pe o) p l (land pe l).
+
+    Definition edgeAtoms (I : Inst) (p : Pkg.t) (l : Path.t)
+        : T.DependeesSet.t :=
+      T.DependeesSet.union
+        (T.DependeesSet.union (kindAtoms I false false p l)
+           (kindAtoms I true false p l))
+        (T.DependeesSet.union (kindAtoms I false true p l)
+           (kindAtoms I true true p l)).
+
+    Lemma mem_edgeAtoms : forall I p l h,
+        T.DependeesSet.In h (edgeAtoms I p l) <->
+        exists pe o n vs, C.DepRel.In (p, (n, vs)) (rel I pe o) /\
+          h = (Name.Walk l n, admit o (land pe l) vs).
+    Proof.
+      intros I p l h; unfold edgeAtoms, kindAtoms.
+      rewrite !T.DependeesSet.union_spec, !mem_atoms; split.
+      - intros [[H | H] | [H | H]]; destruct H as [n [vs H]];
+          eexists _, _, n, vs; exact H.
+      - intros [pe [o [n [vs H]]]].
+        destruct pe, o; [right; right | left; right | right; left | left; left];
+          exists n, vs; exact H.
+    Qed.
+
     Definition treeAtom (R : PkgSet.t) (l : Path.t) : T.DependeesSet.t :=
       match l with
       | nil => T.DependeesSet.empty
@@ -585,9 +664,7 @@ Module Placement (N V : UsualOrderedType).
 
     Definition occDeps (I : Inst) (l : Path.t) (p : Pkg.t)
         : T.DependeesSet.t :=
-      T.DependeesSet.union (treeAtom (inst_repo I) (par l))
-        (T.DependeesSet.union (atoms (inst_deps I) p l l)
-           (atoms (inst_peers I) p l (par l))).
+      T.DependeesSet.union (treeAtom (inst_repo I) (par l)) (edgeAtoms I p l).
 
     Definition walkDeps (l : Path.t) (a : N.t) (w : Version.t)
         : T.DependeesSet.t :=
@@ -749,23 +826,19 @@ Module Placement (N V : UsualOrderedType).
            exists w, T.VSet.In w ws /\ T.PkgSet.In (n, w) S) ->
         Holds I (placementResolution S) l p.
     Proof.
-      intros I depth S l p Hres Hcl.
-      assert (Hat : forall E la,
-                 (forall h, T.DependeesSet.In h (atoms E p l la) ->
-                    T.DependeesSet.In h (occDeps I l p)) ->
-                 forall n vs, C.DepRel.In (p, (n, vs)) E ->
-                 Resolves (placementResolution S) l la n vs).
-      { intros E la Hin n vs HE.
-        assert (Ha : T.DependeesSet.In (Name.Walk l n, accept la vs)
-                       (atoms E p l la))
-          by (apply mem_atoms; exists n, vs; split; [exact HE | reflexivity]).
-        destruct (Hcl _ _ (Hin _ Ha)) as [w [Hw HS]].
-        unfold accept in Hw; apply mem_along in Hw.
+      intros I depth S l p Hres Hcl pe o n vs HE.
+      assert (Ha : T.DependeesSet.In (Name.Walk l n, admit o (land pe l) vs)
+                     (occDeps I l p)).
+      { apply T.DependeesSet.union_spec; right; apply mem_edgeAtoms.
+        exists pe, o, n, vs; split; [exact HE | reflexivity]. }
+      destruct (Hcl _ _ Ha) as [w [Hw HS]].
+      pose proof (walk_decode I depth S Hres _ _ _ HS) as Hwalk.
+      apply mem_admit in Hw; destruct Hw as [[Ho ->] | Hw].
+      - right; split; [exact Ho | exact Hwalk].
+      - unfold accept in Hw; apply mem_along in Hw.
         destruct Hw as [l' [u [Hs [_ [Hu ->]]]]].
-        exists l', u; split; [exact (walk_decode I depth S Hres _ _ _ HS) |].
-        split; [exact Hs | exact Hu]. }
-      split; apply Hat; intros h Hh; unfold occDeps;
-        rewrite !T.DependeesSet.union_spec; tauto.
+        left; exists l', u; split; [exact Hwalk |].
+        split; [exact Hs | exact Hu].
     Qed.
 
     Theorem placement_soundness : forall I depth S,
@@ -864,23 +937,24 @@ Module Placement (N V : UsualOrderedType).
 
     Lemma holds_met : forall I depth L l p,
         length l <= depth -> LocPath I l -> Holds I L l p ->
-        forall n ws, T.DependeesSet.In (n, ws)
-          (T.DependeesSet.union (atoms (inst_deps I) p l l)
-             (atoms (inst_peers I) p l (par l))) ->
+        forall n ws, T.DependeesSet.In (n, ws) (edgeAtoms I p l) ->
         exists w, T.VSet.In w ws /\ T.PkgSet.In (n, w) (coreResolution I depth L).
     Proof.
-      intros I depth L l p Hlen Hk [Hd Hp] n ws Hh.
-      apply T.DependeesSet.union_spec in Hh; destruct Hh as [Hh | Hh];
-        apply mem_atoms in Hh; destruct Hh as [m [vs [HE E]]];
-        injection E as -> ->; apply resolves_met.
-      - exact Hlen.
-      - apply List.Forall_cons;
-          [exact (locNames_deps I p m vs (or_introl HE)) | exact Hk].
-      - exact (Hd _ _ HE).
-      - exact Hlen.
-      - apply List.Forall_cons;
-          [exact (locNames_deps I p m vs (or_intror HE)) | exact Hk].
-      - exact (Hp _ _ HE).
+      intros I depth L l p Hlen Hk Hh n ws Hn.
+      apply mem_edgeAtoms in Hn; destruct Hn as [pe [o [m [vs [HE E]]]]].
+      injection E as -> ->.
+      assert (Hr : InRange I depth (Name.Walk l m))
+        by (split; [exact Hlen |];
+            apply List.Forall_cons;
+            [exact (locNames_deps I pe o p m vs HE) | exact Hk]).
+      destruct (Hh _ _ _ _ HE) as [Hres | [Ho Hw]].
+      - destruct (resolves_met I depth L l (land pe l) m vs Hlen
+                    (proj2 Hr) Hres) as [w [Hw HS]].
+        exists w; split; [apply mem_admit; right; exact Hw | exact HS].
+      - exists Version.Bot; split; [apply mem_admit; left; split;
+                                    [exact Ho | reflexivity] |].
+        apply mem_coreResolution; split; [exact Hr |].
+        cbn [value]; rewrite Hw; reflexivity.
     Qed.
 
     Lemma walk_par_inRange : forall I depth l a,
@@ -1031,6 +1105,8 @@ Module Placement (N V : UsualOrderedType).
         {| inst_repo := PkgFibred.tailFibre (inst_repo I) a
          ; inst_deps := C.DepRel.empty
          ; inst_peers := C.DepRel.empty
+         ; inst_optDeps := C.DepRel.empty
+         ; inst_optPeers := C.DepRel.empty
          ; inst_root := inst_root I |}.
 
       Definition occSubInst (I : Inst) (l : Path.t) (p : Pkg.t) : Inst :=
@@ -1040,6 +1116,8 @@ Module Placement (N V : UsualOrderedType).
                         end
          ; inst_deps := DepFibred.tailFibre (inst_deps I) p
          ; inst_peers := DepFibred.tailFibre (inst_peers I) p
+         ; inst_optDeps := DepFibred.tailFibre (inst_optDeps I) p
+         ; inst_optPeers := DepFibred.tailFibre (inst_optPeers I) p
          ; inst_root := inst_root I |}.
 
       Definition Reached (I : Inst) (depth : nat) (n : Name.t) : Prop :=
@@ -1053,21 +1131,29 @@ Module Placement (N V : UsualOrderedType).
         split; [intros [H _]; exact H | intro H; split; [exact H | reflexivity]].
       Qed.
 
-      Lemma atoms_fibre : forall E p l la,
-          atoms (DepFibred.tailFibre E p) p l la = atoms E p l la.
+      Lemma atoms_fibre : forall o E p l la,
+          atoms o (DepFibred.tailFibre E p) p l la = atoms o E p l la.
       Proof.
-        intros E p l la; apply T.DependeesSet.ext; intro h; rewrite !mem_atoms.
+        intros o E p l la; apply T.DependeesSet.ext; intro h.
+        rewrite !mem_atoms.
         split; intros [n [vs [HE ->]]]; exists n, vs; (split; [| reflexivity]).
         - apply DepFibred.mem_tailFibre in HE; exact (proj1 HE).
         - apply DepFibred.mem_tailFibre; split; [exact HE | reflexivity].
       Qed.
 
+      Lemma edgeAtoms_sub : forall I l' l p,
+          edgeAtoms (occSubInst I l' p) p l = edgeAtoms I p l.
+      Proof.
+        intros I l' l p; unfold edgeAtoms, kindAtoms; cbn [rel occSubInst
+          inst_deps inst_peers inst_optDeps inst_optPeers].
+        rewrite !atoms_fibre; reflexivity.
+      Qed.
+
       Lemma occDeps_sub : forall I l p,
           occDeps (occSubInst I (par l) p) l p = occDeps I l p.
       Proof.
-        intros I l p; unfold occDeps;
-          cbn [occSubInst inst_repo inst_deps inst_peers].
-        rewrite !atoms_fibre; f_equal.
+        intros I l p; unfold occDeps; rewrite edgeAtoms_sub; f_equal.
+        cbn [occSubInst inst_repo].
         destruct l as [| a [| b l]]; cbn [par treeAtom]; try reflexivity.
         rewrite versions_fibre; reflexivity.
       Qed.
@@ -1078,20 +1164,16 @@ Module Placement (N V : UsualOrderedType).
       Proof.
         intros I depth l p n ws Hlen Hk Hh.
         destruct (locPath_par I depth l Hlen Hk) as [Htlen Htk].
-        unfold occDeps in Hh; rewrite !T.DependeesSet.union_spec in Hh.
-        destruct Hh as [Hh | [Hh | Hh]].
+        unfold occDeps in Hh; rewrite T.DependeesSet.union_spec in Hh.
+        destruct Hh as [Hh | Hh].
         - destruct l as [| a [| b l]]; cbn [par treeAtom length] in *;
             try destruct (T.DependeesSet.empty_spec Hh).
           apply T.DependeesSet.singleton_spec in Hh; injection Hh as -> _.
           split; [lia | exact Htk].
-        - apply mem_atoms in Hh; destruct Hh as [m [vs [HE E]]].
-          injection E as -> _; split; [exact Hlen |].
-          apply List.Forall_cons;
-            [exact (locNames_deps I p m vs (or_introl HE)) | exact Hk].
-        - apply mem_atoms in Hh; destruct Hh as [m [vs [HE E]]].
+        - apply mem_edgeAtoms in Hh; destruct Hh as [pe [o [m [vs [HE E]]]]].
           injection E as -> _; split; [exact Hlen |].
           apply List.Forall_cons;
-            [exact (locNames_deps I p m vs (or_intror HE)) | exact Hk].
+            [exact (locNames_deps I pe o p m vs HE) | exact Hk].
       Qed.
 
       Lemma reached_inRange : forall I depth n, Reached I depth n -> InRange I depth n.
diff --git a/theories/Smoke.v b/theories/Smoke.v
index 169b87a..c6f70e7 100644
--- a/theories/Smoke.v
+++ b/theories/Smoke.v
@@ -2,7 +2,7 @@ From Stdlib Require Import MSets List.
 From PackageCalculus Require Import Prelude Core Complexity Versions Semver
   Conflict ConflictClass Concurrent PeerDependency Visibility Feature
   Virtual PackageFormula VariableFormula FeatureConcurrent Debian DebianMA
-  Opam Cargo Alpine Npm Placement.
+  Opam Cargo Alpine Npm Placement NpmPlacement.
 
 Module C := Core Nat_as_OT Nat_as_OT.
 Module Cx := Complexity Nat_as_OT Nat_as_OT Nat_as_OT.
@@ -682,3 +682,27 @@ Example npm_prerelease_admitted :
     (NpmP.rangeEval ((NpmP.COp OpGe 5 :: NpmP.COp OpLt 8 :: nil) :: nil)
        (NpmP.realVersions npmPreRepo npmC)) = 5 :: 6 :: nil.
 Proof. reflexivity. Qed.
+
+Module NplS := NpmPlacement Nat_as_OT Nat_as_OT NpmVM.
+
+(* The project depends on key 4 aliasing package 2 and on 3 optionally;
+   no version of 3 is in range, so that edge may find nothing. *)
+Definition nplInst : NplS.Inst :=
+  NplS.MkInst
+    (fold_right NplS.RepoSet.add NplS.RepoSet.empty
+       ((npmB, 1) :: (npmC, 1) :: nil))
+    (((npmA, 1), NplS.MkDep npmX npmB ((NplS.COp OpEq 1 :: nil) :: nil) false false)
+     :: ((npmA, 1), NplS.MkDep npmC npmC ((NplS.COp OpEq 2 :: nil) :: nil) false true)
+     :: nil)
+    nil nil (npmA, 1).
+
+Example npl_edges :
+  List.map (fun e => (NplS.e_dir e, NplS.e_name e, NplS.e_opt e))
+    (NplS.edgesOf nplInst NplS.Occ.Top) =
+  (npmX, npmB, false) :: (npmC, npmC, true) :: nil.
+Proof. reflexivity. Qed.
+
+Example npl_key :
+  NplS.Pl.VSet.elements (NplS.Pl.repoVersions (NplS.placeRepo nplInst) npmX) =
+  NplS.Occ.Reg npmB 1 :: nil.
+Proof. reflexivity. Qed.
-- 
knotmirror 0.0.1