Segments

Definition segid_type := ident.

A segment occupies a region of memory

Record segment : Type := mkSegment
{
segid : segid_type;
segsize : ptrofs;
}.

Label to an offset in a segment

Definition seglabel: Type := segid_type * ptrofs.

Definition offset_seglabel (l:seglabel) (ofs:ptrofs) : seglabel :=
  match l with
  | (s,o) => (s, Ptrofs.add o ofs)
  end.

Lemma offset_seglabel_zero : forall l,
  offset_seglabel l Ptrofs.zero = l.

Proof.

intros l. destruct l. simpl. rewrite Ptrofs.add_zero. auto.
Qed.

Blocks in a segment

Record segblock:Type := mkSegBlock
{
  segblock_id: segid_type;
  segblock_start : ptrofs; (* The begining of the block relative to the starting point of the segment *)
  segblock_size : ptrofs;
}.

Definition segblock_to_label (sb: segblock) : seglabel :=
  (segblock_id sb, segblock_start sb).

Get the offset of a block in a section