diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-05-14 14:44:55 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-05-14 14:44:55 +0100 |
| commit | 56d3a4d3f189a2f89d52375b1c71b230d87b05ee (patch) | |
| tree | 7da7049020f97cccfcbcb7ea3d1af95d159e304e /src/hls/GiblePargenproofBackward.v | |
| parent | 17f479648a2912e6a7c8c20664645f22a75cf1b8 (diff) | |
| download | vericert-56d3a4d3f189a2f89d52375b1c71b230d87b05ee.tar.gz vericert-56d3a4d3f189a2f89d52375b1c71b230d87b05ee.zip | |
Split correctness lemma into two
Diffstat (limited to 'src/hls/GiblePargenproofBackward.v')
| -rw-r--r-- | src/hls/GiblePargenproofBackward.v | 21 |
1 files changed, 19 insertions, 2 deletions
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. |