Adding sharing validator tool

.github/scripts/fuzz_ab.py

@@ -9,7 +9,7 @@
 diverging inputs with distinct first-differing operations, the input is
 shrunk with lean/shrink.py and a standalone Rust reproducer is emitted with
 `pathmap_trace --repro` into the summary and $FUZZ_OUT/repro/.  The harness
-(differential/) and the model (lean/) are taken from HEAD for both sides, so
+(validation/) and the model (lean/) are taken from HEAD for both sides, so
 the only thing that differs is the crate under test in src/.  If BASE cannot
 be built with HEAD's harness, BASE's own harness is tried; if that fails too
 there is no baseline, which is reported loudly and does not fail the job.
@@ -95,16 +95,16 @@ def build_side(self, side, src):
 
     def prepare_base(self):
         """Build base with head's harness and model; fall back to base's own.  Returns the baseline kind."""
-        log(f"== building base ({self.short(self.base_sha)}) with head's differential/ and lean/")
-        for d in ('differential', 'lean'):
+        log(f"== building base ({self.short(self.base_sha)}) with head's validation/ and lean/")
+        for d in ('validation', 'lean'):
             shutil.rmtree(self.base_src / d)
             shutil.copytree(self.repo / d, self.base_src / d, symlinks=True,
                             ignore=shutil.ignore_patterns('.lake'))
         if self.build_side('base', self.base_src):
             return 'head-harness'
         log("== head's harness does not build against base; trying base's own")
-        git('checkout', '--', 'differential', 'lean', cwd=self.base_src)
-        git('clean', '-fdq', '--', 'differential', 'lean', cwd=self.base_src)
+        git('checkout', '--', 'validation', 'lean', cwd=self.base_src)
+        git('clean', '-fdq', '--', 'validation', 'lean', cwd=self.base_src)
         return 'base-harness' if self.build_side('base', self.base_src) else 'none'
 
     def run_side(self, side, src, label, n, flags):

.gitignore

@@ -1,4 +1,4 @@
-/target
+target/
 .DS_Store
 Cargo.lock
 .tmp/

Cargo.toml

@@ -9,7 +9,7 @@ repository = "https://github.com/adam-Vandervorst/pathMap/"
 keywords = ["trie", "MORK", "path", "algebra"]
 categories = ["algorithms", "data-structures", "database-implementations"]
 readme = "README.md"
-exclude = ["target/", "benches/", "pathmap-book/", ".*"]
+exclude = ["target/", "benches/", "validation/", "pathmap-book/", ".*"]
 
 [package.metadata.docs.rs]
 rustc-args = ["-C", "target-feature=+aes,+sse2"]
@@ -143,5 +143,5 @@ harness = false
 required-features = ["arena_compact", "serialization"]
 
 [workspace]
-members = ["pathmap-derive", "examples/sampling", "examples/arena_compact_tests", "differential"]
+members = ["pathmap-derive", "examples/sampling", "examples/arena_compact_tests", "validation/differential", "validation/algebra_sharing"]
 resolver = "2"

lean/FINDINGS.md

@@ -343,7 +343,7 @@ wz.remove_unmasked_branches(ByteMask::EMPTY, false);
 
 The same model, the same operation table, the same trace format -- with an
 `ArenaCompactTree` as the read source instead of a `PathMap`
-(`differential.py --act`, `differential/src/bin/act_trace.rs`).  ACT is a second
+(`differential.py --act`, `validation/differential/src/bin/act_trace.rs`).  ACT is a second
 implementation of the same read specification, so the model holds it to exactly
 the same standard.
 

lean/Main.lean

@@ -9,15 +9,15 @@ One-shot:
     pathmap-oracle                    -- read the bytes from stdin
     pathmap-oracle --act <input-file> -- ArenaCompactTree mode: skip the
                                       -- operations an ACT read source cannot
-                                      -- serve, matching differential/src/bin/act_trace.rs
+                                      -- serve, matching validation/differential/src/bin/act_trace.rs
 
 Resident:
 
     pathmap-oracle --server [--act]   -- one process, many inputs
 
 Spawning a fresh process per fuzzer input costs more than running the input
 does, so `differential.py` keeps the oracle resident and feeds it work over
-stdin.  The protocol matches `differential/src/server.rs`, one command per line:
+stdin.  The protocol matches `validation/differential/src/server.rs`, one command per line:
 
     run-input <timeout-ms> <hex>    run the decoded bytes, print the trace
     quit                            exit 0
@@ -29,17 +29,17 @@ only line beginning with `!`:
     !TIMEOUT                        exceeded <timeout-ms>
     !PANIC <one-line message>       malformed command
 
-Prints the trace produced by the model.  `differential/src/bin/pathmap_trace.rs` prints the
+Prints the trace produced by the model.  `validation/differential/src/bin/pathmap_trace.rs` prints the
 same trace from the real crate for the same input bytes, and
