Refine meet model

differential/src/harness.rs

@@ -747,7 +747,8 @@ pub fn run_ops<R: ReadSource>(
                     ("join_map_into", s)
                 }
                 38 => {
-                    let _pr = get!(d.boolean()); // decoded for stream alignment; see `no_prune`
+                    // `prune = true` is best-effort, so only `prune = false` is compared
+                    let _pr = get!(d.boolean());
                     ("meet_into", show_status_opt((*rz).do_meet_into(&mut wz, no_prune)))
                 }
                 39 => {
@@ -823,7 +824,7 @@ pub fn run_ops<R: ReadSource>(
                 }
                 46 => {
                     let k = get!(d.modn(4));
-                    let _pr = get!(d.boolean()); // decoded for stream alignment; see `no_prune`
+                    let _pr = get!(d.boolean()); // decoded for stream alignment; see op 38
                     // `meet_k_path_into` spins forever when the focus has no
                     // children, and escapes the focus subtree when k == 0.
                     // See `Zip.meetKPathUnspecified`.

lean/PathMapModel/Check.lean

@@ -147,6 +147,9 @@ def dropT1Result : T := ((zipAt dropT1 [0x31,0x32,0x33,0x3a] []).joinKPathInto o
 #guard fixtures.all (joinIdem ops)
 #guard fixtures.all (fun a => fixtures.all (fun b => fixtures.all (joinAssoc ops a b)))
 #guard fixtures.all (meetIdemOnVals ops)
+#guard fixtures.all (meetIdem ops)
+#guard fixtures.all (meetPrunedIdem ops)
+#guard fixtures.all (fun a => fixtures.all (meetCommOnPaths ops a))
 #guard fixtures.all (subSelfEmptyVals ops)
 #guard fixtures.all (restrictSelf ops)
 

lean/PathMapModel/Fuzz.lean

@@ -407,6 +407,7 @@ def step (s : St) (d : Dec) : Option (St × Dec) := do
   | 38 => do let (_pr, d) ← d.bool
              if s.act then some (emit s "meet_into" skipAct, d)
              else
+               -- `prune = true` is best-effort, so only `prune = false` is compared
                let (st, z) := s.wz.meetInto ops s.rz noPrune
                some (emit { s with wz := z } "meet_into" (toString st), d)
   | 39 => do let (_pr, d) ← d.bool

lean/PathMapModel/PathMap.lean

@@ -338,11 +338,19 @@ def join (a b : PathMap V) : PathMap V :=
   mk' (keys.filterMap fun k => (joinVal ops (a.valAt k) (b.valAt k)).map (k, ·))
       (a.paths ++ b.paths)
 
-/-- Meet (intersection).  A location survives only if it lies on the way to a
-surviving value, so dangling paths never survive a meet. -/
+/-- Meet (`prune = false`): a location survives iff both sides have it, a value iff
+both hold one. -/
 def meet (a b : PathMap V) : PathMap V :=
   let keys := Path.sortDedup (a.vals.map (·.1))
-  mk' (keys.filterMap fun k => (meetVal ops (a.valAt k) (b.valAt k)).map (k, ·)) []
+  mk' (keys.filterMap fun k => (meetVal ops (a.valAt k) (b.valAt k)).map (k, ·))
+      (a.paths.filter b.pathExists)
+
+/-- `t` without its dangling paths. -/
+def dropDangling (t : PathMap V) : PathMap V := mk' t.vals []
+
+/-- Meet with `prune = true`, fully pruned.  `pathmap` may skip shared nodes, so its
+result lies between this and `meet`; not compared by the fuzzer. -/
+def meetPruned (a b : PathMap V) : PathMap V := (meet ops a b).dropDangling
 
 /-- Subtract.
 

lean/PathMapModel/Spec.lean

@@ -314,11 +314,22 @@ def joinIdem (ops : ValOps V) (a : PathMap V) : Bool :=
 def joinAssoc (ops : ValOps V) (a b c : PathMap V) : Bool :=
   PathMap.beqT ops (PathMap.join ops (PathMap.join ops a b) c) (PathMap.join ops a (PathMap.join ops b c))
 
-/-- `meet` is idempotent *on values*.  It is not idempotent on locations: a meet
-discards dangling paths, so `meet a a` keeps only the value-bearing skeleton. -/
+/-- `meet` is idempotent *on values*. -/
 def meetIdemOnVals (ops : ValOps V) (a : PathMap V) : Bool :=
   (PathMap.meet ops a a).vals.map (·.1) == a.vals.map (·.1)
 
+/-- `meet` is idempotent, dangling paths included. -/
+def meetIdem (ops : ValOps V) (a : PathMap V) : Bool :=
+  PathMap.beqT ops (PathMap.meet ops a a) a
+
+/-- `meetPruned a a` is `a` with its dangling paths dropped. -/
+def meetPrunedIdem (ops : ValOps V) (a : PathMap V) : Bool :=
+  PathMap.beqT ops (PathMap.meetPruned ops a a) a.dropDangling
+
+/-- `meet` is commutative on locations. -/
+def meetCommOnPaths (ops : ValOps V) (a b : PathMap V) : Bool :=
+  (PathMap.meet ops a b).paths == (PathMap.meet ops b a).paths
+
 /-- Subtracting a map from itself leaves no values. -/
 def subSelfEmptyVals (ops : ValOps V) (a : PathMap V) : Bool :=
   (PathMap.sub ops a a).vals.isEmpty

lean/PathMapModel/Write.lean

@@ -328,9 +328,8 @@ def joinIntoTake (src : Zip V) (prune : Bool) : AlgStatus × Zip V × Zip V :=
 
 /-- `ZipperWriting::meet_into`: intersect the focus's subtrie with the source's.
 
-The value step runs first and can prune the focus out from under the node step.
-A meet drops every dangling path, since a location only survives if it leads to
-a surviving value. -/
+Below the focus the result is `PathMap.meet`, or `PathMap.meetPruned` with `prune`
+(best-effort in `pathmap`, not compared).  The focus is never removed. -/
 def meetInto (src : Zip V) (prune : Bool) : AlgStatus × Zip V :=
   let (valStatus, valWasNone, z1) :=
     match z.val, src.val with
@@ -339,26 +338,20 @@ def meetInto (src : Zip V) (prune : Bool) : AlgStatus × Zip V :=
         (AlgStatus.ofValRes r, false,
           match r.resolve sv ov with
           | some v => (z.setVal v).2
-          | none => (z.removeVal prune).2)
+          | none => (z.removeVal false).2)
     | none, some _ => (AlgStatus.none, true, z)
-    | some _, none => (AlgStatus.none, false, (z.removeVal prune).2)
+    | some _, none => (AlgStatus.none, false, (z.removeVal false).2)
     | none, none => (AlgStatus.none, true, z)
   let selfB := z1.focusNode
   let srcB := src.focusNode
   if selfB.isEmptyMap then
     (AlgStatus.merge .none valStatus true valWasNone, z1)
   else if srcB.isEmptyMap then
-    let z2 := z1.withTrie (z1.trie.removeBelow z1.focus)
-    let z3 := if prune then (z2.prunePath).2 else z2
-    (AlgStatus.merge .none valStatus false valWasNone, z3)
+    (AlgStatus.merge .none valStatus false valWasNone, z1.withTrie (z1.trie.removeBelow z1.focus))
   else
-    let r := PathMap.meet ops selfB srcB
+    let r := if prune then PathMap.meetPruned ops selfB srcB else PathMap.meet ops selfB srcB
     let st := nodeStatus ops selfB r
-    let z2 :=
-      if st == .identity then z1
-      else
-        let zg := z1.withTrie (z1.trie.graftBelow z1.focus r)
-        if st == .none && prune then (zg.prunePath).2 else zg
+    let z2 := if st == .identity then z1 else z1.withTrie (z1.trie.graftBelow z1.focus r)
     (AlgStatus.merge st valStatus false valWasNone, z2)
 
 /-- `ZipperWriting::subtract_into`: remove the source's subtrie from the focus's.
@@ -396,7 +389,7 @@ def subtractInto (src : Zip V) (prune : Bool) : AlgStatus × Zip V :=
     (AlgStatus.merge st valStatus false valWasNone, z2)
 
 /-- `ZipperWriting::meet_2`: meet two *source* subtries and write the result at
-the focus.
+the focus, as `PathMap.meet`.
 
 Two things separate this from `meet_into`.  It does not consult what is already
 at the focus, so — as the implementation notes — it never reports `Identity`,
@@ -486,9 +479,10 @@ def meetKPathInto (k : Nat) (prune : Bool) : Bool × Zip V :=
       match acc with
       | none => some m
       | some a => some (PathMap.meet ops a m)) none
-  match result with
-  | some m => if m.isEmptyMap then (false, (z.removeBranches prune).2) else (true, z.graftMap m)
-  | none => (false, (z.removeBranches prune).2)
+  -- `prune` drops dangling paths below the focus
+  match result.map fun m => if prune then m.dropDangling else m with
+  | some m => if m.isEmptyMap then (false, (z.removeBranches false).2) else (true, z.graftMap m)
+  | none => (false, (z.removeBranches false).2)
 
 end Zip
 end PathMapModel