From 9bccd4a26cc9d04536ddba46b3e161eaaa422bf2 Mon Sep 17 00:00:00 2001 From: Michalis Pardalos Date: Sun, 18 Apr 2021 12:56:03 +0100 Subject: [WIP] Use Program instead of state_incr lemmas --- src/hls/HTLgen.v | 205 +++++++++++-------------------------------------------- 1 file changed, 40 insertions(+), 165 deletions(-) (limited to 'src/hls/HTLgen.v') diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v index 087c28f..dfea1f3 100644 --- a/src/hls/HTLgen.v +++ b/src/hls/HTLgen.v @@ -147,43 +147,18 @@ Proof. intros. case (s.(st_controllogic)!n); tauto. Defined. -Lemma declare_reg_state_incr : - forall i s r sz, - st_incr s - (mkstate - s.(st_st) - s.(st_freshreg) - s.(st_freshstate) - (AssocMap.set r (i, VScalar sz) s.(st_scldecls)) - s.(st_arrdecls) - s.(st_datapath) - s.(st_controllogic)). -Proof. auto with htlh. Qed. - -Definition declare_reg (i : option io) (r : reg) (sz : nat) : mon unit := +Program Definition declare_reg (i : option io) (r : reg) (sz : nat) : mon unit := fun s => OK tt (mkstate - s.(st_st) - s.(st_freshreg) - s.(st_freshstate) + (st_st s) + (st_freshreg s) + (st_freshstate s) (AssocMap.set r (i, VScalar sz) s.(st_scldecls)) - s.(st_arrdecls) - s.(st_datapath) - s.(st_controllogic)) - (declare_reg_state_incr i s r sz). - -Lemma create_state_state_incr: - forall s, - st_incr s (mkstate - s.(st_st) - (st_freshreg s) - (Pos.succ (st_freshstate s)) - (st_scldecls s) - (st_arrdecls s) - (st_datapath s) - (st_controllogic s)). -Proof. constructor; simpl; auto with htlh. Qed. - -Definition create_state : mon node := + (st_arrdecls s) + (st_datapath s) + (st_controllogic s)) _. +Next Obligation. auto with htlh. Qed. + +Program Definition create_state : mon node := fun s => let r := s.(st_freshstate) in OK r (mkstate s.(st_st) @@ -192,29 +167,10 @@ Definition create_state : mon node := (st_scldecls s) (st_arrdecls s) (st_datapath s) - (st_controllogic s)) - (create_state_state_incr s). - -Lemma add_instr_state_incr : - forall s n n' st, - (st_datapath s)!n = None -> - (st_controllogic s)!n = None -> - st_incr s - (mkstate - s.(st_st) - s.(st_freshreg) - (st_freshstate s) - s.(st_scldecls) - s.(st_arrdecls) - (AssocMap.set n st s.(st_datapath)) - (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic))). -Proof. - constructor; intros; - try (simpl; destruct (peq n n0); subst); - auto with htlh. -Qed. + (st_controllogic s)) _. +Next Obligation. constructor; simpl; eauto with htlh. Qed. -Definition add_instr (n : node) (n' : node) (st : datapath_stmnt) : mon unit := +Program Definition add_instr (n : node) (n' : node) (st : datapath_stmnt) : mon unit := fun s => match check_empty_node_datapath s n, check_empty_node_controllogic s n with | left STM, left TRANS => @@ -225,48 +181,14 @@ Definition add_instr (n : node) (n' : node) (st : datapath_stmnt) : mon unit := s.(st_scldecls) s.(st_arrdecls) (AssocMap.set n st s.(st_datapath)) - (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic))) - (add_instr_state_incr s n n' st STM TRANS) + (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic))) _ | _, _ => Error (Errors.msg "HTL.add_instr") end. - -Lemma add_instr_skip_state_incr : - forall s n st, - (st_datapath s)!n = None -> - (st_controllogic s)!n = None -> - st_incr s - (mkstate - s.(st_st) - s.(st_freshreg) - (st_freshstate s) - s.(st_scldecls) - s.(st_arrdecls) - (AssocMap.set n st s.(st_datapath)) - (AssocMap.set n Vskip s.(st_controllogic))). -Proof. - constructor; intros; - try (simpl; destruct (peq n n0); subst); - auto with htlh. -Qed. - -Lemma add_instr_wait_state_incr : - forall wait_mod s n n' st, - (st_datapath s)!n = None -> - (st_controllogic s)!n = None -> - st_incr s - (mkstate - s.(st_st) - s.(st_freshreg) - (st_freshstate s) - s.(st_scldecls) - s.(st_arrdecls) - (AssocMap.set n st s.(st_datapath)) - (AssocMap.set n (HTLwait wait_mod s.(st_st) (Vlit (posToValue n'))) s.(st_controllogic))). -Proof. +Next Obligation. constructor; intros; try (simpl; destruct (peq n n0); subst); auto with htlh. -Qed. + Qed. Program Definition add_instr_wait (wait_reg : reg) (n : node) (n' : node) (st : datapath_stmnt) : mon unit := fun s => @@ -289,7 +211,7 @@ Next Obligation. auto with htlh. Qed. -Definition add_instr_skip (n : node) (st : datapath_stmnt) : mon unit := +Program Definition add_instr_skip (n : node) (st : datapath_stmnt) : mon unit := fun s => match check_empty_node_datapath s n, check_empty_node_controllogic s n with | left STM, left TRANS => @@ -301,30 +223,16 @@ Definition add_instr_skip (n : node) (st : datapath_stmnt) : mon unit := s.(st_arrdecls) (AssocMap.set n st s.(st_datapath)) (AssocMap.set n Vskip s.(st_controllogic))) - (add_instr_skip_state_incr s n st STM TRANS) + _ | _, _ => Error (Errors.msg "HTL.add_instr") end. - -Lemma add_node_skip_state_incr : - forall s n st, - (st_datapath s)!n = None -> - (st_controllogic s)!n = None -> - st_incr s - (mkstate - s.(st_st) - s.(st_freshreg) - (st_freshstate s) - s.(st_scldecls) - s.(st_arrdecls) - (AssocMap.set n Vskip s.(st_datapath)) - (AssocMap.set n st s.(st_controllogic))). -Proof. +Next Obligation. constructor; intros; try (simpl; destruct (peq n n0); subst); auto with htlh. Qed. -Definition add_node_skip (n : node) (st : control_stmnt) : mon unit := +Program Definition add_node_skip (n : node) (st : control_stmnt) : mon unit := fun s => match check_empty_node_datapath s n, check_empty_node_controllogic s n with | left STM, left TRANS => @@ -336,10 +244,14 @@ Definition add_node_skip (n : node) (st : control_stmnt) : mon unit := s.(st_arrdecls) (AssocMap.set n Vskip s.(st_datapath)) (AssocMap.set n st s.(st_controllogic))) - (add_node_skip_state_incr s n st STM TRANS) + _ | _, _ => Error (Errors.msg "HTL.add_instr") end. - +Next Obligation. + constructor; intros; + try (simpl; destruct (peq n n0); subst); + auto with htlh. +Qed. Definition translate_comparison (c : Integers.comparison) (args : list reg) : mon expr := match c, args with @@ -473,25 +385,7 @@ Definition translate_instr (op : Op.operation) (args : list reg) : mon expr := | _, _ => error (Errors.msg "Htlgen: Instruction not implemented: other") end. -Lemma add_branch_instr_state_incr: - forall s e n n1 n2, - (st_datapath s) ! n = None -> - (st_controllogic s) ! n = None -> - st_incr s (mkstate - s.(st_st) - (st_freshreg s) - (st_freshstate s) - s.(st_scldecls) - s.(st_arrdecls) - (AssocMap.set n Vskip (st_datapath s)) - (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s))). -Proof. - intros. apply state_incr_intro; simpl; - try (intros; destruct (peq n0 n); subst); - auto with htlh. -Qed. - -Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit := +Program Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit := fun s => match check_empty_node_datapath s n, check_empty_node_controllogic s n with | left NSTM, left NTRANS => @@ -503,9 +397,14 @@ Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit := s.(st_arrdecls) (AssocMap.set n Vskip (st_datapath s)) (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s))) - (add_branch_instr_state_incr s e n n1 n2 NSTM NTRANS) + _ | _, _ => Error (Errors.msg "Htlgen: add_branch_instr") end. +Next Obligation. + intros. apply state_incr_intro; simpl; + try (intros; destruct (peq n0 n); subst); + auto with htlh. +Qed. Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing) (args : list reg) (stack : reg) : mon expr := @@ -597,19 +496,7 @@ Definition transf_instr (modmap : PTree.t HTL.module) (fin rtrn stack: reg) (ni: end end. -Lemma create_reg_state_incr: - forall s sz i, - st_incr s (mkstate - s.(st_st) - (Pos.succ (st_freshreg s)) - (st_freshstate s) - (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls)) - s.(st_arrdecls) - (st_datapath s) - (st_controllogic s)). -Proof. constructor; simpl; auto with htlh. Qed. - -Definition create_reg (i : option io) (sz : nat) : mon reg := +Program Definition create_reg (i : option io) (sz : nat) : mon reg := fun s => let r := s.(st_freshreg) in OK r (mkstate s.(st_st) @@ -618,22 +505,10 @@ Definition create_reg (i : option io) (sz : nat) : mon reg := (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls)) (st_arrdecls s) (st_datapath s) - (st_controllogic s)) - (create_reg_state_incr s sz i). - -Lemma create_arr_state_incr: - forall s sz ln i, - st_incr s (mkstate - s.(st_st) - (Pos.succ (st_freshreg s)) - (st_freshstate s) - s.(st_scldecls) - (AssocMap.set s.(st_freshreg) (i, VArray sz ln) s.(st_arrdecls)) - (st_datapath s) - (st_controllogic s)). -Proof. constructor; simpl; auto with htlh. Qed. - -Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) := + (st_controllogic s)) _. +Next Obligation. constructor; simpl; auto with htlh. Qed. + +Program Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) := fun s => let r := s.(st_freshreg) in OK (r, ln) (mkstate s.(st_st) @@ -642,8 +517,8 @@ Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) := s.(st_scldecls) (AssocMap.set s.(st_freshreg) (i, VArray sz ln) s.(st_arrdecls)) (st_datapath s) - (st_controllogic s)) - (create_arr_state_incr s sz ln i). + (st_controllogic s)) _. +Next Obligation. constructor; simpl; auto with htlh. Qed. Definition stack_correct (sz : Z) : bool := (0 <=? sz) && (sz