From 56d3a4d3f189a2f89d52375b1c71b230d87b05ee Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 14 May 2023 14:44:55 +0100 Subject: Split correctness lemma into two --- src/hls/GiblePargenproofBackward.v | 21 +++++++++++++++++++-- 1 file changed, 19 insertions(+), 2 deletions(-) (limited to 'src/hls/GiblePargenproofBackward.v') diff --git a/src/hls/GiblePargenproofBackward.v b/src/hls/GiblePargenproofBackward.v index e2bb23c..ebb2744 100644 --- a/src/hls/GiblePargenproofBackward.v +++ b/src/hls/GiblePargenproofBackward.v @@ -67,6 +67,22 @@ Context (prog: GibleSeq.program) (tprog : GiblePar.program). Let ge : GibleSeq.genv := Globalenvs.Genv.globalenv prog. Let tge : GiblePar.genv := Globalenvs.Genv.globalenv tprog. +Lemma sem_equiv_execution : + forall sp x i i' ti cf x' ti', + abstract_sequence x = Some x' -> + sem (mk_ctx i sp ge) x' (i', (Some cf)) -> + SeqBB.step ge sp (Iexec ti) x (Iterm ti' cf) -> + state_lessdef i ti -> + state_lessdef i' ti'. +Proof. Admitted. + +Lemma sem_exists_execution : + forall sp x i i' ti cf x', + abstract_sequence x = Some x' -> + sem (mk_ctx i sp ge) x' (i', (Some cf)) -> + exists ti', SeqBB.step ge sp (Iexec ti) x (Iterm ti' cf). +Proof. Admitted. + Lemma abstr_seq_reverse_correct : forall sp x i i' ti cf x', abstract_sequence x = Some x' -> @@ -75,6 +91,9 @@ Lemma abstr_seq_reverse_correct : exists ti', SeqBB.step ge sp (Iexec ti) x (Iterm ti' cf) /\ state_lessdef i' ti'. Proof. + intros. exploit sem_exists_execution; eauto; simplify. + eauto using sem_equiv_execution. +Qed. (*| Proof Sketch: @@ -91,6 +110,4 @@ comparison, because there two abstract states can be equal without one being evaluable. |*) -Admitted. - End CORRECTNESS. -- cgit