From 8f2cf0b53b3a7fd4bc339fddf89197601eb549c2 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 9 Dec 2020 09:13:40 +0100 Subject: one 'admit' less --- backend/CSE3proof.v | 38 ++++++++++++++++++++++++++++++++++++-- 1 file changed, 36 insertions(+), 2 deletions(-) (limited to 'backend') diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index 69e779cd..661329e8 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -930,7 +930,7 @@ Proof. TR_AT. unfold transf_instr. fold invs. fold ctx. rewrite FIND_COND. reflexivity. * replace bfound with b. { econstructor; eauto. - (* BEGIN 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. @@ -1031,7 +1031,41 @@ Proof. eassumption. ** reflexivity. * 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 andb_true_iff in IND_step_me. + rewrite andb_true_iff in IND_step_me. + destruct IND_step_me as [IND_so [IND_not ZOT]]. + clear ZOT. + destruct (invs # ifso) as [inv_so | ] eqn:INV_so; cbn in *. + 2: discriminate. + destruct (invs # ifnot) as [inv_not | ] eqn:INV_not; cbn in *. + 2: discriminate. + rewrite rel_leb_correct in IND_so. + rewrite rel_leb_correct in IND_not. + destruct b. + { + rewrite INV_so. + cbn. + eapply rel_ge; eauto. + } + { + rewrite INV_not. + cbn. + eapply rel_ge; eauto. + } + (* END INVARIANT *) - (* Ijumptable *) econstructor. split. -- cgit