diff --git a/differential/src/bin/pruned_trace.rs b/differential/src/bin/pruned_trace.rs new file mode 100644 index 00000000..9f066582 --- /dev/null +++ b/differential/src/bin/pruned_trace.rs @@ -0,0 +1,36 @@ +//! Prints the dangling-path-free differential trace for a fuzzer input, from +//! the real crate. +//! +//! pruned_trace # or read the bytes from stdin +//! +//! `lean/.lake/build/bin/pruned-oracle` prints the same trace from +//! `PrunedModel`; `lean/pruned_differential.py` runs both and diffs them. +//! +//! `--check` needs no oracle: it asserts the zipper invariants after every +//! operation and, at the end of the run, that the write target contains no +//! dangling path -- which is the whole claim this harness's operation subset +//! makes. See `differential::pruned`. + +use differential::pruned::run; +use differential::serve; + +fn main() { + let args: Vec = std::env::args().skip(1).collect(); + 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") { + serve(check, run); + return; + } + let file = args.iter().find(|a| !a.starts_with("--")).cloned(); + let bytes: Vec = match file { + Some(p) => std::fs::read(p).expect("cannot read input"), + None => { + use std::io::Read; + let mut v = Vec::new(); + std::io::stdin().read_to_end(&mut v).unwrap(); + v + } + }; + print!("{}", run(&bytes, check)); +} diff --git a/differential/src/lib.rs b/differential/src/lib.rs index 661cf803..e546ea72 100644 --- a/differential/src/lib.rs +++ b/differential/src/lib.rs @@ -8,9 +8,14 @@ //! * [`server`] is the resident-process protocol the driver speaks. //! * [`repro`] turns an input back into standalone `pathmap` calls. //! * [`act`] is the `ArenaCompactTree` read source behind `act_trace`. +//! * [`pruned`] is a second, smaller harness: the subset of the API that +//! cannot leave a dangling path, checked against `lean/PrunedModel` and +//! driven by `lean/pruned_differential.py`. See its module docs for why it +//! is not `harness` with a flag. pub mod act; pub mod harness; +pub mod pruned; pub mod repro; pub mod server; diff --git a/differential/src/pruned.rs b/differential/src/pruned.rs new file mode 100644 index 00000000..0d1acc79 --- /dev/null +++ b/differential/src/pruned.rs @@ -0,0 +1,611 @@ +//! The crate side of the **dangling-path-free** differential harness. +//! +//! `lean/.lake/build/bin/pruned-oracle` prints the same trace from +//! `PrunedModel`; `lean/pruned_differential.py` runs both and diffs them. The +//! wire format and operation table are a contract shared with +//! `lean/PrunedModel/Fuzz.lean`; any change here must be mirrored there. +//! +//! This is not [`crate::harness`] with a flag. That harness explores the whole +//! zipper API and reproduces whatever `pathmap` does with dangling paths; its +//! prune flags are pinned to `false` and compared against nothing, because the +//! flag's effect is a function of where an internal node boundary happens to +//! fall. This one explores a smaller API and makes a stronger claim about it: +//! +//! 1. **No `create_path`.** Its whole purpose is a location with no value. +//! 2. **`prune = true` everywhere**, and `prune_path` / `prune_ascend` stay in +//! the table as assertions: the model says `0`, so a non-zero count means +//! something in the subset leaked a dangling path for it to find. +//! 3. **The write zipper is rooted at the map root.** A write zipper rooted +//! below it holds a node at its own root, which survives as a location +//! leading nowhere once everything beneath it is removed, and `prune_path` +//! does not rise above the zipper's origin. Off-root *writing* is still +//! covered: the root-rooted zipper reaches every focus with `descend_to`. +//! +//! There is one read source, a `PathMap` read zipper, so no `ReadSource` trait +//! and no ACT mode — `graft_child_maps`, quarantined in the other harness, is +//! simply not in this table. +//! +//! `--check` adds in-process assertions needing no oracle: the zipper +//! invariants from [`crate::harness::check_zipper`], plus the one this harness +//! is named for — [`check_no_dangling`]. + +use pathmap::PathMap; +use pathmap::utils::ByteMask; +use pathmap::zipper::*; + +use crate::harness::{ + check_zipper, dump, fingerprint, hex_path, show_bool, show_byte_opt, show_status, show_val, + Dec, MAX_STEPS, +}; + +use core::fmt::Write as _; + +/// Number of distinct operations. Must match `PrunedModel.Fuzz.nops`. +pub const NOPS: usize = 54; + +/// Why an operation was skipped. Every `skip` in the trace carries one of +/// these. `lean/PrunedModel/Fuzz.lean` emits the same tokens; the two must +/// agree exactly or every input with a skip diverges. +/// +/// Note which reasons from [`crate::harness`] are *absent*: `skip:act` (there is +/// one read source here), `skip:off-root-prune` (the write zipper is always at +/// the map root, so the prune count is well-defined), and `skip:quarantined` +/// (`graft_child_maps` is not in this table). +/// +/// `to_next`/`to_prev_sibling_byte` at the zipper root, where the native read +/// zipper escapes its own root. +pub const SKIP_AT_ROOT: &str = "skip:at-root"; +/// A degenerate `k = 0` on `join_k_path_into` / `meet_k_path_into`. +pub const SKIP_K0: &str = "skip:k0"; +/// The focus has nothing below it, where the op's behaviour is a function of +/// node materialisation rather than of trie state. +pub const SKIP_EMPTY_FOCUS: &str = "skip:empty-focus"; +/// `insert_prefix("")`, which destroys the subtrie. +pub const SKIP_EMPTY_PATH: &str = "skip:empty-path"; + +/// The prune flag every operation in this subset is driven with. +/// +/// The opposite of [`crate::harness`]'s `no_prune`, and for the same reason +/// stated the other way round: there, the flag's effect is unspecifiable, so it +/// is never exercised; here, removal is *defined* to reclaim the chain, so it is +/// always exercised and always compared. +const PRUNE: bool = true; + +/// Does the focus have no descendants at all? +/// +/// Several return values (`remove_branches`, `restricting`, `join_map_into`, +/// `take_map`, `restrict`) hinge on whether an *empty node* happens to be +/// materialised at the focus rather than on the logical state, so they are +/// masked here. +fn focus_node_empty(z: &Z) -> bool { + z.child_count() == 0 +} + +/// Canonical rendering of a decoded byte mask: ascending, deduplicated, which is +/// what `ByteMask.ofList` produces on the Lean side. +fn canon_mask(m: &[u8]) -> Vec { + let mut v = m.to_vec(); + v.sort_unstable(); + v.dedup(); + v +} + +/// **The invariant this harness is named for**: no location exists without +/// leading to a value. +/// +/// Walks the whole map and asserts that every location with no children carries +/// a value. The root of an empty map is the one exception — `PathMap::new()` +/// reports `path_exists() == true` at the root, and there is nothing it could +/// lead to. +/// +/// This needs no oracle, which makes it the cheapest way to run the subset: +/// `--check` asserts it after every operation, and a failure localises the +/// leaking operation to one step without a trace diff. +pub fn check_no_dangling(map: &PathMap, label: &str) { + let mut z = map.read_zipper(); + // `to_next_step` visits every location strictly below the root in + // depth-first order, and the root is where the walk starts -- so step first + // and check after. The root is deliberately not checked: `PathMap::new()` + // reports `path_exists() == true` there with nothing to lead to, which is + // the one location in this model that may exist without a value below it. + while z.to_next_step() { + if z.child_count() == 0 && !z.is_val() { + panic!( + "{label}: dangling path at {} -- a location with no value and no children", + hex_path(z.path()) + ); + } + } +} + +/// Decode the header: two seeded maps and the read zipper's root. +/// +/// The write zipper's root is not decoded — it is always the map root. The read +/// zipper's root is decoded as a path and then clamped to its longest existing +/// prefix, rather than created: `create_path` is not in this subset, and a +/// zipper whose root does not exist can walk out of it (lean/FINDINGS.md #3), +/// which would contaminate every other comparison. +pub fn decode_header(d: &mut Dec) -> Option<(PathMap, PathMap, Vec)> { + let mut m0 = PathMap::::new(); + let n0 = d.modn(8)?; + for _ in 0..n0 { + let p = d.path(6)?; + let v = d.u8()? as u64; + m0.set_val_at(&p, v); + } + let mut m1 = PathMap::::new(); + let n1 = d.modn(8)?; + for _ in 0..n1 { + let p = d.path(6)?; + let v = d.u8()? as u64; + m1.set_val_at(&p, v); + } + let raw = d.path(4)?; + // Existence is prefix-closed, so the prefixes that exist form an initial + // segment: stop at the first one that does not. `PrunedModel.Fuzz`'s + // `clampToExisting` is the same computation over the model. + let mut root1: Vec = Vec::new(); + for j in 1..=raw.len() { + if m1.read_zipper_at_path(&raw[..j]).path_exists() { + root1 = raw[..j].to_vec(); + } else { + break; + } + } + Some((m0, m1, root1)) +} + +/// Decode and execute a fuzzer input. +pub fn run(bytes: &[u8], check: bool) -> String { + let mut d = Dec { bytes, pos: 0 }; + let (mut map0, map1, root1) = match decode_header(&mut d) { + Some(x) => x, + None => return "EMPTY\n".to_string(), + }; + let mut out = String::new(); + { + // NOTE: `read_zipper_at_borrowed_path` would panic (release: wrap) in + // `to_next_k_path`, whose `path_len()` underflows before the path buffer + // is prepared. Use the owned-path constructor so that known bug does + // not abort every run. + let mut rz = map1.read_zipper_at_path(&root1); + run_ops(&mut d, &mut out, &mut map0, &mut rz, &root1, check); + } + // The check needs the whole map, which the live write zipper holds, so it + // runs here rather than per step. Localising a leak to one operation is the + // trace diff's job; this is the no-oracle path. + if check { + check_no_dangling(&map0, "map0"); + } + let _ = writeln!(out, "MAP0 {}", dump(&mut map0.read_zipper())); + let _ = writeln!(out, "MAP1 {}", dump(&mut map1.read_zipper())); + // Printed for trace compatibility with the other harness, and because a + // reader of a divergence wants to see both roots stated rather than inferred. + let _ = writeln!(out, "ROOT0 {}", hex_path(&[])); + let _ = writeln!(out, "ROOT1 {}", hex_path(&root1)); + out +} + +/// Bind `$z` to the write zipper (`t == 0`) or the read zipper, then run `$e`. +macro_rules! tgt { + ($t:expr, $wz:expr, $rz:expr, $z:ident, $e:expr) => { + if $t == 0 { + let $z = &mut $wz; + $e + } else { + let $z = &mut $rz; + $e + } + }; +} + +/// Run the operation table. +pub fn run_ops( + d: &mut Dec, + out: &mut String, + map0: &mut PathMap, + rz: &mut ReadZipperUntracked<'_, '_, u64>, + root1: &[u8], + check: bool, +) { + let mut wz = map0.write_zipper(); + let root0: &[u8] = &[]; + let mut step = 0usize; + + macro_rules! get { + ($e:expr) => { + match $e { + Some(x) => x, + None => break, + } + }; + } + + loop { + if step >= MAX_STEPS { + break; + } + let op = get!(d.u8()) as usize % NOPS; + let (name, ret): (&str, String) = match op { + // ## Movement and reading, on either zipper + 0 => { + let t = get!(d.modn(2)); + let p = get!(d.path(6)); + tgt!(t, wz, *rz, z, z.descend_to(&p)); + ("descend_to", hex_path(&p)) + } + 1 => { + let t = get!(d.modn(2)); + let b = get!(d.path_byte()); + tgt!(t, wz, *rz, z, z.descend_to_byte(b)); + ("descend_to_byte", format!("{b:02x}")) + } + 2 => { + let t = get!(d.modn(2)); + let n = get!(d.modn(8)); + let r = tgt!(t, wz, *rz, z, z.ascend(n)); + ("ascend", format!("{r}")) + } + 3 => { + let t = get!(d.modn(2)); + let r = tgt!(t, wz, *rz, z, z.ascend_byte()); + ("ascend_byte", show_bool(r).to_string()) + } + 4 => { + let t = get!(d.modn(2)); + tgt!(t, wz, *rz, z, z.reset()); + ("reset", "-".to_string()) + } + 5 => { + let t = get!(d.modn(2)); + let r = tgt!(t, wz, *rz, z, z.descend_first_byte()); + ("descend_first_byte", show_byte_opt(r)) + } + 6 => { + let t = get!(d.modn(2)); + let r = tgt!(t, wz, *rz, z, z.descend_last_byte()); + ("descend_last_byte", show_byte_opt(r)) + } + 7 => { + let t = get!(d.modn(2)); + let i = get!(d.modn(6)); + let r = tgt!(t, wz, *rz, z, z.descend_indexed_byte(i)); + ("descend_indexed_byte", show_byte_opt(r)) + } + 8 => { + let t = get!(d.modn(2)); + let r = tgt!(t, wz, *rz, z, z.descend_until()); + ("descend_until", show_bool(r).to_string()) + } + 9 => { + let t = get!(d.modn(2)); + let r = tgt!(t, wz, *rz, z, z.ascend_until()); + ("ascend_until", format!("{r}")) + } + 10 => { + let t = get!(d.modn(2)); + let r = tgt!(t, wz, *rz, z, z.ascend_until_branch()); + ("ascend_until_branch", format!("{r}")) + } + 11 => { + let t = get!(d.modn(2)); + // Skipped at the zipper root: the native ReadZipper escapes its + // own root there. + if tgt!(t, wz, *rz, z, z.at_root()) { + ("to_next_sibling_byte", SKIP_AT_ROOT.to_string()) + } else { + let r = tgt!(t, wz, *rz, z, z.to_next_sibling_byte()); + ("to_next_sibling_byte", show_byte_opt(r)) + } + } + 12 => { + let t = get!(d.modn(2)); + if tgt!(t, wz, *rz, z, z.at_root()) { + ("to_prev_sibling_byte", SKIP_AT_ROOT.to_string()) + } else { + let r = tgt!(t, wz, *rz, z, z.to_prev_sibling_byte()); + ("to_prev_sibling_byte", show_byte_opt(r)) + } + } + 13 => { + let t = get!(d.modn(2)); + let r = tgt!(t, wz, *rz, z, z.to_next_step()); + ("to_next_step", show_bool(r).to_string()) + } + 14 => { + // `ZipperIteration` is read-only: the target byte is still + // consumed, but the operation always applies to `rz`. + let _t = get!(d.modn(2)); + ("to_next_val", show_bool(rz.to_next_val()).to_string()) + } + 15 => { + let _t = get!(d.modn(2)); + let k = get!(d.modn(4)); + // k == 0 is specified as an unsuccessful descent. + ("descend_first_k_path", show_bool(rz.descend_first_k_path(k)).to_string()) + } + 16 => { + let _t = get!(d.modn(2)); + let k = get!(d.modn(4)); + // A whole k-path iteration: `to_next_k_path` on its own + // continues state left by `descend_first_k_path`. + let mut v: Vec = Vec::new(); + if rz.descend_first_k_path(k) { + v.push(hex_path(rz.path())); + while v.len() < 32 && rz.to_next_k_path(k) { + v.push(hex_path(rz.path())); + } + } + ("k_path_walk", v.join(",")) + } + 17 => { + let _t = get!(d.modn(2)); + ("descend_last_path", show_bool(rz.descend_last_path()).to_string()) + } + 18 => { + let t = get!(d.modn(2)); + let p = get!(d.path(6)); + let n = tgt!(t, wz, *rz, z, z.move_to_path(&p)); + ("move_to_path", format!("{n}")) + } + 19 => { + let t = get!(d.modn(2)); + let p = get!(d.path(6)); + let n = tgt!(t, wz, *rz, z, z.descend_to_existing(&p)); + ("descend_to_existing", format!("{n}")) + } + 20 => { + let t = get!(d.modn(2)); + let p = get!(d.path(6)); + let n = tgt!(t, wz, *rz, z, z.descend_to_val(&p)); + ("descend_to_val", format!("{n}")) + } + 21 => { + let t = get!(d.modn(2)); + let b = get!(d.path_byte()); + let r = tgt!(t, wz, *rz, z, z.descend_to_existing_byte(b)); + ("descend_to_existing_byte", show_bool(r).to_string()) + } + 22 => { + let t = get!(d.modn(2)); + let n = get!(d.modn(8)); + let r = tgt!(t, wz, *rz, z, z.descend_until_max_bytes(n)); + ("descend_until_max_bytes", show_bool(r).to_string()) + } + 23 => { + let t = get!(d.modn(2)); + let p = get!(d.path(6)); + let r = tgt!(t, wz, *rz, z, z.descend_to_check(&p)); + ("descend_to_check", show_bool(r).to_string()) + } + 24 => { + let t = get!(d.modn(2)); + let p = get!(d.path(6)); + let v = tgt!(t, wz, *rz, z, show_val(z.val_at(&p))); + ("val_at", v) + } + 25 => { + let t = get!(d.modn(2)); + let n = if t == 0 { + wz.make_map().val_count() + } else { + rz.make_map().val_count() + }; + ("make_map_val_count", format!("{n}")) + } + 26 => { + let t = get!(d.modn(2)); + let s = if t == 0 { + dump(&mut wz.fork_read_zipper()) + } else { + dump(&mut rz.fork_read_zipper()) + }; + ("dump", s) + } + 27 => { + let t = get!(d.modn(2)); + // The blind-zipper addition: `descend_until` reporting the bytes + // it descended. The observer's output is a blind zipper's only + // account of where it went, so it is compared byte for byte. + let mut obs: Vec = Vec::new(); + let r = tgt!(t, wz, *rz, z, z.descend_until_observed(&mut obs)); + ("descend_until_observed", format!("{}:{}", show_bool(r), hex_path(&obs))) + } + 28 => { + let t = get!(d.modn(2)); + let p = get!(d.path(6)); + // `get_val`/`get_val_at` must agree with `val`/`val_at`; they + // differ only in the lifetime of the reference returned. + let (g, ga, agree) = if t == 0 { + // A write zipper has no `ZipperReadOnlyValues`. + (wz.val().copied(), wz.val_at(&p).copied(), true) + } else { + let (g, ga) = (rz.get_val().copied(), rz.get_val_at(&p).copied()); + let agree = g == rz.val().copied() && ga == rz.val_at(&p).copied(); + (g, ga, agree) + }; + ( + "get_val_agrees", + format!("{}:{}:{}", show_val(g.as_ref()), show_val(ga.as_ref()), show_bool(agree)), + ) + } + 29 => { + let got = rz.to_next_get_val().copied(); + // `to_next_get_val` is specified as `to_next_val` followed by + // reading the value, so `Some` must mean it moved and must equal + // what `val` reports. + let agree = got == rz.val().copied() || (got.is_none() && rz.at_root()); + ( + "to_next_get_val", + format!("{}:{}:{}", show_bool(got.is_some()), show_val(got.as_ref()), show_bool(agree)), + ) + } + // ## Writing, on the write zipper + 30 => { + let v = get!(d.u8()) as u64; + ("set_val", show_val(wz.set_val(v).as_ref())) + } + 31 => ("remove_val", show_val(wz.remove_val(PRUNE).as_ref())), + 32 => { + // Must be `0`: a trie built from this subset has no dangling tip. + ("prune_path", format!("{}", wz.prune_path())) + } + 33 => ("prune_ascend", format!("{}", wz.prune_ascend())), + 34 => { + let leaky = focus_node_empty(&wz); + let r = wz.remove_branches(PRUNE); + // An empty node still comes back as `Some(..)` from + // `into_option()` for some representations, so `true` gets + // reported for a removal of nothing. Compared only when there + // was something below. + let s = if leaky { "?".to_string() } else { show_bool(r).to_string() }; + ("remove_branches", s) + } + 35 => { + let n = get!(d.modn(4)); + let m = get!(d.path_n(n)); + wz.remove_unmasked_branches(ByteMask::from_iter(m.iter().copied()), PRUNE); + ("remove_unmasked_branches", hex_path(&canon_mask(&m))) + } + 36 => { + wz.graft(&*rz); + ("graft", "-".to_string()) + } + 37 => { + let p = get!(d.path(6)); + wz.graft_src_at(&*rz, &p); + ("graft_src_at", hex_path(&p)) + } + 38 => ("join_into", show_status(wz.join_into(&*rz)).to_string()), + 39 => { + let leaky = focus_node_empty(&wz); + let st = wz.join_map_into(rz.make_map()); + let s = if leaky { "?".to_string() } else { show_status(st).to_string() }; + ("join_map_into", s) + } + 40 => ("meet_into", show_status(wz.meet_into(&*rz, PRUNE)).to_string()), + 41 => ("subtract_into", show_status(wz.subtract_into(&*rz, PRUNE)).to_string()), + 42 => { + let leaky = focus_node_empty(&wz); + let st = wz.restrict(&*rz); + let s = if leaky { "?".to_string() } else { show_status(st).to_string() }; + ("restrict", s) + } + 43 => { + // Skipped when either side has nothing below its focus: there + // `restricting` branches on whether an empty node happens to be + // materialised, and the branches differ in *effect*. + if focus_node_empty(&wz) || focus_node_empty(rz) { + ("restricting", SKIP_EMPTY_FOCUS.to_string()) + } else { + ("restricting", show_bool(wz.restricting(&*rz)).to_string()) + } + } + 44 => { + let k = get!(d.modn(4)); + // `join_k_path_into(0)` collapses the subtrie instead of being + // the identity. + if k == 0 { + ("join_k_path_into", SKIP_K0.to_string()) + } else { + let r = wz.join_k_path_into(k, PRUNE); + let s = if focus_node_empty(&wz) { "?".to_string() } else { show_bool(r).to_string() }; + ("join_k_path_into", s) + } + } + 45 => { + let p = get!(d.path(6)); + // `insert_prefix("")` destroys the subtrie. + if p.is_empty() { + ("insert_prefix", SKIP_EMPTY_PATH.to_string()) + } else { + ("insert_prefix", show_bool(wz.insert_prefix(&p)).to_string()) + } + } + 46 => { + let n = get!(d.modn(6)); + ("remove_prefix", show_bool(wz.remove_prefix(n)).to_string()) + } + 47 => { + let leaky = focus_node_empty(&wz) && wz.val().is_none(); + let r = match wz.take_map(PRUNE) { + Some(m) => { + wz.graft_map(m); + "1" + } + None => "0", + }; + ("take_map_restore", if leaky { "?".to_string() } else { r.to_string() }) + } + 48 => { + let k = get!(d.modn(4)); + // `meet_k_path_into` spins forever when the focus has no + // children, and escapes the focus subtree when k == 0. + if k == 0 { + ("meet_k_path_into", SKIP_K0.to_string()) + } else if wz.child_count() == 0 { + ("meet_k_path_into", SKIP_EMPTY_FOCUS.to_string()) + } else { + ("meet_k_path_into", show_bool(wz.meet_k_path_into(k, PRUNE)).to_string()) + } + } + 49 => { + let v = get!(d.u8()) as u64; + // Writing through the reference `get_val_mut` hands back. It + // must behave like `set_val` where a value exists and do nothing + // -- crucially, not create the path -- where one does not. + let old = match wz.get_val_mut() { + Some(slot) => { + let old = *slot; + *slot = v; + Some(old) + } + None => None, + }; + ("get_val_mut_write", show_val(old.as_ref())) + } + 50 => { + let v = get!(d.u8()) as u64; + let r = *wz.get_val_or_set_mut(v); + ("get_val_or_set_mut", show_val(Some(&r))) + } + 51 => { + let v = get!(d.u8()) as u64; + // `ran` records whether the closure was invoked; the contract is + // that it supplies the value only when none exists. + let mut ran = false; + let r = *wz.get_val_or_set_mut_with(|| { + ran = true; + v + }); + ("get_val_or_set_mut_with", format!("{}:{}", show_val(Some(&r)), show_bool(ran))) + } + 52 => { + let n = get!(d.modn(4)); + let m = get!(d.path_n(n)); + let ru = get!(d.boolean()); + wz.graft_masked_branches(&*rz, ByteMask::from_iter(m.iter().copied()), ru); + ("graft_masked_branches", format!("{}:{}", hex_path(&canon_mask(&m)), show_bool(ru))) + } + 53 => { + let p = get!(d.path(6)); + // `meet_2` takes two sources; the second is the first moved to `p`. + let mut b = rz.clone(); + b.descend_to(&p); + ("meet_2", show_status(wz.meet_2(&*rz, &b)).to_string()) + } + _ => ("nop", "-".to_string()), + }; + if check { + check_zipper(&wz, "write zipper", root0); + check_zipper(rz, "read zipper", root1); + } + let _ = writeln!( + out, + "{step} {name} ret={ret} W={} R={}", + fingerprint(&wz, root0), + fingerprint(rz, root1) + ); + step += 1; + } +} diff --git a/lean/PRUNED_FINDINGS.md b/lean/PRUNED_FINDINGS.md new file mode 100644 index 00000000..519a6d27 --- /dev/null +++ b/lean/PRUNED_FINDINGS.md @@ -0,0 +1,366 @@ +# Findings from the dangling-path-free model + +What `lean/pruned_differential.py` found, driving `PrunedModel` (the oracle) +against `differential/src/pruned.rs` (the crate) on `pathmap` 0.4.0 at +`833d524`. + +This is a separate file from `FINDINGS.md` because it is a separate claim. +`FINDINGS.md` records what the crate does with dangling paths, as discovered by +a model that reproduces them. This model instead *forbids* them: its subset is +chosen so that no operation in it should be able to make a location that leads +nowhere. So every finding here has the same shape — "this operation made one" — +and the interest is in which operations, and why. + +Minimal reproducers are in `lean/pruned-corpus/`, 9–47 bytes each. Replay one +with + + ./target/release/pruned_trace lean/pruned-corpus/.bin + ./lean/.lake/build/bin/pruned-oracle lean/pruned-corpus/.bin + +or check the whole corpus with `./lean/pruned_differential.py +lean/pruned-corpus/*`. + +## 1. An empty write materialises the focus + +**Seven operations create or keep a dangling path when what they write is +empty.** First 300 random inputs: 63 of 70 divergences, and every one of them +this. + +| operation | reproducer | +| --- | --- | +| `graft` | `graft-empty-src-creates-dangling-focus.bin` | +| `graft_src_at` | `graft_src_at-empty-src-creates-dangling-focus.bin` | +| `graft_masked_branches` | `graft_masked_branches-creates-dangling-focus.bin` | +| `meet_2` | `meet_2-empty-result-creates-dangling-focus.bin` | +| `restrict` | `restrict-empty-result-creates-dangling-focus.bin` | +| `restricting` | `restricting-creates-dangling-focus.bin` | +| `remove_prefix` | `remove_prefix-creates-dangling-chain.bin` | + +The smallest is nine bytes. An empty `map1`, a `map0` holding one root value, a +write zipper at the map root descended one byte to a location that does not +exist, and then `graft` from a read zipper whose subtrie is empty: + + 0 descend_to_byte ret=00 W=00 o00 e0 v- c0 n0 + 1 graft ret=- W=00 o00 e0 v- c0 n0 model + 1 graft ret=- W=00 o00 e1 v- c0 n0 crate + MAP0 _:- model + MAP0 _:-,00:- crate + +`path_exists()` reports `true` at a location with no value and no children. +Nothing leads there and nothing can reach it except a zipper that already knows +the path, so it is pure overhead to every traversal — and `val_count() == 0` +beside `child_count() == 0` and `path_exists() == true` is a state no reader of +the trait documentation would expect to have to handle. + +Every fingerprint in a trace is the state **after** the operation, so the `e0` +on the model side is the model saying the location is gone, not that it was +missing beforehand. In every reproducer the focus existed and held content +before the call: in the one above it held the value `0`, which `graft` correctly +clears (the empty source has no root value) before leaving the emptied location +behind. So this is a missing prune throughout, and not — as an earlier reading +of these traces had it — an operation creating a location from nothing. A +direct probe confirms it: `graft` of an empty source at a focus that genuinely +does not exist creates nothing. + +`remove_prefix` shows the scale: it leaves the whole chain, not just the tip. + + 2 remove_prefix ret=1 MAP0 _:- model + 2 remove_prefix ret=1 MAP0 _:-,00:-,0000:-,000000:- crate + +**Why these seven and not the others.** `remove_val`, `remove_branches`, +`remove_unmasked_branches`, `meet_into`, `subtract_into` and `join_k_path_into` +take a `prune: bool`, and with `prune = true` — which is what this harness +passes throughout — they clean up correctly. The seven above have no such +parameter, so a caller who wants a tidy trie has no way to ask for one. The +asymmetry looks unintended rather than designed: `meet_into` and `meet_2` are +the same operation with and without a destination, and only one of them can be +told to prune. + +## 2. `graft_masked_branches` keeps a child whose branch the source lacks + +`graft_masked_branches-creates-dangling-child.bin`, 10 bytes. `map0` is +`{[1] ↦ 0}`, `map1` is empty, write zipper at the root, mask `{0x01}`, +`remove_unset = false`: + + 0 graft_masked_branches ret=01:0 W=_ o_ e1 v- c0 n0 model + 0 graft_masked_branches ret=01:0 W=_ o_ e1 v- c1 n0 crate + MAP0 _:- model + MAP0 _:-,01:- crate + +Each set bit of the mask is specified as a `graft_src_at` of the source's +corresponding child, and grafting nothing removes — so a set bit whose branch is +absent from the source must leave that branch absent here. The value at `[1]` +*is* removed, correctly; the child slot is not. + +It is finding 1's mechanism one level down, and worse there, because what +survives is a *child of the focus* rather than the focus itself: the focus's +`child_mask` now has a bit set for a branch that holds nothing, and +`child_count() == 1` beside `val_count() == 0`. Every consumer that uses +`child_mask` to decide where to recurse walks into it. + +## The fix + +All of it funnels through one line. `graft_internal` is the single place that +learns "the result is empty", and fourteen sites across nine operations hand it a +`None`: + +```rust +pub(crate) fn graft_internal(&mut self, src: Option>) { + match src { + Some(src) => { /* ... */ }, + None => { self.remove_branches(false); } // <-- here + } +} +``` + +It cannot simply be flipped to `true`, because `meet_into` and `subtract_into` +*are* documented to leave dangling paths when their own `prune` is `false`. So +`graft_internal` has to take the flag rather than decide it: + +* `graft_internal(src, prune)`, with the `None` arm as `remove_branches(prune)`. +* The three operations that own a `prune` parameter forward it — which is also + how the codebase already reads, since each of them follows the call with + `if prune { self.prune_path(); }`. +* The rest pass `true`. They have no caller intent to honour, and a location + that leads nowhere is not something a caller can have asked for. + +Three places need the same change for the same reason, because they do their own +removing rather than going through the funnel: + +* the value step of `graft` / `graft_src_at` / `graft_map` — `remove_val(false)`. + The node step cannot reclaim a location whose value is removed *after* it, so + both halves have to prune, and neither alone is enough: a focus with a value + and no children is fixed only by the value step, one with children and no value + only by the node step. +* `graft_masked_branches`'s own `remove_branches` / `remove_unmasked_branches` + (and the identical pair in the `ZipperWriting` default implementation). +* `graft_masked_branches`'s bulk arm, for masks of three bits or more, which + merges through a borrow of the focus node and so never reaches + `graft_internal` at all. It needs a `prune_path()` after the merge — + `prune_path` is already a no-op unless the focus really is a dangling tip, so + that costs one `node_is_empty` check. + +### Measured + +| | before | after | +| --- | --- | --- | +| this class, 4000 programs at seed 11 | 901 | **0** (with `meet_2`: see below) | +| inputs agreeing, same 4000 | 3005 | 3888 | +| `cargo test --lib` | 1030 pass | 1033 pass | + +At scale, and with the §3 value-bias cherry-pick in as well — **200 000 random +programs, seed 7**: + +| | inputs | +| --- | --- | +| agree | 193 413 | +| `meet_2`, left unchanged on purpose (below) | 5 921 | +| residual node-level `Identity` imprecision (§3) | 8 | +| value bias (§3, fixed) | **0** | +| value-level `Identity` imprecision (§3, fixed) | **0** | +| anything else | **0** | + +The old harness, 30 000 programs at the same seed: 28 989 agree, 0 unclassified. + +And without any oracle at all, `pruned_trace --check` asserts the invariant +in-process on the finished trie. Over 4000 programs it aborts on 16 — and on +**0** once `meet_2` prunes too, which is the independent confirmation that +`meet_2` is the only source left. + +### `meet_2` is left out, deliberately + +One call site is not changed, and it is worth saying why rather than quietly +flipping it. Pruning `meet_2` accounts for 100 of the 901, and it collides with +two things: + +* `src/write_zipper.rs`'s own regression test + `write_zipper_subtract_into_dense_drops_reached_dangling_path` asserts "the + meet should leave `[2]` dangling", and uses `meet_2` to *construct* a dangling + path in a particular node representation so that the rest of the test can + subtract against it. Pruning `meet_2` makes that setup impossible, and + rewriting it with `create_path` would reach a different representation and + silently weaken a representation-sensitive test. +* the meet/prune semantics settled on `fuzz-fixes-v3` — "meet is an intersection + of locations, and prune is what drops dangling paths" — under which a meet + without a `prune` flag arguably *should* keep them. + +So the real defect at `meet_2` is that it has no `prune` parameter, where +`meet_into` does: the same operation, with and without a destination, and only +one of them lets the caller ask for a tidy trie. Adding one is an API change +and a decision rather than a bug fix, so it is left stated, not made. Flipping +it is a one-word change at the four `graft_internal(None, false)` sites in +`meet_2`, and it accounts for every dangling path the fixed crate still +produces: 5901 of 200 000 inputs, and all 16 of the `--check` aborts above. + +### One residual, off the map root + +`FINDINGS.md` #7 — the `prune` flag's effect *inside* a node — becomes reachable +through these operations now that they prune unconditionally. With +`prune = true`, `node_prune_limit` hands a prune limit into +`node_remove_all_branches`, which reclaims a dangling key within the node even +where it reports removing nothing, so how deep the reclamation reaches is a +function of where the node boundary falls. + +This is invisible to the harness in this directory, whose write zipper is always +at the map root: 200 000 inputs leave none of it. The other harness allows +off-root write zippers and sees it on 5 of 30 000, all in `remove_prefix`; it is +filed in `lean/differential.py`'s `KNOWN` as `implicit_prune_node_layout`. The +same mechanism is why `PathMapModel`'s `tidy` is *unconditional* — guarding it on +"did the removal report a removal" is the intuitive reading and costs 302 +divergences in 8000 inputs, against 5 in 30 000 for not guarding. + +## 3. Pre-existing classes this model also reports + +Two divergence shapes are not about dangling paths. Both are already recorded +against the other model; they appear here because the operation subsets overlap, +and they are in the corpus so a regression in either shows up in whichever +harness is run. + +* **A value collision resolves to the counterpart.** + `join_into-value-bias-by-node-layout.bin`. `u64`'s `pjoin` returns + `Identity(SELF_IDENT)`, so the destination's value must survive a collision; + at one location out of six the crate kept the source's (`0301:118` against + `0301:0`). Which location depends on node layout, not on the paths — see + `FINDINGS.md` on value bias. 7 of 4000 inputs. + + **Fixed here** by cherry-picking `3dae731` ("Make meet/join value bias + independent of node layout") from `fuzz-fixes-v3`. Three hunks in + `line_list_node.rs` conflicted; the commit message documents its own + resolutions, and master is newer in two of them (`clone_as_dense` for cell + nodes, and `preserve_prune_limit`), so those keep master's form and take only + the new `list_is_left` argument. It is no longer in the driver's `KNOWN`, so a + recurrence reports as new. + +* **`Identity` is not reported where nothing changed**, in `subtract_into` and + `meet_into`. `FINDINGS.md` #8. 686 of 200 000 inputs. + `subtract_into-status-element-when-unchanged.bin`, 22 bytes: + + map0 = {[] ↦ 0, [1] ↦ 0} the destination + map1 = {[1,1] ↦ 1}, read zipper rooted at [1], so the source node is {[1] ↦ 1} + + 0 subtract_into ret=Identity MAP0 _:0,01:0 model + 0 subtract_into ret=Element MAP0 _:0,01:0 crate + + The two dumps are identical: `psubtract(0, 1)` keeps the destination's `0`, so + nothing anywhere changed, and the model reports `Identity` while the crate + reports `Element`. + + The status is *weaker* than the truth rather than wrong — `Element` only + claims "`self` holds the output", which it does — so this costs work, not + correctness. It costs real work, though: the `Identity` arm of + `subtract_into` returns without calling `graft_internal` at all, while the + `Element` arm grafts the freshly built node over the old one, so a destination + that was structurally shared with another trie is copied apart for no reason. + + It comes from two layers. At the **value** level, + `impl DistributiveLattice for u64` returned `AlgebraicResult::Element(*self)` + where the values differ — "here is a newly computed value", which happens to + be `self`'s own — rather than `Identity(SELF_IDENT)`, which `src/ring.rs`'s own + documentation says is the legal way for a non-commutative operation to report + no change. The node algebra propagates identity *masks*, not values, so one + `Element` below a node forces the whole node, and with it `subtract_into`, to + report `Element` for a byte-identical trie. At the **node** level the crate + assembles its status compositionally as it walks and never asks whether the + node it assembled equals the one it replaces, whereas `nodeStatus` decides by + comparing them — so the models recover a precision the crate's path has already + lost. + + **Mostly fixed here** by cherry-picking `f8a4599` from `fuzz-fixes-v3`, which + is the value level: two lines, `Element(*self)` → `Identity(SELF_IDENT)` in the + `u64` and `u16` instances. `bool` in the same file already did this; the + integer instances were the outliers. `Basic.u64Ops.psub` is a transcription of + that instance rather than an independent claim, so it moves with it in the same + commit — otherwise the model asserts the behaviour of a version that no longer + exists. Both models share `Basic.lean`, so one line covers both. + + That takes the class from 686 of 200 000 inputs to **8** — 6 `meet_into` and 2 + `subtract_into`, 0.004%. What is left is the node level: rarer shapes where + the assembled node equals the one it replaces and nothing notices. Fixing + those is per node type, and `fuzz-fixes-v3` has a commit for each + (`7662195`, `15a392d`, `c882a38`, `618f8ce`, `9f382a6`, `3a98201`); they are not + picked here. + + The `join_map_into` form of this, which `join_map_into-status-element-when-unchanged.bin` + reproduces and which accounted for most of the class, **was not a crate + defect**: the empty-source-node exit of `join_map_into` used to `return` the + node status on its own, discarding a value status for a value it had already + written, and master fixed that in PR #142 (`276fca0`, issue #139) by ending + both exits in `node_status.merge(val_status, true, true)`. Both models still + described the early return. So master moved and the models lagged — the + reverse of what §4 of this file first claimed — and correcting them takes the + class from 104 of 4000 to 8. + +## 4. Against `fuzz-fixes-v3` + +Same 4000 inputs, same seed, with the harness built on `fuzz-fixes-v3` +(`ee7546e`) and the oracle unchanged. `fuzz-fixes-v3` carries 73 commits of +fixes off an older master, several of them about dangling paths, so the question +is which of the above it already answers. + +| finding | master `ec818cf` | `fuzz-fixes-v3` | +| --- | --- | --- | +| #1 + #2, empty write materialises a location | 897 + 64 | **not fixed** — 974, and all 8 reproducers still diverge | +| #3, value bias | 7 | fixed (`3dae731`, "Make meet/join value bias independent of node layout") | +| #3, `Identity` not reported | 87 | 0, but see below | + +So the branch fixes the one class this model genuinely inherited, and neither of +the two it found. That is not surprising — `fuzz-fixes-v3` was driven by the +other model, which *reproduces* dangling paths rather than forbidding them, so no +amount of fuzzing against it could have reported finding 1. It is the clearest +argument for keeping both models: they cannot find each other's bugs. + +Two attribution traps are worth writing down, because both caught me. + +* The `Identity` row needs a qualification. Most of that class was **the models + describing a `join_map_into` status master had already changed** in PR #142 + (`276fca0`, issue #139): its empty-source-node exit used to `return` the node + status on its own, discarding a value status for a value it had already + written, and master replaced that with + `node_status.merge(val_status, true, true)`. Both models still described the + early return — corrected in the commit after this one, which takes the class + from 104 of 4000 to 8. `fuzz-fixes-v3` predates PR #142, so it scored 0 on this + not by fixing anything but by still matching what the models said. +* `3e839e8` ("Fix join_into replacing or misreporting a destination that holds + the source") looks like a candidate and is **already on master** as `1e3b1c3` + (PR #116); cherry-picking it yields only comment churn and duplicate tests. + +Check `git log master -S` before attributing anything here to v3. + +Two things in the v3 column are **not** findings and should not be read as any: + +* **420 inputs diverge in `descend_first_k_path` / `k_path_walk`.** v3 changes + the k-path walk (`7f9c59a`, "Fix the default k-path walk looping forever at a + leaf", among others) and updates its own copy of the model to match. + `PrunedModel` was ported from master's model, so it still specifies master's + behaviour. This is spec drift between the two branches, and re-measuring the + k-path operations on v3 needs the port redone against v3's model. +* **45 of 600 inputs show `subtract_into` reporting `Identity`** where the model + says `Element` — the opposite direction from finding 3. v3 deliberately + changed the integer instance (`f8a4599`, "Return Identity from the integer + psubtract when nothing was subtracted"); `Basic.u64Ops` is master's and + returns `Element(*self)`. Also spec drift. + +Both are visible only because the oracle is pinned to master while the crate is +not. The `STATUS-ONLY` shape in particular is two-directional, so the driver's +`KNOWN` note for it says to read the direction rather than the tag. + +## What is not covered + +The subset deliberately excludes three things, and a reader comparing the two +harnesses should know they are gaps here rather than absences of defects: + +* `create_path`, and `remove_val(false)` — they make dangling paths on purpose. +* A write zipper rooted below the map root. It holds a node at its own root, + which survives as a dangling path once everything below it is removed, and + `prune_path` is documented not to rise above the zipper's origin. So a + dangling root there is the documented behaviour, not a defect, and comparing + it would drown everything else. Off-root *writing* is covered: the + root-rooted zipper reaches every focus with `descend_to`. +* `graft_child_maps`, which `FINDINGS.md` #15 records as broken three ways. + +Operations the subset *does* cover are specified, not skipped, even where they +are known to leak — which is why finding 1 is reported rather than suppressed. +The four `skip:` reasons that remain (`at-root`, `k0`, `empty-focus`, +`empty-path`) are the ones where the crate's behaviour is a function of node +materialisation rather than of trie state, so there is nothing for a model to +agree with; each is commented at its site in `PrunedModel/Fuzz.lean`. diff --git a/lean/PathMapModel/Basic.lean b/lean/PathMapModel/Basic.lean index ff22667f..4eb73198 100644 --- a/lean/PathMapModel/Basic.lean +++ b/lean/PathMapModel/Basic.lean @@ -40,8 +40,8 @@ inductive ValRes (V : Type) where These return `ValRes` rather than plain values because `pathmap` reports `AlgebraicStatus` to the caller, and the status depends on *which constructor* the value operation returned, not on whether the value changed. `u64`'s -`psubtract`, for instance, returns `Element(*self)` — an `Element` status even -though the stored value is unchanged. -/ +`pjoin`, for instance, returns `Identity(SELF_IDENT)` rather than `Element` of +the value it selected, so a join reports that nothing changed. -/ structure ValOps (V : Type) where /-- `Lattice::pjoin` -/ pjoin : V → V → ValRes V @@ -63,14 +63,32 @@ def ValRes.resolve {V : Type} : ValRes V → V → V → Option V Both `pjoin` and `pmeet` return `Identity(SELF_IDENT)`: they are *left-biased projections* that ignore the counterpart value entirely. `psubtract` annihilates only when the two values are equal, and otherwise returns -`Element(*self)`. This is the instance the differential fuzz target uses, so -the model reproduces it exactly rather than assuming a "real" lattice. -/ +`Identity(SELF_IDENT)`: subtracting a value that is not there leaves the +destination alone, and says so. This is the instance the differential fuzz +target uses, so the model reproduces it exactly rather than assuming a "real" +lattice. -/ def u64Ops : ValOps UInt64 where pjoin _ _ := .identity true false pmeet _ _ := .identity true false - psub a b := if a == b then .none else .elem a + psub a b := if a == b then .none else .identity true false beq a b := a == b +/-- The instance `pathmap` provides for `()` (see `impl Lattice for ()` in `src/ring.rs`). + +Both `pjoin` and `pmeet` return `Identity(SELF_IDENT | COUNTER_IDENT)` — with only +one value there is nothing to choose between, so each operand is equally "the +answer", and the node algebra is told so. `psubtract` of two `()`s annihilates, +which `src/ring.rs`'s own `option_subtract_test` asserts. + +This is the instance under which a trie is exactly a *set of paths*, and it is +the one for which the lattice laws hold in full — including commutativity, which +`u64Ops` does not satisfy. See `PrunedModel/Lattice.lean`. -/ +def unitOps : ValOps Unit where + pjoin _ _ := .identity true true + pmeet _ _ := .identity true true + psub _ _ := .none + beq _ _ := true + /-! ## Prefix order -/ /-- `p ≼ q`: `p` is a prefix of `q`. -/ @@ -120,6 +138,79 @@ def Path.le (p q : Path) : Bool := Path.lt p q || p == q instance : LT Path := ⟨fun p q => Path.lt p q = true⟩ instance : LE Path := ⟨fun p q => Path.le p q = true⟩ +/-! ### `Path.lt` is a strict total order + +Needed to show that the canonical form is *unique* — that two sorted, +duplicate-free entry lists holding the same values are the same list — which is +what lets `PrunedModel/Lattice.lean` state the lattice laws as equations rather +than as "equal at every path". Nothing else in the model needs them, which is +why they were not here before. -/ + +/-- `UInt8` order facts, routed through `toNat` so `omega` can see them. -/ +private theorem u8_lt_trans {a b c : UInt8} (h1 : a < b) (h2 : b < c) : a < c := by + rw [UInt8.lt_iff_toNat_lt] at *; omega +private theorem u8_lt_irrefl (a : UInt8) : ¬ (a < a) := by + rw [UInt8.lt_iff_toNat_lt]; omega +private theorem u8_eq_of_not_lt {a b : UInt8} (h1 : ¬ (a < b)) (h2 : ¬ (b < a)) : a = b := by + rw [UInt8.lt_iff_toNat_lt] at h1 h2 + exact UInt8.toNat_inj.mp (by omega) +private theorem u8_lt_of_lt_of_not_gt {a b c : UInt8} (h1 : a < b) (h2 : ¬ (c < b)) : a < c := by + rw [UInt8.lt_iff_toNat_lt] at *; omega + +theorem Path.lt_cons (a b : UInt8) (as bs : Path) : + Path.lt (a :: as) (b :: bs) + = if a < b then true else if b < a then false else Path.lt as bs := rfl + +@[simp] theorem Path.lt_irrefl : ∀ p : Path, Path.lt p p = false + | [] => rfl + | a :: as => by simp [Path.lt_cons, u8_lt_irrefl a, Path.lt_irrefl as] + +theorem Path.lt_trans : ∀ {p q r : Path}, + Path.lt p q = true → Path.lt q r = true → Path.lt p r = true + | [], [], _, h1, _ => by simp [Path.lt] at h1 + | [], _ :: _, [], _, h2 => by simp [Path.lt] at h2 + | [], _ :: _, _ :: _, _, _ => rfl + | _ :: _, [], _, h1, _ => by simp [Path.lt] at h1 + | _ :: _, _ :: _, [], _, h2 => by simp [Path.lt] at h2 + | a :: as, b :: bs, c :: cs, h1, h2 => by + rw [Path.lt_cons] at h1 h2 ⊢ + by_cases hab : a < b + · by_cases hcb : c < b + · -- the hypothesis forces `b < c`, which `c < b` contradicts + simp [hcb] at h2 + exact absurd (u8_lt_trans h2 hcb) (u8_lt_irrefl b) + · simp [u8_lt_of_lt_of_not_gt hab hcb] + · by_cases hba : b < a + · simp [hab, hba] at h1 + · -- a = b, so the comparison is decided one level down + have hab' : a = b := u8_eq_of_not_lt hab hba + subst hab' + simp only [hab] at h1 + by_cases hac : a < c + · simp [hac] + · by_cases hca : c < a + · simp [hca] at h2 + exact absurd (u8_lt_trans h2 hca) (u8_lt_irrefl a) + · simp only [hac, hca] at h2 ⊢ + exact Path.lt_trans h1 h2 + +theorem Path.lt_total : ∀ (p q : Path), Path.lt p q = true ∨ p = q ∨ Path.lt q p = true + | [], [] => Or.inr (Or.inl rfl) + | [], _ :: _ => Or.inl rfl + | _ :: _, [] => Or.inr (Or.inr rfl) + | a :: as, b :: bs => by + rw [Path.lt_cons, Path.lt_cons] + by_cases hab : a < b + · exact Or.inl (by simp [hab]) + · by_cases hba : b < a + · exact Or.inr (Or.inr (by simp [hba])) + · have : a = b := u8_eq_of_not_lt hab hba + subst this + rcases Path.lt_total as bs with h | h | h + · exact Or.inl (by simp [hab, h]) + · exact Or.inr (Or.inl (by simp [h])) + · exact Or.inr (Or.inr (by simp [hab, h])) + /-- Insertion into a `Path.lt`-sorted list, dropping duplicates. -/ def Path.insertSorted (p : Path) : List Path → List Path | [] => [p] diff --git a/lean/PathMapModel/Spec.lean b/lean/PathMapModel/Spec.lean index 44158a55..ca2db182 100644 --- a/lean/PathMapModel/Spec.lean +++ b/lean/PathMapModel/Spec.lean @@ -140,10 +140,7 @@ theorem isPrefixOf_append (p q : Path) : p ≼ (p ++ q) := by | nil => simp [isPrefixOf] | cons a as ih => simp [isPrefixOf, ih] -@[simp] theorem lt_irrefl (p : Path) : Path.lt p p = false := by - induction p with - | nil => simp [Path.lt] - | cons a as ih => simp [Path.lt, ih] +-- `Path.lt_irrefl` now lives in Basic.lean, beside `lt_trans` and `lt_total`. end Path @@ -329,11 +326,24 @@ bug — see `tests/pathmap_algebra_differential.rs`. -/ def restrictSelf (ops : ValOps V) (a : PathMap V) : Bool := PathMap.beqT ops (Map.restrict a a) a -/-- `take_map` followed by `graft_map` restores the trie exactly. -/ +/-- `take_map` followed by `graft_map` restores the trie exactly — provided +there was something to take. + +The proviso is not a weakening to dodge a failure; it is where the round-trip +genuinely stops being one. `take_map(false)` at a focus that holds nothing +leaves the location behind as a dangling path and returns `none`, and +`graft_map` of an empty map now *reclaims* that location, because an operation +whose result is nothing leaves no location behind (see +lean/PRUNED_FINDINGS.md). So on that one state the pair is not the identity, and +the two halves disagree about a location rather than about any content. The +differential harness masks exactly this case on op 45 for the same reason. -/ def takeThenGraft (ops : ValOps V) (z : Zip V) : Bool := let (m, z1) := z.takeMap false - let z2 := z1.graftMap (m.getD PathMap.empty) - PathMap.beqT ops z2.trie z.trie + match m with + | none => true + | some m => + let z2 := z1.graftMap m + PathMap.beqT ops z2.trie z.trie /-- Grafting one subtrie into two places makes two *independent* copies: writing under one leaves the other exactly as it was. diff --git a/lean/PathMapModel/Write.lean b/lean/PathMapModel/Write.lean index 6ee3a84e..dd69ee77 100644 --- a/lean/PathMapModel/Write.lean +++ b/lean/PathMapModel/Write.lean @@ -100,6 +100,41 @@ def pruneAscend : Nat × Zip V := let (n, z') := z.prunePath (n, (z'.ascend n).2) +/-- Reclaim the focus when a write left it leading nowhere. + +`prune_path` is already a no-op unless the focus is a dangling tip, so this is +exactly "prune if the write emptied the location". The operations below that +have no `prune` parameter end with it, because `graft_internal` now passes +`prune = true` on its empty-source arm and the `graft` family's value step +passes it too -- an operation whose result is nothing leaves no location behind. +The ones that *do* take a flag (`meet_into`, `subtract_into`, +`join_k_path_into`) still honour it, and `meet_2` deliberately does not prune; +see lean/PRUNED_FINDINGS.md. + +The stop depth is the **zipper's root**, not the map root. `prune_path_internal` +breaks its ascent once the path reaches `root_len`, so an implicit prune cannot +reclaim the zipper's own root even when nothing leads to it any more -- unlike +the explicit `prune_path`, which `Zip.prunePath` models with stop depth `0` +because it was measured rising above the root. A write zipper rooted at `ab` +whose subtrie is emptied therefore keeps `ab`, and the differential harness +compares that. -/ +def tidy : Zip V := z.withTrie (z.trie.prunePath z.root.length z.focus).2 + +/-! ### Why `tidy` is unconditional, which is not obvious + +`remove_branches(prune)` looks like it prunes only where +`node_remove_all_branches` reported a removal, and `remove_val(prune)` returns +early when there was no value -- so one would expect no pruning at a location +that was *already* a dangling tip. Guarding `tidy` on that was measured and is +wrong: with `prune = true`, `node_prune_limit` hands a prune limit *into* +`node_remove_all_branches`, which reclaims the dangling key inside the node and +still reports `false`. That is FINDINGS.md #7 -- the prune flag's in-node effect +-- and it means the crate prunes in nearly all of these cases. Guarding cost +302 divergences in 8000 inputs; not guarding costs 5 in 30000, which are the +cases where the in-node reclamation depends on where the node boundary falls. +See `KNOWN` in lean/differential.py. +-/ + /-- `ZipperWriting::remove_val`: removes the value, leaving the location as a dangling path unless `prune` reclaims it. @@ -154,10 +189,10 @@ its root value becomes the focus value (or clears it), and its branches become the focus's branches. This is `ZipperWriting::graft_map`. -/ def graftMap (m : PathMap V) : Zip V := let t := z.trie.graftBelow z.focus m - z.withTrie <| + (z.withTrie <| match m.valAt [] with | some v => (t.setVal z.focus v).2 - | none => (t.removeVal z.focus).2 + | none => (t.removeVal z.focus).2).tidy /-- `ZipperWriting::graft`: graft the subtrie at `src`'s focus, root value included. -/ def graft (src : Zip V) : Zip V := z.graftMap src.makeMap @@ -246,7 +281,7 @@ def removePrefix (n : Nat) : Bool × Zip V := -- `ascend` now reports how far it got, so "were all `n` bytes removed" is a -- comparison rather than the flag it used to return directly. let (ascended, z1) := z.ascend n - (ascended == n, z1.withTrie (z1.trie.graftBelow z1.focus below)) + (ascended == n, (z1.withTrie (z1.trie.graftBelow z1.focus below)).tidy) /-! ## Algebraic operations @@ -284,7 +319,9 @@ It also short-circuits: when the map has no root node, the node status is returned directly and the value status computed above is discarded — even though the value has already been written. -/ def joinMapInto (m : PathMap V) : AlgStatus × Zip V := - let (valStatus, valWasNone, z1) := + -- `merge` is called with both "was none" flags set, as the crate does, so the + -- second component is carried only for symmetry with the other operations. + let (valStatus, _valWasNone, z1) := match z.val, m.valAt [] with | some sv, some mv => let r := ops.pjoin sv mv @@ -297,19 +334,26 @@ def joinMapInto (m : PathMap V) : AlgStatus × Zip V := | none, none => (AlgStatus.none, true, z) let srcB := (m.removeVal []).2 if srcB.isEmptyMap then - -- Short-circuit, and note the asymmetry with `join_into`: this branch tests + -- Note the asymmetry with `join_into`: this branch tests -- `self.get_focus().is_none()` (does a node exist at all?), not -- `node_is_empty()`. So a *bare* focus reports `Identity` here, where -- `join_into` on the same state reports `None`. - (match z1.entry with - | .bare | .valued _ => AlgStatus.identity - | .absent => AlgStatus.none, z1) + -- + -- The node status is *merged* with the value status rather than returned on + -- its own. It used to be returned directly -- an early `return` that + -- discarded a value the operation had already written -- which is + -- issue #139, fixed by PR #142 (`276fca0`). Both exits of the crate's + -- `join_map_into` now end in the same `merge`. + (AlgStatus.merge + (match z1.entry with + | .bare | .valued _ => AlgStatus.identity + | .absent => AlgStatus.none) valStatus true true, z1) else let selfB := z1.focusNode let r := PathMap.join ops selfB srcB let nodeStatus := if PathMap.beqT ops r selfB then AlgStatus.identity else AlgStatus.element let z2 := if nodeStatus == .identity then z1 else z1.withTrie (z1.trie.graftBelow z1.focus r) - (AlgStatus.merge nodeStatus valStatus true valWasNone, z2) + (AlgStatus.merge nodeStatus valStatus true true, z2) /-- `ZipperWriting::join_into_take`: like `join_into`, but the source subtrie is removed from the source zipper's trie. Returns the updated destination *and* @@ -422,13 +466,13 @@ a value at its focus. The focus value of `self` is never touched. -/ def restrict (src : Zip V) : AlgStatus × Zip V := let srcB := src.focusNode let selfB := z.focusNode - if srcB.isEmptyMap then (.none, z.withTrie (z.trie.removeBelow z.focus)) + if srcB.isEmptyMap then (.none, (z.withTrie (z.trie.removeBelow z.focus)).tidy) else if selfB.isEmptyMap then (.none, z) else let r := PathMap.restrictBelowRoot selfB srcB let st := nodeStatus ops selfB r if st == .identity then (.identity, z) - else (st, z.withTrie (z.trie.graftBelow z.focus r)) + else (st, (z.withTrie (z.trie.graftBelow z.focus r)).tidy) /-- `ZipperWriting::restricting`: the mirror image — fill in `self`'s "stem" paths with the source's subtries. `self`'s subtrie is replaced by the source's, @@ -441,8 +485,8 @@ def restricting (src : Zip V) : Bool × Zip V := -- FINDINGS.md #8. The model specifies the common case. if src.focusNodeIsEmpty then (false, z) else if z.focusNodeIsEmpty then (false, z) - else (true, z.withTrie (z.trie.graftBelow z.focus - (PathMap.restrictBelowRoot src.focusNode z.focusNode))) + else (true, (z.withTrie (z.trie.graftBelow z.focus + (PathMap.restrictBelowRoot src.focusNode z.focusNode))).tidy) /-! ## Collapsing path segments -/ diff --git a/lean/PrunedMain.lean b/lean/PrunedMain.lean new file mode 100644 index 00000000..3018be81 --- /dev/null +++ b/lean/PrunedMain.lean @@ -0,0 +1,91 @@ +import PrunedModel + +/-! +The oracle for the dangling-path-free model. + +One-shot: + + pruned-oracle -- decode and run the file's bytes + pruned-oracle -- read the bytes from stdin + +Resident: + + pruned-oracle --server -- one process, many inputs + +Spawning a fresh process per fuzzer input costs more than running the input +does, so `pruned_differential.py` keeps the oracle resident and feeds it work +over stdin. The protocol matches `differential/src/server.rs`, one command per +line: + + run-input run the decoded bytes, print the trace + quit exit 0 + +The reply is the trace lines, then exactly one terminator line, which is the +only line beginning with `!`: + + !DONE the trace above is complete + !TIMEOUT exceeded + !PANIC malformed command + +`differential/src/bin/pruned_trace.rs` prints the same trace from the real +crate for the same input bytes; `lean/pruned_differential.py` diffs them. + +The timeout argument is parsed and ignored, as in `lean/Main.lean`: no +in-process timeout is reachable from Lean's `IO.asTask`/`IO.hasFinished`, and +the driver has to enforce the deadline from outside regardless, since no +in-process timeout can save a child that has died. The model is total, so it +cannot hang, only be slow. +-/ + +open PrunedModel + +/-- Decode a lowercase/uppercase hex string. -/ +def hexDecode (s : String) : Option ByteArray := + let cs := s.toList + if cs.length % 2 != 0 then none + else + let rec go : List Char → ByteArray → Option ByteArray + | [], acc => some acc + | a :: b :: rest, acc => do + let hi ← a.toString.toNat? |>.orElse fun _ => + "0123456789abcdef".toList.idxOf? a.toLower + let lo ← b.toString.toNat? |>.orElse fun _ => + "0123456789abcdef".toList.idxOf? b.toLower + go rest (acc.push (UInt8.ofNat (hi * 16 + lo))) + | _, _ => none + go cs ByteArray.empty + +/-- The resident command loop. -/ +partial def serve : IO Unit := do + let stdin ← IO.getStdin + let stdout ← IO.getStdout + let rec loop : IO Unit := do + let line ← stdin.getLine + -- `getLine` returns "" only at EOF; a blank line is "\n". + if line.isEmpty then return + let line := line.trimAscii.toString + if line == "quit" then return + let terminator ← + match line.splitOn " " with + | "run-input" :: ms :: rest => + match ms.toNat?, hexDecode (String.intercalate " " rest) with + | some _, some bytes => do + for line in Fuzz.run bytes 256 do + stdout.putStrLn line + pure "!DONE" + | _, _ => pure "!PANIC bad run-input arguments" + | _ => pure s!"!PANIC unknown command: {line}" + stdout.putStrLn terminator + stdout.flush + loop + loop + +def main (args : List String) : IO Unit := do + if args.contains "--server" then + return ← serve + let files := args.filter (fun a => !a.startsWith "--") + let bytes ← match files with + | [] => (← IO.getStdin).readBinToEnd + | path :: _ => IO.FS.readBinFile path + for line in Fuzz.run bytes 256 do + IO.println line diff --git a/lean/PrunedModel.lean b/lean/PrunedModel.lean new file mode 100644 index 00000000..4e194c3d --- /dev/null +++ b/lean/PrunedModel.lean @@ -0,0 +1,8 @@ +import PrunedModel.Canon +import PrunedModel.Map +import PrunedModel.Zipper +import PrunedModel.Write +import PrunedModel.Spec +import PrunedModel.Lattice +import PrunedModel.Nested +import PrunedModel.Fuzz diff --git a/lean/PrunedModel/Canon.lean b/lean/PrunedModel/Canon.lean new file mode 100644 index 00000000..8a42e8f3 --- /dev/null +++ b/lean/PrunedModel/Canon.lean @@ -0,0 +1,453 @@ +import PathMapModel.Basic + +/-! +# Canonical association lists + +`PrunedMap` carries its canonical form in its *type*: an entry list sorted +strictly by key, so there is no junk inhabitant to exclude afterwards. This file +is the list-level development that makes that possible — everything needed to +build the proof field and to read it back off, with no mention of `PrunedMap`. + +Two predicates, and the first implies the second: + +* `SortedKeys` — keys strictly increasing in `Path.lt`. This is the invariant. +* `DistinctKeys` — no key bound twice. Implied, because `Path.lt` is + irreflexive; `distinctKeys_of_sortedKeys` is the proof. + +The payoff is `eq_of_sortedKeys_of_lookup`: a sorted list is determined by its +lookup function. That is what makes `PrunedMap` equality *observational*, and +hence what lets `PrunedModel/Lattice.lean` state the lattice laws as equations +with no side conditions at all. + +These proofs were the first and last thirds of `Lattice.lean`, behind a +`Canonical` predicate every law had to carry as a hypothesis. Moving the +invariant into the type removed the hypothesis; the proofs are unchanged. +-/ + +namespace PrunedModel + +open PathMapModel + +variable {V : Type} + +/-! ## Paths and lookup -/ + +/-- Every path is a prefix of itself. -/ +theorem isPrefixOf_self : ∀ p : Path, (p ≼ p) = true + | [] => rfl + | _ :: as => by simp [Path.isPrefixOf, isPrefixOf_self as] + +/-- A key is bound: `lookup` finds whatever `map (·.1)` saw. -/ +theorem lookup_isSome_of_mem_keys {l : List (Path × V)} {p : Path} + (h : p ∈ l.map (·.1)) : (l.lookup p).isSome = true := by + obtain ⟨kv, hmem, heq⟩ := List.mem_map.mp h + exact List.lookup_isSome_iff.mpr ⟨kv, hmem, by simp [heq]⟩ + +/-- …and conversely, `lookup` only succeeds on a key. -/ +theorem mem_keys_of_lookup_isSome {l : List (Path × V)} {p : Path} + (h : (l.lookup p).isSome = true) : p ∈ l.map (·.1) := by + obtain ⟨kv, hmem, hb⟩ := List.lookup_isSome_iff.mp h + exact List.mem_map.mpr ⟨kv, hmem, (eq_of_beq hb).symm⟩ + +/-- An unbound key looks up to `none` — the contrapositive of +`mem_keys_of_lookup_isSome`. -/ +theorem lookup_eq_none_of_not_mem_keys {l : List (Path × V)} {k : Path} + (h : k ∉ l.map (·.1)) : l.lookup k = none := by + cases hl : l.lookup k with + | none => rfl + | some v => + exact absurd (mem_keys_of_lookup_isSome (l := l) (p := k) (by rw [hl]; rfl)) h + +/-! ## Canonicalisation -/ + +/-- Deduplicate an association list, keeping the *first* binding for each key. +Left-biased, matching `pathmap`'s `Identity(SELF_IDENT)` value instances. -/ +def dedupVals (l : List (Path × V)) : List (Path × V) := + l.foldl (fun acc kv => if acc.any (fun x => x.1 == kv.1) then acc else acc ++ [kv]) [] + +/-- Insert into a key-sorted association list (assumes the key is not present). -/ +def insertValSorted (kv : Path × V) : List (Path × V) → List (Path × V) + | [] => [kv] + | kv' :: rest => + if Path.lt kv.1 kv'.1 then kv :: kv' :: rest + else kv' :: insertValSorted kv rest + +/-- Canonicalise a raw association list: keep the first binding per key, sort by key. -/ +def normVals (l : List (Path × V)) : List (Path × V) := + (dedupVals l).foldl (fun acc kv => insertValSorted kv acc) [] + +/-! ## Canonicalisation moves no lookup -/ + +/-- `dedupVals` keeps the first binding for each key, so it moves no lookup. +Stated with an accumulator, which is what lets the `foldl` be inducted on. -/ +private theorem lookup_dedupAux (k : Path) : + ∀ (l acc : List (Path × V)), + (l.foldl (fun acc kv => if acc.any (fun x => x.1 == kv.1) then acc else acc ++ [kv]) acc).lookup k + = (acc.lookup k).or (l.lookup k) + | [], acc => by simp + | (key, val) :: rest, acc => by + rw [List.foldl_cons, lookup_dedupAux k rest] + cases hany : acc.any (fun x => x.1 == key) with + | true => + -- `key` is already bound, so the entry is dropped and `acc` answers for it. + simp only [if_pos, List.lookup_cons] + cases hk : k == key with + | false => simp + | true => + -- `acc.lookup k` is `some`, so it absorbs whatever comes after. + obtain ⟨p, hp, hpk⟩ := List.any_eq_true.mp hany + have hsome : (acc.lookup k).isSome = true := by + refine List.lookup_isSome_iff.mpr ⟨p, hp, ?_⟩ + have h1 : k = key := by simpa using hk + have h2 : p.1 = key := by simpa using hpk + simp [h1, h2] + cases hs : acc.lookup k with + | none => simp [hs] at hsome + | some v => simp + | false => + -- `key` is new, so the entry is appended and `lookup` sees it after `acc`. + simp only [if_neg, Bool.false_eq_true, not_false_eq_true] + cases hk : k == key <;> + simp [List.lookup_append, List.lookup_cons, hk] + +/-- `dedupVals` preserves every lookup. -/ +theorem lookup_dedupVals (l : List (Path × V)) (k : Path) : + (dedupVals l).lookup k = l.lookup k := by + rw [dedupVals] + simpa using lookup_dedupAux k l [] + +/-- Which keys `insertValSorted` leaves behind: the inserted one, and the old ones. -/ +theorem mem_keys_insertValSorted (kv : Path × V) : + ∀ (acc : List (Path × V)) (k : Path), + k ∈ (insertValSorted kv acc).map (·.1) ↔ (k = kv.1 ∨ k ∈ acc.map (·.1)) + | [], k => by simp [insertValSorted] + | kv' :: rest, k => by + rw [insertValSorted] + cases h : Path.lt kv.1 kv'.1 with + | true => simp + | false => + simp only [Bool.false_eq_true, if_false, List.map_cons, List.mem_cons, + mem_keys_insertValSorted kv rest k] + constructor + · intro hm + rcases hm with hm | hm | hm + · exact Or.inr (Or.inl hm) + · exact Or.inl hm + · exact Or.inr (Or.inr hm) + · intro hm + rcases hm with hm | hm | hm + · exact Or.inr (Or.inl hm) + · exact Or.inl hm + · exact Or.inr (Or.inr hm) + +/-- `insertValSorted` is a lookup update, as long as the key is not already +bound. That hypothesis is what rules out shadowing an existing binding, and it +is exactly what `dedupVals` establishes before the sort runs. -/ +theorem lookup_insertValSorted : + ∀ (kv : Path × V) (acc : List (Path × V)) (k : Path), kv.1 ∉ acc.map (·.1) → + (insertValSorted kv acc).lookup k = if k == kv.1 then some kv.2 else acc.lookup k + | (key, val), [], k, _ => by + cases hk : k == key <;> simp [insertValSorted, List.lookup_cons, hk] + | (key, val), (key', val') :: rest, k, hfresh => by + have hne : key ≠ key' := by intro h; exact hfresh (by simp [h]) + have hrest : key ∉ rest.map (·.1) := fun h => hfresh (by simp [h]) + rw [insertValSorted] + cases h : Path.lt key key' with + | true => cases hk : k == key <;> simp [List.lookup_cons, hk] + | false => + simp only [Bool.false_eq_true, if_false, List.lookup_cons, + lookup_insertValSorted (key, val) rest k hrest] + cases hk : k == key with + | false => simp + | true => + -- `k` is the inserted key, and `key'` is a different one, so the + -- existing head is skipped rather than answering for `k`. + have h1 : k = key := by simpa using hk + have : (k == key') = false := by simp [h1, hne] + simp [this] + + +/-- No key bound twice. Spelled recursively rather than as `List.Nodup ∘ map`, +because every proof below inducts on the list and this shape is what the +induction wants. Implied by `SortedKeys`; see `distinctKeys_of_sortedKeys`. -/ +def DistinctKeys : List (Path × V) → Prop + | [] => True + | kv :: rest => kv.1 ∉ rest.map (·.1) ∧ DistinctKeys rest + +/-- Appending a fresh key to a distinct-keyed list keeps it distinct. -/ +theorem distinctKeys_append_singleton : + ∀ (acc : List (Path × V)) (kv : Path × V), + DistinctKeys acc → kv.1 ∉ acc.map (·.1) → DistinctKeys (acc ++ [kv]) + | [], kv, _, _ => ⟨by simp, trivial⟩ + | kv' :: rest, kv, hacc, hfresh => by + refine ⟨?_, distinctKeys_append_singleton rest kv hacc.2 (fun h => hfresh (by simp [h]))⟩ + intro hm + -- the goal arrives with `List.append`, which `map_append` does not match + simp only [List.append_eq, List.map_append, List.mem_append, + List.map_cons, List.map_nil, List.mem_singleton] at hm + rcases hm with hm | hm + · exact hacc.1 hm + · exact hfresh (by simp [show kv'.1 = kv.1 by simpa using hm]) + +private theorem distinctKeys_dedupAux : + ∀ (l acc : List (Path × V)), DistinctKeys acc → + DistinctKeys (l.foldl (fun acc kv => if acc.any (fun x => x.1 == kv.1) then acc else acc ++ [kv]) acc) + | [], acc, h => h + | kv :: rest, acc, h => by + rw [List.foldl_cons] + cases hany : acc.any (fun x => x.1 == kv.1) with + | true => simpa [hany] using distinctKeys_dedupAux rest acc h + | false => + have hfresh : kv.1 ∉ acc.map (·.1) := by + intro hm + obtain ⟨p, hp, hpe⟩ := List.mem_map.mp hm + have : (acc.any (fun x => x.1 == kv.1)) = true := + List.any_eq_true.mpr ⟨p, hp, by simp [hpe]⟩ + rw [hany] at this; exact Bool.noConfusion this + simpa [hany] using + distinctKeys_dedupAux rest _ (distinctKeys_append_singleton acc kv h hfresh) + +/-- `dedupVals` leaves no key bound twice. -/ +theorem distinctKeys_dedupVals (l : List (Path × V)) : DistinctKeys (dedupVals l) := by + rw [dedupVals]; exact distinctKeys_dedupAux l [] trivial + +/-- The insertion sort moves no lookup either, given distinct keys to start from. + +The two hypotheses are what make the *last* insertion win in `insertValSorted` +agree with the *first* binding won by `lookup`: with distinct keys there is only +one of each. -/ +private theorem lookup_sortAux (k : Path) : + ∀ (ds acc : List (Path × V)), DistinctKeys ds → + (∀ x ∈ ds.map (·.1), x ∉ acc.map (·.1)) → + (ds.foldl (fun acc kv => insertValSorted kv acc) acc).lookup k + = (ds.lookup k).or (acc.lookup k) + | [], acc, _, _ => by simp + | kv :: rest, acc, hd, hdisj => by + have hfresh : kv.1 ∉ acc.map (·.1) := hdisj kv.1 (by simp) + have hdisj' : ∀ x ∈ rest.map (·.1), x ∉ (insertValSorted kv acc).map (·.1) := by + intro x hx hmem + rcases (mem_keys_insertValSorted kv acc x).mp hmem with h | h + · exact hd.1 (h ▸ hx) + · exact hdisj x (by simp [hx]) h + rw [List.foldl_cons, lookup_sortAux k rest _ hd.2 hdisj', + lookup_insertValSorted kv acc k hfresh, List.lookup_cons] + cases hk : k == kv.1 with + | true => + have : rest.lookup k = none := + lookup_eq_none_of_not_mem_keys (by + rw [show k = kv.1 by simpa using hk]; exact hd.1) + simp [this] + | false => simp + +/-- **`normVals` preserves every lookup.** Canonicalisation reorders and +deduplicates; it does not change what the list holds anywhere. -/ +theorem lookup_normVals (l : List (Path × V)) (k : Path) : + (normVals l).lookup k = l.lookup k := by + rw [normVals, lookup_sortAux k (dedupVals l) [] (distinctKeys_dedupVals l) (by simp)] + simp [lookup_dedupVals] + +/-! ## List comprehensions keyed by their own elements -/ + +/-- `lookup` into a list comprehension keyed by its own elements. -/ +theorem lookup_filterMap_self (f : Path → Option V) : + ∀ (l : List Path) (k : Path), + ((l.filterMap fun x => (f x).map (Prod.mk x)).lookup k) = if k ∈ l then f k else none + | [], k => by simp + | x :: rest, k => by + rw [List.filterMap_cons] + cases hfx : f x with + | none => + simp only [Option.map_none, List.mem_cons, + lookup_filterMap_self f rest k] + by_cases hkx : k = x + · simp [hkx, hfx] + · simp [hkx] + | some v => + simp only [Option.map_some, List.lookup_cons, List.mem_cons, + lookup_filterMap_self f rest k] + cases hk : k == x with + | true => simp [show k = x by simpa using hk, hfx] + | false => simp [show ¬ (k = x) by simpa using hk] + +/-- `Path.insertSorted` adds the inserted path and keeps the rest. -/ +theorem Path.mem_insertSorted (p : Path) : + ∀ (acc : List Path) (x : Path), x ∈ Path.insertSorted p acc ↔ (x = p ∨ x ∈ acc) + | [], x => by simp [Path.insertSorted] + | q :: qs, x => by + rw [Path.insertSorted] + cases hpq : p == q with + | true => + have hpq' : p = q := by simpa using hpq + simp only [if_pos, List.mem_cons] + constructor + · intro h; exact Or.inr h + · intro h + rcases h with h | h + · exact Or.inl (by rw [h, hpq']) + · exact h + | false => + cases hlt : Path.lt p q with + | true => simp + | false => + simp only [Bool.false_eq_true, if_false, List.mem_cons, + Path.mem_insertSorted p qs x] + constructor + · intro h + rcases h with h | h | h + · exact Or.inr (Or.inl h) + · exact Or.inl h + · exact Or.inr (Or.inr h) + · intro h + rcases h with h | h | h + · exact Or.inr (Or.inl h) + · exact Or.inl h + · exact Or.inr (Or.inr h) + +private theorem Path.mem_sortAux : + ∀ (ps acc : List Path) (x : Path), + x ∈ ps.foldl (fun acc p => Path.insertSorted p acc) acc ↔ (x ∈ ps ∨ x ∈ acc) + | [], acc, x => by simp + | p :: rest, acc, x => by + rw [List.foldl_cons, Path.mem_sortAux rest _ x, Path.mem_insertSorted] + simp only [List.mem_cons] + constructor + · intro h + rcases h with h | h | h + · exact Or.inl (Or.inr h) + · exact Or.inl (Or.inl h) + · exact Or.inr h + · intro h + rcases h with (h | h) | h + · exact Or.inr (Or.inl h) + · exact Or.inl h + · exact Or.inr (Or.inr h) + +/-- Sorting and deduplicating a path list keeps exactly its members. -/ +theorem Path.mem_sortDedup (ps : List Path) (x : Path) : + x ∈ Path.sortDedup ps ↔ x ∈ ps := by + rw [Path.sortDedup] + simpa using Path.mem_sortAux ps [] x + +/-! ## Sortedness, and the uniqueness of the canonical form -/ + +/-- Entry keys strictly increasing. Strictness folds distinctness in, so this +one predicate is the whole canonical-form invariant. -/ +def SortedKeys : List (Path × V) → Prop + | [] => True + | kv :: rest => (∀ x ∈ rest.map (·.1), Path.lt kv.1 x = true) ∧ SortedKeys rest + +/-- A path strictly below every key of a list is not one of them. -/ +theorem notMem_keys_of_all_lt {l : List (Path × V)} {k : Path} + (h : ∀ x ∈ l.map (·.1), Path.lt k x = true) : k ∉ l.map (·.1) := by + intro hm + have := h k hm + rw [Path.lt_irrefl] at this + exact Bool.noConfusion this + +/-- …so it looks up to nothing. -/ +theorem lookup_eq_none_of_all_lt {l : List (Path × V)} {k : Path} + (h : ∀ x ∈ l.map (·.1), Path.lt k x = true) : l.lookup k = none := + lookup_eq_none_of_not_mem_keys (notMem_keys_of_all_lt h) + +/-- A sorted list's head key is below every key after it, and so is anything +below the head key. -/ +theorem all_lt_of_lt_head {kv : Path × V} {rest : List (Path × V)} {k : Path} + (hs : SortedKeys (kv :: rest)) (hlt : Path.lt k kv.1 = true) : + ∀ x ∈ (kv :: rest).map (·.1), Path.lt k x = true := by + intro x hx + simp only [List.map_cons, List.mem_cons] at hx + rcases hx with hx | hx + · exact hx ▸ hlt + · exact Path.lt_trans hlt (hs.1 x hx) + +theorem sortedKeys_insertValSorted : + ∀ (kv : Path × V) (acc : List (Path × V)), SortedKeys acc → kv.1 ∉ acc.map (·.1) → + SortedKeys (insertValSorted kv acc) + | kv, [], _, _ => ⟨by simp, trivial⟩ + | kv, kv' :: rest, hs, hfresh => by + have hne : kv.1 ≠ kv'.1 := fun h => hfresh (by simp [h]) + have hrest : kv.1 ∉ rest.map (·.1) := fun h => hfresh (by simp [h]) + rw [insertValSorted] + cases hlt : Path.lt kv.1 kv'.1 with + | true => + exact ⟨all_lt_of_lt_head hs hlt, hs⟩ + | false => + -- not below `kv'`, and not equal to it, so strictly above it + have hgt : Path.lt kv'.1 kv.1 = true := by + rcases Path.lt_total kv.1 kv'.1 with h | h | h + · rw [h] at hlt; exact Bool.noConfusion hlt + · exact absurd h hne + · exact h + refine ⟨?_, sortedKeys_insertValSorted kv rest hs.2 hrest⟩ + intro x hx + rcases (mem_keys_insertValSorted kv rest x).mp hx with hx | hx + · exact hx ▸ hgt + · exact hs.1 x hx + +private theorem sortedKeys_sortAux : + ∀ (ds acc : List (Path × V)), DistinctKeys ds → SortedKeys acc → + (∀ x ∈ ds.map (·.1), x ∉ acc.map (·.1)) → + SortedKeys (ds.foldl (fun acc kv => insertValSorted kv acc) acc) + | [], acc, _, hs, _ => hs + | kv :: rest, acc, hd, hs, hdisj => by + have hfresh : kv.1 ∉ acc.map (·.1) := hdisj kv.1 (by simp) + have hdisj' : ∀ x ∈ rest.map (·.1), x ∉ (insertValSorted kv acc).map (·.1) := by + intro x hx hmem + rcases (mem_keys_insertValSorted kv acc x).mp hmem with h | h + · exact hd.1 (h ▸ hx) + · exact hdisj x (by simp [hx]) h + rw [List.foldl_cons] + exact sortedKeys_sortAux rest _ hd.2 (sortedKeys_insertValSorted kv acc hs hfresh) hdisj' + +/-- Canonicalisation really does canonicalise. -/ +theorem sortedKeys_normVals (l : List (Path × V)) : SortedKeys (normVals l) := by + rw [normVals] + exact sortedKeys_sortAux (dedupVals l) [] (distinctKeys_dedupVals l) trivial (by simp) + +/-- **The canonical form is unique.** Two sorted entry lists with the same +lookup are the same list. -/ +theorem eq_of_sortedKeys_of_lookup : + ∀ (l₁ l₂ : List (Path × V)), SortedKeys l₁ → SortedKeys l₂ → + (∀ k, l₁.lookup k = l₂.lookup k) → l₁ = l₂ + | [], [], _, _, _ => rfl + | [], (k₂, v₂) :: r₂, _, _, h => by + have := h k₂; simp at this + | (k₁, v₁) :: r₁, [], _, _, h => by + have := h k₁; simp at this + | (k₁, v₁) :: r₁, (k₂, v₂) :: r₂, hs₁, hs₂, h => by + -- Neither head key can be the smaller one, so they are equal. + have hkey : k₁ = k₂ := by + rcases Path.lt_total k₁ k₂ with hlt | heq | hgt + · exact absurd (h k₁) (by + rw [lookup_eq_none_of_all_lt (all_lt_of_lt_head hs₂ hlt)] + simp) + · exact heq + · exact absurd (h k₂) (by + rw [lookup_eq_none_of_all_lt (all_lt_of_lt_head hs₁ hgt)] + simp) + subst hkey + have hval : v₁ = v₂ := by + have := h k₁; simp at this; exact this + subst hval + -- The tails then agree everywhere: at `k₁` both are `none` by strictness. + have htail : r₁ = r₂ := by + refine eq_of_sortedKeys_of_lookup r₁ r₂ hs₁.2 hs₂.2 (fun k => ?_) + by_cases hk : k = k₁ + · subst hk + rw [lookup_eq_none_of_not_mem_keys (notMem_keys_of_all_lt hs₁.1), + lookup_eq_none_of_not_mem_keys (notMem_keys_of_all_lt hs₂.1)] + · have := h k + simp only [List.lookup_cons, show (k == k₁) = false by simp [hk]] at this + exact this + rw [htail] + +/-- **Sorted implies distinct.** `SortedKeys` asks each key to be *strictly* +below every key after it, and `Path.lt` is irreflexive, so no key can appear +twice. One predicate therefore carries the whole canonical-form invariant, which +is why `PrunedMap` needs only the single proof field. -/ +theorem distinctKeys_of_sortedKeys : + ∀ {l : List (Path × V)}, SortedKeys l → DistinctKeys l + | [], _ => trivial + | _ :: _, hs => ⟨notMem_keys_of_all_lt hs.1, distinctKeys_of_sortedKeys hs.2⟩ + +end PrunedModel diff --git a/lean/PrunedModel/Fuzz.lean b/lean/PrunedModel/Fuzz.lean new file mode 100644 index 00000000..222aaa24 --- /dev/null +++ b/lean/PrunedModel/Fuzz.lean @@ -0,0 +1,551 @@ +import PrunedModel.Spec + +/-! +# Differential-fuzzing front end for the dangling-path-free subset + +This module turns `PrunedModel` into an **oracle**: it decodes a raw fuzzer +input into a program over two maps and two zippers, runs it, and emits a trace. +`differential/src/pruned.rs` decodes the *same bytes* with the *same* rules and +emits the *same* trace format from the real crate, so a behavioural divergence +is a textual diff. `lean/pruned_differential.py` drives the pair. + +## How this differs from `PathMapModel.Fuzz` + +That harness explores the whole zipper API and reproduces whatever `pathmap` +does with dangling paths, including the parts nobody wants. Its prune flags are +therefore pinned to `false` and compared against nothing, because the flag's +effect is a function of where an internal node boundary happens to fall. + +This one explores a smaller API and makes a stronger claim about it. Three +restrictions define the subset: + +1. **No `create_path`.** Its whole purpose is a location with no value. +2. **`prune = true` everywhere.** Removal here is inherently pruning: a chain + that exists only to reach a value goes when the value does. `prune_path` and + `prune_ascend` stay in the table as *assertions* — the model says `0`, so a + non-zero count from the crate means something in the subset leaked a dangling + path for it to find. +3. **The write zipper is rooted at the map root.** A write zipper rooted below + it holds a node at its own root, which survives as a location leading nowhere + once everything beneath is removed, and `prune_path` is documented not to rise + above the zipper's origin. That is outside the model by construction rather + than by a bug. Off-root *writing* is still covered: the root-rooted zipper + reaches every focus with `descend_to`. + +The read zipper may be rooted anywhere that exists. Its root is decoded as a +path and then clamped to its longest existing prefix, so it is never a location +the seeding did not create — a read zipper whose root does not exist can walk +out of it (FINDINGS.md #3), which would contaminate every other comparison. + +Operations that *can* still leave a dangling path in `pathmap` 0.4.0 are +specified, not skipped. `graft` of an empty source is the clearest: the focus +loses its value and its branches, so the model removes it and the chain above +it, while the crate leaves both behind. Producing those divergences is what +this harness is for. + +## Wire format + +The input is consumed one byte at a time; decoding stops, and the program ends, +as soon as the input runs out. + +``` +header: + n := u8 % 8 -- entries seeded into map0 (the write target) + n × ( len := u8 % 6 ; len × pathbyte ; val := u8 ) + n := u8 % 8 -- entries seeded into map1 (the read source) + n × ( len := u8 % 6 ; len × pathbyte ; val := u8 ) + r1 := u8 % 4 ; r1 × pathbyte -- read zipper root, clamped to its + -- longest existing prefix +body: + repeated: op := u8 % 54 ; operands per op (see `step`) +``` + +Every **path byte** is masked to `b % 4`, so generated tries share prefixes +heavily — that is where the interesting shapes (branch points, single-child +runs, chains that exist only to reach one value) live. + +## Trace format + +One line per operation: + +``` + ret= W= o e<0|1> v c n f R=<...> +``` + +followed by a dump of both maps. Values are decimal, paths lowercase hex, `e` +is `path_exists`, `c` is `child_count`, `n` is `val_count`. A location with no +value renders as `-`, so a dangling path the crate left behind shows up in the +dump as an entry the model does not have. +-/ + +namespace PrunedModel +namespace Fuzz + +open PathMapModel + +/-- The value type the harness uses: `PathMap`. -/ +abbrev V := UInt64 +/-- The `Lattice`/`DistributiveLattice` instance `pathmap` provides for `u64`. -/ +def ops : ValOps V := u64Ops + +/-! ## Skip reasons + +Why an operation was skipped. Every `skip` in the trace carries one, so a +skipped op says which rule declined it. `differential/src/pruned.rs` emits the +same tokens; the two must agree exactly or every input with a skip diverges. + +Note which reasons from `PathMapModel.Fuzz` are *absent*: `skip:act` (there is +one read source here), `skip:off-root-prune` (the write zipper is always at the +map root, so the prune count is well-defined), and `skip:quarantined` +(`graft_child_maps` is not in this table at all). -/ + +/-- `to_next`/`to_prev_sibling_byte` at the zipper root, where the native read +zipper escapes its own root. -/ +def skipAtRoot : String := "skip:at-root" +/-- A degenerate `k = 0` on `join_k_path_into` / `meet_k_path_into`. -/ +def skipK0 : String := "skip:k0" +/-- The focus has nothing below it, where the op's behaviour is a function of +node materialisation rather than of trie state. -/ +def skipEmptyFocus : String := "skip:empty-focus" +/-- `insert_prefix("")`, which destroys the subtrie. -/ +def skipEmptyPath : String := "skip:empty-path" + +/-! ## Rendering -/ + +def hexDigit (n : Nat) : Char := + if n < 10 then Char.ofNat (48 + n) else Char.ofNat (87 + n) + +def hexByte (b : UInt8) : String := + let n := b.toNat + String.ofList [hexDigit (n / 16), hexDigit (n % 16)] + +def hexPath (p : Path) : String := + if p.isEmpty then "_" else String.join (p.map hexByte) + +/-- The byte a movement operation moved to, or `-` for "did not move". -/ +def showByteOpt : Option UInt8 → String + | none => "-" + | some b => hexByte b + +def showVal : Option V → String + | none => "-" + | some v => toString v.toNat + +def showBool (b : Bool) : String := if b then "1" else "0" + +/-- One location of a dump: its path, relative to `root`, and its value. -/ +def showEntry (t : PrunedMap V) (root : Path) (q : Path) : String := + hexPath q ++ ":" ++ showVal (t.valAt (root ++ q)) + +/-- All locations at and below `root`, depth-first, capped so a runaway trie +cannot make the trace unbounded. + +Every entry here *should* carry a value or lead to one. An entry rendering `-` +with nothing below it is a dangling path, which is the divergence this harness +exists to find. -/ +def dumpAt (t : PrunedMap V) (root : Path) : String := + let qs := (t.subtrie root).paths.take 64 + String.intercalate "," (qs.map (showEntry t root)) + +/-! ## Decoder -/ + +/-- A cursor over the fuzzer's input bytes. -/ +structure Dec where + bytes : ByteArray + pos : Nat + +/-- Read one byte; `none` once the input is exhausted, which ends the program. -/ +def Dec.u8 (d : Dec) : Option (UInt8 × Dec) := + if h : d.pos < d.bytes.size then some (d.bytes[d.pos]'h, { d with pos := d.pos + 1 }) + else none + +/-- Read one byte reduced modulo `m`. -/ +def Dec.mod (d : Dec) (m : Nat) : Option (Nat × Dec) := + d.u8.map (fun (b, d') => (if m == 0 then 0 else b.toNat % m, d')) + +/-- Read one *path* byte. Masked to a 4-letter alphabet so generated tries +share prefixes and actually branch. -/ +def Dec.pathByte (d : Dec) : Option (UInt8 × Dec) := + d.u8.map (fun (b, d') => (UInt8.ofNat (b.toNat % 4), d')) + +/-- Read `n` path bytes. -/ +def Dec.pathN (d : Dec) : Nat → Option (Path × Dec) + | 0 => some ([], d) + | n + 1 => do + let (b, d) ← d.pathByte + let (rest, d) ← d.pathN n + some (b :: rest, d) + +/-- Read a length-prefixed path (`len := u8 % lim`). -/ +def Dec.path (d : Dec) (lim : Nat := 6) : Option (Path × Dec) := do + let (n, d) ← d.mod lim + d.pathN n + +/-- Read a boolean (`u8 % 2`). -/ +def Dec.bool (d : Dec) : Option (Bool × Dec) := + d.u8.map (fun (b, d') => (b.toNat % 2 == 1, d')) + +/-! ## Interpreter state -/ + +/-- Two maps, two zippers: `wz` writes into map0 and is rooted at its root, `rz` +reads map1. Keeping the read source in a separate map is what lets the real +crate hold both zippers at once. -/ +structure St where + wz : PZip V + rz : PZip V + out : List String + step : Nat + +/-- The per-step fingerprint of one zipper. -/ +def fingerprint (z : PZip V) : String := + hexPath z.path ++ " o" ++ hexPath z.focus ++ + " e" ++ showBool z.pathExists ++ + " v" ++ showVal z.val ++ " c" ++ toString z.childCount ++ + " n" ++ toString z.valCount ++ + -- `focus_byte` is unspecified at the root, so it is only compared below it. + " f" ++ (if z.atRoot then "?" else showByteOpt z.focusByte) + +def emit (s : St) (name : String) (ret : String) : St := + { s with + out := (toString s.step ++ " " ++ name ++ " ret=" ++ ret ++ + " W=" ++ fingerprint s.wz ++ " R=" ++ fingerprint s.rz) :: s.out + step := s.step + 1 } + +/-! ## The operation table + +`op % nops` selects the operation. Ops `0`–`29` act on a target zipper chosen +by a following `u8 % 2` byte (`0` = write zipper, `1` = read zipper); ops +`30`–`53` are write-zipper operations. -/ + +/-- Number of distinct operations. Must match `NOPS` in +`differential/src/pruned.rs`. -/ +def nops : Nat := 54 + +/-- 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 +visited. This is the only well-defined way to use the `k`-path primitives: +`k_path_internal` carries iteration state, so calling `to_next_k_path` cold is +flagged by `pathmap`'s own debug assertions. -/ +def kWalk (z : PZip V) (k : Nat) : List Path × PZip V := + let (ok, z1) := z.descendFirstKPath k + if !ok then ([], z1) else go 31 z1 [z1.path] +where + go : Nat → PZip V → List Path → List Path × PZip V + | 0, z, acc => (acc.reverse, z) + | n + 1, z, acc => + let (moved, z') := z.toNextKPath k + if moved then go n z' (z'.path :: acc) else (acc.reverse, z') + +/-- Apply `f` to the zipper selected by `t`. -/ +def onTarget (s : St) (t : Nat) (f : PZip V → α × PZip V) : α × St := + if t == 0 then let (a, z) := f s.wz; (a, { s with wz := z }) + else let (a, z) := f s.rz; (a, { s with rz := z }) + +/-- Apply an observing operation to the zipper selected by `t`. -/ +def onTargetObs (s : St) (t : Nat) (f : PZip V → Bool × Path × PZip V) : Bool × Path × St := + if t == 0 then let (a, o, z) := f s.wz; (a, o, { s with wz := z }) + else let (a, o, z) := f s.rz; (a, o, { s with rz := z }) + +/-- Read the zipper selected by `t`. -/ +def getTarget (s : St) (t : Nat) : PZip V := if t == 0 then s.wz else s.rz + +/-- Decode and run one operation. `none` means the input ran out mid-operation, +which ends the program. -/ +def step (s : St) (d : Dec) : Option (St × Dec) := do + let (opRaw, d) ← d.u8 + let op := opRaw.toNat % nops + match op with + -- ## Movement and reading, on either zipper + | 0 => do let (t, d) ← d.mod 2; let (p, d) ← d.path + let (_, s) := onTarget s t (fun z => ((), z.descendTo p)) + some (emit s "descend_to" (hexPath p), d) + | 1 => do let (t, d) ← d.mod 2; let (b, d) ← d.pathByte + let (_, s) := onTarget s t (fun z => ((), z.descendToByte b)) + some (emit s "descend_to_byte" (hexByte b), d) + | 2 => do let (t, d) ← d.mod 2; let (n, d) ← d.mod 8 + let (r, s) := onTarget s t (fun z => z.ascend n) + some (emit s "ascend" (toString r), d) + | 3 => do let (t, d) ← d.mod 2 + let (r, s) := onTarget s t (fun z => z.ascendByte) + some (emit s "ascend_byte" (showBool r), d) + | 4 => do let (t, d) ← d.mod 2 + let (_, s) := onTarget s t (fun z => ((), z.reset)) + some (emit s "reset" "-", d) + | 5 => do let (t, d) ← d.mod 2 + let (r, s) := onTarget s t (fun z => z.descendFirstByte) + some (emit s "descend_first_byte" (showByteOpt r), d) + | 6 => do let (t, d) ← d.mod 2 + let (r, s) := onTarget s t (fun z => z.descendLastByte) + some (emit s "descend_last_byte" (showByteOpt r), d) + | 7 => do let (t, d) ← d.mod 2; let (i, d) ← d.mod 6 + let (r, s) := onTarget s t (fun z => z.descendIndexedByte i) + some (emit s "descend_indexed_byte" (showByteOpt r), d) + | 8 => do let (t, d) ← d.mod 2 + let (r, s) := onTarget s t (fun z => z.descendUntil) + some (emit s "descend_until" (showBool r), d) + | 9 => do let (t, d) ← d.mod 2 + let (r, s) := onTarget s t (fun z => z.ascendUntil) + some (emit s "ascend_until" (toString r), d) + | 10 => do let (t, d) ← d.mod 2 + let (r, s) := onTarget s t (fun z => z.ascendUntilBranch) + some (emit s "ascend_until_branch" (toString r), d) + | 11 => do let (t, d) ← d.mod 2 + -- Skipped at the zipper root: `ReadZipper::to_next_sibling_byte` + -- escapes its own root there. + if (getTarget s t).atRoot then some (emit s "to_next_sibling_byte" skipAtRoot, d) + else + let (r, s) := onTarget s t (fun z => z.toNextSiblingByte) + some (emit s "to_next_sibling_byte" (showByteOpt r), d) + | 12 => do let (t, d) ← d.mod 2 + if (getTarget s t).atRoot then some (emit s "to_prev_sibling_byte" skipAtRoot, d) + else + let (r, s) := onTarget s t (fun z => z.toPrevSiblingByte) + some (emit s "to_prev_sibling_byte" (showByteOpt r), d) + | 13 => do let (t, d) ← d.mod 2 + let (r, s) := onTarget s t (fun z => z.toNextStep) + some (emit s "to_next_step" (showBool r), d) + | 14 => do let (_t, d) ← d.mod 2 + -- `ZipperIteration` is read-only: the target byte is still + -- consumed, but the operation always applies to the read zipper. + let (r, z) := s.rz.toNextVal + some (emit { s with rz := z } "to_next_val" (showBool r), d) + | 15 => do let (_t, d) ← d.mod 2; let (k, d) ← d.mod 4 + -- `k = 0` is specified: `false`, focus untouched. `kPathFrom` + -- gives that with no special case, since it wants a location + -- strictly after the focus and the only one at depth base+0 is the + -- focus itself. + let (r, z) := s.rz.descendFirstKPath k + some (emit { s with rz := z } "descend_first_k_path" (showBool r), d) + | 16 => do let (_t, d) ← d.mod 2; let (k, d) ← d.mod 4 + -- The op is the whole walk, not one step; see `kWalk`. With + -- `k = 0` the descent fails, so the walk is empty and the + -- never-ending `to_next_k_path(0)` is not reached. + let (ps, z) := kWalk s.rz k + some (emit { s with rz := z } "k_path_walk" + (String.intercalate "," (ps.map hexPath)), d) + | 17 => do let (_t, d) ← d.mod 2 + let (r, z) := s.rz.descendLastPath + some (emit { s with rz := z } "descend_last_path" (showBool r), d) + | 18 => do let (t, d) ← d.mod 2; let (p, d) ← d.path + let (n, s) := onTarget s t (fun z => z.moveToPath p) + some (emit s "move_to_path" (toString n), d) + | 19 => do let (t, d) ← d.mod 2; let (p, d) ← d.path + let (n, s) := onTarget s t (fun z => z.descendToExisting p) + some (emit s "descend_to_existing" (toString n), d) + | 20 => do let (t, d) ← d.mod 2; let (p, d) ← d.path + let (n, s) := onTarget s t (fun z => z.descendToVal p) + some (emit s "descend_to_val" (toString n), d) + | 21 => do let (t, d) ← d.mod 2; let (b, d) ← d.pathByte + let (r, s) := onTarget s t (fun z => z.descendToExistingByte b) + some (emit s "descend_to_existing_byte" (showBool r), d) + | 22 => do let (t, d) ← d.mod 2; let (n, d) ← d.mod 8 + let (r, s) := onTarget s t (fun z => z.descendUntilMaxBytes n) + some (emit s "descend_until_max_bytes" (showBool r), d) + | 23 => do let (t, d) ← d.mod 2; let (p, d) ← d.path + let (r, s) := onTarget s t (fun z => z.descendToCheck p) + some (emit s "descend_to_check" (showBool r), d) + | 24 => do let (t, d) ← d.mod 2; let (p, d) ← d.path + let z := getTarget s t + some (emit s "val_at" (showVal (z.valAt p)), d) + | 25 => do let (t, d) ← d.mod 2 + let z := getTarget s t + some (emit s "make_map_val_count" (toString (z.makeMap.valCount [])), d) + | 26 => do let (t, d) ← d.mod 2 + let z := getTarget s t + some (emit s "dump" (dumpAt z.trie z.focus), d) + | 27 => do let (t, d) ← d.mod 2 + -- The blind-zipper addition: `descend_until` reporting the bytes + -- it descended. The observer's output is a blind zipper's only + -- account of where it went, so it is compared byte for byte. + let (r, obs, s) := onTargetObs s t (fun z => z.descendUntilObserved) + some (emit s "descend_until_observed" (showBool r ++ ":" ++ hexPath obs), d) + | 28 => do let (t, d) ← d.mod 2; let (p, d) ← d.path + -- `ZipperReadOnlyValues::get_val`/`get_val_at` differ from + -- `val`/`val_at` only in the lifetime of the reference they + -- return, so they must give the same answer. `agree` is `1` in + -- the model by construction; a `0` from the crate is the point. + let z := getTarget s t + some (emit s "get_val_agrees" + (showVal z.val ++ ":" ++ showVal (z.valAt p) ++ ":1"), d) + | 29 => do -- `ZipperReadOnlyIteration::to_next_get_val` must advance exactly + -- as `to_next_val` does and hand back the value at the new focus. + let (moved, z) := s.rz.toNextVal + let v := if moved then z.val else none + some (emit { s with rz := z } "to_next_get_val" + (showBool moved ++ ":" ++ showVal v ++ ":1"), d) + -- ## Writing, on the write zipper + | 30 => do let (v, d) ← d.u8 + let (old, z) := s.wz.setVal (UInt64.ofNat v.toNat) + some (emit { s with wz := z } "set_val" (showVal old), d) + | 31 => do let (old, z) := s.wz.removeVal + some (emit { s with wz := z } "remove_val" (showVal old), d) + | 32 => do -- Must be `0`: a trie built from this subset has no dangling tip. + let (n, z) := s.wz.prunePath + some (emit { s with wz := z } "prune_path" (toString n), d) + | 33 => do let (n, z) := s.wz.pruneAscend + some (emit { s with wz := z } "prune_ascend" (toString n), d) + | 34 => do let leaky := s.wz.focusNodeIsEmpty + let (r, z) := s.wz.removeBranches + -- An empty node still comes back as `Some(..)` from + -- `into_option()` for some representations, so `true` gets + -- reported for a removal of nothing. Compared only when there was + -- something below. + some (emit { s with wz := z } "remove_branches" + (if leaky then "?" else showBool r), d) + | 35 => do let (n, d) ← d.mod 4; let (m, d) ← d.pathN n + let z := s.wz.removeUnmaskedBranches (ByteMask.ofList m) + some (emit { s with wz := z } "remove_unmasked_branches" + (hexPath (ByteMask.ofList m)), d) + | 36 => do let z := s.wz.graft s.rz + some (emit { s with wz := z } "graft" "-", d) + | 37 => do let (p, d) ← d.path + let z := s.wz.graftSrcAt s.rz p + some (emit { s with wz := z } "graft_src_at" (hexPath p), d) + | 38 => do let (st, z) := s.wz.joinInto ops s.rz + some (emit { s with wz := z } "join_into" (toString st), d) + | 39 => do let leaky := s.wz.focusNodeIsEmpty + let (st, z) := s.wz.joinMapInto ops s.rz.makeMap + some (emit { s with wz := z } "join_map_into" + (if leaky then "?" else toString st), d) + | 40 => do let (st, z) := s.wz.meetInto ops s.rz + some (emit { s with wz := z } "meet_into" (toString st), d) + | 41 => do let (st, z) := s.wz.subtractInto ops s.rz + some (emit { s with wz := z } "subtract_into" (toString st), d) + | 42 => do let leaky := s.wz.focusNodeIsEmpty + let (st, z) := s.wz.restrict ops s.rz + some (emit { s with wz := z } "restrict" + (if leaky then "?" else toString st), d) + | 43 => do -- Skipped, not merely masked, when either side has nothing below + -- its focus: there `restricting` branches on whether an empty node + -- happens to be materialised, and the two branches differ in + -- *effect*, not just in the reported bool. + if s.wz.focusNodeIsEmpty || s.rz.focusNodeIsEmpty then + some (emit s "restricting" skipEmptyFocus, d) + else + let (r, z) := s.wz.restricting s.rz + some (emit { s with wz := z } "restricting" (showBool r), d) + | 44 => do let (k, d) ← d.mod 4 + -- `join_k_path_into(0)` should be the identity but collapses the + -- subtrie in `pathmap` 0.4.0. + if k == 0 then some (emit s "join_k_path_into" skipK0, d) + else + let (r, z) := s.wz.joinKPathInto ops k + some (emit { s with wz := z } "join_k_path_into" + (if z.focusNodeIsEmpty then "?" else showBool r), d) + | 45 => do let (p, d) ← d.path + -- `insert_prefix("")` destroys the subtrie in `pathmap` 0.4.0. + if p.isEmpty then some (emit s "insert_prefix" skipEmptyPath, d) + else + let (r, z) := s.wz.insertPrefix p + some (emit { s with wz := z } "insert_prefix" (showBool r), d) + | 46 => do let (n, d) ← d.mod 6 + let (r, z) := s.wz.removePrefix n + some (emit { s with wz := z } "remove_prefix" (showBool r), d) + | 47 => do let leaky := s.wz.focusNodeIsEmpty && s.wz.val.isNone + let (m, z) := s.wz.takeMap + if leaky then + some (emit { s with wz := (z.graftMap (m.getD PrunedMap.empty)) } + "take_map_restore" "?", d) + else + match m with + | some mm => some (emit { s with wz := z.graftMap mm } "take_map_restore" "1", d) + | none => some (emit { s with wz := z } "take_map_restore" "0", d) + | 48 => do let (k, d) ← d.mod 4 + -- `meet_k_path_into` is not implementable for these arguments; see + -- `PZip.meetKPathUnspecified`, whose two disjuncts are split out + -- here so the skip names which one fired. + if k == 0 then some (emit s "meet_k_path_into" skipK0, d) + else if s.wz.focusNodeIsEmpty then + some (emit s "meet_k_path_into" skipEmptyFocus, d) + else + let (r, z) := s.wz.meetKPathInto ops k + some (emit { s with wz := z } "meet_k_path_into" (showBool r), d) + | 49 => do let (v, d) ← d.u8 + -- Writing through the reference `get_val_mut` hands back. It must + -- behave like `set_val` where a value exists and do nothing -- + -- crucially, *not* create the path -- where one does not. + let (old, z) := s.wz.getValMutWrite (UInt64.ofNat v.toNat) + some (emit { s with wz := z } "get_val_mut_write" (showVal old), d) + | 50 => do let (v, d) ← d.u8 + let (r, z) := s.wz.getValOrSetMut (UInt64.ofNat v.toNat) + some (emit { s with wz := z } "get_val_or_set_mut" (showVal (some r)), d) + | 51 => do let (v, d) ← d.u8 + -- `ran` records whether the closure was invoked. The contract says + -- it supplies the value "if no value exists", so invoking it when a + -- value is already present is observable to any caller whose + -- closure has a side effect. + let (r, ran, z) := s.wz.getValOrSetMutWith (UInt64.ofNat v.toNat) + some (emit { s with wz := z } "get_val_or_set_mut_with" + (showVal (some r) ++ ":" ++ showBool ran), d) + | 52 => do let (n, d) ← d.mod 4; let (m, d) ← d.pathN n; let (ru, d) ← d.bool + let z := s.wz.graftMaskedBranches s.rz (ByteMask.ofList m) ru + some (emit { s with wz := z } "graft_masked_branches" + (hexPath (ByteMask.ofList m) ++ ":" ++ showBool ru), d) + | 53 => do let (p, d) ← d.path + -- `meet_2` takes two sources; the second is the first moved to `p`. + 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) + | _ => some (emit s "nop" "-", d) + +/-- Run operations until the input is exhausted or `fuel` runs out. -/ +def loop : Nat → St → Dec → St + | 0, s, _ => s + | n + 1, s, d => + match step s d with + | some (s', d') => loop n s' d' + | none => s + +/-! ## Header -/ + +/-- Decode `n` seed entries and insert them into `t`. -/ +def seed (t : PrunedMap V) (d : Dec) : Nat → Option (PrunedMap V × Dec) + | 0 => some (t, d) + | n + 1 => do + let (p, d) ← d.path + let (v, d) ← d.u8 + seed (t.setVal p (UInt64.ofNat v.toNat)).2 d n + +/-- The longest prefix of `p` that exists in `t`. + +The read zipper's root is clamped this way instead of being created, because +`create_path` is not in this subset. A zipper whose root does not exist can +escape it — `to_next_sibling_byte` and `to_next_step` fall back on the parent's +child mask and walk out of the granted subtrie — and that one bug would +contaminate every other comparison. -/ +def clampToExisting (t : PrunedMap V) (p : Path) : Path := + -- Existence is prefix-closed, so the prefixes that exist form an initial + -- segment and the longest one is the answer. + p.take (((List.range (p.length + 1)).filter + (fun j => t.pathExists (p.take j))).getLast?.getD 0) + +/-- Decode the header: two seeded maps and the read zipper's root. The write +zipper is always rooted at the map root; see the module docstring. -/ +def header (d : Dec) : Option (St × Dec) := do + let (n0, d) ← d.mod 8 + let (m0, d) ← seed PrunedMap.empty d n0 + let (n1, d) ← d.mod 8 + let (m1, d) ← seed PrunedMap.empty d n1 + let (r1raw, d) ← d.path 4 + let r1 := clampToExisting m1 r1raw + some ({ wz := { trie := m0, root := [], path := [] } + rz := { trie := m1, root := r1, path := [] } + out := [], step := 0 }, d) + +/-! ## Entry point -/ + +/-- Decode and run a fuzzer input, returning the trace lines. -/ +def run (bytes : ByteArray) (maxSteps : Nat := 256) : List String := + match header { bytes, pos := 0 } with + | none => ["EMPTY"] + | some (s0, d) => + let s := loop maxSteps s0 d + let final := + ("MAP0 " ++ dumpAt s.wz.trie []) :: + ("MAP1 " ++ dumpAt s.rz.trie []) :: + ("ROOT0 " ++ hexPath s.wz.root) :: + ("ROOT1 " ++ hexPath s.rz.root) :: [] + s.out.reverse ++ final + +end Fuzz +end PrunedModel diff --git a/lean/PrunedModel/Lattice.lean b/lean/PrunedModel/Lattice.lean new file mode 100644 index 00000000..bd5f6a6a --- /dev/null +++ b/lean/PrunedModel/Lattice.lean @@ -0,0 +1,496 @@ +import PrunedModel.Spec + +/-! +# The lattice laws + +`PrunedMap.join` and `PrunedMap.meet` are meant to be union and intersection. +This file proves it, in the only form that means anything: the lattice +identities, derived rather than checked on examples. + +## Why here and not in `PathMapModel` + +The laws are *false* for the other model, and instructively so. +`PathMapModel.meet` keeps a location only when it leads to a surviving value, so +a trie with a dangling path does not survive `meet a a` — idempotence fails on +exactly the states `PrunedModel` cannot represent. A specification that +reproduces the crate's dangling-path behaviour cannot also be a lattice. So +these proofs are not a bonus feature of the pruned model; they are only +available because of what it leaves out. + +## Shape of the development + +1. `valAt` sees through `mk'`: `(mk' l).valAt k = l.lookup k`. Everything rests + on this, because every operation is `mk'` of a list comprehension and every + law is then a pointwise statement about `Option V`. +2. `valAt_join` / `valAt_meet` / `valAt_sub`: each operation is *pointwise* on + `valAt`. This is the step that would be false for a model storing locations + separately from values. +3. `ext`: two maps with the same `valAt` everywhere are equal. This needs + `Path.lt` to be a strict total order, proved here, and it is what lets the + laws be stated as equations rather than as pointwise equivalences. +4. The laws for `PrunedMap V`, from a hypothesis bundle on the value operations + that does *not* include commutativity. +5. `PrunedMap Unit`, where the correspondence is exact — a trie over `()` is a + finite set of paths — and commutativity holds. +-/ + +namespace PrunedModel +namespace PrunedMap + +open PathMapModel + +variable {V : Type} + +/-! ## 1. `valAt` sees through `mk'` -/ + +/-- **`valAt` sees through `mk'`.** Canonicalisation reorders and deduplicates; +it does not change what the map holds anywhere. + +Every operation below is `mk'` of a list comprehension, so this is what turns a +statement about tries into a statement about `Option V`. -/ +theorem valAt_mk' (l : List (Path × V)) (k : Path) : (mk' l).valAt k = l.lookup k := + lookup_normVals l k + +/-! ## 2. Every operation is pointwise on `valAt` + +This is the step that would fail for a model storing locations separately from +values: there, what `meet` does at a path depends on what lies *below* it. -/ + +/-- An unbound path holds nothing. -/ +theorem valAt_eq_none_of_not_mem_keys {a : PrunedMap V} {k : Path} + (h : k ∉ a.keys) : a.valAt k = none := + lookup_eq_none_of_not_mem_keys h + +@[simp] theorem valAt_empty (k : Path) : (empty : PrunedMap V).valAt k = none := rfl + +variable (ops : ValOps V) + +/-- **Join is pointwise.** -/ +theorem valAt_join (a b : PrunedMap V) (k : Path) : + (join ops a b).valAt k = joinVal ops (a.valAt k) (b.valAt k) := by + rw [join, valAt_mk', lookup_filterMap_self] + by_cases hk : k ∈ Path.sortDedup (a.keys ++ b.keys) + · simp [hk] + · -- Outside both key lists both sides hold nothing, and `joinVal none none = none`. + have hab : k ∉ a.keys ++ b.keys := fun h => hk ((Path.mem_sortDedup _ k).mpr h) + have ha : a.valAt k = none := + valAt_eq_none_of_not_mem_keys (fun h => hab (List.mem_append.mpr (Or.inl h))) + have hb : b.valAt k = none := + valAt_eq_none_of_not_mem_keys (fun h => hab (List.mem_append.mpr (Or.inr h))) + simp [hk, ha, hb, joinVal] + +/-- **Meet is pointwise.** It enumerates `a`'s keys only, which is sound because +`meetVal none _ = none`: a path `a` does not hold cannot survive a meet. -/ +theorem valAt_meet (a b : PrunedMap V) (k : Path) : + (meet ops a b).valAt k = meetVal ops (a.valAt k) (b.valAt k) := by + rw [meet, valAt_mk', lookup_filterMap_self] + by_cases hk : k ∈ a.keys + · simp [hk] + · simp [hk, valAt_eq_none_of_not_mem_keys hk, meetVal] + +/-! ## 3. The laws + +The hypotheses are on the *value* operations, lifted to `Option V` — which is +the level `valAt_join` and `valAt_meet` hand back, and the level at which a +value type either is or is not a lattice. Commutativity is deliberately not +among them: `pathmap`'s integer instances are left-biased projections +(`pjoin` returns `Identity(SELF_IDENT)` and ignores the counterpart), so +`join` picks the destination's value on a collision and is *not* commutative. +Everything else holds. -/ + +/-- What a value type must satisfy for tries over it to form a distributive +lattice under `join` and `meet`. No commutativity; see `IsCommVals`. -/ +structure IsLatticeVals {V : Type} (ops : ValOps V) : Prop where + joinAssoc : ∀ x y z : Option V, + joinVal ops (joinVal ops x y) z = joinVal ops x (joinVal ops y z) + meetAssoc : ∀ x y z : Option V, + meetVal ops (meetVal ops x y) z = meetVal ops x (meetVal ops y z) + joinIdem : ∀ x : Option V, joinVal ops x x = x + meetIdem : ∀ x : Option V, meetVal ops x x = x + joinNone : ∀ x : Option V, joinVal ops x none = x + meetNone : ∀ x : Option V, meetVal ops x none = none + absorbMeetJoin : ∀ x y : Option V, meetVal ops x (joinVal ops x y) = x + absorbJoinMeet : ∀ x y : Option V, joinVal ops x (meetVal ops x y) = x + meetDistribJoin : ∀ x y z : Option V, + meetVal ops x (joinVal ops y z) = joinVal ops (meetVal ops x y) (meetVal ops x z) + joinDistribMeet : ∀ x y z : Option V, + joinVal ops x (meetVal ops y z) = meetVal ops (joinVal ops x y) (joinVal ops x z) + +/-- The *mirrored* absorption law: `meet (join a b) a = a`, with the join on the +left of the meet. + +In a commutative lattice this is `absorbMeetJoin` read backwards and needs no +separate assumption. `pathmap`'s join is not commutative, so the two +orientations are genuinely different statements, and only one of them is a +standard lattice axiom. Nothing in §3 needs this one — it is here because +*nesting* does: `PrunedModel/Nested.lean` lifts the lattice structure to tries +whose values are tries, and the one case of `joinDistribMeet` that no longer +collapses is exactly this law. Both of `pathmap`'s instances satisfy it. -/ +structure IsFlipAbsorb {V : Type} (ops : ValOps V) : Prop where + absorbMeetJoinFlip : ∀ x y : Option V, meetVal ops (joinVal ops x y) x = x + +/-- The extra law a *commutative* value type satisfies. `unitOps` does; +`u64Ops` does not. -/ +structure IsCommVals {V : Type} (ops : ValOps V) : Prop where + joinComm : ∀ x y : Option V, joinVal ops x y = joinVal ops y x + meetComm : ∀ x y : Option V, meetVal ops x y = meetVal ops y x + +variable {ops : ValOps V} + +/-- Two tries hold the same thing at every path. The model's observable +equality: `valAt` is the whole interface, and `beqT` — which decides +`AlgebraicStatus::Identity` — agrees with it on canonical maps. -/ +def Agree (a b : PrunedMap V) : Prop := ∀ k, a.valAt k = b.valAt k + +theorem Agree.refl (a : PrunedMap V) : Agree a a := fun _ => rfl +theorem Agree.symm {a b : PrunedMap V} (hab : Agree a b) : Agree b a := fun k => (hab k).symm +theorem Agree.trans {a b c : PrunedMap V} (hab : Agree a b) (hbc : Agree b c) : Agree a c := + fun k => (hab k).trans (hbc k) + +/-! ### Associativity -/ + +theorem join_assoc (h : IsLatticeVals ops) (a b c : PrunedMap V) : + Agree (join ops (join ops a b) c) (join ops a (join ops b c)) := by + intro k; simp only [valAt_join]; exact h.joinAssoc _ _ _ + +theorem meet_assoc (h : IsLatticeVals ops) (a b c : PrunedMap V) : + Agree (meet ops (meet ops a b) c) (meet ops a (meet ops b c)) := by + intro k; simp only [valAt_meet]; exact h.meetAssoc _ _ _ + +/-! ### Idempotence -/ + +theorem join_idem (h : IsLatticeVals ops) (a : PrunedMap V) : Agree (join ops a a) a := by + intro k; rw [valAt_join]; exact h.joinIdem _ + +theorem meet_idem (h : IsLatticeVals ops) (a : PrunedMap V) : Agree (meet ops a a) a := by + intro k; rw [valAt_meet]; exact h.meetIdem _ + +/-! ### `empty` is the identity of `join` and annihilates `meet` -/ + +theorem join_empty (h : IsLatticeVals ops) (a : PrunedMap V) : Agree (join ops a empty) a := by + intro k; rw [valAt_join, valAt_empty]; exact h.joinNone _ + +theorem meet_empty (h : IsLatticeVals ops) (a : PrunedMap V) : + Agree (meet ops a empty) (empty : PrunedMap V) := by + intro k; rw [valAt_meet, valAt_empty]; exact h.meetNone _ + +/-! ### Absorption -/ + +theorem absorb_meet_join (h : IsLatticeVals ops) (a b : PrunedMap V) : Agree (meet ops a (join ops a b)) a := by + intro k; rw [valAt_meet, valAt_join]; exact h.absorbMeetJoin _ _ + +theorem absorb_join_meet (h : IsLatticeVals ops) (a b : PrunedMap V) : Agree (join ops a (meet ops a b)) a := by + intro k; rw [valAt_join, valAt_meet]; exact h.absorbJoinMeet _ _ + +/-- The mirrored absorption, at trie level. -/ +theorem absorb_meet_join_flip (hf : IsFlipAbsorb ops) (a b : PrunedMap V) : + Agree (meet ops (join ops a b) a) a := by + intro k; rw [valAt_meet, valAt_join]; exact hf.absorbMeetJoinFlip _ _ + +/-! ### Distributivity, both ways -/ + +theorem meet_distrib_join (h : IsLatticeVals ops) (a b c : PrunedMap V) : + Agree (meet ops a (join ops b c)) (join ops (meet ops a b) (meet ops a c)) := by + intro k; simp only [valAt_meet, valAt_join]; exact h.meetDistribJoin _ _ _ + +theorem join_distrib_meet (h : IsLatticeVals ops) (a b c : PrunedMap V) : + Agree (join ops a (meet ops b c)) (meet ops (join ops a b) (join ops a c)) := by + intro k; simp only [valAt_join, valAt_meet]; exact h.joinDistribMeet _ _ _ + +/-! ### Commutativity, where the value type allows it -/ + +theorem join_comm (hc : IsCommVals ops) (a b : PrunedMap V) : + Agree (join ops a b) (join ops b a) := by + intro k; simp only [valAt_join]; exact hc.joinComm _ _ + +theorem meet_comm (hc : IsCommVals ops) (a b : PrunedMap V) : + Agree (meet ops a b) (meet ops b a) := by + intro k; simp only [valAt_meet]; exact hc.meetComm _ _ + +/-! ## 4. The two instances the crate actually provides + +`u64Ops` satisfies everything but commutativity; `unitOps` satisfies +everything. -/ + +/-- `pathmap`'s integer instance gives a distributive lattice. -/ +theorem u64_isLattice : IsLatticeVals u64Ops where + joinAssoc x y z := by + cases x <;> cases y <;> cases z <;> simp [joinVal, u64Ops, ValRes.resolve] + meetAssoc x y z := by + cases x <;> cases y <;> cases z <;> simp [meetVal, u64Ops, ValRes.resolve] + joinIdem x := by cases x <;> simp [joinVal, u64Ops, ValRes.resolve] + meetIdem x := by cases x <;> simp [meetVal, u64Ops, ValRes.resolve] + joinNone x := by cases x <;> simp [joinVal] + meetNone x := by cases x <;> simp [meetVal] + absorbMeetJoin x y := by + cases x <;> cases y <;> simp [joinVal, meetVal, u64Ops, ValRes.resolve] + absorbJoinMeet x y := by + cases x <;> cases y <;> simp [joinVal, meetVal, u64Ops, ValRes.resolve] + meetDistribJoin x y z := by + cases x <;> cases y <;> cases z <;> simp [joinVal, meetVal, u64Ops, ValRes.resolve] + joinDistribMeet x y z := by + cases x <;> cases y <;> cases z <;> simp [joinVal, meetVal, u64Ops, ValRes.resolve] + +/-- …but **not** a commutative one, and this is not an artefact of the model. +`impl Lattice for u64` returns `Identity(SELF_IDENT)` from `pjoin`, ignoring the +counterpart entirely, so a collision resolves to whichever side is `self` — +which is the destination for `join_into` and the source for a join evaluated with +the operands swapped. That is also why `FINDINGS.md`'s "value bias by node +layout" class was a bug worth fixing: with a non-commutative join, *which* +operand ends up on the left is observable. -/ +theorem u64_not_isComm : ¬ IsCommVals u64Ops := by + intro hc + have h12 := hc.joinComm (some 1) (some 2) + simp only [joinVal, u64Ops, ValRes.resolve, Option.some.injEq] at h12 + exact absurd h12 (by decide) + +/-- `u64Ops` satisfies the mirrored absorption too, even though it is not +commutative: a left-biased `pjoin` makes `join x y` agree with `x` wherever `x` +has a value, which is exactly where the meet then looks. -/ +theorem u64_isFlipAbsorb : IsFlipAbsorb u64Ops where + absorbMeetJoinFlip x y := by + cases x <;> cases y <;> simp [joinVal, meetVal, u64Ops, ValRes.resolve] + +/-- `pathmap`'s `()` instance gives a distributive lattice… -/ +theorem unit_isLattice : IsLatticeVals unitOps where + joinAssoc x y z := by + cases x <;> cases y <;> cases z <;> simp [joinVal, unitOps, ValRes.resolve] + meetAssoc x y z := by + cases x <;> cases y <;> cases z <;> simp [meetVal, unitOps, ValRes.resolve] + joinIdem x := by cases x <;> simp [joinVal, unitOps, ValRes.resolve] + meetIdem x := by cases x <;> simp [meetVal, unitOps, ValRes.resolve] + joinNone x := by cases x <;> simp [joinVal] + meetNone x := by cases x <;> simp [meetVal] + absorbMeetJoin x y := by + cases x <;> cases y <;> simp [joinVal, meetVal, unitOps, ValRes.resolve] + absorbJoinMeet x y := by + cases x <;> cases y <;> simp [joinVal, meetVal, unitOps, ValRes.resolve] + meetDistribJoin x y z := by + cases x <;> cases y <;> cases z <;> simp [joinVal, meetVal, unitOps, ValRes.resolve] + joinDistribMeet x y z := by + cases x <;> cases y <;> cases z <;> simp [joinVal, meetVal, unitOps, ValRes.resolve] + +theorem unit_isFlipAbsorb : IsFlipAbsorb unitOps where + absorbMeetJoinFlip x y := by + cases x <;> cases y <;> simp [joinVal, meetVal, unitOps, ValRes.resolve] + +/-- …and a **commutative** one. There is only one value, so there is nothing for +a biased projection to be biased about. -/ +theorem unit_isComm : IsCommVals unitOps where + joinComm x y := by cases x <;> cases y <;> simp [joinVal, unitOps, ValRes.resolve] + meetComm x y := by cases x <;> cases y <;> simp [meetVal, unitOps, ValRes.resolve] + +/-! ## 5. Over `()` the correspondence is exact + +A `PrunedMap Unit` does not merely *satisfy* the set laws — it **is** a finite +set of paths. `Option Unit` has two inhabitants, so `valAt` carries exactly one +bit per path, and `join` and `meet` are that bit's `||` and `&&`. -/ + +/-- A trie over `()` holds no information beyond *which* paths are in it. -/ +theorem unit_valAt_determined (a : PrunedMap Unit) (k : Path) : + a.valAt k = if (a.valAt k).isSome then some () else none := by + cases hv : a.valAt k with + | none => simp + | some u => cases u; simp + +/-- `join` is union of those path sets. -/ +theorem unit_join_isSome (a b : PrunedMap Unit) (k : Path) : + ((join unitOps a b).valAt k).isSome = ((a.valAt k).isSome || (b.valAt k).isSome) := by + rw [valAt_join] + cases a.valAt k <;> cases b.valAt k <;> simp [joinVal, unitOps, ValRes.resolve] + +/-- `meet` is intersection of those path sets. -/ +theorem unit_meet_isSome (a b : PrunedMap Unit) (k : Path) : + ((meet unitOps a b).valAt k).isSome = ((a.valAt k).isSome && (b.valAt k).isSome) := by + rw [valAt_meet] + cases a.valAt k <;> cases b.valAt k <;> simp [meetVal, unitOps, ValRes.resolve] + +/-- `empty` is the empty set. -/ +theorem unit_empty_isSome (k : Path) : + ((empty : PrunedMap Unit).valAt k).isSome = false := by simp + +/-! Every law of §3 therefore holds for `PrunedMap Unit` with no side condition, +commutativity included: `unit_isLattice` and `unit_isComm` discharge the +hypotheses. Concretely, for `a b c : PrunedMap Unit`: + +* `join_assoc unit_isLattice a b c`, `meet_assoc unit_isLattice a b c` +* `join_comm unit_isComm a b`, `meet_comm unit_isComm a b` +* `join_idem unit_isLattice a`, `meet_idem unit_isLattice a` +* `join_empty unit_isLattice a`, `meet_empty unit_isLattice a` +* `absorb_meet_join unit_isLattice a b`, `absorb_join_meet unit_isLattice a b` +* `meet_distrib_join unit_isLattice a b c`, `join_distrib_meet unit_isLattice a b c` + +and the same list for `PrunedMap UInt64` through `u64_isLattice`, minus the two +commutativity laws, which `u64_not_isComm` rules out. + +What is *not* claimed is a Boolean algebra proper: `Path` is infinite, so there +is no top element and hence no complement. What this is, is the lattice of +finite sets of paths — a distributive lattice with a least element. The +relative complement that would make it a *generalized* Boolean algebra is +`PrunedMap.sub`, whose pointwise characterisation needs the canonicity +hypothesis that §1's `DistinctKeys` supplies; it is not proved here. -/ + +/-! ## 6. From "equal at every path" to equal + +`Agree` is the honest observational statement, and here it simply *is* equality. +`PrunedMap` carries sortedness in its type, so a trie is the unique sorted +enumeration of its own contents (`eq_of_sortedKeys_of_lookup`) and the proof +fields are `Prop`s, equal automatically. `PrunedMap.ext` does the work. + +This section used to be a hundred lines and a `Canonical` predicate every law in +§7 carried as a hypothesis. -/ + +/-- **Agreement is equality.** No side condition: there is no non-canonical trie +for one to exclude. -/ +theorem eq_of_agree {a b : PrunedMap V} (hab : Agree a b) : a = b := PrunedMap.ext hab + +/-! ## 7. The laws, as equations + +The same ten laws as §3, now as `=`, and **with no side conditions at all**. + +They used to need `Canonical a` wherever the right-hand side was the bare `a` — +idempotence, the `empty` identity, both absorptions — because the old +representation admitted an entry list binding a key twice, and such a trie is +genuinely not equal to its own join. Carrying sortedness in the type removed the +inhabitant, and with it the hypothesis. -/ + +theorem join_assoc_eq (h : IsLatticeVals ops) (a b c : PrunedMap V) : + join ops (join ops a b) c = join ops a (join ops b c) := + eq_of_agree (join_assoc h a b c) + +theorem meet_assoc_eq (h : IsLatticeVals ops) (a b c : PrunedMap V) : + meet ops (meet ops a b) c = meet ops a (meet ops b c) := + eq_of_agree (meet_assoc h a b c) + +theorem join_idem_eq (h : IsLatticeVals ops) (a : PrunedMap V) : + join ops a a = a := + eq_of_agree (join_idem h a) + +theorem meet_idem_eq (h : IsLatticeVals ops) (a : PrunedMap V) : + meet ops a a = a := + eq_of_agree (meet_idem h a) + +theorem join_empty_eq (h : IsLatticeVals ops) (a : PrunedMap V) : + join ops a empty = a := + eq_of_agree (join_empty h a) + +theorem meet_empty_eq (h : IsLatticeVals ops) (a : PrunedMap V) : + meet ops a empty = (empty : PrunedMap V) := + eq_of_agree (meet_empty h a) + +theorem absorb_meet_join_eq (h : IsLatticeVals ops) (a : PrunedMap V) (b : PrunedMap V) : meet ops a (join ops a b) = a := + eq_of_agree (absorb_meet_join h a b) + +theorem absorb_join_meet_eq (h : IsLatticeVals ops) (a : PrunedMap V) (b : PrunedMap V) : join ops a (meet ops a b) = a := + eq_of_agree (absorb_join_meet h a b) + +theorem absorb_meet_join_flip_eq (hf : IsFlipAbsorb ops) (a : PrunedMap V) (b : PrunedMap V) : meet ops (join ops a b) a = a := + eq_of_agree (absorb_meet_join_flip hf a b) + +theorem meet_distrib_join_eq (h : IsLatticeVals ops) (a b c : PrunedMap V) : + meet ops a (join ops b c) = join ops (meet ops a b) (meet ops a c) := + eq_of_agree (meet_distrib_join h a b c) + +theorem join_distrib_meet_eq (h : IsLatticeVals ops) (a b c : PrunedMap V) : + join ops a (meet ops b c) = meet ops (join ops a b) (join ops a c) := + eq_of_agree (join_distrib_meet h a b c) + +theorem join_comm_eq (hc : IsCommVals ops) (a b : PrunedMap V) : + join ops a b = join ops b a := + eq_of_agree (join_comm hc a b) + +theorem meet_comm_eq (hc : IsCommVals ops) (a b : PrunedMap V) : + meet ops a b = meet ops b a := + eq_of_agree (meet_comm hc a b) + +/-! ### Both instances, named + +Everything above is stated for an abstract `ops` under a hypothesis, so this is +where the two value types the crate provides get their own theorems — citable +rather than merely checked. `PrunedMap Unit` gets all twelve laws; +`PrunedMap UInt64` gets ten, and the two it does not get are *proved* unavailable +below. -/ + +section Instances +variable (a b c : PrunedMap Unit) (x y z : PrunedMap UInt64) + +theorem unit_join_assoc : join unitOps (join unitOps a b) c = join unitOps a (join unitOps b c) := + join_assoc_eq unit_isLattice a b c +theorem unit_meet_assoc : meet unitOps (meet unitOps a b) c = meet unitOps a (meet unitOps b c) := + meet_assoc_eq unit_isLattice a b c +theorem unit_join_comm : join unitOps a b = join unitOps b a := join_comm_eq unit_isComm a b +theorem unit_meet_comm : meet unitOps a b = meet unitOps b a := meet_comm_eq unit_isComm a b +theorem unit_join_idem : join unitOps a a = a := join_idem_eq unit_isLattice a +theorem unit_meet_idem : meet unitOps a a = a := meet_idem_eq unit_isLattice a +theorem unit_join_empty : join unitOps a empty = a := + join_empty_eq unit_isLattice a +theorem unit_meet_empty : meet unitOps a empty = empty := meet_empty_eq unit_isLattice a +theorem unit_absorb_meet_join : meet unitOps a (join unitOps a b) = a := + absorb_meet_join_eq unit_isLattice a b +theorem unit_absorb_join_meet : join unitOps a (meet unitOps a b) = a := + absorb_join_meet_eq unit_isLattice a b +theorem unit_meet_distrib_join : + meet unitOps a (join unitOps b c) = join unitOps (meet unitOps a b) (meet unitOps a c) := + meet_distrib_join_eq unit_isLattice a b c +theorem unit_join_distrib_meet : + join unitOps a (meet unitOps b c) = meet unitOps (join unitOps a b) (join unitOps a c) := + join_distrib_meet_eq unit_isLattice a b c + +theorem u64_join_assoc : join u64Ops (join u64Ops x y) z = join u64Ops x (join u64Ops y z) := + join_assoc_eq u64_isLattice x y z +theorem u64_meet_assoc : meet u64Ops (meet u64Ops x y) z = meet u64Ops x (meet u64Ops y z) := + meet_assoc_eq u64_isLattice x y z +theorem u64_join_idem : join u64Ops x x = x := join_idem_eq u64_isLattice x +theorem u64_meet_idem : meet u64Ops x x = x := meet_idem_eq u64_isLattice x +theorem u64_join_empty : join u64Ops x empty = x := + join_empty_eq u64_isLattice x +theorem u64_meet_empty : meet u64Ops x empty = empty := meet_empty_eq u64_isLattice x +theorem u64_absorb_meet_join : meet u64Ops x (join u64Ops x y) = x := + absorb_meet_join_eq u64_isLattice x y +theorem u64_absorb_join_meet : join u64Ops x (meet u64Ops x y) = x := + absorb_join_meet_eq u64_isLattice x y +theorem u64_meet_distrib_join : + meet u64Ops x (join u64Ops y z) = join u64Ops (meet u64Ops x y) (meet u64Ops x z) := + meet_distrib_join_eq u64_isLattice x y z +theorem u64_join_distrib_meet : + join u64Ops x (meet u64Ops y z) = meet u64Ops (join u64Ops x y) (join u64Ops x z) := + join_distrib_meet_eq u64_isLattice x y z +end Instances + +/-! ### Commutativity fails over `UInt64`, at the trie level + +`u64_not_isComm` rules out the *value* hypothesis, which is not quite the same +claim: a priori the asymmetry could have been invisible once lifted to tries. It +is not. Two single-path tries disagreeing only in their value are a +counterexample, so `join` and `meet` over `UInt64` are genuinely +non-commutative operations and the missing pair of laws is missing for a reason. -/ + +private def one : PrunedMap UInt64 := mk' [([0], 1)] +private def two : PrunedMap UInt64 := mk' [([0], 2)] + +theorem u64_join_not_comm : ¬ ∀ a b : PrunedMap UInt64, join u64Ops a b = join u64Ops b a := by + intro h + have hv := congrArg (fun m => m.valAt [0]) (h one two) + simp only [one, two, valAt_join, valAt_mk'] at hv + simp [joinVal, u64Ops, ValRes.resolve] at hv + +theorem u64_meet_not_comm : ¬ ∀ a b : PrunedMap UInt64, meet u64Ops a b = meet u64Ops b a := by + intro h + have hv := congrArg (fun m => m.valAt [0]) (h one two) + simp only [one, two, valAt_meet, valAt_mk'] at hv + simp [meetVal, u64Ops, ValRes.resolve] at hv + +-- The same counterexample, run rather than reasoned about: `beqT` is the +-- equality the model uses to decide `AlgebraicStatus::Identity`, and it says the +-- two orders give different tries. +#guard !(beqT u64Ops (join u64Ops one two) (join u64Ops two one)) +#guard !(beqT u64Ops (meet u64Ops one two) (meet u64Ops two one)) +#guard (join u64Ops one two).entries == [([0], (1 : UInt64))] +#guard (join u64Ops two one).entries == [([0], (2 : UInt64))] +-- …and that it is the *values* that differ, not the paths: over `()` the same +-- two tries are the same trie. +#guard beqT unitOps (join unitOps (mk' [([0], ())]) (mk' [([0], ())])) + (join unitOps (mk' [([0], ())]) (mk' [([0], ())])) + +end PrunedMap +end PrunedModel diff --git a/lean/PrunedModel/Map.lean b/lean/PrunedModel/Map.lean new file mode 100644 index 00000000..adeb66e9 --- /dev/null +++ b/lean/PrunedModel/Map.lean @@ -0,0 +1,312 @@ +import PrunedModel.Canon + +/-! +# A trie with no dangling paths + +## Why a second model + +`PathMapModel` models a `pathmap` trie as `List (Path × Option V)`: every +location that exists, carrying its value *if it has one*. That `Option` is +there because `pathmap` locations really do come in three states — absent, +present-without-a-value (a **dangling path**), and valued — and `create_path`, +`remove_val(false)` and a long list of operation-specific leaks all produce the +middle one. + +Modelling the middle state is necessary to specify those operations, but it is +also where nearly all of the specification's difficulty lives. Half of +`FINDINGS.md` is about it, `subtract` needs a special rule for "where the source +has no node at all, keep `self`'s subtree verbatim, dangling paths included", +and every algebraic operation has to say which valueless locations survive it. + +This model takes the other branch. It covers **only the subset of the API that +cannot produce a dangling path**, and in exchange it has no `Option`: + + entries : List (Path × V) + +A location exists iff some key has it as a prefix. Existence is *derived*, not +stored, so a dangling path is not merely absent from the model — it is +unrepresentable. There is no third state to specify, no prune flag to thread, +and `subtract` is pointwise. + +The claim this model makes is therefore stronger than the other one's. Where +`PathMapModel` says "here is what the crate does with dangling paths", +`PrunedModel` says "these operations never create one", and a trace divergence +is either a wrong value or a dangling path that should not be there. See +`PrunedModel/Fuzz.lean` for which operations are in the subset and why. + +## What is shared + +`PathMapModel.Basic` — `Path` and its prefix and lexicographic orders, +`ByteMask`, `ValOps`/`ValRes`, `AlgStatus` — is vocabulary rather than model, so +it is imported rather than duplicated. Everything below is independent of +`PathMapModel`. + +## Canonical form + +`entries` is sorted by `Path.lt` with no duplicate keys, so structural equality +*is* observational equality — which is what lets the model decide +`AlgebraicStatus::Identity` against `Element`. Every constructor goes through +`mk'`, which restores that form. +-/ + +namespace PrunedModel + +open PathMapModel + +/-- A `pathmap` trie with no dangling paths: a finite path→value map. + +Two things are *derived* rather than stored, and that is the whole design. + +The set of locations that exist is the prefix closure of the keys, plus the root; +`paths` computes it. So a dangling path is not merely absent from the model, it +is unrepresentable — which is what this model is for. + +Canonical form is carried in the type rather than asserted in a docstring. +`sorted` says the keys strictly increase in `Path.lt`, which by +`distinctKeys_of_sortedKeys` also rules out a key bound twice. Two consequences: +there is no junk inhabitant, so `PrunedMap` *is* the finite path→value map rather +than a representation of one; and structural equality is observational equality +(`eq_of_sortedKeys_of_lookup`), which is what lets the lattice laws in +`Lattice.lean` be equations with no side conditions. The field used to be a bare +list with a `Canonical` predicate the laws carried as a hypothesis. -/ +structure PrunedMap (V : Type) where + /-- Every location that carries a value, with it, in depth-first order. -/ + entries : List (Path × V) + /-- Keys strictly increasing: the canonical-form invariant. -/ + sorted : SortedKeys entries + +namespace PrunedMap + +variable {V : Type} + +/-! ## Construction + +`normVals` and its lemmas live in `PrunedModel/Canon.lean`; the only thing to do +here is carry the proof it supplies. -/ + +/-- Build a map from a raw, possibly unsorted, possibly duplicate-keyed +association list. + +This is the *only* constructor, and it takes no path argument: there is nothing +to say about which locations exist, because the keys already say it. The proof +field comes from `sortedKeys_normVals` — canonicalisation is what establishes the +invariant, so every map in the model is canonical by construction. -/ +def mk' (vals : List (Path × V)) : PrunedMap V := ⟨normVals vals, sortedKeys_normVals vals⟩ + +/-- The empty trie. Its root still exists — `PathMap::new().read_zipper()` +reports `path_exists() == true` — but nothing else does. -/ +def empty : PrunedMap V := ⟨[], trivial⟩ + +/-- **Equality is observational.** Two tries holding the same value at every path +are the same trie: the entry lists are sorted, so each is the unique sorted +enumeration of its own contents, and the `sorted` fields are proofs of a `Prop` +and so equal automatically. + +This is why `Lattice.lean` can state the lattice laws as `=`. -/ +theorem ext {a b : PrunedMap V} (h : ∀ k, a.entries.lookup k = b.entries.lookup k) : a = b := by + cases a; cases b + cases eq_of_sortedKeys_of_lookup _ _ ‹SortedKeys _› ‹SortedKeys _› h + rfl + +/-- Printed as its entry list: the `sorted` field is a `Prop` and carries no +information, so `deriving Repr` cannot be used and there is nothing to lose. -/ +instance [Repr V] : Repr (PrunedMap V) where + reprPrec t n := reprPrec t.entries n + +instance : Inhabited (PrunedMap V) := ⟨empty⟩ + +/-! ## Observations + +These functions are the entire observable interface of a trie; every +specification in this model is phrased in terms of them. -/ + +/-- The valued locations, in depth-first order. -/ +def keys (t : PrunedMap V) : List Path := t.entries.map (·.1) + +/-- Every location that carries a value, with it. (`entries` under its +`PathMapModel` name, kept so the two models read alike.) -/ +def vals (t : PrunedMap V) : List (Path × V) := t.entries + +/-- `Zipper::val` / `PathMap::get_val_at`: the value at `p`, if any. -/ +def valAt (t : PrunedMap V) (p : Path) : Option V := t.entries.lookup p + +/-- `Zipper::path_exists`. + +A location exists iff it is the root or some key has it as a prefix. This is +the whole content of the model's claim: there is no way to exist *without* +leading to a value. -/ +def pathExists (t : PrunedMap V) (p : Path) : Bool := + p.isEmpty || t.keys.any (fun k => p ≼ k) + +/-- Every location that exists, in depth-first order: the prefix closure of the +keys, with the root. -/ +def paths (t : PrunedMap V) : List Path := + Path.sortDedup (([] : Path) :: t.keys.flatMap Path.prefixes) + +/-- `Zipper::child_mask`: the bytes `b` for which `p ++ [b]` exists. + +Read straight off the keys — a child exists iff some key goes through it — which +is the simplification the missing `Option` buys. -/ +def childMask (t : PrunedMap V) (p : Path) : ByteMask := + ByteMask.ofList <| t.keys.filterMap fun k => + match Path.stripPrefix p k with + | some (b :: _) => some b + | _ => none + +/-- `Zipper::child_count`. -/ +def childCount (t : PrunedMap V) (p : Path) : Nat := (t.childMask p).length + +/-- `ZipperMoving::val_count`: values at and below `p`. -/ +def valCount (t : PrunedMap V) (p : Path) : Nat := + (t.entries.filter (fun kv => p ≼ kv.1)).length + +/-- `TrieNode::node_is_empty` applied to the node *below* `p`: no descendants. -/ +def belowIsEmpty (t : PrunedMap V) (p : Path) : Bool := + t.keys.all (fun k => !(p ≼ k) || k == p) + +/-- `PathMap::is_empty`. With no dangling paths this is just "no values". -/ +def isEmptyMap (t : PrunedMap V) : Bool := t.entries.isEmpty + +/-! ## Sub-tries and grafting -/ + +/-- The subtrie rooted at `p`, **including** the value at `p` as its root value: +`make_map` / `take_map` under the default `graft_root_vals` feature, and what a +zipper rooted at `p` sees. -/ +def subtrie (t : PrunedMap V) (p : Path) : PrunedMap V := + mk' (t.entries.filterMap fun kv => (Path.stripPrefix p kv.1).map (·, kv.2)) + +/-- Remove everything at and below `p`. -/ +def removeAt (t : PrunedMap V) (p : Path) : PrunedMap V := + mk' (t.entries.filter (fun kv => !(p ≼ kv.1))) + +/-- Remove everything strictly below `p`; the value at `p` survives. -/ +def removeBelow (t : PrunedMap V) (p : Path) : PrunedMap V := + mk' (t.entries.filter (fun kv => !(p ≼ kv.1) || kv.1 == p)) + +/-- Replace everything strictly below `p` with the strictly-below part of `s`. + +The value at `p` is not touched: `graft_internal` only ever replaces a node, and +the value at a location lives in its parent's cell. Grafting an empty node here +*removes* the location, where `PathMapModel.graftBelow` leaves it dangling — +that difference is the model's main claim about `graft`, and `Fuzz.lean` says +what the crate does with it. -/ +def graftBelow (t : PrunedMap V) (p : Path) (s : PrunedMap V) : PrunedMap V := + mk' ((t.removeBelow p).entries ++ s.entries.filterMap + (fun kv => if kv.1.isEmpty then none else some (p ++ kv.1, kv.2))) + +/-! ## Point updates -/ + +/-- `ZipperWriting::set_val` / `PathMap::set_val_at`. Returns the replaced value. -/ +def setVal (t : PrunedMap V) (p : Path) (v : V) : Option V × PrunedMap V := + (t.valAt p, mk' ((p, v) :: t.entries.filter (fun kv => !(kv.1 == p)))) + +/-- `ZipperWriting::remove_val`. + +In this model removal is *inherently* pruning: the chain that led to the value +stops existing the moment the value does, because existence is derived from the +keys. There is no prune flag, and the crate's `remove_val(true)` is what this +specifies. -/ +def removeVal (t : PrunedMap V) (p : Path) : Option V × PrunedMap V := + (t.valAt p, mk' (t.entries.filter (fun kv => !(kv.1 == p)))) + +/-! ## Pruning + +`prune_path` deletes the dangling chain ending at the focus. Here there is +never one: see `Spec.no_dangling_tip`. The operation is kept in the model and in +the fuzzer's table precisely so that the crate's `0` can be checked against it — +a non-zero prune on a trie built only from this subset means something in the +subset leaked a dangling path. -/ + +/-- `ZipperWriting::prune_path`: always a no-op, always `0` bytes. -/ +def prunePath (t : PrunedMap V) (_p : Path) : Nat × PrunedMap V := (0, t) + +/-! ## Algebraic operations + +Pointwise, all of them. `PathMapModel` needs a rule per operation for which +valueless locations survive — and `subtract` needs two, because `psubtract_dyn` +short-circuits on an absent child and keeps `self`'s dangling paths there. With +no dangling paths to keep, "keep `self`'s subtree verbatim where the source has +no node" and "subtract pointwise" coincide, so the rules collapse. -/ + +variable (ops : ValOps V) + +/-- `Option::pjoin` from `src/ring.rs`. -/ +def joinVal : Option V → Option V → Option V + | none, b => b + | some a, none => some a + | some a, some b => (ops.pjoin a b).resolve a b + +/-- `Option::pmeet`: a value survives only where *both* sides have one. -/ +def meetVal : Option V → Option V → Option V + | some a, some b => (ops.pmeet a b).resolve a b + | _, _ => none + +/-- `Option::psubtract`. -/ +def subVal : Option V → Option V → Option V + | none, _ => none + | some a, none => some a + | some a, some b => (ops.psub a b).resolve a b + +/-- Join (union). -/ +def join (a b : PrunedMap V) : PrunedMap V := + mk' <| (Path.sortDedup (a.keys ++ b.keys)).filterMap fun k => + (joinVal ops (a.valAt k) (b.valAt k)).map (k, ·) + +/-- Meet (intersection). -/ +def meet (a b : PrunedMap V) : PrunedMap V := + mk' <| a.keys.filterMap fun k => (meetVal ops (a.valAt k) (b.valAt k)).map (k, ·) + +/-- Subtract. -/ +def sub (a b : PrunedMap V) : PrunedMap V := + mk' <| a.entries.filterMap fun kv => + (subVal ops (some kv.2) (b.valAt kv.1)).map (kv.1, ·) + +/-- Is `q` *validated* by `b` — does some non-empty prefix of `q` carry a value +in `b`? + +The node-level reading of `prestrict`: a node has no root value, so the empty +prefix never validates. -/ +def validatedBy (b : PrunedMap V) (q : Path) : Bool := + (List.range q.length).any fun i => (b.valAt (q.take (i + 1))).isSome + +/-- `prestrict` at node level: keep the values of `a` validated by `b`. Once a +location is validated, everything below it is kept. -/ +def restrictBelowRoot (a b : PrunedMap V) : PrunedMap V := + mk' (a.entries.filter (fun kv => validatedBy b kv.1)) + +/-- Structural — hence observational — equality. Decides +`AlgebraicStatus::Identity`, which `pathmap` reports exactly when the output +equals `self`. -/ +def beqT (ops : ValOps V) (a b : PrunedMap V) : Bool := + a.entries.length == b.entries.length && + (a.entries.zip b.entries).all fun xy => xy.1.1 == xy.2.1 && ops.beq xy.1.2 xy.2.2 + +/-! ## Path surgery -/ + +/-- `ZipperWriting::insert_prefix`: put `k` in front of every path below the +root. The root value has nowhere to go and is dropped. -/ +def insertPrefixBelow (t : PrunedMap V) (k : Path) : PrunedMap V := + mk' (t.entries.filterMap fun kv => + if kv.1.isEmpty then none else some (k ++ kv.1, kv.2)) + +/-- The existing locations exactly `k` bytes below the root, depth-first. + +Locations, not keys: `descend_first_k_path` stops at any location at that depth, +whether or not it carries a value. -/ +def kPaths (t : PrunedMap V) (k : Nat) : List Path := + t.paths.filter (fun q => q.length == k) + +/-- `drop_head` / `join_k_path_into` at node level: strip the first `k` bytes +from every path and join the results. + +Values sitting at depth *exactly* `k` are **discarded** — the joined node has +nowhere to put a root value. (`meet_k_path_into` keeps them, because it routes +through `take_map`/`graft_map`, which do carry root values. The asymmetry is +real.) -/ +def dropHead (t : PrunedMap V) (k : Nat) : PrunedMap V := + if k == 0 then t + else (t.kPaths k).foldl + (fun acc q => join ops acc ((t.subtrie q).removeVal []).2) empty + +end PrunedMap +end PrunedModel diff --git a/lean/PrunedModel/Nested.lean b/lean/PrunedModel/Nested.lean new file mode 100644 index 00000000..2a88b64f --- /dev/null +++ b/lean/PrunedModel/Nested.lean @@ -0,0 +1,169 @@ +import PrunedModel.Lattice + +/-! +# A trie can be a value + +`IsLatticeVals` is a condition on a *value* type, and `PrunedMap V` has `join`, +`meet` and `sub` of its own — so can a trie be the value type of another trie? +Does the lattice structure compose? + +It does, and the shortness of this file is the point. When the entry list was a +bare `List (Path × V)` the answer was *no*: the type admitted +`⟨[([0], 1), ([0], 2)]⟩`, a list binding one key twice, and `join` of it with +itself kept only the first binding, so `join a a = a` was false for it. Five of +the ten laws failed, and they were exactly the five whose right-hand side is an +operand rather than another operation's output — the ones that needed a +`Canonical` hypothesis. Nesting then required a subtype of canonical tries, with +the lattice structure lifted through it by hand. + +Carrying sortedness in `PrunedMap`'s type removed the inhabitant. There is now +nothing to exclude: the expression above does not typecheck, because +`SortedKeys [([0], 1), ([0], 2)]` is false. So `PrunedMap V` is itself a lattice +value type, the subtype is gone, and this file is the ten-line lift. + +One law still needs more than the `Lattice.lean` §3 bundle, and that has nothing +to do with canonicity. `joinDistribMeet` has a single case reducing to +`meet (join a b) a = a` — absorption with the join on the *left*. A commutative +lattice gets it from the standard axiom read backwards; `pathmap`'s join is not +commutative, so the two orientations are different statements and only one is an +axiom. It is `IsFlipAbsorb`, and both instances satisfy it. +-/ + +namespace PrunedModel + +open PathMapModel PrunedMap + +variable {V : Type} {ops : ValOps V} + +/-! ## Tries as a value type -/ + +/-- `PrunedMap V` as a `ValOps`: `pjoin` is `join`, and so on. Each reports +`Element`, the result being a new trie rather than one of the operands. -/ +def trieOps (ops : ValOps V) : ValOps (PrunedMap V) where + pjoin a b := .elem (join ops a b) + pmeet a b := .elem (meet ops a b) + psub a b := .elem (sub ops a b) + beq a b := beqT ops a b + +@[simp] theorem joinVal_trieOps (a b : PrunedMap V) : + joinVal (trieOps ops) (some a) (some b) = some (join ops a b) := rfl + +@[simp] theorem meetVal_trieOps (a b : PrunedMap V) : + meetVal (trieOps ops) (some a) (some b) = some (meet ops a b) := rfl + +/-- **Tries are a lattice value type.** All ten laws, no side conditions: every +case is either a `rfl` on `Option` or a §7 equation applied directly. -/ +theorem trieOps_isLattice (h : IsLatticeVals ops) (hf : IsFlipAbsorb ops) : + IsLatticeVals (trieOps ops) where + joinAssoc x y z := by + match x, y, z with + | none, _, _ => rfl + | some _, none, _ => rfl + | some _, some _, none => rfl + | some a, some b, some c => exact congrArg some (join_assoc_eq h a b c) + meetAssoc x y z := by + match x, y, z with + | none, _, _ => rfl + | some _, none, _ => rfl + | some _, some _, none => rfl + | some a, some b, some c => exact congrArg some (meet_assoc_eq h a b c) + joinIdem x := by + match x with + | none => rfl + | some a => exact congrArg some (join_idem_eq h a) + meetIdem x := by + match x with + | none => rfl + | some a => exact congrArg some (meet_idem_eq h a) + joinNone x := by cases x <;> rfl + meetNone x := by cases x <;> rfl + absorbMeetJoin x y := by + match x, y with + | none, _ => rfl + | some a, none => exact congrArg some (meet_idem_eq h a) + | some a, some b => exact congrArg some (absorb_meet_join_eq h a b) + absorbJoinMeet x y := by + match x, y with + | none, _ => rfl + | some _, none => rfl + | some a, some b => exact congrArg some (absorb_join_meet_eq h a b) + meetDistribJoin x y z := by + match x, y, z with + | none, _, _ => rfl + | some _, none, none => rfl + | some _, none, some _ => rfl + | some _, some _, none => rfl + | some a, some b, some c => exact congrArg some (meet_distrib_join_eq h a b c) + joinDistribMeet x y z := by + match x, y, z with + | none, _, _ => rfl + | some a, none, none => exact congrArg some (meet_idem_eq h a).symm + | some a, none, some c => exact congrArg some (absorb_meet_join_eq h a c).symm + -- the one case a commutative lattice would get for free + | some a, some b, none => exact congrArg some (absorb_meet_join_flip_eq hf a b).symm + | some a, some b, some c => exact congrArg some (join_distrib_meet_eq h a b c) + +/-- …and a commutative one when the values under them are. -/ +theorem trieOps_isComm (hc : IsCommVals ops) : IsCommVals (trieOps ops) where + joinComm x y := by + match x, y with + | none, none => rfl + | none, some _ => rfl + | some _, none => rfl + | some a, some b => exact congrArg some (join_comm_eq hc a b) + meetComm x y := by + match x, y with + | none, none => rfl + | none, some _ => rfl + | some _, none => rfl + | some a, some b => exact congrArg some (meet_comm_eq hc a b) + +/-- The mirrored absorption lifts too, so the construction iterates. -/ +theorem trieOps_isFlipAbsorb (h : IsLatticeVals ops) (hf : IsFlipAbsorb ops) : + IsFlipAbsorb (trieOps ops) where + absorbMeetJoinFlip x y := by + match x, y with + | none, none => rfl + | none, some _ => rfl + | some a, none => exact congrArg some (meet_idem_eq h a) + | some a, some b => exact congrArg some (absorb_meet_join_flip_eq hf a b) + +/-! ## So tries nest, to any depth + +`PrunedMap (PrunedMap Unit)` — a trie whose values are sets of paths — is a +distributive lattice with a least element, commutative. `PrunedMap (PrunedMap +UInt64)` is the same minus commutativity. And `trieOps` of either is again a +lattice value type, so it iterates. -/ + +theorem nested_unit_isLattice : IsLatticeVals (trieOps unitOps) := + trieOps_isLattice unit_isLattice unit_isFlipAbsorb +theorem nested_unit_isComm : IsCommVals (trieOps unitOps) := trieOps_isComm unit_isComm +theorem nested_unit_isFlipAbsorb : IsFlipAbsorb (trieOps unitOps) := + trieOps_isFlipAbsorb unit_isLattice unit_isFlipAbsorb +theorem nested_u64_isLattice : IsLatticeVals (trieOps u64Ops) := + trieOps_isLattice u64_isLattice u64_isFlipAbsorb +theorem nested_u64_isFlipAbsorb : IsFlipAbsorb (trieOps u64Ops) := + trieOps_isFlipAbsorb u64_isLattice u64_isFlipAbsorb + +example (a b c : PrunedMap (PrunedMap Unit)) : + join (trieOps unitOps) (join (trieOps unitOps) a b) c + = join (trieOps unitOps) a (join (trieOps unitOps) b c) := + join_assoc_eq nested_unit_isLattice a b c + +example (a b : PrunedMap (PrunedMap Unit)) : + meet (trieOps unitOps) a b = meet (trieOps unitOps) b a := + meet_comm_eq nested_unit_isComm a b + +example (a b c : PrunedMap (PrunedMap UInt64)) : + meet (trieOps u64Ops) a (join (trieOps u64Ops) b c) + = join (trieOps u64Ops) (meet (trieOps u64Ops) a b) (meet (trieOps u64Ops) a c) := + meet_distrib_join_eq nested_u64_isLattice a b c + +-- Three deep, to show the iteration is real rather than a figure of speech. +example (a b c : PrunedMap (PrunedMap (PrunedMap Unit))) : + join (trieOps (trieOps unitOps)) a (meet (trieOps (trieOps unitOps)) b c) + = meet (trieOps (trieOps unitOps)) + (join (trieOps (trieOps unitOps)) a b) (join (trieOps (trieOps unitOps)) a c) := + join_distrib_meet_eq (trieOps_isLattice nested_unit_isLattice nested_unit_isFlipAbsorb) a b c + +end PrunedModel diff --git a/lean/PrunedModel/Spec.lean b/lean/PrunedModel/Spec.lean new file mode 100644 index 00000000..f26164dc --- /dev/null +++ b/lean/PrunedModel/Spec.lean @@ -0,0 +1,176 @@ +import PrunedModel.Write + +/-! +# What this model claims + +`PathMapModel/Spec.lean` has to say, operation by operation, which valueless +locations survive it. This model has a single claim instead, and everything +else is a consequence. + +**There is no dangling path.** A location that exists with nothing below it +carries a value — not as an invariant the constructors maintain, but because +existence is *defined* as "some key runs through here". `no_dangling` is the +proof, and its shortness is the measure of what dropping the `Option` buys. + +The consequence the fuzzer trades on: `prune_path` has nothing to do, so the +crate must report `0` for it on any trie built from this subset. Each time it +does not, some operation in the subset leaked a location that leads nowhere. + +The `#guard`s at the end are the executable half — small concrete tries run +through the definitions and checked at elaboration time. They catch the class +of mistake that type-checks right through: a swapped argument order, a `take` +that should have been a `drop`. +-/ + +namespace PrunedModel +namespace PrunedMap + +open PathMapModel + +variable {V : Type} + +/-! ## Keys and lookup -/ + +/-- Every path is a prefix of itself. -/ +theorem isPrefixOf_self : ∀ p : Path, (p ≼ p) = true + | [] => rfl + | _ :: as => by simp [Path.isPrefixOf, isPrefixOf_self as] + +/-- A key is bound: `lookup` finds whatever `map (·.1)` saw. -/ +theorem lookup_isSome_of_mem_keys {l : List (Path × V)} {p : Path} + (h : p ∈ l.map (·.1)) : (l.lookup p).isSome = true := by + obtain ⟨kv, hmem, heq⟩ := List.mem_map.mp h + exact List.lookup_isSome_iff.mpr ⟨kv, hmem, by simp [heq]⟩ + +/-- …and conversely, `lookup` only succeeds on a key. -/ +theorem mem_keys_of_lookup_isSome {l : List (Path × V)} {p : Path} + (h : (l.lookup p).isSome = true) : p ∈ l.map (·.1) := by + obtain ⟨kv, hmem, hb⟩ := List.lookup_isSome_iff.mp h + exact List.mem_map.mpr ⟨kv, hmem, (eq_of_beq hb).symm⟩ + +/-- Holding a value entails existing. -/ +theorem pathExists_of_valAt {t : PrunedMap V} {p : Path} {v : V} + (h : t.valAt p = some v) : t.pathExists p = true := by + have hmem : p ∈ t.keys := + mem_keys_of_lookup_isSome (l := t.entries) (p := p) + (show (t.entries.lookup p).isSome = true by + rw [show t.entries.lookup p = some v from h]; rfl) + cases hp : p.isEmpty with + | true => simp [pathExists, hp] + | false => + simp only [pathExists, hp, Bool.false_or, List.any_eq_true] + exact ⟨p, hmem, isPrefixOf_self p⟩ + +/-! ## The claim -/ + +/-- **No dangling paths.** A location that some key runs through, and that has +nothing strictly below it, carries a value. + +`pathExists` admits the root unconditionally — `PathMap::new().read_zipper()` +reports `path_exists() == true`, and the root of an empty trie is the one +location that exists without leading anywhere — so the hypothesis here is its +other disjunct. Together with "nothing strictly below `p`", the key running +through `p` can only be `p` itself. -/ +theorem no_dangling {t : PrunedMap V} {p : Path} + (hx : t.keys.any (fun k => p ≼ k) = true) (hb : t.belowIsEmpty p = true) : + (t.valAt p).isSome = true := by + obtain ⟨k, hk, hpk⟩ := List.any_eq_true.mp hx + have hkp : k == p := by simpa [hpk] using (List.all_eq_true.mp hb) k hk + exact lookup_isSome_of_mem_keys (by simpa [keys, eq_of_beq hkp] using hk) + +/-- Hence `prune_path` has nothing to prune, and reports `0`… -/ +theorem prunePath_eq_zero (t : PrunedMap V) (p : Path) : (t.prunePath p).1 = 0 := rfl + +/-- …and leaves the trie alone. -/ +theorem prunePath_id (t : PrunedMap V) (p : Path) : (t.prunePath p).2 = t := rfl + +/-- The empty trie has no values, so `is_empty` and "no keys" coincide. -/ +theorem isEmptyMap_empty : (empty : PrunedMap V).isEmptyMap = true := rfl + +/-- The root of the empty trie still exists — the one location that does. -/ +theorem pathExists_root (t : PrunedMap V) : t.pathExists [] = true := by + simp [pathExists] + +/-! ## Executable checks + +Concrete tries, run through the definitions at elaboration time. `t1` branches +at the root and carries a value at an interior location; `t2` is a single chain +beside a single leaf, which is the shape every dangling-path question is about. -/ + +section Guards + +private def t1 : PrunedMap UInt64 := mk' [([0, 1], 7), ([0], 3), ([2], 9)] +private def t2 : PrunedMap UInt64 := mk' [([0, 1, 2], 5), ([3], 7)] + +-- Canonical form: sorted depth-first, so a prefix precedes its extensions. +#guard t1.keys == [[0], [0, 1], [2]] +#guard t1.paths == [[], [0], [0, 1], [2]] +#guard t1.valAt [0] == some 3 +#guard t1.valAt [1] == none +#guard t1.valCount [] == 3 && t1.valCount [0] == 2 +#guard t1.childMask [] == ([0, 2] : List UInt8) +#guard t1.childCount [0] == 1 && t1.childCount [0, 1] == 0 + +-- Existence is the prefix closure of the keys, and nothing more. +#guard t1.pathExists [0, 1] && !t1.pathExists [1] && !t1.pathExists [0, 1, 2] +#guard t2.pathExists [0] && t2.pathExists [0, 1] && !t2.pathExists [0, 2] + +-- `no_dangling`, concretely: the one location with nothing below it is valued. +#guard t1.belowIsEmpty [0, 1] && (t1.valAt [0, 1]).isSome + +-- Removing a value removes the chain that existed only to reach it… +#guard (t2.removeVal [0, 1, 2]).2.keys == [[3]] +#guard !(t2.removeVal [0, 1, 2]).2.pathExists [0] +-- …but not a location some other key still runs through. +#guard (t1.removeVal [0]).2.keys == [[0, 1], [2]] && (t1.removeVal [0]).2.pathExists [0] + +-- `set_val` reports the value it replaced. +#guard (t1.setVal [0] 11).1 == some 3 && (t1.setVal [0] 11).2.valAt [0] == some 11 +#guard (t1.setVal [5] 11).1 == none && (t1.setVal [5] 11).2.keys == [[0], [0, 1], [2], [5]] + +-- Grafting an empty node below a *valued* location keeps the location… +#guard (t1.graftBelow [0] empty).keys == [[0], [2]] +-- …and below a valueless one takes the whole chain with it. This is the +-- model's central disagreement with `pathmap` 0.4.0, which leaves `[0]` and +-- `[0,1]` behind as dangling paths. +#guard (t2.graftBelow [0, 1] empty).keys == [[3]] +#guard !(t2.graftBelow [0, 1] empty).pathExists [0] + +-- Sub-tries carry the focus value as their root value. +#guard (t1.subtrie [0]).keys == [[], [1]] && (t1.subtrie [0]).valAt [] == some 3 +#guard (t1.subtrie [9]).isEmptyMap + +-- Algebra. `u64`'s `psubtract` annihilates on equal values, and its `pjoin` +-- and `pmeet` are left-biased projections. +#guard (sub u64Ops t1 t1).isEmptyMap +#guard (sub u64Ops t1 (mk' [([0], 3)])).keys == [[0, 1], [2]] +#guard (meet u64Ops t1 t1).keys == t1.keys +#guard (meet u64Ops t1 (mk' [([0], 99)])).entries == [([0], 3)] +#guard (join u64Ops t1 empty).entries == t1.entries +#guard (join u64Ops (mk' [([0], 1)]) (mk' [([2], 4)])).entries == [([0], 1), ([2], 4)] + +-- `prestrict` validates on a non-empty prefix only, so the root value of the +-- filter is invisible at node level. +#guard (restrictBelowRoot t1 (mk' [([0], 1)])).keys == [[0], [0, 1]] +#guard (restrictBelowRoot t1 (mk' [([], 1)])).isEmptyMap + +-- `drop_head` discards the values sitting at depth exactly `k`: `[3]` is at +-- depth 1, so its value has nowhere to go in the joined node. +#guard (dropHead u64Ops t2 1).entries == [([1, 2], 5)] +#guard (dropHead u64Ops t2 0).entries == t2.entries + +-- A write zipper at the map root, as the fuzzer builds it. +private def z2 : PZip UInt64 := { trie := t2, root := [], path := [0, 1] } + +-- `remove_branches` at a valueless focus takes the focus with it: it has no +-- value of its own and now nothing below, so it stops existing. +#guard (PZip.removeBranches z2).1 && (PZip.removeBranches z2).2.trie.keys == [[3]] +-- Nothing to prune afterwards, which is what the crate is checked against. +#guard (PZip.prunePath (PZip.removeBranches z2).2).1 == 0 +-- `remove_val` at a location with no value is a no-op, flag and all. +#guard (PZip.removeVal z2).1 == none && (PZip.removeVal z2).2.trie.entries == t2.entries + +end Guards + +end PrunedMap +end PrunedModel diff --git a/lean/PrunedModel/Write.lean b/lean/PrunedModel/Write.lean new file mode 100644 index 00000000..a6907cfc --- /dev/null +++ b/lean/PrunedModel/Write.lean @@ -0,0 +1,431 @@ +import PrunedModel.Zipper + +/-! +# The write zipper, restricted to the dangling-path-free subset + +Two invariants shape the whole API: + +1. **A node is what lies strictly below a location.** `get_focus`, + `graft_internal` and every `*_dyn` algebraic primitive operate on nodes, so + they never see or touch the value *at* the focus. Operations that do affect + it (`graft`, `graft_map`, `make_map`, `take_map`, `join_map_into`, + `meet_into`, `subtract_into`) do it in a separate step — the `graft_root_vals` + feature, on by default, which this model assumes. Note the asymmetry: + `graft` adopts the source's focus value but `join_into` does not join focus + values. + +2. **There is no prune flag.** In `PathMapModel` every mutating operation takes + one, because a write leaves a dangling path behind unless it is passed — and + even then the flag's effect is a function of where the internal node boundary + happens to fall (`PathMapModel/Fuzz.lean` therefore always passes `false` and + compares nothing). Here existence is derived from the keys, so removing the + last value under a chain removes the chain, with nothing to opt into. The + crate is driven with `prune = true` and must agree. + +## What is missing, and why + +* **`create_path`** — its entire purpose is to make a location that carries no + value. It cannot be modelled here and is not in the fuzzer's table. +* **`remove_val(false)`** — the non-pruning removal leaves the chain behind. + Only `remove_val(true)` is in the subset. +* **A write zipper below the map root** — see `PrunedModel/Zipper.lean`. + +Everything else in `ZipperWriting` is here. Several of those operations *can* +still leave a dangling path in `pathmap` 0.4.0 — `graft` of an empty source is +the clearest case — and the model says they must not. Those divergences are the +output this model exists to produce, so they are specified, not skipped; see +`PrunedModel/Fuzz.lean`. +-/ + +namespace PrunedModel +namespace PZip + +open PathMapModel + +variable {V : Type} (z : PZip V) + +/-- Replace the trie, keeping the cursor. -/ +def withTrie (t : PrunedMap V) : PZip V := { z with trie := t } + +/-! ## Values at the focus -/ + +/-- `ZipperWriting::get_val_mut` — the same observation as `val`, mutably. +Returns `some` exactly when `val` does; it never creates anything. -/ +def getValMut : Option V := z.val + +/-- `ZipperWriting::set_val`: sets the value at the focus, creating the path if +it did not exist. Returns the replaced value. -/ +def setVal (v : V) : Option V × PZip V := + let (old, t) := z.trie.setVal z.focus v + (old, z.withTrie t) + +/-- Writing through the reference `get_val_mut` returns. + +Specified as: where there is a value, this is `set_val`; where there is not, it +is a no-op — in particular it must **not** create the path, which is what +separates it from `set_val`. -/ +def getValMutWrite (v : V) : Option V × PZip V := + match z.val with + | some old => (some old, (z.setVal v).2) + | none => (none, z) + +/-- `ZipperWriting::get_val_or_set_mut`: the value at the focus, inserting +`default` if there is none. -/ +def getValOrSetMut (d : V) : V × PZip V := + match z.val with + | some v => (v, z) + | none => (d, (z.setVal d).2) + +/-- `ZipperWriting::get_val_or_set_mut_with`: as above, but the value comes from +a closure. + +The documented contract is that the closure supplies the value "if no value +exists", so it must run **exactly when the focus has no value** — running it +otherwise is observable to any caller whose closure has a side effect. The +second component records whether it ran, and the fuzzer compares that too. -/ +def getValOrSetMutWith (d : V) : V × Bool × PZip V := + match z.val with + | some v => (v, false, z) + | none => (d, true, (z.setVal d).2) + +/-- `ZipperWriting::remove_val(true)`. + +The chain above the removed value goes with it, because nothing in this model +can exist without leading to a value. `pathmap`'s own `remove_val(true)` prunes +only as far as the zipper's root, which is why the fuzzer keeps the write zipper +at the map root. -/ +def removeVal : Option V × PZip V := + match z.val with + | none => (none, z) + | some v => (some v, z.withTrie (z.trie.removeVal z.focus).2) + +/-! ## Pruning + +`prune_path` and `prune_ascend` are in the fuzzer's table but have nothing to do +here: a trie built from this subset has no dangling tip to prune (see +`Spec.no_dangling_tip`), so both are no-ops returning `0`. A non-zero count +from the crate is therefore a *finding* — it means some operation in the subset +left a dangling path for `prune_path` to find. -/ + +/-- `ZipperWriting::prune_path`: `0`, and nothing removed. -/ +def prunePath : Nat × PZip V := (0, z) + +/-- `ZipperWriting::prune_ascend`: `prune_path` followed by ascending that far, +so also a no-op. -/ +def pruneAscend : Nat × PZip V := (0, z) + +/-! ## Removing subtries -/ + +/-- `ZipperWriting::remove_branches`: delete everything strictly below the focus. +The value at the focus survives; if there is none, the focus stops existing. +Returns whether anything was removed. -/ +def removeBranches : Bool × PZip V := + (!z.focusNodeIsEmpty, z.withTrie (z.trie.removeBelow z.focus)) + +/-- `ZipperWriting::remove_unmasked_branches`: keep only the child bytes set in +`mask`; delete the rest along with their subtries. -/ +def removeUnmaskedBranches (mask : ByteMask) : PZip V := + let doomed := z.childMask.filter (fun b => !mask.contains b) + z.withTrie <| doomed.foldl (fun t b => t.removeAt (z.focus ++ [b])) z.trie + +/-! ## Grafting -/ + +/-- Replace the subtrie at the focus with `m`, treating `m` as a whole map: its +root value becomes the focus value (or clears it), and its branches become the +focus's branches. This is `ZipperWriting::graft_map`. -/ +def graftMap (m : PrunedMap V) : PZip V := + let t := z.trie.graftBelow z.focus m + z.withTrie <| + match m.valAt [] with + | some v => (t.setVal z.focus v).2 + | none => (t.removeVal z.focus).2 + +/-- `ZipperWriting::graft`: graft the subtrie at `src`'s focus, root value +included. + +Note what this says when the source is empty: the focus loses its value and its +branches, so — having nothing left to lead to — it stops existing, along with +any ancestor chain that existed only for it. `pathmap` 0.4.0 leaves that chain +behind as a dangling path. The model specifies the removal. -/ +def graft (src : PZip V) : PZip V := z.graftMap src.makeMap + +/-- `ZipperWriting::graft_src_at`: graft the subtrie `k` bytes below `src`'s +focus. -/ +def graftSrcAt (src : PZip V) (k : Path) : PZip V := + z.graftMap (src.trie.subtrie (src.focus ++ k)) + +/-- `ZipperWriting::graft_masked_branches`: graft the source's child branches for +each byte set in `mask`. + +Each set bit is a `graft_src_at` of the source's corresponding child, so the +child's *value* travels with it, and a set bit whose branch is absent from the +source leaves that branch absent here — grafting nothing removes. With +`removeUnset`, branches for clear bits are removed first, so `child_mask` +afterwards is a subset of `mask`; without it they are left alone. + +`WriteZipperCore` overrides the trait's default with a native implementation, so +this really compares two implementations of one contract. -/ +def graftMaskedBranches (src : PZip V) (mask : ByteMask) (removeUnset : Bool) : PZip V := + let z0 := if removeUnset then (z.removeBranches).2 else z + z0.withTrie <| mask.foldl (fun t b => + let child := z0.focus ++ [b] + let m := src.trie.subtrie (src.focus ++ [b]) + let t1 := t.graftBelow child m + match m.valAt [] with + | some v => (t1.setVal child v).2 + | none => (t1.removeVal child).2) z0.trie + +/-- `ZipperWriting::take_map`: remove the subtrie at the focus (value included) +and return it as a map. `none` when there was nothing to take. -/ +def takeMap : Option (PrunedMap V) × PZip V := + let rv := z.val + let below := z.focusNode + let z1 := z.withTrie (z.trie.removeAt z.focus) + let taken := + match rv with + | some v => (below.setVal [] v).2 + | none => below + (if below.isEmptyMap && rv.isNone then none else some taken, z1) + +/-! ## Path surgery -/ + +/-- `ZipperWriting::insert_prefix`: put `pre` in front of every path below the +focus. The focus value is untouched. Returns `false` at a location with no +descendants. + +An **empty** prefix should be the identity, but `make_parents_in(b"", node)` +discards the node in `pathmap` 0.4.0 — the subtrie below the focus is destroyed +and `true` is still returned. The model specifies the identity; the fuzzer skips +the empty prefix so the known divergence does not mask others. -/ +def insertPrefix (pre : Path) : Bool × PZip V := + if z.focusNodeIsEmpty then (false, z) + else (true, z.withTrie (z.trie.graftBelow z.focus (z.focusNode.insertPrefixBelow pre))) + +/-- `ZipperWriting::remove_prefix`: lift the subtrie below the focus up by `n` +bytes, replacing whatever was below the new (ascended) focus. Returns whether +the full `n` bytes could be ascended. + +The value at the old focus is *not* carried up — it belonged to the parent's +cell, not to the node that moves. -/ +def removePrefix (n : Nat) : Bool × PZip V := + let below := z.focusNode + let (ascended, z1) := z.ascend n + (ascended == n, z1.withTrie (z1.trie.graftBelow z1.focus below)) + +/-! ## Algebraic operations + +`AlgebraicStatus` is decided structurally: `Identity` exactly when the output +equals the input, `None` when the output is empty, `Element` otherwise. +`Identity(COUNTER_IDENT)` — the output equals the *source* — is reported as +`Element` by `pathmap`, and the model agrees, because the output still differs +from `self`. -/ + +variable (ops : ValOps V) + +/-- The status of replacing `before` with `after`. -/ +def nodeStatus (before after : PrunedMap V) : AlgStatus := + if after.isEmptyMap then .none + else if PrunedMap.beqT ops after before then .identity + else .element + +/-- `ZipperWriting::join_into`: union the source's subtrie into the focus's. + +The focus **values are not joined** — only the nodes below the focus are. The +map-consuming variant `join_map_into` *does* join root values. -/ +def joinInto (src : PZip V) : AlgStatus × PZip V := + let selfB := z.focusNode + let srcB := src.focusNode + if srcB.isEmptyMap then (if selfB.isEmptyMap then .none else .identity, z) + else + let r := PrunedMap.join ops selfB srcB + if PrunedMap.beqT ops r selfB then (.identity, z) + else (.element, z.withTrie (z.trie.graftBelow z.focus r)) + +/-- `ZipperWriting::join_map_into`: union a consumed map into the focus. + +Unlike `join_into` this *does* join the map's root value into the focus value. +It also short-circuits: when the map has no root node the node status is +returned directly and the value status computed above is discarded — even though +the value has already been written. -/ +def joinMapInto (m : PrunedMap V) : AlgStatus × PZip V := + -- `merge` is called with both "was none" flags set, as the crate does, so the + -- second component is carried only for symmetry with the other operations. + let (valStatus, _valWasNone, z1) := + match z.val, m.valAt [] with + | some sv, some mv => + let r := ops.pjoin sv mv + (AlgStatus.ofValRes r, false, + match r.resolve sv mv with + | some v => (z.setVal v).2 + | none => (z.removeVal).2) + | none, some mv => (AlgStatus.element, true, (z.setVal mv).2) + | some _, none => (AlgStatus.identity, false, z) + | none, none => (AlgStatus.none, true, z) + let srcB := (m.removeVal []).2 + if srcB.isEmptyMap then + -- Note the asymmetry with `join_into`: this branch tests + -- `self.get_focus().is_none()` (does a node exist at all?), not + -- `node_is_empty()`. The two coincide here, since a location that exists + -- has something below it or a value of its own. + -- + -- The node status is *merged* with the value status rather than returned on + -- its own. It used to be returned directly -- an early `return` that + -- discarded a value the operation had already written -- which is + -- issue #139, fixed by PR #142 (`276fca0`). + (AlgStatus.merge + (if z1.pathExists then AlgStatus.identity else AlgStatus.none) valStatus true true, z1) + else + let selfB := z1.focusNode + let r := PrunedMap.join ops selfB srcB + let nodeSt := if PrunedMap.beqT ops r selfB then AlgStatus.identity else AlgStatus.element + let z2 := if nodeSt == .identity then z1 else z1.withTrie (z1.trie.graftBelow z1.focus r) + (AlgStatus.merge nodeSt valStatus true true, z2) + +/-- `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. -/ +def meetInto (src : PZip V) : AlgStatus × PZip V := + let (valStatus, valWasNone, z1) := + match z.val, src.val with + | some sv, some ov => + let r := ops.pmeet sv ov + (AlgStatus.ofValRes r, false, + match r.resolve sv ov with + | some v => (z.setVal v).2 + | none => (z.removeVal).2) + | none, some _ => (AlgStatus.none, true, z) + | some _, none => (AlgStatus.none, false, (z.removeVal).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 + (AlgStatus.merge .none valStatus false valWasNone, + z1.withTrie (z1.trie.removeBelow z1.focus)) + else + let r := PrunedMap.meet ops selfB srcB + let st := nodeStatus ops selfB r + 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. + +Pointwise. `PathMapModel` needs a second rule here — where the source has no +node at all, `self`'s subtree survives untouched, dangling paths included — and +that rule is exactly what the missing `Option` makes unnecessary: with nothing +valueless to preserve, "keep verbatim" and "subtract pointwise" agree. -/ +def subtractInto (src : PZip V) : AlgStatus × PZip V := + let (valStatus, valWasNone, z1) := + match z.val, src.val with + | some sv, some ov => + let r := ops.psub sv ov + (AlgStatus.ofValRes r, false, + match r.resolve sv ov with + | some v => (z.setVal v).2 + | none => (z.removeVal).2) + | none, some _ => (AlgStatus.none, true, z) + | some _, none => (AlgStatus.identity, false, z) + | none, none => (AlgStatus.none, true, z) + let selfB := z1.focusNode + let srcB := src.focusNode + if srcB.isEmptyMap then + (AlgStatus.merge (if selfB.isEmptyMap then .none else .identity) valStatus + selfB.isEmptyMap valWasNone, z1) + else if selfB.isEmptyMap then + (AlgStatus.merge .none valStatus true valWasNone, z1) + else + let r := PrunedMap.sub ops selfB srcB + let st := nodeStatus ops selfB r + let z2 := if st == .identity then z1 else z1.withTrie (z1.trie.graftBelow z1.focus r) + (AlgStatus.merge st valStatus false valWasNone, z2) + +/-- `ZipperWriting::meet_2`: meet two *source* subtries and write the result at +the focus. + +It does not consult what is already at the focus, so — as the implementation +notes — it never reports `Identity`, only `Element` or `None`. And it works on +nodes, so neither source's focus value is consulted and the focus value here is +left untouched. -/ +def meet2 (a b : PZip V) : AlgStatus × PZip V := + let an := a.focusNode + let bn := b.focusNode + if an.isEmptyMap || bn.isEmptyMap then + (.none, z.withTrie (z.trie.removeBelow z.focus)) + else + let r := PrunedMap.meet ops an bn + if r.isEmptyMap then (.none, z.withTrie (z.trie.removeBelow z.focus)) + else (.element, z.withTrie (z.trie.graftBelow z.focus r)) + +/-- `ZipperWriting::restrict`: keep only the paths below the focus that are +prefixed by a path to a value in the source's subtrie. + +The empty prefix does **not** validate here: the source's focus value is +invisible to a node-level `prestrict`. `PathMap::restrict` does consult the root +value, so the two disagree exactly when the source has a value at its focus. +`self`'s focus value is never touched. -/ +def restrict (src : PZip V) : AlgStatus × PZip V := + let srcB := src.focusNode + let selfB := z.focusNode + if srcB.isEmptyMap then (.none, z.withTrie (z.trie.removeBelow z.focus)) + else if selfB.isEmptyMap then (.none, z) + else + let r := PrunedMap.restrictBelowRoot selfB srcB + let st := nodeStatus ops selfB r + if st == .identity then (.identity, z) + else (st, z.withTrie (z.trie.graftBelow z.focus r)) + +/-- `ZipperWriting::restricting`: the mirror image — `self`'s subtrie is replaced +by the source's, restricted by the paths to values in `self`. + +`false`, leaving `self` untouched, when either side has nothing below its focus. -/ +def restricting (src : PZip V) : Bool × PZip V := + if src.focusNodeIsEmpty then (false, z) + else if z.focusNodeIsEmpty then (false, z) + else (true, z.withTrie (z.trie.graftBelow z.focus + (PrunedMap.restrictBelowRoot src.focusNode z.focusNode))) + +/-! ## Collapsing path segments -/ + +/-- `ZipperWriting::join_k_path_into` (a.k.a. `drop_head`): strip the leading `k` +bytes from every path below the focus and join the results. Returns whether +anything survives below the focus. + +Values at depth exactly `k` are **lost**: the joined node has no root value slot. + +`k = 0` should be the identity — dropping no bytes — but `drop_head_dyn(0)` +collapses the subtrie instead. The model specifies the identity; the fuzzer +skips `k = 0`. -/ +def joinKPathInto (k : Nat) : Bool × PZip V := + let below := z.focusNode + if below.isEmptyMap then (false, z) + else + let r := PrunedMap.dropHead ops below k + (!r.isEmptyMap, z.withTrie (z.trie.graftBelow z.focus r)) + +/-- `meet_k_path_into` is **not implementable** for these arguments: its +provisional implementation drives `descend_first_k_path` through the +`ZipperIteration` *default* loop, which spins forever when the focus has no +children, and which escapes the focus's subtree entirely when `k = 0`. -/ +def meetKPathUnspecified (k : Nat) : Bool := k == 0 || z.childCount == 0 + +/-- `ZipperWriting::meet_k_path_into`: strip the leading `k` bytes from every +path below the focus and meet the results. + +Unlike `join_k_path_into` this routes through `take_map`/`graft_map`, so values +at depth exactly `k` *are* carried — they become the focus value. Only +meaningful when `meetKPathUnspecified` is `false`. -/ +def meetKPathInto (k : Nat) : Bool × PZip V := + let kps := (z.trie.subtrie z.focus).kPaths k + let result : Option (PrunedMap V) := + kps.foldl (fun acc q => + let m := z.trie.subtrie (z.focus ++ q) + match acc with + | none => some m + | some a => some (PrunedMap.meet ops a m)) none + match result with + | some m => if m.isEmptyMap then (false, (z.removeBranches).2) else (true, z.graftMap m) + | none => (false, (z.removeBranches).2) + +end PZip +end PrunedModel diff --git a/lean/PrunedModel/Zipper.lean b/lean/PrunedModel/Zipper.lean new file mode 100644 index 00000000..b8da5b53 --- /dev/null +++ b/lean/PrunedModel/Zipper.lean @@ -0,0 +1,331 @@ +import PrunedModel.Map + +/-! +# The zipper, over a trie with no dangling paths + +Same cursor as `PathMapModel.Zip` — a trie, the absolute path the zipper was +created at, and the relative path to the focus — and the same read API. What +changes is what the observations *mean*: + +* `path_exists` is now "some value lies at or below here", because that is the + only way to exist. +* `child_mask` is read off the keys rather than off a separate set of locations. +* `descend_until`, `ascend_until_branch`, `to_next_step` and the `k`-path + primitives walk the prefix closure of the keys, which is the whole trie. + +Everything else is a transcription of `PathMapModel.Zipper`, and deliberately so: +the point of the second model is a different *representation* of the same +contract, not a different reading of it. Where the two models disagree, one of +them is wrong, and the fuzzer says which. + +## The write zipper is rooted at the map root + +`PrunedModel`'s fuzzer only ever builds a write zipper at the map root; see +`Fuzz.header`. A write zipper rooted below it holds a node at its own root, +which survives as a dangling path once everything below it is removed, and +`prune_path` is documented not to rise above the zipper's origin. That is a +location that exists without leading to a value, so it is outside this model by +construction rather than by a bug. Off-root *writing* is still covered — the +root-rooted zipper reaches it with `descend_to`. +-/ + +namespace PrunedModel + +open PathMapModel + +/-- A zipper: a trie, the absolute path of the zipper's root, and the relative +path to the focus. -/ +structure PZip (V : Type) where + trie : PrunedMap V + root : Path + path : Path +deriving Repr + +namespace PZip + +variable {V : Type} (z : PZip V) + +/-- `ZipperAbsolutePath::origin_path`: the absolute path of the focus. -/ +def focus : Path := z.root ++ z.path + +/-- `ZipperAbsolutePath::root_prefix_path`. -/ +def rootPrefixPath : Path := z.root + +/-- All locations of the zipper's subtrie, relative to its root, in depth-first +order. The zipper's entire visible universe. -/ +def subPaths : List Path := (z.trie.subtrie z.root).paths + +/-! ## `trait Zipper` -/ + +/-- `Zipper::path_exists`. -/ +def pathExists : Bool := z.trie.pathExists z.focus + +/-- `Zipper::is_val`. -/ +def isVal : Bool := (z.trie.valAt z.focus).isSome + +/-- `Zipper::child_mask`. -/ +def childMask : ByteMask := z.trie.childMask z.focus + +/-- `Zipper::child_count`. -/ +def childCount : Nat := z.childMask.length + +/-- `ZipperMoving::focus_byte`: the byte last descended to reach the focus. +**Unspecified at the root**; the harness masks it there. -/ +def focusByte : Option UInt8 := z.path.getLast? + +/-! ## `trait ZipperValues` -/ + +/-- `ZipperValues::val`. -/ +def val : Option V := z.trie.valAt z.focus + +/-- `ZipperValues::val_at`: the value at `k`, relative to the focus. -/ +def valAt (k : Path) : Option V := z.trie.valAt (z.focus ++ k) + +/-! ## `trait ZipperSubtries` -/ + +/-- `ZipperInfallibleSubtries::make_map`. Under the default `graft_root_vals` +feature the value at the focus becomes the new map's root value. -/ +def makeMap : PrunedMap V := z.trie.subtrie z.focus + +/-- The node below the focus — what `get_focus` returns. This, not `makeMap`, +is what the algebraic operations and `graft_internal` consume. -/ +def focusNode : PrunedMap V := (z.makeMap.removeVal []).2 + +/-- `get_focus().is_none()`: the focus has no descendants. -/ +def focusNodeIsEmpty : Bool := z.trie.belowIsEmpty z.focus + +/-! ## `trait ZipperMoving` — position -/ + +/-- The same zipper with its focus at the relative path `q`, so that an ancestor +or descendant can be named and then asked about. -/ +def atPath (q : Path) : PZip V := { z with path := q } + +/-- `ZipperMoving::at_root`. -/ +def atRoot : Bool := z.path.isEmpty + +/-- `ZipperMoving::reset`. -/ +def reset : PZip V := { z with path := [] } + +/-- `ZipperMoving::val_count`: values at and below the focus. -/ +def valCount : Nat := z.trie.valCount z.focus + +/-! ## `trait ZipperMoving` — descent -/ + +/-- `ZipperMoving::descend_to`. Never fails; the focus may end up off-trie. -/ +def descendTo (k : Path) : PZip V := { z with path := z.path ++ k } + +/-- `ZipperMoving::descend_to_byte`. -/ +def descendToByte (b : UInt8) : PZip V := z.descendTo [b] + +/-- `ZipperMoving::descend_to_check`: descend, then report existence. -/ +def descendToCheck (k : Path) : Bool × PZip V := + let z' := z.descendTo k + (z'.pathExists, z') + +/-- `ZipperMoving::descend_to_existing`: descend byte by byte, stopping where the +path stops existing. Returns the number of bytes actually descended. -/ +def descendToExisting (k : Path) : Nat × PZip V := + -- Existence is prefix-closed, so the prefixes of `k` that still exist form an + -- initial segment: the answer is the longest prefix of `k` that exists. + let reach := ((List.range (k.length + 1)).filter + (fun j => (z.descendTo (k.take j)).pathExists)).getLast?.getD 0 + (reach, z.descendTo (k.take reach)) + +/-- `ZipperMoving::descend_to_val`: descend byte by byte, stopping at the first +value encountered *below* the starting focus, or where the path stops existing. -/ +def descendToVal (k : Path) : Nat × PZip V := + let reach := ((List.range (k.length + 1)).filter + (fun j => (z.descendTo (k.take j)).pathExists)).getLast?.getD 0 + let stop := ((List.range (reach + 1)).filter + (fun j => 0 < j && (z.descendTo (k.take j)).isVal)).head?.getD reach + (stop, z.descendTo (k.take stop)) + +/-- `ZipperMoving::descend_to_existing_byte`. -/ +def descendToExistingByte (b : UInt8) : Bool × PZip V := + let z' := z.descendToByte b + if z'.pathExists then (true, z') else (false, z) + +/-- `ZipperMoving::descend_indexed_byte`: descend into the `idx`-th child in +ascending byte order, returning the byte moved to. -/ +def descendIndexedByte (idx : Nat) : Option UInt8 × PZip V := + match z.childMask.indexedBit idx with + | some b => (some b, z.descendToByte b) + | none => (none, z) + +/-- `ZipperMoving::descend_first_byte`. -/ +def descendFirstByte : Option UInt8 × PZip V := z.descendIndexedByte 0 + +/-- `ZipperMoving::descend_last_byte`. -/ +def descendLastByte : Option UInt8 × PZip V := + let c := z.childCount + if c == 0 then (none, z) else z.descendIndexedByte (c - 1) + +/-- `ZipperMoving::descend_until`: descend while there is exactly one child, +stopping on a value. A no-op on a branch, a leaf, or a non-existent path. + +The destination is the *nearest* descendant that carries a value or is not +single-childed; `subPaths` is in depth-first order, which along a chain is order +of increasing depth, so `find?` returns it. -/ +def descendUntil : Bool × PZip V := + if z.childCount != 1 then (false, z) + else + match (z.subPaths.filter (fun q => z.path ≼ q && Path.lt z.path q)).find? + (fun q => (z.atPath q).isVal || (z.atPath q).childCount != 1) with + | some q => (true, z.atPath q) + | none => (false, z) + +/-- `ZipperMoving::descend_until_observed`: `descend_until`, reporting each byte +it descends. For the `Vec` observer the reported sequence must be exactly +the path delta — the only way a blind zipper learns where it ended up. -/ +def descendUntilObserved : Bool × Path × PZip V := + let (moved, z2) := z.descendUntil + (moved, z2.path.drop z.path.length, z2) + +/-- `ZipperMoving::descend_until_max_bytes`: `descend_until`, then ascend back to +at most `maxBytes` below the starting depth. -/ +def descendUntilMaxBytes (maxBytes : Nat) : Bool × PZip V := + if maxBytes == 0 then (false, z) + else + let target := z.path.length + maxBytes + let (moved, z') := z.descendUntil + if z'.path.length > target then (moved, { z' with path := z'.path.take target }) + else (moved, z') + +/-! ## `trait ZipperMoving` — ascent -/ + +/-- `ZipperMoving::ascend`: ascend `steps` bytes, clamping at the zipper root. +Returns the number of bytes actually ascended. -/ +def ascend (steps : Nat) : Nat × PZip V := + let n := min steps z.path.length + (n, { z with path := z.path.take (z.path.length - n) }) + +/-- `ZipperMoving::ascend_byte`: `ascend(1) == 1`. -/ +def ascendByte : Bool × PZip V := + let (n, z2) := z.ascend 1 + (n == 1, z2) + +/-- `ZipperMoving::ascend_until`: ascend to the nearest strict ancestor that +carries a value or branches, or to the root. Returns the bytes ascended. + +`properPrefixes` is shortest-first, so the last qualifying element is the +deepest; the root always qualifies, so there is always an answer. -/ +def ascendUntil : Nat × PZip V := + if z.atRoot then (0, z) + else + let stops := (Path.properPrefixes z.path).filter fun a => + a.isEmpty || (z.atPath a).isVal || (z.atPath a).childCount > 1 + let a := (stops.getLast?).getD [] + (z.path.length - a.length, z.atPath a) + +/-- `ZipperMoving::ascend_until_branch`: as above, but values do not stop it. -/ +def ascendUntilBranch : Nat × PZip V := + if z.atRoot then (0, z) + else + let stops := (Path.properPrefixes z.path).filter fun a => + a.isEmpty || (z.atPath a).childCount > 1 + let a := (stops.getLast?).getD [] + (z.path.length - a.length, z.atPath a) + +/-! ## `trait ZipperMoving` — lateral movement -/ + +/-- `ZipperMoving::to_next_sibling_byte`. + +At the zipper root there is no last byte, so the documented answer — and the +`ZipperMoving` default implementation's — is "did not move". The native +`ReadZipper` instead consults the last byte of the *absolute* origin path and +can leave its own root (FINDINGS.md #3); the fuzzer skips the operation at the +root so that known bug does not mask others. -/ +def toNextSiblingByte : Option UInt8 × PZip V := + match z.focusByte with + | none => (none, z) + | some cur => + if z.atRoot then (none, z) + else + let up := (z.ascendByte).2 + match up.childMask.nextBit cur with + | some b => (some b, up.descendToByte b) + | none => (none, z) + +/-- `ZipperMoving::to_prev_sibling_byte`. -/ +def toPrevSiblingByte : Option UInt8 × PZip V := + match z.focusByte with + | none => (none, z) + | some cur => + if z.atRoot then (none, z) + else + let up := (z.ascendByte).2 + match up.childMask.prevBit cur with + | some b => (some b, up.descendToByte b) + | none => (none, z) + +/-- `ZipperMoving::move_to_path`: jump to `p` relative to the zipper root. +Returns the number of bytes shared with the old location. -/ +def moveToPath (p : Path) : Nat × PZip V := + let overlap := ((List.range (min p.length z.path.length)).takeWhile + (fun i => p[i]? == z.path[i]?)).length + (overlap, { z with path := p }) + +/-! ## `trait ZipperMoving` — depth-first stepping -/ + +/-- `ZipperMoving::to_next_step`: the next existing location in depth-first +order. On exhaustion the focus returns to the root and the result is `false`. -/ +def toNextStep : Bool × PZip V := + match z.subPaths.find? (fun q => Path.lt z.path q) with + | some q => (true, { z with path := q }) + | none => (false, z.reset) + +/-! ## `trait ZipperIteration` -/ + +/-- `ZipperIteration::to_next_val`: the next location carrying a value, in +depth-first order. Never reports the value at the starting focus. -/ +def toNextVal : Bool × PZip V := + match z.subPaths.find? + (fun q => Path.lt z.path q && (z.trie.valAt (z.root ++ q)).isSome) with + | some q => (true, { z with path := q }) + | none => (false, z.reset) + +/-- `ZipperReadOnlyIteration::to_next_get_val`. -/ +def toNextGetVal : Option V × PZip V := + let (moved, z') := z.toNextVal + (if moved then z'.val else none, z') + +/-- `ZipperIteration::descend_last_path`: follow the last child to the end of +the depth-first-greatest path below the focus. -/ +def descendLastPath : Bool × PZip V := + let cands := z.subPaths.filter (fun q => z.path ≼ q) + match cands.getLast? with + | some q => if q == z.path then (false, z) else (true, { z with path := q }) + | none => (false, z) + +/-- The shared core of `descend_first_k_path` and `to_next_k_path` +(`k_path_internal`): the depth-first-least existing location exactly `k` bytes +below the common ancestor at depth `base`, strictly after the current focus. On +failure the focus moves to that ancestor. -/ +def kPathFrom (base k : Nat) : Bool × PZip V := + let anc := z.path.take base + match z.subPaths.find? + (fun q => q.length == base + k && anc ≼ q && Path.lt z.path q) with + | some q => (true, { z with path := q }) + | none => (false, { z with path := anc }) + +/-- `ZipperIteration::descend_first_k_path`. -/ +def descendFirstKPath (k : Nat) : Bool × PZip V := z.kPathFrom z.path.length k + +/-- `ZipperIteration::to_next_k_path`: the next existing location at the same +depth, under the common ancestor `k` bytes above the focus. + +When the focus is shallower than `k` the native `ReadZipper` falls back to the +**zipper root** as the common ancestor, so the call behaves like +`descend_first_k_path(k)` from the root and can succeed; the `ZipperIteration` +default returns `false` without moving. The model follows the native one, which +is what the public API reaches. -/ +def toNextKPath (k : Nat) : Bool × PZip V := + if k ≤ z.path.length then z.kPathFrom (z.path.length - k) k else z.kPathFrom 0 k + +/-! ## `trait ZipperForking` -/ + +/-- `ZipperForking::fork_read_zipper`: a new zipper rooted at the current focus. -/ +def forkReadZipper : PZip V := { z with root := z.focus, path := [] } + +end PZip +end PrunedModel diff --git a/lean/README.md b/lean/README.md index 60696f91..ed7f6639 100644 --- a/lean/README.md +++ b/lean/README.md @@ -36,8 +36,16 @@ cargo build --release -p differential # generate random programs and compare model against crate ./lean/differential.py --random 500 --seed 1 +# the same, for the dangling-path-free subset (the second model, below) +./lean/pruned_differential.py --random 500 --seed 1 + # minimise an input that diverges (or that panics) ./lean/shrink.py path/to/input.bin + +# ...or one that diverges against the second model +PATHMAP_ORACLE=lean/.lake/build/bin/pruned-oracle \ +PATHMAP_TRACE=target/release/pruned_trace \ + ./lean/shrink.py path/to/input.bin ``` `lake build` also checks every `#guard` in `PathMapModel/Check.lean`, so a build @@ -155,6 +163,8 @@ focus, such that ..." — instead of as a node walk. | `PathMapModel/Check.lean` | `#guard`s: regression fixtures transcribed from `src/write_zipper.rs`'s own tests, and the §2 laws over a battery of tries | | `PathMapModel/Fuzz.lean` | the wire format, the operation table, and the trace producer (including `--act` mode) | | `Main.lean` | the `pathmap-oracle` binary | +| `PrunedModel/*.lean` | the second model — the same API over `List (Path × V)`, covering only the subset that cannot leave a dangling path; see below | +| `PrunedMain.lean` | the `pruned-oracle` binary | ## What is proved versus what is checked @@ -611,6 +621,93 @@ invariants in-process after every operation — no oracle needed: `differential.py` runs without `--check`, because a crate that violates an invariant should show up as a trace diff rather than as an abort. +## A second model: the dangling-path-free subset + +`PrunedModel` is a separate specification of the same crate, and the thing worth +understanding about it is why there are two. + +This model represents a trie as `List (Path × Option V)`. The `Option` is not +optional: `pathmap` locations really do come in three states — absent, +present-without-a-value, valued — and `create_path` makes the middle one on +purpose while `remove_val(false)` leaves it behind. A model that could not +represent it could not specify those operations. + +But that third state is also where most of the specification's difficulty lives. +`subtract` needs a rule of its own for it ("where the source has no node at all, +keep `self`'s subtree verbatim, *including its dangling paths*"), every algebraic +operation has to say which valueless locations survive it, and the `prune` flag +has to be pinned to `false` and compared against nothing, because its effect is +a function of where an internal node boundary happens to fall rather than of the +trie. Several of the findings are about nothing else. + +`PrunedModel` takes the other branch. It covers **only the subset of the API +that cannot produce a dangling path**, and in exchange drops the `Option`: + +```lean +structure PrunedMap (V : Type) where + entries : List (Path × V) +``` + +A location exists iff some key has it as a prefix. Existence is *derived*, not +stored, so a dangling path is not merely absent from the model — it is +unrepresentable. There is no third state to specify, no flag to thread, and +`subtract` is pointwise, because with nothing valueless to preserve, "keep +`self`'s subtree verbatim" and "subtract pointwise" coincide. + +The claim is correspondingly stronger. Where `PathMapModel` says *here is what +the crate does with dangling paths*, `PrunedModel` says *these operations never +make one* — so a trace divergence is either a wrong value or a location that +leads nowhere. `PrunedModel/Spec.lean` proves the claim (`no_dangling`, three +lines) and the corollary the fuzzer trades on: `prune_path` has nothing to do, so +the crate must report `0` for it. + +Three restrictions define the subset: + +1. **No `create_path`**, whose whole purpose is a location with no value. +2. **`prune = true` everywhere.** Removal here is inherently pruning, so there + is nothing to opt into; `prune_path` and `prune_ascend` stay in the operation + table as *assertions*. +3. **The write zipper is rooted at the map root.** One rooted below it holds a + node at its own root, which survives as a location leading nowhere once + everything beneath it is removed, and `prune_path` is documented not to rise + above the zipper's origin — so that is outside the model by construction + rather than by a bug. Off-root *writing* is still covered: the root-rooted + zipper reaches every focus with `descend_to`. + +Operations the subset covers are specified, not skipped, even where the crate is +known to leak. That is the point: `graft` with an empty source is accidentally +`create_path`, and +[PRUNED_FINDINGS.md](PRUNED_FINDINGS.md) is the result. Only four `skip:` +reasons survive (`at-root`, `k0`, `empty-focus`, `empty-path`), against the +other harness's seven. + +`differential/src/pruned.rs` is the crate side — one read source, so no +`ReadSource` trait and no ACT mode — and `lean/pruned_differential.py` is +`differential.py` with `ORACLE`, `TRACE_CANDIDATES` and `KNOWN` repointed, so +nothing about *how* inputs are run is duplicated. `pruned_trace --check` needs +no oracle at all: it asserts the zipper invariants after every operation and, +at the end, that the write target contains no dangling path. + +### Agreement + +4000 random programs, seed 11, against `pathmap` 0.4.0 at `ec818cf`: + +| | inputs | +| --- | --- | +| agree | 3005 | +| the two findings in `PRUNED_FINDINGS.md` | 901 | +| two classes shared with the other model (value bias, `Identity` not reported) | 94 | +| anything else | **0** | + +The same 4000 inputs with the harness built on `fuzz-fixes-v3`: that branch +fixes both of the classes this model inherited and neither of the two it found. +Which is the argument for having both models — `fuzz-fixes-v3` was driven by the +other one, and a model that *reproduces* dangling paths cannot report an +operation for making one. See +[PRUNED_FINDINGS.md](PRUNED_FINDINGS.md) §4, which also says which v3 columns +are spec drift rather than findings: v3 changes the k-path walk and the integer +`psubtract`, and this oracle is pinned to master's reading of both. + ## Out of scope `ZipperHead` and the concurrency story, `ProductZipper` / `PrefixZipper` / diff --git a/lean/differential.py b/lean/differential.py index 0e91a522..bd9816a8 100755 --- a/lean/differential.py +++ b/lean/differential.py @@ -223,6 +223,17 @@ def run(self, blob): "removed [empty_node_leak]"), (["take_map_restore"], "take_map() returns Some(empty map) at a dangling tip [empty_node_leak]"), + # The implicit prune the graft family and remove_prefix now do (see + # lean/PRUNED_FINDINGS.md): with `prune = true`, `node_prune_limit` reclaims + # a dangling key *inside* the node even where `node_remove_all_branches` + # reports removing nothing, so how deep the reclamation reaches depends on + # where the node boundary falls -- FINDINGS.md #7, now reachable through + # operations that prune unconditionally. Only off-root write zippers are + # affected: 60000 inputs through lean/pruned_differential.py, whose write + # zipper is always at the map root, leave none of this. + (["remove_prefix"], + "the depth an implicit prune reaches is a function of node layout off the " + "map root (finding 7) [implicit_prune_node_layout]"), # Panics. These only abort in a debug build; differential.py prefers the # release binary, so they normally surface as wrong values instead. (["src/zipper.rs", "subtract with overflow"], diff --git a/lean/lakefile.toml b/lean/lakefile.toml index 783f6a37..0acf8626 100644 --- a/lean/lakefile.toml +++ b/lean/lakefile.toml @@ -1,5 +1,5 @@ name = "pathmap-model" -defaultTargets = ["PathMapModel", "pathmap-oracle"] +defaultTargets = ["PathMapModel", "pathmap-oracle", "PrunedModel", "pruned-oracle"] [[lean_lib]] name = "PathMapModel" @@ -7,3 +7,13 @@ name = "PathMapModel" [[lean_exe]] name = "pathmap-oracle" root = "Main" + +# The dangling-path-free model: a second, independent specification covering +# only the subset of the API that cannot leave a dangling path. See +# PrunedModel/Map.lean. +[[lean_lib]] +name = "PrunedModel" + +[[lean_exe]] +name = "pruned-oracle" +root = "PrunedMain" diff --git a/lean/pruned-corpus/graft-empty-src-creates-dangling-focus.bin b/lean/pruned-corpus/graft-empty-src-creates-dangling-focus.bin new file mode 100644 index 00000000..0deb5347 Binary files /dev/null and b/lean/pruned-corpus/graft-empty-src-creates-dangling-focus.bin differ diff --git a/lean/pruned-corpus/graft_masked_branches-creates-dangling-child.bin b/lean/pruned-corpus/graft_masked_branches-creates-dangling-child.bin new file mode 100644 index 00000000..17c6e393 Binary files /dev/null and b/lean/pruned-corpus/graft_masked_branches-creates-dangling-child.bin differ diff --git a/lean/pruned-corpus/graft_masked_branches-creates-dangling-focus.bin b/lean/pruned-corpus/graft_masked_branches-creates-dangling-focus.bin new file mode 100644 index 00000000..eefd1db7 Binary files /dev/null and b/lean/pruned-corpus/graft_masked_branches-creates-dangling-focus.bin differ diff --git a/lean/pruned-corpus/graft_src_at-empty-src-creates-dangling-focus.bin b/lean/pruned-corpus/graft_src_at-empty-src-creates-dangling-focus.bin new file mode 100644 index 00000000..a70093f9 Binary files /dev/null and b/lean/pruned-corpus/graft_src_at-empty-src-creates-dangling-focus.bin differ diff --git a/lean/pruned-corpus/join_into-value-bias-by-node-layout.bin b/lean/pruned-corpus/join_into-value-bias-by-node-layout.bin new file mode 100644 index 00000000..c5f233fe Binary files /dev/null and b/lean/pruned-corpus/join_into-value-bias-by-node-layout.bin differ diff --git a/lean/pruned-corpus/join_map_into-status-element-when-unchanged.bin b/lean/pruned-corpus/join_map_into-status-element-when-unchanged.bin new file mode 100644 index 00000000..de1bdd74 Binary files /dev/null and b/lean/pruned-corpus/join_map_into-status-element-when-unchanged.bin differ diff --git a/lean/pruned-corpus/meet_2-empty-result-creates-dangling-focus.bin b/lean/pruned-corpus/meet_2-empty-result-creates-dangling-focus.bin new file mode 100644 index 00000000..8f777b0b Binary files /dev/null and b/lean/pruned-corpus/meet_2-empty-result-creates-dangling-focus.bin differ diff --git a/lean/pruned-corpus/remove_prefix-creates-dangling-chain.bin b/lean/pruned-corpus/remove_prefix-creates-dangling-chain.bin new file mode 100644 index 00000000..294bb6d2 Binary files /dev/null and b/lean/pruned-corpus/remove_prefix-creates-dangling-chain.bin differ diff --git a/lean/pruned-corpus/restrict-empty-result-creates-dangling-focus.bin b/lean/pruned-corpus/restrict-empty-result-creates-dangling-focus.bin new file mode 100644 index 00000000..1b5b0121 Binary files /dev/null and b/lean/pruned-corpus/restrict-empty-result-creates-dangling-focus.bin differ diff --git a/lean/pruned-corpus/restricting-creates-dangling-focus.bin b/lean/pruned-corpus/restricting-creates-dangling-focus.bin new file mode 100644 index 00000000..04ba1ff2 Binary files /dev/null and b/lean/pruned-corpus/restricting-creates-dangling-focus.bin differ diff --git a/lean/pruned-corpus/subtract_into-status-element-when-unchanged.bin b/lean/pruned-corpus/subtract_into-status-element-when-unchanged.bin new file mode 100644 index 00000000..bbd84ab7 Binary files /dev/null and b/lean/pruned-corpus/subtract_into-status-element-when-unchanged.bin differ diff --git a/lean/pruned_differential.py b/lean/pruned_differential.py new file mode 100755 index 00000000..bf3fcea5 --- /dev/null +++ b/lean/pruned_differential.py @@ -0,0 +1,191 @@ +#!/usr/bin/env python3 +"""Differential runner for the dangling-path-free subset. + +Same driver as `differential.py` -- resident children, parallel workers, +timeouts, shrinkable failures -- pointed at the other model/harness pair: + + lean/.lake/build/bin/pruned-oracle PrunedModel (the oracle) + target/*/pruned_trace the real crate + + ./lean/pruned_differential.py --random 2000 -j8 + ./lean/pruned_differential.py pruned-corpus/* + +Everything about *how* inputs are run is inherited rather than copied: there is +one implementation of the resident-child protocol, the restart-on-wedge logic +and the input sourcing, and this file only says which binaries to run and which +divergences are already understood. `differential.py` reads `ORACLE`, +`TRACE_CANDIDATES` and `KNOWN` at call time, which is what makes that possible. + +## Why the KNOWN table starts almost empty + +`differential.py`'s table is large because its model reproduces `pathmap`'s +dangling-path behaviour, so the divergences left over are the subtle ones. This +model instead *forbids* dangling paths, so the first divergences it reports are +the operations that leak one -- which are the point, not noise. An entry gets +added here only once the leak is recorded in FINDINGS.md, so a new one cannot +hide behind it. +""" +import os +import sys + +sys.path.insert(0, os.path.dirname(os.path.abspath(__file__))) + +import re + +import differential as D + +ROOT = os.path.dirname(os.path.dirname(os.path.abspath(__file__))) + +D.ORACLE = os.path.join(ROOT, "lean", ".lake", "build", "bin", "pruned-oracle") +# PRUNED_TRACE overrides the search, for builds that live in another target dir. +D.TRACE_CANDIDATES = [os.environ.get("PRUNED_TRACE", "")] + [ + os.path.join(ROOT, "target", "release", "pruned_trace"), + os.path.join(ROOT, "target", "debug", "pruned_trace"), +] + +def _fields(line): + """The trace line's tokens, keyed by field name, per zipper. + + `0 graft ret=- W=01 o01 e1 v- c0 n0 f01 R=...` -> the W and R groups as + dicts, so a divergence can be asked which field moved. + """ + out = {} + for side in ("W", "R"): + m = re.search(r" %s=(\S+(?: \S+)*?)(?= [WR]=|$)" % side, line) + if not m: + return None + out[side] = { + (re.match(r"[A-Za-z]*", t).group(0) or t): t[len(re.match(r"[A-Za-z]*", t).group(0)):] + for t in m.group(1).split() + } + return out + + +def dangling_focus(a, b): + """The crate has locations the model does not, and none of them holds a value. + + The signature is that `e` and/or `c` moved *up* while `v` and `n` did not + move at all: `path_exists` became true, or `child_mask` gained a bit, without + a value appearing anywhere at or below the focus. So whatever the crate + created or kept leads nowhere. Both halves of + PRUNED_FINDINGS.md #1 and #2 land here -- the focus itself (`e0` -> `e1`) and + a child of it (`c0` -> `c1`), which is why the two are one entry in `KNOWN`. + + The operations that do this are the ones with no `prune` parameter to pass: + `graft`, `graft_src_at`, `graft_masked_branches`, `meet_2`, `restrict`, + `restricting`, `remove_prefix`. The ones that have one (`remove_val`, + `remove_branches`, `meet_into`, `subtract_into`) clean up correctly when it + is set, which is what this harness passes throughout. + """ + fa, fb = _fields(a), _fields(b) + if not fa or not fb: + return None + hit = False + for side in ("W", "R"): + xa, xb = fa[side], fb[side] + if xa == xb: + continue + moved = {k for k in set(xa) | set(xb) if xa.get(k) != xb.get(k)} + if not moved or not moved <= {"e", "c"}: + return None + # No value may appear: `v` at the focus and `n` below it must be equal, + # or the difference is content rather than an empty location. + if xa["v"] != xb["v"] or xa["n"] != xb["n"]: + return None + if "e" in moved and not (xa["e"] == "0" and xb["e"] == "1"): + return None + if "c" in moved and not int(xb["c"]) > int(xa["c"]): + return None + hit = True + return "DANGLING-FOCUS" if hit else None + + +def dangling_kept_dump(a, b): + """The crate's dump holds locations the model's does not, all valueless. + + The same defect seen in a trie dump rather than in a fingerprint: the model's + entries are a subsequence of the crate's, and every entry only the crate has + renders `-`. Nothing leads to those locations, so they are dangling paths + the operation declined to reclaim. + """ + ta, tb = a.split(), b.split() + if len(ta) != len(tb) or len(ta) < 2: + return None + if ta[0] != tb[0] or not (ta[0].startswith("MAP") or ta[1] == "dump"): + return None + sa, sb = ta[-1], tb[-1] + ea = [e for e in sa.split(",") if e] + eb = [e for e in sb.split(",") if e] + if len(eb) <= len(ea): + return None + # Is `ea` a subsequence of `eb`, and is every skipped entry valueless? + i, extra = 0, [] + for e in eb: + if i < len(ea) and e == ea[i]: + i += 1 + else: + extra.append(e) + if i != len(ea) or not extra: + return None + if any(not e.endswith(":-") for e in extra): + return None + return "DANGLING-DUMP" + + +_inherited_shape = D.divergence_shape + + +def divergence_shape(a, b): + """This model's shapes first, then the ones `differential.py` knows. + + Its shapes are about a model that *reproduces* dangling paths, so they + cannot name the class this one exists to report; they stay in place for + everything else. + """ + return dangling_focus(a, b) or dangling_kept_dump(a, b) or _inherited_shape(a, b) + + +D.divergence_shape = divergence_shape + +# Keyed on a substring of the divergence report, newest-understood first; see +# `differential.classify`. Each entry must name the operation *and* the +# finding, so that reading a `known` line tells you what was already decided. +D.KNOWN = [ + (["ESCAPED-ROOT"], + "a zipper left its own root: root_prefix_path() changed [root_escape]"), + # The trie-dump form, tested before the fingerprint form: a line that is + # only a dump has no fingerprint to read. + (["DANGLING-DUMP"], + "an empty write leaves locations that lead nowhere in the trie " + "(PRUNED_FINDINGS.md #1) [empty_write_materialises_focus]"), + # PRUNED_FINDINGS.md #1 and #2 -- one mechanism, seen at the focus (#1) or at + # a child of it (#2). Still present on fuzz-fixes-v3. + (["DANGLING-FOCUS"], + "an operation with no prune parameter materialises an empty location " + "(PRUNED_FINDINGS.md #1, #2) [empty_write_materialises_focus]"), + # What is left of the two classes this model shares with the other one. + # + # VALUE-ONLY is deliberately *not* listed: the value-bias class is fixed on + # this branch by the cherry-pick of 3dae731, so a hit is a regression and + # should be reported as new rather than filed under a known note. + # + # The STATUS-ONLY shape is two-directional and the direction is what names + # it, so read the report rather than the tag. `Identity` from the model + # against `Element` from the crate is the residual FINDINGS.md #8 + # imprecision in `subtract_into` and `meet_into`. The `join_map_into` form + # of it was never a crate defect: master changed that status in PR #142 + # (276fca0, issue #139) and both models described the behaviour it replaced, + # which is now corrected. The reverse direction appears only against + # fuzz-fixes-v3, whose `u64::psubtract` (f8a4599) returns Identity where + # `Basic.u64Ops` still says Element. + (["STATUS-ONLY"], + "AlgebraicStatus::Identity is not returned reliably when nothing changed, " + "in subtract_into/meet_into -- what is left of FINDINGS.md #8 once the " + "value level is fixed: the node algebra does not notice that the node it " + "assembled equals the one it replaces. 8 of 200000 inputs"), +] + +if __name__ == "__main__": + if "--act" in sys.argv: + sys.exit("--act is meaningless here: there is one read source") + D.main() diff --git a/src/dense_byte_node.rs b/src/dense_byte_node.rs index ab6bf2db..0bba7cdd 100644 --- a/src/dense_byte_node.rs +++ b/src/dense_byte_node.rs @@ -260,6 +260,94 @@ impl> ByteNode } } + /// [Self::join_child_into] with `node` as the *left* operand of the join, so on a collision + /// `node`'s values take precedence over `self`'s. The status is still relative to `self`. + pub(crate) fn join_child_into_left(&mut self, k: u8, node: TrieNodeODRc) -> AlgebraicStatus where V: Clone + Lattice { + let ix = self.mask.index_of(k) as usize; + if self.mask.test_bit(k) { + let cf = unsafe { self.values.get_unchecked_mut(ix) }; + match cf.rec_mut() { + Some(existing_node) => { + match node.pjoin(existing_node) { + //`COUNTER_IDENT` means the result is `existing_node`: nothing to do + AlgebraicResult::Identity(mask) if mask & COUNTER_IDENT > 0 => AlgebraicStatus::Identity, + AlgebraicResult::Identity(_) => { + *existing_node = node; + AlgebraicStatus::Element + }, + AlgebraicResult::Element(joined) => { + *existing_node = joined; + AlgebraicStatus::Element + }, + //Only two empty nodes join to nothing, and then there is nothing to change + AlgebraicResult::None => AlgebraicStatus::Identity, + } + }, + None => { + cf.set_rec(node); + AlgebraicStatus::Element + } + } + } else { + self.mask.set_bit(k); + let new_cf = CoFree::new(Some(node), None); + self.values.insert(ix, new_cf); + AlgebraicStatus::Element + } + } + + /// [Self::join_val_into] with `val` as the *left* operand of the join; see [Self::join_child_into_left] + pub(crate) fn join_val_into_left(&mut self, k: u8, val: V) -> AlgebraicStatus where V: Lattice { + let ix = self.mask.index_of(k) as usize; + if self.mask.test_bit(k) { + let cf = unsafe { self.values.get_unchecked_mut(ix) }; + match cf.val_mut() { + Some(existing_val) => { + match val.pjoin(existing_val) { + AlgebraicResult::Identity(mask) if mask & COUNTER_IDENT > 0 => AlgebraicStatus::Identity, + AlgebraicResult::Identity(_) => { + *existing_val = val; + AlgebraicStatus::Element + }, + AlgebraicResult::Element(joined) => { + *existing_val = joined; + AlgebraicStatus::Element + }, + //A join of two present values never has an empty result; see `Lattice::join_into` + AlgebraicResult::None => AlgebraicStatus::Identity, + } + } + None => { + cf.set_val(val); + AlgebraicStatus::Element + } + } + } else { + self.mask.set_bit(k); + let new_cf = CoFree::new(None, Some(val)); + self.values.insert(ix, new_cf); + AlgebraicStatus::Element + } + } + + /// Dispatches to [Self::join_child_into] or [Self::join_child_into_left] + #[inline] + pub(crate) fn join_child_into_oriented(&mut self, k: u8, node: TrieNodeODRc, incoming_is_left: bool) -> AlgebraicStatus where V: Clone + Lattice { + if incoming_is_left { self.join_child_into_left(k, node) } else { self.join_child_into(k, node) } + } + + /// Dispatches to [Self::join_payload_into] or its left-biased counterpart + #[inline] + pub(crate) fn join_payload_into_oriented(&mut self, k: u8, payload: ValOrChild, incoming_is_left: bool) -> AlgebraicStatus where V: Clone + Lattice { + if !incoming_is_left { + return self.join_payload_into(k, payload) + } + match payload { + ValOrChild::Child(child) => self.join_child_into_left(k, child), + ValOrChild::Val(val) => self.join_val_into_left(k, val), + } + } + /// Internal method to remove a CoFree from the node #[inline] fn remove(&mut self, k: u8) -> Option { @@ -557,7 +645,13 @@ impl> ByteNode } /// Merges the entries in the ListNode into the ByteNode - pub fn merge_from_list_node(&mut self, list_node: &LineListNode) -> AlgebraicStatus where V: Clone + Lattice { + /// Joins the contents of `list_node` into `self`. + /// + /// The join is left-biased, so `list_is_left` says which operand `list_node` is: `false` when + /// the caller is computing `self ∪ list_node` (collisions keep `self`'s values), `true` when it + /// is computing `list_node ∪ self` into a clone of the byte node (collisions keep the list + /// node's values). The returned status is always relative to `self`. + pub fn merge_from_list_node(&mut self, list_node: &LineListNode, list_is_left: bool) -> AlgebraicStatus where V: Clone + Lattice { let self_was_empty = self.is_empty(); self.reserve_capacity(2); @@ -567,9 +661,9 @@ impl> ByteNode if key.len() > 1 { let mut child_node = LineListNode::::new_in(self.alloc.clone()); unsafe{ child_node.set_payload_owned::<0>(&key[1..], payload); } - self.join_child_into(key[0], TrieNodeODRc::new_in(child_node, self.alloc.clone())) + self.join_child_into_oriented(key[0], TrieNodeODRc::new_in(child_node, self.alloc.clone()), list_is_left) } else { - self.join_payload_into(key[0], payload) + self.join_payload_into_oriented(key[0], payload, list_is_left) } } else { if self_was_empty { @@ -585,9 +679,9 @@ impl> ByteNode if key.len() > 1 { let mut child_node = LineListNode::::new_in(self.alloc.clone()); unsafe{ child_node.set_payload_owned::<0>(&key[1..], payload); } - self.join_child_into(key[0], TrieNodeODRc::new_in(child_node, self.alloc.clone())) + self.join_child_into_oriented(key[0], TrieNodeODRc::new_in(child_node, self.alloc.clone()), list_is_left) } else { - self.join_payload_into(key[0], payload) + self.join_payload_into_oriented(key[0], payload, list_is_left) } } else { if self_was_empty { @@ -1333,7 +1427,7 @@ impl> TrieNode LINE_LIST_NODE_TAG => { let other_list_node = unsafe{ other.as_list_unchecked() }; let mut new_node = self.clone(); - let status = new_node.merge_from_list_node(other_list_node); + let status = new_node.merge_from_list_node(other_list_node, false); AlgebraicResult::from_status(status, || TrieNodeODRc::new_in(new_node, self.alloc.clone())) }, #[cfg(feature = "bridge_nodes")] @@ -1378,7 +1472,7 @@ impl> TrieNode let other_list_node = unsafe{ other_node.into_list_unchecked() }; //GOAT, optimization opportunity to take the contents from the list, rather than cloning // them, to turn around and drop the ListNode and free them / decrement the refcounts - self.merge_from_list_node(other_list_node) + self.merge_from_list_node(other_list_node, false) }, #[cfg(feature = "bridge_nodes")] TaggedNodeRefMut::BridgeNode(_other_bridge_node) => { @@ -1416,7 +1510,9 @@ impl> TrieNode }, _ => { let mut new_node = Self::new_in(self.alloc.clone()); - while let Some(cf) = self.values.pop() { + //Ascending key order, with the accumulated node as the left operand of every join, + // so a collision keeps the value from the lexicographically first path + for cf in self.values.drain(..) { let child = cf.into_rec().filter(|child| !child.is_empty()); let child = if byte_cnt > 1 { child.and_then(|mut child| child.make_mut().drop_head_dyn(byte_cnt-1)) @@ -1449,7 +1545,9 @@ impl> TrieNode }, LINE_LIST_NODE_TAG => { let other_list_node = unsafe { other.as_list_unchecked() }; - other_list_node.pmeet_dyn(self.as_tagged()).invert_identity() + //`self` is the left operand; the list node enumerates its payloads but must resolve + // every collision as `self op list`, hence `swapped`. + other_list_node.pmeet_dyn_oriented(self.as_tagged(), true).invert_identity() }, #[cfg(feature = "bridge_nodes")] TaggedNodeRef::BridgeNode(other_bridge_node) => { @@ -1461,7 +1559,8 @@ impl> TrieNode }, TINY_REF_NODE_TAG => { let tiny_node = unsafe { other.as_tiny_unchecked() }; - tiny_node.pmeet_dyn(self.as_tagged()).invert_identity() + let full_node = tiny_node.into_full().unwrap(); + self.pmeet_dyn(full_node.as_tagged()) }, EMPTY_NODE_TAG => AlgebraicResult::None, _ => unsafe{ unreachable_unchecked() } diff --git a/src/line_list_node.rs b/src/line_list_node.rs index 85c8f24e..2127d7ed 100644 --- a/src/line_list_node.rs +++ b/src/line_list_node.rs @@ -1304,6 +1304,35 @@ fn try_merge<'a, V: Clone + Lattice + Send + Sync, A: Allocator, const ASLOT: us } /// The part of `try_merge` that we probably shouldn't inline +/// The subtrie left of one list-node slot after `byte_cnt` bytes are dropped from every path +/// below it, or `None` if nothing is left. Part of [TrieNode::drop_head_dyn]. +/// +/// A value sitting at depth `<= byte_cnt` is discarded (the joined node has nowhere to put a root +/// value), a dangling child has nothing below the dropped bytes, and a key longer than `byte_cnt` +/// just loses its first `byte_cnt` bytes. +fn drop_head_from_payload(key: &[u8], payload: ValOrChild, byte_cnt: usize, alloc: &A) -> Option> { + let key_len = key.len(); + if byte_cnt < key_len { + let mut new_node = LineListNode::new_in(alloc.clone()); + unsafe { new_node.set_payload_owned::<0>(&key[byte_cnt..], payload); } + debug_assert!(validate_node(&new_node)); + return Some(TrieNodeODRc::new_in(new_node, alloc.clone())) + } + match payload { + ValOrChild::Val(_) => None, + ValOrChild::Child(mut child) => { + if child.is_empty() { + return None + } + if byte_cnt == key_len { + Some(child) + } else { + child.make_mut().drop_head_dyn(byte_cnt - key_len) + } + } + } +} + fn merge_guts<'a, V: Clone + Lattice + Send + Sync, A: Allocator, const ASLOT: usize, const BSLOT: usize>(mut overlap: usize, a_key: &'a[u8], a: &LineListNode, b_key: &'a[u8], b: &LineListNode) -> AlgebraicResult<(&'a[u8], ValOrChild)> { debug_assert!(overlap > 0); let a_key_len = a_key.len(); @@ -1345,10 +1374,13 @@ fn merge_guts<'a, V: Clone + Lattice + Send + Sync, A: Allocator, const ASLOT: u unsafe{ intermediate_node.set_payload_owned::<0>(&a_key[overlap..], a_payload); } debug_assert!(validate_node(&intermediate_node)); let intermediate_node = TrieNodeODRc::new_in(intermediate_node, a.alloc.clone()); - return match b_child.pjoin(&intermediate_node) { + //`a` is the left operand of this merge, so its payload must be the left operand + // of the join (the join is left-biased on colliding values). + return match intermediate_node.pjoin(b_child) { AlgebraicResult::Element(joined) => AlgebraicResult::Element((&a_key[0..overlap], ValOrChild::Child(joined))), - //`b`'s child already held `a`'s payload, so `b`'s slot is the result - AlgebraicResult::Identity(mask) if mask & SELF_IDENT > 0 => AlgebraicResult::Identity(COUNTER_IDENT), + //`b`'s child already held `a`'s payload, so `b`'s slot is the result. COUNTER_IDENT, + // not SELF_IDENT: `b_child` is the right operand now that `a` is on the left. + AlgebraicResult::Identity(mask) if mask & COUNTER_IDENT > 0 => AlgebraicResult::Identity(COUNTER_IDENT), AlgebraicResult::Identity(_) => AlgebraicResult::Element((&a_key[0..overlap], ValOrChild::Child(intermediate_node))), AlgebraicResult::None => unreachable!(), //`intermediate_node` is never empty } @@ -2659,7 +2691,7 @@ impl TrieNode for LineListNode DENSE_BYTE_NODE_TAG => { let other_dense_node = unsafe{ other.as_dense_unchecked() }; let mut new_node = other_dense_node.clone(); - match new_node.merge_from_list_node(self) { + match new_node.merge_from_list_node(self, true) { //Both nodes were empty so the join is empty too AlgebraicStatus::None => { debug_assert!(self.node_is_empty() && other_dense_node.node_is_empty()); @@ -2676,7 +2708,7 @@ impl TrieNode for LineListNode CELL_BYTE_NODE_TAG => { let other_cell_node = unsafe{ other.as_cell_unchecked() }; let mut new_node = other_cell_node.clone_as_dense(); - match new_node.merge_from_list_node(self) { + match new_node.merge_from_list_node(self, true) { //See the DENSE_BYTE_NODE_TAG arm: two empty nodes join to an empty result AlgebraicStatus::None => { debug_assert!(self.node_is_empty() && other_cell_node.node_is_empty()); @@ -2712,7 +2744,7 @@ impl TrieNode for LineListNode DENSE_BYTE_NODE_TAG => { let other_dense_node = unsafe{ other_node.as_dense_unchecked() }; let mut new_node = other_dense_node.clone(); - let status = new_node.merge_from_list_node(self); + let status = new_node.merge_from_list_node(self, true); debug_assert!(!status.is_none()); (AlgebraicStatus::Element, Err(TrieNodeODRc::new_in(new_node, self.alloc.clone()))) }, @@ -2722,7 +2754,7 @@ impl TrieNode for LineListNode }, CELL_BYTE_NODE_TAG => { let mut new_node = unsafe{ other_node.as_cell_unchecked() }.clone_as_dense(); - let status = new_node.merge_from_list_node(self); + let status = new_node.merge_from_list_node(self, true); debug_assert!(!status.is_none()); (AlgebraicStatus::Element, Err(TrieNodeODRc::new_in(new_node, self.alloc.clone()))) }, @@ -2882,45 +2914,63 @@ impl TrieNode for LineListNode return Some(TrieNodeODRc::new_in(temp_node, self.alloc.clone())) } - //The final case is to construct a brand new node from the remaining parts of the key after we have - // discarded what we can discard and then merged together what's left. And then call this function - // recursively on the newly merged nodes - let chop_bytes = key0_len.min(key1_len); - debug_assert!(chop_bytes <= byte_cnt); - debug_assert!(chop_bytes > 0); - let new_key0 = &key0[chop_bytes-1..]; - let new_key1 = &key1[chop_bytes-1..]; - - let overlap = find_prefix_overlap(&key0[chop_bytes..], &key1[chop_bytes..]); - let merged_payload = match merge_guts::(overlap+1, new_key0, &temp_node, new_key1, &temp_node) { - AlgebraicResult::Element((_shared_key, merged_payload)) => merged_payload, - AlgebraicResult::Identity(mask) => { - if mask & SELF_IDENT > 0 { - temp_node.clone_payload::<0>().unwrap() - } else { - debug_assert_eq!(mask, COUNTER_IDENT); - temp_node.clone_payload::<1>().unwrap() - } - }, - AlgebraicResult::None => unreachable!() //`merge_guts` shouldn't return AlgebraicResult::None because that should have been caught by an earlier case + //The final case: at least one key is no longer than `byte_cnt`. Drop the bytes from each + // slot on its own and join the two results, slot 0 (the lexicographically smaller key) on + // the left. That is the order `PathMap::drop_head` is specified in -- a fold over the + // k-paths in sorted order, keeping the first value on a collision -- and it is what the + // byte node does one level up. Merging the two slots at an intermediate depth and then + // dropping the remaining bytes, as this used to, joins the subtries in a different order + // and keeps different values. + let mut key0_buf: [MaybeUninit; KEY_BYTES_CNT] = [MaybeUninit::new(0); KEY_BYTES_CNT]; + let mut key1_buf: [MaybeUninit; KEY_BYTES_CNT] = [MaybeUninit::new(0); KEY_BYTES_CNT]; + let (key0, key1) = unsafe { + core::ptr::copy_nonoverlapping(key0.as_ptr(), key0_buf.as_mut_ptr().cast::(), key0_len); + core::ptr::copy_nonoverlapping(key1.as_ptr(), key1_buf.as_mut_ptr().cast::(), key1_len); + (core::slice::from_raw_parts(key0_buf.as_ptr().cast::(), key0_len), + core::slice::from_raw_parts(key1_buf.as_ptr().cast::(), key1_len)) }; - - if let ValOrChild::Child(mut child_node) = merged_payload { - //A dangling child (the empty sentinel) has nothing below the dropped bytes and can't be made mutable - if child_node.is_empty() { - return None - } - if chop_bytes == byte_cnt { - return Some(child_node) - } else { - return child_node.make_mut().drop_head_dyn(byte_cnt-chop_bytes) + //Take slot 1 first: taking slot 0 would shift slot 1 into its place. + let payload1 = temp_node.take_payload::<1>().unwrap(); + let payload0 = temp_node.take_payload::<0>().unwrap(); + let dropped0 = drop_head_from_payload(key0, payload0, byte_cnt, &self.alloc); + let dropped1 = drop_head_from_payload(key1, payload1, byte_cnt, &self.alloc); + match (dropped0, dropped1) { + (None, None) => None, + (Some(node), None) | (None, Some(node)) => Some(node), + (Some(node0), Some(node1)) => match node0.pjoin(&node1) { + AlgebraicResult::Element(joined) => Some(joined), + AlgebraicResult::Identity(mask) => Some(if mask & SELF_IDENT > 0 { node0 } else { node1 }), + AlgebraicResult::None => None, } } - - unreachable!() } fn pmeet_dyn(&self, other: TaggedNodeRef) -> AlgebraicResult> where V: Lattice { + self.pmeet_dyn_oriented(other, false) + } + fn psubtract_dyn(&self, other: TaggedNodeRef) -> AlgebraicResult> where V: DistributiveLattice { + debug_assert!(validate_node(self)); + let slot0_result = self.subtract_from_slot_contents::<0>(other); + let slot1_result = self.subtract_from_slot_contents::<1>(other); + self.combine_slot_results_into_node_result(slot0_result, slot1_result) + } + fn prestrict_dyn(&self, other: TaggedNodeRef) -> AlgebraicResult> { + debug_assert!(validate_node(self)); + let slot0_result = self.restrict_slot_contents::<0>(other); + let slot1_result = self.restrict_slot_contents::<1>(other); + self.combine_slot_results_into_node_result(slot0_result, slot1_result) + } + fn clone_self(&self) -> TrieNodeODRc { + TrieNodeODRc::new_in(self.clone(), self.alloc.clone()) + } +} + +impl LineListNode { + /// The body of [TrieNode::pmeet_dyn]. `swapped` means `self` is really the *right* operand of + /// the meet and `other` the left one; see [pmeet_generic]. A node type that cannot enumerate + /// its own payloads cheaply (a `ByteNode`) meets a list node by calling this with `swapped = + /// true` and inverting the identity mask of the result. + pub(crate) fn pmeet_dyn_oriented(&self, other: TaggedNodeRef, swapped: bool) -> AlgebraicResult> where V: Lattice { debug_assert!(validate_node(self)); let mut self_payloads_buf: [(&[u8], PayloadRef); 2] = [(&[], PayloadRef::None); 2]; @@ -2945,7 +2995,7 @@ impl TrieNode for LineListNode _ => unsafe{ unreachable_unchecked() } }; - pmeet_generic::<2, V, A, _>(self_payloads, other, |payloads| { + pmeet_generic::<2, V, A, _>(self_payloads, other, swapped, |payloads| { debug_assert_eq!(payloads.len(), self_payloads.len()); let slot0_payload = payloads.get_mut(0).and_then(|p| core::mem::take(p)).map(|p| p.into()); let slot1_payload = payloads.get_mut(1).and_then(|p| core::mem::take(p)).map(|p| p.into()); @@ -2953,21 +3003,6 @@ impl TrieNode for LineListNode TrieNodeODRc::new_in(new_node, self.alloc.clone()) }) } - fn psubtract_dyn(&self, other: TaggedNodeRef) -> AlgebraicResult> where V: DistributiveLattice { - debug_assert!(validate_node(self)); - let slot0_result = self.subtract_from_slot_contents::<0>(other); - let slot1_result = self.subtract_from_slot_contents::<1>(other); - self.combine_slot_results_into_node_result(slot0_result, slot1_result) - } - fn prestrict_dyn(&self, other: TaggedNodeRef) -> AlgebraicResult> { - debug_assert!(validate_node(self)); - let slot0_result = self.restrict_slot_contents::<0>(other); - let slot1_result = self.restrict_slot_contents::<1>(other); - self.combine_slot_results_into_node_result(slot0_result, slot1_result) - } - fn clone_self(&self) -> TrieNodeODRc { - TrieNodeODRc::new_in(self.clone(), self.alloc.clone()) - } } impl LineListNode { diff --git a/src/morphisms.rs b/src/morphisms.rs index 2a3b4acc..8a546c68 100644 --- a/src/morphisms.rs +++ b/src/morphisms.rs @@ -999,7 +999,7 @@ pub(crate) fn new_map_from_ana_in(w: W, mut alg_f: Alg }, // Path from a graft, we shouldn't descend WOrNode::Node(node) => { - z.core().graft_internal(Some(node)); + z.core().graft_internal(Some(node), true); z.ascend(child_path_len); } } diff --git a/src/ring.rs b/src/ring.rs index 100edaed..1b434aa2 100644 --- a/src/ring.rs +++ b/src/ring.rs @@ -754,6 +754,22 @@ fn option_subtract_test() { assert_eq!(Some(Some(Some(()))).psubtract(&Some(Some(Some(())))), AlgebraicResult::None); } +/// Subtracting a value that isn't there leaves the destination alone, and the integer placeholders +/// have to say so with `Identity(SELF_IDENT)`. Returning `Element(*self)` is the same value, but +/// the node algebra propagates identity *masks*, not values, so an `Element` anywhere below a node +/// forces the whole node -- and with it `subtract_into` -- to report `Element` for a trie that did +/// not change. +#[test] +fn integer_subtract_is_self_identity() { + assert_eq!(3u64.psubtract(&5), AlgebraicResult::Identity(SELF_IDENT)); + assert_eq!(3u64.psubtract(&3), AlgebraicResult::None); + assert_eq!(3u16.psubtract(&5), AlgebraicResult::Identity(SELF_IDENT)); + assert_eq!(3u16.psubtract(&3), AlgebraicResult::None); + //The same, seen through `Option`, which is what the co-free node payloads use + assert_eq!(Some(3u64).psubtract(&Some(5)), AlgebraicResult::Identity(SELF_IDENT)); + assert_eq!(Some(3u64).psubtract(&Some(3)), AlgebraicResult::None); +} + // =-**-==-**-==-**-==-**-==-**-==-**-==-**-==-**-==-**-==-**-==-**-==-**-==-**-==-**-==-**-==-**-==-**-= // =-* `Option<&V>` *-= @@ -873,7 +889,7 @@ impl Lattice for u64 { impl DistributiveLattice for u64 { fn psubtract(&self, other: &Self) -> AlgebraicResult where Self: Sized { if self == other { AlgebraicResult::None } - else { AlgebraicResult::Element(*self) } + else { AlgebraicResult::Identity(SELF_IDENT) } } } @@ -893,7 +909,7 @@ impl Lattice for u16 { impl DistributiveLattice for u16 { fn psubtract(&self, other: &Self) -> AlgebraicResult { if self == other { AlgebraicResult::None } - else { AlgebraicResult::Element(*self) } + else { AlgebraicResult::Identity(SELF_IDENT) } } } diff --git a/src/trie_node.rs b/src/trie_node.rs index 19b7031b..1e79f9e2 100644 --- a/src/trie_node.rs +++ b/src/trie_node.rs @@ -646,7 +646,16 @@ impl ValOrChildUnion { // was observed. Therefore the the ~20% slowdown is simply the higher overheads of this generic function. // //The next port of call for optimization is probably to remove the recursion -pub(crate) fn pmeet_generic(self_payloads: &[(&[u8], PayloadRef)], other: TaggedNodeRef, merge_f: MergeF) -> AlgebraicResult> +// +/// `swapped` says which operand `self_payloads` came from. The meet is left-biased (a `Lattice` +/// impl resolves a collision as `left.pmeet(right)`), so when a caller enumerates the *right* +/// operand's payloads because that node type is the easier one to iterate, it passes `swapped = +/// true`: every value and every recursive node meet is then computed as `other op self` and the +/// identity masks are re-expressed relative to `self_payloads`. The caller still applies +/// `invert_identity()` to the final result to get back to its own orientation. Without this, a +/// dense-node-versus-list-node meet returned the list node's values regardless of which side it +/// was on. +pub(crate) fn pmeet_generic(self_payloads: &[(&[u8], PayloadRef)], other: TaggedNodeRef, swapped: bool, merge_f: MergeF) -> AlgebraicResult> where MergeF: FnOnce(&mut [Option>]) -> TrieNodeODRc, V: Clone + Send + Sync + Lattice @@ -661,7 +670,7 @@ pub(crate) fn pmeet_generic(self_payloads, &mut request_keys[..], &mut request_results[..], &mut element_results[..], other); + let is_exhaustive = pmeet_generic_internal::(self_payloads, &mut request_keys[..], &mut request_results[..], &mut element_results[..], other, swapped); let mut is_none = true; let mut combined_mask = SELF_IDENT | COUNTER_IDENT; let mut result_payloads = ArrayVec::>, MAX_PAYLOAD_CNT>::new(); @@ -701,7 +710,7 @@ pub(crate) fn node_count_branches_recursive(self_payloads: &[(&[u8], PayloadRef)], keys: &mut [(&[u8], bool)], request_results: &mut [(usize, PayloadRef<'trie, V, A>)], results: &mut [FatAlgebraicResult>], other_node: TaggedNodeRef<'trie, V, A>) -> bool +pub(crate) fn pmeet_generic_internal<'trie, const MAX_PAYLOAD_CNT: usize, V, A: Allocator>(self_payloads: &[(&[u8], PayloadRef)], keys: &mut [(&[u8], bool)], request_results: &mut [(usize, PayloadRef<'trie, V, A>)], results: &mut [FatAlgebraicResult>], other_node: TaggedNodeRef<'trie, V, A>, swapped: bool) -> bool where V: Clone + Send + Sync + Lattice { //If is_exhaustive gets set to `false`, then the pmeet method cannot return a `COUNTER_IDENTITY` result @@ -733,14 +742,14 @@ pub(crate) fn pmeet_generic_internal<'trie, const MAX_PAYLOAD_CNT: usize, V, A: // we have the same node as the previous time through the loop if cur_group.is_some() { if (cur_group.as_ref().unwrap().1 as *const TrieNodeODRc) != (child as *const TrieNodeODRc) { - pmeet_generic_recursive_reset::(&mut cur_group, &mut is_exhaustive, idx, self_payloads, keys, request_results, results); + pmeet_generic_recursive_reset::(&mut cur_group, &mut is_exhaustive, idx, self_payloads, keys, request_results, results, swapped); cur_group = Some((idx, child)); } } else { cur_group = Some((idx, child)); } } else { - pmeet_generic_recursive_reset::(&mut cur_group, &mut is_exhaustive, idx, self_payloads, keys, request_results, results); + pmeet_generic_recursive_reset::(&mut cur_group, &mut is_exhaustive, idx, self_payloads, keys, request_results, results, swapped); //We've arrived at a contained value or onward link that has a correspondence // to one of the values or links in `self` @@ -749,13 +758,13 @@ pub(crate) fn pmeet_generic_internal<'trie, const MAX_PAYLOAD_CNT: usize, V, A: let result = match &self_payloads[idx].1 { PayloadRef::Child(self_link) => { let other_link = payload.child(); - let result = self_link.pmeet(other_link); + let result = if swapped { other_link.pmeet(self_link).invert_identity() } else { self_link.pmeet(other_link) }; FatAlgebraicResult::from_binary_op_result(result, self_link, other_link) .map(|child| ValOrChild::Child(child)) }, PayloadRef::Val(self_val) => { let other_val = payload.val(); - let result = (*self_val).pmeet(other_val); + let result = if swapped { other_val.pmeet(*self_val).invert_identity() } else { (*self_val).pmeet(other_val) }; FatAlgebraicResult::from_binary_op_result(result, *self_val, other_val) .map(|val| ValOrChild::Val(val)) }, @@ -766,13 +775,17 @@ pub(crate) fn pmeet_generic_internal<'trie, const MAX_PAYLOAD_CNT: usize, V, A: results[idx] = result; } } else { - pmeet_generic_recursive_reset::(&mut cur_group, &mut is_exhaustive, idx, self_payloads, keys, request_results, results); + pmeet_generic_recursive_reset::(&mut cur_group, &mut is_exhaustive, idx, self_payloads, keys, request_results, results, swapped); let result = match &self_payloads[idx].1 { PayloadRef::Child(self_link) => { match other_node.get_node_at_key(keys[idx].0).into_option() { Some(other_onward_node) => { - let result = self_link.as_tagged().pmeet_dyn(other_onward_node.as_tagged()); + let result = if swapped { + other_onward_node.as_tagged().pmeet_dyn(self_link.as_tagged()).invert_identity() + } else { + self_link.as_tagged().pmeet_dyn(other_onward_node.as_tagged()) + }; FatAlgebraicResult::from_binary_op_result(result, self_link, &other_onward_node) .map(|child| ValOrChild::Child(child)) }, @@ -795,7 +808,7 @@ pub(crate) fn pmeet_generic_internal<'trie, const MAX_PAYLOAD_CNT: usize, V, A: results[idx] = result; } } - pmeet_generic_recursive_reset::(&mut cur_group, &mut is_exhaustive, keys.len(), self_payloads, keys, request_results, results); + pmeet_generic_recursive_reset::(&mut cur_group, &mut is_exhaustive, keys.len(), self_payloads, keys, request_results, results, swapped); is_exhaustive } @@ -803,7 +816,7 @@ pub(crate) fn pmeet_generic_internal<'trie, const MAX_PAYLOAD_CNT: usize, V, A: /// Effectively part of `pmeet_generic_internal`, but factored out separately because it's called in /// several different places. Resets the `cur_group` state and does a recursive call of `pmeet_generic_internal` #[inline] -fn pmeet_generic_recursive_reset<'trie, const MAX_PAYLOAD_CNT: usize, V, A: Allocator>(cur_group: &mut Option<(usize, &'trie TrieNodeODRc)>, is_exhaustive: &mut bool, idx: usize, self_payloads: &[(&[u8], PayloadRef)], keys: &mut [(&[u8], bool)], request_results: &mut [(usize, PayloadRef<'trie, V, A>)], results: &mut [FatAlgebraicResult>]) +fn pmeet_generic_recursive_reset<'trie, const MAX_PAYLOAD_CNT: usize, V, A: Allocator>(cur_group: &mut Option<(usize, &'trie TrieNodeODRc)>, is_exhaustive: &mut bool, idx: usize, self_payloads: &[(&[u8], PayloadRef)], keys: &mut [(&[u8], bool)], request_results: &mut [(usize, PayloadRef<'trie, V, A>)], results: &mut [FatAlgebraicResult>], swapped: bool) where V: Clone + Send + Sync + Lattice { match core::mem::take(cur_group) { @@ -811,7 +824,7 @@ fn pmeet_generic_recursive_reset<'trie, const MAX_PAYLOAD_CNT: usize, V, A: Allo let group_keys = &mut keys[group_start..idx]; let group_results = &mut results[group_start..idx]; let group_self_payloads = &self_payloads[group_start..idx]; - if !pmeet_generic_internal::(group_self_payloads, group_keys, request_results, group_results, next_node.as_tagged()) { + if !pmeet_generic_internal::(group_self_payloads, group_keys, request_results, group_results, next_node.as_tagged(), swapped) { *is_exhaustive = false; } }, @@ -3474,6 +3487,89 @@ mod tests { use crate::PathMap; use crate::zipper::*; + fn mk(ps: &[(&[u8], u64)]) -> PathMap { + let mut m = PathMap::::new(); + for (p, v) in ps { m.set_val_at(p, *v); } + m + } + fn vals(m: &PathMap) -> Vec<(Vec, u64)> { + m.iter().map(|(p, v)| (p.to_vec(), *v)).collect() + } + + /// `Lattice for u64` keeps `self` on a collision, so a meet carries the *left* operand's value. + /// That must not depend on which node type each operand happens to be stored in: a byte node + /// meeting a list node used to run the meet with the operands swapped and returned the list + /// node's values whichever side it was on. Found by lean/differential.py. + #[test] + fn meet_value_bias_is_left_regardless_of_node_layout() { + let two_payload_list = mk(&[(&[0], 0), (&[0, 0], 0), (&[3, 0], 1)]); + let single_line = mk(&[(&[0], 1)]); + let dense = mk(&[(&[0], 0), (&[1], 0), (&[2], 0), (&[3], 0), (&[4], 0)]); + for (a, b, expect) in [ + (&two_payload_list, &single_line, 0u64), + (&single_line, &two_payload_list, 1), + (&dense, &single_line, 0), + (&single_line, &dense, 1), + (&dense, &two_payload_list, 0), + (&two_payload_list, &dense, 0), + ] { + let mut out = PathMap::::new(); + { let mut wz = out.write_zipper(); wz.meet_2(&a.read_zipper(), &b.read_zipper()); } + assert_eq!(out.get_val_at(&[0]), Some(&expect), "meet_2 of {:?} and {:?}", vals(a), vals(b)); + + let mut into = a.clone(); + { let mut wz = into.write_zipper(); wz.meet_into(&b.read_zipper(), false); } + assert_eq!(into.get_val_at(&[0]), Some(&expect), "meet_into of {:?} and {:?}", vals(a), vals(b)); + } + } + + /// The same for joins: `PathMap::join` and `join_into` keep the left operand's value, whether + /// the left operand is a list node joining into a byte node or the other way round. + #[test] + fn join_value_bias_is_left_regardless_of_node_layout() { + let line = mk(&[(&[1], 0)]); + let dense = mk(&[(&[0], 0), (&[1], 1), (&[2], 0)]); + assert_eq!(line.join(&dense).get_val_at(&[1]), Some(&0)); + assert_eq!(dense.join(&line).get_val_at(&[1]), Some(&1)); + + let mut into = line.clone(); + { let mut wz = into.write_zipper(); wz.join_into(&dense.read_zipper()); } + assert_eq!(vals(&into), vec![(vec![0], 0), (vec![1], 0), (vec![2], 0)]); + let mut into = dense.clone(); + { let mut wz = into.write_zipper(); wz.join_into(&line.read_zipper()); } + assert_eq!(vals(&into), vec![(vec![0], 0), (vec![1], 1), (vec![2], 0)]); + + //A deeper collision, so the child-node join is exercised as well as the value join + let line = mk(&[(&[1, 5], 0), (&[1, 6], 0)]); + let dense = mk(&[(&[0], 0), (&[1, 5], 1), (&[2], 0)]); + assert_eq!(line.join(&dense).get_val_at(&[1, 5]), Some(&0)); + assert_eq!(dense.join(&line).get_val_at(&[1, 5]), Some(&1)); + } + + /// `join_k_path_into` joins the surviving subtries in path order (`PathMap.dropHead` in the + /// Lean model folds over the k-paths in sorted order), so on a collision the value from the + /// lexicographically first k-path survives. The byte node used to fold from the highest byte + /// down, and the list node's two-slot merge used to join with the second slot on the left. + #[test] + fn join_k_path_into_keeps_lexicographically_first_value() { + let mut m = mk(&[(&[0, 0, 0, 2], 0), (&[0, 1, 0, 2], 1), (&[0, 1, 0, 2, 0], 0)]); + { let mut wz = m.write_zipper(); wz.join_k_path_into(3, false); } + assert_eq!(vals(&m), vec![(vec![2], 0), (vec![2, 0], 0)]); + + let mut m = mk(&[(&[1, 0, 3], 0), (&[0], 0), (&[0, 0, 0], 0), (&[0, 0, 3], 1)]); + { let mut wz = m.write_zipper(); wz.join_k_path_into(2, false); } + assert_eq!(vals(&m), vec![(vec![0], 0), (vec![3], 1)]); + + let mut m = mk(&[(&[0, 0, 0], 0), (&[0], 0), (&[1, 0, 0], 1)]); + { let mut wz = m.write_zipper(); wz.join_k_path_into(2, false); } + assert_eq!(vals(&m), vec![(vec![0], 0)]); + + //Three-plus branches at the root make it a byte node + let mut m = mk(&[(&[0, 0, 7], 0), (&[1, 0, 7], 1), (&[2, 0, 7], 2), (&[3, 0, 7], 3)]); + { let mut wz = m.write_zipper(); wz.join_k_path_into(2, false); } + assert_eq!(vals(&m), vec![(vec![7], 0)]); + } + #[test] fn slim_ptrs_test1() { let map = PathMap::<()>::new(); diff --git a/src/write_zipper.rs b/src/write_zipper.rs index 141128f9..f0d8d079 100644 --- a/src/write_zipper.rs +++ b/src/write_zipper.rs @@ -141,7 +141,7 @@ pub trait ZipperWriting: Wri /// avoid unnecessarily large allocations. fn graft_masked_branches>(&mut self, src: &Z, child_mask: ByteMask, remove_unset: bool) { if remove_unset { - self.remove_branches(false); + self.remove_branches(true); } for child_byte in child_mask.iter() { @@ -1506,35 +1506,35 @@ impl <'a, 'path, V: Clone + Send + Sync + Unpin, A: Allocator + 'a> WriteZipperC } /// See [ZipperWriting::graft] pub fn graft>(&mut self, read_zipper: &Z) { - self.graft_internal(read_zipper.get_focus().into_option()); + self.graft_internal(read_zipper.get_focus().into_option(), true); #[cfg(feature = "graft_root_vals")] let _ = match read_zipper.val() { Some(src_val) => self.set_val(src_val.clone()), - None => self.remove_val(false) + None => self.remove_val(true) }; } /// See [ZipperWriting::graft_src_at] fn graft_src_at, K: AsRef<[u8]>>(&mut self, src: &Z, path: K) { - self.graft_internal(src.get_focus_at(&path).into_option()); + self.graft_internal(src.get_focus_at(&path).into_option(), true); #[cfg(feature = "graft_root_vals")] let _ = match src.val_at(&path) { Some(src_val) => self.set_val(src_val.clone()), - None => self.remove_val(false) + None => self.remove_val(true) }; } /// See [ZipperWriting::graft_map] pub fn graft_map(&mut self, map: PathMap) { let (src_root_node, src_root_val) = map.into_root(); - self.graft_internal(src_root_node); + self.graft_internal(src_root_node, true); #[cfg(not(feature = "graft_root_vals"))] let _ = src_root_val; #[cfg(feature = "graft_root_vals")] let _ = match src_root_val { Some(src_val) => self.set_val(src_val), - None => self.remove_val(false) + None => self.remove_val(true) }; } /// Internal helper called by graft_masked_branches @@ -1572,12 +1572,12 @@ impl <'a, 'path, V: Clone + Send + Sync + Unpin, A: Allocator + 'a> WriteZipperC match child_mask.count_bits() { 0 => { if remove_unset { - self.remove_branches(false); + self.remove_branches(true); } } 1 => { if remove_unset { - self.remove_branches(false); + self.remove_branches(true); } // SAFETY: this arm is selected only when `child_mask` has one bit. let byte = unsafe { child_mask.indexed_bit::(0).unwrap_unchecked() }; @@ -1587,7 +1587,7 @@ impl <'a, 'path, V: Clone + Send + Sync + Unpin, A: Allocator + 'a> WriteZipperC } 2 => { if remove_unset { - self.remove_branches(false); + self.remove_branches(true); } // SAFETY: this arm is selected only when `child_mask` has two bits. let first_byte = unsafe { child_mask.indexed_bit::(0).unwrap_unchecked() }; @@ -1662,23 +1662,31 @@ impl <'a, 'path, V: Clone + Send + Sync + Unpin, A: Allocator + 'a> WriteZipperC }, TaggedNodeRef::EmptyNode => { if remove_unset { - self.remove_branches(false); + self.remove_branches(true); } else { - self.remove_unmasked_branches(child_mask.not(), false); + self.remove_unmasked_branches(child_mask.not(), true); } }, } if let Some(node) = fresh_node { if !node.as_tagged().node_is_empty() { - self.graft_internal(Some(node)); + self.graft_internal(Some(node), true); } } + // `merge_branches_into_focus` writes through a borrow of the + // focus node, so there is no `graft_internal` on this path to + // notice that the merge emptied it. A mask bit whose branch + // the source lacks removes that branch, and a mask of only + // such bits removes them all -- leaving a focus that leads + // nowhere. `prune_path` is a no-op unless the focus really is + // a dangling tip, so this costs a node_is_empty check. + self.prune_path(); }, None => { if remove_unset { - self.remove_branches(false); + self.remove_branches(true); } else { - self.remove_unmasked_branches(child_mask.not(), false); + self.remove_unmasked_branches(child_mask.not(), true); } } } @@ -1712,11 +1720,11 @@ impl <'a, 'path, V: Clone + Send + Sync + Unpin, A: Allocator + 'a> WriteZipperC } } let new_node_odrc = TrieNodeODRc::new_in(new_node, self.alloc.clone()); - self.graft_internal(Some(new_node_odrc)); + self.graft_internal(Some(new_node_odrc), true); } else { // If we don't have enough children to justify forcing a new ByteNode, just set the nodes if remove_unset { - self.remove_branches(false); + self.remove_branches(true); } let mut maps_iter = maps.into_iter(); for child_byte in child_mask.iter() { @@ -1792,7 +1800,7 @@ impl <'a, 'path, V: Clone + Send + Sync + Unpin, A: Allocator + 'a> WriteZipperC Some(self_node) => { match self_node.pjoin_dyn(src.as_tagged()) { AlgebraicResult::Element(joined) => { - self.graft_internal(Some(joined)); + self.graft_internal(Some(joined), true); AlgebraicStatus::Element } AlgebraicResult::Identity(mask) => { @@ -1800,18 +1808,18 @@ impl <'a, 'path, V: Clone + Send + Sync + Unpin, A: Allocator + 'a> WriteZipperC AlgebraicStatus::Identity } else { debug_assert!(mask & COUNTER_IDENT > 0); - self.graft_internal(src.into_option()); + self.graft_internal(src.into_option(), true); AlgebraicStatus::Element } }, AlgebraicResult::None => { - self.graft_internal(None); + self.graft_internal(None, true); AlgebraicStatus::None } } }, // No destination node, or an empty one: the result is the source. - None => { self.graft_internal(src.into_option()); AlgebraicStatus::Element } + None => { self.graft_internal(src.into_option(), true); AlgebraicStatus::Element } } } /// See [ZipperWriting::join_map_into] @@ -1846,7 +1854,7 @@ impl <'a, 'path, V: Clone + Send + Sync + Unpin, A: Allocator + 'a> WriteZipperC Some(self_node) => { match self_node.pjoin_dyn(src.as_tagged()) { AlgebraicResult::Element(joined) => { - self.graft_internal(Some(joined)); + self.graft_internal(Some(joined), true); AlgebraicStatus::Element }, AlgebraicResult::Identity(mask) => { @@ -1854,17 +1862,17 @@ impl <'a, 'path, V: Clone + Send + Sync + Unpin, A: Allocator + 'a> WriteZipperC AlgebraicStatus::Identity } else { debug_assert!(mask & COUNTER_IDENT > 0); - self.graft_internal(Some(src)); + self.graft_internal(Some(src), true); AlgebraicStatus::Element } }, AlgebraicResult::None => { - self.graft_internal(None); + self.graft_internal(None, true); AlgebraicStatus::None } } }, - None => { self.graft_internal(Some(src)); AlgebraicStatus::Element } + None => { self.graft_internal(Some(src), true); AlgebraicStatus::Element } }; #[cfg(not(feature = "graft_root_vals"))] @@ -1893,11 +1901,11 @@ impl <'a, 'path, V: Clone + Send + Sync + Unpin, A: Allocator + 'a> WriteZipperC // made mutable; the join into nothing is the source itself Some(mut self_node) if !self_node.as_tagged().node_is_empty() => { let status = self_node.join_into(src); - self.graft_internal(Some(self_node)); + self.graft_internal(Some(self_node), true); status }, _ => { - self.graft_internal(Some(src)); + self.graft_internal(Some(src), true); AlgebraicStatus::Element } } @@ -1914,7 +1922,7 @@ impl <'a, 'path, V: Clone + Send + Sync + Unpin, A: Allocator + 'a> WriteZipperC let new_node = self_node.make_mut().drop_head_dyn(byte_cnt) .filter(|node| !node.as_tagged().node_is_empty()); let result = new_node.is_some(); - self.graft_internal(new_node); + self.graft_internal(new_node, prune); result } else { !self_node.as_tagged().node_is_empty() @@ -2000,7 +2008,7 @@ impl <'a, 'path, V: Clone + Send + Sync + Unpin, A: Allocator + 'a> WriteZipperC return true; } let prefixed = make_parents_in(prefix, focus_node, self.alloc.clone()); - self.graft_internal(Some(prefixed)); + self.graft_internal(Some(prefixed), true); true }, None => { false } @@ -2013,7 +2021,7 @@ impl <'a, 'path, V: Clone + Send + Sync + Unpin, A: Allocator + 'a> WriteZipperC let fully_ascended = self.ascend(n) == n; - self.graft_internal(downstream_node); + self.graft_internal(downstream_node, true); fully_ascended } /// See [ZipperWriting::meet_into] @@ -2043,7 +2051,7 @@ impl <'a, 'path, V: Clone + Send + Sync + Unpin, A: Allocator + 'a> WriteZipperC node_was_none = false; let src = read_zipper.get_focus(); if src.is_none() { - self.graft_internal(None); + self.graft_internal(None, prune); if prune { self.prune_path(); } @@ -2051,11 +2059,11 @@ impl <'a, 'path, V: Clone + Send + Sync + Unpin, A: Allocator + 'a> WriteZipperC } else { match self_node.pmeet_dyn(src.as_tagged()) { AlgebraicResult::Element(intersection) => { - self.graft_internal(Some(intersection)); + self.graft_internal(Some(intersection), prune); AlgebraicStatus::Element }, AlgebraicResult::None => { - self.graft_internal(None); + self.graft_internal(None, prune); if prune { self.prune_path(); } @@ -2066,7 +2074,7 @@ impl <'a, 'path, V: Clone + Send + Sync + Unpin, A: Allocator + 'a> WriteZipperC AlgebraicStatus::Identity } else { debug_assert_eq!(mask, COUNTER_IDENT); //It's gotta be self or other - self.graft_internal(Some(src.into_option().unwrap())); + self.graft_internal(Some(src.into_option().unwrap()), prune); AlgebraicStatus::Element } }, @@ -2094,7 +2102,7 @@ impl <'a, 'path, V: Clone + Send + Sync + Unpin, A: Allocator + 'a> WriteZipperC let a = match a_focus.try_as_tagged() { Some(src) => src, None => { - self.graft_internal(None); + self.graft_internal(None, false); return AlgebraicStatus::None } }; @@ -2102,17 +2110,17 @@ impl <'a, 'path, V: Clone + Send + Sync + Unpin, A: Allocator + 'a> WriteZipperC let b = match b_focus.try_as_tagged() { Some(src) => src, None => { - self.graft_internal(None); + self.graft_internal(None, false); return AlgebraicStatus::None } }; match a.pmeet_dyn(b) { AlgebraicResult::Element(intersection) => { - self.graft_internal(Some(intersection)); + self.graft_internal(Some(intersection), true); AlgebraicStatus::Element }, AlgebraicResult::None => { - self.graft_internal(None); + self.graft_internal(None, false); AlgebraicStatus::None }, AlgebraicResult::Identity(mask) => { @@ -2124,12 +2132,12 @@ impl <'a, 'path, V: Clone + Send + Sync + Unpin, A: Allocator + 'a> WriteZipperC }; match src { Some(node) => { - self.graft_internal(Some(node)); + self.graft_internal(Some(node), true); AlgebraicStatus::Element } None => { //An empty result subtrie means clear the destination - self.graft_internal(None); + self.graft_internal(None, false); AlgebraicStatus::None } } @@ -2179,11 +2187,11 @@ impl <'a, 'path, V: Clone + Send + Sync + Unpin, A: Allocator + 'a> WriteZipperC node_was_none = false; match self_node.psubtract_dyn(src.as_tagged()) { AlgebraicResult::Element(diff) => { - self.graft_internal(Some(diff)); + self.graft_internal(Some(diff), prune); AlgebraicStatus::Element }, AlgebraicResult::None => { - self.graft_internal(None); + self.graft_internal(None, prune); if prune { self.prune_path(); } @@ -2211,18 +2219,18 @@ impl <'a, 'path, V: Clone + Send + Sync + Unpin, A: Allocator + 'a> WriteZipperC pub fn restrict>(&mut self, read_zipper: &Z) -> AlgebraicStatus { let src = read_zipper.get_focus(); if src.is_none() { - self.graft_internal(None); + self.graft_internal(None, true); return AlgebraicStatus::None } match self.get_focus().try_as_tagged() { Some(self_node) => { match self_node.prestrict_dyn(src.as_tagged()) { AlgebraicResult::Element(restricted) => { - self.graft_internal(Some(restricted)); + self.graft_internal(Some(restricted), true); AlgebraicStatus::Element }, AlgebraicResult::None => { - self.graft_internal(None); + self.graft_internal(None, true); AlgebraicStatus::None }, AlgebraicResult::Identity(mask) => { @@ -2243,11 +2251,11 @@ impl <'a, 'path, V: Clone + Send + Sync + Unpin, A: Allocator + 'a> WriteZipperC match self.get_focus().try_as_tagged() { Some(self_node) => { match src.as_tagged().prestrict_dyn(self_node) { - AlgebraicResult::Element(restricted) => self.graft_internal(Some(restricted)), - AlgebraicResult::None => self.graft_internal(None), + AlgebraicResult::Element(restricted) => self.graft_internal(Some(restricted), true), + AlgebraicResult::None => self.graft_internal(None, true), AlgebraicResult::Identity(mask) => { debug_assert_eq!(mask, SELF_IDENT); //restrict is non-commutative - self.graft_internal(src.into_option()) + self.graft_internal(src.into_option(), true) }, } true @@ -2413,7 +2421,7 @@ impl <'a, 'path, V: Clone + Send + Sync + Unpin, A: Allocator + 'a> WriteZipperC /// Internal implementation of graft, and other methods that do the same thing #[inline] - pub(crate) fn graft_internal(&mut self, src: Option>) { + pub(crate) fn graft_internal(&mut self, src: Option>, prune: bool) { match src { Some(src) => { debug_assert!(!src.as_tagged().node_is_empty()); @@ -2441,7 +2449,7 @@ impl <'a, 'path, V: Clone + Send + Sync + Unpin, A: Allocator + 'a> WriteZipperC *stack_root = src; } }, - None => { self.remove_branches(false); } + None => { self.remove_branches(prune); } } } @@ -4196,6 +4204,31 @@ mod tests { assert_eq!(remaining, vec![(vec![0], 0), (vec![0, 0, 0], 0)]); } + /// `subtract_into` where every value of the source collides with a *different* value in the + /// destination. Nothing annihilates, so the destination comes back untouched and the status + /// has to be `Identity`. The integer `psubtract` used to answer `Element(*self)`, and the node + /// algebra -- which propagates identity masks, not values -- turned that into `Element` for the + /// whole trie. + #[test] + fn write_zipper_subtract_into_unequal_values_is_identity() { + fn mk(ps: &[(&[u8], u64)]) -> PathMap { let mut m = PathMap::new(); for (p, v) in ps { m.set_val_at(p, *v); } m } + fn vals(m: &PathMap) -> Vec<(Vec, u64)> { m.iter().map(|(k, v)| (k.to_vec(), *v)).collect() } + + let mut dst = mk(&[(&[0], 1), (&[0, 0], 2), (&[1], 3), (&[2], 4)]); + let before = vals(&dst); + let src = mk(&[(&[0], 9), (&[0, 0], 9), (&[1], 9), (&[2], 9)]); + let st = { let mut wz = dst.write_zipper(); wz.subtract_into(&src.read_zipper(), false) }; + assert_eq!(st, AlgebraicStatus::Identity); + assert_eq!(vals(&dst), before); + + //An equal value still annihilates, and that is an `Element`, not an identity + let mut dst = mk(&[(&[0], 1), (&[0, 0], 2), (&[1], 3), (&[2], 4)]); + let src = mk(&[(&[0], 9), (&[0, 0], 2), (&[1], 9), (&[2], 9)]); + let st = { let mut wz = dst.write_zipper(); wz.subtract_into(&src.read_zipper(), false) }; + assert_eq!(st, AlgebraicStatus::Element); + assert_eq!(vals(&dst), vec![(vec![0], 1), (vec![1], 3), (vec![2], 4)]); + } + /// Tests how `subtract_into` handles dangling paths, including situations with extraneous empty nodes hanging around #[test] fn write_zipper_subtract_into_test2() {