diff options
author | James Pollard <james@pollard.dev> | 2020-06-03 19:38:40 +0100 |
---|---|---|
committer | James Pollard <james@pollard.dev> | 2020-06-03 19:38:40 +0100 |
commit | 0729bb6e93307567cc21702005ea1d8c8dddaf8f (patch) | |
tree | 552a10d138056ff26403dc3b72af6c32e27b55c6 /src/translation/HTLgenspec.v | |
parent | e3c66ff88570c5370b37f51404f71f485d2e5dfe (diff) | |
parent | 971b35fd4af24cfffc462df13f8c5b9be982858e (diff) | |
download | vericert-0729bb6e93307567cc21702005ea1d8c8dddaf8f.tar.gz vericert-0729bb6e93307567cc21702005ea1d8c8dddaf8f.zip |
Merge branch 'develop' into arrays-proof
Diffstat (limited to 'src/translation/HTLgenspec.v')
-rw-r--r-- | src/translation/HTLgenspec.v | 73 |
1 files changed, 38 insertions, 35 deletions
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index 3b68a7f..86f27be 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -322,46 +322,49 @@ Proof. destruct a as [pc1 instr1]; simpl in *. inv H0. monadInv H. inv_incr. destruct (peq pc pc1). + subst. - destruct instr1 eqn:?; try discriminate; try destruct_optional; inv_add_instr; econstructor. - * assumption. + destruct instr1 eqn:?; try discriminate; + try destruct_optional; inv_add_instr; econstructor; try assumption. * destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; [ discriminate | apply H9 ]. -(* * inversion H1. inversion H9. rewrite H. apply tr_instr_Inop. - eapply in_map with (f := fst) in H7. simpl in H7. contradiction. - - * destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; - [ discriminate | apply H7 ]. - * destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; - [ discriminate | apply H7 ]. - * inversion H1. inversion H7. unfold nonblock. rewrite <- e2. rewrite H. constructor. + * destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; + [ discriminate | apply H9 ]. + * inversion H2. inversion H9. rewrite H. apply tr_instr_Inop. + eapply in_map with (f := fst) in H9. contradiction. + + * destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; + [ discriminate | apply H9 ]. + * destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; + [ discriminate | apply H9 ]. + * inversion H2. inversion H9. unfold nonblock. rewrite <- e2. rewrite H. constructor. eapply translate_instr_tr_op. apply EQ1. - eapply in_map with (f := fst) in H7. simpl in H7. contradiction. - - * destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; - [ discriminate | apply H7 ]. - * destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; - [ discriminate | apply H7 ]. - * inversion H1. inversion H7. rewrite <- e2. rewrite H. econstructor. apply EQ1. - eapply in_map with (f := fst) in H7. simpl in H7. contradiction. - - * destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; - [ discriminate | apply H7 ]. - * destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; - [ discriminate | apply H7 ]. - * inversion H1. inversion H7. constructor. - eapply in_map with (f := fst) in H7. simpl in H7. contradiction. - - * destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; - [ discriminate | apply H7 ]. - * destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; - [ discriminate | apply H7 ]. - * inversion H1. inversion H7. constructor. - eapply in_map with (f := fst) in H7. simpl in H7. contradiction. + eapply in_map with (f := fst) in H9. contradiction. + + * destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; + [ discriminate | apply H9 ]. + * destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; + [ discriminate | apply H9 ]. + * inversion H2. inversion H9. rewrite <- e2. rewrite H. econstructor. apply EQ1. + eapply in_map with (f := fst) in H9. contradiction. + + * destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; + [ discriminate | apply H9 ]. + * destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; + [ discriminate | apply H9 ]. + * inversion H2. inversion H9. constructor. + eapply in_map with (f := fst) in H9. contradiction. + + * destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; + [ discriminate | apply H9 ]. + * destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; + [ discriminate | apply H9 ]. + * inversion H2. inversion H9. constructor. + eapply in_map with (f := fst) in H9. contradiction. + eapply IHl. apply EQ0. assumption. - destruct H1. inversion H1. subst. contradiction. - assumption.*) -Admitted. + destruct H2. inversion H2. subst. contradiction. + intros. specialize H1 with pc0 instr0. destruct H1. tauto. trivial. + destruct H2. inv H2. contradiction. assumption. assumption. +Qed. Hint Resolve iter_expand_instr_spec : htlspec. Theorem transl_module_correct : |