PageIndexSpec

Require Import Coqlib.
Require Import Maps.
Require Import Integers.
Require Import Values.
Require Import GenSem.
Require Import Maps.
Require Import Integers.
Require Import Values.
Require Import RealParams.
Require Import GenSem.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import PrimSemantics.
Require Import CompatClightSem.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.

Require Import AbsMachine.Spec.
Require Import MemBlock.Spec.
Require Import MemBlock.Layer.
Require Import RData.
Require Import Constants.
Require Import HypsecCommLib.

Local Open Scope Z_scope.

Section PageIndexSpec.

  Definition get_s2_page_index_spec (addr: Z64) (adt: RData) : option Z64 :=
    match addr with
    | VZ64 addr =>
      rely is_addr addr;
      let start := phys_mem_start in
      let size := phys_mem_size in
      if (addr >=? start) && (addr <? start + size) then
        Some (VZ64 ((addr - start) / PAGE_SIZE))
      else
        Some (VZ64 INVALID64)
    end.

End PageIndexSpec.

Section PageIndexSpecLow.

  Context `{real_params: RealParams}.

  Notation LDATA := RData.

  Notation LDATAOps := (cdata (cdata_ops := MemBlock_ops) LDATA).

  Definition get_s2_page_index_spec0 (addr: Z64) (adt: RData) : option Z64 :=
    match addr with
    | VZ64 addr =>
      rely is_addr addr;
      when' start == get_phys_mem_start_spec adt;
      when' size == get_phys_mem_size_spec adt;
      let end' := start + size in
      if (addr >=? start) && (addr <? end') then
        Some (VZ64 ((addr - start) / PAGE_SIZE))
      else
        Some (VZ64 INVALID64)
    end.

  Inductive get_s2_page_index_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
  | get_s2_page_index_spec_low_intro s (WB: _ -> Prop) m'0 labd addr res
      (Hinv: high_level_invariant labd)
      (Hspec: get_s2_page_index_spec0 (VZ64 (Int64.unsigned addr)) labd = Some (VZ64 (Int64.unsigned res))):
      get_s2_page_index_spec_low_step s WB ((Vlong addr)::nil) (m'0, labd) (Vlong res) (m'0, labd).

  Section WITHMEM.

    Context `{Hstencil: Stencil}.
    Context `{Hmem: Mem.MemoryModelX}.
    Context `{Hmwd: UseMemWithData mem}.

    Definition get_s2_page_index_spec_low: compatsem LDATAOps :=
      csem get_s2_page_index_spec_low_step (type_of_list_type (Tint64::nil)) Tint64.

  End WITHMEM.

End PageIndexSpecLow.