From compcert Require Export Clightdefs.
Require Import VST.sepcomp.semantics.

Require Import VST.veric.juicy_base.
Require Import VST.veric.juicy_mem VST.veric.juicy_mem_lemmas VST.veric.juicy_mem_ops.
Require Import VST.veric.res_predicates.
Require Import VST.veric.extend_tc.
Require Import VST.veric.Clight_seplog.
Require Import VST.veric.Clight_assert_lemmas.
Require Import VST.veric.Clight_new.
Require Import VST.sepcomp.extspec.
Require Import VST.sepcomp.step_lemmas.
Require Import VST.veric.juicy_extspec.
Require Import VST.veric.tycontext.
Require Import VST.veric.expr2.
Require Import VST.veric.semax.
Require Import VST.veric.semax_lemmas.
Require Import VST.veric.semax_conseq.
Require Import VST.veric.Clight_lemmas.
Require Import VST.veric.Clight_initial_world.
Require Import VST.veric.semax_call.
Require Import VST.veric.semax_straight.
Require Import VST.veric.semax_loop.
Require Import VST.veric.semax_switch.
Require Import VST.veric.semax_prog.
Require Import VST.veric.semax_ext.
Require Import VST.veric.SeparationLogic.
Require Import VST.veric.expr_rel.
Require Import VST.floyd.SeparationLogicFacts.
Require Import VST.floyd.SeparationLogicAsLogic.
Require Import VST.veric.SeparationLogicSoundness.
Local Open Scope logic.
Require Import VST.veric.ghost_PCM.

Module DeepEmbeddedSoundness
       (Def: CLIGHT_SEPARATION_HOARE_LOGIC_DEF)
       (MinimumLogic: MINIMUM_CLIGHT_SEPARATION_HOARE_LOGIC with Module CSHL_Def := Def)
       (Sound: SEPARATION_HOARE_LOGIC_SOUNDNESS with Module CSHL_Def := Def)
       <: SEPARATION_HOARE_LOGIC_SOUNDNESS.

Module DeepEmbedded := DeepEmbedded (Def) (MinimumLogic).

Module CSHL_Def := DeepEmbedded.DeepEmbeddedDef.

Module CSHL_Defs := DeepEmbedded.DeepEmbeddedDefs.

Arguments CSHL_Def.semax {_} {_} _ _ _ _.

Module Conseq := GenConseq (Def) (MinimumLogic).

Module ExtrFacts := GenExtrFacts (Def) (Conseq) (MinimumLogic).

Import Conseq ExtrFacts.

Module CallF: CLIGHT_SEPARATION_HOARE_LOGIC_CALL_FORWARD with Module CSHL_Def := Def.

Module CSHL_Def := Def.
  
Definition semax_call_forward := @MinimumLogic.semax_call.

End CallF.

Module CallB := CallF2B (Def) (Conseq) (MinimumLogic) (CallF).

Module SetF: CLIGHT_SEPARATION_HOARE_LOGIC_SET_FORWARD with Module CSHL_Def := Def.

Module CSHL_Def := Def.
  
Definition semax_set_forward := @MinimumLogic.semax_set_forward.

End SetF.

Module SetB := SetF2B (Def) (Conseq) (MinimumLogic) (SetF).

Module PtrCmpF: CLIGHT_SEPARATION_HOARE_LOGIC_PTR_CMP_FORWARD with Module CSHL_Def := Def.

Module CSHL_Def := Def.
  
Definition semax_ptr_compare_forward := @MinimumLogic.semax_ptr_compare.

End PtrCmpF.

Module PtrCmpB := PtrCmpF2B (Def) (Conseq) (MinimumLogic) (PtrCmpF).

Module LoadF: CLIGHT_SEPARATION_HOARE_LOGIC_LOAD_FORWARD with Module CSHL_Def := Def.

Module CSHL_Def := Def.
  
Definition semax_load_forward := @MinimumLogic.semax_load.

