diff options
Diffstat (limited to 'backend/CSE3proof.v')
| -rw-r--r-- | backend/CSE3proof.v | 435 |
1 files changed, 221 insertions, 214 deletions
diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index a601d5d5..86c2c8a7 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -582,48 +582,51 @@ Proof. apply oper_sound; unfold ctx; eauto with cse3. (* END INVARIANT *) - (* Iload *) - exists (State ts tf sp pc' (rs # dst <- v) m). split. - + pose (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload trap chunk addr args dst pc')) as instr'. - assert (instr' = (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload trap chunk addr args dst pc'))) by reflexivity. - unfold param_transf_instr, find_load_in_fmap in instr'. - destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC. - pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SLoad chunk addr) - (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) t) as FIND_SOUND. - * destruct rhs_find eqn:FIND. - ** apply exec_Iop with (op := Omove) (args := r :: nil). - TR_AT. - subst instr'. - congruence. - simpl. - specialize FIND_SOUND with (src := r) (rs := rs) (m := m). - simpl in FIND_SOUND. - rewrite subst_args_ok with (sp:=sp) (m:=m) in FIND_SOUND. - rewrite H0 in FIND_SOUND. (* ADDR *) - rewrite H1 in FIND_SOUND. (* LOAD *) - rewrite FIND_SOUND; auto. - unfold fmap_sem. - change ((fst (preanalysis tenv f)) # pc) - with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). - rewrite INV_PC. - assumption. - ** apply exec_Iload with (trap := trap) (chunk := chunk) (a := a) (addr := addr) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial. - TR_AT. - { subst instr'. - congruence. } - rewrite subst_args_ok with (sp:=sp) (m:=m). - { - rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved. - assumption. - } - unfold fmap_sem. - change ((fst (preanalysis tenv f)) # pc) - with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). - rewrite INV_PC. - assumption. - * apply exec_Iload with (chunk := chunk) (trap := trap) (addr := addr) (a := a) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial. + inv H0. + + exists (State ts tf sp pc' (rs # dst <- v) m). split. + * pose (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload trap chunk addr args dst pc')) as instr'. + assert (instr' = (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload trap chunk addr args dst pc'))) by reflexivity. + unfold param_transf_instr, find_load_in_fmap in instr'. + destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC. + pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SLoad chunk addr) + (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) t) as FIND_SOUND. + -- destruct rhs_find eqn:FIND. + ** apply exec_Iop with (op := Omove) (args := r :: nil). + TR_AT. + subst instr'. + congruence. + simpl. + specialize FIND_SOUND with (src := r) (rs := rs) (m := m). + simpl in FIND_SOUND. + rewrite subst_args_ok with (sp:=sp) (m:=m) in FIND_SOUND. + rewrite EVAL in FIND_SOUND. (* ADDR *) + rewrite LOAD in FIND_SOUND. (* LOAD *) + rewrite FIND_SOUND; auto. + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + ** apply exec_Iload with (trap := trap) (chunk := chunk) (addr := addr) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial. + TR_AT. + { subst instr'. + congruence. } + eapply has_loaded_normal; eauto. + rewrite subst_args_ok with (sp:=sp) (m:=m). + { + rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved. + assumption. + } + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + -- apply exec_Iload with (chunk := chunk) (trap := trap) (addr := addr) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial. TR_AT. { subst instr'. congruence. } + eapply has_loaded_normal; eauto. rewrite subst_args_ok with (sp:=sp) (m:=m). { rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved. @@ -634,183 +637,187 @@ Proof. with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). rewrite INV_PC. assumption. - + econstructor; eauto. - * eapply wt_exec_Iload with (f:=f); try eassumption. + * econstructor; eauto. + -- eapply wt_exec_Iload with (f:=f); try eassumption. eauto with wt. - * (* BEGIN INVARIANT *) - fold ctx. fold invs. - assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto). - unfold check_inductiveness in IND. - rewrite andb_true_iff in IND. - destruct IND as [IND_entry IND_step]. - rewrite PTree_Properties.for_all_correct in IND_step. - pose proof (IND_step pc _ H) as IND_step_me. - clear IND_entry IND_step. - destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL. - 2: contradiction. - cbn in IND_step_me. - destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *. - 2: discriminate. - rewrite andb_true_iff in IND_step_me. - destruct IND_step_me. - rewrite rel_leb_correct in *. - eapply rel_ge. - eassumption. - apply oper_sound; unfold ctx; eauto with cse3. - (* END INVARIANT *) - - - (* Iload notrap1 *) - exists (State ts tf sp pc' (rs # dst <- Vundef) m). split. - + pose (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc')) as instr'. - assert (instr' = (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc'))) by reflexivity. - unfold param_transf_instr, find_load_in_fmap in instr'. - destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC. - pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SLoad chunk addr) - (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) t) as FIND_SOUND. - * destruct rhs_find eqn:FIND. - ** apply exec_Iop with (op := Omove) (args := r :: nil). - TR_AT. - subst instr'. - congruence. - simpl. - specialize FIND_SOUND with (src := r) (rs := rs) (m := m). - simpl in FIND_SOUND. - rewrite subst_args_ok with (sp:=sp) (m:=m) in FIND_SOUND. - rewrite H0 in FIND_SOUND. (* ADDR *) - rewrite FIND_SOUND; auto. - unfold fmap_sem. - change ((fst (preanalysis tenv f)) # pc) - with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). - rewrite INV_PC. - assumption. - ** apply exec_Iload_notrap1 with (chunk := chunk) (addr := addr) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial. - TR_AT. - { subst instr'. - congruence. } - rewrite subst_args_ok with (sp:=sp) (m:=m). - { - rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved. - assumption. - } - unfold fmap_sem. - change ((fst (preanalysis tenv f)) # pc) - with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). - rewrite INV_PC. - assumption. - * apply exec_Iload_notrap1 with (chunk := chunk) (addr := addr) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial. - TR_AT. - { subst instr'. - congruence. } - rewrite subst_args_ok with (sp:=sp) (m:=m). - { - rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved. - assumption. - } - unfold fmap_sem. - change ((fst (preanalysis tenv f)) # pc) - with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). - rewrite INV_PC. - assumption. - + econstructor; eauto. - * apply wt_undef; assumption. - * (* BEGIN INVARIANT *) - fold ctx. fold invs. - assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto). - unfold check_inductiveness in IND. - rewrite andb_true_iff in IND. - destruct IND as [IND_entry IND_step]. - rewrite PTree_Properties.for_all_correct in IND_step. - pose proof (IND_step pc _ H) as IND_step_me. - clear IND_entry IND_step. - destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL. - 2: contradiction. - cbn in IND_step_me. - destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *. - 2: discriminate. - rewrite andb_true_iff in IND_step_me. - destruct IND_step_me. - rewrite rel_leb_correct in *. - eapply rel_ge. - eassumption. - apply oper_sound; unfold ctx; eauto with cse3. - (* END INVARIANT *) + -- (* BEGIN INVARIANT *) + fold ctx. fold invs. + assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto). + unfold check_inductiveness in IND. + rewrite andb_true_iff in IND. + destruct IND as [IND_entry IND_step]. + rewrite PTree_Properties.for_all_correct in IND_step. + pose proof (IND_step pc _ H) as IND_step_me. + clear IND_entry IND_step. + destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL. + 2: contradiction. + cbn in IND_step_me. + destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *. + 2: discriminate. + rewrite andb_true_iff in IND_step_me. + destruct IND_step_me. + rewrite rel_leb_correct in *. + eapply rel_ge. + eassumption. + apply oper_sound; unfold ctx; eauto with cse3. + (* END INVARIANT *) + + + destruct (eval_addressing) eqn:EVAL in LOAD. + * specialize (LOAD v). + exists (State ts tf sp pc' (rs # dst <- Vundef) m). split. + -- pose (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc')) as instr'. + assert (instr' = (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc'))) by reflexivity. + unfold param_transf_instr, find_load_in_fmap in instr'. + destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC. + pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SLoad chunk addr) + (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) t) as FIND_SOUND. + ++ destruct rhs_find eqn:FIND. + ** apply exec_Iop with (op := Omove) (args := r :: nil). + TR_AT. + subst instr'. + congruence. + simpl. + specialize FIND_SOUND with (src := r) (rs := rs) (m := m). + simpl in FIND_SOUND. + rewrite subst_args_ok with (sp:=sp) (m:=m) in FIND_SOUND. + rewrite EVAL in FIND_SOUND. (* ADDR *) + rewrite LOAD in FIND_SOUND; auto. (* LOAD *) + rewrite FIND_SOUND; auto. + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + ** apply exec_Iload with (trap := NOTRAP) (chunk := chunk) (addr := addr) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial. + TR_AT. + { subst instr'. + congruence. } + eapply has_loaded_default; eauto. + rewrite subst_args_ok with (sp:=sp) (m:=m). + { + rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved. + intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'. apply LOAD; auto. + } + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + ++ apply exec_Iload with (trap := NOTRAP) (chunk := chunk) (addr := addr) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial. + TR_AT. + { subst instr'. + congruence. } + eapply has_loaded_default; eauto. + rewrite subst_args_ok with (sp:=sp) (m:=m). + { + rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved. + intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'. apply LOAD; auto. + } + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + -- econstructor; eauto. + ++ apply wt_undef; assumption. + ++ (* BEGIN INVARIANT *) + fold ctx. fold invs. + assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto). + unfold check_inductiveness in IND. + rewrite andb_true_iff in IND. + destruct IND as [IND_entry IND_step]. + rewrite PTree_Properties.for_all_correct in IND_step. + pose proof (IND_step pc _ H) as IND_step_me. + clear IND_entry IND_step. + destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL. + 2: contradiction. + cbn in IND_step_me. + destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *. + 2: discriminate. + rewrite andb_true_iff in IND_step_me. + destruct IND_step_me. + rewrite rel_leb_correct in *. + eapply rel_ge. + eassumption. + apply oper_sound; unfold ctx; eauto with cse3. + (* END INVARIANT *) - - (* Iload notrap2 *) - exists (State ts tf sp pc' (rs # dst <- Vundef) m). split. - + pose (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc')) as instr'. - assert (instr' = (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc'))) by reflexivity. - unfold param_transf_instr, find_load_in_fmap in instr'. - destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC. - pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SLoad chunk addr) - (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) t) as FIND_SOUND. - * destruct rhs_find eqn:FIND. - ** apply exec_Iop with (op := Omove) (args := r :: nil). - TR_AT. - subst instr'. - congruence. - simpl. - specialize FIND_SOUND with (src := r) (rs := rs) (m := m). - simpl in FIND_SOUND. - rewrite subst_args_ok with (sp:=sp) (m:=m) in FIND_SOUND. - rewrite H0 in FIND_SOUND. (* ADDR *) - rewrite H1 in FIND_SOUND. (* LOAD *) - rewrite FIND_SOUND; auto. - unfold fmap_sem. - change ((fst (preanalysis tenv f)) # pc) - with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). - rewrite INV_PC. - assumption. - ** apply exec_Iload_notrap2 with (chunk := chunk) (a := a) (addr := addr) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial. - TR_AT. - { subst instr'. - congruence. } - rewrite subst_args_ok with (sp:=sp) (m:=m). - { - rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved. - assumption. - } - unfold fmap_sem. - change ((fst (preanalysis tenv f)) # pc) - with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). - rewrite INV_PC. - assumption. - * apply exec_Iload_notrap2 with (chunk := chunk) (addr := addr) (a := a) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial. - TR_AT. - { subst instr'. - congruence. } - rewrite subst_args_ok with (sp:=sp) (m:=m). - { - rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved. - assumption. - } - unfold fmap_sem. - change ((fst (preanalysis tenv f)) # pc) - with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). - rewrite INV_PC. - assumption. - + econstructor; eauto. - * apply wt_undef; assumption. - * (* BEGIN INVARIANT *) - fold ctx. fold invs. - assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto). - unfold check_inductiveness in IND. - rewrite andb_true_iff in IND. - destruct IND as [IND_entry IND_step]. - rewrite PTree_Properties.for_all_correct in IND_step. - pose proof (IND_step pc _ H) as IND_step_me. - clear IND_entry IND_step. - destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL. - 2: contradiction. - cbn in IND_step_me. - destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *. - 2: discriminate. - rewrite andb_true_iff in IND_step_me. - destruct IND_step_me. - rewrite rel_leb_correct in *. - eapply rel_ge. - eassumption. - apply oper_sound; unfold ctx; eauto with cse3. - (* END INVARIANT *) + * exists (State ts tf sp pc' (rs # dst <- Vundef) m). split. + -- pose (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc')) as instr'. + assert (instr' = (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc'))) by reflexivity. + unfold param_transf_instr, find_load_in_fmap in instr'. + destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC. + pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SLoad chunk addr) + (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) t) as FIND_SOUND. + ++ destruct rhs_find eqn:FIND. + ** apply exec_Iop with (op := Omove) (args := r :: nil). + TR_AT. + subst instr'. + congruence. + simpl. + specialize FIND_SOUND with (src := r) (rs := rs) (m := m). + simpl in FIND_SOUND. + rewrite subst_args_ok with (sp:=sp) (m:=m) in FIND_SOUND. + rewrite EVAL in FIND_SOUND. (* ADDR *) + rewrite FIND_SOUND; auto. + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + ** apply exec_Iload with (trap := NOTRAP) (chunk := chunk) (addr := addr) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial. + TR_AT. + { subst instr'. + congruence. } + eapply has_loaded_default; eauto. + rewrite subst_args_ok with (sp:=sp) (m:=m). + { + rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved. + intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'. + } + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + ++ apply exec_Iload with (trap := NOTRAP) (chunk := chunk) (addr := addr) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial. + TR_AT. + { subst instr'. + congruence. } + eapply has_loaded_default; eauto. + rewrite subst_args_ok with (sp:=sp) (m:=m). + { + rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved. + intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'. + } + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + -- econstructor; eauto. + ++ apply wt_undef; assumption. + ++ (* BEGIN INVARIANT *) + fold ctx. fold invs. + assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto). + unfold check_inductiveness in IND. + rewrite andb_true_iff in IND. + destruct IND as [IND_entry IND_step]. + rewrite PTree_Properties.for_all_correct in IND_step. + pose proof (IND_step pc _ H) as IND_step_me. + clear IND_entry IND_step. + destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL. + 2: contradiction. + cbn in IND_step_me. + destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *. + 2: discriminate. + rewrite andb_true_iff in IND_step_me. + destruct IND_step_me. + rewrite rel_leb_correct in *. + eapply rel_ge. + eassumption. + apply oper_sound; unfold ctx; eauto with cse3. + (* END INVARIANT *) - (* Istore *) exists (State ts tf sp pc' rs m'). split. |