Function lemma_frame_drop_pre_derivable Copy item path

s.inv(),

s.frames.dom().contains(fid),

segment_cover_count(s.segments, s.frames[fid].paddr) == 0,

frame::drop_pre(s.regions, s.frames[fid].paddr),

s.regions.slot_owners[frame_to_index(s.frames[fid].paddr)].inner_perms.ref_count.value()
    == 1 ==> handle_count(s.frames, frame_to_index(s.frames[fid].paddr)) == 1,

Embedding-level Frame::wf(state). Derives the full frame::drop_pre residual (rc / storage / in_list / paths-empty conjuncts) plus the rc == 1 ⟹ handle_count == 1 clause from s.inv(), given only:

• fid is a registered handle,
• no SegmentEntry covers the slot (segment_cover_count == 0).

Replaces the residual drop_pre baggage on op_pre[FrameDrop] / step_frame_drop with a single tracked invariant chain. Every conjunct is recovered from a specific VmStore::inv clause:

• slots.contains_key: structural slot-perm coverage.
• raw_count == 0: structural raw_count == segment_cover_count
  • the segment_cover_count == 0 hypothesis.
• rc > 0 / rc != UNUSED / rc != UNIQUE / rc == H + P: accounting clause 4 (active head: H >= 1 since fid is registered + structural FrameId⟹Frame-usage).
• rc <= REF_COUNT_MAX: clause 4 (rc != UNIQUE) + MetaSlotOwner::inv’s forbidden-range empty (MAX < rc < UNIQUE ⟹ false).
• rc == 1 ⟹ storage.is_init ∧ in_list == 0: MetaSlotOwner::inv’s SHARED branch (0 < rc <= MAX), which is the Item 1 strengthening.
• rc == 1 ⟹ paths_in_pt.is_empty(): clause 4 + H >= 1 gives 1 == H + P ⟹ P == 0 ⟹ paths.len == 0 ⟹ paths.is_empty().
• rc == 1 ⟹ handle_count == 1: clause 4 with rc == 1 gives 1 == H + P; with H >= 1 and P >= 0, H == 1 and P == 0.