diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-05-15 13:11:15 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-05-15 13:11:15 +0100 |
| commit | 1849816610419f688bddcb7446fd946995e3c2be (patch) | |
| tree | fe9bab98dcd7cbb0e889050024aaa52022b2fd8d /src/hls/GiblePargenproofBackward.v | |
| parent | 56d3a4d3f189a2f89d52375b1c71b230d87b05ee (diff) | |
| download | vericert-1849816610419f688bddcb7446fd946995e3c2be.tar.gz vericert-1849816610419f688bddcb7446fd946995e3c2be.zip | |
Add function to reason about executable constraints
Diffstat (limited to 'src/hls/GiblePargenproofBackward.v')
| -rw-r--r-- | src/hls/GiblePargenproofBackward.v | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/src/hls/GiblePargenproofBackward.v b/src/hls/GiblePargenproofBackward.v index ebb2744..93b1778 100644 --- a/src/hls/GiblePargenproofBackward.v +++ b/src/hls/GiblePargenproofBackward.v @@ -67,7 +67,7 @@ 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 : +(*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)) -> @@ -81,7 +81,7 @@ Lemma sem_exists_execution : 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. +Proof. Admitted. *) Lemma abstr_seq_reverse_correct : forall sp x i i' ti cf x', @@ -91,9 +91,10 @@ 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. +(* intros. exploit sem_exists_execution; eauto; simplify. eauto using sem_equiv_execution. -Qed. +Qed. *) + intros. (*| Proof Sketch: |