-`differential/src/bin/act_trace.rs` does the same with an `ArenaCompactTree` as the read
+`validation/differential/src/bin/act_trace.rs` does the same with an `ArenaCompactTree` as the read
 source; they are compared by `lean/differential.py`.
 -/
 
 open PathMapModel
 
 /-! ## Why there is no in-process timeout here
 
-`differential/src/server.rs` runs each input on a thread it can abandon, so a
+`validation/differential/src/server.rs` runs each input on a thread it can abandon, so a
 hanging crate costs one input rather than the process.  The oracle does not, and
 not for want of trying: `IO.asTask` plus `IO.sleep` under `IO.waitAny` blocks on
 the work task in list order and never observes the timer, and polling with

lean/PathMapModel/Fuzz.lean

@@ -5,7 +5,7 @@ import PathMapModel.Spec
 
 This module turns the model into an **oracle**: it decodes a raw fuzzer input
 into a program over two maps and two zippers, runs it, and emits a trace.  The
-Rust side (`differential/src/bin/pathmap_trace.rs`) decodes the *same bytes* with the *same*
+Rust side (`validation/differential/src/bin/pathmap_trace.rs`) decodes the *same bytes* with the *same*
 rules and emits the *same* trace format from the real crate, so any behavioural
 divergence shows up as a textual diff.
 
@@ -54,7 +54,7 @@ def ops : ValOps V := u64Ops
 
 Why an operation was skipped.  Every `skip` in the trace carries one of these,
 so a skipped op says which rule declined it rather than just that something
-declined it.  `differential/src/harness.rs` emits the same tokens; the two must
+declined it.  `validation/differential/src/harness.rs` emits the same tokens; the two must
 agree exactly or every input with a skip diverges.
 
 * `skip:act` — the ACT read source cannot be a merge source
@@ -221,7 +221,7 @@ def noPrune : Bool := false
 a following `u8 % 2` byte (`0` = write zipper, `1` = read zipper); ops `27`–`46`
 are write-zipper operations. -/
 
-/-- Number of distinct operations.  Must match `NOPS` in `differential/src/harness.rs`. -/
+/-- Number of distinct operations.  Must match `NOPS` in `validation/differential/src/harness.rs`. -/
 def nops : Nat := 56
 
 /-- A full `k`-path iteration: `descend_first_k_path` followed by

lean/README.md

@@ -9,7 +9,7 @@ Two things live here:
 1. **The model** (`PathMapModel/`) — a total, executable definition of what each
    API function *means*, with the laws relating them.
 2. **The harness** (`Main.lean`, `differential.py`, `shrink.py`, and the
-   `../differential` crate) — the machinery that runs the same generated
+   `../validation/differential` crate) — the machinery that runs the same generated
    program against the model and against `pathmap`, and diffs the results.
 
 Everything the fuzzing found is written up in [FINDINGS.md](FINDINGS.md), with
@@ -206,7 +206,7 @@ count); the run ends with a full dump of both maps.  Any behavioural difference
 is a textual diff.
 
 The op table lives in `Fuzz.lean` (`PathMapModel.Fuzz.step`) and
-`differential/src/harness.rs`; **the two must be changed together.**
+`validation/differential/src/harness.rs`; **the two must be changed together.**
 
 ### Front ends
 
@@ -228,7 +228,7 @@ The op table lives in `Fuzz.lean` (`PathMapModel.Fuzz.step`) and
 Each front end is spawned once with `--server` and stays up, taking inputs as
 hex on stdin — `run-input <timeout-ms> <hex>`, replying with the trace and one
 `!DONE` / `!TIMEOUT` / `!PANIC <msg>` terminator.  The protocol lives in
