diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-08-12 19:13:31 +0200 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-08-12 19:13:44 +0200 |
| commit | f9d3eaa70b8818d6e3d3ac57e789f58a99ae64e6 (patch) | |
| tree | a91c27d7fe155150714e95b9b849da82b51237bf | |
| parent | 8183f45c4a27dc81f8f43056a90fa4f0017edc8e (diff) | |
| download | vericert-kvx-f9d3eaa70b8818d6e3d3ac57e789f58a99ae64e6.tar.gz vericert-kvx-f9d3eaa70b8818d6e3d3ac57e789f58a99ae64e6.zip | |
Finish proof of conditionals
| -rw-r--r-- | src/translation/HTLgenproof.v | 15 |
1 files changed, 11 insertions, 4 deletions
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 65d5929..ee88d3a 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -867,10 +867,17 @@ Section CORRECTNESS. * assert (HPle1 : Ple r0 (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto). apply H in HPle1. inv HPle1. rewrite EQN2 in H1. inv H1. rewrite EQN2 in H1. inv H1. auto. rewrite EQN2 in H2. discriminate. - + exploit eval_cond_correct'. eauto. intros. eapply RTL.max_reg_function_use. apply INSTR. - simplify. right. right. apply H0. - auto. eapply EQ. intros. inv H0. inv H1. - econstructor. econstructor. eapply Verilog.erun_Vternary_true. apply H0. econstructor. auto. + + exploit eval_cond_correct'; eauto. intros. eapply RTL.max_reg_function_use. apply INSTR. + simplify; tauto. intros. inv H0. inv H1. destruct (Int.eq_dec x0 Int.zero). + econstructor. econstructor. eapply Verilog.erun_Vternary_false. + eassumption. econstructor. auto. subst. auto. constructor. + econstructor. econstructor. eapply Verilog.erun_Vternary_true. + eassumption. econstructor. auto. unfold valueToBool. pose proof n. apply Int.eq_false in n. + unfold uvalueToZ. unfold Int.eq in n. unfold zeq in *. + destruct (Int.unsigned x0 ==Z Int.unsigned Int.zero); try discriminate. + rewrite <- Z.eqb_neq in n0. rewrite Int.unsigned_zero in n0. rewrite n0. auto. + constructor. + Qed. (* Lemma eval_cond_correct : |