Module SCSemLemmas

From mathcomp.ssreflect Require Import fintype ssrnat.
Require Import Coqlib Maps Axioms.
Require Import AST Integers Floats Values Events Globalenvs Smallstep.
Require Import Locations Stacklayout Conventions.

Require Import CUAST.

Require Import Footprint GMemory FMemory.
Require Import GAST GlobDefs ETrace Blockset DRF.

Require Import Languages.
Require Import GlobSemantics RGRels ClientSim ObjectSim.

Require Import ASM_local.
Require Import AsmLang.
Require Import InteractionSemantics.

Lemma taustar_etrace_star:
  forall State step (s s': State) fp,
    tau_star step s fp s' ->
    exists ls, ETrace.star step s ls fp s'.
Proof.

Lemma etrace_star_star:
  forall State step (s1 s2: State) ls1 fp1,
    ETrace.star step s1 ls1 fp1 s2 ->
    forall ls2 fp2 s3,
      ETrace.star step s2 ls2 fp2 s3 ->
      ETrace.star step s1 (ls1 ++ ls2) (FP.union fp1 fp2) s3.
Proof.

Lemma thdp_inv_upd:
  forall ge (tp : @ThreadPool.t ge) i
    (c' : Core.t) (tp' : ThreadPool.t),
    ThreadPool.inv tp ->
    ThreadPool.update tp i c' tp' ->
    ThreadPool.inv tp'.
Proof.

Lemma thdp_upd_next_tid:
  forall GE (tp: @ThreadPool.t GE) t c tp',
    ThreadPool.update tp t c tp' ->
    ThreadPool.next_tid tp' = ThreadPool.next_tid tp.
Proof.

Lemma thdp_upd_next_fmap:
  forall GE (tp: @ThreadPool.t GE) t c tp',
    ThreadPool.update tp t c tp' ->
    forall t0, ThreadPool.next_fmap tp' t0 = ThreadPool.next_fmap tp t0.
Proof.

Require GDefLemmas.

Lemma core_step_globstep:
  forall GE i_x F c m fp c' m',
    let: Mod := GlobEnv.modules GE i_x in
    let: lang := ModSem.lang Mod in
    let: Ge := ModSem.Ge Mod in
    let: fl := FLists.get_fl (GlobEnv.freelists GE) F in
    step lang Ge fl c m fp c' m' ->
    forall (tp: @ThreadPool.t GE) i sg b cs,
      ThreadPool.get_cs tp i = Some ((Core.Build_t i_x c sg F)::cs) ->
      exists tp',
        glob_step (Build_ProgConfig GE tp i m b) ETrace.tau fp
                  (Build_ProgConfig GE tp' i m' b) /\
        ThreadPool.update tp i (Core.Build_t i_x c' sg F) tp'.
Proof.

Lemma core_plus_globstep_plus:
  forall GE i_x F c m fp c' m',
    let: Mod := GlobEnv.modules GE i_x in
    let: lang := ModSem.lang Mod in
    let: Ge := ModSem.Ge Mod in
    let: fl := FLists.get_fl (GlobEnv.freelists GE) F in
    plus (step lang Ge fl) c m fp c' m' ->
    forall (tp: @ThreadPool.t GE) i sg b cs,
      ThreadPool.get_cs tp i = Some (Core.Build_t i_x c sg F :: cs) ->
      exists tp',
        tau_plus glob_step (Build_ProgConfig GE tp i m b) fp
                 (Build_ProgConfig GE tp' i m' b) /\
        ThreadPool.update tp i {| Core.c:=c'; Core.sg:=sg; Core.F:=F |} tp'.
Proof.

Lemma tau_plus_tau_star:
  forall GE (pc: @ProgConfig GE) fp pc',
    tau_plus glob_step pc fp pc' ->
    tau_star glob_step pc fp pc'.
Proof.

Lemma core_star_globstep_star:
  forall GE i_x F c m fp c' m',
    let: Mod := GlobEnv.modules GE i_x in
    let: lang := ModSem.lang Mod in
    let: Ge := ModSem.Ge Mod in
    let: fl := FLists.get_fl (GlobEnv.freelists GE) F in
    star (step lang Ge fl) c m fp c' m' ->
    forall (tp: @ThreadPool.t GE) i sg b cs,
      ThreadPool.get_cs tp i = Some ((Core.Build_t i_x c sg F)::cs) ->
      exists tp',
        tau_star glob_step (Build_ProgConfig GE tp i m b) fp
                 (Build_ProgConfig GE tp' i m' b) /\
        (ThreadPool.update tp i (Core.Build_t i_x c' sg F) tp' \/
         m = m' /\ c = c' /\ tp = tp' /\ fp = FP.emp).
Proof.

Lemma range_perm_client_mem:
  forall m b ofs size p,
    Mem.range_perm m b ofs (ofs + size) Memperm.Cur p ->
    (forall b' ofs',
        FMemOpFP.range_locset b ofs size b' ofs' = true ->
        client_mem (strip m) b' ofs').
Proof.

Lemma valid_access_client_mem:
  forall m chunk b ofs p,
    Mem.valid_access m chunk b ofs p ->
    (forall b' ofs',
        FMemOpFP.range_locset b ofs (size_chunk chunk) b' ofs' = true ->
        client_mem (strip m) b' ofs').
Proof.
  
Lemma loadv_loadv_fp_client_fp:
  forall chunk m v v',
    Mem.loadv chunk m v = Some v' ->
    client_fp (strip m) (strip m) (FMemOpFP.loadv_fp chunk v).
Proof.

Lemma storev_storev_fp_client_fp:
  forall chunk m v v' m',
    Mem.storev chunk m v v' = Some m' ->
    client_fp (strip m) (strip m') (FMemOpFP.storev_fp chunk v).
Proof.

Lemma valid_pointer_client_mem:
  forall m b ofs,
    Mem.valid_pointer m b ofs = true ->
    client_mem (strip m) b ofs.
Proof.

Lemma valid_pointer_client_mem_range_locset:
  forall m b ofs b' ofs',
    Mem.valid_pointer m b ofs = true ->
    FMemOpFP.range_locset b ofs 1 b' ofs' = true ->
    client_mem (strip m) b' ofs'.
Proof.

Lemma weak_valid_pointer_client_mem:
  forall m b ofs b' ofs',
    Mem.weak_valid_pointer m b ofs = true ->
    FP.cmps (FMemOpFP.weak_valid_pointer_fp m b ofs) b' ofs' = true ->
    exists ofs'', client_mem (strip m) b' ofs''.
Proof.

Lemma valid_pointer_valid_pointer_fp_client_fp:
  forall m b ofs,
    Mem.valid_pointer m b ofs = true ->
    client_fp (strip m) (strip m) (FMemOpFP.valid_pointer_fp b ofs).
Proof.

Lemma weak_valid_pointer_weak_valid_pointer_fp_client_fp:
  forall m b ofs,
    Mem.weak_valid_pointer m b ofs = true ->
    client_fp (strip m) (strip m) (FMemOpFP.weak_valid_pointer_fp m b ofs).
Proof.

Lemma alloc_client_or_unused:
  forall m lo hi m' b,
    Mem.alloc m lo hi = (m', b) ->
    forall ofs, client_mem (strip m') b ofs \/ unused_mem (strip m') b ofs.
Proof.

Lemma alloc_obj_mem_unchg:
  forall m lo hi m' b,
    Mem.alloc m lo hi = (m', b) ->
    forall b' ofs', obj_mem (strip m) b' ofs' <-> obj_mem (strip m') b' ofs'.
Proof.

Lemma alloc_clt_mem_unchg:
  forall m lo hi m' b,
    Mem.alloc m lo hi = (m', b) ->
    forall b' ofs', b' <> b -> client_mem (strip m) b' ofs' <-> client_mem (strip m') b' ofs'.
Proof.

Lemma free_obj_mem_unchg:
  forall m b lo hi m',
    Mem.free m b lo hi = Some m' ->
    forall b' ofs', obj_mem (strip m) b' ofs' <-> obj_mem (strip m') b' ofs'.
Proof.

Lemma free_clt_mem':
  forall m b lo hi m',
    Mem.free m b lo hi = Some m' ->
    forall b' ofs', client_mem (strip m') b' ofs' -> client_mem (strip m) b' ofs'.
Proof.
      
Lemma exec_load_client_fp_obj_unchg:
  forall ge chunk m a rs r rs' m',
    sep_obj_client_block (strip m) ->
    exec_load ge chunk m a rs r = AsmLang.Next rs' m' ->
    client_fp (strip m) (strip m') (exec_load_fp ge chunk a rs) /\
    (forall b ofs, obj_mem (strip m) b ofs <-> obj_mem (strip m') b ofs) /\
    sep_obj_client_block (strip m').
Proof.

Lemma exec_store_client_fp_obj_unchg:
  forall ge chunk m a rs r lr rs' m',
    sep_obj_client_block (strip m) ->
    exec_store ge chunk m a rs r lr = AsmLang.Next rs' m' ->
    client_fp (strip m) (strip m') (exec_store_fp ge chunk a rs) /\
    (forall b ofs, obj_mem (strip m) b ofs <-> obj_mem (strip m') b ofs) /\
    sep_obj_client_block (strip m').
Proof.

Lemma check_true_compare_ints_client_fp:
  forall v1 v2 m,
    sep_obj_client_block (strip m) ->
    check_compare_ints v1 v2 m = true ->
    client_fp (strip m) (strip m) (compare_ints_fp v1 v2 m).
Proof.

Lemma test_compare_ints_client_fp:
  forall v1 v2 m,
    client_fp (strip m) (strip m) (compare_ints_fp (Val.and v1 v2) Vzero m).
Proof.

Lemma compare_longs_client_fp:
  forall v1 v2 m,
    client_fp (strip m) (strip m) (compare_longs_fp v1 v2 m).
Proof.

Lemma fp_locs_fp_union_locs_union_fp_locs:
  forall fp1 fp2,
    FP.locs (FP.union fp1 fp2) = Locs.union (FP.locs fp1) (FP.locs fp2).
Proof.

Lemma eval_builtin_arg_fp_client_mem:
  forall ge rs v m a b fp,
    eval_builtin_arg ge rs v m a b ->
    @MemOpFP.eval_builtin_arg_fp Asm.preg ge rs v a fp ->
    forall b' ofs', FP.locs fp b' ofs' = true -> client_mem (strip m) b' ofs'.
Proof.

Lemma extcall_arg_fp_client_mem:
  forall rs m r b fp,
    extcall_arg rs m r b ->
    extcall_arg_fp rs r fp ->
    forall b' ofs', FP.locs fp b' ofs' = true -> client_mem (strip m) b' ofs'.
Proof.

Lemma store_args_fmem_mem_validblock_eq:
  forall m stk args tys m',
    loadframe.store_args_fmem m stk args tys = Some m' ->
    Mem.validblocks m' = Mem.validblocks m.
Proof.

Lemma store_args_fmem_mem_access_eq:
  forall m stk args tys m',
    loadframe.store_args_fmem m stk args tys = Some m' ->
    Mem.mem_access m' = Mem.mem_access m.
Proof.



Lemma AsmLang_step_client_fp:
  forall Ge fl c gm fp c' gm',
    sep_obj_client_block gm ->
    step AsmLang Ge fl c gm fp c' gm' ->
    client_fp gm gm' fp /\
    (forall b ofs, obj_mem gm b ofs <-> obj_mem gm' b ofs) /\
    sep_obj_client_block gm'.
Proof.
      
  

Lemma SpecLang_step_sep:
  forall ge fl c m fp c' m',
    sep_obj_client_block m ->
    step SpecLang.speclang ge fl c m fp c' m' ->
    sep_obj_client_block m'.
Proof.

Require Import Compositionality Soundness.

Inductive abort_behav : behav -> Prop :=
| abort_imm: abort_behav Behav_abort
| abort_cons: forall v B, abort_behav B -> abort_behav (Behav_cons v B).

Lemma non_evt_star_star_step:
  forall state step (pc: state) fp pc',
    non_evt_star step pc fp pc' ->
    exists ll, ETrace.star step pc ll fp pc'.
Proof.

Lemma prog_refine_safety_preserved:
  forall NL L ps pt,
    @prog_refine NL L ps pt ->
    forall (mu : Injections.Mu) (sgm : gmem) (sge : GlobEnv.t)
      (spc : ProgConfig) (ts : tid) (tgm : gmem) (tge : GlobEnv.t)
      (tpc : ProgConfig) (tt : tid),
      InitRel mu sge tge sgm tgm ->
      init_config ps sgm sge spc ts ->
      init_config pt tgm tge tpc tt ->
      safe_state glob_step GlobSemantics.abort spc ->
      safe_state glob_step GlobSemantics.abort tpc.
Proof.
      
Lemma safety_preservation:
  forall NL L scunits tcunits e comps,
    wd_langs scunits ->
    wd_langs tcunits ->
    det_langs tcunits ->
    rc_cunits scunits ->
    cunits_transf comps scunits tcunits ->
    @seqs_correct NL L comps ->
    drf (scunits, e) ->
    safe_prog (scunits, e) ->
    forall mu sgm sge spc ts tgm tge tpc tt,
      InitRel mu sge tge sgm tgm ->
      init_config (scunits, e) sgm sge spc ts ->
      init_config (tcunits, e) tgm tge tpc tt ->
      safe_state glob_step GlobSemantics.abort tpc.
Proof.


Lemma drf_preservation:
  forall NL L scunits tcunits e comps,
    wd_langs scunits ->
    wd_langs tcunits ->
    det_langs tcunits ->
    rc_cunits scunits ->
    cunits_transf comps scunits tcunits ->
    @seqs_correct NL L comps ->
    drf (scunits, e) ->
    safe_prog (scunits, e) ->
    forall mu sgm sge spc ts tgm tge tpc tt,
      InitRel mu sge tge sgm tgm ->
      init_config (scunits, e) sgm sge spc ts ->
      init_config (tcunits, e) tgm tge tpc tt ->
      ~ star_race_config tpc.
Proof.