From 6426456c4cc7c6d11cf0204ff3d3c0aa18762323 Mon Sep 17 00:00:00 2001 From: James Pollard Date: Wed, 3 Jun 2020 20:59:55 +0100 Subject: Fix HTLgenspec proof for arrays. --- src/translation/HTLgenspec.v | 74 +++++++++++++++++++++++++------------------- 1 file changed, 43 insertions(+), 31 deletions(-) (limited to 'src/translation') diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index 86f27be..4bf3843 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -321,46 +321,58 @@ Proof. induction l; simpl; intros; try contradiction. destruct a as [pc1 instr1]; simpl in *. inv H0. monadInv H. inv_incr. destruct (peq pc pc1). - + subst. + - subst. 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 ]. - * 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. + + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + + 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. + + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + + 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 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. + + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + + 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 o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + + destruct H2. + * inversion H2. + replace (st_st s2) with (st_st s0) by congruence. + eauto with htlspec. + * apply in_map with (f := fst) in H2. contradiction. + + + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + + destruct H2. + * inversion H2. + replace (st_st s2) with (st_st s0) by congruence. + eauto with htlspec. + * apply in_map with (f := fst) in H2. contradiction. + + + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + + inversion H2. + * inversion H9. + replace (st_st s2) with (st_st s0) by congruence. + eauto with htlspec. + * apply in_map with (f := fst) in H9. contradiction. + + + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + + inversion H2. + * inversion H9. + replace (st_st s2) with (st_st s0) by congruence. + eauto with htlspec. + * apply in_map with (f := fst) in H9. contradiction. + + - eapply IHl. apply EQ0. assumption. destruct H2. inversion H2. subst. contradiction. intros. specialize H1 with pc0 instr0. destruct H1. tauto. trivial. destruct H2. inv H2. contradiction. assumption. assumption. -- cgit