From 04667b444164f8a54c1aab0a8e2422e1951bf9bc Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 9 Dec 2020 09:47:24 +0100 Subject: proof for jumptable --- backend/CSE3proof.v | 28 +++++++++++++++++++++++++++- 1 file changed, 27 insertions(+), 1 deletion(-) (limited to 'backend') diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index 661329e8..cc4ab686 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -1074,7 +1074,33 @@ Proof. * rewrite subst_arg_ok with (sp:=sp) (m:=m) by trivial. assumption. + econstructor; eauto. - admit. + + (* 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. + rewrite forallb_forall in IND_step_me. + assert (RB.ge (invs # pc') (Some inv_pc)) as GE. + { + apply relb_leb_correct. + specialize IND_step_me with (pc', Some inv_pc). + apply IND_step_me. + apply (in_map (fun pc'0 : node => (pc'0, Some inv_pc))). + eapply list_nth_z_in. + eassumption. + } + destruct (invs # pc'); cbn in *. + 2: contradiction. + eapply rel_ge; eauto. + (* END INVARIANT *) - (* Ireturn *) destruct or as [arg | ]. -- cgit