From b3ba1c4deddcf470ea294b9315051d99328a18f4 Mon Sep 17 00:00:00 2001 From: Igor Malovitsa Date: Wed, 16 Sep 2026 23:21:24 +0000 Subject: [PATCH] Return Identity from integer psubtract of unequal values u64 and u16 psubtract returned Element(*self) when nothing was subtracted. Nodes propagate identity masks, so subtract_into reported Element for an unchanged trie. The Lean model's u64Ops follows. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF --- lean/PathMapModel/Basic.lean | 10 +++++----- src/ring.rs | 16 ++++++++++++++-- src/write_zipper.rs | 21 +++++++++++++++++++++ 3 files changed, 40 insertions(+), 7 deletions(-) diff --git a/lean/PathMapModel/Basic.lean b/lean/PathMapModel/Basic.lean index ff22667f..e646941e 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,12 +63,12 @@ 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)`. 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 /-! ## Prefix order -/ diff --git a/src/ring.rs b/src/ring.rs index 4b9b1d45..1eeba5e8 100644 --- a/src/ring.rs +++ b/src/ring.rs @@ -754,6 +754,18 @@ fn option_subtract_test() { assert_eq!(Some(Some(Some(()))).psubtract(&Some(Some(Some(())))), AlgebraicResult::None); } +/// Subtracting a different value changes nothing, so it's `Identity` +#[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); + //Through `Option`, as co-free payloads use + assert_eq!(Some(3u64).psubtract(&Some(5)), AlgebraicResult::Identity(SELF_IDENT)); + assert_eq!(Some(3u64).psubtract(&Some(3)), AlgebraicResult::None); +} + // =-**-==-**-==-**-==-**-==-**-==-**-==-**-==-**-==-**-==-**-==-**-==-**-==-**-==-**-==-**-==-**-==-**-= // =-* `Option<&V>` *-= @@ -867,7 +879,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) } } } @@ -887,7 +899,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/write_zipper.rs b/src/write_zipper.rs index 0892e475..3806ad0e 100644 --- a/src/write_zipper.rs +++ b/src/write_zipper.rs @@ -6672,4 +6672,25 @@ mod tests { } assert_eq!(keys(&m), ["cx", "cy", "d"]); } + + /// `subtract_into` with only unequal values is `Identity` + #[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); + + //Equal values still annihilate + 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)]); + } }