pub struct BorrowDebt {
pub frame_index: usize,
pub raw_count_at_issue: usize,
}Expand description
A tracked obligation token issued when from_raw is called without the
bookkeeping precondition (raw_count == 1). The holder must ensure that
the resulting Frame is wrapped in ManuallyDrop::new (which increments
raw_count to 1) before the Frame could be dropped.
The token is linear: Verus requires every tracked value to be consumed, so the caller is forced to account for it.
Fields§
§frame_index: usizeIndex of the frame slot this debt applies to.
raw_count_at_issue: usizeThe raw_count that was observed when from_raw was called.
Implementations§
Source§impl BorrowDebt
impl BorrowDebt
Sourcepub proof fn discharge_bookkeeping(tracked self)
pub proof fn discharge_bookkeeping(tracked self)
self.raw_count_at_issue == 1,Discharge the debt when the bookkeeping precondition was already met
(raw_count was 1 at the time of from_raw). This is the zero-cost
path for normal from_raw callers.
Sourcepub proof fn discharge_with_manual_drop(tracked self, regions: &MetaRegionOwners)
pub proof fn discharge_with_manual_drop(tracked self, regions: &MetaRegionOwners)
regions.slot_owners.contains_key(self.frame_index),regions.slot_owners[self.frame_index].raw_count == 1,Discharge the debt after the Frame has been wrapped in
ManuallyDrop::new, which increments raw_count to 1.
This is the path used by borrow_paddr.
Sourcepub proof fn discharge_in_lemma(tracked self, regions: &MetaRegionOwners)
pub proof fn discharge_in_lemma(tracked self, regions: &MetaRegionOwners)
regions.slot_owners.contains_key(self.frame_index),regions.slot_owners[self.frame_index].raw_count == 0,Discharge the debt in the proof of
lemma_from_raw_manuallydrop_general, where the state observed is
the immediate post-from_raw state (raw_count == 0). The lemma
itself proves that the subsequent ManuallyDrop::new restores the
bookkeeping, so consuming the debt here is sound.