diff --git a/backend/AllocproofC.v b/backend/AllocproofC.v index 498af2a9..4ed8154b 100644 --- a/backend/AllocproofC.v +++ b/backend/AllocproofC.v @@ -79,7 +79,6 @@ Let tge := (SkEnv.revive (SkEnv.project skenv_link md_tgt.(Mod.sk)) tprog). Definition msp: ModSemPair.t := ModSemPair.mk (md_src skenv_link) (md_tgt skenv_link) (SimSymbId.mk md_src md_tgt) sm_link. Inductive match_states - (sm_init: SimMem.t) (idx: nat) (st_src0: RTL.state) (st_tgt0: LTL.state) (sm0: SimMem.t): Prop := | match_states_intro (MATCHST: Allocproof.match_states skenv_link tge st_src0 st_tgt0) diff --git a/backend/CSEproofC.v b/backend/CSEproofC.v index 2cf9040c..545a7ad3 100644 --- a/backend/CSEproofC.v +++ b/backend/CSEproofC.v @@ -32,7 +32,6 @@ Let tge := (SkEnv.revive (SkEnv.project skenv_link md_tgt.(Mod.sk)) tprog). Definition msp: ModSemPair.t := ModSemPair.mk (md_src skenv_link) (md_tgt skenv_link) (SimSymbId.mk md_src md_tgt) sm_link. Inductive match_states - (sm_init: SimMem.t) (idx: unit) (st_src0: RTL.state) (st_tgt0: RTL.state) (sm0: SimMem.t): Prop := | match_states_intro (MATCHST: CSEproof.match_states prog ge st_src0 st_tgt0) diff --git a/backend/CleanupLabelsproofC.v b/backend/CleanupLabelsproofC.v index fd290fe7..ae2b9fff 100644 --- a/backend/CleanupLabelsproofC.v +++ b/backend/CleanupLabelsproofC.v @@ -37,7 +37,6 @@ Let tge := (SkEnv.revive (SkEnv.project skenv_link md_tgt.(Mod.sk)) tprog). Definition msp: ModSemPair.t := ModSemPair.mk (md_src skenv_link) (md_tgt skenv_link) (SimSymbId.mk md_src md_tgt) sm_link. Inductive match_states - (sm_init: SimMem.t) (idx: nat) (st_src0 st_tgt0: Linear.state) (sm0: SimMem.t): Prop := | match_states_intro (MATCHST: CleanupLabelsproof.match_states st_src0 st_tgt0) @@ -142,7 +141,7 @@ Proof. * right. esplits; et. { eapply star_refl. } * instantiate (1:= SimMemId.mk _ _). econs; ss. - + Unshelve. all: ss; try (by econs). apply msp. Qed. diff --git a/backend/ConstpropproofC.v b/backend/ConstpropproofC.v index 18950a8a..6d643151 100644 --- a/backend/ConstpropproofC.v +++ b/backend/ConstpropproofC.v @@ -29,7 +29,7 @@ Let ge := (SkEnv.revive (SkEnv.project skenv_link md_src.(Mod.sk)) prog). Let tge := (SkEnv.revive (SkEnv.project skenv_link md_tgt.(Mod.sk)) tprog). Definition msp: ModSemPair.t := ModSemPair.mk (md_src skenv_link) (md_tgt skenv_link) (SimSymbId.mk md_src md_tgt) sm_link. -Inductive match_states (sm_init: SimMem.t) +Inductive match_states (idx: nat) (st_src0: RTL.state) (st_tgt0: RTL.state) (sm0: SimMem.t): Prop := | match_states_intro (MATCHST: Constpropproof.match_states prog idx st_src0 st_tgt0) diff --git a/backend/DeadcodeproofC.v b/backend/DeadcodeproofC.v index 4df4b086..45ec01b6 100644 --- a/backend/DeadcodeproofC.v +++ b/backend/DeadcodeproofC.v @@ -32,7 +32,6 @@ Let tge := (SkEnv.revive (SkEnv.project skenv_link md_tgt.(Mod.sk)) tprog). Definition msp: ModSemPair.t := ModSemPair.mk (md_src skenv_link) (md_tgt skenv_link) (SimSymbId.mk md_src md_tgt) sm_link. Inductive match_states - (sm_init: SimMem.t) (idx: unit) (st_src0: RTL.state) (st_tgt0: RTL.state) (sm0: SimMem.t): Prop := | match_states_intro (MATCHST: Deadcodeproof.match_states prog ge st_src0 st_tgt0) diff --git a/backend/DebugvarproofC.v b/backend/DebugvarproofC.v index 100139e4..c247dee7 100644 --- a/backend/DebugvarproofC.v +++ b/backend/DebugvarproofC.v @@ -33,7 +33,7 @@ Let ge := (SkEnv.revive (SkEnv.project skenv_link md_src.(Mod.sk)) prog). Let tge := (SkEnv.revive (SkEnv.project skenv_link md_tgt.(Mod.sk)) tprog). Definition msp: ModSemPair.t := ModSemPair.mk (md_src skenv_link) (md_tgt skenv_link) (SimSymbId.mk md_src md_tgt) sm_link. -Inductive match_states (sm_init: SimMem.t) +Inductive match_states (idx: nat) (st_src0: Linear.state) (st_tgt0: Linear.state) (sm0: SimMem.t): Prop := | match_states_intro (MATCHST: Debugvarproof.match_states st_src0 st_tgt0) @@ -176,4 +176,3 @@ Proof. Qed. End SIMMOD. - diff --git a/backend/InliningproofC.v b/backend/InliningproofC.v index 344495d1..ea322ee5 100644 --- a/backend/InliningproofC.v +++ b/backend/InliningproofC.v @@ -34,7 +34,6 @@ Let tge := (SkEnv.revive (SkEnv.project skenv_link md_tgt.(Mod.sk)) tprog). Definition msp: ModSemPair.t := ModSemPair.mk (md_src skenv_link) (md_tgt skenv_link) (SimSymbId.mk md_src md_tgt) sm_link. Inductive match_states - (sm_init: SimMem.t) (idx: nat) (st_src0: RTL.state) (st_tgt0: RTL.state) (sm0: SimMem.t): Prop := | match_states_intro (MATCHST: Inliningproof.match_states prog skenv_link skenv_link ge st_src0 st_tgt0 sm0) diff --git a/backend/LinearizeproofC.v b/backend/LinearizeproofC.v index d8c32047..2e12fd48 100644 --- a/backend/LinearizeproofC.v +++ b/backend/LinearizeproofC.v @@ -38,7 +38,6 @@ Let tge := (SkEnv.revive (SkEnv.project skenv_link md_tgt.(Mod.sk)) tprog). Definition msp: ModSemPair.t := ModSemPair.mk (md_src skenv_link) (md_tgt skenv_link) (SimSymbId.mk md_src md_tgt) sm_link. Inductive match_states - (sm_init: SimMem.t) (idx: nat) (st_src0: LTL.state) (st_tgt0: Linear.state) (sm0: SimMem.t): Prop := | match_states_intro (MATCHST: Linearizeproof.match_states st_src0 st_tgt0) diff --git a/backend/RTLgenproofC.v b/backend/RTLgenproofC.v index 75b3b3d4..b8d44eb7 100644 --- a/backend/RTLgenproofC.v +++ b/backend/RTLgenproofC.v @@ -31,7 +31,6 @@ Let tge := (SkEnv.revive (SkEnv.project skenv_link md_tgt.(Mod.sk)) tprog). Definition msp: ModSemPair.t := ModSemPair.mk (md_src skenv_link) (md_tgt skenv_link) (SimSymbId.mk md_src md_tgt) sm_link. Inductive match_states - (sm_init: SimMem.t) (idx: nat * nat) (st_src0: CminorSel.state) (st_tgt0: RTL.state) (sm0: SimMem.t): Prop := | match_states_intro (MATCHST: RTLgenproof.match_states st_src0 st_tgt0) diff --git a/backend/RenumberproofC.v b/backend/RenumberproofC.v index 45e8eee2..5c2104d0 100644 --- a/backend/RenumberproofC.v +++ b/backend/RenumberproofC.v @@ -27,7 +27,7 @@ Let ge := (SkEnv.revive (SkEnv.project skenv_link md_src.(Mod.sk)) prog). Let tge := (SkEnv.revive (SkEnv.project skenv_link md_tgt.(Mod.sk)) tprog). Definition msp: ModSemPair.t := ModSemPair.mk (md_src skenv_link) (md_tgt skenv_link) (SimSymbId.mk md_src md_tgt) sm_link. -Inductive match_states (sm_init: SimMem.t) +Inductive match_states (idx: nat) (st_src0: RTL.state) (st_tgt0: RTL.state) (sm0: SimMem.t): Prop := | match_states_intro (MATCHST: Renumberproof.match_states st_src0 st_tgt0) @@ -117,4 +117,3 @@ Proof. Qed. End SIMMOD. - diff --git a/backend/SelectionproofC.v b/backend/SelectionproofC.v index 8eaf3d42..4d168eb8 100644 --- a/backend/SelectionproofC.v +++ b/backend/SelectionproofC.v @@ -37,7 +37,6 @@ Let tge := (SkEnv.revive (SkEnv.project skenv_link md_tgt.(Mod.sk)) tprog). Definition msp: ModSemPair.t := ModSemPair.mk (md_src skenv_link) (md_tgt skenv_link) (SimSymbId.mk md_src md_tgt) sm_link. Inductive match_states - (sm_init: SimMem.t) (idx: nat) (st_src0: Cminor.state) (st_tgt0: CminorSel.state) (sm0: SimMem.t): Prop := | match_states_intro (MATCHST: Selectionproof.match_states prog skenv_link ge tge st_src0 st_tgt0) diff --git a/backend/StackingproofC.v b/backend/StackingproofC.v index 6448de97..230fb493 100644 --- a/backend/StackingproofC.v +++ b/backend/StackingproofC.v @@ -863,7 +863,6 @@ Qed. Local Opaque sepconj. Inductive match_states - (sm_init: SimMem.t) (idx: nat) (st_src0: Linear.state) (st_tgt0: MachC.state) (sm0: SimMem.t): Prop := | match_states_intro (MATCHST: Stackingproof.match_states skenv_link skenv_link ge tge st_src0 st_tgt0.(st) sm0) diff --git a/backend/TailcallproofC.v b/backend/TailcallproofC.v index e471e571..faca5150 100644 --- a/backend/TailcallproofC.v +++ b/backend/TailcallproofC.v @@ -29,7 +29,6 @@ Let tge := (SkEnv.revive (SkEnv.project skenv_link md_tgt.(Mod.sk)) tprog). Definition msp: ModSemPair.t := ModSemPair.mk (md_src skenv_link) (md_tgt skenv_link) (SimSymbId.mk md_src md_tgt) sm_link. Inductive match_states - (sm_init: SimMem.t) (idx: nat) (st_src0: RTL.state) (st_tgt0: RTL.state) (sm0: SimMem.t): Prop := | match_states_intro (MATCHST: Tailcallproof.match_states st_src0 st_tgt0) diff --git a/backend/TunnelingproofC.v b/backend/TunnelingproofC.v index c77a3a5d..625ccc88 100644 --- a/backend/TunnelingproofC.v +++ b/backend/TunnelingproofC.v @@ -35,7 +35,6 @@ Let tge := (SkEnv.revive (SkEnv.project skenv_link md_tgt.(Mod.sk)) tprog). Definition msp: ModSemPair.t := ModSemPair.mk (md_src skenv_link) (md_tgt skenv_link) (SimSymbId.mk md_src md_tgt) sm_link. Inductive match_states - (sm_init: SimMem.t) (idx: nat) (st_src0: LTL.state) (st_tgt0: LTL.state) (sm0: SimMem.t): Prop := | match_states_intro (MATCHST: Tunnelingproof.match_states st_src0 st_tgt0) @@ -91,7 +90,7 @@ Proof. + econs; eauto; ss. * rpapply match_states_call; eauto. { econs; eauto. - - instantiate (1:= (dummy_stack (fn_sig fd) ls1)). unfold dummy_stack, dummy_function. econs; eauto. + - instantiate (1:= (dummy_stack (fn_sig fd) ls1)). unfold dummy_stack, dummy_function. econs; eauto. - econs; eauto. } { eapply JunkBlock.assign_junk_block_extends; eauto. } * rr. ss. esplits; eauto. diff --git a/backend/UnusedglobproofC.v b/backend/UnusedglobproofC.v index ea278495..8c330c26 100644 --- a/backend/UnusedglobproofC.v +++ b/backend/UnusedglobproofC.v @@ -39,7 +39,6 @@ Definition msp: ModSemPair.t := sm_link. Inductive match_states - (sm_init: SimMem.t) (idx: nat) (st_src0: RTL.state) (st_tgt0: RTL.state) (sm0: SimMem.t): Prop := | match_states_intro (MATCHST: Unusedglobproof.match_states prog tprog (used_set tprog) skenv_link_src skenv_link_tgt ge tge st_src0 st_tgt0 sm0). diff --git a/cfrontend/CminorgenproofC.v b/cfrontend/CminorgenproofC.v index cc335970..b2c44c1f 100644 --- a/cfrontend/CminorgenproofC.v +++ b/cfrontend/CminorgenproofC.v @@ -35,7 +35,6 @@ Let tge: Cminor.genv := (SkEnv.revive (SkEnv.project skenv_link md_tgt.(Mod.sk)) Definition msp: ModSemPair.t := ModSemPair.mk (md_src skenv_link) (md_tgt skenv_link) (SimSymbId.mk md_src md_tgt) sm_link. Inductive match_states - (sm_init: SimMem.t) (idx: nat) (st_src0: Csharpminor.state) (st_tgt0: Cminor.state) (sm0: SimMem.t): Prop := | match_states_intro (MATCHST: Cminorgenproof.match_states skenv_link skenv_link ge st_src0 st_tgt0 sm0) diff --git a/cfrontend/CshmgenproofC.v b/cfrontend/CshmgenproofC.v index 8c177687..32646157 100644 --- a/cfrontend/CshmgenproofC.v +++ b/cfrontend/CshmgenproofC.v @@ -45,7 +45,6 @@ Let tge := (SkEnv.revive (SkEnv.project skenv_link md_tgt.(Mod.sk)) tprog). Definition msp: ModSemPair.t := ModSemPair.mk (md_src skenv_link) (md_tgt skenv_link) (SimSymbId.mk md_src md_tgt) sm_link. Inductive match_states - (sm_init: SimMem.t) (idx: nat) (st_src0: Clight.state) (st_tgt0: Csharpminor.state) (sm0: SimMem.t): Prop := | match_states_intro (MATCHST: Cshmgenproof.match_states prog ge st_src0 st_tgt0) diff --git a/cfrontend/CstrategyproofC.v b/cfrontend/CstrategyproofC.v index d88b6a31..1569a298 100644 --- a/cfrontend/CstrategyproofC.v +++ b/cfrontend/CstrategyproofC.v @@ -41,7 +41,6 @@ Let tge: genv := Build_genv (SkEnv.revive (SkEnv.project skenv_link md_tgt.(Mod. Definition msp: ModSemPair.t := ModSemPair.mk (md_src skenv_link) (md_tgt skenv_link) (SimSymbId.mk md_src md_tgt) sm_link. Inductive match_states - (sm_init: SimMem.t) (idx: nat) (st_src0: Csem.state) (st_tgt0: Csem.state) (sm0: SimMem.t): Prop := | match_states_intro (MATCHST: st_src0 = st_tgt0) diff --git a/cfrontend/SimplExprproofC.v b/cfrontend/SimplExprproofC.v index e5584c84..71ecb65b 100644 --- a/cfrontend/SimplExprproofC.v +++ b/cfrontend/SimplExprproofC.v @@ -33,7 +33,7 @@ Let ge: Csem.genv := Csem.Build_genv (SkEnv.revive (SkEnv.project skenv_link md_ Let tge: genv := Build_genv (SkEnv.revive (SkEnv.project skenv_link md_tgt.(Mod.sk)) tprog) tprog.(prog_comp_env). Definition msp: ModSemPair.t := ModSemPair.mk (md_src skenv_link) (md_tgt skenv_link) (SimSymbId.mk md_src md_tgt) sm_link. -Inductive match_states (sm_init: SimMem.t) +Inductive match_states (idx: nat) (st_src0: Csem.state) (st_tgt0: Clight.state) (sm0: SimMem.t): Prop := | match_states_intro (MATCHST: SimplExprproof.match_states tge st_src0 st_tgt0) diff --git a/cfrontend/SimplLocalsproofC.v b/cfrontend/SimplLocalsproofC.v index 35748f48..8ffd6e0c 100644 --- a/cfrontend/SimplLocalsproofC.v +++ b/cfrontend/SimplLocalsproofC.v @@ -75,7 +75,6 @@ Let tge := Build_genv (SkEnv.revive (SkEnv.project skenv_link md_tgt.(Mod.sk)) t Definition msp: ModSemPair.t := ModSemPair.mk (md_src skenv_link) (md_tgt skenv_link) (SimSymbId.mk md_src md_tgt) sm_link. Inductive match_states - (sm_init: SimMem.t) (idx: nat) (st_src0: Clight.state) (st_tgt0: Clight.state) (sm0: SimMem.t): Prop := | match_states_intro (MATCHST: SimplLocalsproof.match_states skenv_link skenv_link ge st_src0 st_tgt0 sm0). diff --git a/demo/mutrec/IdSimClightIdInv.v b/demo/mutrec/IdSimClightIdInv.v index fecc611c..7aa4c497 100644 --- a/demo/mutrec/IdSimClightIdInv.v +++ b/demo/mutrec/IdSimClightIdInv.v @@ -44,7 +44,7 @@ Local Instance SimSymbP: SimSymb.class SimMemP := SimMemInjInvC.SimSymbIdInv P. Local Existing Instance SoundTop.Top. -Inductive match_states_clight_inv (sm_arg: SimMem.t) +Inductive match_states_clight_inv : unit -> Clight.state -> Clight.state -> SimMem.t -> Prop := | match_states_clight_intro st_src st_tgt j m_src m_tgt sm0 @@ -55,7 +55,7 @@ Inductive match_states_clight_inv (sm_arg: SimMem.t) (MWF: SimMem.wf sm0) : match_states_clight_inv - sm_arg tt st_src st_tgt sm0 + tt st_src st_tgt sm0 . Lemma clight_inj_inv_id diff --git a/demo/mutrec/IdSimMutrecAB.v b/demo/mutrec/IdSimMutrecAB.v index 18532da4..f1462889 100644 --- a/demo/mutrec/IdSimMutrecAB.v +++ b/demo/mutrec/IdSimMutrecAB.v @@ -26,7 +26,7 @@ Set Implicit Arguments. Local Opaque Z.mul Z.add Z.sub Z.div. -Inductive match_states_ext_ab (sm_arg: SimMemExt.t') +Inductive match_states_ext_ab : unit -> state -> state -> SimMemExt.t' -> Prop := | match_ext_Callstate i m_src m_tgt sm0 @@ -35,7 +35,7 @@ Inductive match_states_ext_ab (sm_arg: SimMemExt.t') (MWF: Mem.extends m_src m_tgt) : match_states_ext_ab - sm_arg tt + tt (Callstate i m_src) (Callstate i m_tgt) sm0 @@ -46,7 +46,7 @@ Inductive match_states_ext_ab (sm_arg: SimMemExt.t') (MWF: Mem.extends m_src m_tgt) : match_states_ext_ab - sm_arg tt + tt (Returnstate i m_src) (Returnstate i m_tgt) sm0. @@ -55,7 +55,7 @@ Section ABSOUNDSTATE. Variable skenv_link: SkEnv.t. Variable su: Sound.t. - + Inductive sound_state_ab : state -> Prop := | sound_Callstate @@ -124,7 +124,7 @@ Inductive match_states_ab_internal: j m_src m_tgt . -Inductive match_states_ab (sm_arg: SimMemInj.t') +Inductive match_states_ab : unit -> state -> state -> SimMemInj.t' -> Prop := | match_states_ab_intro st_src st_tgt j m_src m_tgt sm0 @@ -135,7 +135,7 @@ Inductive match_states_ab (sm_arg: SimMemInj.t') (MWF: SimMemInj.wf' sm0) : match_states_ab - sm_arg tt st_src st_tgt sm0 + tt st_src st_tgt sm0 . Lemma a_id @@ -150,7 +150,7 @@ Proof. eapply any_id; auto. Qed. -Lemma a_ext_unreach +Lemma a_ext_unreach (WF: Sk.wf MutrecABspec.module) : exists mp, @@ -284,14 +284,14 @@ Proof. inv SIMSKENV. ss. inv SIMSKE. ss. inv FPTR. exploit SIMDEF; eauto. i. des. clarify. esplits; eauto. econs; ss; eauto. unfold Genv.find_funct_ptr. des_ifs. - + - i. inv MATCH; eauto. - i. ss. inv FINALSRC. inv MATCH. inv MATCHST. esplits; eauto. + econs. + econs; eauto. econs. + refl. - + - right. ii. des. esplits. + i. inv MATCH; inv MATCHST; ss. @@ -338,7 +338,7 @@ Local Existing Instance SimSymbDropInv.SimSymbDropInv. Local Existing Instance SoundTop.Top. -Inductive match_states_ab_inv (sm_arg: SimMem.t) +Inductive match_states_ab_inv : unit -> state -> state -> SimMem.t -> Prop := | match_states_ab_inv_intro st_src st_tgt j m_src m_tgt sm0 @@ -349,7 +349,7 @@ Inductive match_states_ab_inv (sm_arg: SimMem.t) (MWF: SimMem.wf sm0) : match_states_ab_inv - sm_arg tt st_src st_tgt sm0. + tt st_src st_tgt sm0. Lemma ab_inj_inv_id @@ -385,14 +385,14 @@ Proof. inv SIMSKENV. ss. inv SIMSKE. ss. inv FPTR. exploit SIMDEF; eauto. i. des. clarify. esplits; eauto. econs; ss; eauto. unfold Genv.find_funct_ptr. des_ifs. - + - i. inv MATCH; eauto. - i. ss. inv FINALSRC. inv MATCH. inv MATCHST. esplits; eauto. + econs. + econs; eauto. econs. + refl. - + - right. ii. des. esplits. + i. inv MATCH; inv MATCHST; ss. diff --git a/demo/mutrec/IdSimMutrecAIdInv.v b/demo/mutrec/IdSimMutrecAIdInv.v index ce638dc8..1775b906 100644 --- a/demo/mutrec/IdSimMutrecAIdInv.v +++ b/demo/mutrec/IdSimMutrecAIdInv.v @@ -71,7 +71,7 @@ Local Instance SimSymbP: SimSymb.class SimMemP := SimMemInjInvC.SimSymbIdInv P. Local Existing Instance SoundTop.Top. -Inductive match_states_a_inv (sm_arg: SimMem.t) +Inductive match_states_a_inv : unit -> state -> state -> SimMem.t -> Prop := | match_states_a_intro st_src st_tgt j m_src m_tgt sm0 @@ -82,7 +82,7 @@ Inductive match_states_a_inv (sm_arg: SimMem.t) (MWF: SimMem.wf sm0) : match_states_a_inv - sm_arg tt st_src st_tgt sm0 + tt st_src st_tgt sm0 . Lemma a_inj_inv_id diff --git a/demo/mutrec/IdSimMutrecBIdInv.v b/demo/mutrec/IdSimMutrecBIdInv.v index 74145b80..813f90ec 100644 --- a/demo/mutrec/IdSimMutrecBIdInv.v +++ b/demo/mutrec/IdSimMutrecBIdInv.v @@ -71,7 +71,7 @@ Local Instance SimSymbP: SimSymb.class SimMemP := SimMemInjInvC.SimSymbIdInv P. Local Existing Instance SoundTop.Top. -Inductive match_states_b_inv (sm_arg: SimMem.t) +Inductive match_states_b_inv : unit -> state -> state -> SimMem.t -> Prop := | match_states_a_intro st_src st_tgt j m_src m_tgt sm0 @@ -82,7 +82,7 @@ Inductive match_states_b_inv (sm_arg: SimMem.t) (MWF: SimMem.wf sm0) : match_states_b_inv - sm_arg tt st_src st_tgt sm0 + tt st_src st_tgt sm0 . Lemma b_inj_inv_id diff --git a/demo/mutrec/MutrecAproof.v b/demo/mutrec/MutrecAproof.v index d33360c5..67b3e82c 100644 --- a/demo/mutrec/MutrecAproof.v +++ b/demo/mutrec/MutrecAproof.v @@ -125,14 +125,13 @@ Inductive match_states_internal: nat -> MutrecAspec.state -> Clight.state -> Pro -Inductive match_states (sm_init: SimMem.t) +Inductive match_states (idx: nat) (st_src0: MutrecAspec.state) (st_tgt0: Clight.state) (sm0: SimMem.t): Prop := | match_states_intro (MATCHST: match_states_internal idx st_src0 st_tgt0) (MCOMPATSRC: st_src0.(get_mem) = sm0.(SimMem.src)) (MCOMPATTGT: st_tgt0.(ClightC.get_mem) = sm0.(SimMem.tgt)) (MWF: SimMem.wf sm0) - (MLE: SimMem.le sm_init sm0) . Lemma g_blk_exists @@ -187,17 +186,17 @@ Proof. Qed. Lemma match_states_lxsim - sm_init idx st_src0 st_tgt0 sm0 + idx st_src0 st_tgt0 sm0 (SIMSK: SimSymb.sim_skenv sm0 (SimMemInjInvC.mk symbol_memoized md_src md_tgt) (SkEnv.project skenv_link (CSk.of_program signature_of_function prog)) (SkEnv.project skenv_link (CSk.of_program signature_of_function prog))) - (MATCH: match_states sm_init idx st_src0 st_tgt0 sm0) + (MATCH: match_states idx st_src0 st_tgt0 sm0) : < unit -> exists su m_init, SoundTop.sound_state su m_init st) top3 (fun _ _ => SimMem.le) - sm_init (Ord.lift_idx lt_wf idx) st_src0 st_tgt0 sm0>> + (Ord.lift_idx lt_wf idx) st_src0 st_tgt0 sm0>> . Proof. revert_until tge. @@ -461,19 +460,19 @@ Proof. hexploit Mem.valid_access_store. { instantiate (4:=sm_ret.(SimMemInjInv.minj).(SimMemInj.tgt)). inv MWF. inv WF. exploit SATTGT0; eauto. - - inv MLE0. erewrite <- MINVEQTGT. eauto. + - inv MLE. erewrite <- MINVEQTGT. eauto. - i. inv H0. hexploit PERMISSIONS0; eauto. ss. esplits; eauto. } intros [m_tgt STR]. - exploit SimMemInjInvC.unlift_wf; try apply MLE0; eauto. + exploit SimMemInjInvC.unlift_wf; try apply MLE; eauto. { econs; eauto. } intros MLE1. exploit memoized_inv_store_le; eauto. i. des. esplits. { econs; eauto. } - { apply MLE2. } + { apply MLE0. } left. pfold. econs; eauto. i; des. econs 2; eauto. { @@ -561,9 +560,9 @@ Proof. etrans; eauto. { exploit (SimMemLift.lift_priv sm0); eauto. ss. } etrans; eauto; cycle 1. - { hexploit SimMem.pub_priv; try apply MLE2. eauto. } + { hexploit SimMem.pub_priv; try apply MLE0. eauto. } etrans; eauto. - { hexploit SimMem.pub_priv; try apply MLE0; eauto. } + { hexploit SimMem.pub_priv; try apply MLE; eauto. } hexploit SimMemLift.unlift_priv; revgoals. { intro T. ss. eauto. } { eauto. } @@ -579,8 +578,6 @@ Proof. rewrite Int.sub_zero_r. rewrite sum_recurse. des_ifs. } econs 2. - - etrans; eauto. etrans; eauto. - eapply SimMemInjInvC.unlift_spec; eauto. econs; eauto. } } @@ -723,7 +720,8 @@ Proof. - (* return *) econs 4; ss; eauto. - econs; ss; eauto. + + refl. + + econs; ss; eauto. Qed. Theorem sim_modsem @@ -773,7 +771,6 @@ Proof. * inv SIMSKENV; eauto. * econs; eauto. { econs; eauto. omega. } - { refl. } - (* init progress *) i. diff --git a/demo/mutrec/MutrecBproof.v b/demo/mutrec/MutrecBproof.v index 7f2ff348..53dbb55d 100644 --- a/demo/mutrec/MutrecBproof.v +++ b/demo/mutrec/MutrecBproof.v @@ -176,7 +176,7 @@ Inductive curr_pc (v: val) (ofs: ptrofs): Prop := Require Import mktac. -Inductive match_states (sm_init: SimMem.t) +Inductive match_states : nat -> MutrecBspec.state -> AsmC.state -> SimMem.t -> Prop := | match_states_initial @@ -185,7 +185,6 @@ Inductive match_states (sm_init: SimMem.t) (MCOMPATSRC: m_src = sm0.(SimMem.src)) (MCOMPATTGT: m_tgt = sm0.(SimMem.tgt)) (MWF: SimMem.wf sm0) - (MLE: SimMem.le sm_init sm0) (SAVED: well_saved initstk stk init_rs rs m_tgt) (PRIV: forall blk_src blk_tgt delta @@ -200,7 +199,7 @@ Inductive match_states (sm_init: SimMem.t) (RANGE: 0 <= i.(Int.intval) < MAX) (IDX: (idx > 9)%nat) : - match_states sm_init idx (Callstate i m_src) + match_states idx (Callstate i m_src) (AsmC.mkstate init_rs (Asm.State rs m_tgt)) sm0 | match_states_at_external @@ -209,7 +208,6 @@ Inductive match_states (sm_init: SimMem.t) (MCOMPATSRC: m_src = sm0.(SimMem.src)) (MCOMPATTGT: m_tgt = sm0.(SimMem.tgt)) (MWF: SimMem.wf sm0) - (MLE: SimMem.le sm_init sm0) (SAVED: well_saved initstk stk init_rs rs m_tgt) (PRIV: forall blk_src blk_tgt delta @@ -225,7 +223,7 @@ Inductive match_states (sm_init: SimMem.t) (RANGE: 0 < i.(Int.intval) < MAX) (IDX: (idx > 6)%nat) : - match_states sm_init idx (Interstate i m_src) + match_states idx (Interstate i m_src) (AsmC.mkstate init_rs (Asm.State rs m_tgt)) sm0 | match_states_after_external @@ -234,7 +232,6 @@ Inductive match_states (sm_init: SimMem.t) (MCOMPATSRC: m_src = sm0.(SimMem.src)) (MCOMPATTGT: m_tgt = sm0.(SimMem.tgt)) (MWF: SimMem.wf sm0) - (MLE: SimMem.le sm_init sm0) (SAVED: well_saved initstk stk init_rs rs m_tgt) (PRIV: forall blk_src blk_tgt delta @@ -250,7 +247,7 @@ Inductive match_states (sm_init: SimMem.t) (RANGE: 0 < i.(Int.intval) < MAX) (IDX: (idx > 3)%nat) : - match_states sm_init idx (Returnstate (sum i) m_src) + match_states idx (Returnstate (sum i) m_src) (AsmC.mkstate init_rs (Asm.State rs m_tgt))sm0 | match_states_final @@ -259,7 +256,6 @@ Inductive match_states (sm_init: SimMem.t) (MCOMPATSRC: m_src = sm0.(SimMem.src)) (MCOMPATTGT: m_tgt = sm0.(SimMem.tgt)) (MWF: SimMem.wf sm0) - (MLE: SimMem.le sm_init sm0) (SAVED: well_saved initstk stk init_rs rs m_tgt) (PRIV: forall blk_src blk_tgt delta @@ -273,7 +269,7 @@ Inductive match_states (sm_init: SimMem.t) (ARG: rs RAX = Vint i) (IDX: (idx >= 2)%nat) : - match_states sm_init idx (Returnstate i m_src) + match_states idx (Returnstate i m_src) (AsmC.mkstate init_rs (Asm.State rs m_tgt)) sm0 . @@ -338,17 +334,17 @@ Proof. auto. Qed. Hint Resolve E0_double. Lemma match_states_lxsim - sm_init idx st_src0 st_tgt0 sm0 + idx st_src0 st_tgt0 sm0 (SIMSK: SimSymb.sim_skenv sm0 (SimMemInjInvC.mk symbol_memoized md_src md_tgt) (SkEnv.project skenv_link (Sk.of_program fn_sig prog)) (SkEnv.project skenv_link (Sk.of_program fn_sig prog))) - (MATCH: match_states sm_init idx st_src0 st_tgt0 sm0) + (MATCH: match_states idx st_src0 st_tgt0 sm0) : < unit -> exists su m_init, SoundTop.sound_state su m_init st) (top3) (fun _ _ => SimMem.le) - sm_init (Ord.lift_idx lt_wf idx) st_src0 st_tgt0 sm0>> + (Ord.lift_idx lt_wf idx) st_src0 st_tgt0 sm0>> . Proof. destruct (Genv.find_symbol @@ -887,7 +883,7 @@ Proof. exploit Mem_unfree_suceeds. { instantiate (1:=stk). instantiate (1:=SimMemInj.tgt sm_ret.(SimMemInjInv.minj)). - inv MLE1. inv MLE2. ss. + inv MLE0. inv MLE1. ss. unfold Mem.valid_block. eapply Plt_Ple_trans; eauto. - eapply Mem.perm_valid_block; eauto. eapply STKPERM; eauto. instantiate (1:=0). lia. @@ -896,8 +892,8 @@ Proof. exploit Mem_unfree_right_inject; try apply UNFR; eauto. { inv MWF1. inv WF1. eauto. } { instantiate (1:=0). instantiate (1:=0). ii. lia. } intros INJ. - eapply SimMemInjInvC.unlift_wf in MWF1; try apply MLE1; eauto. - dup MLE1. eapply SimMemInjInvC.unlift_spec in MLE1; eauto. + eapply SimMemInjInvC.unlift_wf in MWF1; try apply MLE0; eauto. + dup MLE0. eapply SimMemInjInvC.unlift_spec in MLE0; eauto. exploit SimMemInjInvC.unchanged_on_mle; eauto. { ss. ii. clarify. } { refl. } @@ -928,7 +924,6 @@ Proof. { exploit SimSymb.mle_preserves_sim_skenv; ss; cycle 1; eauto. etrans; eauto. etrans; eauto. } econs 3; ss; eauto. - - etrans; eauto. etrans; eauto. etrans; eauto. - eapply well_saved_keep; eauto. + unfold is_callee_save, nextinstr_nf, nextinstr, undef_regs, to_preg, preg_of, compare_ints, Pregmap.set. @@ -936,18 +931,18 @@ Proof. + etrans. { eapply Mem.free_unchanged_on; eauto. clear. ii. lia. } etrans. - { inv MLE2. ss. inv MLE4. ss. + { inv MLE1. ss. inv MLE3. ss. eapply Mem.unchanged_on_implies; eauto. ii. clarify. split; auto. split; ss; auto. ii. eapply PRIV; eauto. } { eapply Mem.unchanged_on_implies; eauto. - eapply Mem_unfree_unchanged_on; eauto. - clear. ii. destruct H1. lia. } - - inv MLE1. ss. inv MLE4. ss. ii. clarify. + - inv MLE0. ss. inv MLE3. ss. ii. clarify. destruct (SimMemInj.inj (SimMemInjInv.minj sm0) blk_src) eqn:BLK0. + destruct p. dup BLK0. eapply INCR in BLK0. clarify. hexploit PRIV; eauto. - + inv MLE2. ss. inv MLE1. ss. inv FROZEN0. + + inv MLE1. ss. inv MLE0. ss. inv FROZEN0. exploit NEW_IMPLIES_OUTSIDE; eauto. i. des. inv SAVED. eapply (Plt_strict stk). eapply Plt_Ple_trans; eauto. @@ -1070,8 +1065,6 @@ Proof. { exploit SimSymb.mle_preserves_sim_skenv; ss; cycle 1; eauto. } econs 4; ss; eauto. - * etrans; eauto. - * eapply well_saved_keep; eauto. { unfold is_callee_save, nextinstr_nf, nextinstr, undef_regs, to_preg, preg_of, compare_ints, Pregmap.set. @@ -1147,7 +1140,6 @@ Proof. + left. pfold. intros _. econs 4; ss. * instantiate (1:=SimMemInjInv.mk sm2 _ _). econs; ss; eauto. - etrans; eauto. etrans; eauto. inv MLE. eauto. * hexploit (@SimMemInjInv.le_inj_wf_wf SimMemInjInv.top_inv memoized_inv sm0 sm2); ss; eauto. { etrans; eauto. } { eapply SimMemInjInv.private_unchanged_on_invariant; eauto. @@ -1156,7 +1148,6 @@ Proof. - etrans. + eapply Mem.free_unchanged_on; eauto. + eapply Mem.free_unchanged_on; eauto. clear. ii. lia. } - { destruct sm_init. inv MLE. ss. clarify. } * econs; ss; eauto. { repeat rewrite Pregmap.gss. repeat (rewrite Pregmap.gso; [| clarify; fail]). diff --git a/demo/unreadglob/IdSimClightDropInv.v b/demo/unreadglob/IdSimClightDropInv.v index 000ac838..ac49c976 100644 --- a/demo/unreadglob/IdSimClightDropInv.v +++ b/demo/unreadglob/IdSimClightDropInv.v @@ -44,7 +44,7 @@ Local Existing Instance SimSymbDropInv.SimMemInvTop. Local Existing Instance SimSymbDropInv.SimSymbDropInv. Local Existing Instance SoundTop.Top. -Inductive match_states_clight_inv (sm_arg: SimMem.t) +Inductive match_states_clight_inv : unit -> Clight.state -> Clight.state -> SimMem.t -> Prop := | match_states_clight_inv_intro st_src st_tgt j m_src m_tgt sm0 @@ -55,7 +55,7 @@ Inductive match_states_clight_inv (sm_arg: SimMem.t) (MWF: SimMem.wf sm0) : match_states_clight_inv - sm_arg tt st_src st_tgt sm0 + tt st_src st_tgt sm0 . Lemma clight_inj_inv_drop diff --git a/demo/unreadglob/IdSimInvExtra.v b/demo/unreadglob/IdSimInvExtra.v index 1790aff9..70c05af4 100644 --- a/demo/unreadglob/IdSimInvExtra.v +++ b/demo/unreadglob/IdSimInvExtra.v @@ -319,7 +319,6 @@ Require Import AsmC. Inductive match_states P0 P1 (skenv_link_tgt: SkEnv.t) (ge_src ge_tgt: genv) - (sm_init : SimMemInjInv.t') : nat-> AsmC.state -> AsmC.state -> SimMemInjInv.t' -> Prop := | match_states_intro j init_rs_src init_rs_tgt rs_src rs_tgt m_src m_tgt @@ -342,7 +341,7 @@ Inductive match_states P0 P1 match_states P0 P1 skenv_link_tgt - ge_src ge_tgt sm_init 0 + ge_src ge_tgt 0 (AsmC.mkstate init_rs_src (Asm.State rs_src m_src)) (AsmC.mkstate init_rs_tgt (Asm.State rs_tgt m_tgt)) sm0 . diff --git a/demo/unreadglob/UnreadglobproofC.v b/demo/unreadglob/UnreadglobproofC.v index e70c34cb..76fb25fa 100644 --- a/demo/unreadglob/UnreadglobproofC.v +++ b/demo/unreadglob/UnreadglobproofC.v @@ -45,7 +45,6 @@ Definition msp: ModSemPair.t := . Inductive match_states - (sm_init: SimMem.t) (idx: nat) (st_src0: RTL.state) (st_tgt0: RTL.state) (sm0: SimMem.t): Prop := | match_states_intro (MATCHST: Unreadglobproof.match_states prog tprog (used_set tprog) skenv_link_src skenv_link_tgt ge tge st_src0 st_tgt0 sm0) diff --git a/demo/utod/DemoSpecProof.v b/demo/utod/DemoSpecProof.v index b6f260c0..2830ec85 100644 --- a/demo/utod/DemoSpecProof.v +++ b/demo/utod/DemoSpecProof.v @@ -222,12 +222,12 @@ Proof. assert (ARGLONG: exists lng, (Args.vs args_src) = [Vlong lng]). { inv SAFESRC. inv H. rewrite VS. eauto. } inv INITTGT; ss; clarify. inv TYP. ss. - inv SIMARGS; ss. clarify. inv VALS; ss. inv H0; 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 H3. eexists (DemoSpec.mkstate lng (SimMemInj.src sm_arg)). esplits; eauto. - refl. @@ -341,7 +341,7 @@ Proof. { rewrite Int64.unsigned_zero in *. set (Int64.unsigned_range_2 i). nia. } ss. rewrite Float.mul2_add. rewrite Float.of_longu_of_long_2; auto. unfold Int64.ltu. des_ifs. - -- ss. + -- refl. -- eauto. + econs 2. @@ -381,7 +381,7 @@ Proof. set (Int64.unsigned_range i). unfold Int64.ltu, Int64.lt, Int64.signed in *. zsimpl. des_ifs. rewrite Int64.unsigned_zero in *. rewrite Int64.unsigned_repr in *; nia. - -- ss. + -- refl. -- eauto. Unshelve. all: eauto. Qed. diff --git a/demo/utod/IdSimDemoSpec.v b/demo/utod/IdSimDemoSpec.v index b8bb85c7..2387c7d7 100644 --- a/demo/utod/IdSimDemoSpec.v +++ b/demo/utod/IdSimDemoSpec.v @@ -27,7 +27,7 @@ Set Implicit Arguments. Local Opaque Z.mul Z.add Z.sub Z.div. -Inductive match_states_ext_demo (sm_arg: SimMemExt.t') +Inductive match_states_ext_demo : unit -> state -> state -> SimMemExt.t' -> Prop := | match_ext i m_src m_tgt sm0 @@ -36,7 +36,7 @@ Inductive match_states_ext_demo (sm_arg: SimMemExt.t') (MWF: Mem.extends m_src m_tgt) : match_states_ext_demo - sm_arg tt + tt (mkstate i m_src) (mkstate i m_tgt) sm0 @@ -97,7 +97,7 @@ Inductive match_states_demo_internal: j m_src m_tgt . -Inductive match_states_demo (sm_arg: SimMemInj.t') +Inductive match_states_demo : unit -> state -> state -> SimMemInj.t' -> Prop := | match_states_demo_intro st_src st_tgt j m_src m_tgt sm0 @@ -108,7 +108,7 @@ Inductive match_states_demo (sm_arg: SimMemInj.t') (MWF: SimMemInj.wf' sm0) : match_states_demo - sm_arg tt st_src st_tgt sm0 + tt st_src st_tgt sm0 . Lemma demo_id @@ -296,7 +296,7 @@ Local Existing Instance SimSymbDropInv.SimSymbDropInv. Local Existing Instance SoundTop.Top. -Inductive match_states_demo_inv (sm_arg: SimMem.t) +Inductive match_states_demo_inv : unit -> state -> state -> SimMem.t -> Prop := | match_states_demo_inv_intro st_src st_tgt j m_src m_tgt sm0 @@ -307,7 +307,7 @@ Inductive match_states_demo_inv (sm_arg: SimMem.t) (MWF: SimMem.wf sm0) : match_states_demo_inv - sm_arg tt st_src st_tgt sm0 + tt st_src st_tgt sm0 . Lemma demo_inj_inv diff --git a/proof/AdequacyLocal.v b/proof/AdequacyLocal.v index 1b30c6ce..5d40c7bd 100644 --- a/proof/AdequacyLocal.v +++ b/proof/AdequacyLocal.v @@ -201,7 +201,7 @@ Section SIMGE. - ss. econs; eauto. } left. pfold. econs 4. - { eauto. } + { refl. } { eauto. } { econs; eauto. } { econs; eauto. } @@ -329,7 +329,7 @@ Section ADQMATCH. (<>) /\ (<>) /\ (< forall si, exists su m_arg, (sound_states_local si) su m_arg st) - tail_sm i1 lst_src1 lst_tgt1 sm_after>>)) + i1 lst_src1 lst_tgt1 sm_after>>)) (SESRC: ms_src.(ModSem.to_semantics).(symbolenv) = skenv_link_src) (SETGT: ms_tgt.(ModSem.to_semantics).(symbolenv) = skenv_link_tgt): lxsim_stack sm_init @@ -356,7 +356,7 @@ Section ADQMATCH. (MLE: SimMem.le tail_sm sm0) (sound_states_local: sidx -> Sound.t -> Memory.Mem.mem -> ms_src.(ModSem.state) -> Prop) (PRSV: forall si, local_preservation_noguarantee ms_src (sound_states_local si)) - (TOP: lxsim ms_src ms_tgt (fun st => forall si, exists su m_arg, (sound_states_local si) su m_arg st) tail_sm + (TOP: lxsim ms_src ms_tgt (fun st => forall si, exists su m_arg, (sound_states_local si) su m_arg st) i0 lst_src lst_tgt sm0) (SESRC: ms_src.(ModSem.to_semantics).(symbolenv) = skenv_link_src) (SETGT: ms_tgt.(ModSem.to_semantics).(symbolenv) = skenv_link_tgt): @@ -537,7 +537,7 @@ Section ADQSTEP. } instantiate (1:= sm_init). econs; try apply SIM0; eauto. + ss. folder. des_ifs. eapply mfuture_preserves_sim_ge; eauto. apply rtc_once. et. - + eapply lxsim_stack_le; eauto. + + etrans; eauto. + ss. inv GE. folder. rewrite Forall_forall in *. eapply SESRC; et. + ss. inv GE. folder. rewrite Forall_forall in *. eapply SETGT; et. @@ -666,7 +666,7 @@ Section ADQSTEP. inv STACK; ss. folder. sguard in SESRC0. sguard in SETGT0. des_ifs. determ_tac ModSem.final_frame_dtm. clear_tac. exploit K; try apply SIMRETV; eauto. - { etransitivity; eauto. } + { etransitivity; eauto. etrans; eauto. } { unsguard SUST. des_safe. inv SUST. des. simpl_depind. clarify. i. inv TL. simpl_depind. clarify. des. exploit FORALLSU0; eauto. i; des. esplits; eauto. eapply HD; eauto. } diff --git a/proof/MatchSimModSem.v b/proof/MatchSimModSem.v index 023e559b..6fcd6f16 100644 --- a/proof/MatchSimModSem.v +++ b/proof/MatchSimModSem.v @@ -28,7 +28,6 @@ Section MATCHSIMFORWARD. Hypothesis PRSV: local_preservation ms_src sound_state. Variable match_states: forall - (sm_arg: SimMem.t) (idx: index) (st_src0: ms_src.(ModSem.state)) (st_tgt0: ms_tgt.(ModSem.state)) (sm0: SimMem.t), Prop. @@ -37,10 +36,9 @@ Section MATCHSIMFORWARD. Prop. Inductive match_states_at_helper - (sm_init: SimMem.t) (idx_at: index) (st_src0: ms_src.(ModSem.state)) (st_tgt0: ms_tgt.(ModSem.state)) (sm_at sm_arg: SimMem.t): Prop := | match_states_at_intro - (MATCH: match_states sm_init idx_at st_src0 st_tgt0 sm_at) + (MATCH: match_states idx_at st_src0 st_tgt0 sm_at) args_src args_tgt (CALLSRC: ms_src.(ModSem.at_external) st_src0 args_src) (CALLTGT: ms_tgt.(ModSem.at_external) st_tgt0 args_tgt) @@ -58,7 +56,7 @@ Section MATCHSIMFORWARD. exists st_init_src sm_init idx_init, (<>) /\ (<>) /\ - (<>). + (<>). Hypothesis INITPROGRESS: forall sm_arg args_src args_tgt (SIMSKENV: ModSemPair.sim_skenv msp sm_arg) @@ -67,14 +65,14 @@ Section MATCHSIMFORWARD. (SAFESRC: exists st_init_src, ms_src.(ModSem.initial_frame) args_src st_init_src), exists st_init_tgt, (<>). - Hypothesis ATMWF: forall sm_init idx0 st_src0 st_tgt0 sm0 - (MATCH: match_states sm_init idx0 st_src0 st_tgt0 sm0) + Hypothesis ATMWF: forall idx0 st_src0 st_tgt0 sm0 + (MATCH: match_states idx0 st_src0 st_tgt0 sm0) (CALLSRC: ms_src.(ModSem.is_call) st_src0), <>. - Hypothesis ATFSIM: forall sm_init idx0 st_src0 st_tgt0 sm0 args_src + Hypothesis ATFSIM: forall idx0 st_src0 st_tgt0 sm0 args_src (SIMSKENV: ModSemPair.sim_skenv msp sm0) - (MATCH: match_states sm_init idx0 st_src0 st_tgt0 sm0) + (MATCH: match_states idx0 st_src0 st_tgt0 sm0) (CALLSRC: ms_src.(ModSem.at_external) st_src0 args_src) (SOUND: exists su0 m_init, (sound_state) su0 m_init st_src0), exists args_tgt sm_arg, @@ -84,9 +82,9 @@ Section MATCHSIMFORWARD. (<>) /\ (<>). - Hypothesis AFTERFSIM: forall sm_init idx0 st_src0 st_tgt0 sm0 sm_arg sm_ret retv_src retv_tgt st_src1 + Hypothesis AFTERFSIM: forall idx0 st_src0 st_tgt0 sm0 sm_arg sm_ret retv_src retv_tgt st_src1 (SIMSKENV: ModSemPair.sim_skenv msp sm0) - (MATCH: match_states sm_init idx0 st_src0 st_tgt0 sm0) + (MATCH: match_states idx0 st_src0 st_tgt0 sm0) (MLE: SimMem.le sm0 sm_arg) (* (MWF: SimMem.wf sm_arg) *) (MLE: SimMem.le (SimMemLift.lift sm_arg) sm_ret) @@ -96,20 +94,19 @@ Section MATCHSIMFORWARD. (SOUND: exists su0 m_init, (sound_state) su0 m_init st_src0) (* history *) - (HISTORY: match_states_at_helper sm_init idx0 st_src0 st_tgt0 sm0 sm_arg) + (HISTORY: match_states_at_helper idx0 st_src0 st_tgt0 sm0 sm_arg) (* just helpers *) (MWFAFTR: SimMem.wf (SimMemLift.unlift sm_arg sm_ret)) (MLEAFTR: SimMem.le sm_arg (SimMemLift.unlift sm_arg sm_ret)), exists sm_after idx1 st_tgt1, (<>) /\ - (<>) /\ + (<>) /\ (<>). - Hypothesis FINALFSIM: forall sm_init idx0 st_src0 st_tgt0 sm0 retv_src + Hypothesis FINALFSIM: forall idx0 st_src0 st_tgt0 sm0 retv_src (SIMSKENV: ModSemPair.sim_skenv msp sm0) - (MFUTURE: SimMem.le sm_init sm0) - (MATCH: match_states sm_init idx0 st_src0 st_tgt0 sm0) + (MATCH: match_states idx0 st_src0 st_tgt0 sm0) (FINALSRC: ms_src.(ModSem.final_frame) st_src0 retv_src), exists sm_ret retv_tgt, (<>) /\ @@ -117,11 +114,11 @@ Section MATCHSIMFORWARD. (<>) /\ (<>). - Let STEPFSIM := forall sm_init idx0 st_src0 st_tgt0 sm0 + Let STEPFSIM := forall idx0 st_src0 st_tgt0 sm0 (SIMSKENV: ModSemPair.sim_skenv msp sm0) (NOTCALL: ~ ModSem.is_call ms_src st_src0) (NOTRET: ~ ModSem.is_return ms_src st_src0) - (MATCH: match_states sm_init idx0 st_src0 st_tgt0 sm0) + (MATCH: match_states idx0 st_src0 st_tgt0 sm0) (SOUND: exists su0 m_init, (sound_state) su0 m_init st_src0), (<>) /\ (<> \/ <>) /\ (<>) (* Note: We require le for mle_preserves_sim_ge, but we cannot require SimMem.wf, beacuse of DCEproof *) - /\ (<>)>>). + /\ (<>)>>). - Let STEPBSIM := forall sm_init idx0 st_src0 st_tgt0 sm0 + Let STEPBSIM := forall idx0 st_src0 st_tgt0 sm0 (SIMSKENV: ModSemPair.sim_skenv msp sm0) (NOTCALL: ~ ModSem.is_call ms_src st_src0) (NOTRET: ~ ModSem.is_return ms_src st_src0) - (MATCH: match_states sm_init idx0 st_src0 st_tgt0 sm0) + (MATCH: match_states idx0 st_src0 st_tgt0 sm0) (SOUND: exists su0 m_init, (sound_state) su0 m_init st_src0), (* (< ModSem.is_step ms_tgt st_tgt0>>) *) (< ModSem.is_step ms_tgt st_tgt0>>) /\ @@ -146,7 +143,7 @@ Section MATCHSIMFORWARD. (<> \/ <>) /\ (<>) (* Note: We require le for mle_preserves_sim_ge, but we cannot require SimMem.wf, beacuse of DCEproof *) - /\ (<>)>>). + /\ (<>)>>). Remark safe_modsem_is_smaller st_src0 @@ -179,4 +176,3 @@ Section MATCHSIMFORWARD. Qed. End MATCHSIMFORWARD. - diff --git a/proof/MatchSimModSemExcl.v b/proof/MatchSimModSemExcl.v index f89a668c..ba3a05a5 100644 --- a/proof/MatchSimModSemExcl.v +++ b/proof/MatchSimModSemExcl.v @@ -28,7 +28,7 @@ Section MATCHSIMFORWARD. Hypothesis PRSV: forall si, local_preservation ms_src (sound_states si). Variable match_states: forall - (sm_arg: SimMem.t) (idx: index) (st_src0: ms_src.(ModSem.state)) (st_tgt0: ms_tgt.(ModSem.state)) (sm0: SimMem.t), + (idx: index) (st_src0: ms_src.(ModSem.state)) (st_tgt0: ms_tgt.(ModSem.state)) (sm0: SimMem.t), Prop. Variable match_states_at: forall @@ -59,10 +59,9 @@ Section MATCHSIMFORWARD. <>). Inductive match_states_at_helper - (sm_init: SimMem.t) (idx_at: index) (st_src0: ms_src.(ModSem.state)) (st_tgt0: ms_tgt.(ModSem.state)) (sm_at sm_arg: SimMem.t): Prop := | match_states_at_intro - (MATCH: match_states sm_init idx_at st_src0 st_tgt0 sm_at) + (MATCH: match_states idx_at st_src0 st_tgt0 sm_at) args_src args_tgt (CALLSRC: ms_src.(ModSem.at_external) st_src0 args_src) (CALLTGT: ms_tgt.(ModSem.at_external) st_tgt0 args_tgt) @@ -81,8 +80,7 @@ Section MATCHSIMFORWARD. exists st_init_src sm_init idx_init, (<>) /\ (<>) /\ - (<>). + (<>). Hypothesis INITPROGRESS: forall sm_arg args_src args_tgt (SIMSKENV: ModSemPair.sim_skenv msp sm_arg) @@ -91,14 +89,14 @@ Section MATCHSIMFORWARD. (SAFESRC: exists st_init_src, ms_src.(ModSem.initial_frame) args_src st_init_src), exists st_init_tgt, (<>). - Hypothesis ATMWF: forall sm_init idx0 st_src0 st_tgt0 sm0 - (MATCH: match_states sm_init idx0 st_src0 st_tgt0 sm0) + Hypothesis ATMWF: forall idx0 st_src0 st_tgt0 sm0 + (MATCH: match_states idx0 st_src0 st_tgt0 sm0) (CALLSRC: ms_src.(ModSem.is_call) st_src0), <>. - Hypothesis ATFSIM: forall sm_init idx0 st_src0 st_tgt0 sm0 args_src + Hypothesis ATFSIM: forall idx0 st_src0 st_tgt0 sm0 args_src (SIMSKENV: ModSemPair.sim_skenv msp sm0) - (MATCH: match_states sm_init idx0 st_src0 st_tgt0 sm0) + (MATCH: match_states idx0 st_src0 st_tgt0 sm0) (CALLSRC: ms_src.(ModSem.at_external) st_src0 args_src) (SOUND: forall si, exists su0 m_init, (sound_states si) su0 m_init st_src0), exists args_tgt sm_arg, @@ -109,9 +107,9 @@ Section MATCHSIMFORWARD. (<>) /\ (<>). - Hypothesis AFTERFSIM: forall sm_init idx0 st_src0 st_tgt0 sm0 sm_arg sm_ret retv_src retv_tgt st_src1 + Hypothesis AFTERFSIM: forall idx0 st_src0 st_tgt0 sm0 sm_arg sm_ret retv_src retv_tgt st_src1 (SIMSKENV: ModSemPair.sim_skenv msp sm0) - (MATCH: match_states sm_init idx0 st_src0 st_tgt0 sm0) + (MATCH: match_states idx0 st_src0 st_tgt0 sm0) (MLE: SimMem.le sm0 sm_arg) (* (MWF: SimMem.wf sm_arg) *) (MLE: SimMem.le (SimMemLift.lift sm_arg) sm_ret) @@ -121,7 +119,7 @@ Section MATCHSIMFORWARD. (SOUND: forall si, exists su0 m_init, (sound_states si) su0 m_init st_src0) (* history *) - (HISTORY: match_states_at_helper sm_init idx0 st_src0 st_tgt0 sm0 sm_arg) + (HISTORY: match_states_at_helper idx0 st_src0 st_tgt0 sm0 sm_arg) (* just helpers *) (MWFAFTR: SimMem.wf (SimMemLift.unlift sm_arg sm_ret)) @@ -130,12 +128,11 @@ Section MATCHSIMFORWARD. (<>) /\ forall (MLE: SimMem.le sm0 sm_after) (* helper *), ((<>) /\ - (<>)). + (<>)). - Hypothesis FINALFSIM: forall sm_init idx0 st_src0 st_tgt0 sm0 retv_src + Hypothesis FINALFSIM: forall idx0 st_src0 st_tgt0 sm0 retv_src (SIMSKENV: ModSemPair.sim_skenv msp sm0) - (MFUTURE: SimMem.le sm_init sm0) - (MATCH: match_states sm_init idx0 st_src0 st_tgt0 sm0) + (MATCH: match_states idx0 st_src0 st_tgt0 sm0) (FINALSRC: ms_src.(ModSem.final_frame) st_src0 retv_src), exists sm_ret retv_tgt, (<>) /\ @@ -143,11 +140,11 @@ Section MATCHSIMFORWARD. (<>) /\ (<>). - Let STEPFSIM := forall sm_init idx0 st_src0 st_tgt0 sm0 + Let STEPFSIM := forall idx0 st_src0 st_tgt0 sm0 (SIMSKENV: ModSemPair.sim_skenv msp sm0) (NOTCALL: ~ ModSem.is_call ms_src st_src0) (NOTRET: ~ ModSem.is_return ms_src st_src0) - (MATCH: match_states sm_init idx0 st_src0 st_tgt0 sm0) + (MATCH: match_states idx0 st_src0 st_tgt0 sm0) (SOUND: forall si, exists su0 m_init, (sound_states si) su0 m_init st_src0), (<>) /\ (<>) /\ (<>) (* Note: We require le for mle_preserves_sim_ge, but we cannot require SimMem.wf, beacuse of DCEproof *) - /\ (<>)>>). + /\ (<>)>>). - Let STEPBSIM := forall sm_init idx0 st_src0 st_tgt0 sm0 + Let STEPBSIM := forall idx0 st_src0 st_tgt0 sm0 (SIMSKENV: ModSemPair.sim_skenv msp sm0) (NOTCALL: ~ ModSem.is_call ms_src st_src0) (NOTRET: ~ ModSem.is_return ms_src st_src0) - (MATCH: match_states sm_init idx0 st_src0 st_tgt0 sm0) + (MATCH: match_states idx0 st_src0 st_tgt0 sm0) (SOUND: forall si, exists su0 m_init, (sound_states si) su0 m_init st_src0) , (< ModSem.is_step ms_tgt st_tgt0>>) /\ (<>) /\ (<>) (* Note: We require le for mle_preserves_sim_ge, but we cannot require SimMem.wf, beacuse of DCEproof *) - /\ (<>)>>). + /\ (<>)>>). Hypothesis STEPSIM: STEPFSIM \/ STEPBSIM. Hypothesis BAR: bar_True. Lemma match_states_lxsim - sm_init i0 st_src0 st_tgt0 sm0 + i0 st_src0 st_tgt0 sm0 (SIMSKENV: ModSemPair.sim_skenv msp sm0) - (MLE: SimMem.le sm_init sm0) (* (MWF: SimMem.wf sm0) *) (* (MCOMPAT: mem_compat st_src0 st_tgt0 sm0) *) - (MATCH: match_states sm_init i0 st_src0 st_tgt0 sm0): + (MATCH: match_states i0 st_src0 st_tgt0 sm0): (* su0 *) (* <> *) < forall si, exists su0 m_init, sound_states si su0 m_init st) has_footprint mle_excl - sm_init i0.(Ord.lift_idx WFORD) st_src0 st_tgt0 sm0>>. + i0.(Ord.lift_idx WFORD) st_src0 st_tgt0 sm0>>. Proof. (* move su0 at top. *) revert_until BAR. pcofix CIH. i. pfold. ii. @@ -208,16 +204,16 @@ Section MATCHSIMFORWARD. i; des. assert(MLE3: SimMem.le sm0 sm_after). { eapply FOOTEXCL; et. etrans; et. eapply SimMemLift.lift_spec; et. } - spc H1. des. esplits; eauto. right. eapply CIH; eauto. + spc H1. des. esplits; eauto. right. + eapply CIH; [..|eauto]. { eapply ModSemPair.mfuture_preserves_sim_skenv; try apply SIMSKENV; eauto. apply rtc_once. left. et. } - { etrans; eauto. } } generalize (classic (ModSem.is_return ms_src st_src0)). intro RETSRC; des. { (* RETURN *) u in RETSRC. des. exploit FINALFSIM; eauto. i; des. ii. - eapply lxsim_final; try apply SIMRET; eauto. etrans; eauto. + eapply lxsim_final; try apply SIMRET; eauto. } destruct STEPSIM as [STEPFSIM0|STEPBSIM0]. { eapply lxsim_step_forward; eauto. i. @@ -226,9 +222,8 @@ Section MATCHSIMFORWARD. - des. + left. eauto. + right. esplits; eauto. eapply Ord.lift_idx_spec; eauto. - - right. eapply CIH; eauto. + - right. eapply CIH; [..|eauto]. { eapply ModSemPair.mfuture_preserves_sim_skenv; try apply SIMSKENV; eauto. apply rtc_once; eauto. } - { etransitivity; eauto. } } { rr in STEPBSIM0. eapply lxsim_step_backward; eauto. i. @@ -237,9 +232,8 @@ Section MATCHSIMFORWARD. - des. + left. eauto. + right. esplits; eauto. eapply Ord.lift_idx_spec; eauto. - - right. eapply CIH; eauto. + - right. eapply CIH; [..|eauto]. { eapply ModSemPair.mfuture_preserves_sim_skenv; try apply SIMSKENV; eauto. apply rtc_once; eauto. } - { etransitivity; eauto. } } Qed. diff --git a/proof/MatchSimModSemExcl2.v b/proof/MatchSimModSemExcl2.v index 461d11cb..abe29ec5 100644 --- a/proof/MatchSimModSemExcl2.v +++ b/proof/MatchSimModSemExcl2.v @@ -29,7 +29,6 @@ Section MATCHSIMFORWARD. Hypothesis PRSV: forall si, local_preservation ms_src (sound_states si). Variable match_states: forall - (sm_arg: SimMem.t) (idx: index) (st_src0: ms_src.(ModSem.state)) (st_tgt0: ms_tgt.(ModSem.state)) (sm0: SimMem.t), Prop. @@ -38,10 +37,9 @@ Section MATCHSIMFORWARD. Prop. Inductive match_states_at_helper - (sm_init: SimMem.t) (idx_at: index) (st_src0: ms_src.(ModSem.state)) (st_tgt0: ms_tgt.(ModSem.state)) (sm_at sm_arg: SimMem.t): Prop := | match_states_at_intro - (MATCH: match_states sm_init idx_at st_src0 st_tgt0 sm_at) + (MATCH: match_states idx_at st_src0 st_tgt0 sm_at) args_src args_tgt (CALLSRC: ms_src.(ModSem.at_external) st_src0 args_src) (CALLTGT: ms_tgt.(ModSem.at_external) st_tgt0 args_tgt) @@ -61,8 +59,7 @@ Section MATCHSIMFORWARD. exists st_init_src sm_init idx_init, (<>) /\ (<>) /\ - (<>). + (<>). Hypothesis INITPROGRESS: forall sm_arg args_src args_tgt (SIMSKENV: ModSemPair.sim_skenv msp sm_arg) @@ -71,14 +68,14 @@ Section MATCHSIMFORWARD. (SAFESRC: exists st_init_src, ms_src.(ModSem.initial_frame) args_src st_init_src), exists st_init_tgt, (<>). - Hypothesis ATMWF: forall sm_init idx0 st_src0 st_tgt0 sm0 - (MATCH: match_states sm_init idx0 st_src0 st_tgt0 sm0) + Hypothesis ATMWF: forall idx0 st_src0 st_tgt0 sm0 + (MATCH: match_states idx0 st_src0 st_tgt0 sm0) (CALLSRC: ms_src.(ModSem.is_call) st_src0), <>. - Hypothesis ATFSIM: forall sm_init idx0 st_src0 st_tgt0 sm0 args_src + Hypothesis ATFSIM: forall idx0 st_src0 st_tgt0 sm0 args_src (SIMSKENV: ModSemPair.sim_skenv msp sm0) - (MATCH: match_states sm_init idx0 st_src0 st_tgt0 sm0) + (MATCH: match_states idx0 st_src0 st_tgt0 sm0) (CALLSRC: ms_src.(ModSem.at_external) st_src0 args_src) (SOUND: forall si, exists su0 m_init, (sound_states si) su0 m_init st_src0), exists args_tgt sm_arg, @@ -88,9 +85,9 @@ Section MATCHSIMFORWARD. (<>) /\ (<>). - Hypothesis AFTERFSIM: forall sm_init idx0 st_src0 st_tgt0 sm0 sm_arg sm_ret retv_src retv_tgt st_src1 + Hypothesis AFTERFSIM: forall idx0 st_src0 st_tgt0 sm0 sm_arg sm_ret retv_src retv_tgt st_src1 (SIMSKENV: ModSemPair.sim_skenv msp sm0) - (MATCH: match_states sm_init idx0 st_src0 st_tgt0 sm0) + (MATCH: match_states idx0 st_src0 st_tgt0 sm0) (MLE: SimMem.le sm0 sm_arg) (* (MWF: SimMem.wf sm_arg) *) (MLE: SimMem.le (SimMemLift.lift sm_arg) sm_ret) @@ -100,7 +97,7 @@ Section MATCHSIMFORWARD. (SOUND: forall si, exists su0 m_init, (sound_states si) su0 m_init st_src0) (* history *) - (HISTORY: match_states_at_helper sm_init idx0 st_src0 st_tgt0 sm0 sm_arg) + (HISTORY: match_states_at_helper idx0 st_src0 st_tgt0 sm0 sm_arg) (* just helpers *) (MWFAFTR: SimMem.wf (SimMemLift.unlift sm_arg sm_ret)) @@ -109,12 +106,11 @@ Section MATCHSIMFORWARD. (<>) /\ forall (MLE: SimMem.le sm0 sm_after) (* helper *), ((<>) /\ - (<>)). + (<>)). - Hypothesis FINALFSIM: forall sm_init idx0 st_src0 st_tgt0 sm0 retv_src + Hypothesis FINALFSIM: forall idx0 st_src0 st_tgt0 sm0 retv_src (SIMSKENV: ModSemPair.sim_skenv msp sm0) - (MFUTURE: SimMem.le sm_init sm0) - (MATCH: match_states sm_init idx0 st_src0 st_tgt0 sm0) + (MATCH: match_states idx0 st_src0 st_tgt0 sm0) (FINALSRC: ms_src.(ModSem.final_frame) st_src0 retv_src), exists sm_ret retv_tgt, (<>) /\ @@ -122,11 +118,11 @@ Section MATCHSIMFORWARD. (<>) /\ (<>). - Let STEPFSIM := forall sm_init idx0 st_src0 st_tgt0 sm0 + Let STEPFSIM := forall idx0 st_src0 st_tgt0 sm0 (SIMSKENV: ModSemPair.sim_skenv msp sm0) (NOTCALL: ~ ModSem.is_call ms_src st_src0) (NOTRET: ~ ModSem.is_return ms_src st_src0) - (MATCH: match_states sm_init idx0 st_src0 st_tgt0 sm0) + (MATCH: match_states idx0 st_src0 st_tgt0 sm0) (SOUND: forall si, exists su0 m_init, (sound_states si) su0 m_init st_src0), (<>) /\ (<>) /\ (<>) (* Note: We require le for mle_preserves_sim_ge, but we cannot require SimMem.wf, beacuse of DCEproof *) - /\ (<>)>>). + /\ (<>)>>). - Let STEPBSIM := forall sm_init idx0 st_src0 st_tgt0 sm0 + Let STEPBSIM := forall idx0 st_src0 st_tgt0 sm0 (SIMSKENV: ModSemPair.sim_skenv msp sm0) (NOTCALL: ~ ModSem.is_call ms_src st_src0) (NOTRET: ~ ModSem.is_return ms_src st_src0) - (MATCH: match_states sm_init idx0 st_src0 st_tgt0 sm0) + (MATCH: match_states idx0 st_src0 st_tgt0 sm0) (SOUND: forall si, exists su0 m_init, (sound_states si) su0 m_init st_src0), (< ModSem.is_step ms_tgt st_tgt0>>) /\ (<>) /\ (<>) (* Note: We require le for mle_preserves_sim_ge, but we cannot require SimMem.wf, beacuse of DCEproof *) - /\ (<>)>>). + /\ (<>)>>). Hypothesis STEPSIM: STEPFSIM \/ STEPBSIM. @@ -164,11 +160,11 @@ Section MATCHSIMFORWARD. (MLE: SimMem.le sm_init sm0) (* (MWF: SimMem.wf sm0) *) (* (MCOMPAT: mem_compat st_src0 st_tgt0 sm0) *) - (MATCH: match_states sm_init i0 st_src0 st_tgt0 sm0): + (MATCH: match_states i0 st_src0 st_tgt0 sm0): (* su0 *) (* <> *) < forall si, exists su0 m_init, sound_states si su0 m_init st) - sm_init i0.(Ord.lift_idx WFORD) st_src0 st_tgt0 sm0>>. + i0.(Ord.lift_idx WFORD) st_src0 st_tgt0 sm0>>. Proof. (* move su0 at top. *) revert_until BAR. pcofix CIH. i. pfold. ii. @@ -192,12 +188,11 @@ Section MATCHSIMFORWARD. { eapply ModSemPair.mfuture_preserves_sim_skenv; try apply SIMSKENV; eauto. apply rtc_once. left. et. } - { etrans; eauto. } } generalize (classic (ModSem.is_return ms_src st_src0)). intro RETSRC; des. { (* RETURN *) u in RETSRC. des. exploit FINALFSIM; eauto. i; des. ii. - eapply lxsim_final; try apply SIMRET; eauto. etrans; eauto. + eapply lxsim_final; try apply SIMRET; eauto. } destruct STEPSIM as [STEPFSIM0|STEPBSIM0]. { eapply lxsim_step_forward; eauto. i. @@ -208,7 +203,6 @@ Section MATCHSIMFORWARD. + right. esplits; eauto. eapply Ord.lift_idx_spec; eauto. - right. eapply CIH; eauto. { eapply ModSemPair.mfuture_preserves_sim_skenv; try apply SIMSKENV; eauto. apply rtc_once; eauto. } - { etransitivity; eauto. } } { rr in STEPBSIM0. eapply lxsim_step_backward; eauto. i. exploit STEPBSIM0; eauto. { ii. eapply SUSTAR; eauto. eapply star_refl. } i; des. rr in PROGRESS. des. @@ -218,7 +212,6 @@ Section MATCHSIMFORWARD. + right. esplits; eauto. eapply Ord.lift_idx_spec; eauto. - right. eapply CIH; eauto. { eapply ModSemPair.mfuture_preserves_sim_skenv; try apply SIMSKENV; eauto. apply rtc_once; eauto. } - { etransitivity; eauto. } } Qed. diff --git a/proof/MatchSimModSemSR.v b/proof/MatchSimModSemSR.v index 33ff4442..8654f0aa 100644 --- a/proof/MatchSimModSemSR.v +++ b/proof/MatchSimModSemSR.v @@ -26,7 +26,6 @@ Section MATCHSIMFORWARD. Hypothesis PRSV: local_preservation ms_src sound_state. Variable match_states: forall - (sm_arg: SimMem.t) (idx: index) (st_src0: ms_src.(ModSem.state)) (st_tgt0: ms_tgt.(ModSem.state)) (sm0: SimMem.t), Prop. @@ -35,10 +34,9 @@ Section MATCHSIMFORWARD. Prop. Inductive match_states_at_helper - (sm_init: SimMem.t) (idx_at: index) (st_src0: ms_src.(ModSem.state)) (st_tgt0: ms_tgt.(ModSem.state)) (sm_at sm_arg: SimMem.t): Prop := | match_states_at_intro - (MATCH: match_states sm_init idx_at st_src0 st_tgt0 sm_at) + (MATCH: match_states idx_at st_src0 st_tgt0 sm_at) args_src args_tgt (CALLSRC: ms_src.(ModSem.at_external) st_src0 args_src) (CALLTGT: ms_tgt.(ModSem.at_external) st_tgt0 args_tgt) @@ -56,7 +54,7 @@ Section MATCHSIMFORWARD. exists st_init_src sm_init idx_init, (<>) /\ (<>) /\ - (<>). + (<>). Hypothesis INITPROGRESS: forall sm_arg args_src args_tgt (SIMSKENV: ModSemPair.sim_skenv msp sm_arg) @@ -65,14 +63,14 @@ Section MATCHSIMFORWARD. (SAFESRC: exists st_init_src, ms_src.(ModSem.initial_frame) args_src st_init_src), exists st_init_tgt, (<>). - Hypothesis ATMWF: forall sm_init idx0 st_src0 st_tgt0 sm0 - (MATCH: match_states sm_init idx0 st_src0 st_tgt0 sm0) + Hypothesis ATMWF: forall idx0 st_src0 st_tgt0 sm0 + (MATCH: match_states idx0 st_src0 st_tgt0 sm0) (CALLSRC: ms_src.(ModSem.is_call) st_src0), <>. - Hypothesis ATFSIM: forall sm_init idx0 st_src0 st_tgt0 sm0 args_src + Hypothesis ATFSIM: forall idx0 st_src0 st_tgt0 sm0 args_src (SIMSKENV: ModSemPair.sim_skenv msp sm0) - (MATCH: match_states sm_init idx0 st_src0 st_tgt0 sm0) + (MATCH: match_states idx0 st_src0 st_tgt0 sm0) (CALLSRC: ms_src.(ModSem.at_external) st_src0 args_src) (SOUND: exists su0 m_init, sound_state su0 m_init st_src0), exists args_tgt sm_arg, @@ -82,9 +80,9 @@ Section MATCHSIMFORWARD. (<>) /\ (<>). - Hypothesis AFTERFSIM: forall sm_init idx0 st_src0 st_tgt0 sm0 sm_arg sm_ret retv_src retv_tgt st_src1 + Hypothesis AFTERFSIM: forall idx0 st_src0 st_tgt0 sm0 sm_arg sm_ret retv_src retv_tgt st_src1 (SIMSKENV: ModSemPair.sim_skenv msp sm0) - (MATCH: match_states sm_init idx0 st_src0 st_tgt0 sm0) + (MATCH: match_states idx0 st_src0 st_tgt0 sm0) (MLE: SimMem.le sm0 sm_arg) (* (MWF: SimMem.wf sm_arg) *) (MLE: SimMem.lepriv sm_arg sm_ret) @@ -94,20 +92,20 @@ Section MATCHSIMFORWARD. (SOUND: exists su0 m_init, sound_state su0 m_init st_src0) (* history *) - (HISTORY: match_states_at_helper sm_init idx0 st_src0 st_tgt0 sm0 sm_arg), + (HISTORY: match_states_at_helper idx0 st_src0 st_tgt0 sm0 sm_arg), (* just helpers *) (* (MWFAFTR: SimMem.wf (SimMem.unlift sm_arg sm_ret)) *) (* (MLEAFTR: SimMem.le sm_arg (SimMem.unlift sm_arg sm_ret)) *) exists sm_after idx1 st_tgt1, (<>) /\ - (<>) /\ + (<>) /\ (<>) /\ (<>). - Hypothesis FINALFSIM: forall sm_init idx0 st_src0 st_tgt0 sm0 retv_src + Hypothesis FINALFSIM: forall idx0 st_src0 st_tgt0 sm0 retv_src (SIMSKENV: ModSemPair.sim_skenv msp sm0) - (MATCH: match_states sm_init idx0 st_src0 st_tgt0 sm0) + (MATCH: match_states idx0 st_src0 st_tgt0 sm0) (FINALSRC: ms_src.(ModSem.final_frame) st_src0 retv_src), exists sm_ret retv_tgt, (<>) /\ @@ -115,11 +113,11 @@ Section MATCHSIMFORWARD. (<>) /\ (<>). - Let STEPFSIM := forall sm_init idx0 st_src0 st_tgt0 sm0 + Let STEPFSIM := forall idx0 st_src0 st_tgt0 sm0 (SIMSKENV: ModSemPair.sim_skenv msp sm0) (NOTCALL: ~ ModSem.is_call ms_src st_src0) (NOTRET: ~ ModSem.is_return ms_src st_src0) - (MATCH: match_states sm_init idx0 st_src0 st_tgt0 sm0) + (MATCH: match_states idx0 st_src0 st_tgt0 sm0) (SOUND: exists su0 m_init, sound_state su0 m_init st_src0), (<>) /\ (<>) /\ (<>) (* Note: We require le for mle_preserves_sim_ge, but we cannot require SimMem.wf, beacuse of DCEproof *) - /\ (<>)>>). + /\ (<>)>>). - Let STEPBSIM := forall sm_init idx0 st_src0 st_tgt0 sm0 + Let STEPBSIM := forall idx0 st_src0 st_tgt0 sm0 (SIMSKENV: ModSemPair.sim_skenv msp sm0) (NOTCALL: ~ ModSem.is_call ms_src st_src0) (NOTRET: ~ ModSem.is_return ms_src st_src0) - (MATCH: match_states sm_init idx0 st_src0 st_tgt0 sm0) + (MATCH: match_states idx0 st_src0 st_tgt0 sm0) (SOUND: exists su0 m_init, sound_state su0 m_init st_src0), (* (< ModSem.is_step ms_tgt st_tgt0>>) *) (< ModSem.is_step ms_tgt st_tgt0>>) /\ @@ -146,7 +144,7 @@ Section MATCHSIMFORWARD. <>) /\ (<>) (* Note: We require le for mle_preserves_sim_ge, but we cannot require SimMem.wf, beacuse of DCEproof *) - /\ (<>)>>). + /\ (<>)>>). Remark safe_modsem_is_smaller st_src0 @@ -161,16 +159,15 @@ Section MATCHSIMFORWARD. Hypothesis BAR: bar_True. Lemma match_states_lxsimSR - sm_init i0 st_src0 st_tgt0 sm0 + i0 st_src0 st_tgt0 sm0 (SIMSKENV: ModSemPair.sim_skenv msp sm0) - (MLE: SimMem.le sm_init sm0) (* (MWF: SimMem.wf sm0) *) (* (MCOMPAT: mem_compat st_src0 st_tgt0 sm0) *) - (MATCH: match_states sm_init i0 st_src0 st_tgt0 sm0): + (MATCH: match_states i0 st_src0 st_tgt0 sm0): (* su0 *) (* <> *) < unit -> exists su0 m_init, sound_state su0 m_init st) - sm_init i0.(Ord.lift_idx WFORD) st_src0 st_tgt0 sm0>>. + i0.(Ord.lift_idx WFORD) st_src0 st_tgt0 sm0>>. Proof. (* move su0 at top. *) revert_until BAR. pcofix CIH. i. pfold. ii. @@ -186,14 +183,13 @@ Section MATCHSIMFORWARD. i; des. assert(MLE4: SimMem.le sm0 sm_after). { etrans; cycle 1. { et. } refl. } - esplits; eauto. right. eapply CIH; eauto. + esplits; eauto. right. eapply CIH; [..|eauto]. { eapply ModSemPair.mfuture_preserves_sim_skenv; try apply SIMSKENV; eauto. apply rtc_once. left. et. } - { etransitivity; eauto. } } generalize (classic (ModSem.is_return ms_src st_src0)). intro RETSRC; des. { (* RETURN *) u in RETSRC. des. exploit FINALFSIM; eauto. i; des. - eapply lxsimSR_final; try apply SIMRET; eauto. etrans; eauto. + eapply lxsimSR_final; try apply SIMRET; eauto. } destruct STEPSIM as [STEPFSIM0|STEPBSIM0]. { eapply lxsimSR_step_forward; eauto. i. @@ -204,9 +200,8 @@ Section MATCHSIMFORWARD. - des. + left. eauto. + right. esplits; eauto. eapply Ord.lift_idx_spec; eauto. - - right. eapply CIH; eauto. + - right. eapply CIH; [..|eauto]. { eapply ModSemPair.mfuture_preserves_sim_skenv; try apply SIMSKENV; eauto. apply rtc_once; eauto. } - { etransitivity; eauto. } } { rr in STEPBSIM0. eapply lxsimSR_step_backward; eauto. i. (* hexploit1 SU0; ss. *) @@ -215,9 +210,8 @@ Section MATCHSIMFORWARD. - des. + left. eauto. + right. esplits; eauto. eapply Ord.lift_idx_spec; eauto. - - right. eapply CIH; eauto. + - right. eapply CIH; [..|eauto]. { eapply ModSemPair.mfuture_preserves_sim_skenv; try apply SIMSKENV; eauto. apply rtc_once; eauto. } - { etransitivity; eauto. } } Qed. diff --git a/proof/SimModSem.v b/proof/SimModSem.v index 80b4b9f3..bc5cb36d 100644 --- a/proof/SimModSem.v +++ b/proof/SimModSem.v @@ -61,19 +61,17 @@ Section SIMMODSEM. (BSIM: bsim i1 st_src1 st_tgt0 sm1). - Inductive _lxsim_pre (lxsim: SimMem.t -> - idx -> state ms_src -> state ms_tgt -> SimMem.t -> Prop) - (sm_init: SimMem.t) + Inductive _lxsim_pre (lxsim: 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 := | lxsim_step_forward (SU: forall (SU: DUMMY_PROP), - <>) + <>) | lxsim_step_backward (SU: forall (SU: DUMMY_PROP), (<>)>>) /\ + (<>)>>) /\ (<>)>>)) @@ -97,25 +95,25 @@ Section SIMMODSEM. exists st_tgt1 sm_after i1, (<>) /\ (<>) /\ - (<>)>>))>>) + (<>)>>))>>) | lxsim_final sm_ret retv_src retv_tgt - (MLE: SimMem.le sm_init sm_ret) + (MLE: SimMem.le sm0 sm_ret) (MWF: SimMem.wf sm_ret) (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). - Definition _lxsim (lxsim: SimMem.t -> idx -> state ms_src -> state ms_tgt -> SimMem.t -> Prop) (sm_init: SimMem.t) + Definition _lxsim (lxsim: 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 := (forall (SUSTAR: forall st_src1 tr (STAR: Star ms_src st_src0 tr st_src1), sound_states st_src1), - <>). + <>). - Definition lxsim: _ -> _ -> _ -> _ -> _ -> Prop := paco5 _lxsim bot5. + Definition lxsim: _ -> _ -> _ -> _ -> Prop := paco4 _lxsim bot4. - Lemma lxsim_mon: monotone5 _lxsim. + Lemma lxsim_mon: monotone4 _lxsim. Proof. repeat intro. rr in IN. hexploit1 IN; eauto. inv IN; eauto. - econs 1; ss. ii. spc SU. des. esplits; eauto. inv SU. @@ -187,7 +185,7 @@ Context {SM: SimMem.class} {SS: SimSymb.class SM} {SU: Sound.class}. (<>) /\ (<>) /\ (< forall si, exists su m_init, sound_states si su m_init st) - sm_arg idx_init st_init_src st_init_tgt sm_init>>)>>) /\ + idx_init st_init_src st_init_tgt sm_init>>)>>) /\ (<>)>>)). @@ -214,18 +212,17 @@ Section FACTORTARGET. Section LXSIM. Variable sound_states: state ms_src -> Prop. - Variable sm_arg: SimMem.t. Inductive fbs_match: idx -> state ms_src -> (trace * state ms_tgt) -> SimMem.t -> Prop := | fbs_match_intro idx0 st_src0 tr st_src1 st_tgt0 sm0 (STAR: (st_src0 = st_src1 /\ tr = E0) \/ ((Plus ms_src st_src0 tr st_src1) /\ output_trace tr /\ tr <> [])) - (MATCH: lxsim ms_src ms_tgt sound_states sm_arg idx0 st_src1 st_tgt0 sm0): + (MATCH: lxsim ms_src ms_tgt sound_states idx0 st_src1 st_tgt0 sm0): fbs_match idx0 st_src0 (tr, st_tgt0) sm0. Lemma factor_lxsim_target: forall idx0 st_src0 tr st_tgt0 sm0 (SIM: fbs_match idx0 st_src0 (tr, st_tgt0) sm0), - <>. + <>. Proof. clear_tac. unfold NW. pcofix CIH. i. pfold. inv SIM. punfold MATCH. des; clarify; cycle 1. diff --git a/proof/SimModSemLift.v b/proof/SimModSemLift.v index 4d8ac2cc..bbe3cb7c 100644 --- a/proof/SimModSemLift.v +++ b/proof/SimModSemLift.v @@ -72,13 +72,11 @@ Section SIMMODSEM. (MLE: SimMem.le sm0 sm1) (BSIM: bsim i1 st_src1 st_tgt0 sm1). - Inductive _lxsim_pre (lxsim: SimMem.t -> - idx -> state ms_src -> state ms_tgt -> SimMem.t -> Prop) - (sm_init: SimMem.t) + Inductive _lxsim_pre (lxsim: 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 := | lxsim_step_forward (SU: forall (SU: DUMMY_PROP), - <> + <> (* 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 *)) @@ -87,7 +85,7 @@ Section SIMMODSEM. (SU: forall (SU: DUMMY_PROP), (<>)>>) /\ + (<>)>>) /\ (<>)>>)) @@ -123,11 +121,11 @@ Section SIMMODSEM. (<>) /\ (* (<>) /\ *) (<>) /\ - (<>)>>))>>) + (<>)>>))>>) | lxsim_final sm_ret retv_src retv_tgt - (MLE: SimMem.le sm_init sm_ret) + (MLE: SimMem.le sm0 sm_ret) (MWF: SimMem.wf sm_ret) (* (PROGRESS: ms_tgt.(is_return) rs_init_tgt st_tgt0) *) (* (RETBSIM: forall *) @@ -147,14 +145,14 @@ Section SIMMODSEM. (* (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) + Definition _lxsim (lxsim: 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 := (forall (SUSTAR: forall st_src1 tr (STAR: Star ms_src st_src0 tr st_src1), sound_states st_src1), - <>). + <>). - Definition lxsimL: _ -> _ -> _ -> _ -> _ -> Prop := paco5 _lxsim bot5. + Definition lxsimL: _ -> _ -> _ -> _ -> Prop := paco4 _lxsim bot4. - Lemma lxsim_mon: monotone5 _lxsim. + Lemma lxsim_mon: monotone4 _lxsim. Proof. repeat intro. rr in IN. hexploit1 IN; eauto. inv IN; eauto. - econs 1; ss. ii. spc SU. des. esplits; eauto. inv SU. @@ -215,7 +213,7 @@ Context {SMLIFT: SimMemLift.class SM}. (<>) /\ (< forall si, exists su m_init, sound_states si su m_init st) - has_footprint mle_excl sm_arg idx_init st_init_src st_init_tgt sm_init>>)>>) /\ + has_footprint mle_excl idx_init st_init_src st_init_tgt sm_init>>)>>) /\ (<>)>>)). @@ -235,7 +233,7 @@ Section IMPLIES. Context {SMLIFT: SimMemLift.class SM}. Lemma lxsim_lxsim - ms_src ms_tgt sound_state sm_arg idx_init st_init_src st_init_tgt sm_init + ms_src ms_tgt sound_state idx_init st_init_src st_init_tgt sm_init (has_footprint: ms_src.(ModSem.state) -> ms_tgt.(ModSem.state) -> SimMem.t -> Prop) (mle_excl: ms_src.(ModSem.state) -> ms_tgt.(ModSem.state) -> SimMem.t -> SimMem.t -> Prop) (FOOTEXCL: forall st_at_src st_at_tgt sm0 sm1 sm2 @@ -244,8 +242,8 @@ Section IMPLIES. (MLEEXCL: (mle_excl st_at_src st_at_tgt) sm1 sm2) (MLE: SimMem.le sm0 sm1), <>) - (SIM: lxsimL ms_src ms_tgt sound_state has_footprint mle_excl sm_arg idx_init st_init_src st_init_tgt sm_init): - <>. + (SIM: lxsimL ms_src ms_tgt sound_state has_footprint mle_excl idx_init st_init_src st_init_tgt sm_init): + <>. Proof. move has_footprint at top. move mle_excl at top. move FOOTEXCL at top. revert_until sound_state. pcofix CIH. i. pfold. @@ -258,7 +256,7 @@ Section IMPLIES. + pclearbot. econs 2; eauto. - econs 3; et. ii. exploit SU0; et. i; des. - eexists. exists (SimMemLift.lift sm_arg0). + eexists. exists (SimMemLift.lift sm_arg). esplits; eauto. { eapply SimMemLift.lift_args; et. } { eapply SimMemLift.lift_wf; et. } diff --git a/proof/SimModSemSR.v b/proof/SimModSemSR.v index 3bbb3d15..f4c59cee 100644 --- a/proof/SimModSemSR.v +++ b/proof/SimModSemSR.v @@ -70,16 +70,14 @@ Section SIMMODSEM. (MLE: SimMem.le sm0 sm1) (BSIM: bsim i1 st_src1 st_tgt0 sm1). - Inductive _lxsimSR_pre (lxsimSR: SimMem.t -> - idx -> state ms_src -> state ms_tgt -> SimMem.t -> Prop) - (sm_init: SimMem.t) + Inductive _lxsimSR_pre (lxsimSR: 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 := | lxsimSR_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 *)) @@ -91,7 +89,7 @@ Section SIMMODSEM. (* (<>) /\ *) (<>)>>) /\ + (<>)>>) /\ (<>) /\ (<>) /\ - (<>)>>))>>) + (<>)>>))>>) | lxsimSR_final sm_ret retv_src retv_tgt - (MLE: SimMem.le sm_init sm_ret) + (MLE: SimMem.le sm0 sm_ret) (MWF: SimMem.wf sm_ret) (* (PROGRESS: ms_tgt.(is_return) rs_init_tgt st_tgt0) *) (* (RETBSIM: forall *) @@ -171,14 +169,14 @@ Section SIMMODSEM. (* (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 _lxsimSR (lxsimSR: SimMem.t -> idx -> state ms_src -> state ms_tgt -> SimMem.t -> Prop) (sm_init: SimMem.t) + Definition _lxsimSR (lxsimSR: 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 := (forall (SUSTAR: forall st_src1 tr (STAR: Star ms_src st_src0 tr st_src1), sound_states st_src1), - <>). + <>). - Definition lxsimSR: _ -> _ -> _ -> _ -> _ -> Prop := paco5 _lxsimSR bot5. + Definition lxsimSR: _ -> _ -> _ -> _ -> Prop := paco4 _lxsimSR bot4. - Lemma lxsimSR_mon: monotone5 _lxsimSR. + Lemma lxsimSR_mon: monotone4 _lxsimSR. Proof. repeat intro. rr in IN. hexploit1 IN; eauto. inv IN; eauto. - econs 1; ss. ii. spc SU. des. inv SU. @@ -230,7 +228,7 @@ Context {SM: SimMem.class} {SS: SimSymb.class SM} {SU: Sound.class}. (<>) /\ (<>) /\ (< forall si, exists su m_init, (sound_states si) su m_init st) - sm_arg idx_init st_init_src st_init_tgt sm_init>>)>>) /\ + idx_init st_init_src st_init_tgt sm_init>>)>>) /\ (< Prop. - Variable sm_arg: SimMem.t. Inductive ffs_match: idx -> (trace * state ms_src) -> state ms_tgt -> SimMem.t -> Prop := | ffs_match_at idx0 st_src0 st_tgt0 sm0 - (MATCH: lxsimSR ms_src ms_tgt sound_states sm_arg idx0 st_src0 st_tgt0 sm0): + (MATCH: lxsimSR ms_src ms_tgt sound_states idx0 st_src0 st_tgt0 sm0): ffs_match idx0 ([], st_src0) st_tgt0 sm0 | ffs_match_buffer idx0 st_src0 ev tr st_tgt0 st_tgt1 sm0 (* (SSR: strongly_receptive_at ms_src st_src0) *) (PLUS: DPlus ms_tgt st_tgt0 (ev :: tr) st_tgt1) - (MATCH: lxsimSR ms_src ms_tgt sound_states sm_arg idx0 st_src0 st_tgt1 sm0): + (MATCH: lxsimSR ms_src ms_tgt sound_states idx0 st_src0 st_tgt1 sm0): ffs_match idx0 (ev :: tr, st_src0) st_tgt0 sm0. Lemma factor_lxsim_source: forall idx0 st_src0 tr st_tgt0 sm0 (SIM: ffs_match idx0 (tr, st_src0) st_tgt0 sm0), - < sound_states st.(snd)) sm_arg idx0 (tr, st_src0) st_tgt0 sm0>>. + < sound_states st.(snd)) idx0 (tr, st_src0) st_tgt0 sm0>>. Proof. clear_tac. unfold NW. pcofix CIH. i. pfold. inv SIM; cycle 1. (* exploit atomic_receptive; eauto. intro RECEP. *) diff --git a/selfsim/ClightStepExt.v b/selfsim/ClightStepExt.v index c618ac07..65dd8741 100644 --- a/selfsim/ClightStepExt.v +++ b/selfsim/ClightStepExt.v @@ -25,7 +25,7 @@ Set Implicit Arguments. Local Opaque Z.mul Z.add Z.sub Z.div. -Inductive match_states_ext_clight (sm_arg: SimMemExt.t') +Inductive match_states_ext_clight : unit -> state -> state -> SimMemExt.t' -> Prop := | match_ext_State fn stmt K_src K_tgt env_src env_tgt tenv_src tenv_tgt m_src m_tgt sm0 @@ -36,7 +36,7 @@ Inductive match_states_ext_clight (sm_arg: SimMemExt.t') (TENV: match_temp_env inject_id tenv_src tenv_tgt) (CONT: match_cont inject_id K_src K_tgt): match_states_ext_clight - sm_arg tt + tt (State fn stmt K_src env_src tenv_src m_src) (State fn stmt K_tgt env_tgt tenv_tgt m_tgt) sm0 @@ -49,7 +49,7 @@ Inductive match_states_ext_clight (sm_arg: SimMemExt.t') (VALS: Val.lessdef_list args_src args_tgt) (CONT: match_cont inject_id K_src K_tgt): match_states_ext_clight - sm_arg tt + tt (Callstate fptr_src ty args_src K_src m_src) (Callstate fptr_tgt ty args_tgt K_tgt m_tgt) sm0 @@ -61,7 +61,7 @@ Inductive match_states_ext_clight (sm_arg: SimMemExt.t') (INJ: Val.lessdef retv_src retv_tgt) (CONT: match_cont inject_id K_src K_tgt): match_states_ext_clight - sm_arg tt + tt (Returnstate retv_src K_src m_src) (Returnstate retv_tgt K_tgt m_tgt) sm0. @@ -342,12 +342,12 @@ Section CLIGHTEXT. Qed. Lemma clight_step_preserve_extension - sm_arg u st_src0 st_tgt0 st_src1 sm0 tr - (MATCH: match_states_ext_clight sm_arg u st_src0 st_tgt0 sm0) + u st_src0 st_tgt0 st_src1 sm0 tr + (MATCH: match_states_ext_clight u st_src0 st_tgt0 sm0) (STEP: step se ge (function_entry ge) st_src0 tr st_src1): exists st_tgt1 sm1, (<>) /\ - (<>). + (<>). Proof. inv STEP; inv MATCH; try (by inv CONT; esplits; do 3 (econs; eauto)). - exploit eval_expr_extends; eauto. i. des. diff --git a/selfsim/ClightStepInj.v b/selfsim/ClightStepInj.v index f53888a1..771582c9 100644 --- a/selfsim/ClightStepInj.v +++ b/selfsim/ClightStepInj.v @@ -106,7 +106,7 @@ Inductive match_states_clight_internal: (Returnstate retv_tgt K_tgt m_tgt) j m_src m_tgt. -Inductive match_states_clight (sm_arg: SimMemInj.t') +Inductive match_states_clight : unit -> state -> state -> SimMemInj.t' -> Prop := | match_states_clight_intro st_src st_tgt j m_src m_tgt sm0 @@ -115,7 +115,7 @@ Inductive match_states_clight (sm_arg: SimMemInj.t') (MWFINJ: j = sm0.(SimMemInj.inj)) (MATCHST: match_states_clight_internal st_src st_tgt j m_src m_tgt) (MWF: SimMemInj.wf' sm0): - match_states_clight sm_arg tt st_src st_tgt sm0. + match_states_clight tt st_src st_tgt sm0. Section CLIGHTINJ. @@ -574,14 +574,14 @@ Section CLIGHTINJ. Qed. Lemma clight_step_preserve_injection - sm_arg u st_src0 st_tgt0 st_src1 sm0 tr + u st_src0 st_tgt0 st_src1 sm0 tr (SYMBOLS: symbols_inject (SimMemInj.inj sm0) se_src se_tgt) (GENV: meminj_match_globals eq ge_src ge_tgt (SimMemInj.inj sm0)) - (MATCH: match_states_clight sm_arg u st_src0 st_tgt0 sm0) + (MATCH: match_states_clight u st_src0 st_tgt0 sm0) (STEP: step se_src ge_src (function_entry ge_src) st_src0 tr st_src1): exists st_tgt1 sm1, (<>) /\ - (<>) /\ + (<>) /\ (<>). Proof. inv STEP; inv MATCH; inv MATCHST; try (by inv CONT; esplits; try refl; do 3 (econs; eauto)). @@ -697,7 +697,7 @@ Section CLIGHTINJ. assert (SYMBINJ: symbols_inject (SimMemInj.inj sm) se_src se_tgt) by eauto. exploit clight_step_preserve_injection; eauto; ss. - econs; eauto. econs; ss; eauto; try refl; try xomega. - - instantiate (1:=sm). i. des. destruct sm1. + - i. des. destruct sm1. inv MATCH0. inv MLE. inv MWF. ss. esplits; eauto; try (eapply Mem.unchanged_on_implies; eauto; ii; ss). + inv FROZEN. ii. exploit NEW_IMPLIES_OUTSIDE; eauto. i. des. unfold Mem.valid_block. clear - OUTSIDE_SRC OUTSIDE_TGT. xomega. diff --git a/selfsim/IdSimAsm.v b/selfsim/IdSimAsm.v index 595c2b2b..863d3ecf 100644 --- a/selfsim/IdSimAsm.v +++ b/selfsim/IdSimAsm.v @@ -1246,7 +1246,6 @@ Qed. Inductive match_states (skenv_link_tgt: SkEnv.t) (ge_src ge_tgt: genv) - (sm_init : @SimMem.t SimMemInjC.SimMemInj) : nat-> AsmC.state -> AsmC.state -> (@SimMem.t SimMemInjC.SimMemInj) -> Prop := | match_states_intro j init_rs_src init_rs_tgt rs_src rs_tgt m_src m_tgt @@ -1267,7 +1266,7 @@ Inductive match_states (j blk_src = Some (blk_tgt, 0))): match_states skenv_link_tgt - ge_src ge_tgt sm_init 0 + ge_src ge_tgt 0 (AsmC.mkstate init_rs_src (Asm.State rs_src m_src)) (AsmC.mkstate init_rs_tgt (Asm.State rs_tgt m_tgt)) sm0. diff --git a/selfsim/IdSimAsmExtra.v b/selfsim/IdSimAsmExtra.v index 59e808da..1e8791dd 100644 --- a/selfsim/IdSimAsmExtra.v +++ b/selfsim/IdSimAsmExtra.v @@ -533,7 +533,6 @@ Inductive wf_init_rss: signature -> regset -> regset -> Prop := Inductive match_states_ext (skenv_link_tgt : SkEnv.t) (ge_src ge_tgt: genv) - (sm_init : @SimMem.t SimMemExt.SimMemExt) : unit -> AsmC.state -> AsmC.state -> (@SimMem.t SimMemExt.SimMemExt) -> Prop := | match_states_ext_intro init_rs_src init_rs_tgt rs_src rs_tgt m_src m_tgt @@ -550,7 +549,7 @@ Inductive match_states_ext (RAWF: Genv.find_funct skenv_link_tgt (init_rs_tgt RA) = None) : match_states_ext - skenv_link_tgt ge_src ge_tgt sm_init tt + skenv_link_tgt ge_src ge_tgt tt (AsmC.mkstate init_rs_src (Asm.State rs_src m_src)) (AsmC.mkstate init_rs_tgt (Asm.State rs_tgt m_tgt)) sm0. diff --git a/selfsim/IdSimExtra.v b/selfsim/IdSimExtra.v index 8d58771d..02865ae1 100644 --- a/selfsim/IdSimExtra.v +++ b/selfsim/IdSimExtra.v @@ -252,7 +252,7 @@ Proof. eapply MatchSimModSem.match_states_sim; ss. - apply unit_ord_wf. - eapply SoundTop.sound_state_local_preservation. - - instantiate (1:= fun sm_arg _ st_src st_tgt sm0 => + - instantiate (1:= fun _ st_src st_tgt sm0 => (<>) /\ (<>)). ss. i. inv SIMARGS; ss; esplits; eauto; try congruence; ss. diff --git a/x86/AsmgenproofC.v b/x86/AsmgenproofC.v index d0aced16..558312ee 100644 --- a/x86/AsmgenproofC.v +++ b/x86/AsmgenproofC.v @@ -84,7 +84,6 @@ Inductive stack_base (initial_parent_sp initial_parent_ra: val): list Mach.stack stack_base initial_parent_sp initial_parent_ra (fr::ls). Inductive match_states - (sm_init: SimMem.t) (idx: nat) (st_src0: MachC.state) (st_tgt0: AsmC.state) (sm0: SimMem.t): Prop := | match_states_intro