Module segment 

Embedding of Segment lifecycle operations: contiguous-range allocate (segment_from_unused_embedded) and drop (segment_drop_embedded).

A segment “handle” in the embedding is a range-bearing super::SegmentEntry in super::VmStore::segments. Each SegmentEntry represents one outstanding Segment<M> covering its physical range; per-frame raw_count contributions are summed via super::segment_cover_count.

Methods modeled

• Segment::from_unused: allocate a fresh segment over a range of previously-unused slots. Each frame in the range transitions usage == Unused → Frame, rc 0 → 1, raw_count 0 → 1.
• Segment drop: release the segment’s forgotten reference at each frame in the range. Each frame’s rc decrements; if the rc reaches the UNUSED sentinel (no other references), the slot transitions to UNUSED.

Model gaps

• Generic M: AnyFrameMeta + the metadata_fn closure: the embedding doesn’t carry the per-frame metadata. The axioms commit only to usage == PageUsage::Frame (matching the exec Segment::from_unused contract).
• Split / slice / next / clone / into_raw / from_raw: deferred to follow-up; the base from_unused + drop pair is enough to exercise the Shape-B raw_count == segment_cover_count invariant.

Functions

segment_drop_embedded

segment_from_unused_embedded

segment_next_embedded