Return Identity from integer psubtract of unequal values

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 -/

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<V>`, 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<Self> 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<Self> {
         if self == other { AlgebraicResult::None }
-        else { AlgebraicResult::Element(*self) }
+        else { AlgebraicResult::Identity(SELF_IDENT) }
     }
 }
 

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<u64> { let mut m = PathMap::new(); for (p, v) in ps { m.set_val_at(p, *v); } m }
+        fn vals(m: &PathMap<u64>) -> Vec<(Vec<u8>, 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)]);
+    }
 }