Refine meet model

[imlvts]

There was an issue with meet: meet with self-node is a noop, but meet with equal node drops dangling paths.
This refines the meet spec to preserve dangling paths if they're both present.

[adamv-symbolica]

What's the impact for performance here (both constant, and asymptotic)? The right call may be to change the spec to care less about dangling paths.

[imlvts]

The current implementation of meet can have different results between map.meet(&map) and map.meet(&equal_map)). This is logically inconsistent.
The spec is blind with respect to sharing. It cannot express that at all. The only thing I can do is not to check meet this way.
The best we can do now is to leave this as a suggestion and disable meet checks in the differential fuzzer.

[imlvts]

//! `meet` of a map with itself keeps a dangling path; `meet` with an equal map
//! built separately drops it.
use pathmap::PathMap;
use pathmap::zipper::*;

fn locations(m: &PathMap<u64>) -> Vec<(Vec<u8>, Option<u64>)> {
    let mut rz = m.read_zipper();
    let mut out = vec![];
    while rz.to_next_step() {
        if rz.val().is_some() || rz.child_count() == 0 { out.push((rz.path().to_vec(), rz.val().cloned())); }
    }
    out
}

fn build() -> PathMap<u64> {
    let mut map = PathMap::new();
    map.set_val_at([1], 1);
    map.create_path([0, 2, 1]);
    map.set_val_at([1, 2, 2], 1);
    map.write_zipper_at_path(&[0, 2, 1]).remove_branches(true);
    map
}

fn main() {
    let map = build();
    let same = build();
    println!("map                 {:?}", locations(&map));
    println!("map.meet(&map)      {:?}", locations(&map.meet(&map)));
    println!("map.meet(&clone)    {:?}", locations(&map.meet(&map.clone())));
    println!("map.meet(&same)     {:?}", locations(&map.meet(&same)));
    println!("map == same paths:  {}", locations(&map) == locations(&same));
    assert_eq!(locations(&map.meet(&map)), locations(&map.meet(&same)), "meet depends on node identity");
}

[Adam-Vandervorst]

"the same" is load bearing here; "equivalent up to" with "dangling paths" and "sharing" and...

[luketpeterson]

Yikes... It took me more than 2 weeks to write the generic meet function back in early 2025. It was one of the trickiest parts of the whole crate - and the crate has a lot of tricky parts.

I know Fable can probably do better than the un-assisted me of 18 months ago. Especially with the fuzzer to help. But hopefully we can get some more extensive benchmarks and test coverage on how well we preserve sharing too so we make sure not to lose any perf...

Anyway, I don't want to rubber stamp this PR because it's huge and hits the heart of tricky stuff. But I don't have time to spend really understanding this week.

[luketpeterson]

load bearing

As recently as 2025 I thought "load bearing" was clever engineer-architect-speak. Now it's a calling card of slop.

[adamv-symbolica]

I believe the algebraic ops have more interesting structure to them with respect to dangling paths, depending on if you treat them as an optimization or representation feature.

a.join(b) would be the easiest case:
This could return paths pathset(a.iter()).union(pathset(b.iter())), dangling paths subsumption(steps(a)).union(subsumption(steps(b))).subtract(paths), and assert all(a.join(b).node_at(a) == a.node_at(path) or b.contains(path) for path in a) and all(a.join(b).node_at(b) == b.node_at(path) or a.contains(path) for path in b).
Another sensible implementation would instead prune dandling paths while traversing the join (unless we can just accept subtries), that is dangling paths subsumption(steps(a)).sym_diff(subsumption(steps(b))).subtract(paths)

For e.g. a.meet(b)
This ofc returns paths pathset(a.iter()).meet(pathset(b.iter())),
but for dangling paths

1. subsumption(steps(a)).union(subsumption(steps(b))).subtract(paths) would be a "don't drop (i.e. recurse into) any dangling path subtries"
2. subsumption(steps(a)).meet(subsumption(steps(b))).subtract(paths) would be a "calculate the dangling paths in the intersection, and drop a \ b and b \ a"
3. subsumption(steps(a).subtract(steps(b.restrict(a)))).subtract(paths) would be a "keep the dangling paths originating from nodes in a"

They uphold three different guarantees:

1. No dangling paths are cleaned up implicitly
2. Logically dangling paths are paths
3. No compute is wasted on dangling paths

And have three different asymptotics:

1. Worst case additional cost (compared to pruned versions) is time+space |subsumption(steps(a))| + |subsumption(steps(b))| but crucially this can happen even in the case where the pruned version is just wlog |subsumption(steps(a))|
2. Worst case additional cost is time |subsumption(steps(a))| + |subsumption(steps(b))| and space |subsumption(steps(a))|.min(|subsumption(steps(b))|)
3. Worst case additional cost is time is none and space is |subsumption(steps(a).subtract(b.restrict(pathset(a))))|