diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-05-21 17:37:54 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-05-21 17:37:54 +0100 |
| commit | fa3bd7cf4caf43b9e29e3aed834af19aa7a3c794 (patch) | |
| tree | 13682e172f9d723768fe8b81d0b0471a0e8ad2ce /src/hls/GibleSeq.v | |
| parent | fe286deeb5c8a81aad20b81cd2ce9a586cc99dca (diff) | |
| download | vericert-fa3bd7cf4caf43b9e29e3aed834af19aa7a3c794.tar.gz vericert-fa3bd7cf4caf43b9e29e3aed834af19aa7a3c794.zip | |
Finish abstr_seq_reverse_correct_fold
Diffstat (limited to 'src/hls/GibleSeq.v')
| -rw-r--r-- | src/hls/GibleSeq.v | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/src/hls/GibleSeq.v b/src/hls/GibleSeq.v index e99c860..c9d7ab2 100644 --- a/src/hls/GibleSeq.v +++ b/src/hls/GibleSeq.v @@ -314,3 +314,21 @@ Lemma step_instr_unchanged_state : forall A (ge: Genv.t A unit) sp r st st' cf, step_instr ge sp (Iexec st) r (Iterm st' cf) -> st = st'. Proof. intros. inv H; auto. Qed. + +Lemma step_exists: + forall A (ge: Genv.t A unit) sp instrs i i' ti cf, + SeqBB.step ge sp (Iexec i) instrs (Iterm i' cf) -> + state_equiv i ti -> + exists ti', + SeqBB.step ge sp (Iexec ti) instrs (Iterm ti' cf) + /\ state_equiv i' ti'. +Proof. + induction instrs. + - intros. inv H. + - intros. inv H. + + exploit (@step_exists A); eauto; simplify. + exploit IHinstrs; eauto; simplify. + eexists; split. econstructor; eauto. auto. + + inversion H4; subst. eexists. constructor. + constructor. eapply step_exists_Iterm; eauto. auto. +Qed. |