Add beginning to memory generation proof

1 files changed, 53 insertions, 53 deletions

diff --git a/src/hls/HTL.v b/src/hls/HTL.v
index 4e3687a..8cebbfd 100644
--- a/src/hls/HTL.v
+++ b/src/hls/HTL.v
@@ -28,21 +28,18 @@ Require Import compcert.lib.Integers.
 Require Import compcert.lib.Maps.
 
 Require Import vericert.common.Vericertlib.
+Require Import vericert.hls.ValueInt.
+Require Import vericert.hls.AssocMap.
 Require Import vericert.hls.Array.
-Require Import vericert.hls.FunctionalUnits.
 Require vericert.hls.Verilog.
-Require Import AssocMap.
-Require Import ValueInt.
 
 Local Open Scope positive.
 
-(*|
-The purpose of the hardware transfer language (HTL) is to create a more
+(** 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
 instantiations and that we now describe a state machine instead of a
-control-flow graph.
-|*)
+control-flow graph. *)
 
 Local Open Scope assocmap.
 
@@ -57,6 +54,24 @@ Definition map_well_formed {A : Type} (m : PTree.t A) : Prop :=
     In p0 (map fst (Maps.PTree.elements m)) ->
     (Z.pos p0 <= Integers.Int.max_unsigned)%Z.
 
+Record ram := mk_ram {
+  ram_size: nat;
+  ram_mem: reg;
+  ram_en: reg;
+  ram_u_en: reg;
+  ram_addr: reg;
+  ram_wr_en: reg;
+  ram_d_in: reg;
+  ram_d_out: reg;
+  ram_ordering: (ram_addr < ram_en
+                 /\ ram_en < ram_d_in
+                 /\ ram_d_in < ram_d_out
+                 /\ ram_d_out < ram_wr_en
+                 /\ 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;
@@ -64,6 +79,8 @@ Record module: Type :=
     mod_controllogic : controllogic;
     mod_entrypoint : node;
     mod_st : reg;
+    mod_stk : reg;
+    mod_stk_len : nat;
     mod_finish : reg;
     mod_return : reg;
     mod_start : reg;
@@ -71,7 +88,11 @@ Record module: Type :=
     mod_clk : reg;
     mod_scldecls : AssocMap.t (option Verilog.io * Verilog.scl_decl);
     mod_arrdecls : AssocMap.t (option Verilog.io * Verilog.arr_decl);
-    mod_ram : ram;
+    mod_ram : option ram;
+    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';
+    mod_params_wf : Forall (Pos.gt mod_st) mod_params;
   }.
 
 Definition fundef := AST.fundef module.
@@ -85,12 +106,9 @@ Fixpoint init_regs (vl : list value) (rl : list reg) {struct rl} :=
   end.
 
 Definition empty_stack (m : module) : Verilog.assocmap_arr :=
-  (AssocMap.set m.(mod_ram).(ram_mem) (Array.arr_repeat None m.(mod_ram).(ram_size)) (AssocMap.empty Verilog.arr)).
+  (AssocMap.set m.(mod_stk) (Array.arr_repeat None m.(mod_stk_len)) (AssocMap.empty Verilog.arr)).
 
-(*|
-Operational Semantics
-=====================
-|*)
+(** * Operational Semantics *)
 
 Definition genv := Globalenvs.Genv.t fundef unit.
 
@@ -119,13 +137,13 @@ Inductive state : Type :=
            (args : list value), state.
 
 Inductive exec_ram:
-  Verilog.reg_associations -> Verilog.arr_associations -> ram ->
+  Verilog.reg_associations -> Verilog.arr_associations -> option ram ->
   Verilog.reg_associations -> Verilog.arr_associations -> Prop :=
 | exec_ram_Some_idle:
     forall ra ar r,
       Int.eq (Verilog.assoc_blocking ra)#(ram_en r, 32)
              (Verilog.assoc_blocking ra)#(ram_u_en r, 32) = true ->
-      exec_ram ra ar r ra ar
+      exec_ram ra ar (Some r) ra ar
 | exec_ram_Some_write:
     forall ra ar r d_in addr en wr_en u_en,
       Int.eq en u_en = false ->
@@ -135,7 +153,7 @@ Inductive exec_ram:
       (Verilog.assoc_blocking ra)!(ram_wr_en r) = Some wr_en ->
       (Verilog.assoc_blocking ra)!(ram_d_in r) = Some d_in ->
       (Verilog.assoc_blocking ra)!(ram_addr r) = Some addr ->
-      exec_ram ra ar r (Verilog.nonblock_reg (ram_en r) ra u_en)
+      exec_ram ra ar (Some r) (Verilog.nonblock_reg (ram_en r) ra u_en)
                (Verilog.nonblock_arr (ram_mem r) (valueToNat addr) ar d_in)
 | exec_ram_Some_read:
     forall ra ar r addr v_d_out en u_en,
@@ -146,8 +164,11 @@ Inductive exec_ram:
       (Verilog.assoc_blocking ra)!(ram_addr r) = Some addr ->
       Verilog.arr_assocmap_lookup (Verilog.assoc_blocking ar)
                                   (ram_mem r) (valueToNat addr) = Some v_d_out ->
-      exec_ram ra ar r (Verilog.nonblock_reg (ram_en r)
-                               (Verilog.nonblock_reg (ram_d_out r) ra v_d_out) u_en) ar.
+      exec_ram ra ar (Some r) (Verilog.nonblock_reg (ram_en r)
+                               (Verilog.nonblock_reg (ram_d_out r) ra v_d_out) u_en) ar
+| exec_ram_None:
+    forall r a,
+      exec_ram r a None r a.
 
 Inductive step : genv -> state -> Events.trace -> state -> Prop :=
 | step_module :
@@ -225,10 +246,6 @@ Definition semantics (m : program) :=
   Smallstep.Semantics step (initial_state m) final_state
                       (Globalenvs.Genv.globalenv m).
 
-Definition all_module_regs m :=
-  all_ram_regs (mod_ram m) ++
-               (mod_st m::mod_finish m::mod_return m::mod_start m::mod_reset m::mod_clk m::nil).
-
 Definition max_pc_function (m: module) :=
   List.fold_left Pos.max (List.map fst (PTree.elements m.(mod_controllogic))) 1.
 
@@ -249,20 +266,17 @@ Definition max_reg_ram r :=
                      (Pos.max (ram_d_out ram) (ram_u_en ram)))))))
   end.
 
