diff options
author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-04-17 17:35:45 +0100 |
---|---|---|
committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-04-17 17:35:45 +0100 |
commit | 7126b59ac4e768c147ef0ea60ab614b011cb3d36 (patch) | |
tree | 2b313bdab74e5063216c3e4947fa7047d4360132 /src/hls | |
parent | 558f81ee04827ee44e73b2450e96640569b56eb4 (diff) | |
download | vericert-7126b59ac4e768c147ef0ea60ab614b011cb3d36.tar.gz vericert-7126b59ac4e768c147ef0ea60ab614b011cb3d36.zip |
[WIP] HTLgenspec proof
Diffstat (limited to 'src/hls')
-rw-r--r-- | src/hls/HTLgenspec.v | 80 |
1 files changed, 34 insertions, 46 deletions
diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v index d9928a9..a330f6a 100644 --- a/src/hls/HTLgenspec.v +++ b/src/hls/HTLgenspec.v @@ -135,23 +135,23 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> datapath_stmnt - Z.pos n <= Int.max_unsigned -> translate_instr op args s = OK e s' i -> tr_instr fin rtrn st stk (RTL.Iop op args dst n) (data_vstmnt (Vnonblock (Vvar dst) e)) (state_goto st n) -| tr_instr_Icall : - forall n sig fn args dst, - Z.pos n <= Int.max_unsigned -> - tr_instr fin rtrn st stk (RTL.Icall sig (inr fn) args dst n) (HTLfork fn args) (state_goto st n) +(* | tr_instr_Icall : *) +(* forall n sig fn args dst, *) +(* Z.pos n <= Int.max_unsigned -> *) +(* tr_instr fin rtrn st stk (RTL.Icall sig (inr fn) args dst n) (HTLfork fn args) (state_goto st n) *) | tr_instr_Icond : forall n1 n2 cond args s s' i c, Z.pos n1 <= Int.max_unsigned -> Z.pos n2 <= Int.max_unsigned -> translate_condition cond args s = OK c s' i -> tr_instr fin rtrn st stk (RTL.Icond cond args n1 n2) (data_vstmnt Vskip) (state_cond st c n1 n2) -| tr_instr_Ireturn_None : - tr_instr fin rtrn st stk (RTL.Ireturn None) (data_vstmnt (Vseq (block fin (Vlit (ZToValue 1%Z))) - (block rtrn (Vlit (ZToValue 0%Z))))) (ctrl_vstmnt Vskip) -| tr_instr_Ireturn_Some : - forall r, - tr_instr fin rtrn st stk (RTL.Ireturn (Some r)) - (data_vstmnt (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r)))) (ctrl_vstmnt Vskip) +(* | tr_instr_Ireturn_None : *) +(* tr_instr fin rtrn st stk (RTL.Ireturn None) (data_vstmnt (Vseq (block fin (Vlit (ZToValue 1%Z))) *) +(* (block rtrn (Vlit (ZToValue 0%Z))))) (ctrl_vstmnt Vskip) *) +(* | tr_instr_Ireturn_Some : *) +(* forall r, *) +(* tr_instr fin rtrn st stk (RTL.Ireturn (Some r)) *) +(* (data_vstmnt (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r)))) (ctrl_vstmnt Vskip) *) | tr_instr_Iload : forall mem addr args s s' i c dst n, Z.pos n <= Int.max_unsigned -> @@ -554,24 +554,29 @@ Proof. - subst. destruct instr1 eqn:?; try discriminate; try destruct_optional; try inv_add_instr; econstructor; try assumption. + + (* 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. apply Z.leb_le. assumption. eapply in_map with (f := fst) in H9. contradiction. + (* Iop *) + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + inversion H2. inversion H14. unfold nonblock. replace (st_st s4) with (st_st s2) by congruence. econstructor. apply Z.leb_le; assumption. apply EQ1. eapply in_map with (f := fst) in H14. contradiction. + (* Iload *) + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + inversion H2. inversion H14. rewrite <- e2. replace (st_st s2) with (st_st s0) by congruence. econstructor. apply Z.leb_le; assumption. apply EQ1. eapply in_map with (f := fst) in H14. contradiction. + (* Istore *) + 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. @@ -581,17 +586,12 @@ Proof. eauto with htlspec. * apply in_map with (f := fst) in H2. contradiction. - + admit. (* destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; discriminate. *) - + admit. (* destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; discriminate. *) + (* Icall *) + + admit. + + admit. + admit. - (* destruct H2. *) - (* * inversion H2. *) - (* replace (st_st s2) with (st_st s0) by congruence. *) - (* replace (st_st s1) with (st_st s0) by congruence. *) - (* econstructor. *) - (* apply Z.leb_le. assumption. *) - (* * apply in_map with (f := fst) in H2. contradiction. *) + (* Icond *) + 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. @@ -601,32 +601,20 @@ Proof. eauto with htlspec. * apply in_map with (f := fst) in H2. contradiction. - (* + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. *) - (* + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. *) - (* + inversion H2. *) - (* * inversion H14. constructor. congruence. *) - (* * apply in_map with (f := fst) in H14. 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. *) + (* Ireturn (Some r) *) + + admit. + + admit. + + admit. + + (* Ireturn None *) + + admit. + + admit. + + admit. + + - 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. Admitted. Hint Resolve iter_expand_instr_spec : htlspec. |