diff options
author | Yann Herklotz <git@yannherklotz.com> | 2021-11-11 12:30:28 +0000 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2021-11-11 12:30:28 +0000 |
commit | 182b6dec50ee4698bff6ef70f93788641d154cdb (patch) | |
tree | e717f6de915fc5548059a7bfc92cb062f6eebbb5 /src/hls/RTLPargenproof.v | |
parent | 389e66dfa8044cb07c7d32a1ffeb13e2578dc3e8 (diff) | |
download | vericert-182b6dec50ee4698bff6ef70f93788641d154cdb.tar.gz vericert-182b6dec50ee4698bff6ef70f93788641d154cdb.zip |
Prove some of the theorems further
Diffstat (limited to 'src/hls/RTLPargenproof.v')
-rw-r--r-- | src/hls/RTLPargenproof.v | 31 |
1 files changed, 17 insertions, 14 deletions
diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v index c0ba39f..df0615a 100644 --- a/src/hls/RTLPargenproof.v +++ b/src/hls/RTLPargenproof.v @@ -37,11 +37,6 @@ Require Import vericert.hls.Abstr. #[local] Open Scope forest. #[local] Open Scope pred_op. -(*| -Abstract computations -===================== -|*) - (*Definition is_regs i := match i with mk_instr_state rs _ => rs end. Definition is_mem i := match i with mk_instr_state _ m => m end. @@ -616,7 +611,7 @@ Proof. match goal with H: forall _, _ |- context[Mem.storev] => erewrite <- H; eauto end. -Qed. + - admit. Admitted. Lemma step_instr_list_matches : forall a ge sp st st', @@ -687,7 +682,7 @@ Proof. apply check_list_l_false in H. tauto. Qed. -Lemma sem_separate : +(*Lemma sem_separate : forall A ctx b a st', sem ctx (abstract_sequence empty (a ++ b)) st' -> exists st'', @@ -703,7 +698,7 @@ Proof. rewrite abstract_seq. eapply sem_update2; eauto. } -Qed. +Qed.*) Lemma sem_update_RBnop : forall A ctx f st', @@ -711,14 +706,22 @@ Lemma sem_update_RBnop : Proof. auto. Qed. Lemma sem_update_Op : - forall A ge sp ist f st' r l o0 o m rs v, + forall A ge sp ist f st' r l o0 o m rs v ps, @sem A (mk_ctx ist sp ge) f st' -> - Op.eval_operation ge sp o0 rs ## l m = Some v -> - match_states st' (mk_instr_state rs m ps) -> + eval_predf ps o = true -> + Op.eval_operation ge sp o0 (rs ## l) m = Some v -> + match_states st' (mk_instr_state rs ps m) -> exists tst, - sem (mk_ctx ist sp ge) (update f (RBop o o0 l r)) tst /\ match_states (mk_instr_state (Regmap.set r v rs) m ps) tst. + sem (mk_ctx ist sp ge) (update f (RBop (Some o) o0 l r)) tst + /\ match_states (mk_instr_state (Regmap.set r v rs) ps m) tst. Proof. - intros. inv H1. simplify. + intros. inv H1. inv H. inv H1. inv H3. simplify. + econstructor. simplify. + { constructor; try constructor; intros; try solve [rewrite genmap1; now eauto]. + destruct (Pos.eq_dec x r); subst. + { rewrite map2. specialize (H1 r). inv H1. +(*} + } destruct st. econstructor. simplify. { constructor. @@ -731,7 +734,7 @@ Proof. { constructor; eauto. intros. destruct (Pos.eq_dec r x); subst; [repeat rewrite Regmap.gss | repeat rewrite Regmap.gso]; auto. } -Qed. +Qed.*) Admitted. Lemma sem_update : forall A ge sp st x st' st'' st''' f, |