Require Import UCtxtIntroGenDef.
Require Import UCtxtIntroGenSpec.
Require Import PUCtxtIntroDef.
Require Import ObjProc.

Require Import GlobalOracleProp.

Section Refinement.

  Context `{real_params: RealParams}.
  Context `{multi_oracle_prop: MultiOracleProp}.

  Section WITHMEM.

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

    Global Instance: (LoadStoreProp (hflatmem_store:= flatmem_store) (lflatmem_store:= flatmem_store)).
    Proof.
      accessor_prop_tac.
      - eapply flatmem_store_exists; eauto.
      - eapply flatmem_store_match; eauto.
    Qed.

    Lemma passthrough_correct:
      sim (crel HDATA LDATA) puctxtintro_passthrough pqthread.
    Proof.
      unfold pqthread, pqthread_fresh.
      rewrite <- right_upper_bound.
      unfold_layers.
      sim_oplus_split_straight.
      - apply fload_sim.
      - apply fstore_sim.
      - apply vmxinfo_get_sim.
      - apply palloc_sim.
      - apply setPT_sim.
      - apply ptRead_sim.
      - apply ptResv_sim.
      - apply shared_mem_status_sim.
      - apply offer_shared_mem_sim.
      - apply biglow_thread_spawn_sim.
      - apply biglow_thread_wakeup_sim.
      - apply biglow_thread_yield_sim.
      - apply biglow_thread_sleep_sim.
      - apply biglow_sched_init_sim.
      - apply ptin_sim.
      - apply ptout_sim.
      - apply container_get_nchildren_sim.
      - apply container_get_quota_sim.
      - apply container_get_usage_sim.
      - apply container_can_consume_sim.
      - apply get_CPU_ID_sim.
      - apply get_curid_sim.
      - apply acquire_lock_SC_sim.
      - apply release_lock_SC_sim.
      - apply get_sync_chan_busy_sim.
      - apply set_sync_chan_busy_sim.
      - apply ipc_send_body_sim.
      - apply ipc_receive_body_sim.
      - apply cli_sim.
      - apply sti_sim.
      - apply serial_intr_disable_sim.
      - apply serial_intr_enable_sim.
      - apply serial_putc_sim.
      - apply cons_buf_read_sim.
      - apply proc_create_postinit_sim.
      - apply trapin_sim.
      - apply trapout_sim.
      - apply hostin_sim.
      - apply hostout_sim.
      - apply trap_info_get_sim.
      - apply trap_info_ret_sim.
      - layer_sim_simpl.
        + eapply load_correct2.
        + eapply store_correct2.
    Qed.

  End WITHMEM.

End Refinement.