diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-12-09 09:13:40 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-12-09 09:13:40 +0100 |
| commit | 8f2cf0b53b3a7fd4bc339fddf89197601eb549c2 (patch) | |
| tree | 8490baae5d2b324c1705cc971fdc5cc8414d06ff /backend | |
| parent | b4af6cbe24b1108b4e49d3c17fecc37255bd6151 (diff) | |
| download | compcert-kvx-8f2cf0b53b3a7fd4bc339fddf89197601eb549c2.tar.gz compcert-kvx-8f2cf0b53b3a7fd4bc339fddf89197601eb549c2.zip | |
one 'admit' less
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/CSE3proof.v | 38 |
1 files changed, 36 insertions, 2 deletions
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. |