diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-07-16 12:54:19 +0200 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-07-16 12:54:19 +0200 |
| commit | d6a846b641787ea6a5ed113b1d7275ffb5028d9c (patch) | |
| tree | d8c9bad4b9a0e5a82d8e64345a50387b561b3ddb | |
| parent | fd4d085aa988a6044f89fc17e8422be23bc87f9d (diff) | |
| download | compcert-kvx-d6a846b641787ea6a5ed113b1d7275ffb5028d9c.tar.gz compcert-kvx-d6a846b641787ea6a5ed113b1d7275ffb5028d9c.zip | |
rm "Admitted"
| -rw-r--r-- | scheduling/RTLpathScheduler.v | 21 |
1 files changed, 10 insertions, 11 deletions
diff --git a/scheduling/RTLpathScheduler.v b/scheduling/RTLpathScheduler.v index 5a81dd28..31680256 100644 --- a/scheduling/RTLpathScheduler.v +++ b/scheduling/RTLpathScheduler.v @@ -158,7 +158,7 @@ Definition verified_scheduler (f: RTLpath.function) : res (RTLpath.function * (P let (tc, te) := tcte in let tfr := mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) tc te in do tf <- proj1_sig (function_builder tfr tpm); - (* do tt <- function_equiv_checker dm f tf; *) + do tt <- function_equiv_checker dm f tf; OK (tf, dm). Theorem verified_scheduler_correct f tf dm: @@ -172,16 +172,15 @@ Theorem verified_scheduler_correct f tf dm: /\ (forall pc1 pc2, dm ! pc2 = Some pc1 -> sexec_simu dm f tf pc1 pc2) . Proof. - Admitted. -(* intros VERIF. unfold verified_scheduler in VERIF. explore. *) -(* Local Hint Resolve function_equiv_checker_entrypoint *) -(* function_equiv_checker_pathentry1 function_equiv_checker_pathentry2 *) -(* function_equiv_checker_correct: core. *) -(* destruct (function_builder _ _) as [res H]; simpl in * |- *; auto. *) -(* apply H in EQ2. rewrite EQ2. simpl. *) -(* repeat (constructor; eauto). *) -(* exploit function_equiv_checker_entrypoint. eapply EQ4. rewrite EQ2. intuition. *) -(* Qed. *) + intros VERIF. unfold verified_scheduler in VERIF. explore. + Local Hint Resolve function_equiv_checker_entrypoint + function_equiv_checker_pathentry1 function_equiv_checker_pathentry2 + function_equiv_checker_correct: core. + destruct (function_builder _ _) as [res H]; simpl in * |- *; auto. + apply H in EQ2. rewrite EQ2. simpl. + repeat (constructor; eauto). + exploit function_equiv_checker_entrypoint. eapply EQ4. rewrite EQ2. intuition. +Qed. Record match_function (dupmap: PTree.t node) (f1 f2: RTLpath.function): Prop := { preserv_fnsig: fn_sig f1 = fn_sig f2; |