-`differential/src/server.rs`, shared by both crate front ends (it is plumbing;
+`validation/differential/src/server.rs`, shared by both crate front ends (it is plumbing;
 it knows nothing about tries).
 
 This replaced a temp file plus two fresh processes per input.  Process creation
@@ -305,7 +305,7 @@ cargo run --release -p differential --bin pathmap_trace -- --repro --upto 15 FIL
 
 `--upto N` stops after N operations, so a trace line `14 to_next_val ...` is
 reproduced by `--upto 15`.  Shrink first (`shrink.py`) and the result is usually
-a handful of calls, ready to paste into `differential/src/bin/zipper_bug_repros.rs`.
+a handful of calls, ready to paste into `validation/differential/src/bin/zipper_bug_repros.rs`.
 
 The generator decodes the same bytes in the same order as the op table,
 including the operands consumed only to keep the stream aligned, so it is worth
@@ -323,7 +323,7 @@ commented at its site.
 
 A skip is named in the trace — `ret=skip:<reason>`, never a bare `skip` — so a
 skipped op says which rule declined it.  The vocabulary is defined once on each
-side (`SKIP_*` in `differential/src/harness.rs`, `skip*` in
+side (`SKIP_*` in `validation/differential/src/harness.rs`, `skip*` in
 `PathMapModel/Fuzz.lean`) and the two must agree exactly, or every input that
 skips diverges:
 
@@ -529,7 +529,7 @@ cargo build --release -p differential
 ./lean/differential.py --act --random 500 --seed 99 --max-fails 0
 ```
 
-`differential/src/bin/act_trace.rs` builds an ACT from map1 with `from_zipper` and runs the
+`validation/differential/src/bin/act_trace.rs` builds an ACT from map1 with `from_zipper` and runs the
 identical operation table against an `ACTZipper`.  There is still exactly one
 op table: the merge operations sit behind a `ReadSource` trait, whose ACT
 implementation declines them, so the two front ends cannot drift apart.  The
@@ -553,7 +553,7 @@ programs), `descend_first_k_path()` only walks the leftmost chain, and
 `descend_last_path()` can run one byte past the end of the trie.  `from_zipper`
 round-trips faithfully, and `merge_zipper_into_file` -- ACT's one write-shaped
 operation -- matches its specification on all 300 cases of
-`differential/src/bin/act_merge_check.rs`.
+`validation/differential/src/bin/act_merge_check.rs`.
 
 ## Sharing
 

lean/differential.py

@@ -10,7 +10,7 @@
     target/*/act_trace                     ACT read source (--act)
 
 Each child is spawned once with `--server` and stays resident, taking inputs as
-`run-input <timeout-ms> <hex>` on stdin; see `differential/src/server.rs` for the
+`run-input <timeout-ms> <hex>` on stdin; see `validation/differential/src/server.rs` for the
 protocol.  That replaced a temp file and two fresh processes per input, which
 cost about 5x the runtime and left `/tmp/pathmap-diff-*` behind forever.  Only a
 *failing* input is written to disk now, so it can still be replayed and shrunk.
@@ -64,7 +64,7 @@ class Child:
     Spawning a process per input dominated the old runtime — 200 inputs spent
     more time in `sys` (fork/exec) than in `user` — so each front end now stays
     up and takes work as `run-input <timeout-ms> <hex>`, replying with the trace
-    and one `!`-prefixed terminator.  See `differential/src/server.rs`.
+    and one `!`-prefixed terminator.  See `validation/differential/src/server.rs`.
 
     Two failure modes have to be survivable, because a wedged or dead child must
     not take the run with it:

validation/README.md

@@ -0,0 +1,49 @@
+# Developer validation
+
+This directory contains workspace packages used to validate `pathmap` during
+development. The larger effort is the **Lean differential validator**: an
+executable model of trie and zipper behavior in [`lean/`](../lean/README.md),
+paired with the Rust `differential` package here. The smaller
+`algebra-sharing-validation` package explores sharing across algebraic
+operations.
+
+## Lean differential validator
+
+The Lean model specifies zipper operations independently of the Rust
+implementation. A generated byte string becomes the same program on both
+sides. The harness compares return values and state after each operation, then
+the full maps. This gives each generated sequence a semantic oracle, including
+cases where several operations interact. The model also contains laws and
+regression fixtures checked when Lean builds.
+
+[`differential/`](differential/) supplies the Rust trace binaries, input decoder,
+and standalone reproducers. The driver, model, corpus, shrinking tool, and the
+record of findings live in [`lean/`](../lean/README.md). To run a sample from
+the repository root after installing Lean as described there:
+
+```sh
+(cd lean && lake build)
+cargo build --release -p differential
+./lean/differential.py --random 500 --seed 1
+```
+
+Use `./lean/differential.py --act --random 500` to compare the model with the
+`ArenaCompactTree` read source. Failures can be minimized with
+`./lean/shrink.py path/to/input.bin`; the investigated divergences and
+reproducers are catalogued in [`lean/FINDINGS.md`](../lean/FINDINGS.md).
+[`lean/README.md`](../lean/README.md) describes the model, supported operations,
+corpus, and full workflow.
+
+## Algebraic sharing validator
+
+[`algebra_sharing/`](algebra_sharing/) generates related tries and sequences of
+algebraic operations. It checks logical results and identifies steps that lose
+ordinary sharing or miss an opportunity for result sharing. Run
+`cargo run -p algebra-sharing-validation` from the repository root. Ordinary
+and result-sharing losses are counted in the default **report** mode, which
+checks every selected seed and prints aggregate counts. It shows only the first
+four split examples of each kind, clearly labeled in the output. Set
+`PATHMAP_SHARING_ENFORCE_ORDINARY=1` for **strict** mode, which stops at the
+first ordinary-sharing loss and saves a minimized replay. The
+[`source documentation`](algebra_sharing/src/main.rs) explains its model,
+parameters, and replay commands.

validation/algebra_sharing/Cargo.toml

@@ -0,0 +1,9 @@
+[package]
+name = "algebra-sharing-validation"
+version = "0.1.0"
+edition = "2024"
+publish = false
+description = "Developer validation of sharing across pathmap algebraic operations"
+
+[dependencies]
+pathmap = { path = "../.." }