diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-05-25 22:32:33 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-05-25 22:32:33 +0100 |
| commit | 43b078ba35aec32840f459d67de3fe6408184cea (patch) | |
| tree | 85c9332b7b2c9037ffc79d583ee52aa05b99be8b /src/translation/HTLgenspec.v | |
| parent | 9f631b114e1cdcbaf3610eefd6f9fd7baeeda0c1 (diff) | |
| download | vericert-kvx-43b078ba35aec32840f459d67de3fe6408184cea.tar.gz vericert-kvx-43b078ba35aec32840f459d67de3fe6408184cea.zip | |
Finished proving the first case
Diffstat (limited to 'src/translation/HTLgenspec.v')
| -rw-r--r-- | src/translation/HTLgenspec.v | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index 8ea4384..f01ab1c 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -235,7 +235,7 @@ Proof. destruct (peq pc pc1). + subst. - destruct instr1. + destruct instr1 eqn:?. econstructor. unfold add_instr in EQ. destruct (check_empty_node_datapath s1 pc1); try discriminate. @@ -251,10 +251,15 @@ Proof. destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; [ discriminate | apply H7 ]. + inversion H1. inversion H7. rewrite H. apply tr_instr_Inop. + eapply in_map with (f := fst) in H7. simpl in H7. contradiction. + + eapply IHl. apply EQ0. assumption. destruct H1. inversion H1. subst. contradiction. assumption. + + Qed. Theorem transl_module_correct : |