diff options
author | Yann Herklotz <git@yannherklotz.com> | 2021-04-06 23:08:03 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2021-04-06 23:08:03 +0100 |
commit | 23a2a2fb2916a7ecb240aa51686bbe049f8418e4 (patch) | |
tree | f5f9cf0001bbd44cfaab7d70f3c169b8275be15d /src | |
parent | 873162771e87c6c358dc07e58bc0bd3a08f9a00e (diff) | |
download | vericert-23a2a2fb2916a7ecb240aa51686bbe049f8418e4.tar.gz vericert-23a2a2fb2916a7ecb240aa51686bbe049f8418e4.zip |
Finish load and store proof, but broke top-level
Diffstat (limited to 'src')
-rw-r--r-- | src/hls/HTL.v | 109 | ||||
-rw-r--r-- | src/hls/HTLPargen.v | 29 | ||||
-rw-r--r-- | src/hls/HTLgen.v | 48 | ||||
-rw-r--r-- | src/hls/HTLgenspec.v | 8 | ||||
-rw-r--r-- | src/hls/Memorygen.v | 368 | ||||
-rw-r--r-- | src/hls/Verilog.v | 37 | ||||
-rw-r--r-- | src/hls/Veriloggenproof.v | 7 |
7 files changed, 317 insertions, 289 deletions
diff --git a/src/hls/HTL.v b/src/hls/HTL.v index 98ea6d0..e614246 100644 --- a/src/hls/HTL.v +++ b/src/hls/HTL.v @@ -18,6 +18,7 @@ *) Require Import Coq.FSets.FMapPositive. +Require Import Coq.micromega.Lia. Require compcert.common.Events. Require compcert.common.Globalenvs. @@ -32,6 +33,8 @@ Require Import vericert.hls.AssocMap. Require Import vericert.hls.Array. Require vericert.hls.Verilog. +Local Open Scope positive. + (** The purpose of the hardware transfer language (HTL) is to create a more hardware-like layout that is still similar to the register transfer language (RTL) that it came from. The main change is that function calls become module @@ -49,7 +52,7 @@ Definition controllogic := PTree.t Verilog.stmnt. Definition map_well_formed {A : Type} (m : PTree.t A) : Prop := forall p0 : positive, In p0 (map fst (Maps.PTree.elements m)) -> - Z.pos p0 <= Integers.Int.max_unsigned. + (Z.pos p0 <= Integers.Int.max_unsigned)%Z. Record ram := mk_ram { ram_size: nat; @@ -64,9 +67,11 @@ Record ram := mk_ram { /\ ram_en < ram_d_in /\ ram_d_in < ram_d_out /\ ram_d_out < ram_wr_en - /\ ram_wr_en < ram_u_en)%positive + /\ ram_wr_en < ram_u_en) }. +Definition module_ordering a b c d e f g := a < b < c /\ c < d < e /\ e < f < g. + Record module: Type := mkmodule { mod_params : list reg; @@ -84,7 +89,9 @@ Record module: Type := mod_scldecls : AssocMap.t (option Verilog.io * Verilog.scl_decl); mod_arrdecls : AssocMap.t (option Verilog.io * Verilog.arr_decl); mod_ram : option ram; - mod_wf : (map_well_formed mod_controllogic /\ map_well_formed mod_datapath); + mod_wf : map_well_formed mod_controllogic /\ map_well_formed mod_datapath; + mod_ordering_wf : module_ordering mod_st mod_finish mod_return mod_stk mod_start mod_reset mod_clk; + mod_ram_wf : forall r', mod_ram = Some r' -> mod_clk < ram_addr r'; }. Definition fundef := AST.fundef module. @@ -198,7 +205,7 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := asr' = Verilog.merge_regs nasr3 basr3 -> asa' = Verilog.merge_arrs nasa3 basa3 -> asr'!(m.(mod_st)) = Some (posToValue pstval) -> - Z.pos pstval <= Integers.Int.max_unsigned -> + (Z.pos pstval <= Integers.Int.max_unsigned)%Z -> step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa') | step_finish : forall g m st asr asa retval sf, @@ -237,3 +244,97 @@ Inductive final_state : state -> Integers.int -> Prop := Definition semantics (m : program) := Smallstep.Semantics step (initial_state m) final_state (Globalenvs.Genv.globalenv m). + +Definition max_pc_function (m: module) := + List.fold_left Pos.max (List.map fst (PTree.elements m.(mod_controllogic))) 1. + +Definition max_list := fold_right Pos.max 1. + +Definition max_stmnt_tree t := + PTree.fold (fun i _ st => Pos.max (Verilog.max_reg_stmnt st) i) t 1. + +Definition max_reg_ram r := + match r with + | None => 1 + | Some ram => Pos.max (ram_mem ram) + (Pos.max (ram_en ram) + (Pos.max (ram_addr ram) + (Pos.max (ram_addr ram) + (Pos.max (ram_wr_en ram) + (Pos.max (ram_d_in ram) + (Pos.max (ram_d_out ram) (ram_u_en ram))))))) + end. + +Definition max_reg_module m := + Pos.max (max_list (mod_params m)) + (Pos.max (max_stmnt_tree (mod_datapath m)) + (Pos.max (max_stmnt_tree (mod_controllogic m)) + (Pos.max (mod_st m) + (Pos.max (mod_stk m) + (Pos.max (mod_finish m) + (Pos.max (mod_return m) + (Pos.max (mod_start m) + (Pos.max (mod_reset m) + (Pos.max (mod_clk m) (max_reg_ram (mod_ram m))))))))))). + +Lemma max_fold_lt : + forall m l n, m <= n -> m <= (fold_left Pos.max l n). +Proof. induction l; crush; apply IHl; lia. Qed. + +Lemma max_fold_lt2 : + forall (l: list (positive * Verilog.stmnt)) v n, + v <= n -> + v <= fold_left (fun a p => Pos.max (Verilog.max_reg_stmnt (snd p)) a) l n. +Proof. induction l; crush; apply IHl; lia. Qed. + +Lemma max_fold_lt3 : + forall (l: list (positive * Verilog.stmnt)) v v', + v <= v' -> + fold_left (fun a0 p => Pos.max (Verilog.max_reg_stmnt (snd p)) a0) l v + <= fold_left (fun a0 p => Pos.max (Verilog.max_reg_stmnt (snd p)) a0) l v'. +Proof. induction l; crush; apply IHl; lia. Qed. + +Lemma max_fold_lt4 : + forall (l: list (positive * Verilog.stmnt)) (a: positive * Verilog.stmnt), + fold_left (fun a0 p => Pos.max (Verilog.max_reg_stmnt (snd p)) a0) l 1 + <= fold_left (fun a0 p => Pos.max (Verilog.max_reg_stmnt (snd p)) a0) l + (Pos.max (Verilog.max_reg_stmnt (snd a)) 1). +Proof. intros; apply max_fold_lt3; lia. Qed. + +Lemma max_reg_stmnt_lt_stmnt_tree': + forall l (i: positive) v, + In (i, v) l -> + list_norepet (map fst l) -> + Verilog.max_reg_stmnt v <= fold_left (fun a p => Pos.max (Verilog.max_reg_stmnt (snd p)) a) l 1. +Proof. + induction l; crush. inv H; inv H0; simplify. apply max_fold_lt2. lia. + transitivity (fold_left (fun (a : positive) (p : positive * Verilog.stmnt) => + Pos.max (Verilog.max_reg_stmnt (snd p)) a) l 1). + eapply IHl; eauto. apply max_fold_lt4. +Qed. + +Lemma max_reg_stmnt_le_stmnt_tree : + forall d i v, + d ! i = Some v -> + Verilog.max_reg_stmnt v <= max_stmnt_tree d. +Proof. + intros. unfold max_stmnt_tree. rewrite PTree.fold_spec. + apply PTree.elements_correct in H. + eapply max_reg_stmnt_lt_stmnt_tree'; eauto. + apply PTree.elements_keys_norepet. +Qed. + +Lemma max_reg_stmnt_lt_stmnt_tree : + forall d i v, + d ! i = Some v -> + Verilog.max_reg_stmnt v < max_stmnt_tree d + 1. +Proof. intros. apply max_reg_stmnt_le_stmnt_tree in H; lia. Qed. + +Lemma max_stmnt_lt_module : + forall m d i, + (mod_controllogic m) ! i = Some d \/ (mod_datapath m) ! i = Some d -> + Verilog.max_reg_stmnt d < max_reg_module m + 1. +Proof. + inversion 1 as [ Hv | Hv ]; unfold max_reg_module; + apply max_reg_stmnt_le_stmnt_tree in Hv; lia. +Qed. diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v index 9bf7ed7..50defee 100644 --- a/src/hls/HTLPargen.v +++ b/src/hls/HTLPargen.v @@ -786,7 +786,19 @@ Definition transf_bblock (fin rtrn stack preg: reg) (ni : node * bblock) | _ => translate_cfi fin rtrn stack preg (nstate, bb.(bb_exit)) end. -Definition transf_module (f: function) : mon HTL.module := +Definition decide_order a b c d e f g : {module_ordering a b c d e f g} + {True}. + refine (match bool_dec ((a <? b) && (b <? c) && (c <? d) + && (d <? e) && (e <? f) && (f <? g))%positive true with + | left t => left _ + | _ => _ + end); auto. + simplify; repeat match goal with + | H: context[(_ <? _)%positive] |- _ => apply Pos.ltb_lt in H + end; unfold module_ordering; auto. +Defined. + +Definition transf_module (f: function) : mon HTL.module. + refine ( if stack_correct f.(fn_stacksize) then do fin <- create_reg (Some Voutput) 1; do rtrn <- create_reg (Some Voutput) 32; @@ -804,8 +816,10 @@ Definition transf_module (f: function) : mon HTL.module := match zle (Z.pos (max_pc_map current_state.(st_datapath))) Integers.Int.max_unsigned, zle (Z.pos (max_pc_map current_state.(st_controllogic))) - Integers.Int.max_unsigned with - | left LEDATA, left LECTRL => + Integers.Int.max_unsigned, + decide_order (st_st current_state) fin rtrn stack start rst clk + with + | left LEDATA, left LECTRL, left MORD => ret (HTL.mkmodule f.(fn_params) current_state.(st_datapath) @@ -822,10 +836,13 @@ Definition transf_module (f: function) : mon HTL.module := current_state.(st_scldecls) current_state.(st_arrdecls) None - (conj (max_pc_wf _ LECTRL) (max_pc_wf _ LEDATA))) - | _, _ => error (Errors.msg "More than 2^32 states.") + (conj (max_pc_wf _ LECTRL) (max_pc_wf _ LEDATA)) + MORD + _) + | _, _, _ => error (Errors.msg "More than 2^32 states.") end - else error (Errors.msg "Stack size misalignment."). + else error (Errors.msg "Stack size misalignment.")); discriminate. +Defined. Definition max_state (f: function) : state := let st := Pos.succ (max_reg_function f) in diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v index c071868..b55d7a3 100644 --- a/src/hls/HTLgen.v +++ b/src/hls/HTLgen.v @@ -583,7 +583,19 @@ Proof. simplify. transitivity (Z.pos (max_pc_map m)); eauto. Qed. -Definition transf_module (f: function) : mon HTL.module := +Definition decide_order a b c d e f g : {module_ordering a b c d e f g} + {True}. + refine (match bool_dec ((a <? b) && (b <? c) && (c <? d) + && (d <? e) && (e <? f) && (f <? g))%positive true with + | left t => left _ + | _ => _ + end); auto. + simplify; repeat match goal with + | H: context[(_ <? _)%positive] |- _ => apply Pos.ltb_lt in H + end; unfold module_ordering; auto. +Defined. + +Definition transf_module (f: function) : mon HTL.module. + refine ( if stack_correct f.(fn_stacksize) then do fin <- create_reg (Some Voutput) 1; do rtrn <- create_reg (Some Voutput) 32; @@ -595,8 +607,10 @@ Definition transf_module (f: function) : mon HTL.module := do clk <- create_reg (Some Vinput) 1; do current_state <- get; match zle (Z.pos (max_pc_map current_state.(st_datapath))) Integers.Int.max_unsigned, - zle (Z.pos (max_pc_map current_state.(st_controllogic))) Integers.Int.max_unsigned with - | left LEDATA, left LECTRL => + zle (Z.pos (max_pc_map current_state.(st_controllogic))) Integers.Int.max_unsigned, + decide_order (st_st current_state) fin rtrn stack start rst clk + with + | left LEDATA, left LECTRL, left MORD => ret (HTL.mkmodule f.(RTL.fn_params) current_state.(st_datapath) @@ -613,16 +627,19 @@ Definition transf_module (f: function) : mon HTL.module := current_state.(st_scldecls) current_state.(st_arrdecls) None - (conj (max_pc_wf _ LECTRL) (max_pc_wf _ LEDATA))) - | _, _ => error (Errors.msg "More than 2^32 states.") + (conj (max_pc_wf _ LECTRL) (max_pc_wf _ LEDATA)) + MORD + _) + | _, _, _ => error (Errors.msg "More than 2^32 states.") end - else error (Errors.msg "Stack size misalignment."). + else error (Errors.msg "Stack size misalignment.")); discriminate. +Defined. Definition max_state (f: function) : state := let st := Pos.succ (max_reg_function f) in mkstate st (Pos.succ st) - (Pos.succ (max_pc_function f)) + (Pos.succ (RTL.max_pc_function f)) (AssocMap.set st (None, VScalar 32) (st_scldecls (init_state st))) (st_arrdecls (init_state st)) (st_datapath (init_state st)) @@ -633,23 +650,6 @@ Definition transl_module (f : function) : Errors.res HTL.module := Definition transl_fundef := transf_partial_fundef transl_module. -(* Definition transl_program (p : RTL.program) := transform_partial_program transl_fundef p. *) - -(*Definition transl_main_fundef f : Errors.res HTL.fundef := - match f with - | Internal f => transl_fundef (Internal f) - | External f => Errors.Error (Errors.msg "Could not find internal main function") - end. - -(** Translation of a whole program. *) - -Definition transl_program (p: RTL.program) : Errors.res HTL.program := - transform_partial_program2 (fun i f => if Pos.eqb p.(AST.prog_main) i - then transl_fundef f - else transl_main_fundef f) - (fun i v => Errors.OK v) p. -*) - Definition main_is_internal (p : RTL.program) : bool := let ge := Globalenvs.Genv.globalenv p in match Globalenvs.Genv.find_symbol ge p.(AST.prog_main) with diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v index 7cb6d8c..6a10fa2 100644 --- a/src/hls/HTLgenspec.v +++ b/src/hls/HTLgenspec.v @@ -178,12 +178,12 @@ Hint Constructors tr_code : htlspec. Inductive tr_module (f : RTL.function) : module -> Prop := tr_module_intro : - forall data control fin rtrn st stk stk_len m start rst clk scldecls arrdecls wf, + forall data control fin rtrn st stk stk_len m start rst clk scldecls arrdecls wf1 wf2 wf3, m = (mkmodule f.(RTL.fn_params) data control f.(RTL.fn_entrypoint) - st stk stk_len fin rtrn start rst clk scldecls arrdecls None wf) -> + st stk stk_len fin rtrn start rst clk scldecls arrdecls None wf1 wf2 wf3) -> (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i -> tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) -> stk_len = Z.to_nat (f.(RTL.fn_stacksize) / 4) -> @@ -648,5 +648,9 @@ Proof. replace (st_datapath s10) with (st_datapath s3) by congruence. replace (st_st s10) with (st_st s3) by congruence. eapply iter_expand_instr_spec; eauto with htlspec. + rewrite H5. rewrite H7. apply EQ2. apply PTree.elements_complete. + eauto with htlspec. + erewrite <- collect_declare_freshreg_trans; try eassumption. + lia. Qed. diff --git a/src/hls/Memorygen.v b/src/hls/Memorygen.v index 87317ef..4f74b3f 100644 --- a/src/hls/Memorygen.v +++ b/src/hls/Memorygen.v @@ -39,6 +39,10 @@ Require Import vericert.hls.Array. Local Open Scope positive. Local Open Scope assocmap. +Hint Resolve max_reg_stmnt_le_stmnt_tree : mgen. +Hint Resolve max_reg_stmnt_lt_stmnt_tree : mgen. +Hint Resolve max_stmnt_lt_module : mgen. + Lemma int_eq_not_false : forall x, Int.eq x (Int.not x) = false. Proof. intros. unfold Int.eq. @@ -48,138 +52,6 @@ Proof. specialize (X (Int.unsigned x)). apply zeq_false; auto. Qed. -Definition max_pc_function (m: module) := - List.fold_left Pos.max (List.map fst (PTree.elements m.(mod_controllogic))) 1. - -Fixpoint max_reg_expr (e: expr) := - match e with - | Vlit _ => 1 - | Vvar r => r - | Vvari r e => Pos.max r (max_reg_expr e) - | Vrange r e1 e2 => Pos.max r (Pos.max (max_reg_expr e1) (max_reg_expr e2)) - | Vinputvar r => r - | Vbinop _ e1 e2 => Pos.max (max_reg_expr e1) (max_reg_expr e2) - | Vunop _ e => max_reg_expr e - | Vternary e1 e2 e3 => Pos.max (max_reg_expr e1) (Pos.max (max_reg_expr e2) (max_reg_expr e3)) - end. - -Fixpoint max_reg_stmnt (st: stmnt) := - match st with - | Vskip => 1 - | Vseq s1 s2 => Pos.max (max_reg_stmnt s1) (max_reg_stmnt s2) - | Vcond e s1 s2 => - Pos.max (max_reg_expr e) - (Pos.max (max_reg_stmnt s1) (max_reg_stmnt s2)) - | Vcase e stl None => Pos.max (max_reg_expr e) (max_reg_stmnt_expr_list stl) - | Vcase e stl (Some s) => - Pos.max (max_reg_stmnt s) - (Pos.max (max_reg_expr e) (max_reg_stmnt_expr_list stl)) - | Vblock e1 e2 => Pos.max (max_reg_expr e1) (max_reg_expr e2) - | Vnonblock e1 e2 => Pos.max (max_reg_expr e1) (max_reg_expr e2) - end -with max_reg_stmnt_expr_list (stl: stmnt_expr_list) := - match stl with - | Stmntnil => 1 - | Stmntcons e s stl' => - Pos.max (max_reg_expr e) - (Pos.max (max_reg_stmnt s) - (max_reg_stmnt_expr_list stl')) - end. - -Definition max_list := fold_right Pos.max 1. - -Definition max_stmnt_tree t := - PTree.fold (fun i _ st => Pos.max (max_reg_stmnt st) i) t 1. - -Definition max_reg_ram r := - match r with - | None => 1 - | Some ram => Pos.max (ram_mem ram) - (Pos.max (ram_en ram) - (Pos.max (ram_addr ram) - (Pos.max (ram_addr ram) - (Pos.max (ram_wr_en ram) - (Pos.max (ram_d_in ram) - (Pos.max (ram_d_out ram) (ram_u_en ram))))))) - end. - -Definition max_reg_module m := - Pos.max (max_list (mod_params m)) - (Pos.max (max_stmnt_tree (mod_datapath m)) - (Pos.max (max_stmnt_tree (mod_controllogic m)) - (Pos.max (mod_st m) - (Pos.max (mod_stk m) - (Pos.max (mod_finish m) - (Pos.max (mod_return m) - (Pos.max (mod_start m) - (Pos.max (mod_reset m) - (Pos.max (mod_clk m) (max_reg_ram (mod_ram m))))))))))). - -Lemma max_fold_lt : - forall m l n, m <= n -> m <= (fold_left Pos.max l n). -Proof. induction l; crush; apply IHl; lia. Qed. - -Lemma max_fold_lt2 : - forall (l: list (positive * stmnt)) v n, - v <= n -> - v <= fold_left (fun a p => Pos.max (max_reg_stmnt (snd p)) a) l n. -Proof. induction l; crush; apply IHl; lia. Qed. - -Lemma max_fold_lt3 : - forall (l: list (positive * stmnt)) v v', - v <= v' -> - fold_left (fun a0 p => Pos.max (max_reg_stmnt (snd p)) a0) l v - <= fold_left (fun a0 p => Pos.max (max_reg_stmnt (snd p)) a0) l v'. -Proof. induction l; crush; apply IHl; lia. Qed. - -Lemma max_fold_lt4 : - forall (l: list (positive * stmnt)) (a: positive * stmnt), - fold_left (fun a0 p => Pos.max (max_reg_stmnt (snd p)) a0) l 1 - <= fold_left (fun a0 p => Pos.max (max_reg_stmnt (snd p)) a0) l - (Pos.max (max_reg_stmnt (snd a)) 1). -Proof. intros; apply max_fold_lt3; lia. Qed. - -Lemma max_reg_stmnt_lt_stmnt_tree': - forall l (i: positive) v, - In (i, v) l -> - list_norepet (map fst l) -> - max_reg_stmnt v <= fold_left (fun a p => Pos.max (max_reg_stmnt (snd p)) a) l 1. -Proof. - induction l; crush. inv H; inv H0; simplify. apply max_fold_lt2. lia. - transitivity (fold_left (fun (a : positive) (p : positive * stmnt) => - Pos.max (max_reg_stmnt (snd p)) a) l 1). - eapply IHl; eauto. apply max_fold_lt4. -Qed. - -Lemma max_reg_stmnt_le_stmnt_tree : - forall d i v, - d ! i = Some v -> - max_reg_stmnt v <= max_stmnt_tree d. -Proof. - intros. unfold max_stmnt_tree. rewrite PTree.fold_spec. - apply PTree.elements_correct in H. - eapply max_reg_stmnt_lt_stmnt_tree'; eauto. - apply PTree.elements_keys_norepet. -Qed. -Hint Resolve max_reg_stmnt_le_stmnt_tree : mgen. - -Lemma max_reg_stmnt_lt_stmnt_tree : - forall d i v, - d ! i = Some v -> - max_reg_stmnt v < max_stmnt_tree d + 1. -Proof. intros. apply max_reg_stmnt_le_stmnt_tree in H; lia. Qed. -Hint Resolve max_reg_stmnt_lt_stmnt_tree : mgen. - -Lemma max_stmnt_lt_module : - forall m d i, - (mod_controllogic m) ! i = Some d \/ (mod_datapath m) ! i = Some d -> - max_reg_stmnt d < max_reg_module m + 1. -Proof. - inversion 1 as [ Hv | Hv ]; unfold max_reg_module; - apply max_reg_stmnt_le_stmnt_tree in Hv; lia. -Qed. -Hint Resolve max_stmnt_lt_module : mgen. - Definition transf_maps state ram in_ (dc: PTree.t stmnt * PTree.t stmnt) := match dc, in_ with | (d, c), (i, n) => @@ -194,7 +66,9 @@ Definition transf_maps state ram in_ (dc: PTree.t stmnt * PTree.t stmnt) := (PTree.set i nd d, c) else dc | Some (Vnonblock (Vvar e1) (Vvari r e2)), Some (Vnonblock (Vvar st') e3) => - if (r =? (ram_mem ram)) && (st' =? state) then + if (r =? (ram_mem ram)) && (st' =? state) && (Z.pos n <=? Int.max_unsigned)%Z + && (e1 <? state) && (max_reg_expr e2 <? state) && (max_reg_expr e3 <? state) + then let nd := Vseq (Vnonblock (Vvar (ram_u_en ram)) (Vunop Vnot (Vvar (ram_u_en ram)))) (Vseq (Vnonblock (Vvar (ram_wr_en ram)) (Vlit (ZToValue 0))) @@ -228,24 +102,6 @@ Proof. Abort. apply PTree.elements_complete in H4. Abort.*) -Definition set_mod_datapath d c wf m := - mkmodule (mod_params m) - d - c - (mod_entrypoint m) - (mod_st m) - (mod_stk m) - (mod_stk_len m) - (mod_finish m) - (mod_return m) - (mod_start m) - (mod_reset m) - (mod_clk m) - (mod_scldecls m) - (mod_arrdecls m) - (mod_ram m) - wf. - Lemma is_wf: forall A nc nd, @map_well_formed A nc /\ @map_well_formed A nd. @@ -309,13 +165,14 @@ Lemma ram_wf : x + 1 < x + 2 /\ x + 2 < x + 3 /\ x + 3 < x + 4 /\ x + 4 < x + 5 /\ x + 5 < x + 6. Proof. lia. Qed. -Definition module_ordering m := - (mod_st m <? mod_finish m) && (mod_finish m <? mod_return m) && (mod_return m <? mod_stk m) - && (mod_stk m <? mod_start m) && (mod_start m <? mod_reset m) && (mod_reset m <? mod_clk m) - && (max_stmnt_tree (mod_datapath m) <? mod_st m) - && (max_stmnt_tree (mod_controllogic m) <? mod_st m). +Lemma module_ram_wf' : + forall m addr, + addr = max_reg_module m + 1 -> + mod_clk m < addr. +Proof. unfold max_reg_module; lia. Qed. -Definition transf_module (m: module): module := +Definition transf_module (m: module): module. + refine ( let max_reg := max_reg_module m in let addr := max_reg+1 in let en := max_reg+2 in @@ -326,10 +183,9 @@ Definition transf_module (m: module): module := let new_size := (mod_stk_len m) in let ram := mk_ram new_size (mod_stk m) en u_en addr wr_en d_in d_out ltac:(eauto using ram_wf) in match transf_code (mod_st m) ram (mod_datapath m) (mod_controllogic m), - mod_ram m, - module_ordering m + mod_ram m with - | (nd, nc), None, true => + | (nd, nc), None => mkmodule m.(mod_params) nd nc @@ -351,9 +207,11 @@ Definition transf_module (m: module): module := (AssocMap.set m.(mod_stk) (None, VArray 32 (2 ^ Nat.log2_up new_size))%nat m.(mod_arrdecls)) (Some ram) - (is_wf _ nc nd) - | _, _, _ => m - end. + _ _ _ + | _, _ => m + end). apply is_wf. exact (mod_ordering_wf m). + inversion 1; subst. auto using module_ram_wf'. +Defined. Definition transf_fundef := transf_fundef transf_module. @@ -1337,7 +1195,6 @@ Hint Resolve max_module_stmnts : mgen. Lemma transf_module_code : forall m, mod_ram m = None -> - module_ordering m = true -> transf_code (mod_st m) {| ram_size := mod_stk_len m; ram_mem := mod_stk m; @@ -1354,8 +1211,8 @@ Proof. unfold transf_module; intros; repeat destruct_match; crush. Qed. Hint Resolve transf_module_code : mgen. Lemma transf_module_code_ram : - forall m r, mod_ram m = Some r \/ module_ordering m = false -> transf_module m = m. -Proof. unfold transf_module; intros; destruct H; repeat destruct_match; crush. Qed. + forall m r, mod_ram m = Some r -> transf_module m = m. +Proof. unfold transf_module; intros; repeat destruct_match; crush. Qed. Hint Resolve transf_module_code_ram : mgen. Lemma mod_reset_lt : forall m, mod_reset m < max_reg_module m + 1. @@ -2447,7 +2304,11 @@ Definition alt_load state ram d (c : AssocMap.t stmnt) d' c' i n := /\ c' ! i = Some (Vnonblock (Vvar state) (Vlit (posToValue n))) /\ c' ! n = Some (Vnonblock (Vvar state) ns) /\ c ! i = Some (Vnonblock (Vvar state) ns) - /\ d ! i = Some (Vnonblock (Vvar e1) (Vvari (ram_mem ram) e2)). + /\ d ! i = Some (Vnonblock (Vvar e1) (Vvari (ram_mem ram) e2)) + /\ e1 < state + /\ max_reg_expr e2 < state + /\ max_reg_expr ns < state + /\ (Z.pos n <= Int.max_unsigned)%Z. Definition alternatives state ram d c d' c' i n := alt_unchanged d c d' c' i @@ -2475,6 +2336,7 @@ Proof. | |- ( _ # ?s <- _ ) ! ?s = Some _ => apply AssocMap.gss | |- ( _ # ?s <- _ ) ! ?r = Some _ => rewrite AssocMap.gso by lia | |- _ = None => apply max_index_2; lia + | H: context[_ <? _] |- _ => apply Pos.ltb_lt in H end; auto. Qed. @@ -2837,7 +2699,6 @@ Lemma translation_correct : (Z.pos pstval <= 4294967295)%Z -> match_states (State sf m st asr asa) (State res' (transf_module m) st asr'0 asa'0) -> mod_ram m = None -> - module_ordering m = true -> exists R2 : state, Smallstep.plus step tge (State res' (transf_module m) st asr'0 asa'0) Events.E0 R2 /\ match_states (State sf m pstval (merge_regs nasr3 basr3) (merge_arrs nasa3 basa3)) R2. @@ -2858,10 +2719,10 @@ Proof. repeat match goal with H: _ \/ _ |- _ => inv H end. - unfold alt_unchanged in *; simplify. assert (MATCH_SIZE1: match_empty_size m nasa1 /\ match_empty_size m basa1). - { eapply match_arrs_size_stmnt_preserved2; eauto. unfold match_empty_size; mgen_crush. } + { eapply match_arrs_size_stmnt_preserved2; eauto. unfold match_empty_size; eauto with mgen. } assert (MATCH_SIZE2: match_empty_size m nasa2 /\ match_empty_size m basa2). { eapply match_arrs_size_stmnt_preserved2; mgen_crush. } simplify. - assert (MATCH_ARR3: match_arrs_size nasa2 basa2) by mgen_crush. + assert (MATCH_ARR3: match_arrs_size nasa2 basa2) by eauto with mgen. exploit match_states_same; try solve [apply H4 | eapply max_stmnt_lt_module; eauto | econstructor; eauto with mgen]; intros; repeat inv_exists; simplify; tac0. @@ -2869,27 +2730,27 @@ Proof. | econstructor; eauto with mgen]; intros; repeat inv_exists; simplify; tac0. assert (MATCH_SIZE1': match_empty_size m ran'0 /\ match_empty_size m rab'0). - { eapply match_arrs_size_stmnt_preserved2; eauto. unfold match_empty_size; mgen_crush. + { eapply match_arrs_size_stmnt_preserved2; eauto. unfold match_empty_size; eauto with mgen. rewrite empty_stack_transf; eauto with mgen. } assert (MATCH_SIZE2': match_empty_size m ran'2 /\ match_empty_size m rab'2). { eapply match_arrs_size_stmnt_preserved2; mgen_crush. } simplify. - assert (MATCH_ARR3': match_arrs_size ran'2 rab'2) by mgen_crush. + assert (MATCH_ARR3': match_arrs_size ran'2 rab'2) by eauto with mgen. do 2 econstructor. apply Smallstep.plus_one. econstructor. - mgen_crush. mgen_crush. mgen_crush. - rewrite <- H13. eassumption. rewrite <- H7. eassumption. - eauto. mgen_crush. eauto. - rewrite empty_stack_transf. unfold transf_module; repeat destruct_match; crush. + eauto with mgen. eauto with mgen. eauto with mgen. + rewrite <- H12. eassumption. rewrite <- H7. eassumption. + eauto. eauto with mgen. eauto. + rewrite empty_stack_transf. unfold transf_module; repeat destruct_match; try discriminate. econstructor. simplify. unfold disable_ram in *. unfold transf_module in DISABLE_RAM. - repeat destruct_match; crush. - pose proof H18 as R1. apply max_reg_stmnt_not_modified with (r := max_reg_module m + 2) in R1. - pose proof H18 as R2. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 2) in R2. - pose proof H19 as R3. eapply max_reg_stmnt_not_modified with (r := max_reg_module m + 2) in R3. - pose proof H19 as R4. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 2) in R4. - pose proof H18 as R1'. apply max_reg_stmnt_not_modified with (r := max_reg_module m + 6) in R1'. - pose proof H18 as R2'. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 6) in R2'. - pose proof H19 as R3'. eapply max_reg_stmnt_not_modified with (r := max_reg_module m + 6) in R3'. - pose proof H19 as R4'. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 6) in R4'. + repeat destruct_match; try discriminate; []. inv Heqp. simplify. + pose proof H17 as R1. apply max_reg_stmnt_not_modified with (r := max_reg_module m + 2) in R1. + pose proof H17 as R2. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 2) in R2. + pose proof H18 as R3. eapply max_reg_stmnt_not_modified with (r := max_reg_module m + 2) in R3. + pose proof H18 as R4. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 2) in R4. + pose proof H17 as R1'. apply max_reg_stmnt_not_modified with (r := max_reg_module m + 6) in R1'. + pose proof H17 as R2'. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 6) in R2'. + pose proof H18 as R3'. eapply max_reg_stmnt_not_modified with (r := max_reg_module m + 6) in R3'. + pose proof H18 as R4'. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 6) in R4'. simplify. pose proof DISABLE_RAM as DISABLE_RAM1. eapply int_eq_not_changed with (ar' := rab') in DISABLE_RAM; try congruence. @@ -2905,18 +2766,18 @@ Proof. eapply max_reg_module_datapath_gt; eauto; remember (max_reg_module m); lia. eapply max_reg_module_controllogic_gt; eauto; remember (max_reg_module m); lia. eapply max_reg_module_controllogic_gt; eauto; remember (max_reg_module m); lia. - auto. auto. mgen_crush. auto. + auto. auto. eauto with mgen. auto. econstructor; mgen_crush. apply merge_arr_empty; mgen_crush. unfold disable_ram in *. unfold transf_module in DISABLE_RAM. repeat destruct_match; crush. unfold transf_module in Heqo; repeat destruct_match; crush. - pose proof H18 as R1. apply max_reg_stmnt_not_modified with (r := max_reg_module m + 2) in R1. - pose proof H18 as R2. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 2) in R2. - pose proof H19 as R3. eapply max_reg_stmnt_not_modified with (r := max_reg_module m + 2) in R3. - pose proof H19 as R4. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 2) in R4. - pose proof H18 as R1'. apply max_reg_stmnt_not_modified with (r := max_reg_module m + 6) in R1'. - pose proof H18 as R2'. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 6) in R2'. - pose proof H19 as R3'. eapply max_reg_stmnt_not_modified with (r := max_reg_module m + 6) in R3'. - pose proof H19 as R4'. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 6) in R4'. + pose proof H17 as R1. apply max_reg_stmnt_not_modified with (r := max_reg_module m + 2) in R1. + pose proof H17 as R2. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 2) in R2. + pose proof H18 as R3. eapply max_reg_stmnt_not_modified with (r := max_reg_module m + 2) in R3. + pose proof H18 as R4. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 2) in R4. + pose proof H17 as R1'. apply max_reg_stmnt_not_modified with (r := max_reg_module m + 6) in R1'. + pose proof H17 as R2'. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 6) in R2'. + pose proof H18 as R3'. eapply max_reg_stmnt_not_modified with (r := max_reg_module m + 6) in R3'. + pose proof H18 as R4'. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 6) in R4'. simplify. pose proof DISABLE_RAM as DISABLE_RAM1. eapply int_eq_not_changed with (ar' := rab') in DISABLE_RAM; try congruence. @@ -2932,33 +2793,34 @@ Proof. eapply max_reg_module_datapath_gt; eauto; remember (max_reg_module m); lia. eapply max_reg_module_controllogic_gt; eauto; remember (max_reg_module m); lia. eapply max_reg_module_controllogic_gt; eauto; remember (max_reg_module m); lia. - - unfold alt_store in *; simplify. inv H6. inv H20. inv H20. simplify. + - unfold alt_store in *; simplify. inv H6. inv H19. inv H19. simplify. exploit match_states_same; try solve [eapply H4 | eapply max_stmnt_lt_module; eauto | econstructor; eauto with mgen]; intros; repeat inv_exists; simplify; tac0. - do 2 econstructor. apply Smallstep.plus_one. econstructor. mgen_crush. mgen_crush. - mgen_crush. rewrite H7. eassumption. eassumption. eassumption. mgen_crush. + do 2 econstructor. apply Smallstep.plus_one. econstructor. solve [eauto with mgen]. solve [eauto with mgen]. + solve [eauto with mgen]. + rewrite H7. eassumption. eassumption. eassumption. solve [eauto with mgen]. econstructor. econstructor. econstructor. econstructor. econstructor. - simplify. auto. auto. auto. econstructor. econstructor. econstructor. + auto. auto. auto. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. - simplify. eapply expr_runp_matches2. eassumption. 2: { eassumption. } + eapply expr_runp_matches2. eassumption. 2: { eassumption. } pose proof H3 as X. apply max_reg_stmnt_le_stmnt_tree in X. apply expr_lt_max_module_datapath in X; simplify; remember (max_reg_module m); lia. auto. - econstructor. econstructor. simplify. eapply expr_runp_matches2; eauto. + econstructor. econstructor. eapply expr_runp_matches2; eauto. pose proof H3 as X. apply max_reg_stmnt_le_stmnt_tree in X. apply expr_lt_max_module_datapath in X. remember (max_reg_module m); simplify; lia. - simplify. rewrite empty_stack_transf. + rewrite empty_stack_transf. unfold transf_module; repeat destruct_match; try discriminate; simplify; []. eapply exec_ram_Some_write. 3: { simplify. unfold merge_regs. repeat rewrite AssocMapExt.merge_add_assoc. repeat rewrite find_assocmap_gso by lia. - pose proof H13 as X. + pose proof H12 as X. eapply max_reg_stmnt_not_modified_nb with (r := (max_reg_module m + 2)) in X. - simplify. rewrite AssocMap.gempty in X. + rewrite AssocMap.gempty in X. apply merge_find_assocmap. auto. apply max_reg_stmnt_le_stmnt_tree in H2. apply expr_lt_max_module_controllogic in H2. lia. @@ -2969,19 +2831,19 @@ Proof. } { unfold disable_ram in *. unfold transf_module in DISABLE_RAM; repeat destruct_match; try discriminate. - simplify. inv Heqp. - pose proof H13 as X2. - pose proof H13 as X4. + inv Heqp. + pose proof H12 as X2. + pose proof H12 as X4. apply max_reg_stmnt_not_modified with (r := max_reg_module m + 2) in X2. - apply max_reg_stmnt_not_modified with (r := max_reg_module m + 6) in X4. simplify. + apply max_reg_stmnt_not_modified with (r := max_reg_module m + 6) in X4. assert (forall ar ar' x, ar ! x = ar' ! x -> ar # x = ar' # x). { intros. unfold find_assocmap, AssocMapExt.get_default. rewrite H6. auto. } - apply H6 in X2. apply H6 in X4. rewrite <- X2. rewrite <- X4. + apply H6 in X2. apply H6 in X4. simplify. rewrite <- X2. rewrite <- X4. apply int_eq_not. auto. apply max_reg_stmnt_le_stmnt_tree in H2. - apply expr_lt_max_module_controllogic in H2. remember (max_reg_module m). lia. + apply expr_lt_max_module_controllogic in H2. simplify. remember (max_reg_module m). lia. apply max_reg_stmnt_le_stmnt_tree in H2. - apply expr_lt_max_module_controllogic in H2. remember (max_reg_module m). lia. + apply expr_lt_max_module_controllogic in H2. simplify. remember (max_reg_module m). lia. } 2: { simplify. unfold merge_regs. repeat rewrite AssocMapExt.merge_add_assoc. @@ -3003,10 +2865,10 @@ Proof. unfold transf_module; repeat destruct_match; try discriminate; simplify. replace (AssocMapExt.merge value ran' rab') with (merge_regs ran' rab'); [|unfold merge_regs; auto]. - pose proof H20 as X. + pose proof H19 as X. eapply match_assocmaps_merge in X. - 2: { apply H22. } - inv X. rewrite <- H12. eassumption. unfold transf_module in H6; repeat destruct_match; + 2: { apply H21. } + inv X. rewrite <- H14. eassumption. unfold transf_module in H6; repeat destruct_match; try discriminate; simplify. lia. auto. @@ -3014,7 +2876,7 @@ Proof. rewrite AssocMapExt.merge_base_1. remember (max_reg_module m). repeat (apply match_assocmaps_gt; [lia|]). - mgen_crush. + solve [eauto with mgen]. apply merge_arr_empty. apply match_empty_size_merge. apply match_empty_assocmap_set. @@ -3023,9 +2885,9 @@ Proof. apply match_arrs_merge_set2; auto. eapply match_arrs_size_stmnt_preserved in H4; mgen_crush. eapply match_arrs_size_stmnt_preserved in H4; mgen_crush. - eapply match_arrs_size_stmnt_preserved in H13; mgen_crush. + eapply match_arrs_size_stmnt_preserved in H12; mgen_crush. rewrite empty_stack_transf. mgen_crush. - eapply match_arrs_size_stmnt_preserved in H13; mgen_crush. + eapply match_arrs_size_stmnt_preserved in H12; mgen_crush. rewrite empty_stack_transf. mgen_crush. auto. apply merge_arr_empty_match. @@ -3033,7 +2895,7 @@ Proof. eapply match_arrs_size_stmnt_preserved in H4; mgen_crush. eapply match_arrs_size_stmnt_preserved in H4; mgen_crush. apply match_empty_size_merge. apply match_empty_assocmap_set. - mgen_crush. eapply match_arrs_size_stmnt_preserved in H13; mgen_crush. + mgen_crush. eapply match_arrs_size_stmnt_preserved in H12; mgen_crush. rewrite empty_stack_transf; mgen_crush. unfold disable_ram. unfold transf_module; repeat destruct_match; try discriminate; simplify. unfold merge_regs. unfold_merge. @@ -3042,19 +2904,22 @@ Proof. repeat rewrite find_assocmap_gso by lia. rewrite find_assocmap_gss. apply Int.eq_true. - unfold alt_load in *; simplify. inv H6. - 2: { inv H23. } - inv H23. inv H27. simplify. inv H4. - 2: { inv H24. } - inv H24. + 2: { match goal with H: context[location_is] |- _ => inv H end. } + match goal with H: context[location_is] |- _ => inv H end. + inv H30. simplify. inv H4. + 2: { match goal with H: context[location_is] |- _ => inv H end. } + inv H27. simplify. do 2 econstructor. eapply Smallstep.plus_two. econstructor. mgen_crush. mgen_crush. mgen_crush. eassumption. - eassumption. econstructor. simplify. econstructor. econstructor. simplify. - mgen_crush. econstructor. econstructor. simplify. econstructor. simplify. + eassumption. econstructor. simplify. econstructor. econstructor. + solve [eauto with mgen]. econstructor. econstructor. econstructor. econstructor. econstructor. auto. auto. auto. - econstructor. econstructor. simplify. econstructor. simplify. - econstructor. econstructor. econstructor. simplify. eapply expr_runp_matches2; eauto. + econstructor. econstructor. econstructor. + econstructor. econstructor. econstructor. eapply expr_runp_matches2; auto. eassumption. + 2: { eassumption. } pose proof H3 as X. apply max_reg_stmnt_le_stmnt_tree in X. apply expr_lt_max_module_datapath in X. simplify. remember (max_reg_module m); lia. + auto. simplify. rewrite empty_stack_transf. unfold transf_module; repeat destruct_match; crush. eapply exec_ram_Some_read; simplify. @@ -3070,7 +2935,7 @@ Proof. repeat destruct_match; try discriminate. simplify. apply int_eq_not. auto. } { unfold merge_regs; unfold_merge. repeat rewrite AssocMap.gso by lia. apply AssocMap.gss. } { unfold merge_regs; unfold_merge. apply AssocMap.gss. } - { eapply match_arrs_read. apply H23. mgen_crush. } + { eapply match_arrs_read. eassumption. mgen_crush. } { crush. } { crush. } { unfold merge_regs. unfold_merge. @@ -3080,7 +2945,7 @@ Proof. remember (max_reg_module m). repeat rewrite AssocMap.gso by lia. apply AssocMap.gss. } - { assert (Z.pos x <= Int.max_unsigned)%Z by admit; auto. } + { auto. } { econstructor. { unfold merge_regs. unfold_merge. @@ -3088,26 +2953,26 @@ Proof. { unfold max_reg_module; lia. } unfold transf_module; repeat destruct_match; try discriminate; simplify. assert (mod_st m < mod_reset m). - { unfold module_ordering in *. simplify. + { pose proof (mod_ordering_wf m); unfold module_ordering in *. simplify. repeat match goal with | H: context[_ <? _] |- _ => apply Pos.ltb_lt in H end; lia. } repeat rewrite AssocMap.gso by lia. - inv ASSOC. rewrite <- H12. auto. lia. + inv ASSOC. rewrite <- H19. auto. lia. } { unfold merge_regs. unfold_merge. assert (mod_finish m < max_reg_module m + 1). { unfold max_reg_module; lia. } unfold transf_module; repeat destruct_match; try discriminate; simplify. assert (mod_st m < mod_finish m). - { unfold module_ordering in *. simplify. + { pose proof (mod_ordering_wf m). unfold module_ordering in *. simplify. repeat match goal with | H: context[_ <? _] |- _ => apply Pos.ltb_lt in H end; lia. } repeat rewrite AssocMap.gso by lia. - inv ASSOC. rewrite <- H12. auto. lia. + inv ASSOC. rewrite <- H19. auto. lia. } { unfold merge_regs. unfold_merge. assert (mod_st m < max_reg_module m + 1). @@ -3340,9 +3205,7 @@ Section CORRECTNESS. end. induction 1; destruct (mod_ram m) eqn:RAM; simplify; repeat transf_step_correct_assum; repeat transf_step_correct_tac. - - assert (RAM0: transf_module m = m). - { eapply transf_module_code_ram. left. eassumption. } - assert (MATCH_SIZE1: match_empty_size m nasa1 /\ match_empty_size m basa1). + - assert (MATCH_SIZE1: match_empty_size m nasa1 /\ match_empty_size m basa1). { eapply match_arrs_size_stmnt_preserved2; eauto. unfold match_empty_size; mgen_crush. } simplify. assert (MATCH_SIZE2: match_empty_size m nasa2 /\ match_empty_size m basa2). @@ -3353,17 +3216,17 @@ Section CORRECTNESS. assert (MATCH_ARR3: match_arrs_size nasa3 basa3) by mgen_crush. exploit match_states_same. apply H4. eauto with mgen. econstructor; eauto. econstructor; eauto. econstructor; eauto. econstructor; eauto. - intros. repeat inv_exists. simplify. inv H17. inv H20. + intros. repeat inv_exists. simplify. inv H18. inv H21. exploit match_states_same. apply H6. eauto with mgen. - econstructor; eauto. econstructor; eauto. intros. repeat inv_exists. simplify. inv H17. inv H22. + econstructor; eauto. econstructor; eauto. intros. repeat inv_exists. simplify. inv H18. inv H23. exploit exec_ram_same; eauto. eauto with mgen. econstructor. eapply match_assocmaps_merge; eauto. eauto with mgen. econstructor. apply match_arrs_merge; eauto with mgen. eauto with mgen. - intros. repeat inv_exists. simplify. inv H17. inv H27. + intros. repeat inv_exists. simplify. inv H18. inv H28. econstructor; simplify. apply Smallstep.plus_one. econstructor. mgen_crush. mgen_crush. mgen_crush. rewrite RAM0; eassumption. rewrite RAM0; eassumption. - rewrite RAM0. eassumption. mgen_crush. eassumption. rewrite RAM0 in H20. rewrite RAM0. + rewrite RAM0. eassumption. mgen_crush. eassumption. rewrite RAM0 in H21. rewrite RAM0. rewrite RAM. eassumption. eauto. eauto. eauto with mgen. eauto. econstructor. mgen_crush. apply match_arrs_merge; mgen_crush. eauto. apply match_empty_size_merge; mgen_crush; mgen_crush. @@ -3379,16 +3242,14 @@ Section CORRECTNESS. apply match_empty_size_merge; mgen_crush; mgen_crush. unfold disable_ram. unfold transf_module; repeat destruct_match; crush. - apply exec_ram_resets_en in H20. unfold merge_reg_assocs in H20. + apply exec_ram_resets_en in H21. unfold merge_reg_assocs in H21. simplify. auto. auto. - - eapply translation_correct; eauto. admit. + - eapply translation_correct; eauto. - do 2 econstructor. apply Smallstep.plus_one. apply step_finish; mgen_crush. constructor; eauto. - do 2 econstructor. apply Smallstep.plus_one. apply step_finish; mgen_crush. econstructor; eauto. - - assert (RAM0: transf_module m = m). - { eapply transf_module_code_ram. left. eassumption. } - econstructor. econstructor. apply Smallstep.plus_one. econstructor. + - econstructor. econstructor. apply Smallstep.plus_one. econstructor. replace (mod_entrypoint (transf_module m)) with (mod_entrypoint m) by (rewrite RAM0; auto). replace (mod_reset (transf_module m)) with (mod_reset m) by (rewrite RAM0; auto). replace (mod_finish (transf_module m)) with (mod_finish m) by (rewrite RAM0; auto). @@ -3411,12 +3272,10 @@ Section CORRECTNESS. unfold find_assocmap, AssocMapExt.get_default. destruct_match. rewrite AssocMap.gso in Heqo by admit. rewrite AssocMap.gso in Heqo by admit. rewrite AssocMap.gso in Heqo by admit. admit. admit. - - assert (RAM0: transf_module m = m). - { eapply transf_module_code_ram. left. eassumption. } - inv STACKS. destruct b1; subst. + - inv STACKS. destruct b1; subst. econstructor. econstructor. apply Smallstep.plus_one. econstructor. eauto. - clear Learn. inv H0. inv H2. inv STACKS. inv H2. constructor. + clear Learn. inv H0. inv H3. inv STACKS. inv H3. constructor. constructor. intros. rewrite RAM0. destruct (Pos.eq_dec r res); subst. @@ -3428,11 +3287,20 @@ Section CORRECTNESS. rewrite AssocMap.gss. rewrite AssocMap.gss. auto. rewrite AssocMap.gso; auto. - symmetry. rewrite AssocMap.gso; auto. inv MATCH_ASSOC0. apply H0. auto. + symmetry. rewrite AssocMap.gso; auto. inv MATCH_ASSOC0. apply H1. auto. auto. auto. auto. auto. rewrite RAM0. rewrite RAM. rewrite RAM0 in DISABLE_RAM. rewrite RAM in DISABLE_RAM. - apply disable_ram_set_gso. - apply disable_ram_set_gso. auto. admit. admit. admit. admit. + apply disable_ram_set_gso + apply disable_ram_set_gso. auto. + pose proof (mod_ordering_wf m); unfold module_ordering in *. + pose proof (ram_ordering r0). simplify. + pose proof (mod_ram_wf m r0 H). lia. + pose proof (mod_ordering_wf m); unfold module_ordering in *. + pose proof (ram_ordering r0). simplify. + pose proof (mod_ram_wf m r0 H). lia. + pose proof (mod_ordering_wf m); unfold module_ordering in *. + pose proof (ram_ordering r0). simplify. + pose proof (mod_ram_wf m r0 H). - inv STACKS. destruct b1; subst. econstructor. econstructor. apply Smallstep.plus_one. econstructor. eauto. diff --git a/src/hls/Verilog.v b/src/hls/Verilog.v index 46a9674..1dc7e99 100644 --- a/src/hls/Verilog.v +++ b/src/hls/Verilog.v @@ -821,3 +821,40 @@ Proof. - red; simplify; intro; invert H0; invert H; crush. - invert H; invert H0; crush. Qed. + +Local Open Scope positive. + +Fixpoint max_reg_expr (e: expr) := + match e with + | Vlit _ => 1 + | Vvar r => r + | Vvari r e => Pos.max r (max_reg_expr e) + | Vrange r e1 e2 => Pos.max r (Pos.max (max_reg_expr e1) (max_reg_expr e2)) + | Vinputvar r => r + | Vbinop _ e1 e2 => Pos.max (max_reg_expr e1) (max_reg_expr e2) + | Vunop _ e => max_reg_expr e + | Vternary e1 e2 e3 => Pos.max (max_reg_expr e1) (Pos.max (max_reg_expr e2) (max_reg_expr e3)) + end. + +Fixpoint max_reg_stmnt (st: stmnt) := + match st with + | Vskip => 1 + | Vseq s1 s2 => Pos.max (max_reg_stmnt s1) (max_reg_stmnt s2) + | Vcond e s1 s2 => + Pos.max (max_reg_expr e) + (Pos.max (max_reg_stmnt s1) (max_reg_stmnt s2)) + | Vcase e stl None => Pos.max (max_reg_expr e) (max_reg_stmnt_expr_list stl) + | Vcase e stl (Some s) => + Pos.max (max_reg_stmnt s) + (Pos.max (max_reg_expr e) (max_reg_stmnt_expr_list stl)) + | Vblock e1 e2 => Pos.max (max_reg_expr e1) (max_reg_expr e2) + | Vnonblock e1 e2 => Pos.max (max_reg_expr e1) (max_reg_expr e2) + end +with max_reg_stmnt_expr_list (stl: stmnt_expr_list) := + match stl with + | Stmntnil => 1 + | Stmntcons e s stl' => + Pos.max (max_reg_expr e) + (Pos.max (max_reg_stmnt s) + (max_reg_stmnt_expr_list stl')) + end. diff --git a/src/hls/Veriloggenproof.v b/src/hls/Veriloggenproof.v index ccc0688..b621632 100644 --- a/src/hls/Veriloggenproof.v +++ b/src/hls/Veriloggenproof.v @@ -421,8 +421,8 @@ Section CORRECTNESS. econstructor. econstructor. eapply transl_list_correct. - intros. split. lia. pose proof (HTL.mod_wf m) as HP. destruct HP as [_ HP]. auto. - apply Maps.PTree.elements_keys_norepet. eassumption. + intros. split. lia. pose proof (HTL.mod_wf m) as HP. destruct HP as [_ HP]. + auto. apply Maps.PTree.elements_keys_norepet. eassumption. 2: { apply valueToPos_inj. apply unsigned_posToValue_le. eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. split. lia. apply HP. eassumption. eassumption. @@ -468,7 +468,8 @@ Section CORRECTNESS. econstructor. econstructor. eapply transl_list_correct. - intros. split. lia. pose proof (HTL.mod_wf m) as HP. destruct HP as [_ HP]. auto. + intros. split. lia. pose proof (HTL.mod_wf m) as HP. + destruct HP as [_ HP]; auto. apply Maps.PTree.elements_keys_norepet. eassumption. 2: { apply valueToPos_inj. apply unsigned_posToValue_le. eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. |