luketpeterson · Oct 9, 2026
diff --git a/differential/src/act.rs b/differential/src/act.rs
@@ -37,7 +37,7 @@ impl<'t, S: AsRef<[u8]>> ReadSource for ACTZipper<'t, S, u64> {
 /// Decode and execute a fuzzer input with an ACT built from map1 as the read
 /// source.  See `bin/act_trace.rs` for what this does and does not exercise.
 pub fn run_act(bytes: &[u8], check: bool) -> String {
-    let mut d = Dec { bytes, pos: 0 };
+    let Some(mut d) = Dec::new(bytes) else { return "EMPTY\n".to_string(); };
     let (mut map0, map1, root0, root1) = match decode_header(&mut d) {
         Some(x) => x,
         None => return "EMPTY\n".to_string(),

diff --git a/differential/src/bin/act_trace.rs b/differential/src/bin/act_trace.rs
@@ -27,6 +27,10 @@ use differential::*;
 
 fn main() {
     let args: Vec<String> = std::env::args().skip(1).collect();
+    if args.iter().any(|a| a == "--input-header") {
+        println!("{}", hex_path(&input_header()));
+        return;
+    }
     let check = args.iter().any(|a| a == "--check");
     // Resident mode: one process, many inputs over stdin.  See `serve`.
     if args.iter().any(|a| a == "--server") {

diff --git a/differential/src/bin/pathmap_trace.rs b/differential/src/bin/pathmap_trace.rs
@@ -10,6 +10,10 @@ use differential::*;
 fn main() {
     // `--check` also asserts the structural invariants after every operation.
     let args: Vec<String> = std::env::args().skip(1).collect();
+    if args.iter().any(|a| a == "--input-header") {
+        println!("{}", hex_path(&input_header()));
+        return;
+    }
     let check = args.iter().any(|a| a == "--check");
     // Resident mode: one process, many inputs over stdin.  See `serve`.
     if args.iter().any(|a| a == "--server") {

diff --git a/differential/src/harness.rs b/differential/src/harness.rs
@@ -24,8 +24,20 @@ use pathmap::zipper::*;
 // `str::lines()` recovers them then.
 use core::fmt::Write as _;
 
-/// Number of distinct operations. Must match `PathMapModel.Fuzz.nops`.
-pub const NOPS: usize = 56;
+/// Selector count for newly generated inputs. Keep operation IDs permanently assigned.
+pub const NOPS: usize = 57;
+/// Unversioned inputs retain their original operation decoding.
+pub const LEGACY_NOPS: usize = 56;
+/// Input header marker, followed by a little-endian u16 selector count (1..=256).
+pub const WIRE_MAGIC: &[u8] = b"PMFUZZ\x01\x00";
+
+/// Header for new inputs. Decoding always uses the recorded count, never `NOPS`.
+pub fn input_header() -> Vec<u8> {
+    assert!((1..=256).contains(&NOPS));
+    let mut header = WIRE_MAGIC.to_vec();
+    header.extend_from_slice(&(NOPS as u16).to_le_bytes());
+    header
+}
 /// Maximum operations executed. Must match the `maxSteps` default in `Fuzz.run`.
 pub const MAX_STEPS: usize = 256;
 /// Maximum entries in a `dump`. Must match `Fuzz.dumpAt`.
@@ -34,9 +46,24 @@ pub const DUMP_CAP: usize = 64;
 pub struct Dec<'a> {
     pub bytes: &'a [u8],
     pub pos: usize,
+    op_count: usize,
 }
 
 impl<'a> Dec<'a> {
+    pub fn new(bytes: &'a [u8]) -> Option<Self> {
+        let (pos, op_count) = if bytes.starts_with(WIRE_MAGIC) {
+            let count_bytes = bytes.get(WIRE_MAGIC.len()..WIRE_MAGIC.len() + 2)?;
+            let count = u16::from_le_bytes([count_bytes[0], count_bytes[1]]) as usize;
+            if !(1..=256).contains(&count) { return None; }
+            (WIRE_MAGIC.len() + 2, count)
+        } else {
+            (0, LEGACY_NOPS)
+        };
+        Some(Self { bytes, pos, op_count })
+    }
+    pub fn op(&mut self) -> Option<usize> {
+        self.modn(self.op_count)
+    }
     pub fn u8(&mut self) -> Option<u8> {
         let b = *self.bytes.get(self.pos)?;
         self.pos += 1;
@@ -427,7 +454,7 @@ pub fn decode_header(d: &mut Dec) -> Option<(PathMap<u64>, PathMap<u64>, Vec<u8>
 /// Decode and execute a fuzzer input against a `PathMap` read source.
 ///
 pub fn run(bytes: &[u8], check: bool) -> String {
-    let mut d = Dec { bytes, pos: 0 };
+    let Some(mut d) = Dec::new(bytes) else { return "EMPTY\n".to_string(); };
     let (mut map0, map1, root0, root1) = match decode_header(&mut d) {
         Some(x) => x,
         None => return "EMPTY\n".to_string(),
@@ -478,7 +505,7 @@ pub fn run_ops<R: ReadSource>(
             if step >= MAX_STEPS {
                 break;
             }
-            let op = get!(d.u8()) as usize % NOPS;
+            let op = get!(d.op());
             let (name, ret): (&str, String) = match op {
                 0 => {
                     let t = get!(d.modn(2));
@@ -903,6 +930,10 @@ pub fn run_ops<R: ReadSource>(
                     let p = get!(d.path(6));
                     ("meet_2", show_status_opt((*rz).do_meet_2(&mut wz, &p)))
                 }
+                56 => {
+                    let pr = get!(d.boolean());
+                    ("remove_subtrie", show_bool(wz.remove_subtrie(pr)).to_string())
+                }
                 47 => {
                     let t = get!(d.modn(2));
                     // The blind-zipper addition: `descend_until` reporting the
@@ -932,3 +963,89 @@ pub fn run_ops<R: ReadSource>(
     }
 
 }
+
+#[cfg(test)]
+mod input_format_tests {
+    use super::*;
+    use crate::{emit_repro, run_act};
+
+    #[test]
+    fn unversioned_inputs_keep_legacy_operation_decoding() {
+        let bytes: Vec<u8> = (0..=255).collect();
+        let mut d = Dec::new(&bytes).unwrap();
+        for byte in 0..=255 {
+            assert_eq!(d.op(), Some(byte % 56));
+        }
+    }
+
+    #[test]
+    fn input_header_count_controls_decoding_independently_of_current_operation_count() {
+        for count in [1u16, 32, 56, 57, 58, 256] {
+            let mut bytes = WIRE_MAGIC.to_vec();
+            bytes.extend_from_slice(&count.to_le_bytes());
+            bytes.extend(0..=255);
+            let mut d = Dec::new(&bytes).unwrap();
+            for byte in 0..=255 {
+                assert_eq!(d.op(), Some(byte % count as usize));
+            }
+        }
+    }
+
+    #[test]
+    fn invalid_or_truncated_input_headers_are_rejected() {
+        let mut bytes = WIRE_MAGIC.to_vec();
+        assert!(Dec::new(&bytes).is_none());
+        bytes.push(57);
+        assert!(Dec::new(&bytes).is_none());
+        for count in [0u16, 257, u16::MAX] {
+            let mut bytes = WIRE_MAGIC.to_vec();
+            bytes.extend_from_slice(&count.to_le_bytes());
+            assert!(Dec::new(&bytes).is_none());
+            assert_eq!(run(&bytes, true), "EMPTY\n");
+            assert_eq!(run_act(&bytes, true), "EMPTY\n");
+        }
+    }
+
+    #[test]
+    fn header_count_56_preserves_legacy_replay_and_reproducer() {
+        for legacy in [
+            include_bytes!("../../lean/corpus/status-imprecise-join_map_into.bin").as_slice(),
+            include_bytes!("../../lean/corpus/status-imprecise-restrict.bin").as_slice(),
+        ] {
+            let mut bytes = WIRE_MAGIC.to_vec();
+            bytes.extend_from_slice(&56u16.to_le_bytes());
+            bytes.extend_from_slice(legacy);
+            assert_eq!(run(&bytes, false), run(legacy, false));
+            assert_eq!(run_act(&bytes, false), run_act(legacy, false));
+            assert_eq!(emit_repro(&bytes, 256), emit_repro(legacy, 256));
+        }
+    }
+
+    #[test]
+    fn trace_and_reproducer_decode_headered_write_operations() {
+        // Clear [0] and its descendant, prune the dangling focus, then write there again.
+        let mut bytes = input_header();
+        bytes.extend_from_slice(&[
+            4, 0, 9, 1, 0, 10, 2, 0, 1, 12, 1, 1, 11, // map0 entries.
+            1, 1, 2, 13, // map1 entry.
+            0, 0, // Zipper roots.
+            0, 0, 1, 0, // Descend to [0].
+            56, 0, 56, 1, 27, 14, // Remove, prune, then reuse.
+        ]);
+        let trace = run(&bytes, true);
+        assert!(
+            trace.contains("1 remove_subtrie ret=1 W=00 o00 e1 v- c0 n0"),
+            "{trace}"
+        );
+        assert!(
+            trace.contains("2 remove_subtrie ret=0 W=00 o00 e0 v- c0 n0"),
+            "{trace}"
+        );
+        assert!(trace.contains("MAP0 _:9,00:14,01:11"), "{trace}");
+        assert!(trace.contains("MAP1 _:-,02:13"), "{trace}");
+        let repro = emit_repro(&bytes, 256);
+        assert!(repro.contains("wz.remove_subtrie(false);"));
+        assert!(repro.contains("wz.remove_subtrie(true);"));
+        assert!(repro.contains("wz.set_val(14);"));
+    }
+}
diff --git a/differential/src/repro.rs b/differential/src/repro.rs
@@ -45,7 +45,9 @@ pub fn rs_mask(p: &[u8]) -> String {
 /// `upto` is the number of operations to emit; the divergent step from a trace
 /// line `N <op> ...` is reproduced by `upto = N + 1`.
 pub fn emit_repro(bytes: &[u8], upto: usize) -> String {
-    let mut d = Dec { bytes, pos: 0 };
+    let Some(mut d) = Dec::new(bytes) else {
+        return "// Invalid fuzzer input header.\nfn main() {}\n".to_string();
+    };
     let mut o = String::new();
     o.push_str(
         "//! Generated by `pathmap_trace --repro`.  Reproduces a fuzzer input as\n\
@@ -113,8 +115,8 @@ pub fn emit_repro(bytes: &[u8], upto: usize) -> String {
     }
     let mut step = 0usize;
     while step < upto {
-        let op = match d.u8() {
-            Some(b) => b as usize % NOPS,
+        let op = match d.op() {
+            Some(op) => op,
             None => break,
         };
         // `z!` picks the zipper the target byte selects, exactly as `tgt!` does.
@@ -213,6 +215,7 @@ pub fn emit_repro(bytes: &[u8], upto: usize) -> String {
             55 => { let p = g!(d.path(6));
                     format!("{{ let mut b = map1.read_zipper_at_path({}); b.descend_to({}); wz.meet_2(&rz, &b); }}",
                             rs_bytes(&r1), rs_bytes(&p)) }
+            56 => { let pr = g!(d.boolean()); format!("wz.remove_subtrie({pr});") }
             _ => "// nop".to_string(),
         };
         o.push_str(&format!("    /* {step:3} */ {line}\n"));

diff --git a/lean/PathMapModel/Check.lean b/lean/PathMapModel/Check.lean
@@ -1,4 +1,5 @@
 import PathMapModel.Spec
+import PathMapModel.Fuzz
 
 /-!
 # Build-time checks
@@ -51,6 +52,20 @@ def probes : List Path := [[], [0], [1], [0,0], [0,1], [1,1], [0,1,2], [3]]
 def allZips : List (Zip UInt64) :=
   fixtures.flatMap (fun t => probes.map (fun p => zipAt t [] p))
 
+/-! The selector count belongs to each input, independent of the current operation table. -/
+
+def inputWithCount (lo hi : UInt8) : ByteArray :=
+  ByteArray.mk (Fuzz.wireMagic ++ [lo, hi]).toArray
+
+#guard ((Fuzz.Dec.init (ByteArray.mk #[])).map (·.opCount)) == some 56
+#guard ((Fuzz.Dec.init (inputWithCount 56 0)).map (·.opCount)) == some 56
+#guard ((Fuzz.Dec.init (inputWithCount 58 0)).map (·.opCount)) == some 58
+#guard ((Fuzz.Dec.init (inputWithCount 0 1)).map (·.opCount)) == some 256
+#guard (Fuzz.Dec.init (inputWithCount 0 0)).isNone
+#guard (Fuzz.Dec.init (inputWithCount 1 1)).isNone
+#guard (Fuzz.Dec.init (ByteArray.mk Fuzz.wireMagic.toArray)).isNone
+#guard (Fuzz.Dec.init (ByteArray.mk (Fuzz.wireMagic ++ [57]).toArray)).isNone
+
 /-! ## Regression fixtures from `src/write_zipper.rs` -/
 
 /-- `write_zipper_prune_path_test2`, first phase: removing the value at
@@ -127,6 +142,39 @@ def dropT1Result : T := ((zipAt dropT1 [0x31,0x32,0x33,0x3a] []).joinKPathInto o
 #guard dropT1Result.valAt [0x31,0x32,0x33,0x3a,0x42,0x6f,0x62,0x3a,0x46,0x69,0x64,0x6f] == some 1
 #guard dropT1Result.valCount [] == 2
 
+/-! ## Subtrie removal -/
+
+/-! `remove_subtrie` clears the focus and descendants, preserves other content,
+and prunes only up to the zipper root. Dangling descendants count as branches;
+pruning an already dangling focus does not count as removing content. -/
+
+#guard ((zipAt fBranch [] [0]).removeSubtrie false).1
+#guard ((zipAt fBranch [] [0]).removeSubtrie false).2.pathExists
+#guard !((zipAt fBranch [] [0]).removeSubtrie false).2.isVal
+#guard ((zipAt fBranch [] [0]).removeSubtrie false).2.childCount == 0
+#guard ((zipAt fBranch [] [0]).removeSubtrie true).2.trie.valAt [] == some 0
+#guard ((zipAt fBranch [] [0]).removeSubtrie true).2.trie.valAt [1] == some 4
+#guard !((zipAt fBranch [] [0]).removeSubtrie true).2.pathExists
+#guard ((zipAt fBranch [] []).removeSubtrie true).2.trie.isEmptyMap
+#guard !(((zipAt fBranch [] []).removeSubtrie true).2.removeSubtrie true).1
+#guard ((zipAt fDangle [] [0,1]).removeSubtrie false).1
+#guard !((zipAt fDangle [] [0,1,2]).removeSubtrie true).1
+#guard !((zipAt fDangle [] [0,1,2]).removeSubtrie true).2.pathExists
+#guard !((zipAt fEmpty [] [3]).removeSubtrie true).1
+#guard !((zipAt fEmpty [] [3]).removeSubtrie true).2.pathExists
+#guard ((zipAt fRun [0,0] [0]).removeSubtrie true).2.trie.pathExists [0,0]
+#guard !((zipAt fRun [0,0] [0]).removeSubtrie true).2.trie.pathExists [0,0,0]
+#guard ((zipAt fRun [0,0] []).removeSubtrie true).2.pathExists
+
+#guard allZips.all (fun z => [false, true].all (fun pr =>
+  let (removed, after) := z.removeSubtrie pr
+  let (branches, z1) := z.removeBranches pr
+  let (value, composed) := z1.removeVal pr
+  removed == (branches || value.isSome) &&
+    after.trie.vals == composed.trie.vals && after.trie.paths == composed.trie.paths &&
+    after.path == z.path && after.root == z.root &&
+    !after.isVal && after.childCount == 0))
+
 /-! ## Structural invariants over every fixture -/
 
 #guard fixtures.all valsExist

diff --git a/lean/PathMapModel/Fuzz.lean b/lean/PathMapModel/Fuzz.lean
@@ -23,9 +23,14 @@ header:
   r0        := u8 % 4 ; r0 × pathbyte    -- write zipper root
   r1        := u8 % 4 ; r1 × pathbyte    -- read  zipper root
 body:
-  repeated: op := u8 % 56 ; operands per op (see `Op.decode`)
+  repeated: op := u8 % 56 ; operands per op (see `step`)
 ```
 
+Inputs prefixed with `PMFUZZ\x01\x00` followed by a little-endian u16 selector
+count (1..=256) use the same map/zipper header but decode operations modulo that
+recorded count. Headerless inputs use 56. Operation 56 is `remove_subtrie`,
+followed by a prune byte.
+
 Every **path byte** is masked to `b % 4`, so the generated tries share prefixes
 heavily — that is where the interesting trie shapes (branch points, dangling
 chains, single-child runs) live.
@@ -115,6 +120,7 @@ def dumpAt (t : PathMap V) (root : Path) : String :=
 structure Dec where
   bytes : ByteArray
   pos : Nat
+  opCount : Nat := 56
 
 /-- Read one byte; `none` once the input is exhausted, which ends the program. -/
 def Dec.u8 (d : Dec) : Option (UInt8 × Dec) :=
@@ -188,12 +194,22 @@ def showBool (b : Bool) : String := if b then "1" else "0"
 
 /-! ## The operation table
 
-`op % 56` selects the operation.  Ops `0`–`26` act on a target zipper chosen by
-a following `u8 % 2` byte (`0` = write zipper, `1` = read zipper); ops `27`–`46`
-are write-zipper operations. -/
+`op % selector_count` selects the operation (56 for headerless inputs). Ops `0`–`26`
+act on a target zipper chosen by a following `u8 % 2` byte (`0` = write zipper,
+`1` = read zipper); ops `27`–`46` and `56` are write-zipper operations. -/
+
+/-- Input header marker. Must match `WIRE_MAGIC` in the Rust harness. -/
+def wireMagic : List UInt8 := [80, 77, 70, 85, 90, 90, 1, 0]
 
-/-- Number of distinct operations.  Must match `NOPS` in `differential/src/harness.rs`. -/
-def nops : Nat := 56
+def Dec.init (bytes : ByteArray) : Option Dec := do
+  if bytes.data.toList.take wireMagic.length == wireMagic then
+    let d : Dec := { bytes, pos := wireMagic.length }
+    let (lo, d) ← d.u8
+    let (hi, d) ← d.u8
+    let count := lo.toNat + 256 * hi.toNat
+    if count == 0 || count > 256 then none
+    else some { d with opCount := count }
+  else some { bytes, pos := 0 }
 
 /-- A full `k`-path iteration: `descend_first_k_path` followed by
 `to_next_k_path` until it runs out (capped at 32 stops).  Returns the locations
@@ -225,7 +241,7 @@ def getTarget (s : St) (t : Nat) : Zip V := if t == 0 then s.wz else s.rz
 which ends the program. -/
 def step (s : St) (d : Dec) : Option (St × Dec) := do
   let (opRaw, d) ← d.u8
-  let op := opRaw.toNat % nops
+  let op := opRaw.toNat % d.opCount
   match op with
   | 0 => do let (t, d) ← d.mod 2; let (p, d) ← d.path
             let (_, s) := onTarget s t (fun z => ((), z.descendTo p))
@@ -510,6 +526,9 @@ def step (s : St) (d : Dec) : Option (St × Dec) := do
                let b := { s.rz with path := s.rz.path ++ p }
                let (st, z) := s.wz.meet2 ops s.rz b
                some (emit { s with wz := z } "meet_2" (toString st), d)
+  | 56 => do let (pr, d) ← d.bool
+             let (removed, z) := s.wz.removeSubtrie pr
+             some (emit { s with wz := z } "remove_subtrie" (showBool removed), d)
   | _ => some (emit s "nop" "-", d)
 
 /-- Run operations until the input is exhausted or `fuel` runs out. -/
@@ -553,7 +572,7 @@ def header (d : Dec) (act : Bool) : Option (St × Dec) := do
 
 /-- Decode and run a fuzzer input, returning the trace lines. -/
 def run (bytes : ByteArray) (maxSteps : Nat := 256) (act : Bool := false) : List String :=
-  match header { bytes, pos := 0 } act with
+  match Dec.init bytes >>= (fun d => header d act) with
   | none => ["EMPTY"]
   | some (s0, d) =>
       let s := loop maxSteps s0 d

diff --git a/lean/PathMapModel/Write.lean b/lean/PathMapModel/Write.lean
@@ -114,6 +114,14 @@ def removeBranches (prune : Bool) : Bool × Zip V :=
   let z' := z.withTrie (z.trie.removeBelow z.focus)
   (removed, if prune then (z'.prunePath).2 else z')
 
+/-- `ZipperWriting::remove_subtrie`: remove the focus value and all descendants,
+then optionally prune. Returns whether a value or branch was removed; pruning
+alone does not count as removal. The cursor and zipper root do not move. -/
+def removeSubtrie (prune : Bool) : Bool × Zip V :=
+  let (branches, z1) := z.removeBranches false
+  let (value, z2) := z1.removeVal false
+  (branches || value.isSome, if prune then (z2.prunePath).2 else z2)
+
 /-- `ZipperWriting::remove_unmasked_branches`: keep only the child bytes set in
 `mask`; delete the rest along with their subtries. -/
 def removeUnmaskedBranches (mask : ByteMask) (prune : Bool) : Zip V :=