From feb29b9cf4a051ce0df81df84bc5f3228074de20 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 9 Sep 2020 11:41:08 +0200 Subject: Cleanup --- kvx/lib/RTLpathScheduler.v | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) (limited to 'kvx') diff --git a/kvx/lib/RTLpathScheduler.v b/kvx/lib/RTLpathScheduler.v index b70c1685..0f099ce8 100644 --- a/kvx/lib/RTLpathScheduler.v +++ b/kvx/lib/RTLpathScheduler.v @@ -159,7 +159,6 @@ Definition verified_scheduler (f: RTLpath.function) : res (RTLpath.function * (P 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 _ <- injective_checker dm; *) OK (tf, dm). Theorem verified_scheduler_correct f tf dm: @@ -171,13 +170,12 @@ Theorem verified_scheduler_correct f tf dm: /\ (forall pc1 pc2, dm ! pc2 = Some pc1 -> path_entry (fn_path f) pc1) /\ (forall pc1 pc2, dm ! pc2 = Some pc1 -> path_entry (fn_path tf) pc2) /\ (forall pc1 pc2, dm ! pc2 = Some pc1 -> sexec_simu dm f tf pc1 pc2) -(* /\ is_injective dm *) . Proof. 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 (* injective_checker_correct *): core. + function_equiv_checker_correct: core. destruct (function_builder _ _) as [res H]; simpl in * |- *; auto. apply H in EQ2. rewrite EQ2. simpl. repeat (constructor; eauto). @@ -192,7 +190,6 @@ Record match_function (dupmap: PTree.t node) (f1 f2: RTLpath.function): Prop := dupmap_path_entry1: forall pc1 pc2, dupmap!pc2 = Some pc1 -> path_entry (fn_path f1) pc1; dupmap_path_entry2: forall pc1 pc2, dupmap!pc2 = Some pc1 -> path_entry (fn_path f2) pc2; dupmap_correct: forall pc1 pc2, dupmap!pc2 = Some pc1 -> sexec_simu dupmap f1 f2 pc1 pc2; -(* dupmap_injective: is_injective dupmap *) }. Program Definition transf_function (f: RTLpath.function): -- cgit