-Definition max_reg_body m :=
-  Pos.max (max_list (mod_params m))
-          (Pos.max (max_stmnt_tree (mod_datapath m))
-                   (max_stmnt_tree (mod_controllogic m))).
-
 Definition max_reg_module m :=
-  Pos.max (max_reg_body m) (max_list (all_module_regs m)).
-
-Record wf_htl_module m :=
-  mk_wf_htl_module {
-      mod_wf : map_well_formed (mod_controllogic m) /\ map_well_formed (mod_datapath m);
-      mod_ordering_wf : list_norepet (all_module_regs m);
-      mod_gt : Forall (Pos.lt (max_reg_body m)) (all_module_regs 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).
@@ -319,16 +333,12 @@ Proof. intros. apply max_reg_stmnt_le_stmnt_tree in H; lia. Qed.
 
 Lemma max_stmnt_lt_module :
   forall m d i,
-    wf_htl_module m ->
     (mod_controllogic m) ! i = Some d \/ (mod_datapath m) ! i = Some d ->
     Verilog.max_reg_stmnt d < max_reg_module m + 1.
 Proof.
-  intros. apply mod_gt in H.
-  unfold Pos.lt, max_reg_body, max_reg_module, max_list, all_module_regs, all_ram_regs in *.
-  simplify.
-  repeat match goal with H: Forall _ _ |- _ => inv H end.
-  inversion H0 as [Hv | Hv]; apply max_reg_stmnt_le_stmnt_tree in Hv.
-  Admitted.
+  inversion 1 as [ Hv | Hv ]; unfold max_reg_module;
+  apply max_reg_stmnt_le_stmnt_tree in Hv; lia.
+Qed.
 
 Lemma max_list_correct l st : st > max_list l -> Forall (Pos.gt st) l.
 Proof. induction l; crush; constructor; [|apply IHl]; lia. Qed.
@@ -341,14 +351,4 @@ Definition max_list_dec (l: list reg) (st: reg) : {Forall (Pos.gt st) l} + {True
       end
     ); auto.
   apply max_list_correct. apply Pos.ltb_lt in e. lia.
-Defined.
-
-Variant wf_htl_fundef: fundef -> Prop :=
-  | wf_htl_fundef_external: forall ef,
-      wf_htl_fundef (AST.External ef)
-  | wf_htl_function_internal: forall f,
-      wf_htl_module f ->
-      wf_htl_fundef (AST.Internal f).
-
-Definition wf_htl_program (p: program) : Prop :=
-  forall f id, In (id, AST.Gfun f) (AST.prog_defs p) -> wf_htl_fundef f.
+Qed.