From da278826838c018753a64ce095ed66168d1603a3 Mon Sep 17 00:00:00 2001 From: Minki Cho Date: Mon, 21 Oct 2019 05:47:37 +0900 Subject: [PATCH] remove comments (#3) * Create README.md * Update SimMemInjC.v * Update README.md * Update README.md * Update README.md * delete comments * update ReadMe * update ReadMe * Update README.md --- README.md | 20 ++--- bound/LowerBound.v | 3 - bound/UpperBound_B.v | 11 --- compose/Mod.v | 1 - compose/ModSem.v | 39 +--------- compose/Sem.v | 12 --- demo/mutrec/MutrecABproof.v | 2 +- demo/mutrec/MutrecABspec.v | 1 - demo/mutrec/MutrecAproof.v | 57 +------------- demo/mutrec/MutrecAspec.v | 3 - demo/mutrec/MutrecBproof.v | 4 - demo/mutrec/MutrecBspec.v | 3 - demo/mutrec/MutrecHeader.v | 14 ---- demo/mutrec/SimMemInjInvC.v | 8 -- demo/unreadglob/SimSymbDropInv.v | 36 --------- demo/unreadglob/UnreadglobproofC.v | 4 - demo/utod/DemoSpecProof.v | 14 +--- proof/AdequacyLocal.v | 26 +------ proof/Preservation.v | 117 ----------------------------- proof/SimMem.v | 17 ----- proof/SimModSem.v | 68 +---------------- proof/SimSymb.v | 53 ------------- proof/Simulation.v | 4 +- proof/Sound.v | 55 -------------- 24 files changed, 21 insertions(+), 551 deletions(-) diff --git a/README.md b/README.md index 2fa7c6a3..9a77a867 100644 --- a/README.md +++ b/README.md @@ -21,7 +21,7 @@ New directories are roughly as follows. - compose/: interaction semantics and its properties - demo/: examples including Unreadglob, mutual-sum and utod - selfsim/: self-simulation of Clight and Assembly -- scripts/: scripts used for SLOC counting (Table 1, 2, 3) +- scripts/: scripts used for SLOC counting (_Table 1, 2, 3_) - proof/: our meta theory @@ -30,7 +30,7 @@ We list up few important definitions/proofs from the paper. **Semantics** - Interaction Semantics _(Section 5)_ : [compose/Sem.v](compose/Sem.v) - Module _(Page 18, Fig. 9)_: [compose/Mod.v](compose/Mod.v) -- Module Semantics _(Page 18, Fig. 9)_: [compose/ModSem.v](compose/ModSem.v#L140) +- Module Semantics _(Page 18, Fig. 9)_: [compose/ModSem.v](compose/ModSem.v#L138) **Verification Techniques** - RUSC Theory _(Section 2.3)_: [proof/RUSC.v](proof/RUSC.v) @@ -39,21 +39,21 @@ We list up few important definitions/proofs from the paper. - Parameter-SymbRel _(Page 20, Fig. 10)_: [proof/SimSymb.v](proof/SimSymb.v) - Parameter-MemPred _(Page 20, Fig. 10)_: [proof/Sound.v](proof/Sound.v) - Parameterized Open Simulation _(Page 21, Fig. 11)_: [proof/SimModSem.v](proof/SimModSem.v) -- Open Preservation _(Page 21, Fig. 11)_: [proof/Preservation.v](proof/Preservation.v) - [`local_preservation_standard`](proof/Preservation.v#L177) -- Adequacy of Parameterized Open Simulation _(Page 22, Theorem 6.2)_: [proof/AdequacyLocal.v](proof/AdequacyLocal.v) - [`Theorem adequacy_local`](proof/AdequacyLocal.v#729). +- Open Preservation _(Page 21, Fig. 11)_: [proof/Preservation.v](proof/Preservation.v) - [`local_preservation_standard`](proof/Preservation.v#L102) +- Adequacy of Parameterized Open Simulation _(Page 22, Theorem 6.2)_: [proof/AdequacyLocal.v](proof/AdequacyLocal.v) - [`Theorem adequacy_local`](proof/AdequacyLocal.v#L705). **Correctness Theorems** - Compiler cocrrectness theorem (main result): [driver/CompilerC.v](driver/CompilerC.v) - + Compositional Correctness I _(Page 23, Theorem 7.3)_: [`Theorem compiler_correct`](driver/CompilerC.v#L691) + + Compositional Correctness I _(Page 23, Theorem 7.3)_: [`Theorem compiler_correct`](driver/CompilerC.v#L633) + Compositional Correctness II _(Page 24, Theorem 7.5)_: [`Theorem compiler_correct_full`](driver/CompilerC.v#L712) -- Adequacy w.r.t. Assembly _(Page 24, Theorem 7.6)_: [bound/LowerBound.v](bound/LowerBound.v) - [`Theorem lower_bound_correct`](bound/LowerBound.v#L2398) -- Adequacy w.r.t. C _(Page 24, Theorem 7.7)_: [bound/UpperBound_B.v](bound/UpperBound_B.v) - [`Theorem upper_bound_b_correct`](bound/UpperBound_B.v#L1360) +- Adequacy w.r.t. Assembly _(Page 24, Theorem 7.6)_: [bound/LowerBound.v](bound/LowerBound.v) - [`Theorem lower_bound_correct`](bound/LowerBound.v#L2395) +- Adequacy w.r.t. C _(Page 24, Theorem 7.7)_: [bound/UpperBound_B.v](bound/UpperBound_B.v) - [`Theorem upper_bound_b_correct`](bound/UpperBound_B.v#L1349) **Examples** - Unreadglob example _(Section 4.1)_: [demo/unreadglob](demo/unreadglob) ([demo directory in CompCertR](https://github.com/snu-sf/CompCertR/tree/v3.5_adapt/demo) also contains actual optimization and proof files) - mutual-sum example _(Section 4.2)_: [demo/mutrec](demo/mutrec) - + a.c, b.asm (Page 16, Fig. 7): [a.c](mutrec/a.c), [b.s](mutrec/b.s) - + a.spec, b.spec (Page 16, Fig. 7): [MutrecAspec.v](MutrecAspec.v), [MutrecBspec.v](MutrecBspec.v) - + ab.spec (Page 16, Fig. 7): [MutrecABspec.v](demo/mutrec/MutrecABspec.v) + + a.c, b.asm _(Page 16, Fig. 7)_: [a.c](demo/mutrec/a.c), [b.s](demo/mutrec/b.s) + + a.spec, b.spec _(Page 16, Fig. 7)_: [MutrecAspec.v](demo/mutrec/MutrecAspec.v), [MutrecBspec.v](demo/mutrec/MutrecBspec.v) + + ab.spec _(Page 16, Fig. 7)_: [MutrecABspec.v](demo/mutrec/MutrecABspec.v) + refinement proof: [MutrecRefinement.v](demo/mutrec/MutrecRefinement.v) - [`Theorem Mutrec_correct`](demo/mutrec/MutrecRefinement.v#L144) - utod example: [demo/utod](demo/utod) diff --git a/bound/LowerBound.v b/bound/LowerBound.v index dc52e8b0..c2b44a78 100644 --- a/bound/LowerBound.v +++ b/bound/LowerBound.v @@ -140,7 +140,6 @@ Section PRESERVATION. Qed. Definition genv_le (ge_src ge_tgt: Genv.t fundef unit): Prop := - (* sub_match_genvs eq ge_src ge_tgt. *) sub_match_genvs (@def_match _ _) ge_src ge_tgt. Lemma skenv_link_public_eq id: @@ -1717,8 +1716,6 @@ Section PRESERVATION. * ii. ss. des; clarify. } Qed. - (* skenv_inject skenv_link j_callee (assign_junk_blocks m_src n) *) - (** ********************* transf initial final *********************************) Lemma transf_initial_states: diff --git a/bound/UpperBound_B.v b/bound/UpperBound_B.v index e5cb1979..571a0d6f 100644 --- a/bound/UpperBound_B.v +++ b/bound/UpperBound_B.v @@ -43,17 +43,6 @@ Definition internal_function_state (ge: genv) (s: Csem.state) : Prop := Section PRESERVATION. -(* PLAN B-0*) - -(* -B-0 -* : Physical -+ : Logical -c0 * empty ->= -c0 + empty -*) - Inductive my_eq {A: Type} (x: A): A -> Prop := | my_eq_refl: my_eq x x. diff --git a/compose/Mod.v b/compose/Mod.v index 71f71354..f4928369 100644 --- a/compose/Mod.v +++ b/compose/Mod.v @@ -25,7 +25,6 @@ Module Mod. (* 2) This definition will give an error when datatype is changed. *) Record t: Type := mk { datatype: Type; - (* skel: Skel.t; *) get_sk: datatype -> Sk.t; get_modsem: SkEnv.t -> datatype -> ModSem.t; data: datatype; diff --git a/compose/ModSem.v b/compose/ModSem.v index 85939f0d..2017a7bd 100644 --- a/compose/ModSem.v +++ b/compose/ModSem.v @@ -141,35 +141,13 @@ Module ModSem. state: Type; genvtype: Type; step (se: Senv.t) (ge: genvtype) (st0: state) (tr: trace) (st1: state): Prop; - (* TOOD: is ge needed? I follow compcert for now. *) - - (* set_mem (m0: mem) (st0: state): state; *) (* This is not used, after_external is enough *) at_external (st0: state) (args: Args.t): Prop; initial_frame (args: Args.t) (st0: state): Prop; - (* time: rs_arg >> st0 *) - final_frame (* (st_init: state) *) (st0: state) (retv: Retv.t): Prop; - (* time: st0 >> rs_arg *) + final_frame (st0: state) (retv: Retv.t): Prop; after_external (st0: state) (retv: Retv.t) (st1: state): Prop; globalenv: genvtype; - (* internals: list block; *) - (* internals: block -> Prop; *) - (* main_fptr: block; *) - (* Note: "internals" is not enough! A ModSemPair should be able to specify which SimMem it relys. *) skenv: SkEnv.t; skenv_link: SkEnv.t; - (* skenv: SkEnv.t; *) - (* ########################################## I added SkEnv.t only for defining "compat" in sim_mem. *) - (* If it is not used, remove it *) - - - (* good properties *) - (* We need to drop permission ! *) - (* initial_machine_get_mem: forall *) - (* rs_arg m_arg st0 *) - (* (INIT: initial_frame rs_arg m_arg st0) *) - (* , *) - (* <> *) - (* ; *) at_external_dtm: forall st args0 args1 (AT0: at_external st args0) @@ -180,13 +158,6 @@ Module ModSem. (FINAL0: final_frame st retv0) (FINAL1: final_frame st retv1), retv0 = retv1; - (* final_frame_dtm: forall *) - (* rs_init st rs_ret0 m_ret0 rs_ret1 m_ret1 *) - (* (FINAL0: final_frame rs_init st rs_ret0 m_ret0) *) - (* (FINAL1: final_frame rs_init st rs_ret1 m_ret1) *) - (* , *) - (* rs_ret0 = rs_ret1 /\ m_ret0 = m_ret1 *) - (* ; *) after_external_dtm: forall st_call retv st0 st1 (AFTER0: after_external st_call retv st0) (AFTER0: after_external st_call retv st1), @@ -196,19 +167,12 @@ Module ModSem. is_call (st0: state): Prop := exists args, at_external st0 args; is_step (st0: state): Prop := exists tr st1, step skenv_link globalenv st0 tr st1; is_return (st0: state): Prop := exists retv, final_frame st0 retv; - (* exists rs_init rs_ret m_ret, final_frame rs_init st0 rs_ret m_ret; *) - (* Note: "forall" or "exists" for rs_init? *) - (* "forall" -> easy for opt/hard for meta *) - (* "exists" -> hard for opt/easy for meta *) - (* I think "exists" is OK here. *) - (* We can think of something like "forall rs_init (FUTURE: st0 is future of rs_init)", but is overkill. *) call_step_disjoint: is_call /1\ is_step <1= bot1; step_return_disjoint: is_step /1\ is_return <1= bot1; call_return_disjoint: is_call /1\ is_return <1= bot1; }. - (* Note: I didn't want to define this tactic. I wanted to use eauto + Hint Resolve, but it didn't work. *) Ltac tac := try( let TAC := u; esplits; eauto in u in *; des_safe; @@ -323,4 +287,3 @@ End ModSem. Hint Unfold ModSem.is_call ModSem.is_step ModSem.is_return. Coercion ModSem.to_semantics: ModSem.t >-> semantics. -(* I want to use definitions like "Star" or "determinate_at" *) diff --git a/compose/Sem.v b/compose/Sem.v index 1e8425fa..f0e86ac0 100644 --- a/compose/Sem.v +++ b/compose/Sem.v @@ -27,7 +27,6 @@ Module Frame. Record t: Type := mk { ms: ModSem.t; - (* st_init: ms.(ModSem.state); *) st: ms.(ModSem.state); (* local state *) }. @@ -80,7 +79,6 @@ Inductive step (ge: Ge.t): state -> trace -> state -> Prop := | step_internal fr0 frs tr st0 - (* (INTERNAL: fr0.(Frame.is_internal)) *) (STEP: Step (fr0.(Frame.ms)) fr0.(Frame.st) tr st0): step ge (State (fr0 :: frs)) tr (State ((fr0.(Frame.update_st) st0) :: frs)) @@ -97,14 +95,9 @@ Inductive step (ge: Ge.t): state -> trace -> state -> Prop := Section SEMANTICS. Variable p: program. - (* Variable init_skel: Skel.t. *) - (* Hypothesis LINKED: link_list (List.map Mod.skel p) = Some init_skel. *) Definition link_sk: option Sk.t := link_list (List.map Mod.sk p). - (* Definition init_skenv: option SkEnv.t := option_map (@Genv.globalenv (fundef unit) unit) init_sk. *) - (* Definition init_skenv (init_sk: Sk.t): SkEnv.t := (@Genv.globalenv (fundef (option signature)) unit) init_sk. *) - Definition skenv_fill_internals (skenv: SkEnv.t): SkEnv.t := skenv.(Genv_map_defs) (fun _ gd => Some match gd with @@ -118,11 +111,6 @@ Section SEMANTICS. Definition load_modsems (skenv: SkEnv.t): list ModSem.t := List.map ((flip Mod.modsem) skenv) p. - (* Definition init_mem: option mem := option_join (option_map (@Genv.init_mem (fundef unit) unit) init_sk). *) - (* Definition init_mem (init_sk: Sk.t): option mem := (@Genv.init_mem (fundef (option signature)) unit) init_sk. *) - - (* Definition init_genv: option Ge.t := *) - (* option_map (fun skenv => (Ge.mk skenv (init_modsem skenv))) init_skenv. *) Definition load_genv (init_skenv: SkEnv.t): Ge.t := let (system, skenv) := load_system init_skenv in (system :: (load_modsems init_skenv), init_skenv). diff --git a/demo/mutrec/MutrecABproof.v b/demo/mutrec/MutrecABproof.v index b0883219..81c25d7f 100644 --- a/demo/mutrec/MutrecABproof.v +++ b/demo/mutrec/MutrecABproof.v @@ -836,7 +836,7 @@ Section LXSIM. econs 2; eauto; esplits. -- eapply plus_two with (t1 := []) (t2 := []); ss. ++ econs; eauto. - { (* ez - determinate_at *) + { eapply lift_determinate_at; ss; des_ifs; eauto. econs; eauto. - ii; ss. inv H; inv H0; ss. diff --git a/demo/mutrec/MutrecABspec.v b/demo/mutrec/MutrecABspec.v index 12ac923f..b4f85ef5 100644 --- a/demo/mutrec/MutrecABspec.v +++ b/demo/mutrec/MutrecABspec.v @@ -27,7 +27,6 @@ Section MODSEM. Variable skenv_link: SkEnv.t. Variable p: unit. Let skenv: SkEnv.t := skenv_link.(SkEnv.project) sk_link. - (* Let ge: genv := Build_genv (skenv.(SkEnv.revive) p) p.(prog_comp_env). *) Let ge: SkEnv.t := skenv. Inductive state: Type := diff --git a/demo/mutrec/MutrecAproof.v b/demo/mutrec/MutrecAproof.v index 4fcf2e91..d33360c5 100644 --- a/demo/mutrec/MutrecAproof.v +++ b/demo/mutrec/MutrecAproof.v @@ -10,7 +10,6 @@ Require Import MutrecHeader. Require Import MutrecA MutrecAspec. Require Import Simulation. Require Import Skeleton Mod ModSem SimMod SimModSemLift SimSymb SimMemLift AsmregsC MatchSimModSem. -(* Require SimMemInjC. *) Require SoundTop. Require SimMemInjC SimMemInjInvC. Require Import Clightdefs. @@ -111,12 +110,11 @@ Inductive match_states_internal: nat -> MutrecAspec.state -> Clight.state -> Pro | match_callstate_nonzero idx i m_src m_tgt fptr - (* targs tres cconv *) (RANGE: 0 <= i.(Int.intval) < MAX) (FINDF: Genv.find_funct (Smallstep.globalenv (modsem2 skenv_link prog)) fptr = Some (Internal func_f)) (IDX: (idx > 3)%nat) : - match_states_internal idx (Callstate i m_src) (Clight.Callstate fptr (Tfunction (* targs tres cconv) *) + match_states_internal idx (Callstate i m_src) (Clight.Callstate fptr (Tfunction (Tcons tint Tnil) tint cc_default) [Vint i] Kstop m_tgt) | match_returnstate @@ -126,40 +124,6 @@ Inductive match_states_internal: nat -> MutrecAspec.state -> Clight.state -> Pro . -(* Inductive match_states_internal: MutrecAspec.state -> Clight.state -> Prop := *) -(* | match_callstate_nonzero_memoized *) -(* i m_src m_tgt *) -(* fptr blk memov *) -(* (* targs tres cconv *) *) -(* (FINDF: Genv.find_funct (Smallstep.globalenv (modsem2 skenv_link prog)) fptr = Some (Internal func_f)) *) -(* (SYMB: Genv.find_symbol skenv_link _memoized = Some blk) *) -(* (MEMOLD: Mem.loadv *) -(* Mint64 m_tgt *) -(* (Vptr blk (Ptrofs.repr (size_chunk Mint64 * i.(Int.intval)))) = Some (Vint memov)) *) -(* (MEMOIZED: memov = sum i) *) -(* : *) -(* match_states_internal (Callstate i m_src) (Clight.Callstate fptr (Tfunction (* targs tres cconv) *) *) -(* (Tcons tint Tnil) tint cc_default) *) -(* [Vint i] Kstop m_tgt) *) -(* | match_callstate_nonzero_nonmemoized *) -(* i m_src m_tgt *) -(* fptr blk memov *) -(* (* targs tres cconv *) *) -(* (FINDF: Genv.find_funct (Smallstep.globalenv (modsem2 skenv_link prog)) fptr = Some (Internal func_f)) *) -(* (SYMB: Genv.find_symbol skenv_link _memoized = Some blk) *) -(* (MEMOLD: Mem.loadv *) -(* Mint64 m_tgt *) -(* (Vptr blk (Ptrofs.repr (size_chunk Mint64 * i.(Int.intval)))) = Some (Vint memov)) *) -(* (NONMEMOIZED: memov.(Int.intval) < 0) *) -(* : *) -(* match_states_internal (Callstate i m_src) (Clight.Callstate fptr (Tfunction (* targs tres cconv) *) *) -(* (Tcons tint Tnil) tint cc_default) *) -(* [Vint i] Kstop m_tgt) *) -(* | match_returnstate *) -(* i m_src m_tgt *) -(* : *) -(* match_states_internal (Returnstate i m_src) (Clight.Returnstate (Vint i) Kstop m_tgt) *) -(* . *) Inductive match_states (sm_init: SimMem.t) (idx: nat) (st_src0: MutrecAspec.state) (st_tgt0: Clight.state) (sm0: SimMem.t): Prop := @@ -169,7 +133,6 @@ Inductive match_states (sm_init: SimMem.t) (MCOMPATTGT: st_tgt0.(ClightC.get_mem) = sm0.(SimMem.tgt)) (MWF: SimMem.wf sm0) (MLE: SimMem.le sm_init sm0) - (* (IDX: (idx > 3)%nat) *) . Lemma g_blk_exists @@ -203,7 +166,6 @@ Proof. rename b into g_blk. eexists. splits; et. { unfold Genv.find_funct_ptr. des_ifs. } - (* exploit (@SkEnv.project_revive_precise _ _ skenv_link); eauto. *) { inv INCL. exploit (CSk.of_program_prog_defmap prog signature_of_function); et. rewrite T. intro S. @@ -272,7 +234,6 @@ Proof. { apply Ord.lift_idx_spec. instantiate (1:=2%nat). nia. } - (* left. *) eapply plus_left with (t1 := E0) (t2 := E0); ss. { econs; eauto. { eapply modsem2_determinate; eauto. } @@ -306,7 +267,6 @@ Proof. apply star_refl. * refl. - (* * refl. *) * right. eapply CIH; eauto. econs; ss; eauto. replace (Int.repr 0) with (sum Int.zero). { econs; eauto. } @@ -485,7 +445,6 @@ Proof. clarify. eexists (Args.mk _ [Vint (Int.sub i (Int.repr 1))] _). exists sm0. - (* eexists (SimMemInjInv.mk minj _ _ (SimMemInjInv.mem_inv sm_init)). *) esplits; ss; eauto. { econs; ss; eauto. instantiate (1:=Vptr g_blk Ptrofs.zero). @@ -514,11 +473,7 @@ Proof. esplits. { econs; eauto. } - { apply MLE2. (* eassumption. *) - (* etrans; eauto. refl. *) - (* eapply SimMemInjInv.unlift_spec; eauto. *) - (* econs; eauto. } *) - } + { apply MLE2. } left. pfold. econs; eauto. i; des. econs 2; eauto. { @@ -626,7 +581,7 @@ Proof. econs 2. - etrans; eauto. etrans; eauto. eapply SimMemInjInvC.unlift_spec; eauto. econs; eauto. - (* - omega. *) } + } } { hexploit VAL; eauto. i. des. clarify. @@ -819,17 +774,11 @@ Proof. * econs; eauto. { econs; eauto. omega. } { refl. } - (* { omega. } *) - (* init progress *) i. des. inv SAFESRC. inv SIMARGS; ss. - (* hexploit (SimMemInjC.skenv_inject_revive prog); et. { apply SIMSKENV. } intro SIMSKENV0; des. *) - - (* exploit make_match_genvs; eauto. { apply SIMSKENV. } intro SIMGE. *) - - (* hexploit (@fsim_external_inject_eq); try apply FINDF; eauto. clear FPTR. intro FPTR. *) esplits; eauto. econs; eauto. + instantiate (1:= func_f). diff --git a/demo/mutrec/MutrecAspec.v b/demo/mutrec/MutrecAspec.v index 3afb9871..dce562b6 100644 --- a/demo/mutrec/MutrecAspec.v +++ b/demo/mutrec/MutrecAspec.v @@ -19,7 +19,6 @@ Section MODSEM. Variable skenv_link: SkEnv.t. Variable p: unit. Let skenv: SkEnv.t := skenv_link.(SkEnv.project) prog.(CSk.of_program signature_of_function). - (* Let ge: genv := Build_genv (skenv.(SkEnv.revive) prog) prog.(prog_comp_env). *) Inductive state: Type := | Callstate @@ -47,8 +46,6 @@ Section MODSEM. (SYMB: Genv.find_symbol skenv f_id = Some blk) (FPTR: args.(Args.fptr) = Vptr blk Ptrofs.zero) (RANGE: 0 <= i.(Int.intval) < MAX) - (* (DEF: Genv.find_funct skenv args.(Args.fptr) = *) - (* Some (AST.Internal (mksignature [AST.Tint] (Some AST.Tint) cc_default))) *) (VS: args.(Args.vs) = [Vint i]) (M: args.(Args.m) = m) : diff --git a/demo/mutrec/MutrecBproof.v b/demo/mutrec/MutrecBproof.v index 5484ba7f..7f2ff348 100644 --- a/demo/mutrec/MutrecBproof.v +++ b/demo/mutrec/MutrecBproof.v @@ -8,7 +8,6 @@ Require Import MutrecHeader IntegersC. Require Import MutrecB MutrecBspec. Require Import Simulation. Require Import Skeleton Mod ModSem SimMod SimModSemLift SimSymb SimMemLift AsmregsC MatchSimModSem. -(* Require SimMemInjC. *) Require SoundTop. Require SimMemInjC SimMemInjInv SimMemInjInvC. Require Mach. @@ -119,8 +118,6 @@ Let md_src: Mod.t := (MutrecBspec.module). Let md_tgt: Mod.t := (AsmC.module prog). Hypothesis (INCL: SkEnv.includes skenv_link md_src.(Mod.sk)). Hypothesis (WF: SkEnv.wf skenv_link). -(* Let ge := (SkEnv.project skenv_link md_src.(Mod.sk)). *) -(* Let tge := (SkEnv.revive (SkEnv.project skenv_link md_tgt.(Mod.sk)). *) Let tge := (skenv_link.(SkEnv.project) prog.(Sk.of_program fn_sig)).(SkEnv.revive) prog. Definition msp: ModSemPair.t := @@ -312,7 +309,6 @@ Proof. rename b into f_blk. eexists. splits; et. { unfold Genv.find_funct_ptr. des_ifs. } - (* exploit (@SkEnv.project_revive_precise _ _ skenv_link); eauto. *) { inv INCL. exploit (Sk.of_program_prog_defmap prog fn_sig); et. rewrite DMAP. intro S. ss. diff --git a/demo/mutrec/MutrecBspec.v b/demo/mutrec/MutrecBspec.v index 1ef003e2..a8512e9c 100644 --- a/demo/mutrec/MutrecBspec.v +++ b/demo/mutrec/MutrecBspec.v @@ -18,7 +18,6 @@ Section MODSEM. Variable skenv_link: SkEnv.t. Variable p: unit. Let skenv: SkEnv.t := skenv_link.(SkEnv.project) prog.(Sk.of_program fn_sig). - (* Let ge: genv := Build_genv (skenv.(SkEnv.revive) prog) prog.(prog_comp_env). *) Inductive state: Type := | Callstate @@ -44,8 +43,6 @@ Section MODSEM. (SYMB: Genv.find_symbol skenv g_id = Some blk) (FPTR: args.(Args.fptr) = Vptr blk Ptrofs.zero) (RANGE: 0 <= i.(Int.intval) < MAX) - (* (DEF: Genv.find_funct skenv args.(Args.fptr) = *) - (* Some (AST.Internal (mksignature [AST.Tint] (Some AST.Tint) cc_default))) *) (VS: args.(Args.vs) = [Vint i]) (M: args.(Args.m) = m) : initial_frame args (Callstate i m). diff --git a/demo/mutrec/MutrecHeader.v b/demo/mutrec/MutrecHeader.v index 27b8f610..7525d1f8 100644 --- a/demo/mutrec/MutrecHeader.v +++ b/demo/mutrec/MutrecHeader.v @@ -29,7 +29,6 @@ Proof. clarify. Qed. -(* Local Transparent Int.repr. *) Lemma sum_recurse i : @@ -76,19 +75,6 @@ Proof. rewrite MOD1. lia. Qed. -(* Function elements_rec (lo hi: Z) {wf (Zwf lo) hi} : list Z := *) -(* if zlt lo hi then (hi - 1)%Z :: elements_rec lo (hi - 1) else nil. *) -(* Proof. *) -(* intros. red. omega. *) -(* apply Zwf_well_founded. *) -(* Qed. *) - -(* Function sum (i: int): int := *) -(* m *) -(* Fixpoint sum (i: int): int := *) -(* i.(intval) *) -(* . *) - Require AST. Definition fg_sig: AST.signature := (AST.mksignature [AST.Tint] (Some AST.Tint) AST.cc_default true). diff --git a/demo/mutrec/SimMemInjInvC.v b/demo/mutrec/SimMemInjInvC.v index 4ce74f0e..5b9ba855 100644 --- a/demo/mutrec/SimMemInjInvC.v +++ b/demo/mutrec/SimMemInjInvC.v @@ -41,8 +41,6 @@ Section MEMINJINV. wf := wf' P_src P_tgt; le := le'; lepriv := lepriv; - (* lift := lift'; *) - (* unlift := unlift'; *) sim_val := fun (mrel: t') => Val.inject mrel.(SimMemInj.inj); sim_val_list := fun (mrel: t') => Val.inject_list mrel.(SimMemInj.inj); }. @@ -720,12 +718,6 @@ Section SIMSYMBINV. Next Obligation. eapply sim_skenv_inj_lepriv; eauto. Qed. - (* Next Obligation. *) - (* inv SIMSKENV. inv MWF. inv WF. *) - (* destruct sm0; ss. destruct minj; ss. econs; ss; eauto. *) - (* - ss. etrans; eauto. *) - (* - ss. etrans; eauto. *) - (* Qed. *) Next Obligation. inv LE. inv SIMSKENV. econs; ss; eauto. - i. assert (Genv.find_symbol skenv_link_tgt id = Some blk). diff --git a/demo/unreadglob/SimSymbDropInv.v b/demo/unreadglob/SimSymbDropInv.v index 088fba3f..2cd210bb 100644 --- a/demo/unreadglob/SimSymbDropInv.v +++ b/demo/unreadglob/SimSymbDropInv.v @@ -31,7 +31,6 @@ Section MEMINJ. Definition SimMemInvTop: SimMem.class := SimMemInjInvC.SimMemInjInv SimMemInjInv.top_inv SimMemInjInv.top_inv. Local Existing Instance SimMemInvTop. -(* Definition t': Type := ident -> bool. *) Record t': Type := mk { dropped:> ident -> Prop; src: Sk.t; @@ -46,10 +45,6 @@ Inductive wf (ss: t'): Prop := (DROP: forall id (DROP: ss id), ss.(tgt).(prog_defmap) ! id = None) - (* (SIMSK: forall *) - (* id *) - (* , *) - (* sk_tgt.(prog_defmap) ! id = if ss id then None else sk_src.(prog_defmap) ! id) *) (CLOSED: ss <1= ss.(src).(privs)) (PUB: ss.(src).(prog_public) = ss.(tgt).(prog_public)) (MAIN: ss.(src).(prog_main) = ss.(tgt).(prog_main)) @@ -86,7 +81,6 @@ Inductive sim_skenv (sm0: SimMem.t) (ss: t') (skenv_src skenv_tgt: SkEnv.t): Pro exists blk_src, (<>) /\ (<>) - (* /\ <> <---------- This can be obtained via SIMSYMB1. *) ) (SSINV: forall id blk_src @@ -189,7 +183,6 @@ Definition sim_skenv_splittable (sm0: SimMem.t) (ss: t') (skenv_src skenv_tgt: S exists blk_src, (<>) /\ (<>) - (* /\ <> <---------- This can be obtained via SIMSYMB1. *) >>) /\ (< eq) @@ -183,7 +181,6 @@ Proof. - instantiate (1:= Nat.lt). apply lt_wf. - eapply SoundTop.sound_state_local_preservation. - (* init bsim *) - (* destruct sm_arg; ss. clarify. *) inv INITTGT. des. inv SAFESRC. destruct args_src, args_tgt; ss. inv SIMARGS; ss. clarify. assert(SIMGE: meminj_preserves_globals prog tprog (used_set tprog) ge tge (SimMemInjInv.mem_inv_src sm_arg) (SimMemInj.inj sm_arg.(SimMemInjInv.minj))). @@ -361,7 +358,6 @@ Proof. inv TRANSL0. assert(PROG0: (prog_defmap tprog) ! id = Some (Gvar gv)). { - (* TODO: make lemma!!!!!!!!!!!!!!!!!!! *) generalize (Sk.of_program_prog_defmap tprog fn_sig id). intro REL. inv REL; try congruence. rewrite PROG in *. clarify. diff --git a/demo/utod/DemoSpecProof.v b/demo/utod/DemoSpecProof.v index b66807fa..b6f260c0 100644 --- a/demo/utod/DemoSpecProof.v +++ b/demo/utod/DemoSpecProof.v @@ -80,8 +80,6 @@ Proof. des_ifs. lia. } - (* unfold Float32.of_longu. *) - (* rewrite Float32.of_long_round_odd. *) rewrite Float.of_longu_of_long_1; ss. } { rename g0 into G. @@ -95,7 +93,6 @@ Proof. rewrite two_power_pos_correct in *. assert(P0: Z.pow_pos 2 36 <= Int64.unsigned l). { etrans; eauto. unfold Val.orl in *. des_ifs. } - (* des_ifs. ss. clarify. *) rename i into rto. assert(P1: Z.pow_pos 2 36 <= (Z.abs (Int64.signed (Int64.or (Int64.shru' l Int.one) (Int64.and l Int64.one))))). @@ -141,9 +138,6 @@ Proof. etrans; cycle 1. { eapply Int64.or_le; eauto. } rewrite Int64.unsigned_repr in *; ss. - (* assert(Int64.unsigned l <= 2 * Int64.unsigned (Int64.shru' l Int.one)). *) - (* { *) - (* } *) assert(Int64.testbit l 63 = true). { rewrite Int64.sign_bit_of_unsigned. des_ifs. rewrite Int64.half_modulus_power in *. ss. rewrite two_power_pos_correct in *. lia. @@ -227,15 +221,13 @@ Proof. assert (ARGLONG: exists lng, (Args.vs args_src) = [Vlong lng]). { inv SAFESRC. inv H. rewrite VS. eauto. } - (* clear SAFESRC. *) - inv INITTGT; ss; clarify. inv TYP. ss. (* destruct args_tgt. ss. *) - (* destruct vs; clarify. destruct vs; clarify; ss. *) - inv SIMARGS; ss. clarify. inv VALS; ss. inv H0; ss. (* destruct args_src. *) + inv INITTGT; ss; clarify. inv TYP. ss. + inv SIMARGS; ss. clarify. inv VALS; ss. inv H0; ss. ss. clarify. unfold AsmC.store_arguments in *. des. dup STORE0. inv STORE0. unfold typify_list, zip in *. inv VALS. des_ifs_safe. unfold Conventions1.loc_arguments, Conventions1.size_arguments in *. ss. des_ifs. - inv H3. (* inv H0. *) + inv H3. eexists (DemoSpec.mkstate lng (SimMemInj.src sm_arg)). esplits; eauto. - refl. diff --git a/proof/AdequacyLocal.v b/proof/AdequacyLocal.v index 7bb55736..f08a9538 100644 --- a/proof/AdequacyLocal.v +++ b/proof/AdequacyLocal.v @@ -9,7 +9,7 @@ Require Import Integers. Require Import Events. Require Import Skeleton ModSem Mod Sem. -Require Import SimSymb SimMem SimMod SimModSem SimProg (* SimLoad *) SimProg. +Require Import SimSymb SimMem SimMod SimModSem SimProg SimProg. Require Import ModSemProps SemProps Ord. Require Import Sound Preservation AdequacySound. Require Import Program. @@ -26,7 +26,6 @@ Section SIMGE. Context `{SM: SimMem.class}. Context `{SU: Sound.class}. Context {SS: SimSymb.class SM}. - (* Inductive sim_gepair (sm0: SimMem.t) (ge_src ge_tgt: list ModSem.t): Prop := *) Inductive sim_ge (sm0: SimMem.t): Ge.t -> Ge.t -> Prop := | sim_ge_src_stuck ge_tgt skenv_link_src skenv_link_tgt: @@ -42,20 +41,6 @@ Section SIMGE. (SESRC: List.Forall (fun ms => ms.(ModSem.to_semantics).(symbolenv) = skenv_link_src) ge_src) (SETGT: List.Forall (fun ms => ms.(ModSem.to_semantics).(symbolenv) = skenv_link_tgt) ge_tgt): sim_ge sm0 (ge_src, skenv_link_src) (ge_tgt, skenv_link_tgt). - (* | sim_ge_intro *) - (* msps *) - (* (SIMSKENV: List.Forall (fun msp => ModSemPair.sim_skenv msp sm0) msps) *) - (* (SIMMSS: List.Forall (ModSemPair.sim) msps) *) - (* ge_src ge_tgt *) - (* skenv_link_src skenv_link_tgt *) - (* (GESRC: ge_src = System.modsem skenv_link_src :: (map (ModSemPair.src) msps)) *) - (* (GETGT: ge_tgt = System.modsem skenv_link_tgt :: (map (ModSemPair.tgt) msps)) *) - (* ss_link *) - (* (SIMSYS: SimSymb.sim_skenv sm0 ss_link skenv_link_src skenv_link_tgt) *) - (* : *) - (* sim_ge sm0 ge_src ge_tgt *) - - Lemma find_fptr_owner_fsim sm0 ge_src ge_tgt fptr_src fptr_tgt ms_src @@ -130,7 +115,6 @@ Section SIMGE. (SIMSKENV: SimSymb.sim_skenv sm_init ss_link skenv_src skenv_tgt): <>. Proof. - (* inv SIMMP. specialize (SIMMS skenv_src skenv_tgt). *) u. econs; ss; eauto; cycle 1. { rewrite ! Mod.get_modsem_skenv_link_spec. eauto. } inv SIMMP. @@ -182,8 +166,6 @@ Section SIMGE. /\ (<>)). { exploit SimSymb.system_sim_skenv; eauto. i; des. eexists (ModSemPair.mk _ _ ss_link sm_init). ss. esplits; eauto. - (* eapply SimSymb.sim_skenv_func_bisim in SIMSKENV. des. *) - (* clears sm_init; clear sm_init. *) - exploit system_local_preservation. intro SYSSU; des. econs. { ss. eauto. } { instantiate (2:= Empty_set). ii; ss. } @@ -309,7 +291,6 @@ Section ADQMATCH. Context `{SU: Sound.class}. Variable pp: ProgPair.t. - (* Hypothesis SIMPROG: ProgPair.sim pp. *) Let p_src := pp.(ProgPair.src). Let p_tgt := pp.(ProgPair.tgt). @@ -322,10 +303,6 @@ Section ADQMATCH. Let skenv_link_src := sk_link_src.(Sk.load_skenv). Let skenv_link_tgt := sk_link_tgt.(Sk.load_skenv). - (* Interpretation: the stack called top with following regset/regset/SimMem.t as arguments. *) - (* (SimMem.t is lifted. lifting/unlifting is caller's duty) *) - (* Simulation can go continuation when SimMem.t bigger than argument is given, (after unlifting it) *) - (* with after_external fed with regsets sent. *) Inductive lxsim_stack: SimMem.t -> list Frame.t -> list Frame.t -> Prop := | lxsim_stack_nil @@ -703,7 +680,6 @@ Section ADQSTEP. { unsguard SUST. des_safe. eapply sound_progress; eauto. ss. folder. des_ifs_safe. econs; eauto. } instantiate (1:= sm_after). econs; ss; cycle 3; eauto. - (* { eauto. } *) { folder. des_ifs. eapply mfuture_preserves_sim_ge; et. econs 2; et. } { etrans; eauto. } Qed. diff --git a/proof/Preservation.v b/proof/Preservation.v index f117fb76..71f80b5f 100644 --- a/proof/Preservation.v +++ b/proof/Preservation.v @@ -19,68 +19,6 @@ Set Implicit Arguments. -(* Section SOUNDMODSEM. *) - -(* Variables ms: ModSem.t. *) -(* Context {SU: Sound.class}. *) - -(* Inductive _lprsv (lprsv: mem -> Sound.t -> ms.(ModSem.state) -> Prop) *) -(* (m_init: mem) (su: Sound.t) (st0: ms.(ModSem.state)): Prop := *) -(* | lprsv_step *) -(* (SAFE: ~ ms.(ModSem.is_call) st0 /\ ~ ms.(ModSem.is_return) st0) *) -(* (STEP: forall *) -(* tr st1 *) -(* (STEP: Step ms st0 tr st1) *) -(* , *) -(* <>) *) -(* | lprsv_at_external *) -(* (* (ATEXT: forall *) *) -(* (* args *) *) -(* (* (AT: ms.(ModSem.at_external) st0 args) *) *) -(* (* , *) *) -(* (* exists su_lifted, *) *) -(* (* (<>) *) *) -(* (* /\ (<>>>)) *) *) -(* su_lifted args *) -(* (AT: ms.(ModSem.at_external) st0 args) *) -(* (LE: Sound.lift su su_lifted) *) -(* (ARGS: su_lifted.(Sound.args) args) *) -(* (K: forall *) -(* retv st1 *) -(* (RETV: su_lifted.(Sound.retv) retv) *) -(* (MLE: Sound.mle su_lifted args.(Args.m) retv.(Retv.m)) *) -(* (AFTER: ms.(ModSem.after_external) st0 retv st1) *) -(* , *) -(* <>) *) -(* | lprsv_final *) -(* retv *) -(* (FINAL: ms.(ModSem.final_frame) st0 retv) *) -(* (MLE: Sound.mle su m_init retv.(Retv.m)) *) -(* (RETV: su.(Sound.retv) retv) *) -(* . *) - -(* Definition lprsv: _ -> _ -> _ -> Prop := paco3 _lprsv bot3. *) - -(* Lemma lprsv_mon: *) -(* monotone3 _lprsv. *) -(* Proof. *) -(* ii. inv IN; eauto. *) -(* - econs 1; ii; ss; eauto. eapply LE; eauto. eapply STEP; eauto. *) -(* - econs 2; ii; ss; eauto. *) -(* (* exploit ATEXT; eauto. i; des. esplits; eauto. ii. hexpl K. *) *) -(* exploit K; eauto. *) -(* - econs 3; ii; ss; eauto. *) -(* Qed. *) - -(* End SOUNDMODSEM. *) - - Section PRSV. Context `{SU: Sound.class}. @@ -104,22 +42,16 @@ Inductive local_preservation (sound_state: Sound.t -> mem -> ms.(state) -> Prop) (CALL: forall m_arg su0 st0 args (SUST: sound_state su0 m_arg st0) (AT: ms.(ModSem.at_external) st0 args), - (* (<>) /\ *) <> /\ exists su_gr, (<>) /\ (<>) /\ - (* (<>) /\ *) - (* (<>) /\ *) (<>)>>)) *) (<>)>>)) (RET: forall m_arg su0 st0 retv (SUST: sound_state su0 m_arg st0) @@ -146,21 +78,15 @@ Inductive local_preservation_noguarantee (sound_state: Sound.t -> mem -> ms.(sta (CALL: forall m_arg su0 st0 args (SUST: sound_state su0 m_arg st0) (AT: ms.(ModSem.at_external) st0 args), - (* (<>) /\ *) exists su_gr, (<>) /\ (<>) /\ - (* (<>) /\ *) - (* (<>) /\ *) (<>)>>)) *) (<>)>>)) . @@ -168,7 +94,6 @@ Lemma local_preservation_noguarantee_weak: <>. Proof. ii. inv PR. econs; eauto. ii; ss. exploit CALL; eauto. i; des. esplits; eauto. - (* - ii. exploit RET; eauto. i; des. esplits; eauto. *) Qed. Variable get_mem: ms.(ModSem.state) -> mem. @@ -189,31 +114,23 @@ Inductive local_preservation_standard (sound_state: Sound.t -> ms.(state) -> Pro (SUST: sound_state su0 st0) (SAFE: ~ ms.(ModSem.is_call) st0 /\ ~ ms.(ModSem.is_return) st0) (STEP: Step ms st0 tr st1), - (* <> /\ <>) *) exists su1, <> /\ <> /\ <>) (CALL: forall su0 st0 args (SUST: sound_state su0 st0) (AT: ms.(ModSem.at_external) st0 args) , <> /\ - (* (exists su_lifted, <> /\ <>) /\ *) exists su_gr, (<>) /\ (<>) /\ - (* (<>) /\ *) - (* (<>) /\ *) (<> /\ - (* (<>)>>)) *) - (* (<> /\ <>)>>)) *) (<> /\ <>)>>)) (RET: forall su0 st0 retv @@ -238,9 +155,6 @@ Proof. + etrans; eauto. eapply Sound.hle_mle; eauto. + etrans; eauto. - ii. des. exploit CALL; eauto. i; des. esplits; eauto. - (* exploit Sound.get_greatest_hle; eauto. intro GRH. des. *) - (* assert(LE1: Sound.lift su_h su_gr). *) - (* { eapply Sound.greatest_adq; eauto. } *) { etrans; eauto. eapply Sound.hle_mle; eauto. } { etrans; eauto. eapply Sound.hle_lepriv; eauto. } ii. exploit K; eauto. i; des. esplits; try apply SUST; eauto; etrans; eauto. eapply Sound.hle_mle; eauto. etrans; eauto. @@ -248,8 +162,6 @@ Proof. Qed. Variable lift: Sound.t -> Sound.t -> Prop. -(* Hypothesis lift_spec: forall su0 su1 m0 m1 (MLE: Sound.mle su1 m0 m1) (LE: lift su0 su1), <>. *) -(* Hypothesis lift_lepriv: lift <2= Sound.lepriv. *) Inductive local_preservation_strong (sound_state: Sound.t -> ms.(state) -> Prop): Prop := | local_preservation_strong_intro @@ -278,18 +190,12 @@ Inductive local_preservation_strong (sound_state: Sound.t -> ms.(state) -> Prop) exists su_gr, (<>) /\ (<>) /\ - (* (<>) /\ *) - (* (<>) /\ *) (<>)>>)) *) - (* (<> /\ <>)>>)) *) (< ms.(stat (SUST: sound_state su0 st0) (SAFE: ~ ms.(ModSem.is_call) st0 /\ ~ ms.(ModSem.is_return) st0) (STEP: Step ms st0 tr st1), - (* <> /\ <>) *) exists su1, <> /\ <> /\ <>) (CALL: forall su0 st0 args (SUST: sound_state su0 st0) (AT: ms.(ModSem.at_external) st0 args), <> /\ - (* (exists su_lifted, <> /\ <>) /\ *) exists su_gr, (<>) /\ (<>) /\ - (* (<>) /\ *) - (* (<>) /\ *) (<> /\ - (* (<>)>>)) *) - (* (<> /\ <>)>>)) *) (<> /\ <>)>>)) (RET: forall su0 st0 retv @@ -389,9 +287,6 @@ Proof. eapply Sound.hle_mle; eauto. + etrans; eauto. - ii. des. exploit CALL; eauto. i; des. - (* exploit Sound.get_greatest_hle; eauto. intro GRH. des. *) - (* assert(LE1: Sound.lift su_h su_gr). *) - (* { eapply Sound.greatest_adq; eauto. } *) esplits; eauto. { etrans; eauto. eapply Sound.hle_mle; eauto. } { etrans; eauto. eapply Sound.hle_lepriv; eauto. } @@ -480,7 +375,6 @@ Inductive local_preservation_strong_horizontal_excl (sound_state: Sound.t -> ms. (SUST: sound_state su0 st0) (SAFE: ~ ms.(ModSem.is_call) st0 /\ ~ ms.(ModSem.is_return) st0) (STEP: Step ms st0 tr st1), - (* <> /\ <>) *) exists su1, <> /\ <> /\ <>) (CALL: forall su0 st0 args (SUST: sound_state su0 st0) @@ -490,20 +384,13 @@ Inductive local_preservation_strong_horizontal_excl (sound_state: Sound.t -> ms. exists su_gr, (<>) /\ (<>) /\ - (* (<>) /\ *) - (* (<>) /\ *) - (* (<>) /\ *) (<> /\ - (* (<>)>>)) *) - (* (<> /\ <>)>>)) *) (<> /\ <>)>>)) (RET: forall su0 st0 retv @@ -528,9 +415,6 @@ Proof. eapply Sound.hle_mle; eauto. + etrans; eauto. - ii. des. exploit CALL; eauto. i; des. - (* exploit Sound.get_greatest_hle; eauto. intro GRH. des. *) - (* assert(LE1: Sound.lift su_h su_gr). *) - (* { eapply Sound.greatest_adq; eauto. } *) esplits; eauto. { etrans; eauto. eapply Sound.hle_mle; eauto. } { etrans; eauto. eapply Sound.hle_lepriv; eauto. } @@ -551,7 +435,6 @@ Definition system_sound_state `{SU: Sound.class} (ms: ModSem.t): Sound.t -> mem /\ su.(Sound.skenv) m_arg ms.(ModSem.skenv) | System.Returnstate v m => exists su_ret, Sound.hle su su_ret /\ su_ret.(Sound.retv) (Retv.Cstyle v m) /\ su.(Sound.mle) m_arg m - (* su.(Sound.retv) retv /\ su.(Sound.mle) m_arg retv.(Retv.get_m) *) /\ su.(Sound.skenv) m ms.(ModSem.skenv) end. diff --git a/proof/SimMem.v b/proof/SimMem.v index 4ef9dbbd..77274b22 100644 --- a/proof/SimMem.v +++ b/proof/SimMem.v @@ -29,14 +29,10 @@ Module SimMem. wf: t -> Prop; le: t -> t -> Prop; lepriv: t -> t -> Prop; - (* Time order: unlift second arg into first arg. *) - (* TODO: reorder arg? from->to? *) le_PreOrder :> PreOrder le; pub_priv: forall sm0 sm1, le sm0 sm1 -> lepriv sm0 sm1; - (* lift_le: forall mrel, le mrel (lift mrel); *) - (* lift_spec: forall mrel0 mrel1, le (lift mrel0) mrel1 -> wf mrel0 -> le mrel0 (unlift mrel0 mrel1); *) sim_val: t -> val -> val -> Prop; sim_val_list: t -> list val -> list val -> Prop; @@ -45,14 +41,6 @@ Module SimMem. sim_val_int: forall sm0 v_src v_tgt, sim_val sm0 v_src v_tgt -> forall i, v_src = Vint i -> v_tgt = Vint i; }. - (* Lemma le_sim_val *) - (* `{SM: class} *) - (* mrel0 mrel1 *) - (* (MWF: SimMem.wf mrel0) *) - (* (MLE: le mrel0 mrel1): *) - (* sim_val mrel0 <2= sim_val mrel1. *) - (* Proof. eapply lepriv_sim_val; et. eapply pub_priv; et. Qed. *) - Lemma sim_val_list_length `{SM: class} (sm0: t) vs_src vs_tgt @@ -63,13 +51,8 @@ Module SimMem. Definition sim_block `{SM: class} (sm0: t) (blk_src blk_tgt: block): Prop := sm0.(sim_val) (Vptr blk_src Ptrofs.zero) (Vptr blk_tgt Ptrofs.zero). - (* Definition lifted `{SM: class} (sm0 sm1: t): Prop := SimMem.lift sm0 = sm1 /\ SimMem.wf sm0. *) - Definition future `{SM: class}: t -> t -> Prop := rtc (lepriv \2/ le). - (* Definition sim_regset `{SM: class} (sm0: t) (rs_src rs_tgt: regset): Prop := *) - (* forall pr, sm0.(sim_val) (rs_src pr) (rs_tgt pr) *) - (* . *) Definition sim_regset `{SM: class} (sm0: SimMem.t) (rs_src rs_tgt: Asm.regset): Prop := forall pr, sm0.(sim_val) (rs_src pr) (rs_tgt pr). diff --git a/proof/SimModSem.v b/proof/SimModSem.v index 72cf4cfc..80b4b9f3 100644 --- a/proof/SimModSem.v +++ b/proof/SimModSem.v @@ -28,12 +28,6 @@ Section SIMMODSEM. Context {SS: SimSymb.class SM}. Variable sound_states: ms_src.(state) -> Prop. - (* Record mem_compat (st_src0: ms_src.(state)) (st_tgt0: ms_tgt.(state)) (sm0: SimMem.t): Prop := { *) - (* mcompat_src: <>; *) - (* mcompat_tgt: <>; *) - (* } *) - (* . *) - Inductive fsim_step (fsim: idx -> state ms_src -> state ms_tgt -> SimMem.t -> Prop) (i0: idx) (st_src0: ms_src.(state)) (st_tgt0: ms_tgt.(state)) (sm0: SimMem.t): Prop := | fsim_step_step @@ -42,9 +36,7 @@ Section SIMMODSEM. (STEPSRC: Step ms_src st_src0 tr st_src1), exists i1 st_tgt1 sm1, (<> \/ <>) - (* /\ <> *) /\ <> -(* Note: We require le for mle_preserves_sim_ge, but we cannot require SimMem.wf, beacuse of DCEproof *) /\ <>) (RECEP: receptive_at ms_src st_src0) | fsim_step_stutter @@ -60,7 +52,6 @@ Section SIMMODSEM. (STEPTGT: Step ms_tgt st_tgt0 tr st_tgt1), exists i1 st_src1 sm1, (<> \/ <>) - (* /\ <> *) /\ <> /\ <>) | bsim_step_stutter @@ -76,61 +67,20 @@ Section SIMMODSEM. (i0: idx) (st_src0: ms_src.(state)) (st_tgt0: ms_tgt.(state)) (sm0: SimMem.t): Prop := | lxsim_step_forward (SU: forall (SU: DUMMY_PROP), - (* (INTERNALSRC: ms_src.(ModSem.is_internal) st_src0) *) - (* (INTERNALTGT: ms_tgt.(ModSem.is_internal) st_tgt0) *) - (* (SAFESRC: ms_src.(ModSem.is_step) st_src0) *) - <> - (* Note: We used coercion on determinate_at. See final_state, which is bot2. *) - (* sd_determ_at_final becomes nothing, but it is OK. *) - (* In composed semantics, when it stepped, it must not be final *)) + <>) | lxsim_step_backward (SU: forall (SU: DUMMY_PROP), - (* (INTERNALSRC: ms_src.(ModSem.is_internal) st_src0) *) - (* (INTERNALTGT: ms_tgt.(ModSem.is_internal) st_tgt0) *) (<>)>>) /\ (<>)>>)) - (* | lxsim_at_external *) - (* rs_arg_src rs_arg_tgt *) - (* (MCOMPAT: mem_compat st_src0 st_tgt0 sm0) *) - (* m_arg_src m_arg_tgt *) - (* (ATSRC: ms_src.(at_external) st_src0 rs_arg_src m_arg_src) *) - (* (ATTGT: ms_tgt.(at_external) st_tgt0 rs_arg_tgt m_arg_tgt) *) - (* (RSREL: sm0.(SimMem.sim_regset) rs_arg_src rs_arg_tgt) *) - (* (VALID: SimMem.wf sm0) *) - (* (AFTER: forall *) - (* sm1 rs_ret_src rs_ret_tgt *) - (* (MLE: SimMem.le (SimMem.lift sm0) sm1) *) - (* (VALID: SimMem.wf sm1) *) - (* (RETVREL: sm1.(SimMem.sim_regset) rs_ret_src rs_ret_tgt) *) - (* st_tgt1 *) - (* (AFTERTGT: ms_tgt.(after_external) st_tgt0 rs_arg_tgt rs_ret_tgt sm1.(SimMem.tgt) *) - (* st_tgt1) *) - (* , *) - (* exists i1 st_src1, *) - (* (<>) *) - (* /\ *) - (* (<>)) *) - | lxsim_at_external - (* (MCOMPAT: mem_compat st_src0 st_tgt0 sm0) *) (MWF: SimMem.wf sm0) - (* (CALLPROGRESS: forall *) - (* rs_arg_src m_arg_src *) - (* (ATSRC: ms_src.(at_external) st_src0 rs_arg_src m_arg_src) *) - (* , *) - (* exists rs_arg_tgt m_arg_tgt, <>) *) - (* (SAFESRC: exists rs_arg_src m_arg_src, <>) *) - (* (SAFESRC: ms_tgt.(is_call) st_tgt0) *) (SAFESRC: ms_src.(is_call) st_src0) - (* (PROGSRC: ms_src.(is_call) st_src0) *) (SU: forall (SU: DUMMY_PROP), <>) /\ - (* (<>) *) - (* /\ *) (<>) /\ (<>)>>))>>) @@ -155,23 +103,10 @@ Section SIMMODSEM. sm_ret retv_src retv_tgt (MLE: SimMem.le sm_init sm_ret) (MWF: SimMem.wf sm_ret) - (* (PROGRESS: ms_tgt.(is_return) rs_init_tgt st_tgt0) *) - (* (RETBSIM: forall *) - (* rs_ret_tgt m_ret_tgt *) - (* (FINALTGT: ms_tgt.(final_frame) rs_init_tgt st_tgt0 rs_ret_tgt m_ret_tgt) *) - (* , *) - (* exists rs_ret_src m_ret_src, *) - (* (<>) *) - (* /\ (<>)) *) (FINALSRC: ms_src.(final_frame) st_src0 retv_src) (FINALTGT: ms_tgt.(final_frame) st_tgt0 retv_tgt) (SIMRETV: SimMem.sim_retv retv_src retv_tgt sm_ret). - (* Note: Actually, final_frame can be defined as a function. *) - - (* (FINALSRC: ms_src.(final_frame) rs_init_src st_src0 rs_ret_src m_ret_src) *) - (* (FINALTGT: ms_tgt.(final_frame) rs_init_tgt st_tgt0 rs_ret_tgt m_ret_tgt) *) - Definition _lxsim (lxsim: SimMem.t -> idx -> state ms_src -> state ms_tgt -> SimMem.t -> Prop) (sm_init: SimMem.t) (i0: idx) (st_src0: ms_src.(state)) (st_tgt0: ms_tgt.(state)) (sm0: SimMem.t): Prop := @@ -231,7 +166,6 @@ Context {SM: SimMem.class} {SS: SimSymb.class SM} {SU: Sound.class}. Inductive sim (msp: t): Prop := | sim_intro - (* (SIMSKENV: sim_skenv msp msp.(sm)) *) sidx sound_states sound_state_ex (PRSV: local_preservation msp.(src) sound_state_ex) (PRSVNOGR: forall (si: sidx), local_preservation_noguarantee msp.(src) (sound_states si)) diff --git a/proof/SimSymb.v b/proof/SimSymb.v index 8378eabe..44c78de2 100644 --- a/proof/SimSymb.v +++ b/proof/SimSymb.v @@ -27,7 +27,6 @@ Module SimSymb. (FUNCSRC: skenv_src.(Genv.find_funct) fptr_src = Some def_src), exists def_tgt, <> /\ <>). - (* TODO: Try moving t into argument? sim_symb coercion gets broken and I don't know how to fix it. *) Class class (SM: SimMem.class) := { t: Type; le: t -> t -> Prop; @@ -78,56 +77,17 @@ Module SimSymb. (<>); - (* mle_preserves_sim_skenv: forall *) - (* sm0 sm1 *) - (* (MLE: SimMem.le sm0 sm1) *) - (* ss skenv_src skenv_tgt *) - (* (SIMSKENV: sim_skenv sm0 ss skenv_src skenv_tgt) *) - (* , *) - (* <> *) - (* ; *) - mlepriv_preserves_sim_skenv: forall sm0 sm1 ss skenv_src skenv_tgt (MLE: SimMem.lepriv sm0 sm1) (SIMSKENV: sim_skenv sm0 ss skenv_src skenv_tgt), <>; - (* sim_skenv_monotone_ss: forall *) - (* sm ss_link skenv_src skenv_tgt *) - (* (SIMSKENV: sim_skenv sm ss_link skenv_src skenv_tgt) *) - (* ss *) - (* (LE: linkorder ss ss_link) *) - (* , *) - (* <> *) - (* (* Note: this should be trivial. kept becomes smaller *) *) - (* ; *) - - (* (* TODO: Can we separate sim_skenv_monotone_skenv, like sim_skenv_monotone_ss? *) *) - (* sim_skenv_monotone_skenv: forall *) - (* sm ss skenv_link_src skenv_link_tgt *) - (* (SIMSKENV: sim_skenv sm ss skenv_link_src skenv_link_tgt) *) - (* (* F_src V_src F_tgt V_tgt *) *) - (* (* (flesh_src: list (ident * globdef (AST.fundef F_src) V_src)) *) *) - (* (* (flesh_tgt: list (ident * globdef (AST.fundef F_tgt) V_tgt)) *) *) - (* sk_src sk_tgt *) - (* (SIMSK: sim_sk ss sk_src sk_tgt) *) - (* skenv_src skenv_tgt *) - (* (LESRC: skenv_link_src.(SkEnv.project) sk_src.(defs) skenv_src) *) - (* (LETGT: skenv_link_tgt.(SkEnv.project) sk_tgt.(defs) skenv_tgt) *) - (* , *) - (* <> *) - (* ; *) - - (* TODO: Can we separate sim_skenv_monotone_skenv, like sim_skenv_monotone_ss? *) sim_skenv_monotone: forall sm ss_link skenv_link_src skenv_link_tgt ss skenv_src skenv_tgt (WFSRC: SkEnv.wf skenv_link_src) (WFTGT: SkEnv.wf skenv_link_tgt) (SIMSKENV: sim_skenv sm ss_link skenv_link_src skenv_link_tgt) - (* F_src V_src F_tgt V_tgt *) - (* (flesh_src: list (ident * globdef (AST.fundef F_src) V_src)) *) - (* (flesh_tgt: list (ident * globdef (AST.fundef F_tgt) V_tgt)) *) (SIMSK: wf ss) (LE: le ss ss_link) (INCLSRC: SkEnv.includes skenv_link_src ss.(src)) @@ -143,17 +103,6 @@ Module SimSymb. system_sim_skenv: forall sm ss skenv_src skenv_tgt (SIMSKENV: sim_skenv sm ss skenv_src skenv_tgt), <>; - (* system_sim_skenv_sim_ge: forall *) - (* sm ss_sys ss sk_src sk_tgt *) - (* skenv_src skenv_tgt *) - (* (LOADSRC: sk_src.(Sk.load_skenv) = skenv_src) *) - (* (LOADTGT: sk_tgt.(Sk.load_skenv) = skenv_tgt) *) - (* (SIMSK: sim_sk ss sk_src sk_tgt) *) - (* (* (LE: SimSymb.le ss_sys ss) *) *) - (* (SIMSKENV: sim_skenv sm ss_sys skenv_src.(System.skenv) skenv_tgt.(System.skenv)) *) - (* , *) - (* <> *) - (* ; *) system_axiom: forall sm0 ss_sys skenv_sys_src skenv_sys_tgt args_src args_tgt tr retv_src ef @@ -165,7 +114,6 @@ Module SimSymb. (SYSSRC: external_call ef skenv_sys_src (args_src.(Args.vs)) (args_src.(Args.m)) tr (retv_src.(Retv.v)) (retv_src.(Retv.m))), - (* exists sm_lift, SimMem.lepriv sm0 sm_lift /\ *) exists sm1 retv_tgt, (<>) /\ (<>) /\ (<>); - (* /\ exists sm_unlift, (<>) /\ (<>) *) }. Lemma mle_preserves_sim_skenv: forall diff --git a/proof/Simulation.v b/proof/Simulation.v index 339c180c..02a4af43 100644 --- a/proof/Simulation.v +++ b/proof/Simulation.v @@ -690,7 +690,6 @@ Proof. { i. eapply PROGRESS. eapply star_safe; eauto. } + econs 2; try apply BSIM; eauto. des. esplits; eauto. eapply star_trans; eauto. inv STAR0; econs; eauto. { eapply t_trans; eauto. } - (* - i. exploit PROGRESS; eauto. ii. eapply SAFESRC. eapply star_trans; eauto. *) Qed. Lemma x2b_progress: @@ -719,7 +718,7 @@ Proof. } subst. exploit REC; eauto. eapply star_safe; eauto. apply star_one; auto. i. eapply x2b_transitions_src_tau_rev; eauto. apply star_one; ss. - + des. pclearbot. clears t. clear t. inv PLUS. (* TODO: update tactic properly *) + + des. pclearbot. clears t. clear t. inv PLUS. destruct t1, t2; ss. clear_tac. eapply x2b_trans_forward_stutter; eauto. apply star_refl. econs; eauto. apply rt_refl. } @@ -734,7 +733,6 @@ Lemma xsim_simulation_not_E0: receptive_at mt L1 s1 -> (forall t s1', Step L1 s1 t s1' -> exists i', exists s2', - (* (DPlus mt L2 s2 t s2' \/ (DStar mt L2 s2 t s2')) *) (DPlus mt L2 s2 t s2' \/ (s2 = s2' /\ t = E0)) /\ match_states i' s1' s2') -> exists i', exists s2', DPlus mt L2 s2 t s2' /\ match_states i' s1' s2'. diff --git a/proof/Sound.v b/proof/Sound.v index 7aabd2d7..c7c14105 100644 --- a/proof/Sound.v +++ b/proof/Sound.v @@ -27,33 +27,15 @@ Module Sound. Class class := { t: Type; - (* wf: t -> Prop; *) mle: t -> Memory.mem -> Memory.mem -> Prop; mle_PreOrder su0 :> PreOrder (mle su0); - (* lift: t -> t -> Prop; *) - (* lift_PreOrder :> PreOrder lift; *) hle: t -> t -> Prop; hle_PreOrder :> PreOrder hle; lepriv: t -> t -> Prop; lepriv_PreOrder :> PreOrder lepriv; - (* le_val: forall *) - (* su0 su1 *) - (* (LE: le su0 su1) *) - (* , *) - (* <> *) - (* ; *) - - (* TODO: rename it into le_monotone *) wf: t -> Prop; - (* hle_le: forall *) - (* su0 su1 *) - (* (HLE: hle su0 su1) *) - (* (WF: wf su0) *) - (* , *) - (* <> *) - (* ; *) hle_lepriv: forall su0 su1 (HLE: hle su0 su1) @@ -156,43 +138,6 @@ Module Sound. i. eapply skenv_lepriv; eauto. eapply hle_lepriv; eauto. Qed. - (* Lemma hle_spec: forall *) - (* su0 su1 m0 m1 *) - (* (HLELIFT: forall su0 su1 (HLE: hle su0 su1) (WF: wf su0), <>) *) - (* (MLE: mle su1 m0 m1) *) - (* (LE: hle su0 su1) *) - (* (WF: wf su0) *) - (* , *) - (* <> *) - (* . *) - (* Proof. *) - (* i. eapply Sound.lift_spec; et. eapply HLELIFT; et. *) - (* Qed. *) - - - (* Lemma get_greatest_le *) - (* su0 su1 args0 su_gr *) - (* (GR: get_greatest su1 args0 su_gr) *) - (* (LE: le su0 su1) *) - (* : *) - (* <> *) - (* . *) - (* Proof. *) - (* exploit Sound.greatest_adq; eauto. i; des. *) - (* exploit (Sound.greatest_ex su0); eauto. *) - (* { esplits; try apply SUARGS; eauto. etrans; eauto. } *) - (* i; des. *) - (* rp; eauto. symmetry. *) - (* eapply Sound.get_greatest_irr; eauto. *) - (* Qed. *) - - (* Inductive args (su: t) (args0: Args.t): Prop := *) - (* | args_intro *) - (* (VAL: su.(val) args0.(Args.fptr)) *) - (* (VALS: su.(val_list) args0.(Args.vs)) *) - (* (MEM: su.(mem) args0.(Args.m)) *) - (* . *) - End SOUND. End Sound.