End LoadF.

Module LoadB := LoadF2B (Def) (Conseq) (MinimumLogic) (LoadF).

Module CastLoadF: CLIGHT_SEPARATION_HOARE_LOGIC_CAST_LOAD_FORWARD with Module CSHL_Def := Def.

Module CSHL_Def := Def.
  
Definition semax_cast_load_forward := @MinimumLogic.semax_cast_load.

End CastLoadF.

Module CastLoadB := CastLoadF2B (Def) (Conseq) (MinimumLogic) (CastLoadF).

Module StoreF: CLIGHT_SEPARATION_HOARE_LOGIC_STORE_FORWARD with Module CSHL_Def := Def.

Module CSHL_Def := Def.
  
Definition semax_store_forward := @MinimumLogic.semax_store.

End StoreF.

Module StoreB := StoreF2B (Def) (Conseq) (MinimumLogic) (StoreF).

Module Extr : CLIGHT_SEPARATION_HOARE_LOGIC_EXTRACTION with Module CSHL_Def := Def := MinimumLogic.

Module Sset := ToSset (Def) (Conseq) (Extr) (SetB) (PtrCmpB) (LoadB) (CastLoadB).

Theorem semax_sound: forall Espec CS Delta P c Q,
  @DeepEmbedded.DeepEmbeddedDef.semax Espec CS Delta P c Q ->
  @Def.semax Espec CS Delta P c Q.
