From 314c82621c45203844255eafbad4bc3ce007f087 Mon Sep 17 00:00:00 2001 From: Ivan Zuzak Date: Thu, 16 Jul 2026 20:18:03 +0200 Subject: [PATCH 01/10] Avoid rechecking for duplicates in IdOrdMap::from_iter_unique --- crates/iddqd/src/id_ord_map/imp.rs | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/crates/iddqd/src/id_ord_map/imp.rs b/crates/iddqd/src/id_ord_map/imp.rs index 0b81b2c1..923a92fb 100644 --- a/crates/iddqd/src/id_ord_map/imp.rs +++ b/crates/iddqd/src/id_ord_map/imp.rs @@ -237,8 +237,8 @@ impl IdOrdMap { vec![duplicate], )); } - Entry::Vacant(entry) => { - entry.insert_ref(value); + Entry::Vacant(_) => { + map.insert_known_unique_impl(value); } } } @@ -1491,6 +1491,10 @@ impl IdOrdMap { } } + Ok(self.insert_known_unique_impl(value)) + } + + fn insert_known_unique_impl(&mut self, value: T) -> ItemIndex { // Take the `GrowHandle` after the read-only duplicate check but before // the B-tree mutation. With this approach, a panic from // `assert_can_grow` (which means that the map is full) cannot leave the @@ -1528,7 +1532,7 @@ impl IdOrdMap { grow_handle.insert(value); insert.insert(); - Ok(next_index) + next_index } pub(super) fn remove_by_index( From ae75a867e8fd1833946ac7ac320512595f41966c Mon Sep 17 00:00:00 2001 From: Ivan Zuzak Date: Thu, 16 Jul 2026 22:45:06 +0200 Subject: [PATCH 02/10] Add doc comment for new insert_known_unique_impl method --- crates/iddqd/src/id_ord_map/imp.rs | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/crates/iddqd/src/id_ord_map/imp.rs b/crates/iddqd/src/id_ord_map/imp.rs index 923a92fb..64579049 100644 --- a/crates/iddqd/src/id_ord_map/imp.rs +++ b/crates/iddqd/src/id_ord_map/imp.rs @@ -1494,6 +1494,11 @@ impl IdOrdMap { Ok(self.insert_known_unique_impl(value)) } + /// Inserts `value` without checking for duplicates. + /// + /// Only call this after verifying that `value` does not conflict with any + /// existing item. Callers that haven't determined uniqueness should use + /// `insert_unique_impl` instead. fn insert_known_unique_impl(&mut self, value: T) -> ItemIndex { // Take the `GrowHandle` after the read-only duplicate check but before // the B-tree mutation. With this approach, a panic from From 5f7ca4d95152958ffe8d0ffe28bc7dba90ec8373 Mon Sep 17 00:00:00 2001 From: Ivan Zuzak Date: Fri, 17 Jul 2026 10:07:21 +0200 Subject: [PATCH 03/10] Avoid rechecking for duplicates in IdOrdMap::insert_overwrite --- crates/iddqd/src/id_ord_map/imp.rs | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/crates/iddqd/src/id_ord_map/imp.rs b/crates/iddqd/src/id_ord_map/imp.rs index 9a97121d..1544ac74 100644 --- a/crates/iddqd/src/id_ord_map/imp.rs +++ b/crates/iddqd/src/id_ord_map/imp.rs @@ -756,13 +756,15 @@ impl IdOrdMap { // mutation. A panic in user code therefore leaves the map in its // pre-call state. // - // We use `vacant.insert_entry` rather than `vacant.insert` to avoid - // creating a `RefMut`, which would (unnecessarily) re-hash the key - // after the mutation when that `RefMut` is created. + // In the vacant case, the Entry lookup has already established that the + // key is unique. Calling `vacant.insert_entry` would route back through + // `insert_unique_impl` and check for duplicates again, while + // `vacant.insert` would also create a `RefMut` and re-hash the key. We + // use `insert_known_unique_impl` instead, which avoids both. match self.entry(value.key()) { Entry::Occupied(mut occupied) => Some(occupied.insert(value)), - Entry::Vacant(vacant) => { - vacant.insert_entry(value); + Entry::Vacant(_) => { + self.insert_known_unique_impl(value); None } } From c9bed35ab4750420a3264dad3ac1152b4d26e62e Mon Sep 17 00:00:00 2001 From: Ivan Zuzak Date: Fri, 17 Jul 2026 11:40:40 +0200 Subject: [PATCH 04/10] Avoid rechecking for duplicates in IdHashMap::insert_overwrite --- crates/iddqd/src/id_hash_map/imp.rs | 25 ++++++++++++++++++++----- 1 file changed, 20 insertions(+), 5 deletions(-) diff --git a/crates/iddqd/src/id_hash_map/imp.rs b/crates/iddqd/src/id_hash_map/imp.rs index d4ee0403..875f84c8 100644 --- a/crates/iddqd/src/id_hash_map/imp.rs +++ b/crates/iddqd/src/id_hash_map/imp.rs @@ -983,13 +983,15 @@ impl IdHashMap { // mutation. A panic in user code therefore leaves the map in its // pre-call state. // - // We use `vacant.insert_entry` rather than `vacant.insert` to avoid - // creating a `RefMut`, which would (unnecessarily) re-hash the key - // after the mutation when that `RefMut` is created. + // In the vacant case, the Entry lookup has already established that the + // key is unique. Calling `vacant.insert_entry` would route back through + // `insert_unique_impl` and check for duplicates again, while + // `vacant.insert` would also create a `RefMut` and re-hash the key. We + // use `insert_known_unique_impl` instead, which avoids both. match self.entry(value.key()) { Entry::Occupied(mut occupied) => Some(occupied.insert(value)), - Entry::Vacant(vacant) => { - vacant.insert_entry(value); + Entry::Vacant(_) => { + self.insert_known_unique_impl(value); None } } @@ -1464,6 +1466,19 @@ impl IdHashMap { Ok(next_index) } + /// Inserts `value` without checking for duplicates. + /// + /// Only call this after verifying that `value` does not conflict with any + /// existing item. Callers that cannot prove uniqueness should use + /// `insert_unique_impl` instead. + fn insert_known_unique_impl(&mut self, value: T) -> ItemIndex { + let hash = self.make_hash(&value); + self.tables.key_to_item.reserve(1); + let next_index = self.items.assert_can_grow().insert(value); + self.tables.key_to_item.insert_prehashed_unchecked(hash, next_index); + next_index + } + pub(super) fn remove_by_index( &mut self, remove_index: ItemIndex, From 2b951b68b1cc5399070f068ac66785c7bcdb95a0 Mon Sep 17 00:00:00 2001 From: Ivan Zuzak Date: Fri, 17 Jul 2026 11:49:52 +0200 Subject: [PATCH 05/10] Reserve capacity for new IdOrdMap in from_iter_unique --- crates/iddqd/src/id_ord_map/imp.rs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/crates/iddqd/src/id_ord_map/imp.rs b/crates/iddqd/src/id_ord_map/imp.rs index 1544ac74..27b44164 100644 --- a/crates/iddqd/src/id_ord_map/imp.rs +++ b/crates/iddqd/src/id_ord_map/imp.rs @@ -223,7 +223,8 @@ impl IdOrdMap { pub fn from_iter_unique>( iter: I, ) -> Result> { - let mut map = IdOrdMap::new(); + let iter = iter.into_iter(); + let mut map = IdOrdMap::with_capacity(iter.size_hint().0); for value in iter { // It would be nice to use insert_unique here, but that would return // a `DuplicateItem`, which can only be converted into an From 3017f0a16ab4a5ccfbef79be10120fd30ef44b0b Mon Sep 17 00:00:00 2001 From: Ivan Zuzak Date: Sun, 19 Jul 2026 09:52:04 +0200 Subject: [PATCH 06/10] Reuse vacant entry hash in IdHashMap::insert_overwrite --- crates/iddqd/src/id_hash_map/entry.rs | 15 +++++++++++++++ crates/iddqd/src/id_hash_map/imp.rs | 19 +++---------------- 2 files changed, 18 insertions(+), 16 deletions(-) diff --git a/crates/iddqd/src/id_hash_map/entry.rs b/crates/iddqd/src/id_hash_map/entry.rs index a4e16337..70fa65da 100644 --- a/crates/iddqd/src/id_hash_map/entry.rs +++ b/crates/iddqd/src/id_hash_map/entry.rs @@ -133,6 +133,21 @@ impl<'a, T: IdHashItem, S: Clone + BuildHasher, A: Allocator> map.get_by_index_mut(index).expect("index is known to be valid") } + /// Sets the entry to a new value without checking for duplicates or + /// recomputing its key hash. + /// + /// Only call this on a vacant entry obtained from `value.key()`. Unlike + /// `insert`, this method does not validate the hash or recheck uniqueness. + #[inline] + pub(super) fn insert_known_unique(self, value: T) { + // SAFETY: The safety assumption behind `Self::new` guarantees that the + // original reference to the map is not used at this point. + let map = unsafe { self.map.awaken() }; + map.tables.key_to_item.reserve(1); + let next_index = map.items.assert_can_grow().insert(value); + map.tables.key_to_item.insert_prehashed_unchecked(self.hash, next_index); + } + /// Sets the value of the entry, and returns an `OccupiedEntry`. #[inline] pub fn insert_entry(mut self, value: T) -> OccupiedEntry<'a, T, S, A> { diff --git a/crates/iddqd/src/id_hash_map/imp.rs b/crates/iddqd/src/id_hash_map/imp.rs index 875f84c8..f3484507 100644 --- a/crates/iddqd/src/id_hash_map/imp.rs +++ b/crates/iddqd/src/id_hash_map/imp.rs @@ -987,11 +987,11 @@ impl IdHashMap { // key is unique. Calling `vacant.insert_entry` would route back through // `insert_unique_impl` and check for duplicates again, while // `vacant.insert` would also create a `RefMut` and re-hash the key. We - // use `insert_known_unique_impl` instead, which avoids both. + // use `vacant.insert_known_unique` instead, which avoids both. match self.entry(value.key()) { Entry::Occupied(mut occupied) => Some(occupied.insert(value)), - Entry::Vacant(_) => { - self.insert_known_unique_impl(value); + Entry::Vacant(vacant) => { + vacant.insert_known_unique(value); None } } @@ -1466,19 +1466,6 @@ impl IdHashMap { Ok(next_index) } - /// Inserts `value` without checking for duplicates. - /// - /// Only call this after verifying that `value` does not conflict with any - /// existing item. Callers that cannot prove uniqueness should use - /// `insert_unique_impl` instead. - fn insert_known_unique_impl(&mut self, value: T) -> ItemIndex { - let hash = self.make_hash(&value); - self.tables.key_to_item.reserve(1); - let next_index = self.items.assert_can_grow().insert(value); - self.tables.key_to_item.insert_prehashed_unchecked(hash, next_index); - next_index - } - pub(super) fn remove_by_index( &mut self, remove_index: ItemIndex, From af2a01e710b8301f77d7a7eef13a701a7c6ec1f7 Mon Sep 17 00:00:00 2001 From: Ivan Zuzak Date: Sun, 19 Jul 2026 09:54:22 +0200 Subject: [PATCH 07/10] whoops, forgot cargo fmt --- crates/iddqd/src/id_hash_map/entry.rs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/crates/iddqd/src/id_hash_map/entry.rs b/crates/iddqd/src/id_hash_map/entry.rs index 70fa65da..dcb3ad7a 100644 --- a/crates/iddqd/src/id_hash_map/entry.rs +++ b/crates/iddqd/src/id_hash_map/entry.rs @@ -145,7 +145,9 @@ impl<'a, T: IdHashItem, S: Clone + BuildHasher, A: Allocator> let map = unsafe { self.map.awaken() }; map.tables.key_to_item.reserve(1); let next_index = map.items.assert_can_grow().insert(value); - map.tables.key_to_item.insert_prehashed_unchecked(self.hash, next_index); + map.tables + .key_to_item + .insert_prehashed_unchecked(self.hash, next_index); } /// Sets the value of the entry, and returns an `OccupiedEntry`. From 2a666fc9dc8f9e08873e093bff145428a0e34763 Mon Sep 17 00:00:00 2001 From: Rain Date: Sun, 19 Jul 2026 13:55:45 -0700 Subject: [PATCH 08/10] update Soteria proofs + comments --- crates/iddqd-soteria-runner/tests/runner.rs | 6 ++--- crates/iddqd/src/id_ord_map/imp.rs | 15 ++++++----- crates/iddqd/tests/soteria/bi_hash_map.rs | 14 ++++------ crates/iddqd/tests/soteria/id_hash_map.rs | 30 +++++++++------------ crates/iddqd/tests/soteria/tri_hash_map.rs | 29 +++++++------------- 5 files changed, 39 insertions(+), 55 deletions(-) diff --git a/crates/iddqd-soteria-runner/tests/runner.rs b/crates/iddqd-soteria-runner/tests/runner.rs index a0fe4cf5..96a47cc5 100644 --- a/crates/iddqd-soteria-runner/tests/runner.rs +++ b/crates/iddqd-soteria-runner/tests/runner.rs @@ -74,7 +74,7 @@ lib_proof!(item_set_remove_then_insert_reuses_freed_slot); test_module!(id_hash_map { lawful_roundtrip, lawless_operation_sequence, - overwrite_fail_fast_is_sound, + lawless_overwrite_is_sound, }); test_module!(id_ord_map { @@ -86,11 +86,11 @@ test_module!(id_ord_map { test_module!(bi_hash_map { lawful_roundtrip, lawless_operation_sequence, - overwrite_fail_fast_is_sound, + lawless_overwrite_is_sound, }); test_module!(tri_hash_map { lawful_roundtrip, lawless_operation_sequence, - overwrite_fail_fast_is_sound, + lawless_overwrite_is_sound, }); diff --git a/crates/iddqd/src/id_ord_map/imp.rs b/crates/iddqd/src/id_ord_map/imp.rs index 27b44164..6fd02cb5 100644 --- a/crates/iddqd/src/id_ord_map/imp.rs +++ b/crates/iddqd/src/id_ord_map/imp.rs @@ -112,7 +112,7 @@ impl IdOrdMap { /// Creates a new `IdOrdMap` with the given capacity. /// - /// The capacity will be used to initialize the underlying hash table. + /// The capacity will be used to initialize the underlying item set. /// /// # Examples /// @@ -760,8 +760,8 @@ impl IdOrdMap { // In the vacant case, the Entry lookup has already established that the // key is unique. Calling `vacant.insert_entry` would route back through // `insert_unique_impl` and check for duplicates again, while - // `vacant.insert` would also create a `RefMut` and re-hash the key. We - // use `insert_known_unique_impl` instead, which avoids both. + // `vacant.insert` would also create a `RefMut` and hash the key. We use + // `insert_known_unique_impl` instead, which avoids both. match self.entry(value.key()) { Entry::Occupied(mut occupied) => Some(occupied.insert(value)), Entry::Vacant(_) => { @@ -1503,10 +1503,11 @@ impl IdOrdMap { /// existing item. Callers that haven't determined uniqueness should use /// `insert_unique_impl` instead. fn insert_known_unique_impl(&mut self, value: T) -> ItemIndex { - // Take the `GrowHandle` after the read-only duplicate check but before - // the B-tree mutation. With this approach, a panic from - // `assert_can_grow` (which means that the map is full) cannot leave the - // B-tree referencing an index that was never assigned to an item. + // Take the `GrowHandle` now, after the caller has checked that `value` + // does not conflict with any existing item, but before the B-tree + // mutation. With this approach, a panic from `assert_can_grow` (which + // means that the map is full) cannot leave the B-tree referencing an + // index that was never assigned to an item. // // The handle holds `&mut self.items` and is consumed by // `GrowHandle::insert`, so the type system enforces that we cannot diff --git a/crates/iddqd/tests/soteria/bi_hash_map.rs b/crates/iddqd/tests/soteria/bi_hash_map.rs index 51fda995..3231c8c2 100644 --- a/crates/iddqd/tests/soteria/bi_hash_map.rs +++ b/crates/iddqd/tests/soteria/bi_hash_map.rs @@ -67,10 +67,8 @@ fn lawful_roundtrip() { /// We only exercise `remove1` -- `remove2` is symmetric, and we want to /// keep the proofs fast enough to run in CI. /// -/// We don't cover `insert_overwrite` here since that will panic under -/// adversarial input. We could catch the panic here but that slows down -/// proof execution tremendously. So instead, we have a separate proof -/// for `insert_overwrite` below. +/// We don't cover `insert_overwrite` here to avoid bloating up the runtime too +/// much. We have a separate proof for `insert_overwrite` below. /// /// We only call `validate_structural`, not full `validate`, since under /// an adversarial hash we can end up not finding items by their key. Only @@ -112,19 +110,17 @@ fn lawless_operation_sequence() { } #[test] -fn overwrite_fail_fast_is_sound() { +fn lawless_overwrite_is_sound() { let mut map: BiHashMap = BiHashMap::with_hasher(LawlessHasher); let k1 = nondet_u8_below(SEQ_KEYS); let k2 = nondet_u8_below(SEQ_KEYS); let _ = map.insert_unique(BiItem { key1: k1, key2: k2, value: 0 }); - let _ = std::panic::catch_unwind(std::panic::AssertUnwindSafe(|| { - let _ = map.insert_overwrite(BiItem { key1: k1, key2: k2, value: 1 }); - })); + let _ = map.insert_overwrite(BiItem { key1: k1, key2: k2, value: 1 }); map.validate_structural(ValidateCompact::NonCompact).expect( - "sound whether insert_overwrite completed or fail-fast panicked", + "sound whether the overwrite displaced the old item or duplicated it", ); std::mem::forget(map); } diff --git a/crates/iddqd/tests/soteria/id_hash_map.rs b/crates/iddqd/tests/soteria/id_hash_map.rs index 2edb1824..98665fa3 100644 --- a/crates/iddqd/tests/soteria/id_hash_map.rs +++ b/crates/iddqd/tests/soteria/id_hash_map.rs @@ -59,10 +59,8 @@ fn lawful_roundtrip() { /// /// # Notes /// -/// We don't cover `insert_overwrite` here since that will panic under -/// adversarial input. We could catch the panic here but that slows down -/// proof execution tremendously. So instead, we have a separate proof -/// for `insert_overwrite` below. +/// We don't cover `insert_overwrite` here to avoid bloating up the runtime too +/// much. We have a separate proof for `insert_overwrite` below. /// /// We only call `validate_structural`, not full `validate`, since under /// an adversarial hash we can end up not finding items by their key. Only @@ -100,26 +98,24 @@ fn lawless_operation_sequence() { std::mem::forget(map); } -/// `insert_overwrite` is structurally sound under a lawless hash, whether it -/// completes or trips iddqd's own `is_same_hash` fail-fast guard (which the -/// lawless hash induces by disagreeing on the recomputed key hash). +/// Prove that `insert_overwrite` is structurally sound under a lawless hash, +/// whichever arm the lawless lookup steers it into: /// -/// Note that this isn't proving panic safety in general, only that an -/// `insert_overwrite` panic leaves the map in a valid state. For panic safety, -/// see the corresponding model-based tests. +/// * If the existing item is found, an in-place replace. +/// * If the item is not found, an unchecked insert that reuses the vacant entry's +/// stored hash. +/// +/// This proof shows that in either case, the map is still structurally valid. #[test] -fn overwrite_fail_fast_is_sound() { +fn lawless_overwrite_is_sound() { let mut map: IdHashMap = IdHashMap::with_hasher(LawlessHasher); let k = nondet_u8_below(2); let _ = map.insert_unique(Item { key: k, value: 0 }); - let _ = std::panic::catch_unwind(std::panic::AssertUnwindSafe(|| { - let _ = map.insert_overwrite(Item { key: k, value: 1 }); - })); + let _ = map.insert_overwrite(Item { key: k, value: 1 }); - map.validate_structural(ValidateCompact::NonCompact).expect( - "sound whether insert_overwrite completed or fail-fast panicked", - ); + map.validate_structural(ValidateCompact::NonCompact) + .expect("sound whether the overwrite replaced or duplicated"); std::mem::forget(map); } diff --git a/crates/iddqd/tests/soteria/tri_hash_map.rs b/crates/iddqd/tests/soteria/tri_hash_map.rs index 62004c5a..32b69021 100644 --- a/crates/iddqd/tests/soteria/tri_hash_map.rs +++ b/crates/iddqd/tests/soteria/tri_hash_map.rs @@ -92,10 +92,8 @@ fn lawful_roundtrip() { /// We only exercise `remove1` -- `remove2` and `remove3` are symmetric, and we /// want to keep the proofs fast enough to run in CI. /// -/// We don't cover `insert_overwrite` here since that will panic under -/// adversarial input. We could catch the panic here but that slows down -/// proof execution tremendously. So instead, we have a separate proof -/// for `insert_overwrite` below. +/// We don't cover `insert_overwrite` here to avoid bloating up the runtime too +/// much. We have a separate proof for `insert_overwrite` below. /// /// We only call `validate_structural`, not full `validate`, since under /// an adversarial hash we can end up not finding items by their key. Only @@ -142,13 +140,8 @@ fn lawless_operation_sequence() { std::mem::forget(map); } -/// `insert_overwrite` is structurally sound under a lawless hash, whether it -/// completes (displacing up to three conflicting items) or trips iddqd's own -/// `is_same_hash` fail-fast guard. **Not** a general panic-safety claim — -/// arbitrary user-code panics mid-operation are the fault-injection -/// `proptest_panic_ops` tests' domain. #[test] -fn overwrite_fail_fast_is_sound() { +fn lawless_overwrite_is_sound() { let mut map: TriHashMap = TriHashMap::with_hasher(LawlessHasher); let k1 = nondet_u8_below(SEQ_KEYS); @@ -157,17 +150,15 @@ fn overwrite_fail_fast_is_sound() { let _ = map.insert_unique(TriItem { key1: k1, key2: k2, key3: k3, value: 0 }); - let _ = std::panic::catch_unwind(std::panic::AssertUnwindSafe(|| { - let _ = map.insert_overwrite(TriItem { - key1: k1, - key2: k2, - key3: k3, - value: 1, - }); - })); + let _ = map.insert_overwrite(TriItem { + key1: k1, + key2: k2, + key3: k3, + value: 1, + }); map.validate_structural(ValidateCompact::NonCompact).expect( - "sound whether insert_overwrite completed or fail-fast panicked", + "sound whether the overwrite displaced the old item or duplicated it", ); std::mem::forget(map); } From 2f5cb23169d9dd57c0b3eab2e11a54771c536789 Mon Sep 17 00:00:00 2001 From: Rain Date: Sun, 19 Jul 2026 15:48:20 -0700 Subject: [PATCH 09/10] update flip-key pin tests --- .../iddqd/tests/integration/pathological.rs | 78 ++++++++++--------- 1 file changed, 40 insertions(+), 38 deletions(-) diff --git a/crates/iddqd/tests/integration/pathological.rs b/crates/iddqd/tests/integration/pathological.rs index 6e57acb3..c06c1066 100644 --- a/crates/iddqd/tests/integration/pathological.rs +++ b/crates/iddqd/tests/integration/pathological.rs @@ -1015,19 +1015,6 @@ fn tri_hash_silent_tertiary_key_change_insert_overwrite() { .expect("map remains valid after silent-mutation insert_overwrite"); } -fn assert_panic_message(f: impl FnOnce(), expected: &str) { - let payload = std::panic::catch_unwind(std::panic::AssertUnwindSafe(f)) - .expect_err("the armed flip should trigger a fail-fast panic"); - let message: &str = if let Some(s) = payload.downcast_ref::<&str>() { - s - } else if let Some(s) = payload.downcast_ref::() { - s.as_str() - } else { - panic!("fail-fast panics carry a string payload"); - }; - assert_eq!(message, expected); -} - #[derive(Debug)] struct FlipItem { id: u32, @@ -1073,7 +1060,7 @@ impl IdOrdItem for FlipItem { } #[test] -fn id_hash_flip_key_insert_overwrite_panics() { +fn id_hash_flip_key_insert_overwrite_inserts_under_stale_hash() { let mut map: IdHashMap = IdHashMap::with_capacity_and_hasher( 8, foldhash::fast::FixedState::with_seed(0), @@ -1082,50 +1069,65 @@ fn id_hash_flip_key_insert_overwrite_panics() { map.insert_unique(FlipItem::plain(id)).unwrap(); } - assert_panic_message( - || { - map.insert_overwrite(FlipItem::flips_after_first_key_call(99, 42)); - }, - "key hashes do not match", - ); + let displaced = + map.insert_overwrite(FlipItem::flips_after_first_key_call(99, 42)); + assert!(displaced.is_none(), "the flipped key displaced nothing"); - assert_eq!(map.len(), 8); + assert_eq!(map.len(), 9); assert!(map.get(&99u32).is_none()); assert!(map.get(&42u32).is_none()); - map.validate(ValidateCompact::NonCompact) - .expect("map remains valid after a flip-key insert_overwrite panic"); + assert!( + map.validate(ValidateCompact::NonCompact).is_err(), + "the stale-hash item is unfindable by its current key" + ); + map.validate_structural(ValidateCompact::NonCompact).expect( + "map remains structurally sound after a flip-key insert_overwrite", + ); } #[test] -fn id_ord_flip_key_insert_overwrite_panics() { +fn id_ord_flip_key_insert_overwrite_inserts_logical_duplicate() { let mut map = IdOrdMap::::new(); for id in 0..8u32 { map.insert_unique(FlipItem::plain(id)).unwrap(); } - assert_panic_message( - || { - map.insert_overwrite(FlipItem::flips_after_first_key_call(99, 3)); - }, - "key already present in map", - ); + let displaced = + map.insert_overwrite(FlipItem::flips_after_first_key_call(99, 3)); + assert!(displaced.is_none(), "the flipped key displaced nothing"); - assert_eq!(map.len(), 8); + assert_eq!(map.len(), 9); assert!(map.get(&99u32).is_none()); - assert_eq!(map.get(&3u32).expect("original id 3 remains").id, 3); - map.validate(ValidateCompact::NonCompact, ValidateChaos::No) - .expect("map remains valid after a flip-key insert_overwrite panic"); + assert_eq!(map.get(&3u32).expect("key 3 still resolves").id, 3); + assert!( + map.validate(ValidateCompact::NonCompact, ValidateChaos::No).is_err(), + "one of the two key-3 items is unfindable" + ); + map.validate_structural(ValidateCompact::NonCompact).expect( + "map remains structurally sound after a flip-key insert_overwrite", + ); } #[test] -#[should_panic = "key already present in map"] -fn id_ord_flip_key_from_iter_unique_existing_key_panics() { - let _ = IdOrdMap::::from_iter_unique([ +fn id_ord_flip_key_from_iter_unique_inserts_logical_duplicate() { + let map = IdOrdMap::::from_iter_unique([ FlipItem::plain(0), FlipItem::plain(1), FlipItem::plain(2), FlipItem::flips_after_first_key_call(99, 1), - ]); + ]) + .expect("the flip evades the duplicate check"); + + assert_eq!(map.len(), 4); + assert!(map.get(&99u32).is_none()); + assert_eq!(map.get(&1u32).expect("key 1 still resolves").id, 1); + assert!( + map.validate(ValidateCompact::NonCompact, ValidateChaos::No).is_err(), + "one of the two key-1 items is unfindable" + ); + map.validate_structural(ValidateCompact::NonCompact).expect( + "map remains structurally sound after a flip-key from_iter_unique", + ); } #[test] From c787ba4386e143ecf42682984bcecbdbc33b0f43 Mon Sep 17 00:00:00 2001 From: Rain Date: Sun, 19 Jul 2026 16:21:06 -0700 Subject: [PATCH 10/10] update stale comments --- crates/iddqd/tests/soteria/id_ord_map.rs | 28 +++++++++++++++++------- 1 file changed, 20 insertions(+), 8 deletions(-) diff --git a/crates/iddqd/tests/soteria/id_ord_map.rs b/crates/iddqd/tests/soteria/id_ord_map.rs index f524a8fa..cd10df90 100644 --- a/crates/iddqd/tests/soteria/id_ord_map.rs +++ b/crates/iddqd/tests/soteria/id_ord_map.rs @@ -134,10 +134,12 @@ fn lawful_roundtrip() { /// /// # Notes /// -/// We don't cover `insert_overwrite` here since that will panic under -/// adversarial input. We could catch the panic here but that slows down -/// proof execution tremendously. So instead, we have a separate proof -/// for `insert_overwrite` below. +/// We don't cover `insert_overwrite` here since its occupied arm can still +/// panic under a lawless `Ord` (`replace_at_index`'s key-equality check, +/// reached because `LawlessKey`'s `Eq` delegates to the lawless `cmp`). We +/// could catch the panic here but that slows down proof execution +/// tremendously. So instead, we have a separate proof for +/// `insert_overwrite` below. /// /// We only call `validate_structural`, not full `validate`, since under /// an adversarial `Ord` we can end up not finding items by their key. Only @@ -174,12 +176,22 @@ fn lawless_operation_sequence() { std::mem::forget(map); } -/// `insert_overwrite` is structurally sound under a lawless `Ord`, whether it -/// completes or trips a fail-fast guard. +/// Prove that `insert_overwrite` is structurally sound under a lawless +/// `Ord`, whichever arm the lawless lookup steers it into: +/// +/// * If an existing item is found, an in-place replace. This arm can still +/// fail fast: `replace_at_index` re-checks key equality, and +/// `LawlessKey`'s `Eq` delegates to the lawless `cmp`. This is why this +/// proof keeps `catch_unwind` while the hash-map proofs (whose key `Eq` +/// is lawful) dropped it. +/// * If no item is found, an unchecked insert that may create a logical +/// duplicate. This arm no longer panics, but note that the B-tree +/// comparator's index tiebreaker keeps the two entries structurally distinct +/// (so structural soundness is preserved). /// /// Note that this isn't proving panic safety in general, only that an -/// `insert_overwrite` panic leaves the map in a valid state. For panic safety, -/// see the corresponding model-based tests. +/// `insert_overwrite` panic leaves the map in a valid state. For panic +/// safety, see the corresponding model-based tests. #[test] fn overwrite_fail_fast_is_sound() { let mut map: IdOrdMap = IdOrdMap::new();