Proof.
(* Goal: forall (Espec : OracleKind) (CS : compspecs) (V : varspecs) (G : funspecs) (prog : program) (m : mem) (h : nat) (_ : @DeepEmbedded.DeepEmbeddedDefs.semax_prog Espec CS prog V G) (_ : @eq (option mem) (@Genv.init_mem (Ctypes.fundef function) type (@program_of_program function prog)) (@Some mem m)), @sigT block (fun b : block => @sigT corestate (fun q : corestate => prod (prod (@eq (option block) (@Genv.find_symbol fundef type (genv_genv (globalenv prog)) (@prog_main function prog)) (@Some block b)) (forall (jm : juicy_mem) (_ : @eq mem (m_dry jm) m), @ex juicy_mem (fun jm' : juicy_mem => @semantics.initial_core corestate juicy_mem (@juicy_core_sem corestate (cl_core_sem (globalenv prog))) h jm q jm' (Vptr b Ptrofs.zero) (@nil val)))) (forall (n : nat) (z : @OK_ty Espec), @sig juicy_mem (fun jm : juicy_mem => and (@eq mem (m_dry jm) m) (and (@eq nat (@level juicy_mem juicy_mem_ageable jm) n) (and (@eq (option (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds))) (@nth_error (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (ghost_of (m_phi jm)) O) (@Some (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (@Some (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds) (@pair (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds (@ext_ghost (@OK_ty Espec) z) NoneP)))) (and (@jsafeN (@OK_ty Espec) (@OK_spec Espec) (globalenv prog) n z q jm) (and (no_locks (m_phi jm)) (and (matchfunspecs (globalenv prog) G (m_phi jm)) (@app_pred rmap ag_rmap (funassert (nofunc_tycontext V G) (empty_environ (globalenv prog))) (m_phi jm))))))))))) *)
  intros.
(* Goal: None *)
  induction H.
  + rewrite andp_assoc.
(* Goal: None *)
    apply semax_extract_prop.
(* Goal: forall (Espec : OracleKind) (CS : compspecs) (V : varspecs) (G : funspecs) (prog : program) (m : mem) (h : nat) (_ : @DeepEmbedded.DeepEmbeddedDefs.semax_prog Espec CS prog V G) (_ : @eq (option mem) (@Genv.init_mem (Ctypes.fundef function) type (@program_of_program function prog)) (@Some mem m)), @sigT block (fun b : block => @sigT corestate (fun q : corestate => prod (prod (@eq (option block) (@Genv.find_symbol fundef type (genv_genv (globalenv prog)) (@prog_main function prog)) (@Some block b)) (forall (jm : juicy_mem) (_ : @eq mem (m_dry jm) m), @ex juicy_mem (fun jm' : juicy_mem => @semantics.initial_core corestate juicy_mem (@juicy_core_sem corestate (cl_core_sem (globalenv prog))) h jm q jm' (Vptr b Ptrofs.zero) (@nil val)))) (forall (n : nat) (z : @OK_ty Espec), @sig juicy_mem (fun jm : juicy_mem => and (@eq mem (m_dry jm) m) (and (@eq nat (@level juicy_mem juicy_mem_ageable jm) n) (and (@eq (option (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds))) (@nth_error (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (ghost_of (m_phi jm)) O) (@Some (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (@Some (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds) (@pair (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds (@ext_ghost (@OK_ty Espec) z) NoneP)))) (and (@jsafeN (@OK_ty Espec) (@OK_spec Espec) (globalenv prog) n z q jm) (and (no_locks (m_phi jm)) (and (matchfunspecs (globalenv prog) G (m_phi jm)) (@app_pred rmap ag_rmap (funassert (nofunc_tycontext V G) (empty_environ (globalenv prog))) (m_phi jm))))))))))) *)
    intros.
(* Goal: None *)
    apply MinimumLogic.semax_ifthenelse; auto.
  + eapply MinimumLogic.semax_seq; eauto.
  + apply MinimumLogic.semax_break.
  + apply MinimumLogic.semax_continue.
  + eapply MinimumLogic.semax_loop; eauto.
  + apply semax_extract_prop.
(* Goal: forall (Espec : OracleKind) (CS : compspecs) (V : varspecs) (G : funspecs) (prog : program) (m : mem) (h : nat) (_ : @DeepEmbedded.DeepEmbeddedDefs.semax_prog Espec CS prog V G) (_ : @eq (option mem) (@Genv.init_mem (Ctypes.fundef function) type (@program_of_program function prog)) (@Some mem m)), @sigT block (fun b : block => @sigT corestate (fun q : corestate => prod (prod (@eq (option block) (@Genv.find_symbol fundef type (genv_genv (globalenv prog)) (@prog_main function prog)) (@Some block b)) (forall (jm : juicy_mem) (_ : @eq mem (m_dry jm) m), @ex juicy_mem (fun jm' : juicy_mem => @semantics.initial_core corestate juicy_mem (@juicy_core_sem corestate (cl_core_sem (globalenv prog))) h jm q jm' (Vptr b Ptrofs.zero) (@nil val)))) (forall (n : nat) (z : @OK_ty Espec), @sig juicy_mem (fun jm : juicy_mem => and (@eq mem (m_dry jm) m) (and (@eq nat (@level juicy_mem juicy_mem_ageable jm) n) (and (@eq (option (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds))) (@nth_error (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (ghost_of (m_phi jm)) O) (@Some (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (@Some (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds) (@pair (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds (@ext_ghost (@OK_ty Espec) z) NoneP)))) (and (@jsafeN (@OK_ty Espec) (@OK_spec Espec) (globalenv prog) n z q jm) (and (no_locks (m_phi jm)) (and (matchfunspecs (globalenv prog) G (m_phi jm)) (@app_pred rmap ag_rmap (funassert (nofunc_tycontext V G) (empty_environ (globalenv prog))) (m_phi jm))))))))))) *)
    intros.
(* Goal: None *)
    apply MinimumLogic.semax_switch; auto.
  + apply CallB.semax_call_backward.
  + apply MinimumLogic.semax_return.
  + apply Sset.semax_set_ptr_compare_load_cast_load_backward.
  + apply StoreB.semax_store_backward.
  + apply MinimumLogic.semax_skip.
  + rewrite <- (andp_dup FF).
(* Goal: None *)
    unfold FF at 1.
(* Goal: None *)
    apply semax_extract_prop.
(* Goal: None *)
    tauto.
  + apply MinimumLogic.semax_Slabel; auto.
  + rewrite <- (andp_dup FF).
(* Goal: None *)
    unfold FF at 1.
(* Goal: None *)
    apply semax_extract_prop.
(* Goal: None *)
    tauto.
  + eapply MinimumLogic.semax_conseq; eauto.
Qed.

Theorem semax_body_sound: forall Vspec Gspec CS f id,
  @DeepEmbedded.DeepEmbeddedDefs.semax_body Vspec Gspec CS f id ->
  @MinimumLogic.CSHL_Defs.semax_body Vspec Gspec CS f id.
Proof.
(* Goal: forall (Espec : OracleKind) (CS : compspecs) (V : varspecs) (G : funspecs) (prog : program) (m : mem) (h : nat) (_ : @DeepEmbedded.DeepEmbeddedDefs.semax_prog Espec CS prog V G) (_ : @eq (option mem) (@Genv.init_mem (Ctypes.fundef function) type (@program_of_program function prog)) (@Some mem m)), @sigT block (fun b : block => @sigT corestate (fun q : corestate => prod (prod (@eq (option block) (@Genv.find_symbol fundef type (genv_genv (globalenv prog)) (@prog_main function prog)) (@Some block b)) (forall (jm : juicy_mem) (_ : @eq mem (m_dry jm) m), @ex juicy_mem (fun jm' : juicy_mem => @semantics.initial_core corestate juicy_mem (@juicy_core_sem corestate (cl_core_sem (globalenv prog))) h jm q jm' (Vptr b Ptrofs.zero) (@nil val)))) (forall (n : nat) (z : @OK_ty Espec), @sig juicy_mem (fun jm : juicy_mem => and (@eq mem (m_dry jm) m) (and (@eq nat (@level juicy_mem juicy_mem_ageable jm) n) (and (@eq (option (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds))) (@nth_error (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (ghost_of (m_phi jm)) O) (@Some (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (@Some (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds) (@pair (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds (@ext_ghost (@OK_ty Espec) z) NoneP)))) (and (@jsafeN (@OK_ty Espec) (@OK_spec Espec) (globalenv prog) n z q jm) (and (no_locks (m_phi jm)) (and (matchfunspecs (globalenv prog) G (m_phi jm)) (@app_pred rmap ag_rmap (funassert (nofunc_tycontext V G) (empty_environ (globalenv prog))) (m_phi jm))))))))))) *)
  intros.
(* Goal: None *)
  unfold MinimumLogic.CSHL_Defs.semax_body, CSHL_Defs.semax_body in H |- *.
(* Goal: None *)
  destruct id.
(* Goal: None *)
  destruct f0.
(* Goal: forall (Espec : OracleKind) (CS : compspecs) (V : varspecs) (G : funspecs) (prog : program) (m : mem) (h : nat) (_ : @DeepEmbedded.DeepEmbeddedDefs.semax_prog Espec CS prog V G) (_ : @eq (option mem) (@Genv.init_mem (Ctypes.fundef function) type (@program_of_program function prog)) (@Some mem m)), @sigT block (fun b : block => @sigT corestate (fun q : corestate => prod (prod (@eq (option block) (@Genv.find_symbol fundef type (genv_genv (globalenv prog)) (@prog_main function prog)) (@Some block b)) (forall (jm : juicy_mem) (_ : @eq mem (m_dry jm) m), @ex juicy_mem (fun jm' : juicy_mem => @semantics.initial_core corestate juicy_mem (@juicy_core_sem corestate (cl_core_sem (globalenv prog))) h jm q jm' (Vptr b Ptrofs.zero) (@nil val)))) (forall (n : nat) (z : @OK_ty Espec), @sig juicy_mem (fun jm : juicy_mem => and (@eq mem (m_dry jm) m) (and (@eq nat (@level juicy_mem juicy_mem_ageable jm) n) (and (@eq (option (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds))) (@nth_error (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (ghost_of (m_phi jm)) O) (@Some (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (@Some (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds) (@pair (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds (@ext_ghost (@OK_ty Espec) z) NoneP)))) (and (@jsafeN (@OK_ty Espec) (@OK_spec Espec) (globalenv prog) n z q jm) (and (no_locks (m_phi jm)) (and (matchfunspecs (globalenv prog) G (m_phi jm)) (@app_pred rmap ag_rmap (funassert (nofunc_tycontext V G) (empty_environ (globalenv prog))) (m_phi jm))))))))))) *)
  intros.
(* Goal: None *)
  apply semax_sound.
(* Goal: @DeepEmbedded.DeepEmbeddedDef.semax CS Espec (func_tycontext f Vspec Gspec (@nil (prod ident Annotation))) (@sepcon (_functor (ffunc (fconst environ) fidentity) mpred) (@LiftNatDed' (_functor fidentity mpred) Nveric) (@LiftSepLog' (_functor fidentity mpred) Nveric Sveric) (P ts x) (@stackframe_of CS f)) (Ssequence (fn_body f) (Sreturn (@None expr))) (frame_ret_assert (function_body_ret_assert (fn_return f) (Q ts x)) (@stackframe_of CS f)) *)
  apply H.
Qed.

Theorem semax_func_sound: forall Espec Vspec Gspec CS ids fs,
  @DeepEmbedded.DeepEmbeddedDef.semax_func Espec Vspec Gspec CS ids fs ->
  @Def.semax_func Espec Vspec Gspec CS ids fs.
Proof.
(* Goal: forall (Espec : OracleKind) (CS : compspecs) (V : varspecs) (G : funspecs) (prog : program) (m : mem) (h : nat) (_ : @DeepEmbedded.DeepEmbeddedDefs.semax_prog Espec CS prog V G) (_ : @eq (option mem) (@Genv.init_mem (Ctypes.fundef function) type (@program_of_program function prog)) (@Some mem m)), @sigT block (fun b : block => @sigT corestate (fun q : corestate => prod (prod (@eq (option block) (@Genv.find_symbol fundef type (genv_genv (globalenv prog)) (@prog_main function prog)) (@Some block b)) (forall (jm : juicy_mem) (_ : @eq mem (m_dry jm) m), @ex juicy_mem (fun jm' : juicy_mem => @semantics.initial_core corestate juicy_mem (@juicy_core_sem corestate (cl_core_sem (globalenv prog))) h jm q jm' (Vptr b Ptrofs.zero) (@nil val)))) (forall (n : nat) (z : @OK_ty Espec), @sig juicy_mem (fun jm : juicy_mem => and (@eq mem (m_dry jm) m) (and (@eq nat (@level juicy_mem juicy_mem_ageable jm) n) (and (@eq (option (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds))) (@nth_error (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (ghost_of (m_phi jm)) O) (@Some (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (@Some (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds) (@pair (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds (@ext_ghost (@OK_ty Espec) z) NoneP)))) (and (@jsafeN (@OK_ty Espec) (@OK_spec Espec) (globalenv prog) n z q jm) (and (no_locks (m_phi jm)) (and (matchfunspecs (globalenv prog) G (m_phi jm)) (@app_pred rmap ag_rmap (funassert (nofunc_tycontext V G) (empty_environ (globalenv prog))) (m_phi jm))))))))))) *)
  intros.
(* Goal: None *)
  induction H.
  + apply MinimumLogic.semax_func_nil.
  + apply MinimumLogic.semax_func_cons; auto.
(* Goal: None *)
    apply semax_body_sound; auto.
  + eapply MinimumLogic.semax_func_cons_ext; eauto.
Qed.

Theorem semax_prog_sound: forall Espec prog Vspec Gspec f,
  @DeepEmbedded.DeepEmbeddedDefs.semax_prog Espec prog Vspec Gspec f ->
  @MinimumLogic.CSHL_Defs.semax_prog Espec prog Vspec Gspec f.
Proof.
(* Goal: forall (Espec : OracleKind) (CS : compspecs) (V : varspecs) (G : funspecs) (prog : program) (m : mem) (h : nat) (_ : @DeepEmbedded.DeepEmbeddedDefs.semax_prog Espec CS prog V G) (_ : @eq (option mem) (@Genv.init_mem (Ctypes.fundef function) type (@program_of_program function prog)) (@Some mem m)), @sigT block (fun b : block => @sigT corestate (fun q : corestate => prod (prod (@eq (option block) (@Genv.find_symbol fundef type (genv_genv (globalenv prog)) (@prog_main function prog)) (@Some block b)) (forall (jm : juicy_mem) (_ : @eq mem (m_dry jm) m), @ex juicy_mem (fun jm' : juicy_mem => @semantics.initial_core corestate juicy_mem (@juicy_core_sem corestate (cl_core_sem (globalenv prog))) h jm q jm' (Vptr b Ptrofs.zero) (@nil val)))) (forall (n : nat) (z : @OK_ty Espec), @sig juicy_mem (fun jm : juicy_mem => and (@eq mem (m_dry jm) m) (and (@eq nat (@level juicy_mem juicy_mem_ageable jm) n) (and (@eq (option (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds))) (@nth_error (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (ghost_of (m_phi jm)) O) (@Some (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (@Some (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds) (@pair (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds (@ext_ghost (@OK_ty Espec) z) NoneP)))) (and (@jsafeN (@OK_ty Espec) (@OK_spec Espec) (globalenv prog) n z q jm) (and (no_locks (m_phi jm)) (and (matchfunspecs (globalenv prog) G (m_phi jm)) (@app_pred rmap ag_rmap (funassert (nofunc_tycontext V G) (empty_environ (globalenv prog))) (m_phi jm))))))))))) *)
  intros.
(* Goal: None *)
  hnf in H |- *.
(* Goal: None *)
  pose proof semax_func_sound Espec Gspec f prog (prog_funct Vspec) f.
(* Goal: None *)
  tauto.
Qed.

Theorem semax_prog_rule :
  forall {Espec: OracleKind}{CS: compspecs},
  OK_ty = unit -> 
  forall V G prog m h,
     @DeepEmbedded.DeepEmbeddedDefs.semax_prog Espec CS prog V G ->
     Genv.init_mem prog = Some m ->
     { b : block & { q : corestate &
       (Genv.find_symbol (globalenv prog) (prog_main prog) = Some b) *
       (forall jm, m_dry jm = m -> exists jm', semantics.initial_core (juicy_core_sem (cl_core_sem (globalenv prog))) h
                    jm q jm' (Vptr b Ptrofs.zero) nil) *
       forall n,
         { jm |
           m_dry jm = m /\ level jm = n /\
           (forall z, jsafeN (@OK_spec Espec) (globalenv prog) n z q jm) /\
           no_locks (m_phi jm) /\
           matchfunspecs (globalenv prog) G (m_phi jm) /\
           app_pred (funassert (nofunc_tycontext V G) (empty_environ (globalenv prog))) (m_phi jm)
     } } }%type.
Proof.
(* Goal: forall (Espec : OracleKind) (CS : compspecs) (V : varspecs) (G : funspecs) (prog : program) (m : mem) (h : nat) (_ : @DeepEmbedded.DeepEmbeddedDefs.semax_prog Espec CS prog V G) (_ : @eq (option mem) (@Genv.init_mem (Ctypes.fundef function) type (@program_of_program function prog)) (@Some mem m)), @sigT block (fun b : block => @sigT corestate (fun q : corestate => prod (prod (@eq (option block) (@Genv.find_symbol fundef type (genv_genv (globalenv prog)) (@prog_main function prog)) (@Some block b)) (forall (jm : juicy_mem) (_ : @eq mem (m_dry jm) m), @ex juicy_mem (fun jm' : juicy_mem => @semantics.initial_core corestate juicy_mem (@juicy_core_sem corestate (cl_core_sem (globalenv prog))) h jm q jm' (Vptr b Ptrofs.zero) (@nil val)))) (forall (n : nat) (z : @OK_ty Espec), @sig juicy_mem (fun jm : juicy_mem => and (@eq mem (m_dry jm) m) (and (@eq nat (@level juicy_mem juicy_mem_ageable jm) n) (and (@eq (option (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds))) (@nth_error (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (ghost_of (m_phi jm)) O) (@Some (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (@Some (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds) (@pair (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds (@ext_ghost (@OK_ty Espec) z) NoneP)))) (and (@jsafeN (@OK_ty Espec) (@OK_spec Espec) (globalenv prog) n z q jm) (and (no_locks (m_phi jm)) (and (matchfunspecs (globalenv prog) G (m_phi jm)) (@app_pred rmap ag_rmap (funassert (nofunc_tycontext V G) (empty_environ (globalenv prog))) (m_phi jm))))))))))) *)
  intros.
(* Goal: @sigT block (fun b : block => @sigT corestate (fun q : corestate => prod (prod (@eq (option block) (@Genv.find_symbol fundef type (genv_genv (globalenv prog)) (@prog_main function prog)) (@Some block b)) (forall (jm : juicy_mem) (_ : @eq mem (m_dry jm) m), @ex juicy_mem (fun jm' : juicy_mem => @semantics.initial_core corestate juicy_mem (@juicy_core_sem corestate (cl_core_sem (globalenv prog))) h jm q jm' (Vptr b Ptrofs.zero) (@nil val)))) (forall n : nat, @sig juicy_mem (fun jm : juicy_mem => and (@eq mem (m_dry jm) m) (and (@eq nat (@level juicy_mem juicy_mem_ageable jm) n) (and (forall z : @OK_ty Espec, @jsafeN (@OK_ty Espec) (@OK_spec Espec) (globalenv prog) n z q jm) (and (no_locks (m_phi jm)) (and (matchfunspecs (globalenv prog) G (m_phi jm)) (@app_pred rmap ag_rmap (funassert (nofunc_tycontext V G) (empty_environ (globalenv prog))) (m_phi jm)))))))))) *)
  apply Sound.semax_prog_rule; auto.
(* Goal: None *)
  apply semax_prog_sound; auto.
Qed.

Theorem semax_prog_rule' :
  forall {Espec: OracleKind}{CS: compspecs},
  forall V G prog m h,
     @DeepEmbedded.DeepEmbeddedDefs.semax_prog Espec CS prog V G ->
     Genv.init_mem prog = Some m ->
     { b : block & { q : corestate &
       (Genv.find_symbol (globalenv prog) (prog_main prog) = Some b) *
       (forall jm, m_dry jm = m -> exists jm', semantics.initial_core (juicy_core_sem (cl_core_sem (globalenv prog))) h
                    jm q jm' (Vptr b Ptrofs.zero) nil) *
       forall n z,
         { jm |
           m_dry jm = m /\ level jm = n /\
           nth_error (ghost_of (m_phi jm)) 0 = Some (Some (ext_ghost z, NoneP)) /\
           jsafeN (@OK_spec Espec) (globalenv prog) n z q jm /\
           no_locks (m_phi jm) /\
           matchfunspecs (globalenv prog) G (m_phi jm) /\
           app_pred (funassert (nofunc_tycontext V G) (empty_environ (globalenv prog))) (m_phi jm)
     } } }%type.
Proof.
(* Goal: forall (Espec : OracleKind) (CS : compspecs) (V : varspecs) (G : funspecs) (prog : program) (m : mem) (h : nat) (_ : @DeepEmbedded.DeepEmbeddedDefs.semax_prog Espec CS prog V G) (_ : @eq (option mem) (@Genv.init_mem (Ctypes.fundef function) type (@program_of_program function prog)) (@Some mem m)), @sigT block (fun b : block => @sigT corestate (fun q : corestate => prod (prod (@eq (option block) (@Genv.find_symbol fundef type (genv_genv (globalenv prog)) (@prog_main function prog)) (@Some block b)) (forall (jm : juicy_mem) (_ : @eq mem (m_dry jm) m), @ex juicy_mem (fun jm' : juicy_mem => @semantics.initial_core corestate juicy_mem (@juicy_core_sem corestate (cl_core_sem (globalenv prog))) h jm q jm' (Vptr b Ptrofs.zero) (@nil val)))) (forall (n : nat) (z : @OK_ty Espec), @sig juicy_mem (fun jm : juicy_mem => and (@eq mem (m_dry jm) m) (and (@eq nat (@level juicy_mem juicy_mem_ageable jm) n) (and (@eq (option (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds))) (@nth_error (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (ghost_of (m_phi jm)) O) (@Some (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (@Some (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds) (@pair (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds (@ext_ghost (@OK_ty Espec) z) NoneP)))) (and (@jsafeN (@OK_ty Espec) (@OK_spec Espec) (globalenv prog) n z q jm) (and (no_locks (m_phi jm)) (and (matchfunspecs (globalenv prog) G (m_phi jm)) (@app_pred rmap ag_rmap (funassert (nofunc_tycontext V G) (empty_environ (globalenv prog))) (m_phi jm))))))))))) *)
  intros.
(* Goal: @sigT block (fun b : block => @sigT corestate (fun q : corestate => prod (prod (@eq (option block) (@Genv.find_symbol fundef type (genv_genv (globalenv prog)) (@prog_main function prog)) (@Some block b)) (forall (jm : juicy_mem) (_ : @eq mem (m_dry jm) m), @ex juicy_mem (fun jm' : juicy_mem => @semantics.initial_core corestate juicy_mem (@juicy_core_sem corestate (cl_core_sem (globalenv prog))) h jm q jm' (Vptr b Ptrofs.zero) (@nil val)))) (forall (n : nat) (z : @OK_ty Espec), @sig juicy_mem (fun jm : juicy_mem => and (@eq mem (m_dry jm) m) (and (@eq nat (@level juicy_mem juicy_mem_ageable jm) n) (and (@eq (option (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds))) (@nth_error (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (ghost_of (m_phi jm)) O) (@Some (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (@Some (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds) (@pair (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds (@ext_ghost (@OK_ty Espec) z) NoneP)))) (and (@jsafeN (@OK_ty Espec) (@OK_spec Espec) (globalenv prog) n z q jm) (and (no_locks (m_phi jm)) (and (matchfunspecs (globalenv prog) G (m_phi jm)) (@app_pred rmap ag_rmap (funassert (nofunc_tycontext V G) (empty_environ (globalenv prog))) (m_phi jm))))))))))) *)
  apply Sound.semax_prog_rule'; auto.
(* Goal: None *)
  apply semax_prog_sound; auto.
Qed.

End DeepEmbeddedSoundness.

(********************************************************)
(*                                                      *)
(*            Main Theorem of Verifiable C              *)
(*                                                      *)
(********************************************************)

Module MainTheorem: MAIN_THEOREM_STATEMENT.

Module DeepEmbedded := DeepEmbedded (VericDef) (VericMinimumSeparationLogic).

Import DeepEmbedded.

Module CSHL_Def := DeepEmbeddedDef.

Module CSHL_Defs := DeepEmbeddedDefs.

Module CSHL_MinimumLogic := DeepEmbeddedMinimumSeparationLogic.

Module CSHL_PracticalLogic := DeepEmbeddedPracticalLogic.

Module CSHL_Sound := DeepEmbeddedSoundness (VericDef) (VericMinimumSeparationLogic) (VericSound).

End MainTheorem.
